From c6eb55537a372271906b03201e6fd93645c722d0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 26 Feb 2021 05:05:36 -0800
Subject: [PATCH] Throttle nra solver when progress is being made by
 linearization

---
 src/math/lp/nla_core.cpp   | 10 ++++++++--
 src/math/lp/nra_solver.cpp |  9 +++++++++
 src/math/lp/nra_solver.h   |  1 +
 3 files changed, 18 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 072cd1ac0..354a30099 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1523,8 +1523,14 @@ lbool core::check(vector<lemma>& l_vec) {
               { 1, check3 }};
         check_weighted(3, checks);
 
-        if (!conflict_found() && m_nla_settings.run_nra() && random() % 30 == 0) {
-            ret = m_nra.check();
+        if (!conflict_found() && m_nla_settings.run_nra() && random() % 50 == 0 && 
+            lp_settings().stats().m_nla_calls > 500) {
+            params_ref p;
+            p.set_uint("max_conflicts", 100);
+            m_nra.updt_params(p);
+            ret = m_nra.check(); 
+            p.set_uint("max_conflicts", UINT_MAX);           
+            m_nra.updt_params(p);
             m_stats.m_nra_calls++;
         }
     }
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 05fe7b901..2fd880679 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -235,6 +235,11 @@ struct solver::imp {
         return m_nlsat->am();
     }
 
+    void updt_params(params_ref& p) {
+        m_params.append(p);
+    }
+
+
     std::ostream& display(std::ostream& out) const {
         for (auto m : m_nla_core.emons()) {
             out << "j" << m.var() << " = ";
@@ -276,4 +281,8 @@ nlsat::anum_manager& solver::am() {
     return m_imp->am();
 }
 
+void solver::updt_params(params_ref& p) {
+    m_imp->updt_params(p);
+}
+
 }
diff --git a/src/math/lp/nra_solver.h b/src/math/lp/nra_solver.h
index eaac27655..56dcd69b5 100644
--- a/src/math/lp/nra_solver.h
+++ b/src/math/lp/nra_solver.h
@@ -48,6 +48,7 @@ namespace nra {
 
         nlsat::anum_manager& am();        
 
+        void updt_params(params_ref& p);
 
         /*
           \brief display state