From: Alex Ozdemir Date: Tue, 19 Jan 2021 22:25:02 +0000 (-0800) Subject: Implement proofs for arith BRAB lemmas (#5784) X-Git-Tag: cvc5-1.0.0~2376 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3c754308f66d92cd4b03d5f159464585c315b528;p=cvc5.git Implement proofs for arith BRAB lemmas (#5784) All changes: Add a Pf type alias for std::shared_ptr to expr/proof_rule.h Add an eager proof generator to TheoryArith for preprocessing rewrites. Right now those are proven with INT_TRUST. Will eventually fix. Generate proved lemmas in TheoryArithPrivate::branchIntegerVariable. Same for TheoryArithPrivate::roundRobinBranch Add EagerProofGenerator::mkTrustedRewrite. Add some proofsEnabled methods. --- diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index 0c36deada..a505b1bc0 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -27,6 +27,9 @@ namespace CVC4 { class ProofNodeManager; class ProofNode; +// Alias for shared pointer to a proof node +using Pf = std::shared_ptr; + struct ProofNodeHashFunction { inline size_t operator()(std::shared_ptr pfn) const; diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 7437ce223..6de5c7221 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -17,6 +17,7 @@ #include "theory/arith/theory_arith.h" +#include "expr/proof_rule.h" #include "options/smt_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_rewriter.h" @@ -42,6 +43,7 @@ TheoryArith::TheoryArith(context::Context* c, d_internal( new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)), d_ppRewriteTimer("theory::arith::ppRewriteTimer"), + d_ppPfGen(pnm, c, "Arith::ppRewrite"), d_astate(*d_internal, c, u, valuation), d_inferenceManager(*this, d_astate, pnm), d_nonlinearExtension(nullptr), @@ -131,7 +133,17 @@ TrustNode TheoryArith::ppRewrite(TNode atom) Debug("arith::preprocess") << "arith::preprocess() : returning " << rewritten << endl; // don't need to rewrite terms since rewritten is not a non-standard op - return TrustNode::mkTrustRewrite(atom, rewritten, nullptr); + if (proofsEnabled()) + { + return d_ppPfGen.mkTrustedRewrite( + atom, + rewritten, + d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)})); + } + else + { + return TrustNode::mkTrustRewrite(atom, rewritten, nullptr); + } } } return ppRewriteTerms(atom); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index e26ff51ef..eba84e339 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -45,6 +45,9 @@ class TheoryArith : public Theory { TimerStat d_ppRewriteTimer; + /** Used to prove pp-rewrites */ + EagerProofGenerator d_ppPfGen; + public: TheoryArith(context::Context* c, context::UserContext* u, @@ -152,6 +155,7 @@ class TheoryArith : public Theory { ArithPreprocess d_arithPreproc; /** The theory rewriter for this theory. */ ArithRewriter d_rewriter; + };/* class TheoryArith */ }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 7b0096f30..58e874158 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -34,6 +34,7 @@ #include "expr/node_builder.h" #include "expr/proof_generator.h" #include "expr/proof_node_manager.h" +#include "expr/proof_rule.h" #include "expr/skolem_manager.h" #include "options/arith_options.h" #include "options/smt_options.h" // for incrementalSolving() @@ -3033,11 +3034,11 @@ bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel){ ArithVar canBranch = nextIntegerViolatation(false); if(canBranch != ARITHVAR_SENTINEL){ ++d_statistics.d_panicBranches; - Node branch = branchIntegerVariable(canBranch); - Assert(branch.getKind() == kind::OR); - Node rwbranch = Rewriter::rewrite(branch[0]); + TrustNode branch = branchIntegerVariable(canBranch); + Assert(branch.getNode().getKind() == kind::OR); + Node rwbranch = Rewriter::rewrite(branch.getNode()[0]); if(!isSatLiteral(rwbranch)){ - d_approxCuts.push_back(branch); + d_approxCuts.push_back(branch.getNode()); return true; } } @@ -3619,15 +3620,15 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) } if(!emmittedConflictOrSplit) { - Node possibleLemma = roundRobinBranch(); - if(!possibleLemma.isNull()){ + TrustNode possibleLemma = roundRobinBranch(); + if (!possibleLemma.getNode().isNull()) + { ++(d_statistics.d_externalBranchAndBounds); d_cutCount = d_cutCount + 1; emmittedConflictOrSplit = true; Debug("arith::lemma") << "rrbranch lemma" << possibleLemma << endl; - outputLemma(possibleLemma); - + outputTrustedLemma(possibleLemma); } } @@ -3662,7 +3663,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel) bool TheoryArithPrivate::foundNonlinear() const { return d_foundNl; } -Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const { +TrustNode TheoryArithPrivate::branchIntegerVariable(ArithVar x) const +{ const DeltaRational& d = d_partialModel.getAssignment(x); Assert(!d.isIntegral()); const Rational& r = d.getNoninfinitesimalPart(); @@ -3674,7 +3676,7 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const { TNode var = d_partialModel.asNode(x); Integer floor_d = d.floor(); - Node lem; + TrustNode lem = TrustNode::null(); NodeManager* nm = NodeManager::currentNM(); if (options::brabTest()) { @@ -3691,38 +3693,102 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const { nm->mkNode(kind::LEQ, var, mkRationalNode(nearest - 1))); Node lb = Rewriter::rewrite( nm->mkNode(kind::GEQ, var, mkRationalNode(nearest + 1))); - lem = nm->mkNode(kind::OR, ub, lb); - Node eq = Rewriter::rewrite( - nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest))); + Node right = nm->mkNode(kind::OR, ub, lb); + Node rawEq = nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest)); + Node eq = Rewriter::rewrite(rawEq); // Also preprocess it before we send it out. This is important since // arithmetic may prefer eliminating equalities. + TrustNode teq; if (Theory::theoryOf(eq) == THEORY_ARITH) { - TrustNode teq = d_containing.ppRewrite(eq); + teq = d_containing.ppRewrite(eq); eq = teq.isNull() ? eq : teq.getNode(); } Node literal = d_containing.getValuation().ensureLiteral(eq); + Trace("integers") << "eq: " << eq << "\nto: " << literal << endl; d_containing.getOutputChannel().requirePhase(literal, true); - lem = nm->mkNode(kind::OR, literal, lem); + Node l = nm->mkNode(kind::OR, literal, right); + Trace("integers") << "l: " << l << endl; + if (proofsEnabled()) + { + Node less = nm->mkNode(kind::LT, var, mkRationalNode(nearest)); + Node greater = nm->mkNode(kind::GT, var, mkRationalNode(nearest)); + // TODO (project #37): justify. Thread proofs through *ensureLiteral*. + Debug("integers::pf") << "less: " << less << endl; + Debug("integers::pf") << "greater: " << greater << endl; + Debug("integers::pf") << "literal: " << literal << endl; + Debug("integers::pf") << "eq: " << eq << endl; + Debug("integers::pf") << "rawEq: " << rawEq << endl; + Pf pfNotLit = d_pnm->mkAssume(literal.negate()); + // rewrite notLiteral to notRawEq, using teq. + Pf pfNotRawEq = + literal == rawEq + ? pfNotLit + : d_pnm->mkNode( + PfRule::MACRO_SR_PRED_TRANSFORM, + {pfNotLit, teq.getGenerator()->getProofFor(teq.getProven())}, + {rawEq.negate()}); + Pf pfBot = + d_pnm->mkNode(PfRule::CONTRA, + {d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY, + {d_pnm->mkAssume(less.negate()), pfNotRawEq}, + {greater}), + d_pnm->mkAssume(greater.negate())}, + {}); + std::vector assumptions = { + literal.negate(), less.negate(), greater.negate()}; + // Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i)))) + Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions); + Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM, + {d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})}, + {l}); + lem = d_pfGen->mkTrustNode(l, pfL); + } + else + { + lem = TrustNode::mkTrustLemma(l, nullptr); + } } else { Node ub = Rewriter::rewrite(nm->mkNode(kind::LEQ, var, mkRationalNode(floor_d))); Node lb = ub.notNode(); - lem = nm->mkNode(kind::OR, ub, lb); + if (proofsEnabled()) + { + lem = d_pfGen->mkTrustNode( + nm->mkNode(kind::OR, ub, lb), PfRule::SPLIT, {}, {ub}); + } + else + { + lem = TrustNode::mkTrustLemma(nm->mkNode(kind::OR, ub, lb), nullptr); + } } Trace("integers") << "integers: branch & bound: " << lem << endl; - if(isSatLiteral(lem[0])) { - Debug("integers") << " " << lem[0] << " == " << getSatValue(lem[0]) << endl; - } else { - Debug("integers") << " " << lem[0] << " is not assigned a SAT literal" << endl; - } - if(isSatLiteral(lem[1])) { - Debug("integers") << " " << lem[1] << " == " << getSatValue(lem[1]) << endl; - } else { - Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl; + if (Debug.isOn("integers")) + { + Node l = lem.getNode(); + if (isSatLiteral(l[0])) + { + Debug("integers") << " " << l[0] << " == " << getSatValue(l[0]) + << endl; + } + else + { + Debug("integers") << " " << l[0] << " is not assigned a SAT literal" + << endl; + } + if (isSatLiteral(l[1])) + { + Debug("integers") << " " << l[1] << " == " << getSatValue(l[1]) + << endl; + } + else + { + Debug("integers") << " " << l[1] << " is not assigned a SAT literal" + << endl; + } } return lem; } @@ -3748,9 +3814,10 @@ std::vector TheoryArithPrivate::cutAllBounded() const{ } /** Returns true if the roundRobinBranching() issues a lemma. */ -Node TheoryArithPrivate::roundRobinBranch(){ +TrustNode TheoryArithPrivate::roundRobinBranch() +{ if(hasIntegerModel()){ - return Node::null(); + return TrustNode::null(); }else{ ArithVar v = d_nextIntegerCheckVar; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 31435221f..e7f5d82b2 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -552,9 +552,11 @@ private: * Returns a cut for a lemma. * If there is an integer model, this returns Node::null(). */ - Node roundRobinBranch(); + TrustNode roundRobinBranch(); -public: + bool proofsEnabled() const { return d_pnm; } + + public: /** * This requests a new unique ArithVar value for x. * This also does initial (not context dependent) set up for a variable, @@ -709,7 +711,7 @@ private: /** Counts the number of fullCheck calls to arithmetic. */ uint32_t d_fullCheckCounter; std::vector cutAllBounded() const; - Node branchIntegerVariable(ArithVar x) const; + TrustNode branchIntegerVariable(ArithVar x) const; void branchVector(const std::vector& lemmas); context::CDO d_cutCount; diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp index c49c33790..a1c78fc7d 100644 --- a/src/theory/eager_proof_generator.cpp +++ b/src/theory/eager_proof_generator.cpp @@ -120,6 +120,18 @@ TrustNode EagerProofGenerator::mkTrustNode(Node conc, return mkTrustNode(pfs->getResult(), pfs, isConflict); } +TrustNode EagerProofGenerator::mkTrustedRewrite( + Node a, Node b, std::shared_ptr pf) +{ + if (pf == nullptr) + { + return TrustNode::null(); + } + Node eq = a.eqNode(b); + setProofFor(eq, pf); + return TrustNode::mkTrustRewrite(a, b, this); +} + TrustNode EagerProofGenerator::mkTrustedPropagation( Node n, Node exp, std::shared_ptr pf) { diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h index 29f916e00..4b94228c5 100644 --- a/src/theory/eager_proof_generator.h +++ b/src/theory/eager_proof_generator.h @@ -146,6 +146,17 @@ class EagerProofGenerator : public ProofGenerator TrustNode mkTrustedPropagation(Node n, Node exp, std::shared_ptr pf); + /** + * Make trust node: `a = b` as a Rewrite trust node + * + * @param a the original + * @param b what is rewrites to + * @param pf The proof of a = b, + * @return The trust node corresponding to the fact that this generator has + * a proof of a = b + */ + TrustNode mkTrustedRewrite( + Node a, Node b, std::shared_ptr pf); //--------------------------------------- common proofs /** * This returns the trust node corresponding to the splitting lemma diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 9ab20e6cb..5bea454e8 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -424,6 +424,11 @@ void Theory::getCareGraph(CareGraph* careGraph) { d_careGraph = NULL; } +bool Theory::proofsEnabled() const +{ + return d_pnm != nullptr; +} + EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) { // if not using an equality engine, then by default we don't know the status diff --git a/src/theory/theory.h b/src/theory/theory.h index a9783c19c..0eb3d9a33 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -237,6 +237,13 @@ class Theory { /** Pointer to proof node manager */ ProofNodeManager* d_pnm; + /** + * Are proofs enabled? + * + * They are considered enabled if the ProofNodeManager is non-null. + */ + bool proofsEnabled() const; + /** * Returns the next assertion in the assertFact() queue. *