From 8ad308b23c705e73507a42d2425289e999d47f86 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 1 Sep 2020 19:08:23 -0300 Subject: Removes old proof code (#4964) This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure. It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver). --- src/theory/output_channel.cpp | 5 ----- 1 file changed, 5 deletions(-) (limited to 'src/theory/output_channel.cpp') diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp index c918438ee..ad60dbe0e 100644 --- a/src/theory/output_channel.cpp +++ b/src/theory/output_channel.cpp @@ -93,11 +93,6 @@ TNode LemmaStatus::getRewrittenLemma() const { return d_rewrittenLemma; } unsigned LemmaStatus::getLevel() const { return d_level; } -LemmaStatus OutputChannel::lemma(TNode n, LemmaProperty p) -{ - return lemma(n, RULE_INVALID, p); -} - LemmaStatus OutputChannel::split(TNode n) { return splitLemma(n.orNode(n.notNode())); -- cgit v1.2.3