diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-08 11:06:45 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-08 17:06:45 +0000 |
| commit | b536a5fefb654439d6a0dee65b91ece12419fc0b (patch) | |
| tree | 9bdd43687b885a2379201c021fa2430b7c321f87 /src/theory/inference_id.h | |
| parent | 4a5a4ab5d7b4751ce0d730a2cff6678aa64b3306 (diff) | |
(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)
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.
Diffstat (limited to 'src/theory/inference_id.h')
| -rw-r--r-- | src/theory/inference_id.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index 8a787ca2d..995cb1083 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -42,7 +42,10 @@ enum class InferenceId { // ---------------------------------- arith theory //-------------------- preprocessing + // equivalence of term and its preprocessed form ARITH_PP_ELIM_OPERATORS, + // a lemma from arithmetic preprocessing + ARITH_PP_ELIM_OPERATORS_LEMMA, //-------------------- nonlinear core // simple congruence x=y => f(x)=f(y) ARITH_NL_CONGRUENCE, |