| Age | Commit message (Collapse) | Author |
|---|
|
This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.
For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.
The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.
|
|
This splits the eager solver from solver state. The solver state contains the EqcInfo data, while the eager solver is responsible for populating it.
This is in preparation for adding new techniques to the eager solver.
No behavior changes in this PR, only reorganization.
|
|
The pull request addressed issue #5593 for adding an unit test.
|
|
Was causing arithmetic to process a Boolean equality when --arith-rewrite-equalities is true.
Fixes #5761.
|
|
|
|
Use ASSERT instead of EXPECT for consistency. There's no real benefit
for us to use EXPECT -- the main difference is that within a test,
EXPECT failures do not terminate the test, while ASSERT failures do.
This further fixes a minor issue in theory_sets_type_rules_white.h
(which is still not migrated to google test yet).
|
|
We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.
This PR is the third and final step. It adds the user-facing option that turn this feature on, as well as regression tests.
|
|
The motivation of this PR is to make TheoryProxy the single point of contact to TheoryEngine from PropEngine.
This merges the helper class TheoryRegistrar into TheoryProxy.
|
|
This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.
These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.
This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.
|
|
This rewrite is no longer needed since our philosophy on rewriting extended arithmetic symbols has changed (we employ aggressive rewriting for extended arithmetic symbols in the normal rewriter). Moreover there was a soundness bug in the extended rewriter for division and mod by 0.
Fixes #5737, fixes #5740.
|
|
We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.
This PR is the second step. It includes the implementation of the main function, as well as unit tests for it.
A subsequent PR will add a user-level option that will turn on this preprocessing pass, as well as regression tests.
|
|
Fix issue5513 by throwing an exception for unsupported bag operators
|
|
Changes:
renamed d_new_skolem to d_newSkolem
renamed d_ant to d_premises (antecedent is usually used with consequent, and premise is used with conclusion)
|
|
A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits).
|
|
This PR adds inference generator for basic bag rules.
|
|
In bv-to-int, we first binarize the applications of associative-commutative operators (like bvadd etc.).
With this PR, we first check whether we already binarized a node, and only if we didn't, we perform binarization.
|
|
CAD theory (used in nl-cad) requires that polynomials are properly factorized (a finest square-free basis). This PR replaces usage of raw std::vector by a new wrapper PolyVector that ensures proper factorization whenever a polynomial is added. This fixes one piece of code that omitted factorization, leading to soundness issues as in #5726.
Fixes #5726.
|
|
|
|
|
|
We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.
This PR is the first step. It only includes the preprocessing pass infrastructure, with an empty implementation of the main function StrLenSimplify::simplify. It also adds the pass to the registry.
The implementation of this function is not complicated, but is left for a future PR in order to keep the PR short.
Future PRs will include an implementation of the main function, tests, and a command line option to turn on the pass.
|
|
This is in preparation for lazy lemmas for term formula removal.
|
|
This PR adds str.len to symbols that are considered for instantiations.
It is motivated by a benchmark that originated from Boogie.
A minimized version of that benchmark is added as a regression.
|
|
Leftover from a development branch.
|
|
Now the old proofs are used for unsat cores only if proofNew is disabled. Later commits will generate unsat cores from the new proofs when requested. Eventually we will compare them and when we confirm the new unsat core generation is better we will delete the old one.
This also does some minor refactoring in some preprocessing. No behavior is changed.
|
|
Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.
It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.
|
|
This adds functionality to CNF stream to allow e.g. TheoryProxy to be notified when a formula is asserted (not just literals).
This will be required for SAT relevancy.
No behavior changes in this PR.
|
|
This was an experimental option used in combination with separation logic.
|
|
Based on proof nodes of refutations.
|
|
|
|
This PR adds proof support for NL_SIGN lemmas.
|
|
This removes the special case of constants based on the observation that the theory that owns the type of a constant and the theory that owns its kind always should be the same.
This should lead to a small (maybe 1%) performance improvement, as this method is run ~191M times in our coverage build.
|
|
|
|
|
|
Some theories rewrite equalities during ppRewrite. An example is arithmetic with the option arith-rewrite-eq, which rewrites (= x y) to (and (>= x y) (<= x y)) during theory preprocessing.
This PR makes it so that ppRewrite is only called on equalities in preprocessing, during a new preprocessing pass "TheoryRewriteEq". On the other hand, ppRewrite is never called on new equalities generated in lemmas from TheoryEngine.
In detail, the motivation for this change:
(1) Rewriting equalities during ppRewrite is dangerous since it may break invariants wrt theory combination. In particular, equalities in splitting lemmas originating from theory combination must not be theory-preprocessed, or else we may be non-terminating or solution unsound. This can happen if a theory requests a split on (= x y) but is not notified of this atom when another theory rewrites (= x y) during ppRewrite.
(2) After this PR, we can simplify our policy for all lemmas generated, in particular, we can say that all lemmas must be theory preprocessed before their literals are asserted to TheoryEngine. This is now possible as the invariant cannot be broken (theoryRewriteEq is relegated to the preprocessor, which is only applied once). This will make LemmaProperty::PREPROCESS obsolete, which in turn will simplify several lemma caches for nonlinear and quantifiers. It will also significantly simplify proof production for the theory preprocessor (which maintains two stacks of utilities for preprocessed vs non-preprocessed lemmas).
(3) Simplifications to the above policy will make it significantly easier to implement theory-preprocessing apply when literals are asserted. It is currently not possible to implement this in a coherent way without tracking which literals were a part of lemmas marked as "do not theory-preprocess".
|
|
This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.
|
|
This PR adds proofs for lemmas that introduce bounds on the constant representing pi.
|
|
Changing our unsat core infrastructure may change the cores we produce. This can be problematic for regressions that hardcode the number of assertions we get (such as this one). This commit changes such a regression to rather expect any core. It is motivated by exactly the previously described issue occurring after using the new proof infrastructure to generate unsat cores, which yielded a smaller core.
Kudos to @4tXJ7f for the sed magic.
|
|
With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.
No significant behavior changes in this PR.
The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.
|
|
This PR adds proofs for the sine shift lemmas that add equivalent instances of the sine function where the argument is in its "main phase" between minus pi and pi.
|
|
This PR adds proofs for the lemmas from the nonlinear factoring check.
|
|
This makes all recursion (applying term formula removal on lemmas introduced by term formula removal) optionally happen at the top level call.
This is in preparation for making term formula removal lazier, in which case we will only apply one step of term formula removal at a time.
One QF_UFNIA regression times out due to changing the search, an option is changed for this benchmark.
|
|
Code could segfault if the number of wrongly applied selector applications was different from correctly applied ones.
|
|
This PR introduces the infrastructure for adding proofs to the transcendental solver:
a CDProofSet to easily create new proofs
a proof checker
|
|
This makes simplifications to the internal sygus API now that the SmtEngine interface is independent of parsing.
|
|
This PR is a follow-up to #5700 which lacked the proof checker for the proof that was added for nonlinear tangent plane lemmas.
|
|
Arith has a normal form for literals, which the rewriter computes.
Nonetheless, arith sometimes gets (and ultimately propagates) non-normal
literals. It normalizes them internally and goes about its business.
However, when asked for an explanation, it must prove the non-normal
literal, rather than the normal one.
Also includes a regression for the bug, courtesy of Andy.
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
|
|
This PR adds a proof for the tangent plane lemmas from nl-ext.
As this lemma uses some insight about the tangent plane of a multiplication term, this PR adds a new proof rule.
|
|
This PR adds a proof for the nl-ext check to split at zero. As we can use the SPLIT rule, this requires no new proof rule.
|
|
Minor updates to term conversion proof generator
|
|
The TheoryInferenceManager cached lemmas as they came in. This PR always rewrites before consulting the cache, making caching more consistent and robust. This change is coming in from proof-new.
|
