From b536a5fefb654439d6a0dee65b91ece12419fc0b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 8 Mar 2021 11:06:45 -0600 Subject: (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& 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. --- src/theory/inference_id.cpp | 2 ++ 1 file changed, 2 insertions(+) (limited to 'src/theory/inference_id.cpp') 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"; -- cgit v1.2.3