add facility to experiment with nla justified conflicts from Grobner equations

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/grobner/pdd_simplifier.cpp

@@ -89,7 +89,7 @@ namespace dd {
 
     bool simplifier::simplify_linear_step(bool binary) {
         TRACE("dd.solver", tout << "binary " << binary << "\n";);
-        IF_VERBOSE(2, verbose_stream() << "binary " << binary << "\n");
+        IF_VERBOSE(3, verbose_stream() << "binary " << binary << "\n");
         equation_vector linear;
         for (equation* e : s.m_to_simplify) {
             pdd p = e->poly();
@@ -184,7 +184,7 @@ namespace dd {
      */
     bool simplifier::simplify_cc_step() {
         TRACE("dd.solver", tout << "cc\n";);
-        IF_VERBOSE(2, verbose_stream() << "cc\n");
+        IF_VERBOSE(3, verbose_stream() << "cc\n");
         u_map<equation*> los;
         bool reduced = false;
         unsigned j = 0;
@@ -217,7 +217,7 @@ namespace dd {
     */
     bool simplifier::simplify_leaf_step() {
         TRACE("dd.solver", tout << "leaf\n";);
-        IF_VERBOSE(2, verbose_stream() << "leaf\n");
+        IF_VERBOSE(3, verbose_stream() << "leaf\n");
         use_list_t use_list = get_use_list();
         equation_vector leaves;
         for (unsigned i = 0; i < s.m_to_simplify.size(); ++i) {
@@ -262,7 +262,7 @@ namespace dd {
     */
     bool simplifier::simplify_elim_pure_step() {
         TRACE("dd.solver", tout << "pure\n";);
-        IF_VERBOSE(2, verbose_stream() << "pure\n");
+        IF_VERBOSE(3, verbose_stream() << "pure\n");
         use_list_t use_list = get_use_list();        
         unsigned j = 0;
         for (equation* e : s.m_to_simplify) {

src/math/lp/nla_grobner.cpp

@@ -36,7 +36,7 @@ namespace nla {
         if (m_quota == 0)
             m_quota = c().params().arith_nl_gr_q();                    
 
-        if (m_quota == 1)
+        if (false && m_quota == 1)
             return;
 
         lp_settings().stats().m_grobner_calls++;
@@ -316,7 +316,11 @@ namespace nla {
                       c().m_intervals.display(tout << "j" << j << " ", a); tout << " ";
                   }
                   tout << "\n");
-        
+            
+#if 0
+            if (add_nla_conflict(e)) 
+                return true;
+#endif
             return false;
         }
         eval.get_interval<dd::w_dep::with_deps>(e.poly(), i_wd);  
@@ -329,6 +333,10 @@ namespace nla {
             return true;
         }
         else {
+#if 0
+            if (add_nla_conflict(e)) 
+                return true;
+#endif
             TRACE("grobner", m_solver.display(tout << "no conflict ", e) << "\n");
             return false;
         }
@@ -567,14 +575,30 @@ namespace nla {
         tout << "\n");
     }
 
-    void grobner::check_missing_propagation(const dd::solver::equation& e) { 
+    bool grobner::is_nla_conflict(const dd::solver::equation& eq) {
         vector<dd::pdd> eqs;
-        eqs.push_back(e.poly());
+        eqs.push_back(eq.poly());
-        lbool r = c().m_nra.check(eqs);
+        return l_false == c().m_nra.check(eqs);
-        CTRACE("grobner", r == l_false, m_solver.display(tout << "missed conflict ", e););
+    }
-        if (r != l_true) 
+
+    bool grobner::add_nla_conflict(const dd::solver::equation& eq) {
+        if (is_nla_conflict(eq)) {
+            new_lemma lemma(m_core,"nla-conflict");
+            lp::explanation exp;
+            explain(eq, exp);
+            lemma &= exp;
+            return true;
+        }
+        return false;
+    }
+
+
+    void grobner::check_missing_propagation(const dd::solver::equation& e) { 
+        bool is_confl = is_nla_conflict(e);
+        CTRACE("grobner", is_confl, m_solver.display(tout << "missed conflict ", e););
+        if (is_confl) 
             return;
-        r = c().m_nra.check_tight(e.poly());
+        lbool r = c().m_nra.check_tight(e.poly());
         CTRACE("grobner", r == l_false, m_solver.display(tout << "tight equality ", e););
     }
 

src/math/lp/nla_grobner.h

@@ -43,6 +43,8 @@ namespace nla {
         void add_dependencies(new_lemma& lemma, const dd::solver::equation& eq);
         void explain(const dd::solver::equation& eq, lp::explanation& exp);
 
+        bool is_nla_conflict(const dd::solver::equation& eq);
+        bool add_nla_conflict(const dd::solver::equation& eq);
         void check_missing_propagation(const dd::solver::equation& eq);
 
         // setup