diff options
| -rw-r--r-- | src/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/expr/proof_checker.cpp | 20 | ||||
| -rw-r--r-- | src/expr/proof_checker.h | 16 | ||||
| -rw-r--r-- | src/expr/proof_rule.h | 14 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 115 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.h | 48 |
6 files changed, 97 insertions, 120 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5cddccc58..9c95163bc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -367,13 +367,13 @@ libcvc4_add_sources( theory/booleans/theory_bool_rewriter.h theory/booleans/theory_bool_type_rules.h theory/booleans/type_enumerator.h + theory/builtin/proof_checker.cpp + theory/builtin/proof_checker.h theory/builtin/theory_builtin.cpp theory/builtin/theory_builtin.h theory/builtin/theory_builtin_rewriter.cpp theory/builtin/theory_builtin_rewriter.h theory/builtin/theory_builtin_type_rules.h - theory/builtin/proof_checker.cpp - theory/builtin/proof_checker.h theory/builtin/type_enumerator.cpp theory/builtin/type_enumerator.h theory/bv/abstraction.cpp diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp index acbf6ee49..8f786052b 100644 --- a/src/expr/proof_checker.cpp +++ b/src/expr/proof_checker.cpp @@ -25,14 +25,8 @@ Node ProofRuleChecker::check(PfRule id, const std::vector<Node>& children, const std::vector<Node>& args) { - // convert to witness form - std::vector<Node> childrenw = children; - std::vector<Node> argsw = args; - SkolemManager::convertToWitnessFormVec(childrenw); - SkolemManager::convertToWitnessFormVec(argsw); - Node res = checkInternal(id, childrenw, argsw); - // res is in terms of witness form, convert back to Skolem form - return SkolemManager::getSkolemForm(res); + // call instance-specific checkInternal method + return checkInternal(id, children, args); } Node ProofRuleChecker::checkChildrenArg(PfRule id, @@ -259,4 +253,14 @@ void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc) d_checker[id] = psc; } +ProofRuleChecker* ProofChecker::getCheckerFor(PfRule id) +{ + std::map<PfRule, ProofRuleChecker*>::const_iterator it = d_checker.find(id); + if (it == d_checker.end()) + { + return nullptr; + } + return it->second; +} + } // namespace CVC4 diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index d6d77df2b..65ad9f24d 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -40,8 +40,8 @@ class ProofRuleChecker * premises and arguments, or null if such a proof node is not well-formed. * * Note that the input/output of this method expects to be terms in *Skolem - * form*. To facilitate checking, this method converts to/from witness - * form, calling the subprocedure checkInternal below. + * form*, which is passed to checkInternal below. Rule checkers may + * convert premises to witness form when necessary. * * @param id The id of the proof node to check * @param children The premises of the proof node to check. These are nodes @@ -75,17 +75,15 @@ class ProofRuleChecker protected: /** - * This checks a single step in a proof. It is identical to check above - * except that children and args have been converted to "witness form" - * (see SkolemManager). Likewise, its output should be in witness form. + * This checks a single step in a proof. * * @param id The id of the proof node to check * @param children The premises of the proof node to check. These are nodes * corresponding to the conclusion (ProofNode::getResult) of the children - * of the proof node we are checking, in witness form. + * of the proof node we are checking. * @param args The arguments of the proof node to check - * @return The conclusion of the proof node, in witness form, if successful or - * null if such a proof node is malformed. + * @return The conclusion of the proof node if successful or null if such a + * proof node is malformed. */ virtual Node checkInternal(PfRule id, const std::vector<Node>& children, @@ -158,6 +156,8 @@ class ProofChecker const char* traceTag); /** Indicate that psc is the checker for proof rule id */ void registerChecker(PfRule id, ProofRuleChecker* psc); + /** get checker for */ + ProofRuleChecker* getCheckerFor(PfRule id); private: /** statistics class */ diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index ec589a16e..a15d8a2d2 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -102,12 +102,8 @@ enum class PfRule : uint32_t // Conclusion: (= t t') // where // t' is - // toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))) - // toSkolem(...) converts terms from witness form to Skolem form, - // toWitness(...) converts terms from Skolem form to witness form. + // Rewriter{idr}(t*sigma{ids}(Fn)*...*sigma{ids}(F1)) // - // Notice that: - // toSkolem(t')=Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1)) // In other words, from the point of view of Skolem forms, this rule // transforms t to t' by standard substitution + rewriting. // @@ -125,7 +121,7 @@ enum class PfRule : uint32_t // --------------------------------------------------------------- // Conclusion: F // where - // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true + // Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) == true // where ids and idr are method identifiers. // // Notice that we apply rewriting on the witness form of F, meaning that this @@ -145,7 +141,7 @@ enum class PfRule : uint32_t // Conclusion: F' // where // F' is - // toWitness(Rewriter{idr}(toSkolem(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)). + // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)). // where ids and idr are method identifiers. // // We rewrite only on the Skolem form of F, similar to MACRO_SR_EQ_INTRO. @@ -161,8 +157,8 @@ enum class PfRule : uint32_t // ---------------------------------------- // Conclusion: G // where - // Rewriter{idr}(F*sigma{ids}(Fn)*...*sigma{ids}(F1)) == - // Rewriter{idr}(G*sigma{ids}(Fn)*...*sigma{ids}(F1)) + // Rewriter{idr}(toWitness(F)*sigma{ids}(Fn)*...*sigma{ids}(F1)) == + // Rewriter{idr}(toWitness(G)*sigma{ids}(Fn)*...*sigma{ids}(F1)) // // Notice that we apply rewriting on the witness form of F and G, similar to // MACRO_SR_PRED_INTRO. 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 |