Simplify lemma interface (#5819)

This makes it so that TheoryEngine::lemma returns void not LemmaStatus.

Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions.

It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.

1 files changed, 2 insertions, 14 deletions

diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp
index 91f30514c..e63b78486 100644
--- a/src/theory/output_channel.cpp
+++ b/src/theory/output_channel.cpp
@@ -84,19 +84,7 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p)
   return out;
 }
 
-LemmaStatus::LemmaStatus(TNode rewrittenLemma, unsigned level)
-    : d_rewrittenLemma(rewrittenLemma), d_level(level)
-{
-}
-
-TNode LemmaStatus::getRewrittenLemma() const { return d_rewrittenLemma; }
-
-unsigned LemmaStatus::getLevel() const { return d_level; }
-
-LemmaStatus OutputChannel::split(TNode n)
-{
-  return splitLemma(n.orNode(n.notNode()));
-}
+void OutputChannel::split(TNode n) { splitLemma(n.orNode(n.notNode())); }
 
 void OutputChannel::trustedConflict(TrustNode pconf)
 {
@@ -104,7 +92,7 @@ void OutputChannel::trustedConflict(TrustNode pconf)
                 << std::endl;
 }
 
-LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
+void OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
 {
   Unreachable() << "OutputChannel::trustedLemma: no implementation"
                 << std::endl;