Improve flexibility of lemma output in non-linear solver (#3518)

2 files changed, 193 insertions, 133 deletions

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index d76089541..287acbc36 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -540,28 +540,46 @@ Node NonlinearExtension::mkMonomialRemFactor(
   return ret;
 }
 
-int NonlinearExtension::flushLemma(Node lem) {
+void NonlinearExtension::sendLemmas(const std::vector<Node>& out,
+                                    bool preprocess)
+{
+  for (const Node& lem : out)
+  {
+    Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
+    d_containing.getOutputChannel().lemma(lem, false, preprocess);
+    // add to cache if not preprocess
+    if (!preprocess)
+    {
+      d_lemmas.insert(lem);
+    }
+  }
+}
+
+unsigned NonlinearExtension::filterLemma(Node lem, std::vector<Node>& out)
+{
   Trace("nl-ext-lemma-debug")
       << "NonlinearExtension::Lemma pre-rewrite : " << lem << std::endl;
   lem = Rewriter::rewrite(lem);
-  if (Contains(d_lemmas, lem)) {
+  if (d_lemmas.find(lem) != d_lemmas.end()
+      || std::find(out.begin(), out.end(), lem) != out.end())
+  {
     Trace("nl-ext-lemma-debug")
         << "NonlinearExtension::Lemma duplicate : " << lem << std::endl;
-    // should not generate duplicates
-    // Assert( false );
     return 0;
   }
-  d_lemmas.insert(lem);
-  Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : " << lem << std::endl;
-  d_containing.getOutputChannel().lemma(lem);
+  out.push_back(lem);
   return 1;
 }
 
-int NonlinearExtension::flushLemmas(std::vector<Node>& lemmas) {
-  if (options::nlExtEntailConflicts()) {
+unsigned NonlinearExtension::filterLemmas(std::vector<Node>& lemmas,
+                                          std::vector<Node>& out)
+{
+  if (options::nlExtEntailConflicts())
+  {
     // check if any are entailed to be false
-    for (unsigned i = 0; i < lemmas.size(); i++) {
-      Node ch_lemma = lemmas[i].negate();
+    for (const Node& lem : lemmas)
+    {
+      Node ch_lemma = lem.negate();
       ch_lemma = Rewriter::rewrite(ch_lemma);
       Trace("nl-ext-et-debug")
           << "Check entailment of " << ch_lemma << "..." << std::endl;
@@ -569,11 +587,13 @@ int NonlinearExtension::flushLemmas(std::vector<Node>& lemmas) {
           THEORY_OF_TYPE_BASED, ch_lemma);
       Trace("nl-ext-et-debug") << "entailment test result : " << et.first << " "
                                << et.second << std::endl;
-      if (et.first) {
-        Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : "
-                           << lemmas[i] << std::endl;
+      if (et.first)
+      {
+        Trace("nl-ext-et") << "*** Lemma entailed to be in conflict : " << lem
+                           << std::endl;
         // return just this lemma
-        if (flushLemma(lemmas[i])) {
+        if (filterLemma(lem, out) > 0)
+        {
           lemmas.clear();
           return 1;
         }
@@ -581,9 +601,10 @@ int NonlinearExtension::flushLemmas(std::vector<Node>& lemmas) {
     }
   }
 
-  int sum = 0;
-  for (unsigned i = 0; i < lemmas.size(); i++) {
-    sum += flushLemma(lemmas[i]);
+  unsigned sum = 0;
+  for (const Node& lem : lemmas)
+  {
+    sum += filterLemma(lem, out);
   }
   lemmas.clear();
   return sum;
@@ -730,7 +751,9 @@ std::vector<Node> NonlinearExtension::checkModelEval(
 }
 
 bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
-                                    const std::vector<Node>& false_asserts)
+                                    const std::vector<Node>& false_asserts,
+                                    std::vector<Node>& lemmas,
+                                    std::vector<Node>& gs)
 {
   Trace("nl-ext-cm") << "--- check-model ---" << std::endl;
 
@@ -791,23 +814,8 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
       }
     }
   }
-  std::vector<Node> lemmas;
-  std::vector<Node> gs;
   bool ret = d_model.checkModel(
       passertions, false_asserts, d_taylor_degree, lemmas, gs);
-  for (Node& mg : gs)
-  {
-    mg = Rewriter::rewrite(mg);
-    mg = d_containing.getValuation().ensureLiteral(mg);
-    d_containing.getOutputChannel().requirePhase(mg, true);
-    d_builtModel = true;
-  }
-  for (Node& lem : lemmas)
-  {
-    Trace("nl-ext-lemma-model")
-        << "Lemma from check model : " << lem << std::endl;
-    d_containing.getOutputChannel().lemma(lem);
-  }
   return ret;
 }
 
@@ -856,7 +864,10 @@ class ArgTrie
 
 int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                                       const std::vector<Node>& false_asserts,
-                                      const std::vector<Node>& xts)
+                                      const std::vector<Node>& xts,
+                                      std::vector<Node>& lems,
+                                      std::vector<Node>& lemsPp,
+                                      std::vector<Node>& wlems)
 {
   d_ms_vars.clear();
   d_ms_proc.clear();
@@ -869,9 +880,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   d_ci_max.clear();
   d_f_map.clear();
   d_tf_region.clear();
-  d_waiting_lemmas.clear();
 
-  int lemmas_proc = 0;
   std::vector<Node> lemmas;
   NodeManager* nm = NodeManager::currentNM();
 
@@ -989,10 +998,12 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     getCurrentPiBounds(lemmas);
   }
 
-  lemmas_proc = flushLemmas(lemmas);
-  if (lemmas_proc > 0) {
-    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas during registration." << std::endl;
-    return lemmas_proc;
+  filterLemmas(lemmas, lems);
+  if (!lems.empty())
+  {
+    Trace("nl-ext") << "  ...finished with " << lems.size()
+                    << " new lemmas during registration." << std::endl;
+    return lems.size();
   }
 
   // process SINE phase shifting
@@ -1035,15 +1046,14 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       // must do preprocess on this one
       Trace("nl-ext-lemma")
           << "NonlinearExtension::Lemma : purify : " << lem << std::endl;
-      d_containing.getOutputChannel().lemma(lem, false, true);
-      lemmas_proc++;
+      lemsPp.push_back(lem);
     }
   }
-  if (lemmas_proc > 0)
+  if (!lemsPp.empty())
   {
-    Trace("nl-ext") << "  ...finished with " << lemmas_proc
+    Trace("nl-ext") << "  ...finished with " << lemsPp.size()
                     << " new lemmas SINE phase shifting." << std::endl;
-    return lemmas_proc;
+    return lemsPp.size();
   }
   Trace("nl-ext") << "We have " << d_ms.size() << " monomials." << std::endl;
 
@@ -1088,35 +1098,43 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   if (options::nlExtSplitZero()) {
     Trace("nl-ext") << "Get zero split lemmas..." << std::endl;
     lemmas = checkSplitZero();
-    lemmas_proc = flushLemmas(lemmas);
-    if (lemmas_proc > 0) {
-      Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
-      return lemmas_proc;
+    filterLemmas(lemmas, lems);
+    if (!lems.empty())
+    {
+      Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+                      << std::endl;
+      return lems.size();
     }
   }
 
   //-----------------------------------initial lemmas for transcendental functions
   lemmas = checkTranscendentalInitialRefine();
-  lemmas_proc = flushLemmas(lemmas);
-  if (lemmas_proc > 0) {
-    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
-    return lemmas_proc;
+  filterLemmas(lemmas, lems);
+  if (!lems.empty())
+  {
+    Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+                    << std::endl;
+    return lems.size();
   }
-  
+
   //-----------------------------------lemmas based on sign (comparison to zero)
   lemmas = checkMonomialSign();
-  lemmas_proc = flushLemmas(lemmas);
-  if (lemmas_proc > 0) {
-    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
-    return lemmas_proc;
+  filterLemmas(lemmas, lems);
+  if (!lems.empty())
+  {
+    Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+                    << std::endl;
+    return lems.size();
   }
-  
+
   //-----------------------------------monotonicity of transdental functions
   lemmas = checkTranscendentalMonotonic();
-  lemmas_proc = flushLemmas(lemmas);
-  if (lemmas_proc > 0) {
-    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
-    return lemmas_proc;
+  filterLemmas(lemmas, lems);
+  if (!lems.empty())
+  {
+    Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+                    << std::endl;
+    return lems.size();
   }
 
   //-----------------------------------lemmas based on magnitude of non-zero monomials
@@ -1138,12 +1156,13 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     // c is effort level
     lemmas = checkMonomialMagnitude( c );
     unsigned nlem = lemmas.size();
-    lemmas_proc = flushLemmas(lemmas);
-    if (lemmas_proc > 0) {
-      Trace("nl-ext") << "  ...finished with " << lemmas_proc
+    filterLemmas(lemmas, lems);
+    if (!lems.empty())
+    {
+      Trace("nl-ext") << "  ...finished with " << lems.size()
                       << " new lemmas (out of possible " << nlem << ")."
                       << std::endl;
-      return lemmas_proc;
+      return lems.size();
     }
   }
 
@@ -1162,36 +1181,40 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " <<
   // nt_lemmas.size() << std::endl;  prioritize lemmas that do not
   // introduce new monomials
-  lemmas_proc = flushLemmas(lemmas);
+  filterLemmas(lemmas, lems);
 
   if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave())
   {
     lemmas = checkTangentPlanes();
-    lemmas_proc += flushLemmas(lemmas);
+    filterLemmas(lemmas, lems);
   }
 
-  if (lemmas_proc > 0) {
-    Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas."
+  if (!lems.empty())
+  {
+    Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
                     << std::endl;
-    return lemmas_proc;
+    return lems.size();
   }
-  
+
   // from inferred bound inferences : now do ones that introduce new terms
-  lemmas_proc = flushLemmas(nt_lemmas);
-  if (lemmas_proc > 0) {
-    Trace("nl-ext") << "  ...finished with " << lemmas_proc
+  filterLemmas(nt_lemmas, lems);
+  if (!lems.empty())
+  {
+    Trace("nl-ext") << "  ...finished with " << lems.size()
                     << " new (monomial-introducing) lemmas." << std::endl;
-    return lemmas_proc;
+    return lems.size();
   }
-  
+
   //------------------------------------factoring lemmas
   //   x*y + x*z >= t => exists k. k = y + z ^ x*k >= t
   if( options::nlExtFactor() ){
     lemmas = checkFactoring(assertions, false_asserts);
-    lemmas_proc = flushLemmas(lemmas);
-    if (lemmas_proc > 0) {
-      Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
-      return lemmas_proc;
+    filterLemmas(lemmas, lems);
+    if (!lems.empty())
+    {
+      Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+                      << std::endl;
+      return lems.size();
     }
   }
 
@@ -1199,10 +1222,12 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   //  e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
   if (options::nlExtResBound()) {
     lemmas = checkMonomialInferResBounds();
-    lemmas_proc = flushLemmas(lemmas);
-    if (lemmas_proc > 0) {
-      Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas." << std::endl;
-      return lemmas_proc;
+    filterLemmas(lemmas, lems);
+    if (!lems.empty())
+    {
+      Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+                      << std::endl;
+      return lems.size();
     }
   }
   
@@ -1210,19 +1235,15 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave())
   {
     lemmas = checkTangentPlanes();
-    d_waiting_lemmas.insert(
-        d_waiting_lemmas.end(), lemmas.begin(), lemmas.end());
-    lemmas.clear();
+    filterLemmas(lemmas, wlems);
   }
   if (options::nlExtTfTangentPlanes())
   {
     lemmas = checkTranscendentalTangentPlanes();
-    d_waiting_lemmas.insert(
-        d_waiting_lemmas.end(), lemmas.begin(), lemmas.end());
-    lemmas.clear();
+    filterLemmas(lemmas, wlems);
   }
-  Trace("nl-ext") << "  ...finished with " << d_waiting_lemmas.size()
-                  << " waiting lemmas." << std::endl;
+  Trace("nl-ext") << "  ...finished with " << wlems.size() << " waiting lemmas."
+                  << std::endl;
 
   return 0;
 }
@@ -1255,9 +1276,13 @@ void NonlinearExtension::check(Theory::Effort e) {
     TheoryModel* tm = d_containing.getValuation().getModel();
     if (!d_builtModel.get())
     {
-      // run model-based refinement
-      if (modelBasedRefinement())
+      // run a last call effort check
+      std::vector<Node> mlems;
+      std::vector<Node> mlemsPp;
+      if (modelBasedRefinement(mlems, mlemsPp))
       {
+        sendLemmas(mlems);
+        sendLemmas(mlemsPp, true);
         return;
       }
     }
@@ -1278,7 +1303,8 @@ void NonlinearExtension::check(Theory::Effort e) {
   }
 }
 
-bool NonlinearExtension::modelBasedRefinement()
+bool NonlinearExtension::modelBasedRefinement(std::vector<Node>& mlems,
+                                              std::vector<Node>& mlemsPp)
 {
   // reset the model object
   d_model.reset(d_containing.getValuation().getModel());
@@ -1359,14 +1385,15 @@ bool NonlinearExtension::modelBasedRefinement()
     // complete_status:
     //   1 : we may answer SAT, -1 : we may not answer SAT, 0 : unknown
     int complete_status = 1;
-    int num_added_lemmas = 0;
-    // we require a check either if an assertion is false or a shared term has
+    // lemmas that should be sent later
+    std::vector<Node> wlems;
+    // We require a check either if an assertion is false or a shared term has
     // a wrong value
     if (!false_asserts.empty() || num_shared_wrong_value > 0)
     {
       complete_status = num_shared_wrong_value > 0 ? -1 : 0;
-      num_added_lemmas = checkLastCall(assertions, false_asserts, xts);
-      if (num_added_lemmas > 0)
+      checkLastCall(assertions, false_asserts, xts, mlems, mlemsPp, wlems);
+      if (!mlems.empty() || !mlemsPp.empty())
       {
         return true;
       }
@@ -1382,20 +1409,34 @@ bool NonlinearExtension::modelBasedRefinement()
           << std::endl;
       // check the model based on simple solving of equalities and using
       // error bounds on the Taylor approximation of transcendental functions.
-      if (checkModel(assertions, false_asserts))
+      std::vector<Node> lemmas;
+      std::vector<Node> gs;
+      if (checkModel(assertions, false_asserts, lemmas, gs))
       {
         complete_status = 1;
       }
+      for (const Node& mg : gs)
+      {
+        Node mgr = Rewriter::rewrite(mg);
+        mgr = d_containing.getValuation().ensureLiteral(mgr);
+        d_containing.getOutputChannel().requirePhase(mgr, true);
+        d_builtModel = true;
+      }
+      filterLemmas(lemmas, mlems);
+      if (!mlems.empty())
+      {
+        return true;
+      }
     }
 
     // if we have not concluded SAT
     if (complete_status != 1)
     {
       // flush the waiting lemmas
-      num_added_lemmas = flushLemmas(d_waiting_lemmas);
-      if (num_added_lemmas > 0)
+      if (!wlems.empty())
       {
-        Trace("nl-ext") << "...added " << num_added_lemmas << " waiting lemmas."
+        mlems.insert(mlems.end(), wlems.begin(), wlems.end());
+        Trace("nl-ext") << "...added " << wlems.size() << " waiting lemmas."
                         << std::endl;
         return true;
       }
@@ -1406,20 +1447,20 @@ bool NonlinearExtension::modelBasedRefinement()
         complete_status = -1;
         if (!shared_term_value_splits.empty())
         {
-          std::vector<Node> shared_term_value_lemmas;
+          std::vector<Node> stvLemmas;
           for (const Node& eq : shared_term_value_splits)
           {
             Node req = Rewriter::rewrite(eq);
             Node literal = d_containing.getValuation().ensureLiteral(req);
             d_containing.getOutputChannel().requirePhase(literal, true);
             Trace("nl-ext-debug") << "Split on : " << literal << std::endl;
-            shared_term_value_lemmas.push_back(
-                literal.orNode(literal.negate()));
+            Node split = literal.orNode(literal.negate());
+            filterLemma(split, stvLemmas);
           }
-          num_added_lemmas = flushLemmas(shared_term_value_lemmas);
-          if (num_added_lemmas > 0)
+          if (!stvLemmas.empty())
           {
-            Trace("nl-ext") << "...added " << num_added_lemmas
+            mlems.insert(mlems.end(), stvLemmas.begin(), stvLemmas.end());
+            Trace("nl-ext") << "...added " << stvLemmas.size()
                             << " shared term value split lemmas." << std::endl;
             return true;
           }
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 1690c9334..20357b722 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -138,13 +138,13 @@ class NonlinearExtension {
    * described in Reynolds et al. FroCoS 2017 that are based on ruling out
    * the current candidate model.
    *
-   * This function returns true if a lemma was sent out on the output
-   * channel of the theory of arithmetic. Otherwise, it returns false. In the
-   * latter case, the model object d_model may have information regarding
-   * how to construct a model, in the case that we determined the problem
-   * is satisfiable.
+   * This function returns true if a lemma was added to the vector lems/lemsPp.
+   * Otherwise, it returns false. In the latter case, the model object d_model
+   * may have information regarding how to construct a model, in the case that
+   * we determined the problem is satisfiable.
    */
-  bool modelBasedRefinement();
+  bool modelBasedRefinement(std::vector<Node>& mlems,
+                            std::vector<Node>& mlemsPp);
   /** returns true if the multiset containing the
    * factors of monomial a is a subset of the multiset
    * containing the factors of monomial b.
@@ -181,12 +181,26 @@ class NonlinearExtension {
    *
    * xts : the list of (non-reduced) extended terms in the current context.
    *
-   * This method returns the number of lemmas added on the output channel of
-   * TheoryArith.
+   * This method adds lemmas to arguments lems, lemsPp, and wlems, each of
+   * which are intended to be sent out on the output channel of TheoryArith
+   * under certain conditions.
+   *
+   * If the set lems or lemsPp is non-empty, then no further processing is
+   * necessary. The last call effort check should terminate and these
+   * lemmas should be sent. The set lemsPp is distinguished from lems since
+   * the preprocess flag on the lemma(...) call should be set to true.
+   *
+   * The "waiting" lemmas wlems contain lemmas that should be sent on the
+   * output channel as a last resort. In other words, only if we are not
+   * able to establish SAT via a call to checkModel(...) should wlems be
+   * considered. This set typically contains tangent plane lemmas.
    */
   int checkLastCall(const std::vector<Node>& assertions,
                     const std::vector<Node>& false_asserts,
-                    const std::vector<Node>& xts);
+                    const std::vector<Node>& xts,
+                    std::vector<Node>& lems,
+                    std::vector<Node>& lemsPp,
+                    std::vector<Node>& wlems);
   //---------------------------------------term utilities
   static bool isArithKind(Kind k);
   static Node mkLit(Node a, Node b, int status, bool isAbsolute = false);
@@ -240,9 +254,15 @@ class NonlinearExtension {
    *
    * For details, see Section 3 of Cimatti et al CADE 2017 under the heading
    * "Detecting Satisfiable Formulas".
+   *
+   * The arguments lemmas and gs store the lemmas and guard literals to be sent
+   * out on the output channel of TheoryArith as lemmas and calls to
+   * ensureLiteral respectively.
    */
   bool checkModel(const std::vector<Node>& assertions,
-                  const std::vector<Node>& false_asserts);
+                  const std::vector<Node>& false_asserts,
+                  std::vector<Node>& lemmas,
+                  std::vector<Node>& gs);
   //---------------------------end check model
 
   /** In the following functions, status states a relationship
@@ -327,18 +347,19 @@ class NonlinearExtension {
   /** Is n entailed with polarity pol in the current context? */
   bool isEntailed(Node n, bool pol);
 
-  /** flush lemmas
-   *
-   * Potentially sends lem on the output channel if lem has not been sent on the
-   * output channel in this context. Returns the number of lemmas sent on the
-   * output channel of TheoryArith.
+  /**
+   * 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
+   * been sent on the output channel of TheoryArith.
    */
-  int flushLemma(Node lem);
+  unsigned filterLemmas(std::vector<Node>& lemmas, std::vector<Node>& out);
+  /** singleton version of above */
+  unsigned filterLemma(Node lem, std::vector<Node>& out);
 
-  /** Potentially sends lemmas to the output channel and clears lemmas. Returns
-   * the number of lemmas sent to the output channel.
+  /**
+   * Send lemmas in out on the output channel of theory of arithmetic.
    */
-  int flushLemmas(std::vector<Node>& lemmas);
+  void sendLemmas(const std::vector<Node>& out, bool preprocess = false);
 
   // Returns the NodeMultiset for an existing monomial.
   const NodeMultiset& getMonomialExponentMap(Node monomial) const;
@@ -439,8 +460,6 @@ class NonlinearExtension {
   /** Stores skolems in the range of the above map */
   std::map<Node, bool> d_tr_is_base;
   std::map< Node, bool > d_tf_initial_refine;
-  /** the list of lemmas we are waiting to flush until after check model */
-  std::vector<Node> d_waiting_lemmas;
 
   void mkPi();
   void getCurrentPiBounds( std::vector< Node >& lemmas );