diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 115 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.h | 48 |
2 files changed, 70 insertions, 93 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index df6109b1d..f6b41104a 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -61,46 +61,17 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this); } -Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr) -{ - Node nk = SkolemManager::getSkolemForm(n); - Node nkr = applyRewriteExternal(nk, idr); - return SkolemManager::getWitnessForm(nkr); -} - -Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids) -{ - if (exp.isNull() || exp.getKind() != EQUAL) - { - return Node::null(); - } - Node nk = SkolemManager::getSkolemForm(n); - Node nks = applySubstitutionExternal(nk, exp, ids); - return SkolemManager::getWitnessForm(nks); -} - -Node BuiltinProofRuleChecker::applySubstitution(Node n, - const std::vector<Node>& exp, - MethodId ids) -{ - Node nk = SkolemManager::getSkolemForm(n); - Node nks = applySubstitutionExternal(nk, exp, ids); - return SkolemManager::getWitnessForm(nks); -} - Node BuiltinProofRuleChecker::applySubstitutionRewrite( Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr) { - Node nk = SkolemManager::getSkolemForm(n); - Node nks = applySubstitutionExternal(nk, exp, ids); - Node nksr = applyRewriteExternal(nks, idr); - return SkolemManager::getWitnessForm(nksr); + Node nks = applySubstitution(n, exp, ids); + return applyRewrite(nks, idr); } -Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr) +Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr) { Trace("builtin-pfcheck-debug") - << "applyRewriteExternal (" << idr << "): " << n << std::endl; + << "applyRewrite (" << idr << "): " << n << std::endl; if (idr == MethodId::RW_REWRITE) { return Rewriter::rewrite(n); @@ -111,50 +82,62 @@ Node BuiltinProofRuleChecker::applyRewriteExternal(Node n, MethodId idr) return n; } // unknown rewriter - Assert(false) - << "BuiltinProofRuleChecker::applyRewriteExternal: no rewriter for " - << idr << std::endl; + Assert(false) << "BuiltinProofRuleChecker::applyRewrite: no rewriter for " + << idr << std::endl; return n; } -Node BuiltinProofRuleChecker::applySubstitutionExternal(Node n, - Node exp, - MethodId ids) +bool BuiltinProofRuleChecker::getSubstitution(Node exp, + TNode& var, + TNode& subs, + MethodId ids) { - Assert(!exp.isNull()); - Node expk = SkolemManager::getSkolemForm(exp); - TNode var, subs; if (ids == MethodId::SB_DEFAULT) { - if (expk.getKind() != EQUAL) + if (exp.getKind() != EQUAL) { - return Node::null(); + return false; } - var = expk[0]; - subs = expk[1]; + var = exp[0]; + subs = exp[1]; } else if (ids == MethodId::SB_LITERAL) { - bool polarity = expk.getKind() != NOT; - var = polarity ? expk : expk[0]; + bool polarity = exp.getKind() != NOT; + var = polarity ? exp : exp[0]; subs = NodeManager::currentNM()->mkConst(polarity); } else if (ids == MethodId::SB_FORMULA) { - var = expk; + var = exp; subs = NodeManager::currentNM()->mkConst(true); } else { - Assert(false) << "BuiltinProofRuleChecker::applySubstitutionExternal: no " + Assert(false) << "BuiltinProofRuleChecker::applySubstitution: no " "substitution for " << ids << std::endl; + return false; + } + return true; +} + +Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids) +{ + TNode var, subs; + if (!getSubstitution(exp, var, subs, ids)) + { + return Node::null(); } + Trace("builtin-pfcheck-debug") + << "applySubstitution (" << ids << "): " << var << " -> " << subs + << " (from " << exp << ")" << std::endl; return n.substitute(var, subs); } -Node BuiltinProofRuleChecker::applySubstitutionExternal( - Node n, const std::vector<Node>& exp, MethodId ids) +Node BuiltinProofRuleChecker::applySubstitution(Node n, + const std::vector<Node>& exp, + MethodId ids) { Node curr = n; // apply substitution one at a time, in reverse order @@ -164,7 +147,7 @@ Node BuiltinProofRuleChecker::applySubstitutionExternal( { return Node::null(); } - curr = applySubstitutionExternal(curr, exp[nexp - 1 - i], ids); + curr = applySubstitution(curr, exp[nexp - 1 - i], ids); if (curr.isNull()) { break; @@ -233,12 +216,12 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, { Assert(children.empty()); Assert(1 <= args.size() && args.size() <= 2); - MethodId ids = MethodId::RW_REWRITE; - if (args.size() == 2 && !getMethodId(args[1], ids)) + MethodId idr = MethodId::RW_REWRITE; + if (args.size() == 2 && !getMethodId(args[1], idr)) { return Node::null(); } - Node res = applyRewrite(args[0]); + Node res = applyRewrite(args[0], idr); return args[0].eqNode(res); } else if (id == PfRule::MACRO_SR_EQ_INTRO) @@ -269,7 +252,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } // **** NOTE: can rewrite the witness form here. This enables certain lemmas // to be provable, e.g. (= k t) where k is a purification Skolem for t. - res = Rewriter::rewrite(res); + res = Rewriter::rewrite(SkolemManager::getWitnessForm(res)); if (!res.isConst() || !res.getConst<bool>()) { Trace("builtin-pfcheck") @@ -311,14 +294,18 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, exp.insert(exp.end(), children.begin() + 1, children.end()); Node res1 = applySubstitutionRewrite(children[0], exp, ids, idr); Node res2 = applySubstitutionRewrite(args[0], exp, ids, idr); - // can rewrite the witness forms - res1 = Rewriter::rewrite(res1); - res2 = Rewriter::rewrite(res2); - if (res1.isNull() || res1 != res2) + // if not already equal, do rewriting + if (res1 != res2) { - Trace("builtin-pfcheck") << "Failed to match results" << std::endl; - Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl; - return Node::null(); + // can rewrite the witness forms + res1 = Rewriter::rewrite(SkolemManager::getWitnessForm(res1)); + res2 = Rewriter::rewrite(SkolemManager::getWitnessForm(res2)); + if (res1.isNull() || res1 != res2) + { + Trace("builtin-pfcheck") << "Failed to match results" << std::endl; + Trace("builtin-pfcheck-debug") << res1 << " vs " << res2 << std::endl; + return Node::null(); + } } return args[0]; } diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index a2ec8b715..6dc7023d5 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -67,24 +67,31 @@ class BuiltinProofRuleChecker : public ProofRuleChecker BuiltinProofRuleChecker() {} ~BuiltinProofRuleChecker() {} /** - * Apply rewrite on n (in witness form). This encapsulates the exact behavior - * of a REWRITE step in a proof. Rewriting is performed on the Skolem form of - * n. + * Apply rewrite on n (in skolem form). This encapsulates the exact behavior + * of a REWRITE step in a proof. * - * @param n The node (in witness form) to rewrite, + * @param n The node to rewrite, * @param idr The method identifier of the rewriter, by default RW_REWRITE * specifying a call to Rewriter::rewrite. * @return The rewritten form of n. */ static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); /** - * Apply substitution on n (in witness form). This encapsulates the exact - * behavior of a SUBS step in a proof. Substitution is on the Skolem form of - * n. + * Get substitution. Updates vars/subs to the substitution specified by + * exp (e.g. as an equality) for the substitution method ids. + */ + static bool getSubstitution(Node exp, + TNode& var, + TNode& subs, + MethodId ids = MethodId::SB_DEFAULT); + + /** + * Apply substitution on n in skolem form. This encapsulates the exact + * behavior of a SUBS step in a proof. * - * @param n The node (in witness form) to substitute, - * @param exp The (set of) equalities (in witness form) corresponding to the - * substitution + * @param n The node to substitute, + * @param exp The (set of) equalities/literals/formulas that the substitution + * is derived from * @param ids The method identifier of the substitution, by default SB_DEFAULT * specifying that lhs/rhs of equalities are interpreted as a substitution. * @return The substituted form of n. @@ -99,9 +106,8 @@ class BuiltinProofRuleChecker : public ProofRuleChecker * * Combines the above two steps. * - * @param n The node (in witness form) to substitute and rewrite, - * @param exp The (set of) equalities (in witness form) corresponding to the - * substitution + * @param n The node to substitute and rewrite, + * @param exp The (set of) equalities corresponding to the substitution * @param ids The method identifier of the substitution. * @param idr The method identifier of the rewriter. * @return The substituted, rewritten form of n. @@ -129,27 +135,11 @@ class BuiltinProofRuleChecker : public ProofRuleChecker /** Register all rules owned by this rule checker into pc. */ void registerTo(ProofChecker* pc) override; - protected: /** Return the conclusion of the given proof step, or null if it is invalid */ Node checkInternal(PfRule id, const std::vector<Node>& children, const std::vector<Node>& args) override; - /** - * Apply rewrite (on Skolem form). id is the identifier of the rewriter. - */ - static Node applyRewriteExternal(Node n, MethodId idr = MethodId::RW_REWRITE); - /** - * Apply substitution for n (on Skolem form), where exp is an equality - * (or set of equalities) in Witness form. Returns the result of - * n * sigma{ids}(exp), where sigma{ids} is a substitution based on method - * identifier ids. - */ - static Node applySubstitutionExternal(Node n, Node exp, MethodId ids); - /** Same as above, for a list of substitutions in exp */ - static Node applySubstitutionExternal(Node n, - const std::vector<Node>& exp, - MethodId ids); }; } // namespace builtin |