Update option --nl-ext to enable/disable incremental linearization solver only (#4649)

Previously, this option disabled/enabled the entire non-linear solver. This is in preparation for new CAD techniques.

I am intentionally not renaming "--nl-ext" to e.g. "--nl-inc-lin" for the sake of not breaking user configurations.

It makes some minor changes to clean the interface in a few places and to not enable the non-linear solver in linear logics.

8 files changed, 153 insertions, 135 deletions

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 0bfc26338..ce747b62d 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -435,7 +435,7 @@ header = "options/arith_options.h"
   type       = "bool"
   default    = "true"
   read_only  = true
-  help       = "extended approach to non-linear"
+  help       = "incremental linearization approach to non-linear"
 
 [[option]]
   name       = "nlExtResBound"
@@ -444,7 +444,7 @@ header = "options/arith_options.h"
   type       = "bool"
   default    = "false"
   read_only  = true
-  help       = "use resolution-style inference for inferring new bounds"
+  help       = "use resolution-style inference for inferring new bounds in non-linear incremental linearization solver"
 
 [[option]]
   name       = "nlExtFactor"
@@ -453,7 +453,7 @@ header = "options/arith_options.h"
   type       = "bool"
   default    = "true"
   read_only  = true
-  help       = "use factoring inference in non-linear solver"
+  help       = "use factoring inference in non-linear incremental linearization solver"
 
 [[option]]
   name       = "nlExtTangentPlanes"
@@ -462,7 +462,7 @@ header = "options/arith_options.h"
   type       = "bool"
   default    = "false"
   read_only  = true
-  help       = "use non-terminating tangent plane strategy for non-linear"
+  help       = "use non-terminating tangent plane strategy for non-linear incremental linearization solver"
 
 [[option]]
   name       = "nlExtTangentPlanesInterleave"
@@ -470,7 +470,7 @@ header = "options/arith_options.h"
   long       = "nl-ext-tplanes-interleave"
   type       = "bool"
   default    = "false"
-  help       = "interleave tangent plane strategy for non-linear"
+  help       = "interleave tangent plane strategy for non-linear incremental linearization solver"
 
 [[option]]
   name       = "nlExtTfTangentPlanes"
@@ -479,7 +479,7 @@ header = "options/arith_options.h"
   type       = "bool"
   default    = "true"
   read_only  = true
-  help       = "use non-terminating tangent plane strategy for transcendental functions for non-linear"
+  help       = "use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver"
 
 [[option]]
   name       = "nlExtEntailConflicts"
@@ -497,7 +497,7 @@ header = "options/arith_options.h"
   type       = "bool"
   default    = "true"
   read_only  = true
-  help       = "do rewrites in non-linear solver"
+  help       = "do context-dependent simplification based on rewrites in non-linear solver"
 
 [[option]]
   name       = "nlExtPurify"
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index afc8eb7bb..d663352f7 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -1442,12 +1442,6 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
     disableModels = true;
     sOptNoModel = "minisat-elimination";
   }
-  else if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
-           && !options::nlExt())
-  {
-    disableModels = true;
-    sOptNoModel = "nonlinear arithmetic without nl-ext";
-  }
   else if (options::globalNegate())
   {
     disableModels = true;
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index bf27ecbb3..d471bf0f6 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -211,13 +211,12 @@ int NlModel::compareValue(Node i, Node j, bool isAbsolute) const
 }
 
 bool NlModel::checkModel(const std::vector<Node>& assertions,
-                         const std::vector<Node>& false_asserts,
                          unsigned d,
                          std::vector<NlLemma>& lemmas,
                          std::vector<Node>& gs)
 {
   Trace("nl-ext-cm-debug") << "  solve for equalities..." << std::endl;
-  for (const Node& atom : false_asserts)
+  for (const Node& atom : assertions)
   {
     // see if it corresponds to a univariate polynomial equation of degree two
     if (atom.getKind() == EQUAL)
@@ -489,6 +488,7 @@ bool NlModel::solveEqualitySimple(Node eq,
     {
       if (seq.getConst<bool>())
       {
+        // already true
         d_check_model_solved[eq] = Node::null();
         return true;
       }
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index 86bac88a9..fdce446fc 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -151,7 +151,6 @@ class NlModel
    * d is a degree indicating how precise our computations are.
    */
   bool checkModel(const std::vector<Node>& assertions,
-                  const std::vector<Node>& false_asserts,
                   unsigned d,
                   std::vector<NlLemma>& lemmas,
                   std::vector<Node>& gs);
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index 087d7681a..5ded7d3d0 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -380,17 +380,18 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
   // get the presubstitution
   Trace("nl-ext-cm-debug") << "  apply pre-substitution..." << std::endl;
   std::vector<Node> passertions = assertions;
-
-  // preprocess the assertions with the trancendental solver
-  if (!d_trSlv.preprocessAssertionsCheckModel(passertions))
+  if (options::nlExt())
   {
-    return false;
+    // preprocess the assertions with the trancendental solver
+    if (!d_trSlv.preprocessAssertionsCheckModel(passertions))
+    {
+      return false;
+    }
   }
 
   Trace("nl-ext-cm") << "-----" << std::endl;
   unsigned tdegree = d_trSlv.getTaylorDegree();
-  bool ret =
-      d_model.checkModel(passertions, false_asserts, tdegree, lemmas, gs);
+  bool ret = d_model.checkModel(passertions, tdegree, lemmas, gs);
   return ret;
 }
 
@@ -400,14 +401,16 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                                       std::vector<NlLemma>& lems,
                                       std::vector<NlLemma>& wlems)
 {
-  // initialize the non-linear solver
-  d_nlSlv.initLastCall(assertions, false_asserts, xts);
-  // initialize the trancendental function solver
   std::vector<NlLemma> lemmas;
-  d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas);
-
-  // process lemmas that may have been generated by the transcendental solver
-  filterLemmas(lemmas, lems);
+  if (options::nlExt())
+  {
+    // initialize the non-linear solver
+    d_nlSlv.initLastCall(assertions, false_asserts, xts);
+    // initialize the trancendental function solver
+    d_trSlv.initLastCall(assertions, false_asserts, xts, lemmas);
+    // process lemmas that may have been generated by the transcendental solver
+    filterLemmas(lemmas, lems);
+  }
   if (!lems.empty())
   {
     Trace("nl-ext") << "  ...finished with " << lems.size()
@@ -416,7 +419,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
 
   //----------------------------------- possibly split on zero
-  if (options::nlExtSplitZero())
+  if (options::nlExt() && options::nlExtSplitZero())
   {
     Trace("nl-ext") << "Get zero split lemmas..." << std::endl;
     lemmas = d_nlSlv.checkSplitZero();
@@ -430,90 +433,34 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
 
   //-----------------------------------initial lemmas for transcendental
-  //functions
-  lemmas = d_trSlv.checkTranscendentalInitialRefine();
-  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 = d_nlSlv.checkMonomialSign();
-  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 = d_trSlv.checkTranscendentalMonotonic();
-  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
-  for (unsigned c = 0; c < 3; c++)
+  if (options::nlExt())
   {
-    // c is effort level
-    lemmas = d_nlSlv.checkMonomialMagnitude(c);
-    unsigned nlem = lemmas.size();
+    // functions
+    lemmas = d_trSlv.checkTranscendentalInitialRefine();
     filterLemmas(lemmas, lems);
     if (!lems.empty())
     {
-      Trace("nl-ext") << "  ...finished with " << lems.size()
-                      << " new lemmas (out of possible " << nlem << ")."
+      Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
                       << std::endl;
       return lems.size();
     }
   }
 
-  //-----------------------------------inferred bounds lemmas
-  //  e.g. x >= t => y*x >= y*t
-  std::vector<NlLemma> nt_lemmas;
-  lemmas =
-      d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts);
-  // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " <<
-  // nt_lemmas.size() << std::endl;  prioritize lemmas that do not
-  // introduce new monomials
-  filterLemmas(lemmas, lems);
-
-  if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave())
+  // main calls to nlExt
+  if (options::nlExt())
   {
-    lemmas = d_nlSlv.checkTangentPlanes();
+    //---------------------------------lemmas based on sign (comparison to zero)
+    lemmas = d_nlSlv.checkMonomialSign();
     filterLemmas(lemmas, lems);
-  }
-
-  if (!lems.empty())
-  {
-    Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
-                    << std::endl;
-    return lems.size();
-  }
-
-  // from inferred bound inferences : now do ones that introduce new terms
-  filterLemmas(nt_lemmas, lems);
-  if (!lems.empty())
-  {
-    Trace("nl-ext") << "  ...finished with " << lems.size()
-                    << " new (monomial-introducing) lemmas." << std::endl;
-    return lems.size();
-  }
+    if (!lems.empty())
+    {
+      Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
+                      << std::endl;
+      return lems.size();
+    }
 
-  //------------------------------------factoring lemmas
-  //   x*y + x*z >= t => exists k. k = y + z ^ x*k >= t
-  if (options::nlExtFactor())
-  {
-    lemmas = d_nlSlv.checkFactoring(assertions, false_asserts);
+    //-----------------------------------monotonicity of transdental functions
+    lemmas = d_trSlv.checkTranscendentalMonotonic();
     filterLemmas(lemmas, lems);
     if (!lems.empty())
     {
@@ -521,33 +468,98 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
                       << std::endl;
       return lems.size();
     }
-  }
 
-  //------------------------------------resolution bound inferences
-  //  e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
-  if (options::nlExtResBound())
-  {
-    lemmas = d_nlSlv.checkMonomialInferResBounds();
+    //------------------------lemmas based on magnitude of non-zero monomials
+    for (unsigned c = 0; c < 3; c++)
+    {
+      // c is effort level
+      lemmas = d_nlSlv.checkMonomialMagnitude(c);
+      unsigned nlem = lemmas.size();
+      filterLemmas(lemmas, lems);
+      if (!lems.empty())
+      {
+        Trace("nl-ext") << "  ...finished with " << lems.size()
+                        << " new lemmas (out of possible " << nlem << ")."
+                        << std::endl;
+        return lems.size();
+      }
+    }
+
+    //-----------------------------------inferred bounds lemmas
+    //  e.g. x >= t => y*x >= y*t
+    std::vector<NlLemma> nt_lemmas;
+    lemmas =
+        d_nlSlv.checkMonomialInferBounds(nt_lemmas, assertions, false_asserts);
+    // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " <<
+    // nt_lemmas.size() << std::endl;  prioritize lemmas that do not
+    // introduce new monomials
     filterLemmas(lemmas, lems);
+
+    if (options::nlExtTangentPlanes()
+        && options::nlExtTangentPlanesInterleave())
+    {
+      lemmas = d_nlSlv.checkTangentPlanes();
+      filterLemmas(lemmas, lems);
+    }
+
     if (!lems.empty())
     {
       Trace("nl-ext") << "  ...finished with " << lems.size() << " new lemmas."
                       << std::endl;
       return lems.size();
     }
-  }
 
-  //------------------------------------tangent planes
-  if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave())
-  {
-    lemmas = d_nlSlv.checkTangentPlanes();
-    filterLemmas(lemmas, wlems);
-  }
-  if (options::nlExtTfTangentPlanes())
-  {
-    lemmas = d_trSlv.checkTranscendentalTangentPlanes();
-    filterLemmas(lemmas, wlems);
+    // from inferred bound inferences : now do ones that introduce new terms
+    filterLemmas(nt_lemmas, lems);
+    if (!lems.empty())
+    {
+      Trace("nl-ext") << "  ...finished with " << lems.size()
+                      << " new (monomial-introducing) lemmas." << std::endl;
+      return lems.size();
+    }
+
+    //------------------------------------factoring lemmas
+    //   x*y + x*z >= t => exists k. k = y + z ^ x*k >= t
+    if (options::nlExtFactor())
+    {
+      lemmas = d_nlSlv.checkFactoring(assertions, false_asserts);
+      filterLemmas(lemmas, lems);
+      if (!lems.empty())
+      {
+        Trace("nl-ext") << "  ...finished with " << lems.size()
+                        << " new lemmas." << std::endl;
+        return lems.size();
+      }
+    }
+
+    //------------------------------------resolution bound inferences
+    //  e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t
+    if (options::nlExtResBound())
+    {
+      lemmas = d_nlSlv.checkMonomialInferResBounds();
+      filterLemmas(lemmas, lems);
+      if (!lems.empty())
+      {
+        Trace("nl-ext") << "  ...finished with " << lems.size()
+                        << " new lemmas." << std::endl;
+        return lems.size();
+      }
+    }
+
+    //------------------------------------tangent planes
+    if (options::nlExtTangentPlanes()
+        && !options::nlExtTangentPlanesInterleave())
+    {
+      lemmas = d_nlSlv.checkTangentPlanes();
+      filterLemmas(lemmas, wlems);
+    }
+    if (options::nlExtTfTangentPlanes())
+    {
+      lemmas = d_trSlv.checkTranscendentalTangentPlanes();
+      filterLemmas(lemmas, wlems);
+    }
   }
+
   Trace("nl-ext") << "  ...finished with " << wlems.size() << " waiting lemmas."
                   << std::endl;
 
@@ -774,7 +786,8 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems)
       }
 
       // we are incomplete
-      if (options::nlExtIncPrecision() && d_model.usedApproximate())
+      if (options::nlExt() && options::nlExtIncPrecision()
+          && d_model.usedApproximate())
       {
         d_trSlv.incrementTaylorDegree();
         needsRecheck = true;
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 7310233f1..cb436bda7 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -300,7 +300,7 @@ class NonlinearExtension
   /** The nonlinear extension object
    *
    * This is the subsolver responsible for running the procedure for
-   * constraints involving nonlinear mulitplication.
+   * constraints involving nonlinear mulitplication, Cimatti et al., TACAS 2017.
    */
   NlSolver d_nlSlv;
   /**
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c25090f38..30b8ed01d 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -40,7 +40,9 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
     , d_proofRecorder(nullptr)
 {
   smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer);
-  if (options::nlExt()) {
+  // if logic is non-linear
+  if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
+  {
     setupExtTheory();
     getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT);
     getExtTheory()->addFunctionKind(kind::EXPONENTIAL);
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 7b7f5a411..d0da29e7a 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -158,7 +158,9 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
       d_statistics(),
       d_opElim(logicInfo)
 {
-  if( options::nlExt() ){
+  // only need to create if non-linear logic
+  if (logicInfo.isTheoryEnabled(THEORY_ARITH) && !logicInfo.isLinear())
+  {
     d_nonlinearExtension = new nl::NonlinearExtension(
         containing, d_congruenceManager.getEqualityEngine());
   }
@@ -1263,7 +1265,8 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){
       throw LogicException("A non-linear fact was asserted to arithmetic in a linear logic.");
     }
 
-    if( !options::nlExt() ){
+    if (d_nonlinearExtension == nullptr)
+    {
       d_nlIncomplete = true;
     }
 
@@ -1274,7 +1277,8 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){
 
     markSetup(vlNode);
   }else{
-    if( !options::nlExt() ){
+    if (d_nonlinearExtension == nullptr)
+    {
       if( vlNode.getKind()==kind::EXPONENTIAL || vlNode.getKind()==kind::SINE || 
           vlNode.getKind()==kind::COSINE || vlNode.getKind()==kind::TANGENT ){
         d_nlIncomplete = true;
@@ -1440,8 +1444,9 @@ void TheoryArithPrivate::setupAtom(TNode atom) {
 
 void TheoryArithPrivate::preRegisterTerm(TNode n) {
   Debug("arith::preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
-  
-  if( options::nlExt() ){
+
+  if (d_nonlinearExtension != nullptr)
+  {
     d_containing.getExtTheory()->registerTermRec( n );
   }
 
@@ -3322,7 +3327,8 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
   }
 
   if(effortLevel == Theory::EFFORT_LAST_CALL){
-    if( options::nlExt() ){
+    if (d_nonlinearExtension != nullptr)
+    {
       d_nonlinearExtension->check(effortLevel);
     }
     return;
@@ -3646,7 +3652,8 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){
   }//if !emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()
 
   if(!emmittedConflictOrSplit && effortLevel>=Theory::EFFORT_FULL){
-    if( options::nlExt() ){
+    if (d_nonlinearExtension != nullptr)
+    {
       d_nonlinearExtension->check( effortLevel );
     }
   }
@@ -3849,7 +3856,8 @@ void TheoryArithPrivate::debugPrintModel(std::ostream& out) const{
 }
 
 bool TheoryArithPrivate::needsCheckLastEffort() {
-  if( options::nlExt() ){
+  if (d_nonlinearExtension != nullptr)
+  {
     return d_nonlinearExtension->needsCheckLastEffort();
   }else{
     return false;
@@ -3886,7 +3894,8 @@ Node TheoryArithPrivate::explain(TNode n)
 }
 
 bool TheoryArithPrivate::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
-  if( options::nlExt() ){
+  if (d_nonlinearExtension != nullptr)
+  {
     return d_nonlinearExtension->getCurrentSubstitution( effort, vars, subs, exp );
   }else{
     return false;
@@ -3895,7 +3904,8 @@ bool TheoryArithPrivate::getCurrentSubstitution( int effort, std::vector< Node >
 
 bool TheoryArithPrivate::isExtfReduced(int effort, Node n, Node on,
                                        std::vector<Node>& exp) {
-  if (options::nlExt()) {
+  if (d_nonlinearExtension != nullptr)
+  {
     std::pair<bool, Node> reduced =
         d_nonlinearExtension->isExtfReduced(effort, n, on, exp);
     if (!reduced.second.isNull()) {
@@ -4143,7 +4153,7 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
 
         Node qNode = mkRationalNode(qmodel);
         Debug("arith::collectModelInfo") << "m->assertEquality(" << term << ", " << qmodel << ", true)" << endl;
-        if (options::nlExt())
+        if (d_nonlinearExtension != nullptr)
         {
           // Let non-linear extension inspect the values before they are sent
           // to the theory model.
@@ -4162,7 +4172,7 @@ bool TheoryArithPrivate::collectModelInfo(TheoryModel* m)
       }
     }
   }
-  if (options::nlExt())
+  if (d_nonlinearExtension != nullptr)
   {
     // Non-linear may repair values to satisfy non-linear constraints (see
     // documentation for NonlinearExtension::interceptModel).
@@ -4312,7 +4322,7 @@ void TheoryArithPrivate::presolve(){
     outputLemma(lem);
   }
 
-  if (options::nlExt())
+  if (d_nonlinearExtension != nullptr)
   {
     d_nonlinearExtension->presolve();
   }