| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
|
|
|
|
|
|
On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
