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, 12 insertions, 16 deletions

diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index 0aa56a381..1105b918b 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -67,7 +67,7 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r)
   }
 }
 
-theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
+void EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
 {
   Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
                          << lemma << ")"
@@ -76,15 +76,13 @@ theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
   d_engine->d_outputChannelUsed = true;
 
   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
-  theory::LemmaStatus result = d_engine->lemma(
-      tlem,
-      p,
-      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
-      d_theory);
-  return result;
+  d_engine->lemma(tlem,
+                  p,
+                  isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
+                  d_theory);
 }
 
-theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
+void EngineOutputChannel::splitLemma(TNode lemma, bool removable)
 {
   Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
                          << lemma << ")" << std::endl;
@@ -95,8 +93,7 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
                        << std::endl;
   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
   LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE;
-  theory::LemmaStatus result = d_engine->lemma(tlem, p, d_theory);
-  return result;
+  d_engine->lemma(tlem, p, d_theory);
 }
 
 bool EngineOutputChannel::propagate(TNode literal)
@@ -172,7 +169,7 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf)
   d_engine->conflict(pconf, d_theory);
 }
 
-LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
+void EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
 {
   Trace("theory::lemma") << "EngineOutputChannel<" << d_theory
                          << ">::trustedLemma(" << plem << ")" << std::endl;
@@ -184,11 +181,10 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
   ++d_statistics.lemmas;
   d_engine->d_outputChannelUsed = true;
   // now, call the normal interface for lemma
-  return d_engine->lemma(
-      plem,
-      p,
-      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
-      d_theory);
+  d_engine->lemma(plem,
+                  p,
+                  isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
+                  d_theory);
 }
 
 }  // namespace theory