From 7452e556987816f369e0520066371e6b13ca63bc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Mar 2020 12:51:10 +0100 Subject: [PATCH] fix #3190 fix #3168 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 4 +--- src/ast/ast.h | 2 +- src/math/euclid/euclidean_solver.cpp | 11 +++++++---- src/nlsat/nlsat_evaluator.cpp | 1 + src/smt/smt_context.h | 3 ++- src/smt/smt_internalizer.cpp | 28 +++++++++++++--------------- src/smt/smt_justification.cpp | 7 ++++--- src/smt/smt_model_finder.cpp | 3 ++- src/smt/theory_lra.cpp | 3 ++- src/util/mpf.cpp | 1 + 10 files changed, 34 insertions(+), 29 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index e60da2031..719d82b41 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1794,6 +1794,7 @@ bool ast_manager::slow_not_contains(ast const * n) { } #endif + ast * ast_manager::register_node_core(ast * n) { unsigned h = get_node_hash(n); n->m_hash = h; @@ -1824,7 +1825,6 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); - TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); // increment reference counters @@ -1921,8 +1921,6 @@ ast * ast_manager::register_node_core(ast * n) { if (n->m_id == 1525) { std::cout << n->m_id << ": " << mk_ll_pp(n, *this) << "\n"; } - //VERIFY(n->m_id != 1549); - //VERIFY(s_count != 2); #endif return n; } diff --git a/src/ast/ast.h b/src/ast/ast.h index abce32d30..e7bfc0710 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1679,7 +1679,7 @@ public: void debug_ref_count() { m_debug_ref_count = true; } - void inc_ref(ast * n) { + void inc_ref(ast* n) { if (n) { n->inc_ref(); } diff --git a/src/math/euclid/euclidean_solver.cpp b/src/math/euclid/euclidean_solver.cpp index 05a1d80f5..96586a1d6 100644 --- a/src/math/euclid/euclidean_solver.cpp +++ b/src/math/euclid/euclidean_solver.cpp @@ -444,13 +444,15 @@ struct euclidean_solver::imp { if (idx == UINT_MAX) return; mpz const & a1 = as[idx]; + SASSERT(!m().is_zero(a1)); equation const & eq2 = *(m_solution[m_solved[x]]); - SASSERT(eq2.pos_x(x) != UINT_MAX); - SASSERT(m().is_minus_one(eq2.a(eq2.pos_x(x)))); TRACE("euclidean_solver_apply", tout << "applying: " << m().to_string(a1) << " * "; display(tout, eq2); tout << "\n"; + tout << "index: " << idx << "\n"; for (unsigned i = 0; i < xs.size(); i++) tout << m().to_string(as[i]) << "*x" << xs[i] << " "; tout << "\n";); + SASSERT(eq2.pos_x(x) != UINT_MAX); + SASSERT(m().is_minus_one(eq2.a(eq2.pos_x(x)))); addmul(as, xs, a1, eq2.m_as, eq2.m_xs, m_tmp_as, m_tmp_xs, eq_idx, except_var); m().addmul(c, a1, eq2.m_c, c); m_tmp_as.swap(as); @@ -665,7 +667,7 @@ struct euclidean_solver::imp { var p = mk_var(true); mpz new_a_i; equation & eq = *(m_equations[m_next_eq]); - TRACE("euclidean_solver", tout << "decompositing equation for x" << m_next_x << "\n"; display(tout, eq); tout << "\n";); + TRACE("euclidean_solver", tout << "decomposing equation for x" << m_next_x << "\n"; display(tout, eq); tout << "\n";); unsigned sz = eq.size(); unsigned j = 0; for (unsigned i = 0; i < sz; i++) { @@ -713,7 +715,8 @@ struct euclidean_solver::imp { // new_eq doesn't need to normalized, since it has unit coefficients TRACE("euclidean_solver", tout << "decomposition: new parameter x" << p << " aux eq:\n"; display(tout, *new_eq); tout << "\n"; - display(tout, eq); tout << "\n";); + display(tout, eq); tout << "\n"; + tout << "next_x " << m_next_x << "\n";); m_solved[m_next_x] = m_solution.size(); m_solution.push_back(new_eq); substitute_most_recent_solution(m_next_x); diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index 980701aef..c1b2e7323 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -490,6 +490,7 @@ namespace nlsat { interval_set_ref infeasible_intervals(ineq_atom * a, bool neg, clause const* cls) { sign_table & table = m_sign_table_tmp; table.reset(); + TRACE("nsat_evaluator", m_solver.display(tout, a) << "\n";); unsigned num_ps = a->size(); var x = a->max_var(); for (unsigned i = 0; i < num_ps; i++) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 37be040a4..c3419ca94 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1056,7 +1056,8 @@ namespace smt { } bool inconsistent() const { - return m_conflict != null_b_justification; + return m_conflict != null_b_justification || + m_asserted_formulas.inconsistent(); } unsigned get_num_conflicts() const { diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 2dfaa49c9..44c10f9be 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1323,21 +1323,27 @@ namespace smt { case CLS_AUX: case CLS_TH_AXIOM: { literal_buffer simp_lits; - if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) - return nullptr; // clause is equivalent to true; - DEBUG_CODE({ - for (unsigned i = 0; i < simp_lits.size(); i++) { - SASSERT(get_assignment(simp_lits[i]) == l_true); + if (!simplify_aux_clause_literals(num_lits, lits, simp_lits)) { + if (j && !j->in_region()) { + j->del_eh(m); + dealloc(j); } - }); + return nullptr; // clause is equivalent to true; + } + DEBUG_CODE(for (literal lit : simp_lits) SASSERT(get_assignment(lit) == l_true);); if (!simp_lits.empty()) { j = mk_justification(unit_resolution_justification(m_region, j, simp_lits.size(), simp_lits.c_ptr())); } break; } case CLS_TH_LEMMA: { - if (!simplify_aux_lemma_literals(num_lits, lits)) + if (!simplify_aux_lemma_literals(num_lits, lits)) { + if (j && !j->in_region()) { + j->del_eh(m); + dealloc(j); + } return nullptr; // clause is equivalent to true + } // simplify_aux_lemma_literals does not delete literals assigned to false, so // it is not necessary to create a unit_resolution_justification break; @@ -1346,14 +1352,6 @@ namespace smt { break; } TRACE("mk_clause", tout << "after simplification:\n"; display_literals_verbose(tout, num_lits, lits) << "\n";); -#if 0 - for (unsigned i = 0; i < num_lits; ++i) { - expr_ref tmp(m); - literal2expr(lits[i], tmp); - std::cout << tmp << "\n"; - } - std::cout << "\n"; -#endif unsigned activity = 0; if (activity == 0) diff --git a/src/smt/smt_justification.cpp b/src/smt/smt_justification.cpp index c80b90304..65f4c4a12 100644 --- a/src/smt/smt_justification.cpp +++ b/src/smt/smt_justification.cpp @@ -377,8 +377,8 @@ namespace smt { justification(false), m_th_id(fid), m_params(num_params, params), - m_num_literals(num_lits) { - ast_manager & m = ctx.get_manager(); + m_num_literals(num_lits) { + ast_manager& m = ctx.get_manager(); m_literals = alloc_svect(expr*, num_lits); for (unsigned i = 0; i < num_lits; i++) { bool sign = lits[i].sign(); @@ -396,7 +396,8 @@ namespace smt { void theory_lemma_justification::del_eh(ast_manager & m) { for (unsigned i = 0; i < m_num_literals; i++) { - m.dec_ref(UNTAG(expr*, m_literals[i])); + expr* v = UNTAG(expr*, m_literals[i]); + m.dec_ref(v); } m_params.reset(); } diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 29452573a..06862630f 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -3179,6 +3179,7 @@ namespace smt { } mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) const { + TRACE("model_finder", tout << q->get_id() << ": " << q << " " << &m_q2info << " " << mk_pp(q, m) << "\n";); return m_q2info[q]; } @@ -3190,7 +3191,7 @@ namespace smt { } void model_finder::register_quantifier(quantifier * q) { - TRACE("model_finder", tout << "registering:\n" << mk_pp(q, m) << "\n";); + TRACE("model_finder", tout << "registering:\n" << q->get_id() << ": " << q << " " << &m_q2info << " " << mk_pp(q, m) << "\n";); quantifier_info * new_info = alloc(quantifier_info, *this, m, q); m_q2info.insert(q, new_info); m_quantifiers.push_back(q); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 6617e2211..d9b34861a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1356,7 +1356,8 @@ public: body = m.mk_implies(m.mk_not(m.mk_eq(q, zero)), a.mk_le(mod, upper)); th.log_axiom_instantiation(body); } - mk_axiom(mk_literal(a.mk_le(mod, upper))); + expr_ref le(a.mk_le(mod, upper), m); + mk_axiom(mk_literal(le)); if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; if (k.is_pos()) { if (m.has_trace_stream()) { diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 49335467d..df0b8fd3b 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1186,6 +1186,7 @@ void mpf_manager::to_sbv_mpq(mpf_rounding_mode rm, const mpf & x, scoped_mpq & o scoped_mpf t(*this); scoped_mpz z(m_mpz_manager); + set(t, x); unpack(t, true);