diff options
Diffstat (limited to 'src/expr/proof.cpp')
| -rw-r--r-- | src/expr/proof.cpp | 16 |
1 files changed, 3 insertions, 13 deletions
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 1c879ef0b..20e8e29e2 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -18,18 +18,6 @@ using namespace CVC4::kind; namespace CVC4 { -std::ostream& operator<<(std::ostream& out, CDPOverwrite opol) -{ - switch (opol) - { - case CDPOverwrite::ALWAYS: out << "ALWAYS"; break; - case CDPOverwrite::ASSUME_ONLY: out << "ASSUME_ONLY"; break; - case CDPOverwrite::NEVER: out << "NEVER"; break; - default: out << "CDPOverwrite:unknown"; break; - } - return out; -} - CDProof::CDProof(ProofNodeManager* pnm, context::Context* c) : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context) { @@ -37,7 +25,7 @@ CDProof::CDProof(ProofNodeManager* pnm, context::Context* c) CDProof::~CDProof() {} -std::shared_ptr<ProofNode> CDProof::mkProof(Node fact) +std::shared_ptr<ProofNode> CDProof::getProofFor(Node fact) { std::shared_ptr<ProofNode> pf = getProofSymm(fact); if (pf != nullptr) @@ -436,4 +424,6 @@ Node CDProof::getSymmFact(TNode f) return polarity ? symFact : symFact.notNode(); } +std::string CDProof::identify() const { return "CDProof"; } + } // namespace CVC4 |