| Age | Commit message (Collapse) | Author |
|---|
|
This commit removes the old bit-vector solver code.
|
|
PR #6848 disabled relevancy order by default, but for QF_NIA, it helps
us solve significantly more benchmarks (17525 vs. 16889 with a 20 minute
timeout using the updated SMT-COMP script). This also updates the
options for `QF_AUFBV` and `QF_ALIA` to use `--decision=stoponly`,
following the name change of the option.
|
|
This introduces a new versioning mechanism that allows for better automation.
|
|
PR #7219 removed CVC language support and therefore also the file src/parser/cvc/Cvc.g. This commit fixes the check (and the nightlies).
|
|
|
|
This commit copies the run-script-smtcomp-current* scripts to run-script-smtcomp2021* to archive them.
|
|
This commit:
- Disables `--tear-down-incremental=X` for the competition since
it currently does not work correctly on master and a fixed version did
not show significant benefits.
- Changes the occurrences of `--nl-ext` to `--nl-ext=full` because it
is now a mode option.
- Removes the use of `--bv-assert-input` because the option currently
has some issues in incremental mode (#6738)
- Removes the use of `--bitblast=eager` for the model validation track
because it produces invalid models (#6741)
|
|
|
|
This commit removes obsolete options for BV and strings logics, and
updates QF_NIA to spend more time on our best configuration.
Co-authored-by: Gereon Kremer nafur42@gmail.com
Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
|
|
This commit removes some of the options in the run scripts that are not
supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of
those options are effectively enabled by default in cvc5.
|
|
This enables the new implementation of justification heuristic by default.
Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.
|
|
Covers improvements to quantifiers.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
|
|
Refactors GMP and libpoly to also use external projects and be available within cmake as proper targets.
|
|
This PR refactors how we obtain, build and use the external SAT solvers used by CVC4: CaDiCaL, CryptoMiniSat and Kissat.
All three contrib scripts are removed and instead an external project is integrated into the cmake find scripts.
|
|
This PR refactors the contrib script to download SymFPU to a cmake external project.
|
|
This PR refactors our first, and arguably most fragile, dependency.
Right now all dependencies need to be manually installed (by calling the appropriate contrib/get-X script). For optional dependencies, we additionally need to enable them when calling the configure script (or via ccmake).
This PR is the first step in refactoring all dependencies to be automatically build (if required) as an external project.
Note that this not only eliminates the need to call contrib scripts, but also simplifies cross compilation: as all dependencies are now built within the build folders, every build folder has its own copy which may use different toolchains.
|
|
This PR further decouples LFSC from the remaining build system, but makes it more convenient to use at the same time.
The contrib/get-lfsc-checker script is now completely standalone and installs LFSC and the necessary signatures to deps/, as well as wrapper scripts to conveniently run lfscc from there and directly check cvc4 proofs.
The goal would be to automatically use LFSC in our regressions as well.
|
|
Cryptominisat supports writing statistics to a sqlite3 database, and automatically enabled it when it can find sqlite bindings.
This disables sqlite3, as we don't need it anyway.
Fixes #6131.
|
|
Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
|
|
|
|
On some systems HOST is set by default to the host name. This commit adds a --host option for the get-antlr-3.4 and get-gmp-dev scripts. It further simplifies the machine type check in get-antlr-3.4 and updates the GMP version to 6.2.1.
|
|
This commit adds support for cross-compiling for aarch64 platforms and simplifies cross-compilation handling for Windows. The configure script now automatically downloads and cross-compiles the required dependencies ANTLR3 and GMP when passing option --arm64 or --win64.
Fixes #1479 #5769.
|
|
When updating the copyright headers file permissions were not preserved. In some cases this results in losing the permission to execute scripts. This commit makes sure to preserve the file permissions for updated files.
|
|
The main goal of the resource limitation mechanism (via `--rlimit`) is to have a deterministic limitation on runtime. The ultimate goal would be that the actual runtime grows linearly with the spent resources.
To achieve this, this PR does the following:
- introduce new resources spent in places that are not yet covered
- find resource weights that best approximate the runtime
It provides a contrib script `learn_resource_weights.py` that uses statistics from a given benchmark run and uses linear regression to find good resource weights. The script also evaluates this estimate and identifies outliers, benchmarks for which this approximation is particularly bad. This probably indicates that on such a benchmark, some part of the code takes a significant amount of time but is not yet represented by a resource.
Eventually, we should use the resulting resource weights as defaults for the options like `--rewrite-step`, `--theory-check-step`, etc.
|
|
I chose commit 61ef1dc55d2bc909656f905699b28c99ddcfc518,
which is missing:
any changes to the OSX build process
(We're still figuring this out)
change to top-level identifier shadowing
(we have a few versions of the signatures floating around, and I
worry that they may not all be fixed w.r.t. no re-using identifiers)
|
|
This automatically removes dependency directories for scripts that get
external dependencies instead of aborting with an error.
|
|
On OSX there is another libtoolize tool already available.
The gnu libtoolize version installed with MacPorts or brew is called glibtoolize.
This change makes it easier to run the file on OSX.
Signed-off-by: Malte Mues (mail.mues@gmail.com)
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
on GitHub (#4989)
Signed-off-by: Malte Mues (mail.mues@gmail.com)
|
|
release + a set of patches (#4775)
This PR attempts to migrate from @timothy-king's repo for glpk-cut-log to using a set of patches against the official release that 'glpk-cut-log' was based off of (4.52).
This is in preparation of trying to rework these patches to be against the latest GPLK release (4.65). If we can do this, then it makes it easier for CVC4's dependancy on GPLK to be able to follow upstream (rather than being stuck on a release that is 6.5 years old!).
I have added GPLK as an option for CI, but I do not know if we actually want this. My concern with adding this to CI is that we're then not testing non-GPL builds, which doesn't seem ideal.
However, before starting to rework the patches to be against 4.65, I want to make sure that things are actually working/stable against 4.52; so having at least one CI target that does use GPLK would be great.
Signed-off-by: Andrew V. Jones andrew.jones@vector.com
|
|
|
|
This class is not used based on our coverage tests (although it appears to be possibly enabled based on non-standard runtime checking of assertions), and uses the equality engine in a highly nonstandard way that will be a burden to the new standardization of equality engine in theory solvers.
FYI @aniemetz @mpreiner
|
|
This commit integrates LibPoly into CVC4. It adds `contrib/get-poly`, adds it to the configure script, cmake and places where CVC4 inspects its own build configuration.
Furthermore, it adds `CVC4::RealAlgebraicNumber` (which wraps `poly::AlgebraicNumber`) including some basic unit tests and some utilities.
|
|
This PR creates a "current" sygus comp scripts, similar to what we have been doing for SMT COMP. It updates these scripts to fix the option names, as many have changed recently.
This also copies the SMT COMP current scripts to 2020, since they were used in the current state. @4tXJ7f let me know if this is not the case.
|
|
|
|
|
|
|
|
Adds scripts submitted to CASC competition.
Note that this version of CVC4 submitted to CASC was modified to allow models when --sort-inference is enabled, since model output is required.
|
|
|
|
|
|
|
|
|
|
Commit 00badd3a63a2fa568373d5c58553944b579d42bb changed our run script
to write output other than `sat`/`unsat` to a file if `$2` is passed to
it. However, it looks like StarExec does not pass that parameter to our
script despite the documentation claiming that it does [0]. This commit
makes our check more defensive by redirecting our unnecessary output to
`/dev/null` if `STAREXEC_WALLCLOCK_LIMIT` is set. I've done a quick test
run on StarExec and it looks like this does the trick.
[0]
https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-SpecialVariables
|
|
This commit changes the run-script for the incremental track to use
`--tear-down-incremental=1` for all logics that involve arithmetic. The
main motivation for this change is avoid issues that we have with the
lemmas generated for `mod`/`div` during `ppRewrite` that cause
model-soundness issues.
|
|
|
|
|
|
This commit adds additional options for the model validation track and
makes sure that non-"sat"/"unsat" outputs from the sequential porfolio
approaches are written to a file instead of stderr when running on
StarExec.
|
|
|
