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, 7 deletions

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 9f23dbad6..4b6c1a064 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -54,17 +54,12 @@ class TestOutputChannel : public OutputChannel {
     return true;
   }
 
-  LemmaStatus lemma(TNode n,
-                    LemmaProperty p = LemmaProperty::NONE) override
+  void lemma(TNode n, LemmaProperty p = LemmaProperty::NONE) override
   {
     push(LEMMA, n);
-    return LemmaStatus(Node::null(), 0);
   }
 
-  LemmaStatus splitLemma(TNode n, bool removable) override {
-    push(LEMMA, n);
-    return LemmaStatus(Node::null(), 0);
-  }
+  void splitLemma(TNode n, bool removable) override { push(LEMMA, n); }
 
   void requirePhase(TNode, bool) override { Unreachable(); }
   void setIncomplete() override { Unreachable(); }