diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-04-09 17:30:44 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-09 15:30:44 -0500 |
commit | 62f5fb8db269e12f13ce5c4e1c3f975776737836 (patch) | |
tree | bdf16437b8c0c5ead202ac7fb08f6483aa3a9c19 /src | |
parent | 6923f0cb9930332a61e187d3b4d1a7ec7e65b15c (diff) |
[proof-new] Optimizing sat proof (#6324)
For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/lazy_proof_chain.cpp | 13 | ||||
-rw-r--r-- | src/expr/proof_rule.h | 12 | ||||
-rw-r--r-- | src/prop/sat_proof_manager.cpp | 18 | ||||
-rw-r--r-- | src/prop/sat_proof_manager.h | 3 | ||||
-rw-r--r-- | src/smt/proof_manager.cpp | 1 | ||||
-rw-r--r-- | src/smt/proof_post_processor.cpp | 3 | ||||
-rw-r--r-- | src/theory/booleans/proof_checker.cpp | 7 |
7 files changed, 39 insertions, 18 deletions
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index 7f14adc38..5e638b55f 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -67,7 +67,7 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact) std::vector<std::shared_ptr<ProofNode>>, NodeHashFunction> assumptionsToExpand; - // invariant of the loop below, the first iteration notwhistanding: + // invariant of the loop below, the first iteration notwithstanding: // visit = domain(assumptionsToExpand) \ domain(toConnect) std::vector<Node> visit{fact}; std::unordered_map<Node, bool, NodeHashFunction> visited; @@ -121,13 +121,22 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact) expr::getFreeAssumptionsMap(curPfn, famap); if (Trace.isOn("lazy-cdproofchain")) { + unsigned alreadyToVisit = 0; Trace("lazy-cdproofchain") - << "LazyCDProofChain::getProofFor: free assumptions:\n"; + << "LazyCDProofChain::getProofFor: " << famap.size() + << " free assumptions:\n"; for (auto fap : famap) { Trace("lazy-cdproofchain") << "LazyCDProofChain::getProofFor: - " << fap.first << "\n"; + alreadyToVisit += + std::find(visit.begin(), visit.end(), fap.first) != visit.end() + ? 1 + : 0; } + Trace("lazy-cdproofchain") + << "LazyCDProofChain::getProofFor: " << alreadyToVisit + << " already to visit\n"; } // mark for post-traversal if we are controlling cycles if (d_cyclic) diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 7e0fc31fe..cec85cc99 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -320,6 +320,8 @@ enum class PfRule : uint32_t // The result of the chain resolution is C, which is equal, in its set // representation, to C_n' MACRO_RESOLUTION, + // As above but not checked + MACRO_RESOLUTION_TRUST, // ======== Split // Children: none @@ -1048,8 +1050,9 @@ enum class PfRule : uint32_t // its ki is negative). >< is always one of <, <= // NB: this implies that lower bounds must have negative ki, // and upper bounds must have positive ki. - // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * poly_n) - // t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n * const_n) + // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * + // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n + // * const_n) ARITH_SCALE_SUM_UPPER_BOUNDS, // ======== Sum Upper Bounds @@ -1134,8 +1137,9 @@ enum class PfRule : uint32_t // Arguments: (t, x, y, a, b, sgn) // --------------------- // Conclusion: - // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y b))) - // sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) (>= y b))) + // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y + // b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) + // (>= y b))) // Where x,y are real terms (variables or extended terms), t = (* x y) // (possibly under rewriting), a,b are real constants, and sgn is either -1 // or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index da9354c2f..0d075de45 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -35,6 +35,7 @@ SatProofManager::SatProofManager(Minisat::Solver* solver, d_assumptions(userContext), d_conflictLit(undefSatVariable) { + d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); } @@ -169,7 +170,6 @@ void SatProofManager::endResChain(Node conclusion, } d_redundantLits.clear(); // build resolution chain - NodeManager* nm = NodeManager::currentNM(); // the conclusion is stored already in the arguments because of the // possibility of reordering std::vector<Node> children, args{conclusion}; @@ -212,7 +212,7 @@ void SatProofManager::endResChain(Node conclusion, Trace("sat-proof") << " : "; if (i > 0) { - args.push_back(nm->mkConst(posFirst)); + args.push_back(posFirst ? d_true : d_false); args.push_back(pivot); Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] "; } @@ -249,7 +249,7 @@ void SatProofManager::endResChain(Node conclusion, // step, which bypasses these. Note that we could generate a chain resolution // rule here by explicitly computing the detailed steps, but leave this for // post-processing. - ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); d_resChainPg.addStep(conclusion, ps); // the premises of this resolution may not have been justified yet, so we do // not pass assumptions to check closedness @@ -369,7 +369,6 @@ void SatProofManager::explainLit( // SAT solver, we directly get the literals we need to explain so we no // longer depend on the reference to reason std::vector<Node> toExplain{children.back().begin(), children.back().end()}; - NodeManager* nm = NodeManager::currentNM(); Trace("sat-proof") << push; for (unsigned i = 0; i < size; ++i) { @@ -397,7 +396,7 @@ void SatProofManager::explainLit( // note this is the opposite of what is done in addResolutionStep. This is // because here the clause, which contains the literal being analyzed, is // the first clause rather than the second - args.push_back(nm->mkConst(!negated)); + args.push_back(!negated ? d_true : d_false); args.push_back(negated ? currLitNode[0] : currLitNode); // add child premises and the child itself premises.insert(childPremises.begin(), childPremises.end()); @@ -429,7 +428,7 @@ void SatProofManager::explainLit( Trace("sat-proof") << pop; // create step args.insert(args.begin(), litNode); - ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); d_resChainPg.addStep(litNode, ps); // the premises in the limit of the justification may correspond to other // links in the chain which have, themselves, literals yet to be justified. So @@ -490,7 +489,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, // get resolution Node cur = link.first; std::shared_ptr<ProofNode> pfn = link.second; - while (pfn->getRule() != PfRule::MACRO_RESOLUTION) + while (pfn->getRule() != PfRule::MACRO_RESOLUTION_TRUST) { Assert(pfn->getChildren().size() == 1 && pfn->getChildren()[0]->getRule() == PfRule::ASSUME) @@ -539,7 +538,6 @@ void SatProofManager::finalizeProof(Node inConflictNode, // arguments for the resolution step to conclude false. std::vector<Node> children{inConflictNode}, args; std::unordered_set<TNode, TNodeHashFunction> premises; - NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = inConflict.size(); i < size; ++i) { Assert(d_cnfStream->getNodeCache().find(inConflict[i]) @@ -555,7 +553,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, // note this is the opposite of what is done in addResolutionStep. This is // because here the clause, which contains the literal being analyzed, is // the first clause rather than the second - args.push_back(nm->mkConst(!negated)); + args.push_back(!negated ? d_true : d_false); args.push_back(negated ? litNode[0] : litNode); // add child premises and the child itself premises.insert(childPremises.begin(), childPremises.end()); @@ -578,7 +576,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, } // create step args.insert(args.begin(), d_false); - ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args); d_resChainPg.addStep(d_false, ps); // not yet ready to check closedness because maybe only now we will justify // literals used in resolutions diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 4d45ce3b7..6407939c7 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -561,7 +561,8 @@ class SatProofManager /** The proof generator for resolution chains */ BufferedProofGenerator d_resChainPg; - /** The false node */ + /** The true/false nodes */ + Node d_true; Node d_false; /** All clauses added to the SAT solver, kept in a context-dependent manner. diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 846df7e41..549f10008 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -64,6 +64,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO); d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_ELIM); d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM); + d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION_TRUST); d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION); if (options::proofGranularityMode() != options::ProofGranularityMode::REWRITE) diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a27a5697e..19ca089d3 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -648,7 +648,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {}); return args[0]; } - else if (id == PfRule::MACRO_RESOLUTION) + else if (id == PfRule::MACRO_RESOLUTION + || id == PfRule::MACRO_RESOLUTION_TRUST) { // first generate the naive chain_resolution std::vector<Node> chainResArgs{args.begin() + 1, args.end()}; diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index d6600f14d..6b9d3e44e 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -25,6 +25,7 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::SPLIT, this); pc->registerChecker(PfRule::RESOLUTION, this); pc->registerChecker(PfRule::CHAIN_RESOLUTION, this); + pc->registerTrustedChecker(PfRule::MACRO_RESOLUTION_TRUST, this, 3); pc->registerChecker(PfRule::MACRO_RESOLUTION, this); pc->registerChecker(PfRule::FACTORING, this); pc->registerChecker(PfRule::REORDERING, this); @@ -299,6 +300,12 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, : clauseNodes.size() == 1 ? clauseNodes[0] : nm->mkNode(kind::OR, clauseNodes); } + if (id == PfRule::MACRO_RESOLUTION_TRUST) + { + Assert(children.size() > 1); + Assert(args.size() == 2 * (children.size() - 1) + 1); + return args[0]; + } if (id == PfRule::MACRO_RESOLUTION) { Assert(children.size() > 1); |