summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/proof_rule.h15
-rw-r--r--src/smt/proof_post_processor.cpp48
-rw-r--r--src/theory/builtin/proof_checker.cpp20
-rw-r--r--src/theory/builtin/proof_checker.h6
-rw-r--r--src/theory/rewriter.cpp51
-rw-r--r--src/theory/rewriter.h3
6 files changed, 111 insertions, 32 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index e24d5c522..2b5565318 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -201,16 +201,17 @@ enum class PfRule : uint32_t
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":
//
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index a7723d265..40e61964c 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -21,6 +21,7 @@
#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;
@@ -543,14 +544,11 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
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)
{
@@ -559,10 +557,17 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
// 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
{
@@ -590,6 +595,24 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
}
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?
@@ -712,14 +735,6 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
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())
{
@@ -758,7 +773,8 @@ ProofPostproccess::ProofPostproccess(ProofNodeManager* pnm,
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)
{
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 73d39f417..4e2e78bae 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -34,6 +34,8 @@ const char* toString(MethodId id)
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";
@@ -76,7 +78,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
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(
@@ -282,6 +284,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
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)
@@ -294,6 +300,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
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)
@@ -301,6 +311,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
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)
@@ -312,6 +326,10 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
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)
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 66b04de45..fc26beaa1 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -50,6 +50,12 @@ enum class MethodId : uint32_t
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,
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 9e5708d4d..7ebacee92 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -31,6 +31,13 @@ using namespace std;
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.
@@ -100,7 +107,6 @@ Node Rewriter::rewrite(TNode node) {
}
TrustNode Rewriter::rewriteWithProof(TNode node,
- bool elimTheoryRewrite,
bool isExtEq)
{
// must set the proof checker before calling this
@@ -121,6 +127,7 @@ void Rewriter::setProofNodeManager(ProofNodeManager* pnm)
// 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,
@@ -182,6 +189,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
Node node,
TConvProofGenerator* tcpg)
{
+ RewriteWithProofsAttribute rpfa;
#ifdef CVC4_ASSERTIONS
bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
@@ -195,7 +203,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
// 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;
}
@@ -232,7 +240,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
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(;;) {
@@ -271,7 +279,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
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++;
@@ -355,6 +363,37 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
}
// 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);
@@ -443,11 +482,13 @@ RewriteResponse Rewriter::processTrustRewriteResponse(
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
{
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index f38f3b174..e36426a81 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -83,15 +83,12 @@ class Rewriter {
* 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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback