diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-27 14:44:49 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-27 12:44:49 -0700 |
commit | faa97a6f1ee19760dfb0a79ad18c53afdff6b09a (patch) | |
tree | 557cee42a539a838eaec36a8b8d69a5e1eb70d3c /src/theory/arith/theory_arith.cpp | |
parent | d5141e4086898bb66809c76d4614503e3a2efd6e (diff) |
(proof-new) Arithmetic operator elim proof producing (#4783)
This updates the interface for arithmetic operator elimination for the new proof format.
The actual proof production of the operator elimination class (providing proofs for
introduced witness terms) will be done in a separate PR.
This also changes the witness terms introduced by this class so their body is in
Skolem form, which simplifies term formula removal.
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Diffstat (limited to 'src/theory/arith/theory_arith.cpp')
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index fcbfd1baf..52321ffd4 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -39,7 +39,7 @@ TheoryArith::TheoryArith(context::Context* c, ProofNodeManager* pnm) : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo, pnm), d_internal( - new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo)), + new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)), d_ppRewriteTimer("theory::arith::ppRewriteTimer"), d_proofRecorder(nullptr) { @@ -78,8 +78,7 @@ void TheoryArith::finishInit() TrustNode TheoryArith::expandDefinition(Node node) { - Node expNode = d_internal->expandDefinition(node); - return TrustNode::mkTrustRewrite(node, expNode, nullptr); + return d_internal->expandDefinition(node); } void TheoryArith::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -93,12 +92,7 @@ void TheoryArith::addSharedTerm(TNode n){ TrustNode TheoryArith::ppRewrite(TNode atom) { CodeTimer timer(d_ppRewriteTimer, /* allow_reentrant = */ true); - Node ret = d_internal->ppRewrite(atom); - if (ret != atom) - { - return TrustNode::mkTrustRewrite(atom, ret, nullptr); - } - return TrustNode::null(); + return d_internal->ppRewrite(atom); } Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubstitutions) { |