Use lemma property enum for OutputChannel::lemma (#4755)

There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.

This makes them into a enum.

1 files changed, 23 insertions, 25 deletions

diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp
index d83d2ba62..a271d6d9c 100644
--- a/src/theory/engine_output_channel.cpp
+++ b/src/theory/engine_output_channel.cpp
@@ -73,26 +73,26 @@ void EngineOutputChannel::safePoint(ResourceManager::Resource r)
 
 theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma,
                                                ProofRule rule,
-                                               bool removable,
-                                               bool preprocess,
-                                               bool sendAtoms)
+                                               LemmaProperty p)
 {
   Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
                          << lemma << ")"
-                         << ", preprocess = " << preprocess << std::endl;
+                         << ", properties = " << p << std::endl;
   ++d_statistics.lemmas;
   d_engine->d_outputChannelUsed = true;
 
-  PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); });
+  PROOF({
+    bool preprocess = isLemmaPropertyPreprocess(p);
+    registerLemmaRecipe(lemma, lemma, preprocess, d_theory);
+  });
 
   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
-  theory::LemmaStatus result =
-      d_engine->lemma(tlem.getNode(),
-                      rule,
-                      false,
-                      removable,
-                      preprocess,
-                      sendAtoms ? d_theory : theory::THEORY_LAST);
+  theory::LemmaStatus result = d_engine->lemma(
+      tlem.getNode(),
+      rule,
+      false,
+      p,
+      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST);
   return result;
 }
 
@@ -236,8 +236,9 @@ theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
   Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
                        << std::endl;
   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
-  theory::LemmaStatus result = d_engine->lemma(
-      tlem.getNode(), RULE_SPLIT, false, removable, false, d_theory);
+  LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE;
+  theory::LemmaStatus result =
+      d_engine->lemma(tlem.getNode(), RULE_SPLIT, false, p, d_theory);
   return result;
 }
 
@@ -273,7 +274,7 @@ void EngineOutputChannel::demandRestart()
   Trace("theory::restart") << "EngineOutputChannel<" << d_theory
                            << ">::restart(" << restartVar << ")" << std::endl;
   ++d_statistics.restartDemands;
-  lemma(restartVar, RULE_INVALID, true);
+  lemma(restartVar, RULE_INVALID, LemmaProperty::REMOVABLE);
 }
 
 void EngineOutputChannel::requirePhase(TNode n, bool phase)
@@ -316,10 +317,7 @@ void EngineOutputChannel::trustedConflict(TrustNode pconf)
   d_engine->conflict(pconf.getNode(), d_theory);
 }
 
-LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem,
-                                              bool removable,
-                                              bool preprocess,
-                                              bool sendAtoms)
+LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
 {
   Assert(plem.getKind() == TrustNodeKind::LEMMA);
   if (plem.getGenerator() != nullptr)
@@ -329,12 +327,12 @@ LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem,
   ++d_statistics.lemmas;
   d_engine->d_outputChannelUsed = true;
   // now, call the normal interface for lemma
-  return d_engine->lemma(plem.getNode(),
-                         RULE_INVALID,
-                         false,
-                         removable,
-                         preprocess,
-                         sendAtoms ? d_theory : theory::THEORY_LAST);
+  return d_engine->lemma(
+      plem.getNode(),
+      RULE_INVALID,
+      false,
+      p,
+      isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST);
 }
 
 }  // namespace theory