Age | Commit message (Collapse) | Author |
|
|
|
Commit d1eee40cc (PR #6346), in a foolish attempt to prevent speculated issues, introduced an overwriting policy to addition of resolution chains during SAT solving at the SAT proof manager. First, this is nonsensical because the lazy proof chain is context-dependent and at the same level other ways of proving that clause are simply redundant and therefore should be ignored. Second, and catastrophically, this policy, for reasons beyond me, can lead to open SAT proofs when the same clause is rederived at the same level.
So this commit simply reverts the change and adds an optimization that when the clause would be rederived at the same level we do nothing and leave the method.
|
|
|
|
The preprocess proof generator uses a dummy CDProof to mark input assertions that do not need justification. This CDProof should be user-context dependent to avoid rare cases where an input assertion was the symmetric equality of another, it was previously context independent.
This also refactors the debugging traces in this class.
|
|
This PR makes the CommandExecutor class use the options object from its SmtEngine instead of the driver one. This makes sure that options that are set via (set-option ...) are in effect for the CommandExecutor. It still stores the driver options, though, as they are used for resets.
The PR also does some minor cleanups along the way (remove unused pOptions, make things const).
Fixes #2376.
|
|
Not doing this rewrite for Booleans is probably an artifact of the old IFF kind being removed. This rewrite is important to simplify the generation of proofs for the SAT solver, as clarified in the new comment in the SAT proof manager.
|
|
Fixes #4791.
|
|
Have unsat cores regression tested also with default mode.
|
|
When compiling and running cvc5 on macOS with an M1 CPU, the regression
test regress0/cores/issue4971-0.smt2 returned unsat instead of the
expected unknown for the first (check-sat) command. This commit
makes the regression more robust by adding --cegqi-full and expecting
unsat.
|
|
This fixes an unsoundness issue in the sets + cardinality solver.
One rule of this solver applies in sets when two parents of a child of a cardinality graph are equal, in which case we know that child or one of its siblings must be equal to the opposite parent. For example, this rule tells us that:
if T = (union T S), then (intersect T S) = S.
The explanation of this rule could consider the representative term of one the parents instead of the term itself say (union T S) is representative T, giving the unsound inference: if (union T S) = (union T S), then (intersect T S) = S. This ensures we use the original terms.
This PR also does some minor cleanup.
|
|
|
|
Adds remaining regressions from issue #4791, which we can handle with the different new unsat-core modes. Note that issue4971-1.smt2 requires the sat-proof mode for unsat cores.
|
|
This name is the name of the symbol we parse. Internally, we still call
it POW2. This is a fix for the problem that `pow2` may clash (and
already does clash on SMT-LIB benchmarks) with user-defined symbols.
|
|
Fixes one of the issues in the nightlies.
|
|
Fixes #6834. There were two cases in our extended rewriter for string
equalities that were modifying the node without returning and without
updating information computed from the original node. This mismatch led
to incorrect rewrites. This commit fixes the issue by adding a flag to
returnRewrite() that determines whether node that was an equality
before and after the rewrite should be rewritten again with the extended
rewriter. We generally do not do that (we'd run in danger of rewriting
equality nodes with the extended rewriter even though we shouldn't) but
for the rewrites that were previously continuing to rewrite the node, we
set this flag and return. This ensures that we do not have an issue with
information being out of date. The commit additionally fixes an issue
where we would apply the rewrite STR_EQ_UNIFY even though the node
hadn't changed.
|
|
Regression cmu-dis-0707-3.smt2 has been timing out when using an ASan
build after commit a4f38d6. Before that
commit --strings-exp implicitly enabled --fmf-bound. After the
commit, the solver was supposed to apply the same reasoning but only to
interal quantifiers and without enabling --fmf-bound. However, the
commit missed some options checks that now also have to check whether
--strings-exp is enabled. This commit updates those option checks.
With this fix, we get a slightly different value for bug590.smt2 after
replying unknown. This commit updates the regression to be more lenient
with the value returned.
|
|
Output tags are similar to debug/trace tags, but are always enabled
(except for muzzled builds) to provide useful information for users.
Available output tags can be queried via -o help/--output help and are
specified in the base options module via enum values.
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
|
|
If reset-assertions was called it will now reset the SAT solver and the
CNF stream if clauses were permanently added to the SAT solver via
option --bv-assert-input.
|
|
Fixes #6777.
|
|
This passes recursive function definitions to the verification subsolver in sygus, with a default bounded limit of 3. This required improving the interface for setting up subsolvers by allowing custom options; the sygus solver statically computes an instance of the options that it uses in all calls.
This allows us to solve non-PBE sygus problems with recursive function definitions. The PR adds an example.
|
|
The decision level as previously implemented was not accurate since it
did not consider the user context level. This resulted in facts being
incorrectly recognized as input assertions, which happened for
incremental benchmarks.
|
|
This PR adds a more "real life" unit test for the pow2 solver. Thanks @4tXJ7f for the help with the options.
|
|
enabled (#6816)
There are compelling use cases that combine strings/sequences and quantifiers. Prior to this PR, strings enabled "bounded integer" quantifier instantiation so that internally generated quantifiers for strings reductions are handled in a complete manner. However, this enabled bounded integer quantifier instantiation globally. This degrades performance for "unsat" on quantified formulas in general.
After this PR, we do not enable bounded integer quantifier globally. Instead, we ensure that bounded integer quantification is applied to at least the internally generated quantified formulas; all other quantified formulas are handled as usual.
Notice this required ensuring that all quantified formulas generated by strings are marked properly. It also required adding --fmf-bound to a few regressions that explicitly require it.
|
|
This changes an annotation of a step of rewriting from "post" to "pre" in the theory preprocessor.
Fixes #6754.
|
|
the int-to-bv preprocessing pass produced wrong models.
This PR fixes this in a similar fashion to other preprocessing passes, by adding a substitution to the preprocessing pass context. This requires moving the main translation function to be a class method, rather than a helper method in an empty namespace.
Thanks to @alex-ozdemir for raising this issue and producing a triggering benchmark (added to regressions in this PR).
|
|
This PR introduces a rewrite from (^ 2 t) to (pow2 t) in order to make use of the specialized pow2 solver.
One regression that expects an error when t is not a constant is changed accordingly.
|
|
This commit adds the remaining changes for a working and integrated `pow2` solver.
In particular, it adds a rewrite and a lemma that identify `pow2(x)` with `0` whenever `x<0`.
Regressions are added as well, including `pow2-native-0.smt2` that shows the semantics of `pow2` on negative values.
The next steps are new rewrites and and more lemma schemas.
|
|
The linear arithmetic solver was not robust to cases where a duplicate lemma is emitted. This leads to non-linear arithmetic not being called to check at full effort, leading to potential model soundness issues.
Fixes #6773.
|
|
Fixes #6536
|
|
|
|
(#6790)
Fixes #6526
|
|
This ensures that we don't apply lambda rewriting, which involves array value normalization, to lambda terms returned by TheoryModel::getValue.
This can significantly speed up our time to return function terms for getValue.
|
|
Fixes #6699.
|
|
Fixes #6690.
|
|
For model construction we only compute model values for relevant terms. The set of relevant terms is computed in https://github.com/cvc5/cvc5/blob/master/src/theory/model_manager_distributed.cpp#L58, which skips equalities by default because equalities are usually handled by the equality engine.
When --bitblast=eager is enabled all assertions are wrapped into BITVECTOR_EAGER_ATOM nodes and passed to the BV solver, which results in equalities below BITVECTOR_EAGER_ATOM nodes not being handled by the equality engine but by the BV solver directly. These equalities, however, are skipped when computing the relevant terms and therefore the BV solver is not asked to compute model values for variables below these equalities.
If --bitblast=eager is enabled the BV solver now additionally adds the variables encountered during bit-blasting to the relevant terms via computeRelevantTerms.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
|
|
Since the new BV solver is enabled by default and uses CaDiCaL
(and optionally CryptoMiniSat) we make CaDiCaL a required dependency.
|
|
Commit f10087c3b347da6ef625a2ad92846551ad324d73 added new files that do
not compile without libpoly. This commit excludes those files when
building without libpoly. It also updates one of the regressions to
ignore a warning about approximate values in the model.
|
|
|
|
This commit adds a new parser option, --hol, which marks that HOL is being used. This option has the effect of prepending the problem's logic with "HO_", which teels the solver that the logic is higher order. The parser builder, base parser, and SMT2 and TPTP parsers are all updated to work with this new setting, as is the logic info class.
For now this parser option is enabling the --uf-ho option for internal use, since for now higher-order solving relies it. In a future PR this dependency will be removed (since this information is already given to the SMT solver via the logic).
|
|
solve-int-as-bv is now the preferred method for solving these benchmarks.
Adds solve-int-as-bv to a regression that became slow in my previous commit.
|
|
This PR ensures we do not eagerly rewrite bv2nat and int2bv when using solve-bv-as-int. Instead they are rewritten during expandDefinitions (at the end of preprocessing).
It also updates regressions that relied on lazy extended function reductions in the lazy solver to use solve-bv-as-int, and adds a missing case (INT_TO_BITVECTOR) in the solve-int-as-bv preprocessing pass.
A followup PR will remove support for lazy extended function reductions for bv2nat / int2bv altogether.
|
|
After commit 327a24508ed1d02a3fa233e680ffd0b30aa685a9, the int-to-bv
preprocessing pass is getting rewritten terms. As a result, the terms
can contain negative constants (instead of `(- c)`, i.e., `UMINUS` of a
positive constant) and `NONLINEAR_MULT`. The commit adds support for
those cases, does some minor cleanup, and adds regressions. The
regressions should allow us to detect if/when the preprocessing pass
breaks in the future.
|
|
Fixes #6717. Commit 11c1fba added some
new rewrites for ITE. Due to the new rewrites taking precedence over
existing rewrites, it could happen that some of the previous rewrites
did not apply anymore even though they would have further simplified the
ITE. In the example from the issue, (ite c c true) was rewritten to
(or (not T) T) instead of (ite T true true) and then true. The
commit fixes the issue by moving rewrites resulting in
conjunctions/disjunctions to the end.
|
|
This PR makes a new regression explicitly require statistics.
|
|
This updates 2-dim dependent bounded quantifiers to not map constants to terms when computing ranges, when the type of the variable is closed enumerable. This is require to fix an incorrect model (possible solution unsoundness) issue in the reduction of str.indexof_re.
Fixes the 1st, 4th and 5th benchmarks from #6653. Fixes #6635.
|
|
This PR fixes a typo in the option handler for the statistics options, which lead to options not properly propagating.
|
|
Fixes the 2nd benchmark from #6653.
|
|
This PR fixes a missing connection in trust substitution proofs, which was the cause of open proofs when solved equalities from ppAssert were not justified by proofs.
Also distinguishes TRUST_SUBS_EQ from TRUST_SUBS_MAP for clarity.
|
|
Fixes #6681. When checking whether SPLIT_EQ_STRIP_L applies, we were
using sripSymbolicLength, which changes its inputs depending on how
many elements of the concatenation it could strip. However, one of the
arguments, pfxv0, was reused across multiple checks if the strip did
not result in a rewrite. Later invocations were wrong as a result. This
commit changes the call to stripSymbolicLength() to use a new copy of
the vector instead.
|
|
This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.
Fixes #3958, #5396, #5736, #5743, #5947.
|