From e10c381b821337c239479d86fbf1d2eb617c590a Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 6 Oct 2020 12:15:46 -0700 Subject: [PATCH] (proof-new) proofs for ArithCongMan -> ee facts (#5207) Threads proof production through the ArithCongruenceManager's pipeline of information to the equality engine. The idea is to define a method: ArithCongruenceManager::assertLitToEqualityEngine(literal, reason, pf) This method asserts a literal to the equality engine with the given proof and reason. It stores the proof of the literal for the equality engine's future reference, and is smart about symmetric literals. This machinery uses proofs that are not closed over the reason, as the equality engine requires. Other functions in the pipeline: assertionToEqualityEngine equalsCostant construct proofs and call assertLitToEqualityEngine. Future commits will address the ee -> ArithCongruenceManager pipeline, and the relationship between ArithCongruenceManager and the rest of arithmetic. --- src/theory/arith/congruence_manager.cpp | 205 +++++++++++++++++++++--- src/theory/arith/congruence_manager.h | 40 ++++- src/theory/arith/constraint.h | 6 +- 3 files changed, 224 insertions(+), 27 deletions(-) diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index f2db70d90..404b5bcd0 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -48,8 +48,11 @@ ArithCongruenceManager::ArithCongruenceManager( d_satContext(c), d_userContext(u), d_pnm(pnm), + // Construct d_pfGenEe with the SAT context, since its proof include + // unclosed assumptions of theory literals. d_pfGenEe( new EagerProofGenerator(pnm, c, "ArithCongruenceManager::pfGenEe")), + // Construct d_pfGenEe with the USER context, since its proofs are closed. d_pfGenExplain(new EagerProofGenerator( pnm, u, "ArithCongruenceManager::pfGenExplain")), d_pfee(nullptr) @@ -208,13 +211,32 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP ++(d_statistics.d_watchedVariableIsZero); ArithVar s = lb->getVariable(); - Node reason = Constraint::externalExplainByAssertions(lb,ub); + TNode eq = d_watchedEqualities[s]; + ConstraintCP eqC = d_constraintDatabase.getConstraint( + s, ConstraintType::Equality, lb->getValue()); + NodeBuilder<> reasonBuilder(Kind::AND); + auto pfLb = lb->externalExplainByAssertions(reasonBuilder); + auto pfUb = ub->externalExplainByAssertions(reasonBuilder); + Node reason = safeConstructNary(reasonBuilder); + std::shared_ptr pf{}; + if (isProofEnabled()) + { + pf = d_pnm->mkNode( + PfRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eqC->getProofLiteral()}); + pf = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {eq}); + } d_keepAlive.push_back(reason); - assertionToEqualityEngine(true, s, reason); + Trace("arith-ee") << "Asserting an equality on " << s << ", on trichotomy" + << std::endl; + Trace("arith-ee") << " based on " << lb << std::endl; + Trace("arith-ee") << " based on " << ub << std::endl; + assertionToEqualityEngine(true, s, reason, pf); } void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){ + Debug("arith::cong") << "Cong::watchedVariableIsZero: " << *eq << std::endl; + Assert(eq->isEquality()); Assert(eq->getValue().sgn() == 0); @@ -225,23 +247,86 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP eq){ //Explain for conflict is correct as these proofs are generated //and stored eagerly //These will be safe for propagation later as well - Node reason = eq->externalExplainByAssertions(); + NodeBuilder<> nb(Kind::AND); + // An open proof of eq from literals now in reason. + if (Debug.isOn("arith::cong")) + { + eq->printProofTree(Debug("arith::cong")); + } + auto pf = eq->externalExplainByAssertions(nb); + if (isProofEnabled()) + { + pf = d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {d_watchedEqualities[s]}); + } + Node reason = safeConstructNary(nb); d_keepAlive.push_back(reason); - assertionToEqualityEngine(true, s, reason); + assertionToEqualityEngine(true, s, reason, pf); } void ArithCongruenceManager::watchedVariableCannotBeZero(ConstraintCP c){ + Debug("arith::cong::notzero") + << "Cong::watchedVariableCannotBeZero " << *c << std::endl; ++(d_statistics.d_watchedVariableIsNotZero); ArithVar s = c->getVariable(); + Node disEq = d_watchedEqualities[s].negate(); //Explain for conflict is correct as these proofs are generated and stored eagerly //These will be safe for propagation later as well - Node reason = c->externalExplainByAssertions(); - + NodeBuilder<> nb(Kind::AND); + // An open proof of eq from literals now in reason. + auto pf = c->externalExplainByAssertions(nb); + if (Debug.isOn("arith::cong::notzero")) + { + Debug("arith::cong::notzero") << " original proof "; + pf->printDebug(Debug("arith::cong::notzero")); + Debug("arith::cong::notzero") << std::endl; + } + Node reason = safeConstructNary(nb); + if (isProofEnabled()) + { + if (c->getType() == ConstraintType::Disequality) + { + Assert(c->getLiteral() == d_watchedEqualities[s].negate()); + // We have to prove equivalence to the watched disequality. + pf = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {disEq}); + } + else + { + Debug("arith::cong::notzero") + << " proof modification needed" << std::endl; + + // Four cases: + // c has form x_i = d, d > 0 => multiply c by -1 in Farkas proof + // c has form x_i = d, d > 0 => multiply c by 1 in Farkas proof + // c has form x_i <= d, d < 0 => multiply c by 1 in Farkas proof + // c has form x_i >= d, d > 0 => multiply c by -1 in Farkas proof + const bool scaleCNegatively = c->getType() == ConstraintType::LowerBound + || (c->getType() == ConstraintType::Equality + && c->getValue().sgn() > 0); + const int cSign = scaleCNegatively ? -1 : 1; + TNode isZero = d_watchedEqualities[s]; + const auto isZeroPf = d_pnm->mkAssume(isZero); + const auto nm = NodeManager::currentNM(); + const auto sumPf = d_pnm->mkNode( + PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, + {isZeroPf, pf}, + // Trick for getting correct, opposing signs. + {nm->mkConst(Rational(-1 * cSign)), nm->mkConst(Rational(cSign))}); + const auto botPf = d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)}); + std::vector assumption = {isZero}; + pf = d_pnm->mkScope(botPf, assumption, false); + Debug("arith::cong::notzero") << " new proof "; + pf->printDebug(Debug("arith::cong::notzero")); + Debug("arith::cong::notzero") << std::endl; + } + Assert(pf->getResult() == disEq); + } d_keepAlive.push_back(reason); - assertionToEqualityEngine(false, s, reason); + assertionToEqualityEngine(false, s, reason, pf); } @@ -417,18 +502,86 @@ void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){ d_watchedEqualities.set(s, eq); } -void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar s, TNode reason){ +void ArithCongruenceManager::assertLitToEqualityEngine( + Node lit, TNode reason, std::shared_ptr pf) +{ + bool isEquality = lit.getKind() != Kind::NOT; + Node eq = isEquality ? lit : lit[0]; + Assert(eq.getKind() == Kind::EQUAL); + + Trace("arith-ee") << "Assert to Eq " << lit << ", reason " << reason + << std::endl; + if (isProofEnabled()) + { + if (CDProof::isSame(lit, reason)) + { + Trace("arith-pfee") << "Asserting only, b/c implied by symm" << std::endl; + // The equality engine doesn't ref-count for us... + d_keepAlive.push_back(eq); + d_keepAlive.push_back(reason); + d_ee->assertEquality(eq, isEquality, reason); + } + else if (hasProofFor(lit)) + { + Trace("arith-pfee") << "Skipping b/c already done" << std::endl; + } + else + { + setProofFor(lit, pf); + Trace("arith-pfee") << "Actually asserting" << std::endl; + if (Debug.isOn("arith-pfee")) + { + Trace("arith-pfee") << "Proof: "; + pf->printDebug(Trace("arith-pfee")); + Trace("arith-pfee") << std::endl; + } + // The proof equality engine *does* ref-count for us... + d_pfee->assertFact(lit, reason, d_pfGenEe.get()); + } + } + else + { + // The equality engine doesn't ref-count for us... + d_keepAlive.push_back(eq); + d_keepAlive.push_back(reason); + d_ee->assertEquality(eq, isEquality, reason); + } +} + +void ArithCongruenceManager::assertionToEqualityEngine( + bool isEquality, ArithVar s, TNode reason, std::shared_ptr pf) +{ Assert(isWatchedVariable(s)); TNode eq = d_watchedEqualities[s]; Assert(eq.getKind() == kind::EQUAL); - Trace("arith-ee") << "Assert " << eq << ", pol " << isEquality << ", reason " << reason << std::endl; - if(isEquality){ - d_ee->assertEquality(eq, true, reason); - }else{ - d_ee->assertEquality(eq, false, reason); + Node lit = isEquality ? Node(eq) : eq.notNode(); + Trace("arith-ee") << "Assert to Eq " << eq << ", pol " << isEquality + << ", reason " << reason << std::endl; + assertLitToEqualityEngine(lit, reason, pf); +} + +bool ArithCongruenceManager::hasProofFor(TNode f) const +{ + Assert(isProofEnabled()); + if (d_pfGenEe->hasProofFor(f)) + { + return true; } + Node sym = CDProof::getSymmFact(f); + Assert(!sym.isNull()); + return d_pfGenEe->hasProofFor(sym); +} + +void ArithCongruenceManager::setProofFor(TNode f, + std::shared_ptr pf) const +{ + Assert(!hasProofFor(f)); + d_pfGenEe->mkTrustNode(f, pf); + Node symF = CDProof::getSymmFact(f); + auto symPf = d_pnm->mkNode(PfRule::SYMM, {pf}, {}); + d_pfGenEe->mkTrustNode(symF, symPf); } void ArithCongruenceManager::equalsConstant(ConstraintCP c){ @@ -441,16 +594,18 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP c){ Node xAsNode = d_avariables.asNode(x); Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart()); - - //No guarentee this is in normal form! + // No guarentee this is in normal form! + // Note though, that it happens to be in proof normal form! Node eq = xAsNode.eqNode(asRational); d_keepAlive.push_back(eq); - Node reason = c->externalExplainByAssertions(); + NodeBuilder<> nb(Kind::AND); + auto pf = c->externalExplainByAssertions(nb); + Node reason = safeConstructNary(nb); d_keepAlive.push_back(reason); Trace("arith-ee") << "Assert equalsConstant " << eq << ", reason " << reason << std::endl; - d_ee->assertEquality(eq, true, reason); + assertLitToEqualityEngine(eq, reason, pf); } void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){ @@ -463,18 +618,28 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){ << ub << std::endl; ArithVar x = lb->getVariable(); - Node reason = Constraint::externalExplainByAssertions(lb,ub); + NodeBuilder<> nb(Kind::AND); + auto pfLb = lb->externalExplainByAssertions(nb); + auto pfUb = ub->externalExplainByAssertions(nb); + Node reason = safeConstructNary(nb); Node xAsNode = d_avariables.asNode(x); Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart()); - //No guarentee this is in normal form! + // No guarentee this is in normal form! + // Note though, that it happens to be in proof normal form! Node eq = xAsNode.eqNode(asRational); + std::shared_ptr pf; + if (isProofEnabled()) + { + pf = d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eq}); + } d_keepAlive.push_back(eq); d_keepAlive.push_back(reason); Trace("arith-ee") << "Assert equalsConstant2 " << eq << ", reason " << reason << std::endl; - d_ee->assertEquality(eq, true, reason); + + assertLitToEqualityEngine(eq, reason, pf); } bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; } diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 44a2b9df6..8b9086eb0 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -103,9 +103,12 @@ private: /** proof manager */ ProofNodeManager* d_pnm; /** A proof generator for storing proofs of facts that are asserted to the EQ - * engine. Note that these proofs **are not closed**, and assume the - * explanation of these facts. This is why this generator is separate from the - * TheoryArithPrivate generator, which stores closed proofs. + * engine. Note that these proofs **are not closed**; they may contain + * literals from the explanation of their fact as unclosed assumptions. + * This makes these proofs SAT-context depdent. + * + * This is why this generator is separate from the TheoryArithPrivate + * generator, which stores closed proofs. */ std::unique_ptr d_pfGenEe; /** A proof generator for TrustNodes sent to TheoryArithPrivate. @@ -155,9 +158,36 @@ private: bool propagate(TNode x); void explain(TNode literal, std::vector& assumptions); - + /** Assert this literal to the eq engine. Common functionality for + * * assertionToEqualityEngine(..) + * * equalsConstant(c) + * * equalsConstant(lb, ub) + * If proofNew is off, then just asserts. + */ + void assertLitToEqualityEngine(Node lit, + TNode reason, + std::shared_ptr pf); /** This sends a shared term to the uninterpreted equality engine. */ - void assertionToEqualityEngine(bool eq, ArithVar s, TNode reason); + void assertionToEqualityEngine(bool eq, + ArithVar s, + TNode reason, + std::shared_ptr pf); + + /** Check for proof for this or a symmetric fact + * + * The proof submitted to this method are stored in `d_pfGenEe`, and should + * have closure properties consistent with the documentation for that member. + * + * @returns whether this or a symmetric fact has a proof. + */ + bool hasProofFor(TNode f) const; + /** + * Sets the proof for this fact and the symmetric one. + * + * The proof submitted to this method are stored in `d_pfGenEe`, and should + * have closure properties consistent with the documentation for that member. + * */ + void setProofFor(TNode f, std::shared_ptr pf) const; /** Dequeues the delay queue and asserts these equalities.*/ void enableSharedTerms(); diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index f78d8d22f..05845ec76 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -568,8 +568,10 @@ class Constraint { * This is not appropriate for propagation! * Use explainForPropagation() instead. */ - void externalExplainByAssertions(NodeBuilder<>& nb) const{ - externalExplain(nb, AssertionOrderSentinel); + std::shared_ptr externalExplainByAssertions( + NodeBuilder<>& nb) const + { + return externalExplain(nb, AssertionOrderSentinel); } /* Equivalent to calling externalExplainByAssertions on all constraints in b */ -- 2.30.2