Eliminate PREPROCESS lemma property (#5827)

This is now possible since we always preprocess lemmas.

Note that the LemmaProperty on inferences may be redundant throughout the non-linear solver now.

13 files changed, 22 insertions, 58 deletions

diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp
index 142f02eab..ecab1b92c 100644
--- a/src/theory/arith/arith_preprocess.cpp
+++ b/src/theory/arith/arith_preprocess.cpp
@@ -49,7 +49,7 @@ bool ArithPreprocess::reduceAssertion(TNode atom)
   // tn is of kind REWRITE, turn this into a LEMMA here
   TrustNode tlem = TrustNode::mkTrustLemma(tn.getProven(), tn.getGenerator());
   // must preprocess
-  d_im.trustedLemma(tlem, LemmaProperty::PREPROCESS);
+  d_im.trustedLemma(tlem);
   // mark the atom as reduced
   d_reduced[atom] = true;
   return true;
diff --git a/src/theory/arith/inference_manager.cpp b/src/theory/arith/inference_manager.cpp
index e79c12155..6a1f898d3 100644
--- a/src/theory/arith/inference_manager.cpp
+++ b/src/theory/arith/inference_manager.cpp
@@ -25,7 +25,7 @@ namespace arith {
 InferenceManager::InferenceManager(TheoryArith& ta,
                                    ArithState& astate,
                                    ProofNodeManager* pnm)
-    : InferenceManagerBuffered(ta, astate, pnm), d_lemmasPp(ta.getUserContext())
+    : InferenceManagerBuffered(ta, astate, pnm)
 {
 }
 
@@ -110,25 +110,12 @@ std::size_t InferenceManager::numWaitingLemmas() const
 bool InferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
 {
   Node rewritten = Rewriter::rewrite(lem);
-  if (isLemmaPropertyPreprocess(p))
-  {
-    return d_lemmasPp.find(rewritten) != d_lemmasPp.end();
-  }
   return TheoryInferenceManager::hasCachedLemma(rewritten, p);
 }
 
 bool InferenceManager::cacheLemma(TNode lem, LemmaProperty p)
 {
   Node rewritten = Rewriter::rewrite(lem);
-  if (isLemmaPropertyPreprocess(p))
-  {
-    if (d_lemmasPp.find(rewritten) != d_lemmasPp.end())
-    {
-      return false;
-    }
-    d_lemmasPp.insert(rewritten);
-    return true;
-  }
   return TheoryInferenceManager::cacheLemma(rewritten, p);
 }
 
diff --git a/src/theory/arith/inference_manager.h b/src/theory/arith/inference_manager.h
index 0f2614fd7..6de65d677 100644
--- a/src/theory/arith/inference_manager.h
+++ b/src/theory/arith/inference_manager.h
@@ -116,10 +116,6 @@ class InferenceManager : public InferenceManagerBuffered
 
   /** The waiting lemmas. */
   std::vector<std::unique_ptr<ArithLemma>> d_waitingLem;
-
-  /** cache of all preprocessed lemmas sent on the output channel
-   * (user-context-dependent) */
-  NodeSet d_lemmasPp;
 };
 
 }  // namespace arith
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index f908145fe..5415e6a86 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -150,24 +150,20 @@ void IAndSolver::checkFullRefine()
         Node lem = sumBasedLemma(i);  // add lemmas based on sum mode
         Trace("iand-lemma")
             << "IAndSolver::Lemma: " << lem << " ; SUM_REFINE" << std::endl;
-        // lemma can contain div/mod so need to tag it with the PREPROCESS lemma property
-        d_im.addPendingArithLemma(lem,
-                                  InferenceId::NL_IAND_SUM_REFINE,
-                                  nullptr,
-                                  true,
-                                  LemmaProperty::PREPROCESS);
+        // note that lemma can contain div/mod, and will be preprocessed in the
+        // prop engine
+        d_im.addPendingArithLemma(
+            lem, InferenceId::NL_IAND_SUM_REFINE, nullptr, true);
       }
       else if (options::iandMode() == options::IandMode::BITWISE)
       {
         Node lem = bitwiseLemma(i);  // check for violated bitwise axioms
         Trace("iand-lemma")
             << "IAndSolver::Lemma: " << lem << " ; BITWISE_REFINE" << std::endl;
-        // lemma can contain div/mod so need to tag it with the PREPROCESS lemma property
-        d_im.addPendingArithLemma(lem,
-                                  InferenceId::NL_IAND_BITWISE_REFINE,
-                                  nullptr,
-                                  true,
-                                  LemmaProperty::PREPROCESS);
+        // note that lemma can contain div/mod, and will be preprocessed in the
+        // prop engine
+        d_im.addPendingArithLemma(
+            lem, InferenceId::NL_IAND_BITWISE_REFINE, nullptr, true);
       }
       else
       {
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index cbed48a2a..b0254d2c5 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -45,8 +45,7 @@ void ExponentialSolver::doPurification(TNode a, TNode new_a, TNode y)
   // note we must do preprocess on this lemma
   Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
                         << std::endl;
-  NlLemma nlem(
-      lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG);
+  NlLemma nlem(lem, LemmaProperty::NONE, nullptr, InferenceId::NL_T_PURIFY_ARG);
   d_data->d_im.addPendingArithLemma(nlem);
 }
 
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 40137095c..a88dd7faf 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -79,8 +79,7 @@ void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y)
   // note we must do preprocess on this lemma
   Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
                         << std::endl;
