Age | Commit message (Collapse) | Author |
|
This enables default support for equality proofs in the theory of sets.
This is in preparation for proofs in the central equality engine, which requires that all active theories that use the central equality engine at least support the default interaction with the equality engine.
|
|
|
|
|
|
Followup PRs will unify these with the lemmas / stats infrastructure in theory inference manager.
|
|
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.
|
|
solver (#6736)
This PR is the sequel of #6676 .
It adds the `POW2` kind, inference rules that will be used in the `pow2` solver, an implementation of one function of the solver, as well as stubs for the others. The next PR will include more implementations.
|
|
This also makes the relations solver use the inference manager in the standard way.
|
|
|
|
Adds an instantiation strategy based on user-provided pool annotations.
The next PR will connect this to quantifiers engine.
|
|
|
|
|
|
This PR classifies all internal kinds of incompleteness as identifiers.
It makes it so TheoryEngine records an identifier when its incomplete flag is set.
The next step will be to possibly communicate this value to the user.
|
|
|
|
|
|
Towards having complete stats on inference ids for each lemma, fact, and conflict.
|
|
After this PR, with only a few exceptions, all calls to output channel for lemmas, conflicts are made through inference manager.
This is work towards standardizing the statistics for theories.
|
|
Also eliminates use of raw output channel in strings.
|
|
This PR refactors the linear arithmetic solver to properly use its inference manager, instead of directly sending lemmas to the output channel. To do this, it introduces new InferenceIds for the various linear lemmas.
|
|
This makes quantifiers use standard inference ids.
This eliminates the need to track ad-hoc statistics, per instantiation type.
This makes minor modifications to a few interfaces in quantifiers to enable this.
|
|
This adds inference ID for the datatypes sygus solver, and changes its style to send lemmas instead of passing them to the caller.
|
|
This PR does some more cleanup of the includes.
|
|
|
|
Due to recent simplifications in the internal calculus, we will no longer reason about WITNESS terms in conclusions of ProofNode, instead WITNESS terms will only be for bookkeeping.This means that some implementations of ppRewrite must change to return SKOLEM instead of WITNESS terms.
Since witness terms are currently used as a way of specifying "replace t by skolem k, and send a lemma about k", a followup PR will update Theory::ppRewrite to take an additional argument std::vector<SkolemLemma>& lems where new lemmas must be explicitly added to a vector (instead of encoded as witness). Then, all Theory::ppRewrite will return skolems instead of witness terms.
This PR changes arithmetic in preparation for this change.
Notice that I'm introducing SkolemLemma in this PR, which is a very common pattern that can simplify some of our interfaces, e.g. see https://github.com/CVC4/CVC4/blob/master/src/smt/term_formula_removal.h#L93, https://github.com/CVC4/CVC4/blob/master/src/prop/prop_engine.h#L94.
Note that the indentation of code in operator_elim.cpp changed.
|
|
This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.
|
|
Also updates its inference manager to not track stats since the standard ones are now used.
This also sets up some dependencies in the sygus extension which will be used to implement InferenceId for the sygus extension, to be done on a separate PR.
|
|
This PR cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager:
remove the ArithLemma class and uses SimpleTheoryLemma instead
only use NlLemma if we actually need it
use proper InferenceIds everywhere
remove unused code in the nonlinear extension
|
|
This PR introduces new InferenceId for the theory of sets and uses them instead of InferenceId::UNKNOWN.
|
|
This PR introduces new InferenceId for the BV theory and uses them instead of InferenceId::UNKNOWN.
|
|
Document UF entries of InferenceId enum.
|
|
This PR uses the new InferenceIds in the separation logic theory.
|
|
This PR introduces new InferenceId for the uf theory and uses them instead of InferenceId::UNKNOWN.
|
|
This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.
|
|
This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.
|