Age | Commit message (Collapse) | Author |
|
|
|
|
|
|
|
|
|
|
|
|
|
PR #3062 changed `Smt2::setLogic()` to return a heap-allocated command,
which didn't get cleaned up by our `parser_black` unit test. This commit
fixes the memory leak.
|
|
This commit adds support for the theory of floating-point numbers in the
Java API. Previously, floating-point related classes were missing in the
JAR. The commit also provides an example that showcases how to work with
the theory of floating-point numbers through the API.
|
|
The `--force-logic` command line argument can be used to override a
logic specified in an input file or to set a logic when none is given.
Before this commit, both the `SmtEngine` and the parser were aware of
that argument. However, there were two issues if an input file didn't
specify a logic but `--force-logic` was used:
- Upon parsing `--force-logic`, the `SmtEngine` was informed about it
and set the logic to the forced logic. Then, the parser detected that
there was no `set-logic` command, so it set the logic to `ALL` and
emitted a corresponding warning. Finally, `SmtEngine::setDefaults()`
detected that `forceLogic` was set by the user and changed the logic
back to the forced logic. The warning was confusing and setting the
logic multiple times was not elegant.
- For eager bit-blasting, the logic was checked before resetting the
logic to the forced logic, so it would emit an error that eager
bit-blasting couldn't be used with the logic (which was `ALL` at that
point of the execution). This was a problem in the competition because
our runscript parses the `set-logic` command to decide on the
appropriate arguments to use and passes the logic to CVC4 via
`--force-logic`.
This commit moves the handling of `--force-logic` entirely into the
parser. The rationale for that is that this is not an API-level issue
(if you use the API you simply set the logic you want, forcing a
different logic in addition doesn't make sense) and simplifies the
handling of the option (no listeners need to be installed and the logic
is set only once). This commit also removes the option to set the logic
via `(set-option :cvc4-logic ...)` because it complicates matters (e.g.
which method of setting the logic takes precedence?). For the CVC and
the TPTP languages the commit creates a command to set the logic in
`SmtEngine` when the logic is forced in the parser instead of relying on
`SmtEngine` to figure it out itself.
|
|
Previously, we were just writing temporary files to `/tmp/` but this
commit allows the user to use the `TMPDIR` environment variable to
determine which directory the temporary file should be written to. The
commit adds a helper function for this and also includes some minor
cleanup of existing code.
|
|
This PR makes the skolem normalization in the string solver quite a bit
more aggressive by reducing more skolems to prefix and suffix skolems.
Experiments show that this PR significantly improves performance on CMU
benchmarks.
|
|
Travis has started to switch to Ubuntu 16.04 [0]. We were explicitly
specifying 14.04 as the `dist` in our `.travis.yml`. This commit changes
that specification to 16.04, updates the Java version, and removes
a workaround for an old Travis issue.
[0] https://changelog.travis-ci.com/xenial-as-the-default-build-environment-99476
|
|
This commit adds a lemma that the value of `str.indexof(x, y, n)` must
be between -1 and `str.len(x)`.
|
|
|
|
|
|
|
|
`let_shadowing.smt2` uses dumping to test our printing infrastructure.
Since some builds do not support dumping, this commit disables that
regression for non-dumping builds. Additionally, it enables an error
message when trying to dump with a muzzled build and corrects the output
of `--show-config` to indicate that muzzled builds cannot dump.
Previously, the dumping output of a muzzled build was just silently
empty.
Most of the changes in `dump.cpp` are due to reformatting.
|
|
Fixes #3044. When using CLN instead of GMP, SWIG produces different Java
files for the CLN classes. The bindings expected the GMP files even when
building with CLN, so compilation failed. This commit fixes the issue by
changing the list of files depending on whether we build with CLN or
GMP.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #3005. When printing nodes, we introduce `let` expressions on the
fly. However, when doing that, we have to be careful that we don't
shadow existing variables with the same name. When quantifiers are
involved, we do not descend into the quantifiers to avoid letifying
terms with bound variables that then go out of scope (see #1863). Thus,
to avoid shadowing variables appearing in quantifiers, we have to
collect all the variables appearing in that term to make sure that the
let does not shadow them. In #3005, the issue was caused by a `let` that
was introduced outside of a quantifier and then was shadowed in the body
of the quantifier by another `let` introduced for that body.
|
|
This commit enables DRAT-optimization, which consists of two sub-processes:
1. removing unnecessary instructions from DRAT-proofs and
2. not proving clauses which are not needed by DRAT proofs.
These changes have the effect of dramatically shortening some some bit-vector proofs. Specifically, proofs using lemmas in the ER, DRAT, and LRAT formats, since proofs in any of these formats are derived from a (now optimized!) DRAT proof produced by CryptoMiniSat. What follows is a description of the main parts of this PR:
## DRAT Optimization
The DRAT-optimization is done by `drat-trim`, which is bundled with `drat2er`. The (new) function `ClausalBitVectorProof::optimizeDratProof` is our interface to the optimization machinery, and most of the new logic in this PR is in that function.
## CNF Representation
The ability to not prove unused clauses requires a slight architectural change as well. In particular, we need to be able to describe **which** subset of the original clause set actually needs to be proved. To facilitate this, when the clause set for CryptoMiniSat is first formed it is represented as a (a) map from clause indices to clauses and (b) a list of indices. Then, when the CNF is optimized, we temporarily store a new list of the clauses in the optimized formula. This change in representation requires a number of small tweaks throughout the code.
## Small Fixes to Signatures
When we decided to check and accept two different kinds of DRAT, some of our DRAT-checking broke. In particular, when supporting one kind of DRAT, it is okay to `fail` (crash) when a proof fails to check. If you're supporting two kinds of DRAT, crashing in response to the first checker rejecting the proof denies the second checker an opportunity to check the proof. This PR tweaks the signatures slightly (and soundly!) to do something else instead of `fail`ing.
|
|
SWIG 4 seems to change the name for `std::map<CVC4::Expr, CVC4::Expr>`
to include the implicit template argument for comparisons. To make the
code compatible with both SWIG 4.0.0 and older versions, this commit
creates an explicit instance of the template.
|
|
Due to issues in the current proof code, this commit also disables proof
checking for five QF_LRA benchmarks (see issue #2855).
|
|
This commit adds a check to make sure that the result of a `(check-sat)`
call matches the expected result set via `(set-info :status ...)`. In
doing so, it also fixes an issue where CVC4 would crash if asked for the
unsat core after setting the status to `unsat` but before calling
`(check-sat)` (see regression for concrete example). This happened
because CVC4 was storing the expected result and the computed result
both in the same variable (the expected result wasn't really being used
though). This commit keeps track of the expected result and the computed
result in separate variables to fix that issue.
|
|
`--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.
|
|
This commit adds a check that makes sure that we do not try to create
nodes with more children than the maxmimum number. This can currently
happen when flattening nodes in QF_BV with lots of duplicate children.
|
|
|
|
The commit fixes an issue where FMF could theoretically chose interpreted function applications as "model basis terms". This triggered an incorrect model (caught by an AlwaysAssert) when the interpreted function later did not appear in a model and was chosen by FMF to be equal to a wrong value.
|
|
|
|
When printing an empty symbol name, which can appear in an SMT2 file as
`||`, we were printing the empty string instead of quoting the symbol.
This commit fixes the issue and adds a regression test.
|
|
Fixes #3020. Boolean terms that appear in other terms, e.g. a Boolean
array index, are replaced by `BOOLEAN_TERM_VARIABLE`s to make sure that
they are handled properly in theory combination. When doing this
replacement, an equality of the form `(= <Boolean term> <Boolean term
variable)` is added to the assertions. The problem was that
`Theory::ppAssert()` would derive a substitution when this equality was
registered. The commit fixes the problem by not allowing to add
substitutions for `BOOLEAN_TERM_VARIABLE`s.
|
|
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).
|
|
The rewrite `BvIteConstChildren` assumes that `BvIteEqualChildren` has
been applied before it runs. However, with nested ITEs, it was possible
to violate that assertion. Given `bvite(c1, bvite(c2, 0, 0), bvite(c3,
0, 0))`, `BvIteEqualChildren` would rewrite that term to `bvite(c2, 0,
0)`. The `LinearRewriteStrategy` then ran `BvIteConstChildren` on
`bvite(c2, 0, 0)` which complained about the equal children. This commit
implements a simple fix that splits the `LinearRewriteStrategy` into two
strategies to make sure that if `BvIteEqualChildren` rewrites a node, we
drop back to the `Rewriter`. This ensures that the rewrites on the
rewritten node are invoked in the correct order.
|
|
Although CVC4's behaviour is actually correct, this is to make
things a bit clearer and prevent confusion in the future.
|
|
Fixes #2989. SWIG 3 seems to have an issue properly resolving
`T::const_iterator::value_type` if that type itself is a `typedef`.
This is for example the case in the `UnsatCore` class, which `typedef`s
`const_iterator` to `std::vector<Expr>::const_iterator`. As a
workaround, this commit changes the `JavaIteratorAdapter` class to take
two template parameters, one of which is the `value_type`. The commit
also adds a compile-time assertion that `T::const_iterator::value_type`
can be converted to `value_type` to avoid nasty surprises. A nice
side-effect of this solution is that explicit `typemap`s are not
necessary anymore, so they are removed. Additionally, the commit adds a
`toString()` method for the Java API of `UnsatCore` and adds examples
that show and test the iteration over the unsat core and the statistics.
Iterating over `Statistics` now returns instances of `Statistic` instead
of `Object[]`, which is a bit cleaner and requires less glue code.
|
|
Default install paths are:
- libcvc4jni.so in /usr/lib/
- CVC4.jar in /usr/share/java/cvc4
Fixes #2990.
|