summaryrefslogtreecommitdiff
path: root/src/theory/inference_id.h
AgeCommit message (Collapse)Author
2021-07-26Enable default equality proofs for sets (#6931)Andrew Reynolds
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.
2021-07-15bv: Rename lazy solver to layered solver. (#6889)Mathias Preiner
2021-07-14bv: Rename simple solver to bitblast-internal. (#6888)Mathias Preiner
2021-07-12Add trace for combination splits (#6862)Andrew Reynolds
Followup PRs will unify these with the lemmas / stats infrastructure in theory inference manager.
2021-06-25pow2 -- final changes (#6800)yoni206
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.
2021-06-24pow2: Adding monotonicity lemma (#6793)yoni206
We add the lemma x<=y --> pow2(x)<=pow2(y) to the pow2 solver. Additionally, some renaming of variables is introduced for better clarity.
2021-06-15pow2: adding a kind, inference rules, and some implementations in the pow2 ↵yoni206
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.
2021-05-19Add more missing inference ids (#6313)Andrew Reynolds
This also makes the relations solver use the inference manager in the standard way.
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-13Add pool instantiation strategy (#6308)Andrew Reynolds
Adds an instantiation strategy based on user-provided pool annotations. The next PR will connect this to quantifiers engine.
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-08Add identifiers for sources of incompleteness (#6311)Andrew Reynolds
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.
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31Add missing inference ids (#6242)Andrew Reynolds
Towards having complete stats on inference ids for each lemma, fact, and conflict.
2021-03-21Clean up remaining raw uses of output channel (#6161)Andrew Reynolds
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.
2021-03-16Further standardization of strings statistics (#6128)Andrew Reynolds
Also eliminates use of raw output channel in strings.
2021-03-11Make linear arithmetic use its inference manager (#5934)Gereon Kremer
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.
2021-03-11Introduce inference ids for quantifier instantiation (#6119)Andrew Reynolds
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.
2021-03-11Direct lemmas and inference ids for sygus extension (#5960)Andrew Reynolds
This adds inference ID for the datatypes sygus solver, and changes its style to send lemmas instead of passing them to the caller.
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
This PR does some more cleanup of the includes.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-08(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)Andrew Reynolds
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.
2021-02-22Eliminate raw use of output channel and valuation in quantifiers (#5933)Andrew Reynolds
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.
2021-02-19Fill in missing inference ids in datatypes theory (#5931)Andrew Reynolds
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.
2021-02-19Cleanup of inferences in arithmetic theory (#5927)Gereon Kremer
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
2021-02-18Add InferenceIds for sets theory. (#5900)Gereon Kremer
This PR introduces new InferenceId for the theory of sets and uses them instead of InferenceId::UNKNOWN.
2021-02-18New InferenceIds for BV theory (#5909)Gereon Kremer
This PR introduces new InferenceId for the BV theory and uses them instead of InferenceId::UNKNOWN.
2021-02-18Document UF inferences (#5917)Andrew Reynolds
Document UF entries of InferenceId enum.
2021-02-17Use InferenceId in sep theory. (#5912)Gereon Kremer
This PR uses the new InferenceIds in the separation logic theory.
2021-02-17TheoryIds for UF theory. (#5901)Gereon Kremer
This PR introduces new InferenceId for the uf theory and uses them instead of InferenceId::UNKNOWN.
2021-02-17Add InferenceIds for theory of arrays (#5910)Gereon Kremer
This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.
2021-02-11Merge InferenceIds into one enum (#5892)Gereon Kremer
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback