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.

24 files changed, 244 insertions, 99 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 422888e73..992da9a85 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -475,6 +475,7 @@ libcvc4_add_sources(
   theory/interrupted.h
   theory/logic_info.cpp
   theory/logic_info.h
+  theory/output_channel.cpp
   theory/output_channel.h
   theory/quantifiers/alpha_equivalence.cpp
   theory/quantifiers/alpha_equivalence.h
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
index 1e6e759e3..88467aea6 100644
--- a/src/proof/proof_output_channel.cpp
+++ b/src/proof/proof_output_channel.cpp
@@ -48,8 +48,10 @@ bool ProofOutputChannel::propagate(TNode x) {
   return true;
 }
 
-theory::LemmaStatus ProofOutputChannel::lemma(TNode n, ProofRule rule, bool,
-                                              bool, bool) {
+theory::LemmaStatus ProofOutputChannel::lemma(TNode n,
+                                              ProofRule rule,
+                                              theory::LemmaProperty p)
+{
   Trace("pf::tp") << "ProofOutputChannel: new lemma: " << n << std::endl;
   // TODO(#1231): We should transition to supporting multiple lemmas. The
   // following assertion cannot be enabled due to
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
index 6a91bad7c..b68abd44b 100644
--- a/src/proof/proof_output_channel.h
+++ b/src/proof/proof_output_channel.h
@@ -38,7 +38,9 @@ class ProofOutputChannel : public theory::OutputChannel {
    */
   void conflict(TNode n, std::unique_ptr<Proof> pf) override;
   bool propagate(TNode x) override;
-  theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) override;
+  theory::LemmaStatus lemma(TNode n,
+                            ProofRule rule,
+                            theory::LemmaProperty p) override;
   theory::LemmaStatus splitLemma(TNode, bool) override;
   void requirePhase(TNode n, bool b) override;
   void setIncomplete() override;
diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp
index 0497b5822..49eec186e 100644
--- a/src/theory/arith/nl/nl_lemma_utils.cpp
+++ b/src/theory/arith/nl/nl_lemma_utils.cpp
@@ -21,6 +21,11 @@ namespace theory {
 namespace arith {
 namespace nl {
 
+LemmaProperty NlLemma::getLemmaProperty() const
+{
+  return d_preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE;
+}
+
 std::ostream& operator<<(std::ostream& out, NlLemma& n)
 {
   out << n.d_lemma;
diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h
index 2b5158f18..f40857fda 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -19,6 +19,7 @@
 #include <vector>
 #include "expr/node.h"
 #include "theory/arith/nl/inference.h"
+#include "theory/output_channel.h"
 
 namespace CVC4 {
 namespace theory {
@@ -61,6 +62,8 @@ struct NlLemma
    * Cimatti et al., CADE 2017.
    */
   std::vector<std::tuple<Node, unsigned, Node> > d_secantPoint;
+  /** get lemma property (preprocess or none) */
+  LemmaProperty getLemmaProperty() const;
 };
 /**
  * Writes a non-linear lemma to a stream.
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 432c25f27..4cb1c9fe6 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -18,6 +18,7 @@
 #include "theory/arith/nl/nonlinear_extension.h"
 
 #include "options/arith_options.h"
+#include "options/theory_options.h"
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/theory_arith.h"
 #include "theory/ext_theory.h"
@@ -164,14 +165,14 @@ void NonlinearExtension::sendLemmas(const std::vector<NlLemma>& out)
   for (const NlLemma& nlem : out)
   {
     Node lem = nlem.d_lemma;
-    bool preprocess = nlem.d_preprocess;
+    LemmaProperty p = nlem.getLemmaProperty();
     Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << nlem.d_id
                           << " : " << lem << std::endl;
-    d_containing.getOutputChannel().lemma(lem, false, preprocess);
+    d_containing.getOutputChannel().lemma(lem, p);
     // process the side effect
     processSideEffect(nlem);
-    // add to cache if not preprocess
-    if (preprocess)
+    // add to cache based on preprocess
+    if (isLemmaPropertyPreprocess(p))
     {
       d_lemmasPp.insert(lem);
     }
@@ -408,7 +409,8 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
 
   Trace("nl-ext-cm") << "-----" << std::endl;
   unsigned tdegree = d_trSlv.getTaylorDegree();
-  bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs);
+  bool ret =
+      d_model.checkModel(passertions, tdegree, lemmas, gs);
   return ret;
 }
 
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 36875d8a3..6cc5c29d4 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -257,9 +257,6 @@ class NonlinearExtension
                   std::vector<Node>& gs);
   //---------------------------end check model
 
-  /** Is n entailed with polarity pol in the current context? */
-  bool isEntailed(Node n, bool pol);
-
   /**
    * Potentially adds lemmas to the set out and clears lemmas. Returns
    * the number of lemmas added to out. We do not add lemmas that have already
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 37443c070..f008dc2a1 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -1522,7 +1522,7 @@ void TheoryArrays::check(Effort e) {
           lemma = mkAnd(conjunctions, true);
           // LSH FIXME: which kind of arrays lemma is this
           Trace("arrays-lem") << "Arrays::addExtLemma " << lemma <<"\n";
-          d_out->lemma(lemma, RULE_INVALID, false, false, true);
+          d_out->lemma(lemma, RULE_INVALID, LemmaProperty::SEND_ATOMS);
           d_readTableContext->pop();
           Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
           return;
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 505d08c38..9b8badc5e 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -320,7 +320,7 @@ void TheoryDatatypes::check(Effort e) {
                     Trace("dt-split") << "*************Split for constructors on " << n <<  endl;
                     Node lemma = utils::mkSplit(n, dt);
                     Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
-                    d_out->lemma( lemma, false, false, true );
+                    d_out->lemma(lemma, LemmaProperty::SEND_ATOMS);
                     d_addedLemma = true;
                   }
                   if( !options::dtBlastSplits() ){
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
diff --git a/src/theory/engine_output_channel.h b/src/theory/engine_output_channel.h
index d7b26928d..3e959898f 100644
--- a/src/theory/engine_output_channel.h
+++ b/src/theory/engine_output_channel.h
@@ -51,9 +51,7 @@ class EngineOutputChannel : public theory::OutputChannel
 
   theory::LemmaStatus lemma(TNode lemma,
                             ProofRule rule,
-                            bool removable = false,
-                            bool preprocess = false,
-                            bool sendAtoms = false) override;
+                            LemmaProperty p = LemmaProperty::NONE) override;
 
   theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) override;
 
@@ -81,9 +79,7 @@ class EngineOutputChannel : public theory::OutputChannel
    * the same as calling OutputChannel::lemma on lem.
    */
   LemmaStatus trustedLemma(TrustNode plem,
-                           bool removable = false,
-                           bool preprocess = false,
-                           bool sendAtoms = false) override;
+                           LemmaProperty p = LemmaProperty::NONE) override;
 
  protected:
   /**
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index f84153c06..bdcd5dcff 100644
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -344,7 +344,7 @@ bool ExtTheory::sendLemma(Node lem, bool preprocess)
     if (d_pp_lemmas.find(lem) == d_pp_lemmas.end())
     {
       d_pp_lemmas.insert(lem);
-      d_parent->getOutputChannel().lemma(lem, false, true);
+      d_parent->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
       return true;
     }
   }
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index bffcda7bc..a4cff8c95 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -902,9 +902,8 @@ void TheoryFp::addSharedTerm(TNode node) {
 
 void TheoryFp::handleLemma(Node node) {
   Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
-
-  d_out->lemma(node, false,
-               true);  // Has to be true because it contains embedded ITEs
+  // Preprocess has to be true because it contains embedded ITEs
+  d_out->lemma(node, LemmaProperty::PREPROCESS);
   // Ignore the LemmaStatus structure for now...
 
   return;
diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp
new file mode 100644
index 000000000..9fe973569
--- /dev/null
+++ b/src/theory/output_channel.cpp
@@ -0,0 +1,111 @@
+/*********************                                                        */
+/*! \file output_channel.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The theory output channel interface
+ **/
+
+#include "theory/output_channel.h"
+
+namespace CVC4 {
+namespace theory {
+
+LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs)
+{
+  return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs)
+                                    | static_cast<uint32_t>(rhs));
+}
+LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs)
+{
+  lhs = lhs | rhs;
+  return lhs;
+}
+LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs)
+{
+  return static_cast<LemmaProperty>(static_cast<uint32_t>(lhs)
+                                    & static_cast<uint32_t>(rhs));
+}
+LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs)
+{
+  lhs = lhs & rhs;
+  return lhs;
+}
+bool isLemmaPropertyRemovable(LemmaProperty p)
+{
+  return (p & LemmaProperty::REMOVABLE) != LemmaProperty::NONE;
+}
+bool isLemmaPropertyPreprocess(LemmaProperty p)
+{
+  return (p & LemmaProperty::PREPROCESS) != LemmaProperty::NONE;
+}
+bool isLemmaPropertySendAtoms(LemmaProperty p)
+{
+  return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE;
+}
+
+std::ostream& operator<<(std::ostream& out, LemmaProperty p)
+{
+  if (p == LemmaProperty::NONE)
+  {
+    out << "NONE";
+  }
+  else
+  {
+    out << "{";
+    if (isLemmaPropertyRemovable(p))
+    {
+      out << " REMOVABLE";
+    }
+    if (isLemmaPropertyPreprocess(p))
+    {
+      out << " PREPROCESS";
+    }
+    if (isLemmaPropertySendAtoms(p))
+    {
+      out << " SEND_ATOMS";
+    }
+    out << " }";
+  }
+  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::lemma(TNode n, LemmaProperty p)
+{
+  return lemma(n, RULE_INVALID, p);
+}
+
+LemmaStatus OutputChannel::split(TNode n)
+{
+  return splitLemma(n.orNode(n.notNode()));
+}
+
+void OutputChannel::trustedConflict(TrustNode pconf)
+{
+  Unreachable() << "OutputChannel::trustedConflict: no implementation"
+                << std::endl;
+}
+
+LemmaStatus OutputChannel::trustedLemma(TrustNode lem, LemmaProperty p)
+{
+  Unreachable() << "OutputChannel::trustedLemma: no implementation"
+                << std::endl;
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index ff13d1b6b..d65d4fc53 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -32,6 +32,42 @@
 namespace CVC4 {
 namespace theory {
 
+/** Properties of lemmas */
+enum class LemmaProperty : uint32_t
+{
+  // default
+  NONE = 0,
+  // whether the lemma is removable
+  REMOVABLE = 1,
+  // whether the lemma needs preprocessing
+  PREPROCESS = 2,
+  // whether the processing of the lemma should send atoms to the caller
+  SEND_ATOMS = 4
+};
+/** Define operator lhs | rhs */
+LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs);
+/** Define operator lhs |= rhs */
+LemmaProperty& operator|=(LemmaProperty& lhs, LemmaProperty rhs);
+/** Define operator lhs & rhs */
+LemmaProperty operator&(LemmaProperty lhs, LemmaProperty rhs);
+/** Define operator lhs &= rhs */
+LemmaProperty& operator&=(LemmaProperty& lhs, LemmaProperty rhs);
+/** is the removable bit set on p? */
+bool isLemmaPropertyRemovable(LemmaProperty p);
+/** is the preprocess bit set on p? */
+bool isLemmaPropertyPreprocess(LemmaProperty p);
+/** is the send atoms bit set on p? */
+bool isLemmaPropertySendAtoms(LemmaProperty p);
+
+/**
+ * Writes an lemma property name to a stream.
+ *
+ * @param out The stream to write to
+ * @param p The lemma property to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, LemmaProperty p);
+
 class Theory;
 
 /**
@@ -41,17 +77,17 @@ class Theory;
  */
 class LemmaStatus {
  public:
-  LemmaStatus(TNode rewrittenLemma, unsigned level)
-      : d_rewrittenLemma(rewrittenLemma), d_level(level) {}
+  LemmaStatus(TNode rewrittenLemma, unsigned level);
 
   /** Get the T-rewritten form of the lemma. */
-  TNode getRewrittenLemma() const { return d_rewrittenLemma; }
+  TNode getRewrittenLemma() const;
   /**
    * Get the user-level at which the lemma resides.  After this user level
    * is popped, the lemma is un-asserted from the SAT layer.  This level
    * will be 0 if the lemma didn't reach the SAT layer at all.
    */
-  unsigned getLevel() const { return d_level; }
+  unsigned getLevel() const;
+
  private:
   Node d_rewrittenLemma;
   unsigned d_level;
@@ -114,23 +150,18 @@ class OutputChannel {
    *
    * @param n - a theory lemma valid at decision level 0
    * @param rule - the proof rule for this lemma
-   * @param removable - whether the lemma can be removed at any point
-   * @param preprocess - whether to apply more aggressive preprocessing
-   * @param sendAtoms - whether to ensure atoms are sent to the theory
+   * @param p The properties of the lemma
    * @return the "status" of the lemma, including user level at which
    * the lemma resides; the lemma will be removed when this user level pops
    */
-  virtual LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false,
-                            bool preprocess = false,
-                            bool sendAtoms = false) = 0;
+  virtual LemmaStatus lemma(TNode n,
+                            ProofRule rule,
+                            LemmaProperty p = LemmaProperty::NONE) = 0;
 
   /**
    * Variant of the lemma function that does not require providing a proof rule.
    */
-  virtual LemmaStatus lemma(TNode n, bool removable = false,
-                            bool preprocess = false, bool sendAtoms = false) {
-    return lemma(n, RULE_INVALID, removable, preprocess, sendAtoms);
-  }
+  virtual LemmaStatus lemma(TNode n, LemmaProperty p = LemmaProperty::NONE);
 
   /**
    * Request a split on a new theory atom.  This is equivalent to
@@ -138,7 +169,7 @@ class OutputChannel {
    *
    * @param n - a theory atom; must be of Boolean type
    */
-  LemmaStatus split(TNode n) { return splitLemma(n.orNode(n.notNode())); }
+  LemmaStatus split(TNode n);
 
   virtual LemmaStatus splitLemma(TNode n, bool removable = false) = 0;
 
@@ -197,11 +228,7 @@ class OutputChannel {
    * by the generator pfg. Apart from pfg, the interface for this method is
    * the same as OutputChannel.
    */
-  virtual void trustedConflict(TrustNode pconf)
-  {
-    Unreachable() << "OutputChannel::trustedConflict: no implementation"
-                  << std::endl;
-  }
+  virtual void trustedConflict(TrustNode pconf);
   /**
    * Let plem be the pair (Node lem, ProofGenerator * pfg).
    * Send lem on the output channel of this class whose proof can be generated
@@ -209,13 +236,7 @@ class OutputChannel {
    * the same as OutputChannel.
    */
   virtual LemmaStatus trustedLemma(TrustNode lem,
-                                   bool removable = false,
-                                   bool preprocess = false,
-                                   bool sendAtoms = false)
-  {
-    Unreachable() << "OutputChannel::trustedLemma: no implementation"
-                  << std::endl;
-  }
+                                   LemmaProperty p = LemmaProperty::NONE);
   //---------------------------- end new proof
 }; /* class OutputChannel */
 
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 7f0e93997..5a50bc99a 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -1394,7 +1394,7 @@ void CegInstantiator::presolve( Node q ) {
       lem = NodeManager::currentNM()->mkNode( OR, g, lem );
       Trace("cegqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
       Assert(!expr::hasFreeVar(lem));
-      d_qe->getOutputChannel().lemma( lem, false, true );
+      d_qe->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
     }
   }
 }
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index b3ea69dbc..84f4bb83b 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -723,7 +723,7 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
       nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
       Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] );
       Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl;
-      d_quantEngine->getOutputChannel().lemma(lem, false, true);
+      d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
     }
     return false;
   }else{
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 6dcf1a980..bb5950c5e 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -970,7 +970,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
         Trace("quantifiers-sk-debug")
             << "Skolemize lemma : " << slem << std::endl;
       }
-      getOutputChannel().lemma(lem, false, true);
+      getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
     }
     return;
   }
