| Age | Commit message (Collapse) | Author |
|---|
|
This cleans up various interfaces of Theory now that all theories have been updated to the new standard. This includes making check non-virtual, standardizing when trigger terms are added to equality engines, and simplifications for collectModelInfo.
|
|
This class is an important utility in preprocessing, which we are adding proof support for. This simplifies the interface of this class with regards to unused interfaces for clarity.
|
|
This fixes several subtle issues with theory preprocessing.
The main fix is to ensure proofs are correct for cases where the theory preprocessor applies either with or without theory preprocessing (calling Theory::ppRewrite on subterms) enabled, see argument doTheoryPreprocess of preprocess. If disabled, it applies term formula removal and rewriting only. This is required for processing lemmas that are marked as "do not preprocess", which is an optimization, but is also necessary since theory combination may e.g. split on equality that was solved during ppRewrite. The solution is to use 2 separate term conversion sequences for these 2 cases.
It also fixes an issue where preprocessing is term-context-sensitive: terms underneath quantifiers are treated differently. This is now handled by a new TermContext callback "InQuantTermContext".
|
|
This makes the shared terms database use a proof equality engine as a layer on top of its equality engine, analogous to how this done in theories.
|
|
This PR makes sure that enabling strings and nonlinear real arithmetic at the same time works fine.
Right now, the configuration for strings enforces linear arithmetic if no integers are enabled, in particular for NRA.
Fixed #5109.
|
|
This decouples the arithmetic rewriter, the operator eliminator and the non-linear extension from TheoryArithPrivate and performs some minor cleanup.
This is in preparation for further refactoring of (lazy) arithmetic operator elimination.
|
|
This commit threads proofs through the core of arith:
Constraint::externalExplain, which recursively explain arith literals.
One of the base cases here is asking the EE for an explanation, through
the congruence manager. To delay implementing proofs in
ArithCongruenceManager to a separate commit, we stub out proof
production in ArithCongruenceManager::explain for now.
|
|
|
|
This includes adding a basic inference manager to arrays that ensures that the correct applications of PfRule are given to the inference manager.
Note that some calls to lemma are yet to be converted. Also note that some minor simplifications were made for unnecessary parts of the code.
|
|
This PR adds options to add additional ground terms to the SyGuS instantiation grammars.
|
|
This updates the theory of arithmetic to use the standard check callbacks (preCheck, postCheck, preNotifyFact, notifyFact). It also refactors some use of the non-linear solver which will solely live in TheoryArith.
The longer term goal is to have TheoryArithPrivate be responsible for linear arithmetic solving only, and to be treated as a black box. Eventually, the non-linear solver will be removed from this class.
This PR is required for several things, including refactoring of preprocessing and expand definitions for arithmetic (div/mod will not be eliminated eagerly). It is also required for fixing issues related to div/mod appearing in instantiations.
This is the last class to have a custom check method. Followup PR will make Theory::check non-virtual.
|
|
|
|
While the CAD subsolver already provided for a way to use the linear model to seed the model search, it was not actually used yet.
This PR now does use it, though it is disabled by a Boolean flag.
|
|
pipeline (#5164)
This PR eliminates all uses of assertions pipeline that are not proper, which two-fold:
(1) The assertion list should never be modified in a custom way (without going through replace / push_back),
(2) Places where an assertion is "conjoined" to an existing spot in the vector should use conjoin instead of replace.
This is required for proper proof generation.
This fixes CVC4/cvc4-projects#75.
|
|
Previously, the SmtEngine was using an interface through TheoryEngine to set user attributes to indicate that e.g. a synth-fun is associated with a given grammar. Since SmtEngine and its members are internal now, this can simply be done directly via attributes. This makes it so that SygusSolver does not depend on TheoryEngine nor does it require the TheoryEngine to be initialized at the time a synth-fun is created.
|
|
Previously, BitVector::setBit only allowed to set the bit at the given
index to 1. This changes its behavior to be also able to set it to 0.
|
|
|
|
This PR simply removes an assertion that would trigger whenever the arithmetic theory asserts a model that contains something else than a constant. This can be the case with witness terms.
In offline discussion we concluded that this discussion was overly strict. Note that these examples may still hit an error during model validation (Cannot run check-model on a model with approximate values.).
This PR also fixes a debug output I found during debugging.
Fixes #5113.
|
|
The strategy class added in #5160 was missing the proper includes for std::ostream. For some reason it works for most configurations, but triggers compilation errors in certain cases.
|
|
This PR adds a flexible strategy for the nonlinear extension that replaces the handwritten code in checkLastCall().
|
|
This updates shared solver to have dynamic allocation of equality engine, analogous to theory solvers.
|
|
This class will be used in the theory preprocessor and is planned to be used in other preprocessing passes that can be understood as sequences of rewrite systems.
|
|
Also fixes some weird orderings in src/CMakeLists.txt
|
|
Fix bags headers
|
|
This commit threads ProofNodeManager, EagerProofGenerator, etc
throughout the arith theory into the appropriate locations. These
objects are currently unused, but will be used in future commits.
Crediting Andy, since he set up some of this.
Co-authored-by: Andrew Reynolds andrew.j.reynolds@gmail.com
|
|
pipeline (#5136)
This PR makes several fixes to preprocess proof generator, making it user-context dependent and making it avoid cyclic proofs. It additionally makes assertion pipeline a new interface "conjoin" which should always be used when we conjoin a new assertion to an old position in the assertion vector. It also removes an unnecessary interface to assertion pipeline.
Next PRs will clean up the use of assertions pipeline in all preprocessing passes to use the proper interfaces. This includes removing non-constant references to assertions, which has been fixed on proof-new.
|
|
The post processor connects the two proofs in the prop engine: the refutation proof in the SAT solver and the CNF transformation proof in the CNF stream. The proof generators from theory engine in the latter are also expanded during the connection.
|
|
|
|
A proof generator that wraps the original CNF stream, to be used when the prop engine is proof producing. It tracks in a lazy cdproof both the concrete clausification steps and the proof generators of the formulas being clausified (in particular, theory lemmas).
|
|
This PR performs some cleanups in the nonlinear extension, in particular it removes the old lemma collection scheme. It is no longer needed, as all subsolvers use the inference manager.
|
|
The assertions object is currently not cleared on resetAssertions, only the prop engine is reset. This means that if a user added assertion, did not use them in a check-sat, and then called reset-assertions, they would not be removed from the assertions pipeline (storing the pending assertions before they are sent to the prop engine).
This fixes #5144.
|
|
The arith proof checker was not being built (not in cmake). Now it is. A
few dependencies were missing.
|
|
|
|
|
|
Includes minor changes to the proof checker and a fix in the instantiate module.
|
|
Tracks the refutation proof built by Minisat. See the header for extensive explanations.
This commit also adds a few dependencies for the SAT proof manager to work (making it a friend of the SAT solver, getting the cnf stream from theory proxy, having lazy cdproof chain give all the links).
|
|
This PR implements rewrite rules for bags. This PR focuses on rewrite rules for non constant nodes.
Rewriting nodes with constant children is delegated to bags::NormalForm class (future PR).
|
|
This PR adds a new utility class that extracts bounds on single variables from theory atoms like x > 0 or y <= 17. It does not perform further reasoning (like recognizing x > y with y > 3 as a bound).
Note that the functionality was introduced in arith/nl/icp/variable_bounds.h, but is now available using Node only.
This PR also replaces the VariableBounds by BoundInference in the icp solver which allowed for checking the code.
|
|
The option --sygus-qe-preproc performs quantifier elimination to coerce certain synthesis conjectures to be single invocation. This technique was broken when multiple synthesis functions were present. This fixes the issue and adds a regression where --sygus-qe-preproc enables a benchmark to be quickly solved.
|
|
This PR migrates the nl_solver part of the nonlinear extension to use the new inference manager as well.
It adds a new method clearWaitingLemmas to the inference manager and uses ArithLemma (though NlLemma exists) as we don't need the additional functionality of NlLemma.
|
|
This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database.
It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus.
This PR has no intended behavior changes.
FYI @barrettcw
|
|
This fixes an issue with single invocation solution reconstruction where the preprocessed quantified formula contains internal skolems, thus prohibiting reconstruction. The solution is to use the original quantified formula when doing solution reconstruction. This adds a regression demonstrating the issue.
|
|
Bit-vector operator bvxnor was previously mistakenly marked as
left-assoicative in SMT-LIB. This has recently been corrected in
SMT-LIB. We now restrict bvxnor to only allow two operands in order to
avoid confusion about the semantics, since the behavior of n-ary
operands to bvxnor is now undefined in SMT-LIB.
|
|
Currently, the CEGIS refinement loop of the sygus solver may terminate with "unknown" when a duplicate counterexample is generated. This is caused by a candidate t for a conjecture exists f. forall x. G[f, x] such that:
(1) G[t, c] evaluates to a non-constant expression,
(2) ~G[t, k] is satisfiable with model k = c.
Notice this exclusively limited to theories with incomplete functions, e.g. (non-linear) division.
In this case, we know that t is an incorrect solution, but the counterexample we found was not new.
Currently, we abort with "unknown" since the counterexample was not new. After this PR, we exclude t and continue, which is uncontroversially the correct behavior.
This PR moves the resposibility for lemma from synth engine to synth conjecture, which simplifies the behavior of the main check conjecture method.
|
|
Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream.
|
|
|
|
This defines the function definition finite model finding as a proper preprocessing pass.
This is required for cleaning/fixing bugs in the preprocessor on proof-new.
There are no intended behavior changes in this PR, although the code for the pass was updated to the new style guidelines.
|
|
This changes the lemma vs fact policy for datatype equalities. Previously, datatype equalities were sent as lemmas unless they were over datatypes that were composed of datatypes only. This is now changed so that equalities that do not involve direct subterms with finite non-datatype types are kept internal.
The primary type of equality that this targets are "Instantiate" equalities, e.g. the conclusion of:
(is-cons x) => x = (cons (head x) (tail x))
These equalities have been observed to generate large amounts of new terms for many benchmarks.
With this PR, the the challenging Facebook benchmark goes from 2 min 45 sec -> 29 sec. If the instantiate rule is disabled altogether, it still correctly solves, and is faster (~14 seconds), which however is not correct in general.
This change triggered two other issues:
(1) A relations benchmark involving transitive closure now times out. This has been a common issue for the relations solver and should be revisited.
(2) A potential issue with doPendingLemmas in InferenceManagerBuffer was uncovered. In rare cases, we can be re-entrant into this method since OutputChannel::lemma may trigger further preregistration of terms, which can trigger a recursive call to doPendingLemmas in the case of datatypes, which causes a segfault due to corrupting an iterator. This PR adds a simple guard for this method.
This PR also fixes some existing issues in computing cardinality for parametric datatypes.
|
|
This disables the CAV 2018 techniques for BV quantifier instantiation when solving sygus since they may generate terms with witness in them. This adds a regression where this occurs.
I've opened an cvc4 projects issue to revisit this (CVC4/cvc4-projects#227).
|
|
This PR moves the iand solver (within the nonlinear extension) to use the new inference manager to send lemmas.
|
