| Age | Commit message (Collapse) | Author |
|---|
|
This PR adds two new command line options that govern how the CAD module does projection and lifting, allowing to use the new Lazard evaluation. By default, we use McCallum with regular lifting which does not require CoCoA.
Additionally, this PR adds a bunch of unit tests for the CAD module.
|
|
This adds the learned rewrite preprocessing pass, which rewrites the input formula based on (typically theory specific) reasoning about learned literals. The main motivation is for preprocessing ints division/modulus based on bounds.
|
|
|
|
Adds the basic skeleton of the pass.
|
|
(#6809)
Implement the operator << with std::ostream for OptimizationObjective and OptimizationResult. Currently only supports SMTLib2 or Sygus as output languages.
Objective: (maximize [node] :signed) or (minimize [node]) or ...
Result: (sat [expr]) or (unsat) or (unknown([explanation]) [expr/null])
|
|
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.
|
|
This makes TheoryEngine notify all theories when a theory sends a conflict. This means that buffered inference managers always clear their buffers when any theory sends a conflict.
This is required for making theories robust to conflicts that may arise when using the central equality engine, where a different theory may raise a conflict during another theory's check.
|
|
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 feature is useful for example for succinctly inserting children of
a node in the reverse order. To make this work, the commit fixes the
declaration of `reference` in the `NodeValue::iterator`. The
`std::reverse_iterator` adapter expects the `reference` type to match
the return type of `operator*` in the corresponding iterator (as
mandated by the standard). Despite its name, `reference` does not have
to be a C++ reference. Note that we cannot actually make it a C++
reference because `NodeValue::iterator` wraps the `NodeValue*` in a
`Node`/`TNode` in `operator*`.
|
|
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.
|
|
This adds an option to limit the number of instantiation rounds used by quantifiers engine.
This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions.
This PR also makes minor improvements to the quantifier utility infrastructure.
|
|
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 is an alternative fix to https://github.com/cvc5/cvc5/pull/6808.
This ensures that we do not notify the provided class of an equality engine during initialization.
|
|
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 adds variants for the CAD projection operator to use Lazard's projection operator.
|
|
Fixes #6788
|
|
This rewrites the word blasting function FpConverter::convert to be
easier to follow and read. It further cleans up several things.
This additionally prepares for allowing to convert incoming facts rather
than terms registered with theory FP. That is, when word blasting more
lazily, in preNotifyFact rather than in registerTerm.
|
|
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 replaces (old) internal string kind names to match the API / smt2 standard names.
|
|
There's one spot left in issue #6453, that is the call to `std::allocator<T>::destroy` in `mkMetaKind`. And this commit fixes it.
|
|
In preparation for further changes in the printer.
|
|
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.
|
|
We add the lemma x<=y --> pow2(x)<=pow2(y) to the pow2 solver.
Additionally, some renaming of variables is introduced for better clarity.
|
|
|
|
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.
|
|
This PR adds the actual implementation for the Lazard evaluation based on CoCoALib. It is only used if CoCoALib is available and falls back to a default libpoly-based implementation otherwise.
|
|
Fixes #6536
|
|
This PR adds implementations of functions from the pow2 solver, rewriter and type checker.
|
|
|
|
(#6790)
Fixes #6526
|
|
|
|
Recent experiments have shown that `--tear-down-incremental` is actually
not really helping anymore and it has always been a bit of a workaround.
It is also broken on current master. This commit removes the option.
|
|
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.
|
|
Unit tests are translated from https://github.com/cvc5/cvc5/blob/master/test/unit/api/op_black.cpp
to python.
The only thing that is not faithfully translated is that the `cpp` tests expect the template function `[getIndices](https://github.com/cvc5/cvc5/blob/master/src/api/cpp/cvc5.h#L841)` to fail when an inappropriate type is given to it, while in the [`python` API](https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/src/api/python/cvc5.pxi#L343) this function is not a template, but just tries every supported type.
For example, the following line is not translated:
https://github.com/cvc5/cvc5/blob/90d19f7cdbaf41e389bdcbd099471f658a35ce98/test/unit/api/op_black.cpp#L206
|
|
This PR adds the file int_blaster.cpp. Most of the functions are not yet implemented. Two main functions are implemented.
Additionally, code that will no longer be needed is removed from the BV rewriter.
|
|
This removes the d_performNotify flag from equality engine which was supposedly used to guard a very old dependency concerning notifications during initialization. We are now robust to this and hence the flag can be removed.
|
|
Fixes #6699.
|
|
Fixes #6690.
|
|
This PR translates the cpp API unit tests about results to python.
The original cpp file is: https://github.com/cvc5/cvc5/blob/master/test/unit/api/result_black.cpp
The translation made rise to one addition to the python API:
The UnknownExplanation object from the cpp API was represented by a string in the python API.
Now we have a more faithful representation, as an enum.
|
|
Fixes #6776.
Our computation of when a regular expression was constant did not account for when ITE was embedded in an RE, leading to an unsound rewrite.
That benchmark now gives:
(error "Regular expression variables are not supported.")
|
|
This adds fields to equality engine setup information which will be used to hook up theories to the central equality engine.
This PR does not impact any behavior.
This is in preparation for the central equality engine.
|
|
After commit d70a63324c95210f1d78c2efc46395d2369d2e2b, context-dependent
attributes have not been supported and, as a result, the template
parameter `context_dependent` of `Attribute` has not been used.
Context-dependent attributes also do not fit with our current design of
sharing attributes across different solvers, so it is unlikely that we
will add that feature back in the future. This commit removes the unused
template parameter.
|
|
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>
|
|
This commit adds Grammar.java GrammarTest.java and cvc5_Grammar.cpp to the java api.
|
|
The statistic in `smt_solver.cpp` was not accurate.
|
