From 845ba7a11e9240e1bbea6192eee147ce2a5553df Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 14 Mar 2021 19:14:44 -0700
Subject: [PATCH] use a large delay for nlsat

---
 src/math/lp/nla_core.cpp             | 14 +++++++++-----
 src/smt/params/smt_params_helper.pyg |  2 +-
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 05cacf720..55a42c2f8 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1518,7 +1518,7 @@ lbool core::check(vector<lemma>& l_vec) {
         ret = bounded_nlsat();
     
 
-    if (l_vec.empty() && !done()) {
+    if (l_vec.empty() && !done() && ret == l_undef) {
         std::function<void(void)> check1 = [&]() { m_order.order_lemma(); };
         std::function<void(void)> check2 = [&]() { m_monotone.monotonicity_lemma(); };
         std::function<void(void)> check3 = [&]() { m_tangents.tangent_lemma(); };
@@ -1529,10 +1529,9 @@ lbool core::check(vector<lemma>& l_vec) {
               { 1, check3 }};
         check_weighted(3, checks);
 
-        if (!conflict_found() && m_nla_settings.run_nra() && should_run_bounded_nlsat() && 
-            lp_settings().stats().m_nla_calls > 500) {
+        unsigned num_calls = lp_settings().stats().m_nla_calls;
+        if (!conflict_found() && m_nla_settings.run_nra() && num_calls % 50 == 0 && num_calls > 500) 
             ret = bounded_nlsat();
-        }
     }
 
     if (l_vec.empty() && !done() && m_nla_settings.run_nra() && ret == l_undef) {
@@ -1555,6 +1554,8 @@ lbool core::check(vector<lemma>& l_vec) {
 }
 
 bool core::should_run_bounded_nlsat() {
+    if (!m_nla_settings.run_nra())
+        return false;
     if (m_nlsat_delay > m_nlsat_fails)
         ++m_nlsat_fails;
     return m_nlsat_delay <= m_nlsat_fails;
@@ -1570,11 +1571,14 @@ lbool core::bounded_nlsat() {
     m_nra.updt_params(p);
     m_stats.m_nra_calls++;
     if (ret == l_undef) 
-        ++m_nlsat_delay;
+        ++m_nlsat_delay;    
     else { 
         m_nlsat_fails = 0;
         m_nlsat_delay /= 2;
     }
+    if (ret == l_true) {
+        m_lemma_vec->reset();
+    }
     return ret;
 }
 
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index c789bf0cc..f0a715e96 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -71,7 +71,7 @@ def_module_params(module_name='smt',
                           ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'),
                           ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'),
                           ('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'),   
-	                  ('arith.nl.delay', UINT, 100, 'number of calls to final check before invoking bounded nlsat check'),                       
+	                  ('arith.nl.delay', UINT, 500, 'number of calls to final check before invoking bounded nlsat check'),                       
                           ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
                           ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'),
                           ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),