summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/builtin/proof_checker.cpp115
-rw-r--r--src/theory/builtin/proof_checker.h48
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback