| Age | Commit message (Collapse) | Author |
|---|
|
applicable (#6529)
Fixes #6510.
This PR also eliminates a deprecated variant mkBooleanTermVariable from SkolemManager.
|
|
This unifies top-level substitutions and theory model substitutions. Env is now passed to the TheoryModel, which has access to top-level substitutions.
The former was used for simplfying assertions in the preprocessor, the latter was used for evaluating terms in the model.
There is no reason to have these two things be separate.
|
|
This removes the special case of TUPLE_UPDATE and RECORD_UPDATE in favor of the more general datatype update.
Datatype update is handled analogously to APPLY_SELECTOR / APPLY_TESTER.
|
|
This moves regression test that exceed the time limit of their
respective level to the appropriate level. It further updates the
guidelines in the README with information on how to properly categorize
regression tests into levels (with time limits).
Note: Test regress3/issue4717.smt2 was previously unsolved (unknown) and
is now sat (Z3 agrees).
|
|
|
|
Fixes #6495.
|
|
|
|
SymFPU does not allow to_fp conversion from signed bv of size 1. This
adds rewrites for this case.
Rewrites for the constant and the non-constant cases were tested in
isolation.
|
|
This automatically applies @martin-cs's working patch from 2020-11-14.
It fixes several issues, all covered open issues are added as
regression tests.
Fixes #3582.
Fixes #5511.
Fixes #6164.
|
|
This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:
(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification
The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.
In this PR:
define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.
|
|
Benchmark is taking 40 seconds on production, due to the configuration that tests --check-unsat-cores.
|
|
This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas.
This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables.
This was reported by Geoff Sutcliffe via a TPTP run.
|
|
|
|
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.
This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
|
|
In each case, previously we were generating a define-fun, what we needed was to do a model substitution.
This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.
|
|
This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
|
|
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
|
|
This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.
|
|
simplification (#6394)
This PR removes the quantifiers macro preprocessing pass, which had several shortcomings, both in terms of performance and features.
This makes it so that quantifier macros are the (optional) implementation of TheoryQuantifiers::ppAssert.
In other words, quantifiers can now be put into "solved form", forall x. P(x) ---> P = lambda x. true.
This is part of an effort to improve proofs for preprocessing, as well as centralizing our reason about substitutions for the sake of efficiency.
|
|
Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.
Fixes #5473.
|
|
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
|
|
|
|
This PR modifies the behavior of the reconstruction algorithm when the term to reconstruct contains two or more equivalent sub-terms, but one is easier to reconstruct than the others. Since we do not know which one is easier to reconstruct by matching, we match against all sub-terms. If a solution is found for one sub-term, we use it to solve the others.
|
|
|
|
This does some refactoring of quantifiers macros preprocessing pass to use up-to-date utility methods, including lambdas, substitutions, methods for getting free variables.
This is work towards adding proofs for macros.
|
|
When a command is invoked, its result/status may be printed depending on its current verbosity, which (for probably an outdated reason) is stored in SMTEngine. One of my previous PRs modified the SMTEngine to return the verbosity as an sexpr. The modification works correctly when the output language is SMT2, but it breaks down with the AST output language, which prints sexprs in a different way. This PR fixes this bug by making SMTEngine return options as strings instead of sexpr.
|
|
This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite.
Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).
|
|
|
|
|
|
Adds 3 of the 6 benchmarks from issue 6214, the 1st and 5th benchmarks timeout.
Fixes #6214.
These benchmarks were fixed by 3c98bb2.
|
|
Previously, the circuit propagator was not learning literals of the form (= x t) where x is Boolean, since this term was not treated as a theory literal.
This commit changes that, which improves performance significantly, since it
allows the elimination of Boolean variables, which, in turn, can make the
justification heuristic much more effective.
Signed-off-by: Andres Noetzli noetzli@amazon.com
|
|
The options --check-synth-sol and --check-abducts are independent from the rest of the solver. Hence, it is not necessary to run with/without them enabled in our regressions.
This saves roughly 30-40 seconds on regression regress0-2.
|
|
Previously, we were not checking models / proofs / unsat cores for cvc inputs on CI.
|
|
Fixes #5101.
|
|
Fixes #4400.
|
|
Fixes #6298.
Enables parsing of par in the sygus parser, and adds support for default grammar construction.
Also fixes a bug related to single invocation for non-function types.
|
|
|
|
Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.
This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.
|
|
Adds a benchmark that was previous sensitive to assertion order, fixes #4420.
|
|
Fixes benchmarks 2 and 3 from #5848.
|
|
Fixes #5942.
This benchmark was fixed by recent changes to ppRewrite.
|
|
|
|
Fixes #4370.
|
|
Fixes #4179.
|
|
Fixes #6271.
This was triggered by recent fixes, this fixes solution soundness issues with symbolic regular expressions due to spuriously included antecedants, which made lemmas SAT-context dependent while being cached as user-context dependent.
|
|
|
|
Fixes #4328.
|
|
We were getting types for set singleton/membership in a way that was unsafe for subtyping, which was leading to incorrectly computing care graphs for sets of reals.
Fixes #5705.
|
|
Fixes the first benchmark from #6203.
|
|
An RE unfolding lemma may rewrite to true for tautological RE memberships that our rewriter does not rewrite the membership to true.
An example is (str.in_re x (re.* (re.union (str.to_re "A") (str.to_re x))).
This PR ensures we are robust to these cases.
This fixes benchmarks 3-5 from #6203. Benchmark 3 is added here, 4-5 time out.
|
