| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
We now can handle all cases of (in|dis)equality over BITVECTOR_UREM. This also simplifies some
of the side conditions for equality.
|
|
|
|
Previously, we only handled the case x s < t. With this fix, we now get BITVECTOR_[SU]GT for litk
if we encounter a literal t < x s.
|
|
|
|
|
|
|
|
We now can handle all cases of (in|dis)equality over UREM. Previously, we could not handle equality
for index=0 and had to rewrite x % s = t to x - x / s * s. Since we can now handle this case, we do not
apply this rewriting anymore.
|
|
The default value for the seed for CVC4's RNG is 0. However, xorshift* requires a non-zero seed, else it generates only zero values. This fixes and prevents this behavior by resetting a given zero seed to ~0.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
BV. (#1447)
This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.
|
|
|
|
|
|
For reasons unknown, after the latest update of the Trusty environment on Travis,
we encountered write errors for the three Clang builds. As suggested here
https://github.com/travis-ci/travis-ci/issues/4704#issuecomment-321777557,
adding filter_secrets: false to the .travis.yml fixes the problem.
Note: switching back to the deprecated builds did not fix the problem.
|
|
PR #1441 forgot to enable the missing side condition handling for shifts. This PR enables it.
|
|
This adds side conditions for operators BITVECTOR_SHL, BITVECTOR_LSHR and
BITVECTOR_ASHR for index = 1, i.e., s << x = t and s >> x = t. Previously, we treated
these cases as non-invertible.
|
|
Print statistics if CVC4 gets a SIGTERM signal.
|
|
This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).
|
|
|
|
When compiling the Java bindings on macOS, the linker complained about
CVC4::ExprManager::mkConst<CVC4::TypeConstant>() and
CVC4::Expr::getConst<CVC4::TypeConstant>() being undefined. After some
research, I found that the issue has been introduced by commit
36bf9f8bcb2a1a3aea1f90eb4d13aed3bbf6da8f. It looks like adding the
-no-undefined flags resulted in the symbols in question being omitted
due to TypeConstant not being exported. This commit makes TypeConstant
CVC4_PUBLIC, which fixes the issue.
|
|
Adds support for linearizing additions w.r.t. to a variable.
For example,
a * x + b + c * d * -x = e + x
is rewritten to
x * (a - c * d - 1) = e - b.
This also adds an additional rewriting rule x * x = x --> x < 2.
|
|
This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL,
BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL.
It refactors side condition generation for better readability and unit testing.
It further adds unit tests for all side conditions we generate in order to check if they too weak
or to restrictive (which may result in unsound behavior).
This is achieved by checking the following two implications:
not (exists x. s * x = t => SC) ... if sat, SC is too restrictive
not (SC => exists x. s * x = t) ... if sat SC is too weak
This simplifies to checking not (SC <=> exists x. s * x = t).
|
|
|
|
|
|
|
|
|
|
Also, moved implementation of BVMinisatSatSolver::MinisatNotify::notify to .cpp file.
|
|
|
|
Now prints each tag in a separate line.
|
|
|
|
|
|
|
|
|
|
This is another step towards addressing #1304 and #1344. This pull request:
- Refactors SygusGrammarNorm
- Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used.
- Performs a "chain transformation" in the application of the PLUS operator in integer grammars
- Removes redundant expansions of definitions from TermDbSygus
- Adds a default empty print callback to SygusEmptyPrintCallback
This lays the basis for more general linearizations.
|
|
|
|
|
|
This commit fixes two issues with reset-assertions:
- pending pops were not done in SmtEngine, resulting in the following
assertion failure:
d_userLevels.size() == 0 && d_userContext->getLevel() == 1
- all definitions were erased on reset-assertion in an SMT2 file,
leading to errors about undefined types
|
