From 5fd55819da2ea6fdf0472f2e212330d09c4b5317 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 9 Oct 2020 05:55:14 -0700 Subject: (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 --- src/theory/arith/constraint.cpp | 126 +++++++++++++++++++++++++++++++++++----- 1 file changed, 113 insertions(+), 13 deletions(-) (limited to 'src/theory/arith/constraint.cpp') 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(); } -- cgit v1.2.3