From: Alex Ozdemir Date: Fri, 9 Oct 2020 12:55:14 +0000 (-0700) Subject: (proof-new) proofs for arith-constraint explanations (#5224) X-Git-Tag: cvc5-1.0.0~2731 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5fd55819da2ea6fdf0472f2e212330d09c4b5317;p=cvc5.git (proof-new) proofs for arith-constraint explanations (#5224) Threads proofs through arith::Constraint's machinery for explaining constraints. Changes, by function: externalExplainByAssertions: introduce scope to prove the implication externalExplainForPropagation: introduce scope to prove the implication externalExplainConflict: use other machinery to prove conflicting constraints use the CONTRA rule introduce scope to close the conflict proof Future commits will pick up these proofs in theory_arith_private.cpp. Future commits will prove the "split" lemmas produced in constraint.cpp --- diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 9e421efc7..55bbe67cc 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -245,8 +245,7 @@ inline Node getIdentity(Kind k){ case kind::MULT: case kind::NONLINEAR_MULT: return mkRationalNode(1); - default: - Unreachable(); + default: Unreachable(); return {}; // silence warning } } diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index ecccca35b..a08122295 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -477,6 +477,29 @@ bool Constraint::isInternalAssumption() const { return getProofType() == InternalAssumeAP; } +TrustNode Constraint::externalExplainByAssertions() const +{ + NodeBuilder<> nb(kind::AND); + auto pfFromAssumptions = externalExplain(nb, AssertionOrderSentinel); + Node exp = safeConstructNary(nb); + if (d_database->isProofEnabled()) + { + std::vector assumptions; + if (exp.getKind() == Kind::AND) + { + assumptions.insert(assumptions.end(), exp.begin(), exp.end()); + } + else + { + assumptions.push_back(exp); + } + auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions); + return d_database->d_pfGen->mkTrustedPropagation( + getLiteral(), safeConstructNary(Kind::AND, assumptions), pf); + } + return TrustNode::mkTrustPropExp(getLiteral(), exp); +} + bool Constraint::isAssumption() const { return getProofType() == AssumeAP; } @@ -1453,14 +1476,92 @@ Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){ return externalExplain(b, AssertionOrderSentinel); } -Node Constraint::externalExplainConflict() const{ +TrustNode Constraint::externalExplainForPropagation() const +{ + Assert(hasProof()); + Assert(!isAssumption()); + Assert(!isInternalAssumption()); + NodeBuilder<> nb(Kind::AND); + auto pfFromAssumptions = externalExplain(nb, d_assertionOrder); + Node n = safeConstructNary(nb); + if (d_database->isProofEnabled()) + { + std::vector assumptions; + if (n.getKind() == Kind::AND) + { + assumptions.insert(assumptions.end(), n.begin(), n.end()); + } + else + { + assumptions.push_back(n); + } + if (getProofLiteral() != getLiteral()) + { + pfFromAssumptions = d_database->d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {pfFromAssumptions}, {getLiteral()}); + } + auto pf = d_database->d_pnm->mkScope(pfFromAssumptions, assumptions); + return d_database->d_pfGen->mkTrustedPropagation( + getLiteral(), safeConstructNary(Kind::AND, assumptions), pf); + } + else + { + return TrustNode::mkTrustPropExp(getLiteral(), n); + } +} + +TrustNode Constraint::externalExplainConflict() const +{ Debug("pf::arith::explain") << this << std::endl; Assert(inConflict()); NodeBuilder<> nb(kind::AND); - externalExplainByAssertions(nb); - getNegation()->externalExplainByAssertions(nb); - - return safeConstructNary(nb); + auto pf1 = externalExplainByAssertions(nb); + auto not2 = getNegation()->getProofLiteral().negate(); + auto pf2 = getNegation()->externalExplainByAssertions(nb); + Node n = safeConstructNary(nb); + if (d_database->isProofEnabled()) + { + auto pfNot2 = d_database->d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, {pf1}, {not2}); + std::vector lits; + if (n.getKind() == Kind::AND) + { + lits.insert(lits.end(), n.begin(), n.end()); + } + else + { + lits.push_back(n); + } + if (Debug.isOn("arith::pf::externalExplainConflict")) + { + Debug("arith::pf::externalExplainConflict") << "Lits:" << std::endl; + for (const auto& l : lits) + { + Debug("arith::pf::externalExplainConflict") << " : " << l << std::endl; + } + } + std::vector contraLits = {getProofLiteral(), + getNegation()->getProofLiteral()}; + auto bot = + not2.getKind() == Kind::NOT + ? d_database->d_pnm->mkNode(PfRule::CONTRA, {pf2, pfNot2}, {}) + : d_database->d_pnm->mkNode(PfRule::CONTRA, {pfNot2, pf2}, {}); + if (Debug.isOn("arith::pf::tree")) + { + Debug("arith::pf::tree") << *this << std::endl; + Debug("arith::pf::tree") << *getNegation() << std::endl; + Debug("arith::pf::tree") << "\n\nTree:\n"; + printProofTree(Debug("arith::pf::tree")); + getNegation()->printProofTree(Debug("arith::pf::tree")); + } + auto confPf = d_database->d_pnm->mkScope(bot, lits); + return d_database->d_pfGen->mkTrustNode( + safeConstructNary(Kind::AND, lits), confPf, true); + } + else + { + return TrustNode::mkTrustConflict(n); + } } struct ConstraintCPHash { @@ -1519,13 +1620,6 @@ Node Constraint::externalExplain(const ConstraintCPVec& v, AssertionOrder order) return safeConstructNary(nb); } -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 { @@ -1843,13 +1937,19 @@ ConstraintP ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t } } } - TrustNode ConstraintDatabase::eeExplain(const Constraint* const c) const { Assert(c->hasLiteral()); return d_congruenceManager.explain(c->getLiteral()); } +void ConstraintDatabase::eeExplain(ConstraintCP c, NodeBuilder<>& nb) const +{ + Assert(c->hasLiteral()); + // NOTE: this is not a recommended method since it ignores proofs + d_congruenceManager.explain(c->getLiteral(), nb); +} + bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const { return v < d_varDatabases.size(); } diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index 05845ec76..02bc3c988 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -553,9 +553,7 @@ class Constraint { * This is the minimum fringe of the implication tree s.t. * every constraint is assertedToTheTheory() or hasEqualityEngineProof(). */ - Node externalExplainByAssertions() const { - return externalExplain(AssertionOrderSentinel); - } + TrustNode externalExplainByAssertions() const; /** * Writes an explanation of a constraint into the node builder. @@ -598,22 +596,19 @@ class Constraint { * The constraint must have a proof. * The constraint cannot be an assumption. * - * This is the minimum fringe of the implication tree (excluding the constraint itself) - * s.t. every constraint is assertedToTheTheory() or hasEqualityEngineProof(). + * This is the minimum fringe of the implication tree (excluding the + * constraint itself) s.t. every constraint is assertedToTheTheory() or + * hasEqualityEngineProof(). + * + * All return conjuncts were asserted before this constraint. */ - Node externalExplainForPropagation() const { - Assert(hasProof()); - Assert(!isAssumption()); - Assert(!isInternalAssumption()); - return externalExplain(d_assertionOrder); - } + TrustNode externalExplainForPropagation() const; /** * Explain the constraint and its negation in terms of assertions. * The constraint must be in conflict. */ - Node externalExplainConflict() const; - + TrustNode externalExplainConflict() const; /** The constraint is known to be true. */ inline bool hasProof() const { @@ -1155,7 +1150,11 @@ private: bool variableDatabaseIsSetup(ArithVar v) const; void removeVariable(ArithVar v); + /** Get an explanation and proof for this constraint from the equality engine + */ TrustNode eeExplain(ConstraintCP c) const; + /** Get an explanation for this constraint from the equality engine */ + void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const; /** * Returns a constraint with the variable v, the constraint type t, and a value diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 6652d3ee9..760d98b1b 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1632,9 +1632,9 @@ Node TheoryArithPrivate::callDioSolver(){ Node orig = Node::null(); if(lb->isEquality()){ - orig = lb->externalExplainByAssertions(); + orig = lb->externalExplainByAssertions().getNode(); }else if(ub->isEquality()){ - orig = ub->externalExplainByAssertions(); + orig = ub->externalExplainByAssertions().getNode(); }else { orig = Constraint::externalExplainByAssertions(ub, lb); } @@ -1888,7 +1888,7 @@ void TheoryArithPrivate::outputConflicts(){ pf.print(std::cout); std::cout << std::endl; } - Node conflict = confConstraint->externalExplainConflict(); + Node conflict = confConstraint->externalExplainConflict().getNode(); ++conflicts; Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict @@ -3797,13 +3797,13 @@ Node TheoryArithPrivate::explain(TNode n) ConstraintP c = d_constraintDatabase.lookup(n); if(c != NullConstraint){ Assert(!c->isAssumption()); - Node exp = c->externalExplainForPropagation(); + Node exp = c->externalExplainForPropagation().getNode(); Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl; return exp; }else if(d_assertionsThatDoNotMatchTheirLiterals.find(n) != d_assertionsThatDoNotMatchTheirLiterals.end()){ c = d_assertionsThatDoNotMatchTheirLiterals[n]; if(!c->isAssumption()){ - Node exp = c->externalExplainForPropagation(); + Node exp = c->externalExplainForPropagation().getNode(); Debug("arith::explain") << "assertions explanation" << n << ":" << exp << endl; return exp; }else{ @@ -5006,7 +5006,7 @@ void TheoryArithPrivate::entailmentCheckBoundLookup(std::pairexternalExplainByAssertions(); + tmp.first = c->externalExplainByAssertions().getNode(); tmp.second = c->getValue(); } }