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/arith/arith_preprocess.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/arith/arith_preprocess.h')
| -rw-r--r-- | src/theory/arith/arith_preprocess.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/arith/arith_preprocess.h b/src/theory/arith/arith_preprocess.h index 622357e73..e1f43db1b 100644 --- a/src/theory/arith/arith_preprocess.h +++ b/src/theory/arith/arith_preprocess.h @@ -22,6 +22,7 @@ #include "theory/arith/inference_manager.h" #include "theory/arith/operator_elim.h" #include "theory/logic_info.h" +#include "theory/skolem_lemma.h" namespace CVC4 { namespace theory { @@ -52,7 +53,9 @@ class ArithPreprocess * @return the trust node proving (= n nr) where nr is the return of * eliminating operators in n, or the null trust node if n was unchanged. */ - TrustNode eliminate(TNode n, bool partialOnly = false); + TrustNode eliminate(TNode n, + std::vector<SkolemLemma>& lems, + bool partialOnly = false); /** * Reduce assertion. This sends a lemma via the inference manager if atom * contains any extended operators. When applicable, the lemma is of the form: |