This includes support for some trusted rules (whose use is to come). It also modifies THEORY_REWRITE so that it is a "trusted" rule, that is, it is not re-checked. The reason for this is that TheoryRewriter is not deterministic. An example of non-determinism in TheoryRewriter are rules that introduce bound variables (e.g. quantifiers rewriter) since these bound variables are fresh each time it is invoked. Non-deterministic theory rewriters cannot be rechecked, which was leading to failures on proof-new at proof check time. The other way to fix this would be to cache TheoryRewriter responses, but then the checker would only be verifying that the caching was being done properly. This is not worthwhile.
case PfRule::SCOPE: return "SCOPE";
case PfRule::SUBS: return "SUBS";
case PfRule::REWRITE: return "REWRITE";
+ case PfRule::EVALUATE: return "EVALUATE";
case PfRule::MACRO_SR_EQ_INTRO: return "MACRO_SR_EQ_INTRO";
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::REMOVE_TERM_FORMULA_AXIOM: return "REMOVE_TERM_FORMULA_AXIOM";
//================================================= Trusted rules
+ case PfRule::THEORY_LEMMA: return "THEORY_LEMMA";
+ case PfRule::THEORY_REWRITE: return "THEORY_REWRITE";
case PfRule::PREPROCESS: return "PREPROCESS";
case PfRule::PREPROCESS_LEMMA: return "PREPROCESS_LEMMA";
case PfRule::THEORY_PREPROCESS: return "THEORY_PREPROCESS";
// where idr is a MethodId identifier, which determines the kind of rewriter
// to apply, e.g. Rewriter::rewrite.
REWRITE,
+ // ======== Evaluate
+ // Children: none
+ // Arguments: (t)
+ // ----------------------------------------
+ // Conclusion: (= t Evaluator::evaluate(t))
+ // Note this is equivalent to:
+ // (REWRITE t MethodId::RW_EVALUATE)
+ EVALUATE,
// ======== Substitution + Rewriting equality introduction
//
// In this rule, we provide a term t and conclude that it is equal to its
// 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
// ======== Remove Term Formulas Axiom
REMOVE_TERM_FORMULA_AXIOM,
//================================================= Trusted rules
+ // ======== Theory lemma
+ // Children: none
+ // Arguments: (F, tid)
+ // ---------------------------------------------------------------
+ // Conclusion: F
+ // where F is a (T-valid) theory lemma generated by theory with TheoryId tid.
+ // This is a "coarse-grained" rule that is used as a placeholder if a theory
+ // did not provide a proof for a lemma or conflict.
+ THEORY_LEMMA,
+ // ======== Theory Rewrite
+ // Children: none
+ // Arguments: (F, tid, preRewrite?)
+ // ----------------------------------------
+ // 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.
+ THEORY_REWRITE,
// The rules in this section have the signature of a "trusted rule":
//
// Children: none
#include "expr/skolem_manager.h"
#include "smt/term_formula_removal.h"
+#include "theory/evaluator.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
switch (id)
{
case MethodId::RW_REWRITE: return "RW_REWRITE";
+ case MethodId::RW_EXT_REWRITE: return "RW_EXT_REWRITE";
+ 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::SB_DEFAULT: return "SB_DEFAULT";
case MethodId::SB_LITERAL: return "SB_LITERAL";
pc->registerChecker(PfRule::SCOPE, this);
pc->registerChecker(PfRule::SUBS, this);
pc->registerChecker(PfRule::REWRITE, this);
+ pc->registerChecker(PfRule::EVALUATE, this);
pc->registerChecker(PfRule::MACRO_SR_EQ_INTRO, this);
pc->registerChecker(PfRule::MACRO_SR_PRED_INTRO, this);
pc->registerChecker(PfRule::MACRO_SR_PRED_ELIM, this);
pc->registerChecker(PfRule::THEORY_REWRITE, this);
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::WITNESS_AXIOM, this, 2);
}
-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 Rewriter::rewrite(n);
}
- else if (idr == MethodId::RW_IDENTITY)
+ if (idr == MethodId::RW_EXT_REWRITE)
+ {
+ return d_ext_rewriter.extendedRewrite(n);
+ }
+ if (idr == MethodId::RW_REWRITE_EQ_EXT)
+ {
+ return Rewriter::rewriteEqualityExt(n);
+ }
+ if (idr == MethodId::RW_EVALUATE)
+ {
+ Evaluator eval;
+ return eval.eval(n, {}, {}, false);
+ }
+ if (idr == MethodId::RW_IDENTITY)
{
// does nothing
return n;
{
exp.push_back(children[i]);
}
- Node res = applySubstitution(args[0], exp);
+ Node res = applySubstitution(args[0], exp, ids);
return args[0].eqNode(res);
}
else if (id == PfRule::REWRITE)
Node res = applyRewrite(args[0], idr);
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);
+ return args[0].eqNode(res);
+ }
else if (id == PfRule::MACRO_SR_EQ_INTRO)
{
Assert(1 <= args.size() && args.size() <= 3);
Assert(args.size() == 1);
return RemoveTermFormulas::getAxiomFor(args[0]);
}
- else if (id == PfRule::PREPROCESS || id == PfRule::PREPROCESS_LEMMA
- || id == PfRule::THEORY_PREPROCESS
- || id == PfRule::THEORY_PREPROCESS_LEMMA
- || id == PfRule::WITNESS_AXIOM)
+ else if (id == PfRule::PREPROCESS || id == PfRule::THEORY_PREPROCESS
+ || id == PfRule::WITNESS_AXIOM || id == PfRule::THEORY_LEMMA
+ || id == PfRule::PREPROCESS_LEMMA || id == PfRule::THEORY_REWRITE)
{
+ // "trusted" rules
Assert(children.empty());
- Assert(args.size() == 1);
+ Assert(!args.empty());
+ Assert(args[0].getType().isBoolean());
return args[0];
}
// no rule
}
}
+bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid)
+{
+ uint32_t i;
+ if (!getUInt32(n, i))
+ {
+ return false;
+ }
+ tid = static_cast<TheoryId>(i);
+ return true;
+}
+
+Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
+{
+ return NodeManager::currentNM()->mkConst(
+ Rational(static_cast<uint32_t>(tid)));
+}
+
} // namespace builtin
} // namespace theory
} // namespace CVC4
#include "expr/node.h"
#include "expr/proof_checker.h"
#include "expr/proof_node.h"
+#include "theory/quantifiers/extended_rewrite.h"
namespace CVC4 {
namespace theory {
-/**
+/**
* Identifiers for rewriters and substitutions, which we abstractly
* classify as "methods". Methods have a unique identifier in the internal
* proof calculus implemented by the checker below.
//---------------------------- Rewriters
// Rewriter::rewrite(n)
RW_REWRITE,
+ // d_ext_rew.extendedRewrite(n);
+ RW_EXT_REWRITE,
+ // Rewriter::rewriteExtEquality(n)
+ RW_REWRITE_EQ_EXT,
+ // Evaluator::evaluate(n)
+ RW_EVALUATE,
// identity
RW_IDENTITY,
//---------------------------- Substitutions
* specifying a call to Rewriter::rewrite.
* @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);
+ Node applyRewrite(Node n, MethodId idr = MethodId::RW_REWRITE);
/**
* Get substitution. Updates vars/subs to the substitution specified by
- * exp (e.g. as an equality) for the substitution method ids.
+ * exp for the substitution method ids.
*/
static bool getSubstitution(Node exp,
TNode& var,
* @param idr The method identifier of the rewriter.
* @return The substituted, rewritten form of n.
*/
- static Node applySubstitutionRewrite(Node n,
- const std::vector<Node>& exp,
- MethodId ids = MethodId::SB_DEFAULT,
- MethodId idr = MethodId::RW_REWRITE);
+ Node applySubstitutionRewrite(Node n,
+ const std::vector<Node>& exp,
+ MethodId ids = MethodId::SB_DEFAULT,
+ MethodId idr = MethodId::RW_REWRITE);
/** get a method identifier from a node, return false if we fail */
static bool getMethodId(TNode n, MethodId& i);
/**
*/
static void addMethodIds(std::vector<Node>& args, MethodId ids, MethodId idr);
+ /** get a TheoryId from a node, return false if we fail */
+ static bool getTheoryId(TNode n, TheoryId& tid);
+ /** Make a TheoryId into a node */
+ static Node mkTheoryIdNode(TheoryId tid);
+
/** Register all rules owned by this rule checker into pc. */
void registerTo(ProofChecker* pc) override;
protected:
Node checkInternal(PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args) override;
+
+ /** extended rewriter object */
+ quantifiers::ExtendedRewriter d_ext_rewriter;
};
} // namespace builtin
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
+#include "theory/builtin/proof_checker.h"
#include "theory/rewriter_tables.h"
#include "theory/theory.h"
#include "util/resource_manager.h"
return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
}
-void Rewriter::setProofChecker(ProofChecker* pc)
+void Rewriter::setProofNodeManager(ProofNodeManager* pnm)
{
// 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()));
+ // the rewriter is staticly determinstic, thus use static cache policy
+ // for the term conversion proof generator
+ d_tpg.reset(new TConvProofGenerator(pnm,
+ nullptr,
+ TConvPolicy::FIXPOINT,
+ TConvCachePolicy::STATIC,
+ "Rewriter::TConvProofGenerator"));
}
}
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 processTrustRewriteResponse(theoryId, tresponse, true, tcpg);
}
return d_theoryRewriters[theoryId]->preRewrite(n);
}
// same as above, for post-rewrite
TrustRewriteResponse tresponse =
d_theoryRewriters[theoryId]->postRewriteWithProof(n);
- return processTrustRewriteResponse(tresponse, false, tcpg);
+ return processTrustRewriteResponse(theoryId, tresponse, false, tcpg);
}
return d_theoryRewriters[theoryId]->postRewrite(n);
}
}
RewriteResponse Rewriter::processTrustRewriteResponse(
+ theory::TheoryId theoryId,
const TrustRewriteResponse& tresponse,
bool isPre,
TConvProofGenerator* tcpg)
ProofGenerator* pg = trn.getGenerator();
if (pg == nullptr)
{
+ Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
// add small step trusted rewrite
NodeManager* nm = NodeManager::currentNM();
tcpg->addRewriteStep(proven[0],
proven[1],
PfRule::THEORY_REWRITE,
{},
- {proven[0], nm->mkConst(isPre)});
+ {proven, tidn, nm->mkConst(isPre)});
}
else
{
/**
* 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.
+ * to setProofNodeManager prior to this call.
*
* @param node The node to rewrite.
* @param elimTheoryRewrite Whether we also want fine-grained proofs for
bool elimTheoryRewrite = false,
bool isExtEq = false);
- /** Set proof checker */
- void setProofChecker(ProofChecker* pc);
+ /** Set proof node manager */
+ void setProofNodeManager(ProofNodeManager* pnm);
/**
* Garbage collects the rewrite caches.
TConvProofGenerator* tcpg = nullptr);
/** processes a trust rewrite response */
RewriteResponse processTrustRewriteResponse(
+ theory::TheoryId theoryId,
const TrustRewriteResponse& tresponse,
bool isPre,
TConvProofGenerator* tcpg);
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
projects / cvc5.git / commitdiff