From 64e7ff24ad33a1fb297adfda8ec5aa4631ed9dba Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 3 May 2018 12:24:08 -0500
Subject: [PATCH] Option to interleave tangent plane inferences (#1833)

---
 contrib/run-script-smtcomp2018           | 11 ++++++-----
 src/options/arith_options.toml           |  8 ++++++++
 src/smt/smt_engine.cpp                   |  8 ++++++++
 src/theory/arith/nonlinear_extension.cpp |  9 ++++++++-
 4 files changed, 30 insertions(+), 6 deletions(-)

diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index 403f6c8a8..b920152b2 100644
--- a/contrib/run-script-smtcomp2018
+++ b/contrib/run-script-smtcomp2018
@@ -34,7 +34,8 @@ QF_LIA)
   finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
   ;;
 QF_NIA)
-  trywith 300 --nl-ext --nl-ext-tplanes --decision=internal
+  trywith 300 --nl-ext-tplanes --decision=internal
+  trywith 30 --no-nl-ext-tplanes --decision=internal
   # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail
   trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cryptominisat
   trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cryptominisat
@@ -43,10 +44,10 @@ QF_NIA)
   finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
   ;;
 QF_NRA)
-  trywith 300 --nl-ext --nl-ext-tplanes --decision=internal
-  trywith 300 --nl-ext --nl-ext-tplanes --decision=justification --no-nl-ext-factor
-  trywith 30 --nl-ext --nl-ext-tplanes --decision=internal --solve-real-as-int
-  finishwith --nl-ext --nl-ext-tplanes --decision=justification
+  trywith 300 --nl-ext-tplanes --decision=internal
+  trywith 300 --nl-ext-tplanes --decision=justification --no-nl-ext-factor
+  trywith 30 --nl-ext-tplanes --decision=internal --solve-real-as-int
+  finishwith --nl-ext-tplanes --decision=justification
   ;;
 # all logics with UF + quantifiers should either fall under this or special cases below
 ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA)
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
@@ -450,6 +450,14 @@ header = "options/arith_options.h"
   read_only  = true
   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"
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(
-- 
2.30.2