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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/theory/inference_id.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 94f90bc46..822f79397 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -24,6 +24,8 @@ const char* toString(InferenceId i) switch (i) { case InferenceId::ARITH_PP_ELIM_OPERATORS: return "ARITH_PP_ELIM_OPERATORS"; + case InferenceId::ARITH_PP_ELIM_OPERATORS_LEMMA: + return "ARITH_PP_ELIM_OPERATORS_LEMMA"; case InferenceId::ARITH_NL_CONGRUENCE: return "ARITH_NL_CONGRUENCE"; case InferenceId::ARITH_NL_SHARED_TERM_VALUE_SPLIT: return "ARITH_NL_SHARED_TERM_VALUE_SPLIT"; |