diff options
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/proof_checker.cpp | 68 | ||||
-rw-r--r-- | src/theory/builtin/proof_checker.h | 40 |
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 |