From a6d3c9e7fb765704f34815900712b10e85687edc Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 26 Jan 2021 19:20:32 -0800 Subject: Thread proofs through arith channels & similar (#5818) Thread proofs through conflict/lemma storages & channels in TheoryArithPrivate d_acTmp d_approxCuts lemma output channel conflict output channel --- src/theory/arith/theory_arith_private.cpp | 47 +++++++++++++++++++++++-------- src/theory/arith/theory_arith_private.h | 6 ++-- 2 files changed, 40 insertions(+), 13 deletions(-) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index d51efa707..3b5f0dd82 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1704,12 +1704,28 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(TNode assertion) Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion; Assert(!isSetup(eq)); Node reEq = Rewriter::rewrite(eq); + Debug("arith::distinct::const") << "Assertion: " << assertion << std::endl; + Debug("arith::distinct::const") << "Eq : " << eq << std::endl; + Debug("arith::distinct::const") << "reEq : " << reEq << std::endl; if(reEq.getKind() == CONST_BOOLEAN){ if(reEq.getConst() == isDistinct){ // if is (not true), or false Assert((reEq.getConst() && isDistinct) || (!reEq.getConst() && !isDistinct)); - raiseBlackBoxConflict(assertion); + if (proofsEnabled()) + { + Pf assume = d_pnm->mkAssume(assertion); + std::vector assumptions = {assertion}; + Pf pf = d_pnm->mkScope(d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, + {d_pnm->mkAssume(assertion)}, + {}), + assumptions); + raiseBlackBoxConflict(assertion, pf); + } + else + { + raiseBlackBoxConflict(assertion); + } } return NullConstraint; } @@ -1978,7 +1994,7 @@ void TheoryArithPrivate::outputConflicts(){ void TheoryArithPrivate::outputTrustedLemma(TrustNode lemma) { Debug("arith::channel") << "Arith trusted lemma: " << lemma << std::endl; - (d_containing.d_out)->lemma(lemma.getNode()); + (d_containing.d_out)->trustedLemma(lemma); } void TheoryArithPrivate::outputLemma(TNode lem) { @@ -1989,7 +2005,7 @@ void TheoryArithPrivate::outputLemma(TNode lem) { void TheoryArithPrivate::outputTrustedConflict(TrustNode conf) { Debug("arith::channel") << "Arith trusted conflict: " << conf << std::endl; - (d_containing.d_out)->conflict(conf.getNode()); + (d_containing.d_out)->trustedConflict(conf); } void TheoryArithPrivate::outputConflict(TNode lit) { @@ -2663,7 +2679,7 @@ std::vector TheoryArithPrivate::replayLogRec(ApproximateSimplex d_replayedLemmas = replayLemmas(approx); Assert(d_acTmp.empty()); while(!d_approxCuts.empty()){ - Node lem = d_approxCuts.front(); + TrustNode lem = d_approxCuts.front(); d_approxCuts.pop(); d_acTmp.push_back(lem); } @@ -2673,7 +2689,7 @@ std::vector TheoryArithPrivate::replayLogRec(ApproximateSimplex /* move into the current context. */ while(!d_acTmp.empty()){ - Node lem = d_acTmp.back(); + TrustNode lem = d_acTmp.back(); d_acTmp.pop_back(); d_approxCuts.push_back(lem); } @@ -2812,7 +2828,8 @@ bool TheoryArithPrivate::replayLemmas(ApproximateSimplex* approx){ Node implication = asLemma.impNode(implied); // DO NOT CALL OUTPUT LEMMA! - d_approxCuts.push_back(implication); + // TODO (project #37): justify + d_approxCuts.push_back(TrustNode::mkTrustLemma(implication, nullptr)); Debug("approx::lemmas") << "cut["<mkTrustNode(branch, PfRule::SPLIT, {}, {lit}); + } + else + { + d_approxCuts.push_back(TrustNode::mkTrustLemma(branch, nullptr)); + } ++(d_statistics.d_mipExternalBranch); Debug("approx::lemmas") << "branching "<< root <<" as " << branch << endl; } @@ -3068,7 +3092,7 @@ bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel){ Assert(branch.getNode().getKind() == kind::OR); Node rwbranch = Rewriter::rewrite(branch.getNode()[0]); if(!isSatLiteral(rwbranch)){ - d_approxCuts.push_back(branch.getNode()); + d_approxCuts.push_back(branch); return true; } } @@ -3523,12 +3547,12 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) if(!d_approxCuts.empty()){ bool anyFresh = false; while(!d_approxCuts.empty()){ - Node lem = d_approxCuts.front(); + TrustNode lem = d_approxCuts.front(); d_approxCuts.pop(); Debug("arith::approx::cuts") << "approximate cut:" << lem << endl; - anyFresh = anyFresh || hasFreshArithLiteral(lem); + anyFresh = anyFresh || hasFreshArithLiteral(lem.getNode()); Debug("arith::lemma") << "approximate cut:" << lem << endl; - outputLemma(lem); + outputTrustedLemma(lem); } if(anyFresh){ emmittedConflictOrSplit = true; @@ -3630,6 +3654,7 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) if(possibleConflict != Node::null()){ revertOutOfConflict(); Debug("arith::conflict") << "dio conflict " << possibleConflict << endl; + // TODO (project #37): justify (proofs in the DIO solver) raiseBlackBoxConflict(possibleConflict); outputConflicts(); emmittedConflictOrSplit = true; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 1a06355a0..56e8fa4b0 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -713,8 +713,10 @@ private: return (d_containing.d_valuation).getSatValue(n); } - context::CDQueue d_approxCuts; - std::vector d_acTmp; + /** Used for replaying approximate simplex */ + context::CDQueue d_approxCuts; + /** Also used for replaying approximate simplex. "approximate cuts temporary storage" */ + std::vector d_acTmp; /** Counts the number of fullCheck calls to arithmetic. */ uint32_t d_fullCheckCounter; -- cgit v1.2.3