diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 2d3b89928..25e4c8d25 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/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(); diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 084e3a479..d023bb65e 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/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; - out << "(set-logic ALL)\n"; - if (is_valid) { - display_smt2_bool_decls(out); - display_smt2_arith_decls(out); + if (!is_valid) + return; + if (false && ttt != 219) + return; + + // Collect arithmetic variables referenced by cls. + std::vector arith_vars = collect_vars_on_clause(n, cls); + + // Collect uninterpreted Boolean variables referenced by cls. + bool_vector seen_bool; + svector 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 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); diff --git a/src/test/main.cpp b/src/test/main.cpp index 5e416c4af..72013c86c 100644 --- a/src/test/main.cpp +++ b/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); diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 8b283247d..7d00fa033 100644 --- a/src/test/nlsat.cpp +++ b/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;