| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
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.
|
|
|
|
When bit-blasting eagerly, we were not assigning values to the Boolean
variables in the `TheoryModel`. With eager bit-blasting, the BV SAT
solver gets all (converted) terms, including the Boolean ones, so
`EagerBitblaster::collectModelInfo()` is responsible for assigning
values to Boolean variables. However, it has only been assigning values
to bit-vector variables, which lead to wrong models. This commit fixes
the issue by asking the `CnfStream` for the Boolean variables, querying
the SAT solver for their value, and assigning them in the `TheoryModel`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This cleans up naming of API functions to create first-order constants and variables.
mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.
Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
* [BV] An option for SAT proof optimization
The option doesn't **do** anything yet, but exists.
* CopyPaste Fix: BvOptimizeSatProof documentation
It was the documentation for a different option. Now it has been
updated.
* Fix Typos per Mathias' review.
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Fixes #2958.
The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with.
The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering.
|
|
|
|
The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor}
[0, 1] as left-associative. CVC4 treats all but bvxnor as having
variable arity anyway but the arity check was too strict when using
`--strict-parsing`. This commit changes the strict parsing check. For
bvxnor, it adds code to the parser that expands an application of bvxnor
into multiple applications of a binary bvxnor if needed.
References:
[0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand,
bvor, bvadd, bvmul)
[1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor)
|
|
|
|
|
|
This is a minor fix for systems with glibc version < 2.17. In that case, we need to link with `-lrt` according to the clock_gettime man page.
|
|
For now, they are just copies of the 2018 version of the scripts.
|
|
|
|
|
|
|
|
|
|
|
