This PR fixes proofs in the rewriter so that we use attributes for marking whether a node has been rewritten with proofs instead of consulting the provided TConvProofGenerator for hasRewriteStep. This additionally marks TRUST_REWRITE steps if a rewriter happens to be nondeterministic (e.g. quantifiers). It furthermore decouples rewriteWithProof from reconstruction for theory rewrite steps.
The proof postprocessor is additionally updated so that extended equality REWRITE steps are converted to THEORY_REWRITE steps with identifier RW_REWRITE_EQ_EXT for consistency, since eliminating REWRITE should result in THEORY_REWRITE only. This required generalizing the argument to THEORY_REWRITE to be a MethodId instead of a Boolean.
THEORY_LEMMA,
// ======== Theory Rewrite
// Children: none
- // Arguments: (F, tid, preRewrite?)
+ // Arguments: (F, tid, rid)
// ----------------------------------------
// Conclusion: F
// where F is an equality of the form (= t t') where t' is obtained by
- // applying the theory rewriter with identifier tid in either its prewrite
- // (when preRewrite is true) or postrewrite method. Notice that the checker
- // for this rule does not replay the rewrite to ensure correctness, since
- // theory rewriter methods are not static. For example, the quantifiers
- // rewriter involves constructing new bound variables that are not guaranteed
- // to be consistent on each call.
+ // applying the kind of rewriting given by the method identifier rid, which
+ // is one of:
+ // { RW_REWRITE_THEORY_PRE, RW_REWRITE_THEORY_POST, RW_REWRITE_EQ_EXT }
+ // Notice that the checker for this rule does not replay the rewrite to ensure
+ // correctness, since theory rewriter methods are not static. For example,
+ // the quantifiers rewriter involves constructing new bound variables that are
+ // not guaranteed to be consistent on each call.
THEORY_REWRITE,
// The rules in this section have the signature of a "trusted rule":
//
#include "smt/smt_statistics_registry.h"
#include "theory/builtin/proof_checker.h"
#include "theory/rewriter.h"
+#include "theory/theory.h"
using namespace CVC4::kind;
using namespace CVC4::theory;
Node eq = args[0].eqNode(ret);
if (idr == MethodId::RW_REWRITE || idr == MethodId::RW_REWRITE_EQ_EXT)
{
- // automatically expand THEORY_REWRITE as well here if set
- bool elimTR =
- (d_elimRules.find(PfRule::THEORY_REWRITE) != d_elimRules.end());
// rewrites from theory::Rewriter
bool isExtEq = (idr == MethodId::RW_REWRITE_EQ_EXT);
// use rewrite with proof interface
Rewriter* rr = d_smte->getRewriter();
- TrustNode trn = rr->rewriteWithProof(args[0], elimTR, isExtEq);
+ TrustNode trn = rr->rewriteWithProof(args[0], isExtEq);
std::shared_ptr<ProofNode> pfn = trn.toProofNode();
if (pfn == nullptr)
{
// did not have a proof of rewriting, probably isExtEq is true
if (isExtEq)
{
- // don't update
- return Node::null();
+ // update to THEORY_REWRITE with idr
+ Assert(args.size() >= 1);
+ TheoryId theoryId = Theory::theoryOf(args[0].getType());
+ Node tid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
+ cdp->addStep(eq, PfRule::THEORY_REWRITE, {}, {eq, tid, args[1]});
+ }
+ else
+ {
+ // this should never be applied
+ cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq});
}
- cdp->addStep(eq, PfRule::TRUST_REWRITE, {}, {eq});
}
else
{
}
return eq;
}
+ else if (id == PfRule::THEORY_REWRITE)
+ {
+ Assert(!args.empty());
+ Node eq = args[0];
+ Assert(eq.getKind() == EQUAL);
+ // try to replay theory rewrite
+ // first, check that maybe its just an evaluation step
+ ProofChecker* pc = d_pnm->getChecker();
+ Node ceval =
+ pc->checkDebug(PfRule::EVALUATE, {}, {eq[0]}, eq, "smt-proof-pp-debug");
+ if (!ceval.isNull() && ceval == eq)
+ {
+ cdp->addStep(eq, PfRule::EVALUATE, {}, {eq[0]});
+ return eq;
+ }
+ // otherwise no update
+ Trace("final-pf-hole") << "hole: " << id << " : " << eq << std::endl;
+ }
// TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?
bool& continueUpdate)
{
PfRule r = pn->getRule();
- if (Trace.isOn("final-pf-hole"))
- {
- if (r == PfRule::THEORY_REWRITE)
- {
- Trace("final-pf-hole") << "hole: " << r << " : " << pn->getResult()
- << std::endl;
- }
- }
// if not doing eager pedantic checking, fail if below threshold
if (!options::proofNewPedanticEager())
{
ProofGenerator* pppg)
: d_pnm(pnm),
d_cb(pnm, smte, pppg),
- d_updater(d_pnm, d_cb),
+ // the update merges subproofs
+ d_updater(d_pnm, d_cb, true),
d_finalCb(pnm),
d_finalizer(d_pnm, d_finalCb)
{
case MethodId::RW_REWRITE_EQ_EXT: return "RW_REWRITE_EQ_EXT";
case MethodId::RW_EVALUATE: return "RW_EVALUATE";
case MethodId::RW_IDENTITY: return "RW_IDENTITY";
+ case MethodId::RW_REWRITE_THEORY_PRE: return "RW_REWRITE_THEORY_PRE";
+ case MethodId::RW_REWRITE_THEORY_POST: return "RW_REWRITE_THEORY_POST";
case MethodId::SB_DEFAULT: return "SB_DEFAULT";
case MethodId::SB_LITERAL: return "SB_LITERAL";
case MethodId::SB_FORMULA: return "SB_FORMULA";
pc->registerTrustedChecker(PfRule::WITNESS_AXIOM, this, 3);
pc->registerTrustedChecker(PfRule::TRUST_REWRITE, this, 1);
pc->registerTrustedChecker(PfRule::TRUST_SUBS, this, 1);
- pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 1);
+ pc->registerTrustedChecker(PfRule::TRUST_SUBS_MAP, this, 3);
}
Node BuiltinProofRuleChecker::applySubstitutionRewrite(
exp.push_back(children[i]);
}
Node res = applySubstitution(args[0], exp, ids);
+ if (res.isNull())
+ {
+ return Node::null();
+ }
return args[0].eqNode(res);
}
else if (id == PfRule::REWRITE)
return Node::null();
}
Node res = applyRewrite(args[0], idr);
+ if (res.isNull())
+ {
+ return Node::null();
+ }
return args[0].eqNode(res);
}
else if (id == PfRule::EVALUATE)
Assert(children.empty());
Assert(args.size() == 1);
Node res = applyRewrite(args[0], MethodId::RW_EVALUATE);
+ if (res.isNull())
+ {
+ return Node::null();
+ }
return args[0].eqNode(res);
}
else if (id == PfRule::MACRO_SR_EQ_INTRO)
return Node::null();
}
Node res = applySubstitutionRewrite(args[0], children, ids, idr);
+ if (res.isNull())
+ {
+ return Node::null();
+ }
return args[0].eqNode(res);
}
else if (id == PfRule::MACRO_SR_PRED_INTRO)
RW_EVALUATE,
// identity
RW_IDENTITY,
+ // theory preRewrite, note this is only intended to be used as an argument
+ // to THEORY_REWRITE in the final proof. It is not implemented in
+ // applyRewrite below, see documentation in proof_rule.h for THEORY_REWRITE.
+ RW_REWRITE_THEORY_PRE,
+ // same as above, for theory postRewrite
+ RW_REWRITE_THEORY_POST,
//---------------------------- Substitutions
// (= x y) is interpreted as x -> y, using Node::substitute
SB_DEFAULT,
namespace CVC4 {
namespace theory {
+/** Attribute true for nodes that have been rewritten with proofs enabled */
+struct RewriteWithProofsAttributeId
+{
+};
+typedef expr::Attribute<RewriteWithProofsAttributeId, bool>
+ RewriteWithProofsAttribute;
+
// Note that this function is a simplified version of Theory::theoryOf for
// (type-based) theoryOfMode. We expand and simplify it here for the sake of
// efficiency.
}
TrustNode Rewriter::rewriteWithProof(TNode node,
- bool elimTheoryRewrite,
bool isExtEq)
{
// must set the proof checker before calling this
// if not already initialized with proof support
if (d_tpg == nullptr)
{
+ Trace("rewriter") << "Rewriter::setProofNodeManager" << std::endl;
// the rewriter is staticly determinstic, thus use static cache policy
// for the term conversion proof generator
d_tpg.reset(new TConvProofGenerator(pnm,
Node node,
TConvProofGenerator* tcpg)
{
+ RewriteWithProofsAttribute rpfa;
#ifdef CVC4_ASSERTIONS
bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
// Check if it's been cached already
Node cached = getPostRewriteCache(theoryId, node);
- if (!cached.isNull() && (tcpg == nullptr || tcpg->hasRewriteStep(node)))
+ if (!cached.isNull() && (tcpg == nullptr || node.getAttribute(rpfa)))
{
return cached;
}
cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
rewriteStackTop.d_node);
if (cached.isNull()
- || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node)))
+ || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
{
// Rewrite until fix-point is reached
for(;;) {
rewriteStackTop.d_node);
// If not, go through the children
if (cached.isNull()
- || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node)))
+ || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
{
// The child we need to rewrite
unsigned child = rewriteStackTop.d_nextChild++;
}
// We're done with the post rewrite, so we add to the cache
+ if (tcpg != nullptr)
+ {
+ // if proofs are enabled, mark that we've rewritten with proofs
+ rewriteStackTop.d_original.setAttribute(rpfa, true);
+ if (!cached.isNull())
+ {
+ // We may have gotten a different node, due to non-determinism in
+ // theory rewriters (e.g. quantifiers rewriter which introduces
+ // fresh BOUND_VARIABLE). This can happen if we wrote once without
+ // proofs and then rewrote again with proofs.
+ if (rewriteStackTop.d_node != cached)
+ {
+ Trace("rewriter-proof") << "WARNING: Rewritten forms with and "
+ "without proofs were not equivalent"
+ << std::endl;
+ Trace("rewriter-proof")
+ << " original: " << rewriteStackTop.d_original << std::endl;
+ Trace("rewriter-proof")
+ << "with proofs: " << rewriteStackTop.d_node << std::endl;
+ Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl;
+ Node eq = rewriteStackTop.d_node.eqNode(cached);
+ tcpg->addRewriteStep(rewriteStackTop.d_node,
+ cached,
+ PfRule::TRUST_REWRITE,
+ {},
+ {eq});
+ // don't overwrite the cache, should be the same
+ rewriteStackTop.d_node = cached;
+ }
+ }
+ }
setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
rewriteStackTop.d_original,
rewriteStackTop.d_node);
Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
// add small step trusted rewrite
NodeManager* nm = NodeManager::currentNM();
+ Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE
+ : MethodId::RW_REWRITE_THEORY_POST);
tcpg->addRewriteStep(proven[0],
proven[1],
PfRule::THEORY_REWRITE,
{},
- {proven, tidn, nm->mkConst(isPre)});
+ {proven, tidn, rid});
}
else
{
* to setProofNodeManager prior to this call.
*
* @param node The node to rewrite.
- * @param elimTheoryRewrite Whether we also want fine-grained proofs for
- * THEORY_REWRITE steps.
* @param isExtEq Whether node is an equality which we are applying
* rewriteEqualityExt on.
* @return The trust node of kind TrustNodeKind::REWRITE that contains the
* rewritten form of node.
*/
TrustNode rewriteWithProof(TNode node,
- bool elimTheoryRewrite = false,
bool isExtEq = false);
/** Set proof node manager */
projects / cvc5.git / commitdiff