Age | Commit message (Collapse) | Author |
|
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.
|
|
|
|
--no-checking. (#4417)
|
|
Changes run script to be consistent for 20 minute timeout. This divides most of the previous time allocation by 2, with a few exceptions (for non-linear).
It adds a configuration involving --no-arith-brab to QF_NIA and reallocates some time.
|
|
|
|
This PR merges --lang=smt2.6.1 and --lang=smt2.6 (default). It makes it so that 2.6 always expects the syntax of the string standard http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.
I've updated the regressions so that the 2.6 benchmarks are now compliant with the standard. Some of the <=2.5 benchmarks I've updated to 2.6. Others I have left for now, in particular the ones that rely on special characters or ad-hoc escape sequences. The old formats will be supported in the release but removed shortly afterwards.
This PR is a prerequisite for the release, but not necessarily SMT-COMP (which will use --lang=smt2.6.1 if needed). Notice that we still do not have parsing support for str.replace_re or str.replace_re_all. This is required to be fully compliant.
|
|
This also updates the SMT COMP script to revert to our previous behavior.
This is required for SMT COMP. It should be beneficial for satisfiable QF_NIA instances. I will revisit/test this independently.
|
|
This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.
Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.
The changes were done by these commands in the given directories:
src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done
And a few minor fixes afterwards.
This should be merged close to the time of the next stable release.
|
|
This will fix the CI caching issues we sometimes encountered on GH actions.
|
|
|
|
This includes:
All options pertaining to SMTEngine are now handled at the top of setDefaults.
smtlibStrict was deleted in favor of a script.
statsEveryQuery enables stats by modifying a public option function. This is a slight hack but this code will likely get refactored as well soon.
A few other changes:
Fix a bug in SMTEngine: defineFunction should finalize options.
Call setDefaults before initilizing the TheoryEngine and ProofManager. This is necessary so that the PROOF(...) macro works earlier during initialization.
The next step will be to remove the links infrastructure for the options infrastructure. This will enable further detangling of our options dependencies.
|
|
|
|
This PR delays error on unsupported symbols as much as possible, by only throwing the error when actually constructing the node.
|
|
Moves SMT-COMP-specific options to the SMT-COMP script. Both of these options have led to issues (segfaults or infinite loops).
Issue #789 can be downgraded to "minor" after this PR.
Btw, I did not add these specialized options to the "incremental" script of SMT-COMP, since I'm assuming they should not be used there.
|
|
|
|
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
|
|
|
|
Fixes #3058. Commit a7c4cd3ecacb1e484a076edde0274c282bb43ffb changed
CVC4's behavior to emit an error when `--unconstrained-simp` is used
with `--incremental`. Before, we were silently disabling it. For some
reason, we had that option enabled for the incremental QF_LIA track of
SMT-COMP, so CVC4 failed on those benchmarks. This commit changes the
corresponding competition script to not use the option.
|
|
|
|
|
|
We use the command which to determine if a command is available on the system. However, which is not installed on all platforms by default (e.g. CentOS). command is a shell builtin that can be used for the same purpose.
|
|
|
|
|
|
* Removes incremental API check (#3011)
* Fixes toSatValueLit to use the new semantics of CaDiCaL's val()
Fixes #3011
|
|
|
|
* Use a custom implementation instead of relying on realpath, because it doesn't exist on Mac
* Use local variables and move portable_realpath to its own file
* Replace portable_realpath with python realpath
* Consistent command substitution
Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
* Substitute pwd directly
|
|
|
|
`--unconstrained-simp` is not compatible with unsat cores.
|
|
This year's timeout is 40min up from 20min last year. This commit scales
the timeouts accordingly.
|
|
We cannot Ackermannize all the QF_UFBV benchmarks due to uninterpreted
sorts. This commit adds lazy bit-blasting as a backup strategy.
|
|
This commit enables SymFPU assertions in production. The reason for this
is that there are some known problems with certain bit-widths, so we
prefer to be conservative. The commit also updates the run scripts for SMT-COMP 2019 to use `--fp-exp` since we have those additional checks in place now.
|
|
`--unconstrained-simp` is not compatible with unsat cores, so this
commit removes it for QF_LRA. `--bitblast=eager` is not compatible with
unsat cores for QF_UFBV because the dependencies are not tracked
correctly in the Ackermannization preprocessing pass, so the commit
changes the script to use the lazy BV solver instead. Strings need some
additional options to use the correct theory symbols.
|
|
|
|
Fixes #2932. fp.roundToIntegral was rounding some very small subnormals up to
between 1 and 2, which is A. wrong and B. not idempotent. The
corresponding symfpu update fixes this as it was an overflow caused
by the unpacked significand not being able to represent an extra
significand bits.
|
|
The "Application Track" has been renamed to "Incremental Track" this
year, so this commit renames the script accordingly and updates the name
of the CVC4 binary that the script calls to be just `cvc4`. The commit
also adds an initial script for the model validation track.
|
|
|
|
|
|
This commit adds support for eager bit-blasting with CaDiCaL on
incremental benchmarks. Since not all CaDiCaL versions support
incremental solving, the commit adds a CMake check that checks whether
`CaDiCaL::Solver::assume()` exists.
Note: The check uses `check_cxx_source_compiles`, which is not very
elegant but I could not find a better solution (e.g.
`check_cxx_symbol_exists()` does not seem to support methods in classes
and `check_struct_has_member()` only seems to support data members).
|
|
For now, they are just copies of the 2018 version of the scripts.
|
|
|
|
|
|
|
|
Exclude lines that #include header files and define namespaces.
Since we use git blame -C -M to determine the current top contributors,
git tries to match all #include and namespace definitions to an original
author, which is not accurate since these lines are usually not
copied over from other files.
|
|
|
|
|
|
drat2er is a C/C++ project which includes support for
* Checking DRAT proofs
* Converting DRAT proofs to LRAT proofs
* Converting DRAT proofs to ER proofs
It does the first 2 by using drat-trim under the hood.
I've modified our CMake configuration to allow drat2er to be linked into
CVC4, and I added a contrib script.
|
|
This commit changes the two www,antlr3.org URL's in contrib/get-antlr-3.4 to use https instead of http, which is more secure.
|
|
This commit changes the contrib/get-cryptominisat script to only build
the CryptoMiniSat library instead of both the library and the binary.
The advantage of this is that we can compile a static version of the
CryptoMiniSat library without having a static version of glibc or
libstdc++ (this is fine as long as we do a shared library build of
CVC4). This is an issue on Fedora (tested on version 25) where the
contrib/get-cryptominisat script was failing when building the
CryptoMiniSat binary due to the static version of these libraries not
being available. Since we just want to build the library, the commit
also changes the script to not install CryptoMiniSat anymore and updates
the CMake find script to accomodate the new folder structure. Side note:
the folder structure generated after this commit is a bit more uniform
with, e.g. the CaDiCaL script: The source files are directly in the
cryptominisat5 folder, not in a subfolder.
|
|
|
|
|