summaryrefslogtreecommitdiff
path: root/src/theory/builtin
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/builtin')
-rw-r--r--src/theory/builtin/proof_checker.cpp68
-rw-r--r--src/theory/builtin/proof_checker.h40
2 files changed, 73 insertions, 35 deletions
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 7521d116e..cf27b516e 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -16,6 +16,7 @@
#include "expr/skolem_manager.h"
#include "smt/term_formula_removal.h"
+#include "theory/evaluator.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
@@ -29,6 +30,9 @@ const char* toString(MethodId id)
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";
@@ -56,6 +60,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
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);
@@ -63,6 +68,7 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
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);
@@ -70,16 +76,6 @@ void BuiltinProofRuleChecker::registerTo(ProofChecker* pc)
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)
{
@@ -95,7 +91,20 @@ Node BuiltinProofRuleChecker::applyRewrite(Node n, 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;
@@ -228,7 +237,7 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
{
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)
@@ -243,6 +252,13 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
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);
@@ -334,13 +350,14 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id,
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
@@ -390,6 +407,23 @@ void BuiltinProofRuleChecker::addMethodIds(std::vector<Node>& args,
}
}
+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
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 7e46587b7..3251b4e9e 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -20,11 +20,12 @@
#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.
@@ -41,6 +42,12 @@ enum class MethodId : uint32_t
//---------------------------- 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
@@ -75,21 +82,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
* 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,
@@ -123,10 +119,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
* @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);
/**
@@ -144,6 +140,11 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
*/
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:
@@ -151,6 +152,9 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback