From f2884088cc17b915beae2923b7bacd3d84852e7f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 10 Jan 2020 16:38:13 -0800
Subject: [PATCH] add quota to Grobner

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_core.cpp | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index c3e4a8fd1..c4456f2a6 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1397,6 +1397,10 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const
 
 
 void core::run_grobner() {
+    static unsigned quota = 8;
+    if (quota == 0) {
+        return;
+    }
     lp_settings().stats().m_grobner_calls++;
     configure_grobner();
     m_pdd_grobner.saturate();
@@ -1414,7 +1418,11 @@ void core::run_grobner() {
         IF_VERBOSE(2, verbose_stream() << "grobner conflict\n");
     }
     else {
-        IF_VERBOSE(2, verbose_stream() << "grobner miss\n");
+        if (quota == 1)
+            quota = 0;
+        else
+            quota /= 2; 
+        IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota <<  "\n");
         IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
     }
 }