From d3fcaabbafdfebe17aa20f656ff2d3922d0dcb96 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 2 Oct 2020 06:03:23 -0700 Subject: [PATCH] (proof-new) New proofs in arith::Constraint::externalExplain (#5176) This commit threads proofs through the core of arith: Constraint::externalExplain, which recursively explain arith literals. One of the base cases here is asking the EE for an explanation, through the congruence manager. To delay implementing proofs in ArithCongruenceManager to a separate commit, we stub out proof production in ArithCongruenceManager::explain for now. --- src/theory/arith/congruence_manager.cpp | 30 ++- src/theory/arith/congruence_manager.h | 4 +- src/theory/arith/constraint.cpp | 292 ++++++++++++++++++---- src/theory/arith/constraint.h | 20 +- src/theory/arith/theory_arith_private.cpp | 6 +- 5 files changed, 288 insertions(+), 64 deletions(-) diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 520903562..465128b1b 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -375,11 +375,20 @@ Node ArithCongruenceManager::explainInternal(TNode internal){ } } -Node ArithCongruenceManager::explain(TNode external){ +TrustNode ArithCongruenceManager::explain(TNode external) +{ Trace("arith-ee") << "Ask for explanation of " << external << std::endl; Node internal = externalToInternal(external); Trace("arith-ee") << "...internal = " << internal << std::endl; - return explainInternal(internal); + Node exp = explainInternal(internal); + if (isProofEnabled()) + { + Node impl = NodeManager::currentNM()->mkNode(Kind::IMPLIES, exp, external); + // For now, we just trust + auto pfOfImpl = d_pnm->mkNode(PfRule::INT_TRUST, {}, {impl}); + return d_pfGenExplain->mkTrustNode(impl, pfOfImpl); + } + return TrustNode::mkTrustPropExp(external, exp, nullptr); } void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){ @@ -474,6 +483,23 @@ void ArithCongruenceManager::addSharedTerm(Node x){ bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; } +std::vector andComponents(TNode an) +{ + auto nm = NodeManager::currentNM(); + if (an == nm->mkConst(true)) + { + return {}; + } + else if (an.getKind() != Kind::AND) + { + return {an}; + } + std::vector a{}; + a.reserve(an.getNumChildren()); + a.insert(a.end(), an.begin(), an.end()); + return a; +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 3565d86b5..67df9237c 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -196,7 +196,7 @@ public: void finishInit(eq::EqualityEngine* ee, eq::ProofEqEngine* pfee); //--------------------------------- end initialization - Node explain(TNode literal); + TrustNode explain(TNode literal); void explain(TNode lit, NodeBuilder<>& out); void addWatchedPair(ArithVar s, TNode x, TNode y); @@ -244,6 +244,8 @@ public: };/* class ArithCongruenceManager */ +std::vector andComponents(TNode an); + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 06ecb9618..ecccca35b 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -554,14 +554,11 @@ void Constraint::printProofTree(std::ostream& out, size_t depth) const { const ConstraintRule& rule = getConstraintRule(); out << std::string(2 * depth, ' ') << "* " << getVariable() << " ["; - if (hasLiteral()) + out << getProofLiteral(); + if (assertedToTheTheory()) { - out << getLiteral(); + out << " | wit: " << getWitness(); } - else - { - out << "NOLIT"; - }; out << "]" << ' ' << getType() << ' ' << getValue() << " (" << getProofType() << ")"; if (getProofType() == FarkasAP) @@ -1522,68 +1519,208 @@ Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order) return safeConstructNary(nb); } -void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{ - Assert(hasProof()); - Assert(!isAssumption() || assertedToTheTheory()); - Assert(!isInternalAssumption()); +Node Constraint::externalExplain(AssertionOrder order) const +{ + NodeBuilder<> nb(kind::AND); + externalExplain(nb, order); + return safeConstructNary(nb); +} +std::shared_ptr Constraint::externalExplain( + NodeBuilder<>& nb, AssertionOrder order) const +{ if (Debug.isOn("pf::arith::explain")) { + this->printProofTree(Debug("arith::pf::tree")); Debug("pf::arith::explain") << "Explaining: " << this << " with rule "; getConstraintRule().print(Debug("pf::arith::explain")); Debug("pf::arith::explain") << std::endl; } + Assert(hasProof()); + Assert(!isAssumption() || assertedToTheTheory()); + Assert(!isInternalAssumption()); + std::shared_ptr pf{}; - if(assertedBefore(order)){ + ProofNodeManager* pnm = d_database->d_pnm; + + if (assertedBefore(order)) + { + Debug("pf::arith::explain") << " already asserted" << std::endl; nb << getWitness(); - }else if(hasEqualityEngineProof()){ - d_database->eeExplain(this, nb); - }else{ + if (d_database->isProofEnabled()) + { + pf = pnm->mkAssume(getWitness()); + // If the witness and literal differ, prove the difference through a + // rewrite. + if (getWitness() != getProofLiteral()) + { + pf = pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {pf}, {getProofLiteral()}); + } + } + } + else if (hasEqualityEngineProof()) + { + Debug("pf::arith::explain") << " going to ee:" << std::endl; + TrustNode exp = d_database->eeExplain(this); + if (d_database->isProofEnabled()) + { + Assert(exp.getProven().getKind() == Kind::IMPLIES); + std::vector> hypotheses; + hypotheses.push_back(exp.getGenerator()->getProofFor(exp.getProven())); + if (exp.getNode().getKind() == Kind::AND) + { + for (const auto& h : exp.getNode()) + { + hypotheses.push_back( + pnm->mkNode(PfRule::TRUE_INTRO, {pnm->mkAssume(h)}, {})); + } + } + else + { + hypotheses.push_back(pnm->mkNode( + PfRule::TRUE_INTRO, {pnm->mkAssume(exp.getNode())}, {})); + } + pf = pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {hypotheses}, {getProofLiteral()}); + } + Debug("pf::arith::explain") + << " explanation: " << exp.getNode() << std::endl; + if (exp.getNode().getKind() == Kind::AND) + { + nb.append(exp.getNode().begin(), exp.getNode().end()); + } + else + { + nb << exp.getNode(); + } + } + else + { + Debug("pf::arith::explain") << " recursion!" << std::endl; Assert(!isAssumption()); AntecedentId p = getEndAntecedent(); ConstraintCP antecedent = d_database->d_antecedents[p]; + std::vector> children; - while(antecedent != NullConstraint){ + while (antecedent != NullConstraint) + { Debug("pf::arith::explain") << "Explain " << antecedent << std::endl; - antecedent->externalExplain(nb, order); + auto pn = antecedent->externalExplain(nb, order); + if (d_database->isProofEnabled()) + { + children.push_back(pn); + } --p; antecedent = d_database->d_antecedents[p]; } - } -} -Node Constraint::externalExplain(AssertionOrder order) const{ - Assert(hasProof()); - Assert(!isAssumption() || assertedBefore(order)); - Assert(!isInternalAssumption()); - if(assertedBefore(order)){ - return getWitness(); - }else if(hasEqualityEngineProof()){ - return d_database->eeExplain(this); - }else{ - Assert(hasFarkasProof() || hasIntHoleProof() || hasIntTightenProof() || hasTrichotomyProof()); - Assert(!antecentListIsEmpty()); - //Force the selection of the layer above if the node is - // assertedToTheTheory()! - - AntecedentId listEnd = getEndAntecedent(); - if(antecedentListLengthIsOne()){ - ConstraintCP antecedent = d_database->d_antecedents[listEnd]; - return antecedent->externalExplain(order); - }else{ - NodeBuilder<> nb(kind::AND); - Assert(!isAssumption()); - - AntecedentId p = listEnd; - ConstraintCP antecedent = d_database->d_antecedents[p]; - while(antecedent != NullConstraint){ - antecedent->externalExplain(nb, order); - --p; - antecedent = d_database->d_antecedents[p]; + if (d_database->isProofEnabled()) + { + switch (getProofType()) + { + case ArithProofType::AssumeAP: + case ArithProofType::EqualityEngineAP: + { + Unreachable() << "These should be handled above"; + break; + } + case ArithProofType::FarkasAP: + { + // Per docs in constraint.h, + // the 0th farkas coefficient is for the negation of the deduced + // constraint the 1st corresponds to the last antecedent the nth + // corresponds to the first antecedent Then, the farkas coefficients + // and the antecedents are in the same order. + + // Enumerate child proofs (negation included) in d_farkasCoefficients + // order + std::vector> farkasChildren; + farkasChildren.push_back( + pnm->mkAssume(getNegation()->getProofLiteral())); + farkasChildren.insert( + farkasChildren.end(), children.rbegin(), children.rend()); + + NodeManager* nm = NodeManager::currentNM(); + + // Enumerate d_farkasCoefficients as nodes. + std::vector farkasCoeffs; + for (Rational r : *getFarkasCoefficients()) + { + farkasCoeffs.push_back(nm->mkConst(r)); + } + + // Apply the scaled-sum rule. + std::shared_ptr sumPf = + pnm->mkNode(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, + farkasChildren, + farkasCoeffs); + + // Provable rewrite the result + auto botPf = pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {sumPf}, {nm->mkConst(false)}); + + // Scope out the negated constraint, yielding a proof of the + // constraint. + std::vector assump{getNegation()->getProofLiteral()}; + auto maybeDoubleNotPf = pnm->mkScope(botPf, assump, false); + + // No need to ensure that the expected node aggrees with `assump` + // because we are not providing an expected node. + // + // Prove that this is the literal (may need to clean a double-not) + pf = pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, + {maybeDoubleNotPf}, + {getProofLiteral()}); + + break; + } + case ArithProofType::IntTightenAP: + { + if (isUpperBound()) + { + pf = pnm->mkNode( + PfRule::INT_TIGHT_UB, children, {}, getProofLiteral()); + } + else if (isLowerBound()) + { + pf = pnm->mkNode( + PfRule::INT_TIGHT_LB, children, {}, getProofLiteral()); + } + else + { + Unreachable(); + } + break; + } + case ArithProofType::IntHoleAP: + { + pf = pnm->mkNode(PfRule::INT_TRUST, + children, + {getProofLiteral()}, + getProofLiteral()); + break; + } + case ArithProofType::TrichotomyAP: + { + pf = pnm->mkNode(PfRule::ARITH_TRICHOTOMY, + children, + {getProofLiteral()}, + getProofLiteral()); + break; + } + case ArithProofType::InternalAssumeAP: + case ArithProofType::NoAP: + default: + { + Unreachable() << getProofType() + << " should not be visible in explanation"; + break; + } } - return nb; } } + return pf; } Node Constraint::externalExplainByAssertions(ConstraintCP a, ConstraintCP b){ @@ -1706,14 +1843,11 @@ ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t } } } -Node ConstraintDatabase::eeExplain(const Constraint* const c) const{ - Assert(c->hasLiteral()); - return d_congruenceManager.explain(c->getLiteral()); -} -void ConstraintDatabase::eeExplain(const Constraint* const c, NodeBuilder<>& nb) const{ +TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const +{ Assert(c->hasLiteral()); - d_congruenceManager.explain(c->getLiteral(), nb); + return d_congruenceManager.explain(c->getLiteral()); } bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const { @@ -1740,6 +1874,58 @@ void Constraint::setLiteral(Node n) { map.insert(make_pair(d_literal, this)); } +Node Constraint::getProofLiteral() const +{ + Assert(d_database != nullptr); + Assert(d_database->d_avariables.hasNode(d_variable)); + Node varPart = d_database->d_avariables.asNode(d_variable); + Kind cmp; + bool neg = false; + switch (d_type) + { + case ConstraintType::UpperBound: + { + if (d_value.infinitesimalIsZero()) + { + cmp = Kind::LEQ; + } + else + { + cmp = Kind::LT; + } + break; + } + case ConstraintType::LowerBound: + { + if (d_value.infinitesimalIsZero()) + { + cmp = Kind::GEQ; + } + else + { + cmp = Kind::GT; + } + break; + } + case ConstraintType::Equality: + { + cmp = Kind::EQUAL; + break; + } + case ConstraintType::Disequality: + { + cmp = Kind::EQUAL; + neg = true; + break; + } + default: Unreachable() << d_type; + } + NodeManager* nm = NodeManager::currentNM(); + Node constPart = nm->mkConst(d_value.getNoninfinitesimalPart()); + Node posLit = nm->mkNode(cmp, varPart, constPart); + return neg ? posLit.negate() : posLit; +} + void implies(std::vector& out, ConstraintP a, ConstraintP b){ Node la = a->getLiteral(); Node lb = b->getLiteral(); diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 0afc0bc2f..f78d8d22f 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -92,6 +92,7 @@ #include "theory/arith/constraint_forward.h" #include "theory/arith/delta_rational.h" #include "theory/arith/proof_macros.h" +#include "theory/trust_node.h" namespace CVC4 { namespace theory { @@ -463,6 +464,14 @@ class Constraint { return d_literal; } + /** Gets a literal in the normal form suitable for proofs. + * That is, (sum of non-const monomials) >< const. + * + * This is a sister method to `getLiteral`, which returns a normal form + * literal, suitable for external solving use. + */ + Node getProofLiteral() const; + /** * Set the node as having a proof and being an assumption. * The node must be assertedToTheTheory(). @@ -848,7 +857,6 @@ class Constraint { static std::pair unateFarkasSigns(ConstraintCP a, ConstraintCP b); Node externalExplain(AssertionOrder order) const; - /** * Returns an explanation of that was assertedBefore(order). * The constraint must have a proof. @@ -857,7 +865,8 @@ class Constraint { * This is the minimum fringe of the implication tree * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof(). */ - void externalExplain(NodeBuilder<>& nb, AssertionOrder order) const; + std::shared_ptr externalExplain(NodeBuilder<>& nb, + AssertionOrder order) const; static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order); @@ -1144,8 +1153,7 @@ private: bool variableDatabaseIsSetup(ArithVar v) const; void removeVariable(ArithVar v); - Node eeExplain(ConstraintCP c) const; - void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const; + TrustNode eeExplain(ConstraintCP c) const; /** * Returns a constraint with the variable v, the constraint type t, and a value @@ -1208,7 +1216,9 @@ private: /** AntecendentID must be in range. */ ConstraintCP getAntecedent(AntecedentId p) const; -private: + bool isProofEnabled() const { return d_pnm != nullptr; } + + private: /** returns true if cons is now in conflict. */ bool handleUnateProp(ConstraintP ant, ConstraintP cons); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index d2293131f..1a13f44fa 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -3865,12 +3865,12 @@ Node TheoryArithPrivate::explain(TNode n) Debug("arith::explain") << "this is a strange mismatch" << n << endl; Assert(d_congruenceManager.canExplain(n)); Debug("arith::explain") << "this is a strange mismatch" << n << endl; - return d_congruenceManager.explain(n); + return d_congruenceManager.explain(n).getNode(); } }else{ Assert(d_congruenceManager.canExplain(n)); Debug("arith::explain") << "dm explanation" << n << endl; - return d_congruenceManager.explain(n); + return d_congruenceManager.explain(n).getNode(); } } @@ -3930,7 +3930,7 @@ void TheoryArithPrivate::propagate(Theory::Effort e) { outputPropagate(toProp); }else if(constraint->negationHasProof()){ - Node exp = d_congruenceManager.explain(toProp); + Node exp = d_congruenceManager.explain(toProp).getNode(); Node notNormalized = normalized.getKind() == NOT ? normalized[0] : normalized.notNode(); Node lp = flattenAnd(exp.andNode(notNormalized)); -- 2.30.2