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/expr | |
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/expr')
-rw-r--r-- | src/expr/lazy_proof_chain.cpp | 13 | ||||
-rw-r--r-- | src/expr/proof_rule.h | 12 |
2 files changed, 19 insertions, 6 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 |