diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index e04b95a40..2cbf80849 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -384,7 +384,8 @@ namespace nlsat { int eval_sign(poly * p) { // TODO: check if it is useful to cache results SASSERT(m_assignment.is_assigned(max_var(p))); - return m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment); + int r = m_am.eval_sign_at(polynomial_ref(p, m_pm), m_assignment); + return r > 0 ? +1 : (r < 0 ? 0 : -1); } bool satisfied(int sign, atom::kind k) { diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 523e5a929..fae9a1c69 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -920,7 +920,7 @@ namespace nlsat { m_justifications[b] = j; save_assign_trail(b); updt_eq(b); - TRACE("nlsat_assign", tout << "b" << b << " -> " << m_bvalues[b] << " " << m_atoms[b] << "\n";); + TRACE("nlsat_assign", tout << "b" << b << " -> " << m_bvalues[b] << "\n";); } /** @@ -936,20 +936,23 @@ namespace nlsat { */ lbool value(literal l) { lbool val = assigned_value(l); - TRACE("nlsat_verbose", display(tout << " assigned value " << val << " for ", l) << "\n";); - if (val != l_undef) { + if (val != l_undef) { + TRACE("nlsat_verbose", display(tout << " assigned value " << val << " for ", l) << "\n";); return val; } bool_var b = l.var(); atom * a = m_atoms[b]; if (a == nullptr) { + TRACE("nlsat_verbose", display(tout << " no atom for ", l) << "\n";); return l_undef; } var max = a->max_var(); if (!m_assignment.is_assigned(max)) { + TRACE("nlsat_verbose", display(tout << " maximal variable not assigned ", l) << "\n";); return l_undef; } val = to_lbool(m_evaluator.eval(a, l.sign())); + TRACE("nlsat_verbose", display(tout << " evaluated value " << val << " for ", l) << "\n";); TRACE("value_bug", tout << "value of: "; display(tout, l); tout << " := " << val << "\n"; tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n"; display_assignment(tout);); @@ -1086,7 +1089,7 @@ namespace nlsat { SASSERT(max_var(l) == m_xk); bool_var b = l.var(); atom * a = m_atoms[b]; - SASSERT(a != 0); + SASSERT(a != nullptr); interval_set_ref curr_set(m_ism); TRACE("nlsat_inf_set", tout << "xk: " << m_xk << ", max_var(l): " << max_var(l) << ", l: "; display(tout, l); tout << "\n";); curr_set = m_evaluator.infeasible_intervals(a, l.sign()); @@ -1148,7 +1151,7 @@ namespace nlsat { If satisfy_learned is true, then (arithmetic) learned clauses are satisfied even if m_lazy > 0 */ bool process_clause(clause const & cls, bool satisfy_learned) { - TRACE("nlsat", tout << "processing clause: "; display(tout, cls); tout << "\n";); + TRACE("nlsat", display(tout << "processing clause: ", cls) << "sat: " << is_satisfied(cls) << "\n";); if (is_satisfied(cls)) return true; if (m_xk == null_var) @@ -1175,7 +1178,7 @@ namespace nlsat { */ void peek_next_bool_var() { while (m_bk < m_atoms.size()) { - if (!m_dead[m_bk] && m_atoms[m_bk] == 0 && m_bvalues[m_bk] == l_undef) { + if (!m_dead[m_bk] && m_atoms[m_bk] == nullptr && m_bvalues[m_bk] == l_undef) { return; } m_bk++; @@ -1235,11 +1238,19 @@ namespace nlsat { if (m_bk == null_bool_var && m_xk >= num_vars()) { TRACE("nlsat", tout << "found model\n"; display_assignment(tout);); fix_patch(); + SASSERT(check_satisfied(m_clauses)); return l_true; // all variables were assigned, and all clauses were satisfied. } - TRACE("nlsat", tout << "processing variable "; - if (m_xk != null_var) m_display_var(tout, m_xk); else tout << "boolean b" << m_bk; tout << "\n";); while (true) { + TRACE("nlsat", tout << "processing variable "; + if (m_xk != null_var) { + m_display_var(tout, m_xk); tout << " " << m_watches[m_xk].size(); + } + else { + tout << m_bwatches[m_bk].size() << " boolean b" << m_bk; + } + tout << "\n"; + ); checkpoint(); clause * conflict_clause; if (m_xk == null_var) @@ -1856,7 +1867,7 @@ namespace nlsat { clause const & c = *(cs[i]); if (!is_satisfied(c)) { TRACE("nlsat", tout << "not satisfied\n"; display(tout, c); tout << "\n";); - UNREACHABLE(); + return false; } } return true; @@ -2052,7 +2063,7 @@ namespace nlsat { reset_watches(); assignment new_assignment(m_am); for (var x = 0; x < num_vars(); x++) { - if (m_assignment.is_assigned(x)) + if (m_assignment.is_assigned(x)) new_assignment.set(p[x], m_assignment.value(x)); } var_vector new_inv_perm; @@ -2091,7 +2102,10 @@ namespace nlsat { del_ill_formed_lemmas(); TRACE("nlsat_bool_assignment_bug", tout << "before reinit cache\n"; display_bool_assignment(tout);); reinit_cache(); - m_assignment.swap(new_assignment); + for (var x = 0; x < num_vars(); x++) { + if (new_assignment.is_assigned(x)) + m_assignment.set(x, new_assignment.value(x)); + } reattach_arith_clauses(m_clauses); reattach_arith_clauses(m_learned); TRACE("nlsat_reorder", tout << "solver after variable reorder\n"; display(tout); display_vars(tout);); @@ -2586,7 +2600,9 @@ namespace nlsat { } TRACE("nlsat_bool_assignment", for (bool_var b = 0; b < sz; b++) { - out << "b" << b << " -> " << m_bvalues[b] << " " << m_atoms[b] << "\n"; + out << "b" << b << " -> " << m_bvalues[b] << " "; + if (m_atoms[b]) display(out, *m_atoms[b]); + out << "\n"; }); return out; } diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 14b6c6b41..611783077 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -401,15 +401,18 @@ struct purify_arith_proc { return BR_DONE; bool is_int = u().is_int(args[0]); + expr * x = args[0]; + rational xr; + if (u().is_numeral(x, xr) && xr.is_zero()) + return BR_FAILED; expr * k = mk_fresh_var(is_int); result = k; mk_def_proof(k, t, result_pr); cache_result(t, result, result_pr); - expr * x = args[0]; - expr * zero = u().mk_numeral(rational(0), is_int); - expr * one = u().mk_numeral(rational(1), is_int); + expr_ref zero(u().mk_numeral(rational(0), is_int), m()); + expr_ref one(u().mk_numeral(rational(1), is_int), m()); if (y.is_zero()) { // (^ x 0) --> k | x != 0 implies k = 1, x = 0 implies k = 0^0 push_cnstr(OR(EQ(x, zero), EQ(k, one))); diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index a9a6032f1..ec22c7c19 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -98,7 +98,6 @@ static tactic * mk_qfnia_nlsat_solver(ast_manager & m, params_ref const & p) { simp_p.set_bool("som", true); // expand into sums of monomials simp_p.set_bool("factor", false); - return and_then(using_params(mk_simplify_tactic(m), simp_p), try_for(mk_qfnra_nlsat_tactic(m, simp_p), 3000), mk_fail_if_undecided_tactic());