From: Andrew Reynolds Date: Thu, 27 May 2021 21:28:58 +0000 (-0500) Subject: Update proof namespaces (#6614) X-Git-Tag: cvc5-1.0.0~1684 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b3de13131d24bf400ba5f36fc234008d950f345;p=cvc5.git Update proof namespaces (#6614) This removes namespace theory from proof utilities, and moves MethodId to its own file in src/proof/. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0bdd1c4fe..5faeddbed 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -155,6 +155,8 @@ libcvc5_add_sources( proof/lazy_proof_chain.h proof/lazy_tree_proof_generator.cpp proof/lazy_tree_proof_generator.h + proof/method_id.cpp + proof/method_id.h proof/proof.cpp proof/proof.h proof/proof_checker.cpp diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 5542cfcf3..665415772 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -82,9 +82,9 @@ void AssertionPipeline::push_back(Node n, } } -void AssertionPipeline::pushBackTrusted(theory::TrustNode trn) +void AssertionPipeline::pushBackTrusted(TrustNode trn) { - Assert(trn.getKind() == theory::TrustNodeKind::LEMMA); + Assert(trn.getKind() == TrustNodeKind::LEMMA); // push back what was proven push_back(trn.getProven(), false, false, trn.getGenerator()); } @@ -105,14 +105,14 @@ void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen) d_nodes[i] = n; } -void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn) +void AssertionPipeline::replaceTrusted(size_t i, TrustNode trn) { if (trn.isNull()) { // null trust node denotes no change, nothing to do return; } - Assert(trn.getKind() == theory::TrustNodeKind::REWRITE); + Assert(trn.getKind() == TrustNodeKind::REWRITE); Assert(trn.getProven()[0] == d_nodes[i]); replace(i, trn.getNode(), trn.getGenerator()); } diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h index af88d5164..b6bd8a94c 100644 --- a/src/preprocessing/assertion_pipeline.h +++ b/src/preprocessing/assertion_pipeline.h @@ -72,7 +72,7 @@ class AssertionPipeline bool isInput = false, ProofGenerator* pg = nullptr); /** Same as above, with TrustNode */ - void pushBackTrusted(theory::TrustNode trn); + void pushBackTrusted(TrustNode trn); /** * Get the constant reference to the underlying assertions. It is only @@ -97,7 +97,7 @@ class AssertionPipeline * Same as above, with TrustNode trn, which is of kind REWRITE and proves * d_nodes[i] = n for some n. */ - void replaceTrusted(size_t i, theory::TrustNode trn); + void replaceTrusted(size_t i, TrustNode trn); IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; } const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; } diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp index dc47c9c8e..7578bcad6 100644 --- a/src/preprocessing/passes/ite_removal.cpp +++ b/src/preprocessing/passes/ite_removal.cpp @@ -47,7 +47,7 @@ PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions) for (unsigned i = 0, size = assertions->size(); i < size; ++i) { Node assertion = (*assertions)[i]; - std::vector newAsserts; + std::vector newAsserts; std::vector newSkolems; TrustNode trn = pe->removeItes(assertion, newAsserts, newSkolems); if (!trn.isNull()) diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index 921442f0e..b05dbbe1c 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -474,7 +474,7 @@ Node NonClausalSimp::processLearnedLit(Node lit, return lit; } -Node NonClausalSimp::processRewrittenLearnedLit(theory::TrustNode trn) +Node NonClausalSimp::processRewrittenLearnedLit(TrustNode trn) { if (isProofEnabled()) { diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h index de16cc49a..329542f38 100644 --- a/src/preprocessing/passes/non_clausal_simp.h +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -76,7 +76,7 @@ class NonClausalSimp : public PreprocessingPass * This tracks the proof in the learned literal preprocess proof generator * d_llpg below and returns the rewritten learned literal. */ - Node processRewrittenLearnedLit(theory::TrustNode trn); + Node processRewrittenLearnedLit(TrustNode trn); /** Is proof enabled? */ bool isProofEnabled() const; /** The proof node manager */ diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp index 1eb21cd96..641cab162 100644 --- a/src/preprocessing/passes/theory_preprocess.cpp +++ b/src/preprocessing/passes/theory_preprocess.cpp @@ -44,7 +44,7 @@ PreprocessingPassResult TheoryPreprocess::applyInternal( for (unsigned i = 0, size = assertions->size(); i < size; ++i) { Node assertion = (*assertions)[i]; - std::vector newAsserts; + std::vector newAsserts; std::vector newSkolems; TrustNode trn = propEngine->preprocess(assertion, newAsserts, newSkolems); if (!trn.isNull()) diff --git a/src/preprocessing/passes/theory_rewrite_eq.cpp b/src/preprocessing/passes/theory_rewrite_eq.cpp index 44aedc754..93ba2b7cd 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.cpp +++ b/src/preprocessing/passes/theory_rewrite_eq.cpp @@ -45,7 +45,7 @@ PreprocessingPassResult TheoryRewriteEq::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } -theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) +TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) { NodeManager* nm = NodeManager::currentNM(); TheoryEngine* te = d_preprocContext->getTheoryEngine(); @@ -97,7 +97,7 @@ theory::TrustNode TheoryRewriteEq::rewriteAssertion(TNode n) if (ret.getKind() == kind::EQUAL && !ret[0].getType().isBoolean()) { // For example, (= x y) ---> (and (>= x y) (<= x y)) - theory::TrustNode trn = te->ppRewriteEquality(ret); + TrustNode trn = te->ppRewriteEquality(ret); // can make proof producing by using proof generator from trn ret = trn.isNull() ? Node(ret) : trn.getNode(); } diff --git a/src/preprocessing/passes/theory_rewrite_eq.h b/src/preprocessing/passes/theory_rewrite_eq.h index 2312c38ed..73d20f77c 100644 --- a/src/preprocessing/passes/theory_rewrite_eq.h +++ b/src/preprocessing/passes/theory_rewrite_eq.h @@ -47,7 +47,7 @@ class TheoryRewriteEq : public PreprocessingPass * (= x y) ---> (and (>= x y) (<= x y)) * Returns the trust node corresponding to the rewrite. */ - theory::TrustNode rewriteAssertion(TNode assertion); + TrustNode rewriteAssertion(TNode assertion); }; } // namespace passes diff --git a/src/proof/conv_seq_proof_generator.cpp b/src/proof/conv_seq_proof_generator.cpp index 65a7e462b..7b6a06ddd 100644 --- a/src/proof/conv_seq_proof_generator.cpp +++ b/src/proof/conv_seq_proof_generator.cpp @@ -122,13 +122,13 @@ std::shared_ptr TConvSeqProofGenerator::getSubsequenceProofFor( return d_pnm->mkTrans(transChildren, f); } -theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence( +TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence( const std::vector& cterms) { Assert(cterms.size() == d_tconvs.size() + 1); if (cterms[0] == cterms[cterms.size() - 1]) { - return theory::TrustNode::null(); + return TrustNode::null(); } bool useThis = false; ProofGenerator* pg = nullptr; @@ -163,8 +163,7 @@ theory::TrustNode TConvSeqProofGenerator::mkTrustRewriteSequence( } } Assert(pg != nullptr); - return theory::TrustNode::mkTrustRewrite( - cterms[0], cterms[cterms.size() - 1], pg); + return TrustNode::mkTrustRewrite(cterms[0], cterms[cterms.size() - 1], pg); } std::string TConvSeqProofGenerator::identify() const { return d_name; } diff --git a/src/proof/conv_seq_proof_generator.h b/src/proof/conv_seq_proof_generator.h index 8d4417134..ac8663b58 100644 --- a/src/proof/conv_seq_proof_generator.h +++ b/src/proof/conv_seq_proof_generator.h @@ -98,7 +98,7 @@ class TConvSeqProofGenerator : public ProofGenerator * then we return a trust node proving (= d e) with the 2nd component proof * generator, as it alone is capable of proving this equality. */ - theory::TrustNode mkTrustRewriteSequence(const std::vector& cterms); + TrustNode mkTrustRewriteSequence(const std::vector& cterms); protected: using NodeIndexPairHashFunction = diff --git a/src/proof/eager_proof_generator.cpp b/src/proof/eager_proof_generator.cpp index 34ff4fa75..2a86f982c 100644 --- a/src/proof/eager_proof_generator.cpp +++ b/src/proof/eager_proof_generator.cpp @@ -20,7 +20,6 @@ #include "proof/proof_node_manager.h" namespace cvc5 { -namespace theory { EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm, context::Context* c, @@ -155,5 +154,4 @@ TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f) std::string EagerProofGenerator::identify() const { return d_name; } -} // namespace theory } // namespace cvc5 diff --git a/src/proof/eager_proof_generator.h b/src/proof/eager_proof_generator.h index ada48d893..90e2787fd 100644 --- a/src/proof/eager_proof_generator.h +++ b/src/proof/eager_proof_generator.h @@ -29,8 +29,6 @@ namespace cvc5 { class ProofNode; class ProofNodeManager; -namespace theory { - /** * An eager proof generator, with explicit proof caching. * @@ -191,7 +189,6 @@ class EagerProofGenerator : public ProofGenerator NodeProofNodeMap d_proofs; }; -} // namespace theory } // namespace cvc5 #endif /* CVC5__PROOF__PROOF_GENERATOR_H */ diff --git a/src/proof/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp index a50b9efd4..225a6c75c 100644 --- a/src/proof/lazy_tree_proof_generator.cpp +++ b/src/proof/lazy_tree_proof_generator.cpp @@ -23,7 +23,6 @@ #include "proof/proof_node_manager.h" namespace cvc5 { -namespace theory { LazyTreeProofGenerator::LazyTreeProofGenerator(ProofNodeManager* pnm, const std::string& name) @@ -142,5 +141,4 @@ std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg) return os; } -} // namespace theory } // namespace cvc5 diff --git a/src/proof/lazy_tree_proof_generator.h b/src/proof/lazy_tree_proof_generator.h index 8b8d344e9..ff5d0ad2e 100644 --- a/src/proof/lazy_tree_proof_generator.h +++ b/src/proof/lazy_tree_proof_generator.h @@ -25,7 +25,6 @@ #include "proof/proof_node_manager.h" namespace cvc5 { -namespace theory { namespace detail { /** * A single node in the proof tree created by the LazyTreeProofGenerator. @@ -217,7 +216,6 @@ class LazyTreeProofGenerator : public ProofGenerator */ std::ostream& operator<<(std::ostream& os, const LazyTreeProofGenerator& ltpg); -} // namespace theory } // namespace cvc5 #endif diff --git a/src/proof/method_id.cpp b/src/proof/method_id.cpp new file mode 100644 index 000000000..c5e8458cd --- /dev/null +++ b/src/proof/method_id.cpp @@ -0,0 +1,118 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Implementation of method identifier + */ + +#include "proof/method_id.h" + +#include "proof/proof_checker.h" +#include "util/rational.h" + +namespace cvc5 { + +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::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"; + case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL"; + case MethodId::SBA_SIMUL: return "SBA_SIMUL"; + case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT"; + default: return "MethodId::Unknown"; + }; +} + +std::ostream& operator<<(std::ostream& out, MethodId id) +{ + out << toString(id); + return out; +} + +Node mkMethodId(MethodId id) +{ + return NodeManager::currentNM()->mkConst(Rational(static_cast(id))); +} + +bool getMethodId(TNode n, MethodId& i) +{ + uint32_t index; + if (!ProofRuleChecker::getUInt32(n, index)) + { + return false; + } + i = static_cast(index); + return true; +} + +bool getMethodIds(const std::vector& args, + MethodId& ids, + MethodId& ida, + MethodId& idr, + size_t index) +{ + ids = MethodId::SB_DEFAULT; + ida = MethodId::SBA_SEQUENTIAL; + idr = MethodId::RW_REWRITE; + for (size_t offset = 0; offset <= 2; offset++) + { + if (args.size() > index + offset) + { + MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr); + if (!getMethodId(args[index + offset], id)) + { + Trace("builtin-pfcheck") + << "Failed to get id from " << args[index + offset] << std::endl; + return false; + } + } + else + { + break; + } + } + Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / " + << ida << " / " << idr << "\n"; + return true; +} + +void addMethodIds(std::vector& args, + MethodId ids, + MethodId ida, + MethodId idr) +{ + bool ndefRewriter = (idr != MethodId::RW_REWRITE); + bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL); + if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply) + { + args.push_back(mkMethodId(ids)); + } + if (ndefApply || ndefRewriter) + { + args.push_back(mkMethodId(ida)); + } + if (ndefRewriter) + { + args.push_back(mkMethodId(idr)); + } +} + +} // namespace cvc5 diff --git a/src/proof/method_id.h b/src/proof/method_id.h new file mode 100644 index 000000000..b353232f4 --- /dev/null +++ b/src/proof/method_id.h @@ -0,0 +1,109 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Method identifier enumeration + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__METHOD_ID_H +#define CVC5__PROOF__METHOD_ID_H + +#include "expr/node.h" + +namespace cvc5 { + +/** + * 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. + * + * A "rewriter" is abstractly a method from Node to Node, where the output + * is semantically equivalent to the input. The identifiers below list + * various methods that have this contract. This identifier is used + * in a number of the builtin rules. + * + * A substitution is a method for turning a formula into a substitution. + */ +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, + // 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, + // P, (not P) are interpreted as P -> true, P -> false using Node::substitute + SB_LITERAL, + // P is interpreted as P -> true using Node::substitute + SB_FORMULA, + //---------------------------- Substitution applications + // multiple substitutions are applied sequentially + SBA_SEQUENTIAL, + // multiple substitutions are applied simultaneously + SBA_SIMUL, + // multiple substitutions are applied to fix point + SBA_FIXPOINT + // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to + // y gives: + // - f(g(x)) for SBA_SEQUENTIAL + // - f(z) for SBA_SIMUL + // - f(g(u)) for SBA_FIXPOINT + // Notice that SBA_FIXPOINT should provide a terminating rewrite system + // as a substitution, or else non-termination will occur during proof + // checking. +}; +/** Converts a rewriter id to a string. */ +const char* toString(MethodId id); +/** Write a rewriter id to out */ +std::ostream& operator<<(std::ostream& out, MethodId id); +/** Make a method id node */ +Node mkMethodId(MethodId id); + +/** get a method identifier from a node, return false if we fail */ +bool getMethodId(TNode n, MethodId& i); +/** + * Get method identifiers from args starting at the given index. Store their + * values into ids, ida, and idr. This method returns false if args does not + * contain valid method identifiers at position index in args. + */ +bool getMethodIds(const std::vector& args, + MethodId& ids, + MethodId& ida, + MethodId& idr, + size_t index); +/** + * Add method identifiers ids, ida and idr as nodes to args. This does not add + * ids, ida or idr if their values are the default ones. + */ +void addMethodIds(std::vector& args, + MethodId ids, + MethodId ida, + MethodId idr); + +} // namespace cvc5 + +#endif /* CVC5__PROOF__METHOD_ID_H */ diff --git a/src/proof/theory_proof_step_buffer.cpp b/src/proof/theory_proof_step_buffer.cpp index f00c664c8..79e98471d 100644 --- a/src/proof/theory_proof_step_buffer.cpp +++ b/src/proof/theory_proof_step_buffer.cpp @@ -20,7 +20,6 @@ using namespace cvc5::kind; namespace cvc5 { -namespace theory { TheoryProofStepBuffer::TheoryProofStepBuffer(ProofChecker* pc) : ProofStepBuffer(pc) @@ -36,7 +35,7 @@ bool TheoryProofStepBuffer::applyEqIntro(Node src, { std::vector args; args.push_back(src); - builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); + addMethodIds(args, ids, ida, idr); Node res = tryStep(PfRule::MACRO_SR_EQ_INTRO, exp, args); if (res.isNull()) { @@ -73,7 +72,7 @@ bool TheoryProofStepBuffer::applyPredTransform(Node src, // try to prove that tgt rewrites to src children.insert(children.end(), exp.begin(), exp.end()); args.push_back(tgt); - builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); + addMethodIds(args, ids, ida, idr); Node res = tryStep(PfRule::MACRO_SR_PRED_TRANSFORM, children, args); if (res.isNull()) { @@ -93,7 +92,7 @@ bool TheoryProofStepBuffer::applyPredIntro(Node tgt, { std::vector args; args.push_back(tgt); - builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); + addMethodIds(args, ids, ida, idr); Node res = tryStep(PfRule::MACRO_SR_PRED_INTRO, exp, args); if (res.isNull()) { @@ -113,7 +112,7 @@ Node TheoryProofStepBuffer::applyPredElim(Node src, children.push_back(src); children.insert(children.end(), exp.begin(), exp.end()); std::vector args; - builtin::BuiltinProofRuleChecker::addMethodIds(args, ids, ida, idr); + addMethodIds(args, ids, ida, idr); Node srcRew = tryStep(PfRule::MACRO_SR_PRED_ELIM, children, args); if (CDProof::isSame(src, srcRew)) { @@ -236,5 +235,4 @@ Node TheoryProofStepBuffer::elimDoubleNegLit(Node n) return n; } -} // namespace theory } // namespace cvc5 diff --git a/src/proof/theory_proof_step_buffer.h b/src/proof/theory_proof_step_buffer.h index fc2e25e5a..ac58d3718 100644 --- a/src/proof/theory_proof_step_buffer.h +++ b/src/proof/theory_proof_step_buffer.h @@ -25,7 +25,6 @@ #include "theory/builtin/proof_checker.h" namespace cvc5 { -namespace theory { /** * Class used to speculatively try and buffer a set of proof steps before * sending them to a proof object, extended with theory-specfic proof rule @@ -114,7 +113,6 @@ class TheoryProofStepBuffer : public ProofStepBuffer Node elimDoubleNegLit(Node n); }; -} // namespace theory } // namespace cvc5 #endif /* CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H */ diff --git a/src/proof/trust_node.cpp b/src/proof/trust_node.cpp index d99e6de51..6c5de13c7 100644 --- a/src/proof/trust_node.cpp +++ b/src/proof/trust_node.cpp @@ -19,7 +19,6 @@ #include "proof/proof_generator.h" namespace cvc5 { -namespace theory { const char* toString(TrustNodeKind tnk) { @@ -146,5 +145,4 @@ std::ostream& operator<<(std::ostream& out, TrustNode n) return out; } -} // namespace theory } // namespace cvc5 diff --git a/src/proof/trust_node.h b/src/proof/trust_node.h index 200dececd..8971df1d1 100644 --- a/src/proof/trust_node.h +++ b/src/proof/trust_node.h @@ -25,8 +25,6 @@ namespace cvc5 { class ProofGenerator; class ProofNode; -namespace theory { - /** A kind for trust nodes */ enum class TrustNodeKind : uint32_t { @@ -172,7 +170,6 @@ class TrustNode */ std::ostream& operator<<(std::ostream& out, TrustNode n); -} // namespace theory } // namespace cvc5 #endif /* CVC5__PROOF__TRUST_NODE_H */ diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index 6a2430f82..d09854bce 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -515,7 +515,7 @@ void ProofCnfStream::convertAndAssertIte(TNode node, bool negated) } } -void ProofCnfStream::convertPropagation(theory::TrustNode trn) +void ProofCnfStream::convertPropagation(TrustNode trn) { Node proven = trn.getProven(); Trace("cnf") << "ProofCnfStream::convertPropagation: proven explanation" diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index 97abdb077..9972581c0 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -83,7 +83,7 @@ class ProofCnfStream : public ProofGenerator * clause in the SAT solver, as this is handled internally by the SAT * solver. The clausification steps and the generator within the trust node * are saved in d_proof if we are producing proofs in the theory engine. */ - void convertPropagation(theory::TrustNode ttn); + void convertPropagation(TrustNode ttn); /** * Ensure that the given node will have a designated SAT literal that is * definitionally equal to it. The result of this function is that the Node @@ -162,7 +162,7 @@ class ProofCnfStream : public ProofGenerator LazyCDProof d_proof; /** An accumulator of steps that may be applied to normalize the clauses * generated during clausification. */ - theory::TheoryProofStepBuffer d_psb; + TheoryProofStepBuffer d_psb; /** Blocked proofs. * * These are proof nodes added to this class by external generators. */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index bcf75b43a..fe3a5ecff 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -158,18 +158,16 @@ PropEngine::~PropEngine() { delete d_theoryProxy; } -theory::TrustNode PropEngine::preprocess( - TNode node, - std::vector& newLemmas, - std::vector& newSkolems) +TrustNode PropEngine::preprocess(TNode node, + std::vector& newLemmas, + std::vector& newSkolems) { return d_theoryProxy->preprocess(node, newLemmas, newSkolems); } -theory::TrustNode PropEngine::removeItes( - TNode node, - std::vector& newLemmas, - std::vector& newSkolems) +TrustNode PropEngine::removeItes(TNode node, + std::vector& newLemmas, + std::vector& newSkolems) { return d_theoryProxy->removeItes(node, newLemmas, newSkolems); } @@ -205,14 +203,14 @@ void PropEngine::assertInputFormulas( } } -void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) +void PropEngine::assertLemma(TrustNode tlemma, theory::LemmaProperty p) { bool removable = isLemmaPropertyRemovable(p); // call preprocessor - std::vector ppLemmas; + std::vector ppLemmas; std::vector ppSkolems; - theory::TrustNode tplemma = + TrustNode tplemma = d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems); Assert(ppSkolems.size() == ppLemmas.size()); @@ -244,12 +242,11 @@ void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable); } -void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn, - bool removable) +void PropEngine::assertTrustedLemmaInternal(TrustNode trn, bool removable) { Node node = trn.getNode(); Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl; - bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT; + bool negated = trn.getKind() == TrustNodeKind::CONFLICT; Assert( !isProofEnabled() || trn.getGenerator() != nullptr || options::unsatCores() @@ -296,17 +293,16 @@ void PropEngine::assertInternal( } } -void PropEngine::assertLemmasInternal( - theory::TrustNode trn, - const std::vector& ppLemmas, - const std::vector& ppSkolems, - bool removable) +void PropEngine::assertLemmasInternal(TrustNode trn, + const std::vector& ppLemmas, + const std::vector& ppSkolems, + bool removable) { if (!trn.isNull()) { assertTrustedLemmaInternal(trn, removable); } - for (const theory::TrustNode& tnl : ppLemmas) + for (const TrustNode& tnl : ppLemmas) { assertTrustedLemmaInternal(tnl, removable); } @@ -513,11 +509,11 @@ Node PropEngine::ensureLiteral(TNode n) Node PropEngine::getPreprocessedTerm(TNode n) { // must preprocess - std::vector newLemmas; + std::vector newLemmas; std::vector newSkolems; - theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems); + TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems); // send lemmas corresponding to the skolems introduced by preprocessing n - theory::TrustNode trnNull; + TrustNode trnNull; assertLemmasInternal(trnNull, newLemmas, newSkolems, false); return tpn.isNull() ? Node(n) : tpn.getNode(); } diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 8903d4bc3..74da49cf6 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -94,9 +94,9 @@ class PropEngine * @return The (REWRITE) trust node corresponding to rewritten node via * preprocessing. */ - theory::TrustNode preprocess(TNode node, - std::vector& ppLemmas, - std::vector& ppSkolems); + TrustNode preprocess(TNode node, + std::vector& ppLemmas, + std::vector& ppSkolems); /** * Remove term ITEs (and more generally, term formulas) from the given node. * Return the REWRITE trust node corresponding to rewriting node. New lemmas @@ -110,9 +110,9 @@ class PropEngine * @return The (REWRITE) trust node corresponding to rewritten node via * preprocessing. */ - theory::TrustNode removeItes(TNode node, - std::vector& ppLemmas, - std::vector& ppSkolems); + TrustNode removeItes(TNode node, + std::vector& ppLemmas, + std::vector& ppSkolems); /** * Converts the given formulas to CNF and assert the CNF to the SAT solver. @@ -136,7 +136,7 @@ class PropEngine * @param trn the trust node storing the formula to assert * @param p the properties of the lemma */ - void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p); + void assertLemma(TrustNode tlemma, theory::LemmaProperty p); /** * If ever n is decided upon, it must be in the given phase. This @@ -321,7 +321,7 @@ class PropEngine * @param removable whether this lemma can be quietly removed based * on an activity heuristic */ - void assertTrustedLemmaInternal(theory::TrustNode trn, bool removable); + void assertTrustedLemmaInternal(TrustNode trn, bool removable); /** * Assert node as a formula to the CNF stream * @param node The formula to assert @@ -342,8 +342,8 @@ class PropEngine * skolem definitions and skolems obtained from preprocessing it, and * removable is whether the lemma is removable. */ - void assertLemmasInternal(theory::TrustNode trn, - const std::vector& ppLemmas, + void assertLemmasInternal(TrustNode trn, + const std::vector& ppLemmas, const std::vector& ppSkolems, bool removable); diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index b0eab66e9..845289841 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -96,7 +96,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) { TNode lNode = d_cnfStream->getNode(l); Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl; - theory::TrustNode tte = d_theoryEngine->getExplanation(lNode); + TrustNode tte = d_theoryEngine->getExplanation(lNode); Node theoryExplanation = tte.getNode(); if (options::produceProofs() && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS) @@ -184,26 +184,23 @@ SatValue TheoryProxy::getDecisionPolarity(SatVariable var) { CnfStream* TheoryProxy::getCnfStream() { return d_cnfStream; } -theory::TrustNode TheoryProxy::preprocessLemma( - theory::TrustNode trn, - std::vector& newLemmas, - std::vector& newSkolems) +TrustNode TheoryProxy::preprocessLemma(TrustNode trn, + std::vector& newLemmas, + std::vector& newSkolems) { return d_tpp.preprocessLemma(trn, newLemmas, newSkolems); } -theory::TrustNode TheoryProxy::preprocess( - TNode node, - std::vector& newLemmas, - std::vector& newSkolems) +TrustNode TheoryProxy::preprocess(TNode node, + std::vector& newLemmas, + std::vector& newSkolems) { return d_tpp.preprocess(node, newLemmas, newSkolems); } -theory::TrustNode TheoryProxy::removeItes( - TNode node, - std::vector& newLemmas, - std::vector& newSkolems) +TrustNode TheoryProxy::removeItes(TNode node, + std::vector& newLemmas, + std::vector& newSkolems) { RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas(); return rtf.run(node, newLemmas, newSkolems, true); diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index d6ae1f975..f988c00e2 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -105,22 +105,22 @@ class TheoryProxy : public Registrar * Call the preprocessor on node, return trust node corresponding to the * rewrite. */ - theory::TrustNode preprocessLemma(theory::TrustNode trn, - std::vector& newLemmas, - std::vector& newSkolems); + TrustNode preprocessLemma(TrustNode trn, + std::vector& newLemmas, + std::vector& newSkolems); /** * Call the preprocessor on node, return trust node corresponding to the * rewrite. */ - theory::TrustNode preprocess(TNode node, - std::vector& newLemmas, - std::vector& newSkolems); + TrustNode preprocess(TNode node, + std::vector& newLemmas, + std::vector& newSkolems); /** * Remove ITEs from the node. */ - theory::TrustNode removeItes(TNode node, - std::vector& newLemmas, - std::vector& newSkolems); + TrustNode removeItes(TNode node, + std::vector& newLemmas, + std::vector& newSkolems); /** * Get the skolems within node and their corresponding definitions, store * them in sks and skAsserts respectively. Note that this method does not diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h index ba89a1063..997e97391 100644 --- a/src/smt/expand_definitions.h +++ b/src/smt/expand_definitions.h @@ -64,9 +64,9 @@ class ExpandDefs * Helper function for above, called to specify if we want proof production * based on the optional argument tpg. */ - theory::TrustNode expandDefinitions(TNode n, - std::unordered_map& cache, - TConvProofGenerator* tpg); + TrustNode expandDefinitions(TNode n, + std::unordered_map& cache, + TConvProofGenerator* tpg); /** Reference to the environment. */ Env& d_env; /** Reference to the SMT stats */ diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp index 3f657db63..12a802f14 100644 --- a/src/smt/preprocess_proof_generator.cpp +++ b/src/smt/preprocess_proof_generator.cpp @@ -59,7 +59,7 @@ void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) { checkEagerPedantic(d_ra); } - d_src[n] = theory::TrustNode::mkTrustLemma(n, pg); + d_src[n] = TrustNode::mkTrustLemma(n, pg); } else { @@ -67,7 +67,7 @@ void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg) } } -void PreprocessProofGenerator::notifyNewTrustedAssert(theory::TrustNode tn) +void PreprocessProofGenerator::notifyNewTrustedAssert(TrustNode tn) { notifyNewAssert(tn.getProven(), tn.getGenerator()); } @@ -82,17 +82,17 @@ void PreprocessProofGenerator::notifyPreprocessed(Node n, return; } // call the trusted version - notifyTrustedPreprocessed(theory::TrustNode::mkTrustRewrite(n, np, pg)); + notifyTrustedPreprocessed(TrustNode::mkTrustRewrite(n, np, pg)); } -void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp) +void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp) { if (tnp.isNull()) { // no rewrite, nothing to do return; } - Assert(tnp.getKind() == theory::TrustNodeKind::REWRITE); + Assert(tnp.getKind() == TrustNodeKind::REWRITE); Node np = tnp.getNode(); Trace("smt-proof-pp-debug") << "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven() @@ -161,8 +161,8 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) } Trace("smt-pppg") << "...update" << std::endl; - theory::TrustNodeKind tnk = (*it).second.getKind(); - if (tnk == theory::TrustNodeKind::REWRITE) + TrustNodeKind tnk = (*it).second.getKind(); + if (tnk == TrustNodeKind::REWRITE) { Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl; Assert(proven.getKind() == kind::EQUAL); @@ -185,17 +185,15 @@ std::shared_ptr PreprocessProofGenerator::getProofFor(Node f) else { Trace("smt-pppg") << "...lemma" << std::endl; - Assert(tnk == theory::TrustNodeKind::LEMMA); + Assert(tnk == TrustNodeKind::LEMMA); } if (!proofStepProcessed) { Trace("smt-pppg") << "...add missing step" << std::endl; // add trusted step, the rule depends on the kind of trust node - cdp.addStep(proven, - tnk == theory::TrustNodeKind::LEMMA ? d_ra : d_rpp, - {}, - {proven}); + cdp.addStep( + proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven}); } } } while (success); diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h index 347f4af3b..a0e88b3e9 100644 --- a/src/smt/preprocess_proof_generator.h +++ b/src/smt/preprocess_proof_generator.h @@ -55,7 +55,7 @@ namespace smt { */ class PreprocessProofGenerator : public ProofGenerator { - typedef context::CDHashMap NodeTrustNodeMap; + typedef context::CDHashMap NodeTrustNodeMap; public: /** @@ -82,14 +82,14 @@ class PreprocessProofGenerator : public ProofGenerator */ void notifyNewAssert(Node n, ProofGenerator* pg); /** Notify a new assertion, trust node version. */ - void notifyNewTrustedAssert(theory::TrustNode tn); + void notifyNewTrustedAssert(TrustNode tn); /** * Notify that n was replaced by np due to preprocessing, where pg can * provide a proof of the equality n=np. */ void notifyPreprocessed(Node n, Node np, ProofGenerator* pg); /** Notify preprocessed, trust node version */ - void notifyTrustedPreprocessed(theory::TrustNode tnp); + void notifyTrustedPreprocessed(TrustNode tnp); /** * Get proof for f, which returns a proof based on proving an equality based * on transitivity of preprocessing steps, and then using the original diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 7176126fb..6498fa84f 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -431,7 +431,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, MethodId ids = MethodId::SB_DEFAULT; if (args.size() >= 2) { - if (builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids)) + if (getMethodId(args[1], ids)) { sargs.push_back(args[1]); } @@ -439,7 +439,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, MethodId ida = MethodId::SBA_SEQUENTIAL; if (args.size() >= 3) { - if (builtin::BuiltinProofRuleChecker::getMethodId(args[2], ida)) + if (getMethodId(args[2], ida)) { sargs.push_back(args[2]); } @@ -471,7 +471,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, MethodId idr = MethodId::RW_REWRITE; if (args.size() >= 4) { - if (builtin::BuiltinProofRuleChecker::getMethodId(args[3], idr)) + if (getMethodId(args[3], idr)) { rargs.push_back(args[3]); } @@ -804,12 +804,12 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, MethodId ids = MethodId::SB_DEFAULT; if (args.size() >= 2) { - builtin::BuiltinProofRuleChecker::getMethodId(args[1], ids); + getMethodId(args[1], ids); } MethodId ida = MethodId::SBA_SEQUENTIAL; if (args.size() >= 3) { - builtin::BuiltinProofRuleChecker::getMethodId(args[2], ida); + getMethodId(args[2], ida); } std::vector> pfs; std::vector vsList; @@ -950,7 +950,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, MethodId idr = MethodId::RW_REWRITE; if (args.size() >= 2) { - builtin::BuiltinProofRuleChecker::getMethodId(args[1], idr); + getMethodId(args[1], idr); } builtin::BuiltinProofRuleChecker* builtinPfC = static_cast( diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 3bb998688..692b7c889 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -53,17 +53,16 @@ RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u, RemoveTermFormulas::~RemoveTermFormulas() {} -theory::TrustNode RemoveTermFormulas::run( - TNode assertion, - std::vector& newAsserts, - std::vector& newSkolems, - bool fixedPoint) +TrustNode RemoveTermFormulas::run(TNode assertion, + std::vector& newAsserts, + std::vector& newSkolems, + bool fixedPoint) { Node itesRemoved = runInternal(assertion, newAsserts, newSkolems); Assert(newAsserts.size() == newSkolems.size()); if (itesRemoved == assertion) { - return theory::TrustNode::null(); + return TrustNode::null(); } // if running to fixed point, we run each new assertion through the // run lemma method @@ -72,7 +71,7 @@ theory::TrustNode RemoveTermFormulas::run( size_t i = 0; while (i < newAsserts.size()) { - theory::TrustNode trn = newAsserts[i]; + TrustNode trn = newAsserts[i]; // do not run to fixed point on subcall, since we are processing all // lemmas in this loop newAsserts[i] = runLemma(trn, newAsserts, newSkolems, false); @@ -81,35 +80,33 @@ theory::TrustNode RemoveTermFormulas::run( } // The rewriting of assertion can be justified by the term conversion proof // generator d_tpg. - return theory::TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get()); + return TrustNode::mkTrustRewrite(assertion, itesRemoved, d_tpg.get()); } -theory::TrustNode RemoveTermFormulas::run(TNode assertion) +TrustNode RemoveTermFormulas::run(TNode assertion) { - std::vector newAsserts; + std::vector newAsserts; std::vector newSkolems; return run(assertion, newAsserts, newSkolems, false); } -theory::TrustNode RemoveTermFormulas::runLemma( - theory::TrustNode lem, - std::vector& newAsserts, - std::vector& newSkolems, - bool fixedPoint) +TrustNode RemoveTermFormulas::runLemma(TrustNode lem, + std::vector& newAsserts, + std::vector& newSkolems, + bool fixedPoint) { - theory::TrustNode trn = - run(lem.getProven(), newAsserts, newSkolems, fixedPoint); + TrustNode trn = run(lem.getProven(), newAsserts, newSkolems, fixedPoint); if (trn.isNull()) { // no change return lem; } - Assert(trn.getKind() == theory::TrustNodeKind::REWRITE); + Assert(trn.getKind() == TrustNodeKind::REWRITE); Node newAssertion = trn.getNode(); if (!isProofEnabled()) { // proofs not enabled, just take result - return theory::TrustNode::mkTrustLemma(newAssertion, nullptr); + return TrustNode::mkTrustLemma(newAssertion, nullptr); } Trace("rtf-proof-debug") << "RemoveTermFormulas::run: setup proof for processed new lemma" @@ -128,11 +125,11 @@ theory::TrustNode RemoveTermFormulas::runLemma( // ------------------------------------------------------- EQ_RESOLVE // newAssertion d_lp->addStep(newAssertion, PfRule::EQ_RESOLVE, {assertionPre, naEq}, {}); - return theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get()); + return TrustNode::mkTrustLemma(newAssertion, d_lp.get()); } Node RemoveTermFormulas::runInternal(TNode assertion, - std::vector& output, + std::vector& output, std::vector& newSkolems) { NodeManager* nm = NodeManager::currentNM(); @@ -164,7 +161,7 @@ Node RemoveTermFormulas::runInternal(TNode assertion, if (!processedChildren.back()) { // check if we should replace the current node - theory::TrustNode newLem; + TrustNode newLem; Node currt = runCurrent(curr, newLem); // if we replaced by a skolem, we do not recurse if (!currt.isNull()) @@ -251,7 +248,7 @@ Node RemoveTermFormulas::runInternal(TNode assertion, } Node RemoveTermFormulas::runCurrent(std::pair& curr, - theory::TrustNode& newLem) + TrustNode& newLem) { TNode node = curr.first; uint32_t cval = curr.second; @@ -498,7 +495,7 @@ Node RemoveTermFormulas::runCurrent(std::pair& curr, Trace("rtf-debug") << "*** term formula removal introduced " << skolem << " for " << node << std::endl; - newLem = theory::TrustNode::mkTrustLemma(newAssertion, d_lp.get()); + newLem = TrustNode::mkTrustLemma(newAssertion, d_lp.get()); Trace("rtf-proof-debug") << "Checking closed..." << std::endl; newLem.debugCheckClosed("rtf-proof-debug", diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index c2b1f27f3..6f27b9462 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -88,24 +88,24 @@ class RemoveTermFormulas { * right hand side is assertion after removing term formulas, and the proof * generator (if provided) that can prove the equivalence. */ - theory::TrustNode run(TNode assertion, - std::vector& newAsserts, - std::vector& newSkolems, - bool fixedPoint = false); + TrustNode run(TNode assertion, + std::vector& newAsserts, + std::vector& newSkolems, + bool fixedPoint = false); /** * Same as above, but does not track lemmas, and does not run to fixed point. * The relevant lemmas can be extracted by the caller later using getSkolems * and getLemmaForSkolem. */ - theory::TrustNode run(TNode assertion); + TrustNode run(TNode assertion); /** * Same as above, but transforms a lemma, returning a LEMMA trust node that * proves the same formula as lem with term formulas removed. */ - theory::TrustNode runLemma(theory::TrustNode lem, - std::vector& newAsserts, - std::vector& newSkolems, - bool fixedPoint = false); + TrustNode runLemma(TrustNode lem, + std::vector& newAsserts, + std::vector& newSkolems, + bool fixedPoint = false); /** * Get proof generator that is responsible for all proofs for removing term @@ -190,7 +190,7 @@ class RemoveTermFormulas { * the version of assertion with all term formulas removed. */ Node runInternal(TNode assertion, - std::vector& newAsserts, + std::vector& newAsserts, std::vector& newSkolems); /** * This is called on curr of the form (t, val) where t is a term and val is @@ -202,7 +202,7 @@ class RemoveTermFormulas { * Otherwise, if t should not be replaced in the term context, this method * returns the null node. */ - Node runCurrent(std::pair& curr, theory::TrustNode& newLem); + Node runCurrent(std::pair& curr, TrustNode& newLem); /** Whether proofs are enabled */ bool isProofEnabled() const; diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 8ada48cfe..4ab0b313b 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -36,6 +36,7 @@ namespace cvc5 { class ProofNodeManager; +class EagerProofGenerator; namespace context { class Context; @@ -43,8 +44,6 @@ class UserContext; } namespace theory { - -class EagerProofGenerator; struct EeSetupInfo; namespace eq { diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index fce071e6e..f6306049b 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -97,14 +97,13 @@ namespace cvc5 { class ProofNodeManager; +class EagerProofGenerator; namespace context { class Context; } namespace theory { -class EagerProofGenerator; - namespace arith { class Comparison; diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index e3094ae88..b25fa4f69 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -56,9 +56,11 @@ #include "util/statistics_stats.h" namespace cvc5 { -namespace theory { class EagerProofGenerator; + +namespace theory { + class TheoryModel; namespace arith { diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 74e1a7cd8..d01ec081e 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -34,11 +34,9 @@ namespace cvc5 { class ProofGenerator; class ProofNode; - -namespace theory { - class EagerProofGenerator; +namespace theory { namespace booleans { /** diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 9dfc9418f..7ec0525c9 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -26,39 +26,6 @@ using namespace cvc5::kind; namespace cvc5 { namespace theory { - -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::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"; - case MethodId::SBA_SEQUENTIAL: return "SBA_SEQUENTIAL"; - case MethodId::SBA_SIMUL: return "SBA_SIMUL"; - case MethodId::SBA_FIXPOINT: return "SBA_FIXPOINT"; - default: return "MethodId::Unknown"; - }; -} - -std::ostream& operator<<(std::ostream& out, MethodId id) -{ - out << toString(id); - return out; -} - -Node mkMethodId(MethodId id) -{ - return NodeManager::currentNM()->mkConst(Rational(static_cast(id))); -} - namespace builtin { void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) @@ -250,17 +217,6 @@ Node BuiltinProofRuleChecker::applySubstitution(Node n, return ns; } -bool BuiltinProofRuleChecker::getMethodId(TNode n, MethodId& i) -{ - uint32_t index; - if (!getUInt32(n, index)) - { - return false; - } - i = static_cast(index); - return true; -} - Node BuiltinProofRuleChecker::checkInternal(PfRule id, const std::vector& children, const std::vector& args) @@ -455,58 +411,6 @@ Node BuiltinProofRuleChecker::checkInternal(PfRule id, return Node::null(); } -bool BuiltinProofRuleChecker::getMethodIds(const std::vector& args, - MethodId& ids, - MethodId& ida, - MethodId& idr, - size_t index) -{ - ids = MethodId::SB_DEFAULT; - ida = MethodId::SBA_SEQUENTIAL; - idr = MethodId::RW_REWRITE; - for (size_t offset = 0; offset <= 2; offset++) - { - if (args.size() > index + offset) - { - MethodId& id = offset == 0 ? ids : (offset == 1 ? ida : idr); - if (!getMethodId(args[index + offset], id)) - { - Trace("builtin-pfcheck") - << "Failed to get id from " << args[index + offset] << std::endl; - return false; - } - } - else - { - break; - } - } - Trace("builtin-pfcheck") << "Got MethodIds ids/ida/idr: " << ids << " / " - << ida << " / " << idr << "\n"; - return true; -} - -void BuiltinProofRuleChecker::addMethodIds(std::vector& args, - MethodId ids, - MethodId ida, - MethodId idr) -{ - bool ndefRewriter = (idr != MethodId::RW_REWRITE); - bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL); - if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply) - { - args.push_back(mkMethodId(ids)); - } - if (ndefApply || ndefRewriter) - { - args.push_back(mkMethodId(ida)); - } - if (ndefRewriter) - { - args.push_back(mkMethodId(idr)); - } -} - bool BuiltinProofRuleChecker::getTheoryId(TNode n, TheoryId& tid) { uint32_t i; diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 892fc7a4b..1e671a7b3 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Equality proof checker utility. + * Builtin proof checker utility. */ #include "cvc5_private.h" @@ -19,74 +19,13 @@ #define CVC5__THEORY__BUILTIN__PROOF_CHECKER_H #include "expr/node.h" +#include "proof/method_id.h" #include "proof/proof_checker.h" #include "proof/proof_node.h" #include "theory/quantifiers/extended_rewrite.h" namespace cvc5 { 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. - * - * A "rewriter" is abstractly a method from Node to Node, where the output - * is semantically equivalent to the input. The identifiers below list - * various methods that have this contract. This identifier is used - * in a number of the builtin rules. - * - * A substitution is a method for turning a formula into a substitution. - */ -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, - // 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, - // P, (not P) are interpreted as P -> true, P -> false using Node::substitute - SB_LITERAL, - // P is interpreted as P -> true using Node::substitute - SB_FORMULA, - //---------------------------- Substitution applications - // multiple substitutions are applied sequentially - SBA_SEQUENTIAL, - // multiple substitutions are applied simultaneously - SBA_SIMUL, - // multiple substitutions are applied to fix point - SBA_FIXPOINT - // For example, for x -> u, y -> f(z), z -> g(x), applying this substituion to - // y gives: - // - f(g(x)) for SBA_SEQUENTIAL - // - f(z) for SBA_SIMUL - // - f(g(u)) for SBA_FIXPOINT - // Notice that SBA_FIXPOINT should provide a terminating rewrite system - // as a substitution, or else non-termination will occur during proof - // checking. -}; -/** Converts a rewriter id to a string. */ -const char* toString(MethodId id); -/** Write a rewriter id to out */ -std::ostream& operator<<(std::ostream& out, MethodId id); -/** Make a method id node */ -Node mkMethodId(MethodId id); - namespace builtin { /** A checker for builtin proofs */ @@ -166,26 +105,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker MethodId ids = MethodId::SB_DEFAULT, MethodId ida = MethodId::SBA_SEQUENTIAL, MethodId idr = MethodId::RW_REWRITE); - /** get a method identifier from a node, return false if we fail */ - static bool getMethodId(TNode n, MethodId& i); - /** - * Get method identifiers from args starting at the given index. Store their - * values into ids, ida, and idr. This method returns false if args does not - * contain valid method identifiers at position index in args. - */ - bool getMethodIds(const std::vector& args, - MethodId& ids, - MethodId& ida, - MethodId& idr, - size_t index); - /** - * Add method identifiers ids, ida and idr as nodes to args. This does not add - * ids, ida or idr if their values are the default ones. - */ - static void addMethodIds(std::vector& args, - MethodId ids, - MethodId ida, - MethodId idr); /** get a TheoryId from a node, return false if we fail */ static bool getTheoryId(TNode n, TheoryId& tid); diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 063cefd49..6417b501e 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -28,10 +28,10 @@ namespace cvc5 { class TheoryEngine; class Env; +class EagerProofGenerator; namespace theory { -class EagerProofGenerator; class ModelManager; class SharedSolver; diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index 2642ae0c5..019efa950 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -23,10 +23,10 @@ #include "theory/inference_manager_buffered.h" namespace cvc5 { -namespace theory { class EagerProofGenerator; +namespace theory { namespace datatypes { /** diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 1fc685992..3201bb2c8 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -24,11 +24,10 @@ namespace cvc5 { class TConvProofGenerator; class ProofNodeManager; +class TrustNode; namespace theory { -class TrustNode; - namespace builtin { class BuiltinProofRuleChecker; } diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp index b9c331acc..0e17f50a9 100644 --- a/src/theory/shared_terms_database.cpp +++ b/src/theory/shared_terms_database.cpp @@ -300,7 +300,7 @@ bool SharedTermsDatabase::isKnown(TNode literal) const { } } -theory::TrustNode SharedTermsDatabase::explain(TNode literal) const +TrustNode SharedTermsDatabase::explain(TNode literal) const { if (d_pfee != nullptr) { diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h index b684ff56f..4e09ac23f 100644 --- a/src/theory/shared_terms_database.h +++ b/src/theory/shared_terms_database.h @@ -186,7 +186,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj { /** * Returns an explanation of the propagation that came from the database. */ - theory::TrustNode explain(TNode literal) const; + TrustNode explain(TNode literal) const; /** * Add an equality to propagate. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 676351dd5..85cd7e6b3 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -810,7 +810,7 @@ theory::Theory::PPAssertStatus TheoryEngine::solve( return solveStatus; } -theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq) +TrustNode TheoryEngine::ppRewriteEquality(TNode eq) { Assert(eq.getKind() == kind::EQUAL); std::vector lems; @@ -1297,7 +1297,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector& atoms, theory::The } } -void TheoryEngine::lemma(theory::TrustNode tlemma, +void TheoryEngine::lemma(TrustNode tlemma, theory::LemmaProperty p, theory::TheoryId atomsTo, theory::TheoryId from) @@ -1368,7 +1368,7 @@ void TheoryEngine::lemma(theory::TrustNode tlemma, d_lemmasAdded = true; } -void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId) +void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) { Assert(tconflict.getKind() == TrustNodeKind::CONFLICT); TNode conflict = tconflict.getNode(); @@ -1486,7 +1486,7 @@ void TheoryEngine::setIncomplete(theory::TheoryId theory, d_incompleteId = id; } -theory::TrustNode TheoryEngine::getExplanation( +TrustNode TheoryEngine::getExplanation( std::vector& explanationVector) { Assert(explanationVector.size() == 1); @@ -1788,7 +1788,7 @@ theory::TrustNode TheoryEngine::getExplanation( return trn; } - return theory::TrustNode::mkTrustPropExp(conclusion, expNode, nullptr); + return TrustNode::mkTrustPropExp(conclusion, expNode, nullptr); } bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ffcaf392f..f293a2cc8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -191,7 +191,7 @@ class TheoryEngine { * generator (if it exists), * @param theoryId The theory that sent the conflict */ - void conflict(theory::TrustNode conflict, theory::TheoryId theoryId); + void conflict(TrustNode conflict, theory::TheoryId theoryId); /** * Debugging flag to ensure that shutdown() is called before the @@ -272,7 +272,7 @@ class TheoryEngine { * @param atomsTo the theory that atoms of the lemma should be sent to * @param from the theory that sent the lemma */ - void lemma(theory::TrustNode node, + void lemma(TrustNode node, theory::LemmaProperty p, theory::TheoryId atomsTo = theory::THEORY_LAST, theory::TheoryId from = theory::THEORY_LAST); @@ -422,8 +422,7 @@ class TheoryEngine { * where the node is the one to be explained, and the theory is the * theory that sent the literal. */ - theory::TrustNode getExplanation( - std::vector& explanationVector); + TrustNode getExplanation(std::vector& explanationVector); /** Are proofs enabled? */ bool isProofEnabled() const; @@ -433,7 +432,7 @@ class TheoryEngine { * Preprocess rewrite equality, called by the preprocessor to rewrite * equalities appearing in the input. */ - theory::TrustNode ppRewriteEquality(TNode eq); + TrustNode ppRewriteEquality(TNode eq); /** Notify (preprocessed) assertions. */ void notifyPreprocessedAssertions(const std::vector& assertions); @@ -477,8 +476,7 @@ class TheoryEngine { * take this proof into account (when proofs are enabled). */ theory::Theory::PPAssertStatus solve( - theory::TrustNode tliteral, - theory::TrustSubstitutionMap& substitutionOut); + TrustNode tliteral, theory::TrustSubstitutionMap& substitutionOut); /** * Preregister a Theory atom with the responsible theory (or @@ -540,7 +538,7 @@ class TheoryEngine { /** * Returns an explanation of the node propagated to the SAT solver. */ - theory::TrustNode getExplanation(TNode node); + TrustNode getExplanation(TNode node); /** * Get the pointer to the model object used by this theory engine. diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index f10716bd9..073accdae 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -30,21 +30,21 @@ TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm, d_false = NodeManager::currentNM()->mkConst(false); } -theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain( +TrustNode TheoryEngineProofGenerator::mkTrustExplain( TNode lit, Node exp, std::shared_ptr lpf) { Node p; - theory::TrustNode trn; + TrustNode trn; if (lit == d_false) { // propagation of false is a conflict - trn = theory::TrustNode::mkTrustConflict(exp, this); + trn = TrustNode::mkTrustConflict(exp, this); p = trn.getProven(); Assert(p.getKind() == NOT); } else { - trn = theory::TrustNode::mkTrustPropExp(lit, exp, this); + trn = TrustNode::mkTrustPropExp(lit, exp, this); p = trn.getProven(); Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2); } diff --git a/src/theory/theory_engine_proof_generator.h b/src/theory/theory_engine_proof_generator.h index ab0f616fe..68f7dea32 100644 --- a/src/theory/theory_engine_proof_generator.h +++ b/src/theory/theory_engine_proof_generator.h @@ -53,9 +53,9 @@ class TheoryEngineProofGenerator : public ProofGenerator * explanation already exists, then the previous explanation is taken, which * also suffices for proving the implication. */ - theory::TrustNode mkTrustExplain(TNode lit, - Node exp, - std::shared_ptr lpf); + TrustNode mkTrustExplain(TNode lit, + Node exp, + std::shared_ptr lpf); /** * Get proof for, which expects implications corresponding to explained * propagations (=> exp lit) registered by the above method. This currently diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index a81deabc2..672693366 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -115,10 +115,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel void safePoint(Resource r) override {} void conflict(TNode n) override { push(CONFLICT, n); } - void trustedConflict(theory::TrustNode n) override - { - push(CONFLICT, n.getNode()); - } + void trustedConflict(TrustNode n) override { push(CONFLICT, n.getNode()); } bool propagate(TNode n) override { @@ -132,7 +129,7 @@ class DummyOutputChannel : public cvc5::theory::OutputChannel push(LEMMA, n); } - void trustedLemma(theory::TrustNode n, theory::LemmaProperty p) override + void trustedLemma(TrustNode n, theory::LemmaProperty p) override { push(LEMMA, n.getNode()); } @@ -250,10 +247,7 @@ class DummyTheory : public theory::Theory // do not assert to equality engine, since this theory does not use one return true; } - theory::TrustNode explain(TNode n) override - { - return theory::TrustNode::null(); - } + TrustNode explain(TNode n) override { return TrustNode::null(); } Node getValue(TNode n) { return Node::null(); } std::string identify() const override { return "DummyTheory" + d_id; }