| Age | Commit message (Collapse) | Author |
|---|
|
(#2647)
Simplifications based on the special const is now delegated down, only
the concat is pulled up.
|
|
const. (#2647)
|
|
const. (#2643)
Match: `x_m | concat(y_my, 0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n], x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, 1_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, x[m-my-1:m-my-n+1], 1_1, x[m-my-n-1:0] | z)`
Match: `x_m | concat(y_my, ~0_n, z_mz)`
Rewrites to: `concat(x[m-1:m-my] | y, ~0_n, x[m-my-n-1:0] | z)`
On QF_BV with eager and CaDiCaL (time limit 600s, penalty 600s):
```
| CVC4-base | CVC4-concatpullup-or |
BENCHMARK | SLVD SAT UNSAT TO MO CPU[s] | SLVD SAT UNSAT TO MO CPU[s] |
totals | 38992 13844 25148 1082 28 984887.4 | 39028 13845 25183 1046 28 974819.1 |
```
|
|
ones (#2596).
|
|
1 (#2596).
|
|
0 (#2596).
|
|
|
|
|
|
|
|
This adds support for model cores, fixes #1233.
It includes some minor cleanup and additions to utility functions.
|
|
This should also fix CIDs 1465687, 1465695, 1465696, and 1465701.
|
|
|
|
|
|
Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h
|
|
|
|
|
|
|
|
|
|
|
|
condition/child. (#2259)
|
|
This includes:
- A missing case in the smt2 printer,
- A bug in an inference of int2bv applied to bv2nat where the types are different.
|
|
|
|
Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat.
|
|
|
|
|
|
This commit fixes warnings for an unused variable, comparison of two
different types and add virtual destructors to classes that were
previously missing them. It also enables the -Wnon-virtual-dtor warning
which warns about any class definition with virtual methods that does
not have a virtual destructor (except if the destructor is protected).
This flag is supported by both clang and GCC and not enabled by default.
|
|
|
|
Further, fix a bug in the AIG bitblaster that was also uncovered with the
minimized file.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
enabled (#1801)
Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable).
This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user.
|
|
There was a use-after-free in the eager bitblaster: the context used by
the SAT solver was destroyed before the solver. This lead to a
use-after-free in the destructor of the SAT solver when destroying
context-dependent objects. This commit fixes the issue by changing the
desctruction order such that the context is destroyed after the SAT
solver.
Note: This issue was introduced in commit
a917cc2ab4956b542b1f565abf0e62b197692f8d because d_nullContext and
d_satSolver were changed to be std::unique_ptrs.
|
|
|
|
This also adds an additional check in processAssertions to ensure that all
assertions are guaranteed to be rewritten (there was only a comment stating
this).
|
|
This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.
|
|
|
|
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
Adds missing override keywords.
|
|
This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.
|
|
|
|
Tested against the recursive implementation with a temporary assertion on regression tests
with --bv-eq-slicer=auto.
|
|
This unrecursifies and merges bv::utils::isCoreTerm and bv::utils::isEqualityTerm to avoid
code duplication.
In the best case, the recursive implementation visits less nodes. This can be achieved with
the non-recursive implementation, however, at the cost of increased code complexity.
In practice, on QF_BV the new implementation slightly improves performance.
Tested against the recursive implementation with a temporary assertion on regression
tests (bv::utils::isCoreTerm was tested with --bv-eq-slicer=auto).
Further tested on QF_BV with a TO of 300s (slight performance improvement).
|
|
|
|
|
|
|