@@ -1021,7 +1021,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){
     Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl;
     BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem );
     if( itp==d_lemmas_produced_c.end() || !(*itp).second ){
-      //d_curr_out->lemma( lem, false, true );
       d_lemmas_produced_c[ lem ] = true;
       d_lemmas_waiting.push_back( lem );
       Trace("inst-add-debug") << "Added lemma" << std::endl;
@@ -1122,7 +1121,7 @@ void QuantifiersEngine::flushLemmas(){
     d_hasAddedLemma = true;
     for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){
       Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl;
-      getOutputChannel().lemma( d_lemmas_waiting[i], false, true );
+      getOutputChannel().lemma(d_lemmas_waiting[i], LemmaProperty::PREPROCESS);
     }
     d_lemmas_waiting.clear();
   }
diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp
index 224eee57e..ac0a8205b 100644
--- a/src/theory/sets/inference_manager.cpp
+++ b/src/theory/sets/inference_manager.cpp
@@ -212,7 +212,9 @@ void InferenceManager::flushLemma(Node lem, bool preprocess)
   }
   Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
   d_lemmas_produced.insert(lem);
-  d_parent.getOutputChannel()->lemma(lem, false, preprocess);
+  LemmaProperty p =
+      preprocess ? LemmaProperty::PREPROCESS : LemmaProperty::NONE;
+  d_parent.getOutputChannel()->lemma(lem, p);
   d_sentLemma = true;
 }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9955be850..ef237e76d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -41,6 +41,7 @@
 #include "theory/arith/arith_ite_utils.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/care_graph.h"
