| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Currently, we can optionally specify an *.expect file with the metadata
of a regression test. This commit removes that option because it was not
widely used, adds maintenance overhead and makes the transition to a new
build system more cumbersome. Regression files can still be fed to a
solver without removing the metadata first since they are in comments of
the corresponding input format (note that this was not always the case,
it changed in efc6163629c6c5de446eccfe81777c93829995d5).
|
|
|
|
This is in preparation for migration to cmake since ctest determines failure via exit code.
|
|
|
|
|
|
This corrects a bug that was introduced in #2266 (the hack removed there was necessary).
This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus.
This also enables total semantics for BV div-by-zero for sygus.
|
|
|
|
|
|
|
|
Fixes #2298. The `get-unsat-assumptions` command was printing the result
with square brackets and commas instead of parentheses and spaces
between the assumptions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This includes several improvements for cegqi with arithmetic:
- Randomly choose either lower or upper bounds instead of always using lower bounds (this is similar to cegqi+BV),
- Equalities are handled by processAssertions,
- Resort to *only* model values at full effort instead of trying to mix model values/bounds (this is also similar to cegqi+BV),
- cegqi+arithmetic does not try multiple instantiations unless the flag cbqiMultiInst is set. This makes it so that ceg_instantiator does not have exponential behavior when the strategy is non-monotonic.
It also includes a core fix to computing what bound is optimal based on an ordering that incorporates virtual terms. Previously, we would consider, e.g.:
`a+b*delta > c+d*delta if a>=c and b>=d`
Whereas the correct check is lexicographic:
`a+b*delta > c+d*delta if a>c or a=c and b>d`
This means e.g. 2+(-1)*delta > 3 was previously wrongly inferred.
This is part of merging https://github.com/ajreynol/CVC4/tree/cegqiSingleInst, which is +3-0 on SMTLIB BV and +12-9 on SMTLIB LIA+LRA+NRA+NIA.
|
|
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.
|
|
|
|
The rewriter for lambda is currently too aggressive, there are cases like:
lambda xy. x = y
that are converted into an array representation that when indexing based on x gives (store y true false), which is subsequently converted to:
lambda fv_1 fv_2. fv_1 = y
where fv_1 and fv_2 are canonical free variables. Here, y is used as index but was not substituted hence is incorrectly made free.
To make things simpler, this PR disables any rewriting for lambda unless the array representation of the lambda is a constant, which hardcodes/simplifies a previous argument (reqConst=true). This fixes a sygus issue I ran into yesterday (regression added in this PR).
Some parts of the code were formatted as a result.
|
|
|
|
|
|
|
|
(#2184)
|
|
|
|
Fixes issue #2137. CnfProof has a stack of assertions that are being
converted to clauses. Previously, it could happen that while an
assertion was being added, TheoryProxy::explainPropagation() would be
called from Solver::reason() and push an assertion to the stack that was
then not removed. This lead to a clause id of the assertion being
associated with the explanation instead, which in turn could lead to a
wrong unsat core. This commit identifies two cases where
TheoryProxy::explainPropagation() is called without cleaning up the
assertion stack afterwards. It also adds an assertion that the assertion
stack must be empty when we are getting the unsat core.
|
|
|
|
The issue is not triggered anymore after PR #2059 but the test case is
good to have for changes in MiniSat code.
|
|
|
|
In MiniSat's analyze(), we were taking a reference of a clause that
could be invalidated by a call to resolveOutUnit(). resolveOutUnit() can
lead to allocation of clauses which in turn can lead to clauses being
reallocated, making the reference stale. The commit encloses the
reference in a code block that makes the lifetime of the reference more
obvious and removes uses of the potentially stale reference.
|
|
When moving the LFSC checker out of the CVC4 repository in commit
dfa69ff98a14fcc0f2387e59a0c9994ef440e7d0, we disabled checking unsat
cores when CVC4 was compiled without LFSC due to the complexity of the
regression script. This commit changes the new(-ish) Python regression
script to check unsat cores even when CVC4 was compiled without LFSC.
This is done by having two separate flags, --with-lfsc and
--enable-proof, for the regression script that mirror the configuration
flags. The regression script performs unsat cores and proofs checks
based on those flags.
Additionally, this commit changes the regression script to check proofs
and unsat cores in two independent runs. Testing them in a single run
masked issues #1953 and #1954.
|
|
|
|
|
|
|
|
|
|
Commit 106e764a04e4099cc36d13de9cec47cbf717b6cc missed one test case.
This commit disables that test case for the competition build.
|
|
This commit adds the option of skipping regressions when a specified
feature is enabled. It also changes some of the regression tests to be
skipped when it is a competition build because regressions fail
otherwise. In the tests changed in this commit, we do not care about
reproducing error messages in a competition build, so we can skip them.
|
