diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-18 17:17:37 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-18 17:17:37 -0500 |
commit | d4a23ab31a6f811dc4a9c3f24acb9a325fcb6d5a (patch) | |
tree | 6c204671b6110b58c774b87cd5290b5f14c25453 /src/theory/builtin | |
parent | 4d2cc845273d078660a0e8f9946516edec93e25e (diff) |
(proof-new) More features for SMT proof post-processor (#5246)
This updates the SMT proof postprocessor with additional stats. It also adds the feature to handle conjunctions as substitution, e.g. a child proof concluding (and (= x t) (= y s)) is interpreted as a substitution for x, y, whereas previously we insisted they must be provided separately.
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 75 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.h | 26 |
2 files changed, 78 insertions, 23 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 8824859d4..6fc4671ee 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -69,11 +69,11 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::REMOVE_TERM_FORMULA_AXIOM, this); // trusted rules pc->registerTrustedChecker(PfRule::THEORY_LEMMA, this, 1); - pc->registerTrustedChecker(PfRule::PREPROCESS, this, 2); - pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 2); - pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 2); - pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 2); - pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 2); + pc->registerTrustedChecker(PfRule::PREPROCESS, this, 3); + pc->registerTrustedChecker(PfRule::PREPROCESS_LEMMA, this, 3); + pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS, this, 3); + pc->registerTrustedChecker(PfRule::THEORY_PREPROCESS_LEMMA, this, 3); + pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3); pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1); pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1); } @@ -117,10 +117,10 @@ Node BuiltinProofRuleChecker::applyRewrite(Node n, MethodId idr) return n; } -bool BuiltinProofRuleChecker::getSubstitution(Node exp, - TNode& var, - TNode& subs, - MethodId ids) +bool BuiltinProofRuleChecker::getSubstitutionForLit(Node exp, + TNode& var, + TNode& subs, + MethodId ids) { if (ids == MethodId::SB_DEFAULT) { @@ -152,17 +152,57 @@ bool BuiltinProofRuleChecker::getSubstitution(Node exp, return true; } +bool BuiltinProofRuleChecker::getSubstitutionFor(Node exp, + std::vector<TNode>& vars, + std::vector<TNode>& subs, + std::vector<TNode>& from, + MethodId ids) +{ + TNode v; + TNode s; + if (exp.getKind() == AND && ids == MethodId::SB_DEFAULT) + { + for (const Node& ec : exp) + { + // non-recursive, do not use nested AND + if (!getSubstitutionForLit(ec, v, s, ids)) + { + return false; + } + vars.push_back(v); + subs.push_back(s); + from.push_back(ec); + } + return true; + } + bool ret = getSubstitutionForLit(exp, v, s, ids); + vars.push_back(v); + subs.push_back(s); + from.push_back(exp); + return ret; +} + Node BuiltinProofRuleChecker::applySubstitution(Node n, Node exp, MethodId ids) { - TNode var, subs; - if (!getSubstitution(exp, var, subs, ids)) + std::vector<TNode> vars; + std::vector<TNode> subs; + std::vector<TNode> from; + if (!getSubstitutionFor(exp, vars, subs, from, ids)) { return Node::null(); } - Trace("builtin-pfcheck-debug") - << "applySubstitution (" << ids << "): " << var << " -> " << subs - << " (from " << exp << ")" << std::endl; - return n.substitute(var, subs); + Node ns = n; + // apply substitution one at a time, in reverse order + for (size_t i = 0, nvars = vars.size(); i < nvars; i++) + { + TNode v = vars[nvars - 1 - i]; + TNode s = subs[nvars - 1 - i]; + Trace("builtin-pfcheck-debug") + << "applySubstitution (" << ids << "): " << v << " -> " << s + << " (from " << exp << ")" << std::endl; + ns = ns.substitute(v, s); + } + return ns; } Node BuiltinProofRuleChecker::applySubstitution(Node n, @@ -212,6 +252,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, } else if (id == PfRule::SCOPE) { + NodeManager * nm = NodeManager::currentNM(); Assert(children.size() == 1); if (args.empty()) { @@ -224,7 +265,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, { return ant.notNode(); } - return NodeManager::currentNM()->mkNode(IMPLIES, ant, children[0]); + return nm->mkNode(IMPLIES, ant, children[0]); } else if (id == PfRule::SUBS) { @@ -270,7 +311,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, { return Node::null(); } - Node res = applySubstitutionRewrite(args[0], children, idr); + Node res = applySubstitutionRewrite(args[0], children, ids, idr); return args[0].eqNode(res); } else if (id == PfRule::MACRO_SR_PRED_INTRO) diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index d1c3309c3..66b04de45 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -84,13 +84,27 @@ class BuiltinProofRuleChecker : public ProofRuleChecker */ Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE); /** - * Get substitution. Updates vars/subs to the substitution specified by - * exp for the substitution method ids. + * Get substitution for literal exp. Updates vars/subs to the substitution + * specified by exp for the substitution method ids. */ - static bool getSubstitution(Node exp, - TNode& var, - TNode& subs, - MethodId ids = MethodId::SB_DEFAULT); + static bool getSubstitutionForLit(Node exp, + TNode& var, + TNode& subs, + MethodId ids = MethodId::SB_DEFAULT); + /** + * Get substitution for formula exp. Adds to vars/subs to the substitution + * specified by exp for the substitution method ids, which may be multiple + * substitutions if exp is of kind AND and ids is SB_DEFAULT (note the other + * substitution types always interpret applications of AND as a formula). + * The vector "from" are the literals from exp that each substitution in + * vars/subs are based on. For example, if exp is (and (= x t) (= y s)), then + * vars = { x, y }, subs = { t, s }, from = { (= x y), (= y s) }. + */ + static bool getSubstitutionFor(Node exp, + std::vector<TNode>& vars, + std::vector<TNode>& subs, + std::vector<TNode>& from, + MethodId ids = MethodId::SB_DEFAULT); /** * Apply substitution on n in skolem form. This encapsulates the exact |