This adds support for skeleton proofs in the rewriter (REWRITE -> THEORY_REWRITE).
It adds "extended equality rewrite" as a new method of the rewriter/theory rewriters.
The unit test of this feature should be added on a followup PR.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
theory/theory_preprocessor.h
theory/theory_proof_step_buffer.cpp
theory/theory_proof_step_buffer.h
+ theory/theory_rewriter.cpp
theory/theory_rewriter.h
theory/theory_registrar.h
theory/theory_test_utils.h
case PfRule::MACRO_SR_PRED_INTRO: return "MACRO_SR_PRED_INTRO";
case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM";
case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM";
+ case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
case PfRule::PREPROCESS: return "PREPROCESS";
//================================================= Boolean rules
case PfRule::SPLIT: return "SPLIT";
// Notice that we apply rewriting on the witness form of F and G, similar to
// MACRO_SR_PRED_INTRO.
MACRO_SR_PRED_TRANSFORM,
+ // ======== Theory Rewrite
+ // Children: none
+ // Arguments: (t, preRewrite?)
+ // ----------------------------------------
+ // Conclusion: (= t t')
+ // where
+ // t' is the result of applying either a pre-rewrite or a post-rewrite step
+ // to t (depending on the second argument).
+ THEORY_REWRITE,
//================================================= Processing rules
// ======== Preprocess
pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
pc->registerChecker(PfRule::MACRO_SR_PRED_TRANSFORM, this);
+ pc->registerChecker(PfRule::THEORY_REWRITE, this);
pc->registerChecker(PfRule::PREPROCESS, this);
}
+Node BuiltinProofRuleChecker::applyTheoryRewrite(Node n, bool preRewrite)
+{
+ TheoryId tid = Theory::theoryOf(n);
+ Rewriter* rewriter = Rewriter::getInstance();
+ Node nkr = preRewrite ? rewriter->preRewrite(tid, n).d_node
+ : rewriter->postRewrite(tid, n).d_node;
+ return nkr;
+}
+
+
Node BuiltinProofRuleChecker::applySubstitutionRewrite(
Node n, const std::vector<Node>& exp, MethodId ids, MethodId idr)
{
* @return The rewritten form of n.
*/
static Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
+ /**
+ * Apply small-step rewrite on n in skolem form (either pre- or
+ * post-rewrite). This encapsulates the exact behavior of a THEORY_REWRITE
+ * step in a proof.
+ *
+ * @param n The node to rewrite
+ * @param preRewrite If true, performs a pre-rewrite or a post-rewrite
+ * otherwise
+ * @return The rewritten form of n
+ */
+ static Node applyTheoryRewrite(Node n, bool preRewrite);
/**
* Get substitution. Updates vars/subs to the substitution specified by
* exp (e.g. as an equality) for the substitution method ids.
/** The node we're currently rewriting */
Node d_node;
- /** Original node */
+ /** Original node (either the unrewritten node or the node after prerewriting)
+ */
Node d_original;
/** Id of the theory that's currently rewriting this node */
unsigned d_theoryId : 8;
return getInstance()->rewriteTo(theoryOf(node), node);
}
+TrustNode Rewriter::rewriteWithProof(TNode node,
+ bool elimTheoryRewrite,
+ bool isExtEq)
+{
+ // must set the proof checker before calling this
+ Assert(d_tpg != nullptr);
+ if (isExtEq)
+ {
+ // theory rewriter is responsible for rewriting the equality
+ TheoryRewriter* tr = getInstance()->d_theoryRewriters[theoryOf(node)];
+ Assert(tr != nullptr);
+ return tr->rewriteEqualityExtWithProof(node);
+ }
+ Node ret = getInstance()->rewriteTo(theoryOf(node), node, d_tpg.get());
+ return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
+}
+
+void Rewriter::setProofChecker(ProofChecker* pc)
+{
+ // if not already initialized with proof support
+ if (d_tpg == nullptr)
+ {
+ d_pnm.reset(new ProofNodeManager(pc));
+ d_tpg.reset(new TConvProofGenerator(d_pnm.get()));
+ }
+}
+
+Node Rewriter::rewriteEqualityExt(TNode node)
+{
+ Assert(node.getKind() == kind::EQUAL);
+ // note we don't force caching of this method currently
+ return getInstance()->d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(
+ node);
+}
+
void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
TheoryRewriter* trew)
{
return smt::currentSmtEngine()->getRewriter();
}
-Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
-
+Node Rewriter::rewriteTo(theory::TheoryId theoryId,
+ Node node,
+ TConvProofGenerator* tcpg)
+{
#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()) {
+ if (!cached.isNull() && (tcpg == nullptr || tcpg->hasRewriteStep(node)))
+ {
return cached;
}
// Check if the pre-rewrite has already been done (it's in the cache)
cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
rewriteStackTop.d_node);
- if (cached.isNull()) {
+ if (cached.isNull()
+ || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node)))
+ {
// Rewrite until fix-point is reached
for(;;) {
// Perform the pre-rewrite
- RewriteResponse response =
- preRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node);
+ RewriteResponse response = preRewrite(
+ rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
+
// Put the rewritten node to the top of the stack
rewriteStackTop.d_node = response.d_node;
TheoryId newTheory = theoryOf(rewriteStackTop.d_node);
}
rewriteStackTop.d_theoryId = newTheory;
}
+
// Cache the rewrite
setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
rewriteStackTop.d_original,
cached = getPostRewriteCache(rewriteStackTop.getTheoryId(),
rewriteStackTop.d_node);
// If not, go through the children
- if(cached.isNull()) {
-
+ if (cached.isNull()
+ || (tcpg != nullptr && !tcpg->hasRewriteStep(rewriteStackTop.d_node)))
+ {
// The child we need to rewrite
unsigned child = rewriteStackTop.d_nextChild++;
// Done with all pre-rewriting, so let's do the post rewrite
for(;;) {
// Do the post-rewrite
- RewriteResponse response =
- postRewrite(rewriteStackTop.getTheoryId(), rewriteStackTop.d_node);
+ RewriteResponse response = postRewrite(
+ rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
+
// We continue with the response we got
TheoryId newTheoryId = theoryOf(response.d_node);
if (newTheoryId != rewriteStackTop.getTheoryId()
== d_rewriteStack->end());
d_rewriteStack->insert(response.d_node);
#endif
- Node rewritten = rewriteTo(newTheoryId, response.d_node);
+ Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg);
rewriteStackTop.d_node = rewritten;
#ifdef CVC4_ASSERTIONS
d_rewriteStack->erase(response.d_node);
!= rewriteStackTop.d_node);
rewriteStackTop.d_node = response.d_node;
}
+
// We're done with the post rewrite, so we add to the cache
setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
rewriteStackTop.d_original,
rewriteStackTop.d_node);
- } else {
+ }
+ else
+ {
// We were already in cache, so just remember it
rewriteStackTop.d_node = cached;
rewriteStackTop.d_theoryId = theoryOf(cached);
}
Unreachable();
-}/* Rewriter::rewriteTo() */
+} /* Rewriter::rewriteTo() */
-RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId, TNode n)
+RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId,
+ TNode n,
+ TConvProofGenerator* tcpg)
{
Kind k = n.getKind();
std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
(k == kind::EQUAL) ? d_preRewritersEqual[theoryId] : d_preRewriters[k];
if (fn == nullptr)
{
+ if (tcpg != nullptr)
+ {
+ // call the trust rewrite response interface
+ TrustRewriteResponse tresponse =
+ d_theoryRewriters[theoryId]->preRewriteWithProof(n);
+ // process the trust rewrite response: store the proof step into
+ // tcpg if necessary and then convert to rewrite response.
+ return processTrustRewriteResponse(tresponse, true, tcpg);
+ }
return d_theoryRewriters[theoryId]->preRewrite(n);
}
return fn(&d_re, n);
}
-RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId, TNode n)
+RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
+ TNode n,
+ TConvProofGenerator* tcpg)
{
Kind k = n.getKind();
std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
(k == kind::EQUAL) ? d_postRewritersEqual[theoryId] : d_postRewriters[k];
if (fn == nullptr)
{
+ if (tcpg != nullptr)
+ {
+ // same as above, for post-rewrite
+ TrustRewriteResponse tresponse =
+ d_theoryRewriters[theoryId]->postRewriteWithProof(n);
+ return processTrustRewriteResponse(tresponse, false, tcpg);
+ }
return d_theoryRewriters[theoryId]->postRewrite(n);
}
return fn(&d_re, n);
}
+RewriteResponse Rewriter::processTrustRewriteResponse(
+ const TrustRewriteResponse& tresponse,
+ bool isPre,
+ TConvProofGenerator* tcpg)
+{
+ Assert(tcpg != nullptr);
+ TrustNode trn = tresponse.d_node;
+ Assert(trn.getKind() == TrustNodeKind::REWRITE);
+ Node proven = trn.getProven();
+ if (proven[0] != proven[1])
+ {
+ ProofGenerator* pg = trn.getGenerator();
+ if (pg == nullptr)
+ {
+ // add small step trusted rewrite
+ NodeManager* nm = NodeManager::currentNM();
+ tcpg->addRewriteStep(proven[0],
+ proven[1],
+ PfRule::THEORY_REWRITE,
+ {},
+ {proven[0], nm->mkConst(isPre)});
+ }
+ else
+ {
+ // store proven rewrite step
+ tcpg->addRewriteStep(proven[0], proven[1], pg);
+ }
+ }
+ return RewriteResponse(tresponse.d_status, trn.getNode());
+}
+
void Rewriter::clearCaches() {
Rewriter* rewriter = getInstance();
#pragma once
#include "expr/node.h"
+#include "expr/term_conversion_proof_generator.h"
#include "theory/theory_rewriter.h"
+#include "theory/trust_node.h"
#include "util/unsafe_interrupt_exception.h"
namespace CVC4 {
namespace theory {
+namespace builtin {
+class BuiltinProofRuleChecker;
+}
+
class RewriterInitializer;
/**
* The main rewriter class.
*/
class Rewriter {
+ friend builtin::BuiltinProofRuleChecker;
+
public:
Rewriter();
*/
static Node rewrite(TNode node);
+ /**
+ * Rewrites the equality node using theoryOf() to determine which rewriter to
+ * use on the node corresponding to an equality s = t.
+ *
+ * Specifically, this method performs rewrites whose conclusion is not
+ * necessarily one of { s = t, t = s, true, false }, which is an invariant
+ * guaranted by the above method. This invariant is motivated by theory
+ * combination, which needs to guarantee that equalities between terms
+ * can be communicated for all pairs of terms.
+ */
+ static Node rewriteEqualityExt(TNode node);
+
+ /**
+ * Rewrite with proof production, which is managed by the term conversion
+ * proof generator managed by this class (d_tpg). This method requires a call
+ * to setProofChecker 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 checker */
+ void setProofChecker(ProofChecker* pc);
+
/**
* Garbage collects the rewrite caches.
*/
/**
* Rewrites the node using the given theory rewriter.
*/
- Node rewriteTo(theory::TheoryId theoryId, Node node);
+ Node rewriteTo(theory::TheoryId theoryId,
+ Node node,
+ TConvProofGenerator* tcpg = nullptr);
/** Calls the pre-rewriter for the given theory */
- RewriteResponse preRewrite(theory::TheoryId theoryId, TNode n);
+ RewriteResponse preRewrite(theory::TheoryId theoryId,
+ TNode n,
+ TConvProofGenerator* tcpg = nullptr);
/** Calls the post-rewriter for the given theory */
- RewriteResponse postRewrite(theory::TheoryId theoryId, TNode n);
+ RewriteResponse postRewrite(theory::TheoryId theoryId,
+ TNode n,
+ TConvProofGenerator* tcpg = nullptr);
+ /** processes a trust rewrite response */
+ RewriteResponse processTrustRewriteResponse(
+ const TrustRewriteResponse& tresponse,
+ bool isPre,
+ TConvProofGenerator* tcpg);
/**
* Calls the equality-rewriter for the given theory.
RewriteEnvironment d_re;
+ /** The proof node manager */
+ std::unique_ptr<ProofNodeManager> d_pnm;
+ /** The proof generator */
+ std::unique_ptr<TConvProofGenerator> d_tpg;
#ifdef CVC4_ASSERTIONS
std::unique_ptr<std::unordered_set<Node, NodeHashFunction>> d_rewriteStack =
nullptr;
* Specifically, this function performs rewrites whose conclusion is not
* necessarily one of { s = t, t = s, true, false }.
*/
- Node rewriteEqualityExt(Node node);
+ Node rewriteEqualityExt(Node node) override;
/** rewrite string length
* This is the entry point for post-rewriting terms node of the form
* str.len( t )
--- /dev/null
+/********************* */
+/*! \file theory_rewriter.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The TheoryRewriter class
+ **
+ ** The TheoryRewriter class is the interface that theory rewriters implement.
+ **/
+
+#include "theory/theory_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+
+TrustRewriteResponse::TrustRewriteResponse(RewriteStatus status,
+ Node n,
+ Node nr,
+ ProofGenerator* pg)
+ : d_status(status)
+{
+ // we always make non-null, regardless of whether n = nr
+ d_node = TrustNode::mkTrustRewrite(n, nr, pg);
+}
+
+TrustRewriteResponse TheoryRewriter::postRewriteWithProof(TNode node)
+{
+ RewriteResponse response = postRewrite(node);
+ // by default, we return a trust rewrite response with no proof generator
+ return TrustRewriteResponse(
+ response.d_status, node, response.d_node, nullptr);
+}
+
+TrustRewriteResponse TheoryRewriter::preRewriteWithProof(TNode node)
+{
+ RewriteResponse response = preRewrite(node);
+ // by default, we return a trust rewrite response with no proof generator
+ return TrustRewriteResponse(
+ response.d_status, node, response.d_node, nullptr);
+}
+
+Node TheoryRewriter::rewriteEqualityExt(Node node) { return node; }
+
+TrustNode TheoryRewriter::rewriteEqualityExtWithProof(Node node)
+{
+ Node nodeRew = rewriteEqualityExt(node);
+ if (nodeRew != node)
+ {
+ // by default, we return a trust rewrite response with no proof generator
+ return TrustNode::mkTrustRewrite(node, nodeRew, nullptr);
+ }
+ // no rewrite
+ return TrustNode::null();
+}
+
+} // namespace theory
+} // namespace CVC4
#define CVC4__THEORY__THEORY_REWRITER_H
#include "expr/node.h"
+#include "theory/trust_node.h"
namespace CVC4 {
namespace theory {
RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {}
}; /* struct RewriteResponse */
+/** Same as above, with trust node instead of node. */
+struct TrustRewriteResponse
+{
+ TrustRewriteResponse(RewriteStatus status,
+ Node n,
+ Node nr,
+ ProofGenerator* pg);
+ /** The status of the rewrite */
+ const RewriteStatus d_status;
+ /**
+ * The trust node corresponding to the rewrite.
+ */
+ TrustNode d_node;
+};
+
/**
* The interface that a theory rewriter has to implement.
*
*/
virtual RewriteResponse postRewrite(TNode node) = 0;
+ /**
+ * Performs a pre-rewrite step, with proofs.
+ *
+ * @param node The node to rewrite
+ */
+ virtual TrustRewriteResponse postRewriteWithProof(TNode node);
+
/**
* Performs a post-rewrite step.
*
* @param node The node to rewrite
*/
virtual RewriteResponse preRewrite(TNode node) = 0;
+
+ /**
+ * Performs a pre-rewrite step, with proofs.
+ *
+ * @param node The node to rewrite
+ */
+ virtual TrustRewriteResponse preRewriteWithProof(TNode node);
+
+ /** rewrite equality extended
+ *
+ * This method returns a formula that is equivalent to the equality between
+ * two terms s = t, given by node.
+ *
+ * Specifically, this method performs rewrites whose conclusion is not
+ * necessarily one of { s = t, t = s, true, false }. This is in constrast
+ * to postRewrite and preRewrite above, where the rewritten form of an
+ * equality must be one of these.
+ *
+ * @param node The node to rewrite
+ */
+ virtual Node rewriteEqualityExt(Node node);
+
+ /** rewrite equality extended, with proofs
+ *
+ * @param node The node to rewrite
+ * @return A trust node of kind TrustNodeKind::REWRITE, or the null trust
+ * node if no rewrites are applied.
+ */
+ virtual TrustNode rewriteEqualityExtWithProof(Node node);
};
} // namespace theory
projects / cvc5.git / commitdiff