Option to interleave tangent plane inferences (#1833)

3 files changed, 24 insertions, 1 deletions

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index b2b5f0c31..bb572688b 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -451,6 +451,14 @@ header = "options/arith_options.h"
   help       = "use non-terminating tangent plane strategy for non-linear"
 
 [[option]]
+  name       = "nlExtTangentPlanesInterleave"
+  category   = "regular"
+  long       = "nl-ext-tplanes-interleave"
+  type       = "bool"
+  default    = "false"
+  help       = "interleave tangent plane strategy for non-linear"
+
+[[option]]
   name       = "nlExtTfTangentPlanes"
   category   = "regular"
   long       = "nl-ext-tf-tplanes"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ca01ccd8e..0cff9c8fa 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1726,6 +1726,14 @@ void SmtEngine::setDefaults() {
   if (options::arithRewriteEq()) {
     d_earlyTheoryPP = false;
   }
+  if (d_logic.isPure(THEORY_ARITH) && !d_logic.areRealsUsed())
+  {
+    if (!options::nlExtTangentPlanesInterleave.wasSetByUser())
+    {
+      Trace("smt") << "setting nlExtTangentPlanesInterleave to true" << endl;
+      options::nlExtTangentPlanesInterleave.set(true);
+    }
+  }
 
   // Set decision mode based on logic (if not set by user)
   if(!options::decisionMode.wasSetByUser()) {
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index c2ebc55b8..f790a9f1a 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -1553,6 +1553,13 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   // nt_lemmas.size() << std::endl;  prioritize lemmas that do not
   // introduce new monomials
   lemmas_proc = flushLemmas(lemmas);
+
+  if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave())
+  {
+    lemmas = checkTangentPlanes();
+    lemmas_proc += flushLemmas(lemmas);
+  }
+
   if (lemmas_proc > 0) {
     Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas."
                     << std::endl;
@@ -1590,7 +1597,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
   
   //------------------------------------tangent planes
-  if (options::nlExtTangentPlanes())
+  if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave())
   {
     lemmas = checkTangentPlanes();
     d_waiting_lemmas.insert(