-  NlLemma nlem(
-      lem, LemmaProperty::PREPROCESS, proof, InferenceId::NL_T_PURIFY_ARG);
+  NlLemma nlem(lem, LemmaProperty::NONE, proof, InferenceId::NL_T_PURIFY_ARG);
   d_data->d_im.addPendingArithLemma(nlem);
 }
 
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index ac08b1553..7a6d5c9ab 100644
--- a/src/theory/ext_theory.cpp
+++ b/src/theory/ext_theory.cpp
@@ -371,7 +371,7 @@ bool ExtTheory::sendLemma(Node lem, bool preprocess)
     if (d_pp_lemmas.find(lem) == d_pp_lemmas.end())
     {
       d_pp_lemmas.insert(lem);
-      d_out.lemma(lem, LemmaProperty::PREPROCESS);
+      d_out.lemma(lem);
       return true;
     }
   }
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index a71a2d0eb..6df991ef9 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -916,8 +916,9 @@ void TheoryFp::preRegisterTerm(TNode node)
 
 void TheoryFp::handleLemma(Node node) {
   Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
-  // Preprocess has to be true because it contains embedded ITEs
-  d_out->lemma(node, LemmaProperty::PREPROCESS);
+  // will be preprocessed when sent, which is important because it contains
+  // embedded ITEs
+  d_out->lemma(node);
 }
 
 bool TheoryFp::propagateLit(TNode node)
diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp
index e63b78486..e0bae8fae 100644
--- a/src/theory/output_channel.cpp
+++ b/src/theory/output_channel.cpp
@@ -41,10 +41,6 @@ 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;
@@ -67,10 +63,6 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p)
     {
       out << " REMOVABLE";
     }
-    if (isLemmaPropertyPreprocess(p))
-    {
-      out << " PREPROCESS";
-    }
     if (isLemmaPropertySendAtoms(p))
     {
       out << " SEND_ATOMS";
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index c3d4b6a42..313fe24cf 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -37,12 +37,10 @@ enum class LemmaProperty : uint32_t
   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,
+  SEND_ATOMS = 2,
   // whether the lemma is part of the justification for answering "sat"
-  NEEDS_JUSTIFY = 8
+  NEEDS_JUSTIFY = 4
 };
 /** Define operator lhs | rhs */
 LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs);
@@ -54,8 +52,6 @@ LemmaProperty operator&(LemmaProperty lhs, LemmaProperty 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);
 /** is the needs justify bit set on p? */
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 8a8678749..cb31e80d3 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -374,7 +374,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
     ce_vars.push_back(tutil->getInstantiationConstant(q, i));
   }
   // send the lemma
-  d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS);
+  d_quantEngine->getOutputChannel().lemma(lem);
   // get the preprocessed form of the lemma we just sent
   std::vector<Node> skolems;
   std::vector<Node> skAsserts;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 0f17bb04a..9144bca2a 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -725,7 +725,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, LemmaProperty::PREPROCESS);
+      d_quantEngine->getOutputChannel().lemma(lem);
     }
     return false;
   }else{
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 2cc904ed1..6338c30b3 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -781,8 +781,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
         Trace("quantifiers-sk-debug")
             << "Skolemize lemma : " << slem << std::endl;
       }
-      getOutputChannel().trustedLemma(
-          lem, LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY);
+      getOutputChannel().trustedLemma(lem, LemmaProperty::NEEDS_JUSTIFY);
     }
     return;
   }
@@ -947,8 +946,7 @@ void QuantifiersEngine::flushLemmas(){
       const Node& lemw = d_lemmas_waiting[i];
       Trace("qe-lemma") << "Lemma : " << lemw << std::endl;
       itp = d_lemmasWaitingPg.find(lemw);
-      LemmaProperty p =
-          LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY;
+      LemmaProperty p = LemmaProperty::NEEDS_JUSTIFY;
       if (itp != d_lemmasWaitingPg.end())
       {
         TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second);