unsound lemma

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/nlsat/nlsat_explain.cpp

@@ -21,6 +21,7 @@ Revision History:
 #include "nlsat/nlsat_evaluator.h"
 #include "math/polynomial/algebraic_numbers.h"
 #include "util/ref_buffer.h"
+extern int ttt;
 
 namespace nlsat {
 
@@ -839,7 +840,6 @@ namespace nlsat {
                 !mk_quadratic_root(k, y, i, p)) {
                 bool_var b = m_solver.mk_root_atom(k, y, i, p);
                 literal l(b, true);
-                TRACE(nlsat_explain, tout << "adding literal\n"; display(tout, l); tout << "\n";);
                 add_literal(l);
             }
         }
@@ -1013,6 +1013,13 @@ namespace nlsat {
                 // Otherwise, the isolate_roots procedure will assume p is a constant polynomial.
                 m_am.isolate_roots(p, undef_var_assignment(m_assignment, y), roots);
                 unsigned num_roots = roots.size();
+                TRACE(nlsat_explain,
+                      tout << "isolated roots for "; display_var(tout, y);
+                      tout << " with polynomial: " << p << "\n";
+                      for (unsigned ri = 0; ri < num_roots; ++ri) {
+                          m_am.display_decimal(tout << "  root[" << (ri+1) << "] = ", roots[ri]);
+                          tout << "\n";
+                      });
                 bool all_lt = true;
                 for (unsigned i = 0; i < num_roots; i++) {
                     int s = m_am.compare(y_val, roots[i]);
@@ -1648,7 +1655,7 @@ namespace nlsat {
             var max_x = max_var(m_ps);
             TRACE(nlsat_explain, tout << "polynomials in the conflict:\n"; display(tout, m_ps); tout << "\n";);
             elim_vanishing(m_ps);
-            TRACE(nlsat_explain, tout << "elim vanishing\n"; display(tout, m_ps); tout << "\n";);
+            TRACE(nlsat_explain, tout << "after elim_vanishing m_ps:\n"; display(tout, m_ps); tout << "\n";);
             project(m_ps, max_x);
             TRACE(nlsat_explain, tout << "after projection\n"; display(tout, m_ps); tout << "\n";);
         }
@@ -1659,6 +1666,7 @@ namespace nlsat {
                 m_core2.append(num, ls);
                 var max = max_var(num, ls);
                 SASSERT(max != null_var);
+                TRACE(nlsat_explain, display(tout << "core before normalization\n", m_core2) << "\n";);
                 normalize(m_core2, max);
                 TRACE(nlsat_explain, display(tout << "core after normalization\n", m_core2) << "\n";);
                 simplify(m_core2, max);
@@ -1667,6 +1675,7 @@ namespace nlsat {
                 m_core2.reset();
             }
             else {
+                TRACE(nlsat_explain, display(tout << "core befor normalization\n", m_core2) << "\n";);
                 main(num, ls);
             }
         }
@@ -1751,8 +1760,9 @@ namespace nlsat {
                 process2(num, ls);
             }
         }
-      
+
         void operator()(unsigned num, literal const * ls, scoped_literal_vector & result) {
+            ttt++;
             SASSERT(check_already_added());
             SASSERT(num > 0);
             TRACE(nlsat_explain, 
@@ -1760,6 +1770,11 @@ namespace nlsat {
                   display(tout, num, ls) << "\n";
                   m_solver.display_assignment(tout);
                   );
+            if (max_var(num, ls) == 0 && !m_assignment.is_assigned(0)) {
+                TRACE(nlsat_explain, tout << "all literals use unassigned max var; returning justification\n";);
+                result.reset();
+                return;
+            }
             m_result = &result;
             process(num, ls);
             reset_already_added();

src/nlsat/nlsat_solver.cpp

@@ -40,6 +40,8 @@ Revision History:
 #include "nlsat/nlsat_simple_checker.h"
 #include "nlsat/nlsat_variable_ordering_strategy.h"
 
+int ttt = 0;
+
 #define NLSAT_EXTRA_VERBOSE
 
 #ifdef NLSAT_EXTRA_VERBOSE
@@ -750,6 +752,14 @@ namespace nlsat {
             m_atoms[b] = new_atom;
             new_atom->m_bool_var = b;
             m_pm.inc_ref(new_atom->p());
+            TRACE(nlsat_solver,
+                  tout << "created root literal b" << b << ": ";
+                  display(tout, literal(b, false)) << "\n";
+                  tout << "    kind: " << k << ", index: " << i << ", variable: x" << x << "\n";
+                  tout << "    polynomial: ";
+                  display_polynomial(tout, new_atom->p(), m_display_var);
+                  tout << "\n";
+                );
             return b;
         }
 
@@ -1115,20 +1125,47 @@ namespace nlsat {
         }
 
         void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) {
-            ++m_lemma_count;
+            if (!is_valid)
-            out << "(set-logic ALL)\n";
+                return;
-            if (is_valid) {
+            if (false && ttt != 219)
-                display_smt2_bool_decls(out);
+                return;
-                display_smt2_arith_decls(out);
+
+            // Collect arithmetic variables referenced by cls.
+            std::vector<unsigned> arith_vars = collect_vars_on_clause(n, cls);
+
+            // Collect uninterpreted Boolean variables referenced by cls.
+            bool_vector seen_bool;
+            svector<bool_var> bool_vars;
+            for (unsigned i = 0; i < n; ++i) {
+                bool_var b = cls[i].var();
+                if (seen_bool.get(b, false))
+                    continue;
+                seen_bool.setx(b, true, false);
+                if (b != 0 && m_atoms[b] == nullptr)
+                    bool_vars.push_back(b);
             }
-            else             
+
-                display_smt2(out);            
+            out << "(set-logic ALL)\n";
+
+            for (bool_var b : bool_vars) {
+                out << "(declare-fun b" << b << " () Bool)\n";
+            }
+            for (unsigned x : arith_vars) {
+                out << "(declare-fun ";
+                m_display_var(out, x);
+                out << " () " << (is_int(x) ? "Int" : "Real") << ")\n";
+            }
+
             for (unsigned i = 0; i < n; ++i) 
                 display_smt2(out << "(assert ", ~cls[i]) << ")\n";
-            display(out << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n";
+            display(out << "(echo \"#" << ttt << " ", n, cls) << "\")\n";
             out << "(check-sat)\n(reset)\n";
 
-            TRACE(nlsat, display(tout << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n");
+            TRACE(nlsat, display(tout << "(echo \"#" << ttt << " ", n, cls) << "\")\n");
+            if (false && ttt == 219) {
+                std::cout << "early exit()\n";
+                exit(0);
+            }
         }
 
         clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {
@@ -1599,7 +1636,16 @@ namespace nlsat {
                     TRACE(nlsat_inf_set, tout << "infeasible set + current set = R, skip literal\n";
                           display(tout, cls) << "\n";
                           display_assignment_for_clause(tout, cls);
-                          m_ism.display(tout, tmp); tout << "\n";
+                          m_ism.display(tout, tmp) << "\n";
+                          literal_vector inf_lits;
+                          ptr_vector<clause> inf_clauses;
+                          m_ism.get_justifications(tmp, inf_lits, inf_clauses);
+                          if (!inf_lits.empty()) {
+                              tout << "Interval witnesses:\n";
+                              for (literal inf_lit : inf_lits) {
+                                  display(tout << "  ", inf_lit) << "\n";
+                              }
+                          }
                         );
                     R_propagate(~l, tmp, false);
                     continue;
@@ -2408,6 +2454,15 @@ namespace nlsat {
             unsigned top = m_trail.size();
             bool found_decision;
             while (true) {
+                if (ttt >= 10) {
+                   enable_trace("nlsat_explain");
+                   enable_trace("nlsat");
+                   enable_trace("nlsat_resolve");
+                   enable_trace("nlsat_interval");
+                   enable_trace("nlsat_solver");
+                   enable_trace("nlsat_mathematica");
+                   enable_trace("nlsat_inf_set");
+                }
                 found_decision = false;
                 while (m_num_marks > 0) {
                     checkpoint();
@@ -2427,6 +2482,10 @@ namespace nlsat {
                                 break;
                             case justification::LAZY:
                                 resolve_lazy_justification(b, *(jst.get_lazy()));
+                                if (ttt == 48) {
+                                    TRACE(nlsat_solver, tout << "early exit\n";);
+                                    exit(0);
+                                }
                                 break;
                             case justification::DECISION:
                                 SASSERT(m_num_marks == 0);

src/test/main.cpp

@@ -227,6 +227,7 @@ int main(int argc, char ** argv) {
     TST(prime_generator);
     TST(permutation);
     TST(nlsat);
+    TST(nlsat_mv);
     TST(zstring);
     if (test_all) return 0;
     TST(ext_numeral);

src/test/nlsat.cpp

@@ -717,6 +717,104 @@ static void tst10() {
     std::cout << "\n";
 }
 
+void tst_nlsat_mv() {
+    params_ref      ps;
+    reslimit        rlim;
+    nlsat::solver s(rlim, ps, false);
+    anum_manager & am     = s.am();
+    nlsat::pmanager & pm  = s.pm();
+    nlsat::assignment assignment(am);
+    nlsat::explain& ex    = s.get_explain();
+
+    // Regression: reproduce lemma 114 where main_operator adds spurious bounds.
+    nlsat::var x0 = s.mk_var(false);
+    nlsat::var x1 = s.mk_var(false);
+
+    polynomial_ref _x0(pm), _x1(pm);
+    _x0 = pm.mk_polynomial(x0);
+    _x1 = pm.mk_polynomial(x1);
+
+    polynomial_ref x0_sq(pm), x0_cu(pm), x0_4(pm), x0_5(pm);
+    x0_sq = _x0 * _x0;
+    x0_cu = x0_sq * _x0;
+    x0_4 = x0_cu * _x0;
+    x0_5 = x0_4 * _x0;
+
+    polynomial_ref x1_sq(pm), x1_cu(pm), x1_4(pm), x1_5(pm);
+    x1_sq = _x1 * _x1;
+    x1_cu = x1_sq * _x1;
+    x1_4 = x1_cu * _x1;
+    x1_5 = x1_4 * _x1;
+
+    polynomial_ref root_arg(pm);
+    root_arg =
+        x1_5 +
+        (_x0 * x1_4) -
+        (18 * x1_4) -
+        (2 * x0_sq * x1_cu) -
+        (2 * x0_cu * x1_sq) +
+        (36 * x0_sq * x1_sq) +
+        (1296 * _x0 * x1_sq) +
+        (864 * x1_sq) +
+        (x0_4 * _x1) +
+        (1296 * x0_sq * _x1) +
+        (6048 * _x0 * _x1) +
+        x0_5 -
+        (18 * x0_4) +
+        (864 * x0_sq);
+    // should be (x1^5 + x0 x1^4 - 18 x1^4 - 2 x0^2 x1^3 - 2 x0^3 x1^2 + 36 x0^2 x1^2 + 1296 x0 x1^2 + 864 x1^2 + x0^4 x1 + 1296 x0^2 x1 + 6048 x0 x1 + x0^5 - 18 x0^4 + 864 x0^2)
+    std::cout << "big poly:" <<  root_arg << std::endl;
+    nlsat::literal x1_gt_0 = mk_gt(s, _x1);
+    nlsat::bool_var root_gt = s.mk_root_atom(nlsat::atom::ROOT_GT, x1, 3, root_arg.get());
+    nlsat::literal x1_gt_root(root_gt, false);
+
+    nlsat::scoped_literal_vector lits(s);
+    lits.push_back(x1_gt_0);
+    lits.push_back(~x1_gt_root); // !(x1 > root[3](root_arg))
+
+    scoped_anum one(am), one_dup(am);
+    am.set(one, 1);
+    assignment.set(x0, one);
+    s.set_rvalues(assignment);
+
+    nlsat::scoped_literal_vector result(s);
+    ex.main_operator(lits.size(), lits.data(), result);
+
+    std::cout << "main_operator root regression core:\n";
+    s.display(std::cout, lits.size(), lits.data());
+    s.display(std::cout << "\n==>\n", result.size(), result.data());
+    std::cout << "\n";
+
+    // Assign x1 only after the lemma is produced.
+    am.set(one_dup, 1);
+    assignment.set(x1, one_dup);
+    s.set_rvalues(assignment);
+
+    small_object_allocator allocator;
+    nlsat::evaluator eval(s, assignment, pm, allocator);
+    std::cout << "input literal values at x0 = 1, x1 = 1:\n";
+    for (nlsat::literal l : lits) {
+        nlsat::atom* a = s.bool_var2atom(l.var());
+        if (!a) {
+            std::cout << "conversion bug\n";
+        }
+        bool value = a ? eval.eval(a, l.sign()) : false;
+        s.display(std::cout << "  ", l);
+        std::cout << " -> " << (value ? "true" : "false") << "\n";
+    }
+    std::cout << "new literal values at x0 = 1, x1 = 1:\n";
+    for (nlsat::literal l : result) {
+        nlsat::atom* a = s.bool_var2atom(l.var());
+        bool value = a ? eval.eval(a, l.sign()) : false;
+        if (!a) {
+            std::cout << "conversion bug\n";
+        }
+        s.display(std::cout << "  ", l);
+        std::cout << " -> " << (value ? "true" : "false") << "\n";
+    }
+    std::cout << "\n";
+}
+
 static void tst11() {
     params_ref      ps;
     reslimit        rlim;
@@ -791,6 +889,8 @@ x7 := 1
 }
 
 void tst_nlsat() {
+    std::cout << "tst_mv\n"; exit(1);
+    std::cout << "------------------\n";
     tst11();
     std::cout << "------------------\n";
     return;