+#include "theory/decision_manager.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/model_engine.h"
 #include "theory/quantifiers/theory_quantifiers.h"
@@ -621,8 +622,7 @@ void TheoryEngine::combineTheories() {
     lemma(equality.orNode(equality.notNode()),
           RULE_INVALID,
           false,
-          false,
-          false,
+          LemmaProperty::NONE,
           carePair.d_theory);
 
     // This code is supposed to force preference to follow what the theory models already have
@@ -1587,9 +1587,9 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The
 theory::LemmaStatus TheoryEngine::lemma(TNode node,
                                         ProofRule rule,
                                         bool negated,
-                                        bool removable,
-                                        bool preprocess,
-                                        theory::TheoryId atomsTo) {
+                                        theory::LemmaProperty p,
+                                        theory::TheoryId atomsTo)
+{
   // For resource-limiting (also does a time check).
   // spendResource();
 
@@ -1609,6 +1609,8 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
     Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
                      << CheckSatCommand(n.toExpr());
   }
+  bool removable = isLemmaPropertyRemovable(p);
+  bool preprocess = isLemmaPropertyPreprocess(p);
 
   // call preprocessor
   std::vector<TrustNode> newLemmas;
@@ -1705,8 +1707,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     Node fullConflict = mkExplanation(explanationVector);
     Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
     Assert(properConflict(fullConflict));
-    lemma(fullConflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
-
+    lemma(fullConflict,
+          RULE_CONFLICT,
+          true,
+          LemmaProperty::REMOVABLE,
+          THEORY_LAST);
   } else {
     // When only one theory, the conflict should need no processing
     Assert(properConflict(conflict));
@@ -1735,7 +1740,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
         ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
       });
 
-    lemma(conflict, RULE_CONFLICT, true, true, false, THEORY_LAST);
+    lemma(conflict, RULE_CONFLICT, true, LemmaProperty::REMOVABLE, THEORY_LAST);
   }
 
   PROOF({
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 8c0ce6dbf..5b04e49a8 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -330,14 +330,12 @@ class TheoryEngine {
    * Adds a new lemma, returning its status.
    * @param node the lemma
    * @param negated should the lemma be asserted negated
-   * @param removable can the lemma be remove (restrictions apply)
-   * @param needAtoms if not THEORY_LAST, then
+   * @param p the properties of the lemma.
    */
   theory::LemmaStatus lemma(TNode node,
                             ProofRule rule,
                             bool negated,
-                            bool removable,
-                            bool preprocess,
+                            theory::LemmaProperty p,
                             theory::TheoryId atomsTo);
 
   /** Enusre that the given atoms are send to the given theory */
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 61caca82a..2593b11a6 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -79,8 +79,8 @@ public:
     return true;
   }
 
-  LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false,
-                    bool preprocess = false, bool sendAtoms = false) override {
+  LemmaStatus lemma(TNode n, ProofRule rule, LemmaProperty p) override
+  {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 5a16fdc20..fbcfbdb37 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -60,8 +60,10 @@ class FakeOutputChannel : public OutputChannel {
     Unimplemented();
   }
   bool propagate(TNode n) override { Unimplemented(); }
-  LemmaStatus lemma(TNode n, ProofRule rule, bool removable, bool preprocess,
-                    bool sendAtoms) override {
+  LemmaStatus lemma(TNode n,
+                    ProofRule rule,
+                    LemmaProperty p = LemmaProperty::NONE) override
+  {
     Unimplemented();
   }
   void requirePhase(TNode, bool) override { Unimplemented(); }
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 0ff4e918b..5ed7afbe1 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -58,8 +58,10 @@ class TestOutputChannel : public OutputChannel {
     return true;
   }
 
-  LemmaStatus lemma(TNode n, ProofRule rule, bool removable = false,
-                    bool preprocess = false, bool sendAtoms = false) override {
+  LemmaStatus lemma(TNode n,
+                    ProofRule rule,
+                    LemmaProperty p = LemmaProperty::NONE) override
+  {
     push(LEMMA, n);
     return LemmaStatus(Node::null(), 0);
   }