From b09035565a093ff046e69c624f9e038e2cd53468 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 5 Sep 2018 19:04:11 -0400 Subject: [PATCH 01/10] canonicalize encoding of string constants/symbols --- src/ast/seq_decl_plugin.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 07c6fd06a..06f30cbdf 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -842,7 +842,9 @@ void seq_decl_plugin::get_sort_names(svector & sort_names, symbol } app* seq_decl_plugin::mk_string(symbol const& s) { - parameter param(s); + zstring canonStr(s.bare_str()); + symbol canonSym(canonStr.encode().c_str()); + parameter param(canonSym); func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string, func_decl_info(m_family_id, OP_STRING_CONST, 1, ¶m)); return m_manager->mk_const(f); From 211210338a4fac1a26073c6a2a7edf180c2b9ddc Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 7 Sep 2018 22:00:25 -0700 Subject: [PATCH 02/10] bound vars Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 32 +++++++++++++++++++++++++++++++- 1 file changed, 31 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 267412da6..0f07eac7e 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -154,6 +154,7 @@ class theory_lra::imp { ast_manager& m; theory_arith_params& m_arith_params; arith_util a; + bool m_has_int; arith_eq_adapter m_arith_eq_adapter; vector m_columns; @@ -624,6 +625,7 @@ class theory_lra::imp { } if (result == UINT_MAX) { result = m_solver->add_var(v, is_int(v)); + m_has_int |= is_int(v); m_theory_var2var_index.setx(v, result, UINT_MAX); m_var_index2theory_var.setx(result, v, UINT_MAX); m_var_trail.push_back(v); @@ -798,6 +800,7 @@ public: th(th), m(m), m_arith_params(ap), a(m), + m_has_int(false), m_arith_eq_adapter(th, ap, a), m_internalize_head(0), m_not_handled(0), @@ -1414,15 +1417,40 @@ public: return atom; } + bool all_variables_have_bounds() { + if (!m_has_int) { + return true; + } + unsigned nv = th.get_num_vars(); + bool added_bound = false; + for (unsigned v = 0; v < nv; ++v) { + lp::constraint_index ci; + rational bound; + lp::var_index vi = m_theory_var2var_index[v]; + if (!has_upper_bound(vi, ci, bound) && !has_lower_bound(vi, ci, bound)) { + lp::lar_term term; + term.add_monomial(rational::one(), vi); + app_ref b = mk_bound(term, rational::zero(), false); + TRACE("arith", tout << "added bound " << b << "\n";); + added_bound = true; + } + } + return !added_bound; + } + lbool check_lia() { if (m.canceled()) { TRACE("arith", tout << "canceled\n";); return l_undef; } + if (!all_variables_have_bounds()) { + return l_false; + } lp::lar_term term; lp::mpq k; lp::explanation ex; // TBD, this should be streamlined accross different explanations bool upper; + std::cout << "."; switch(m_lia->check(term, k, ex, upper)) { case lp::lia_move::sat: return l_true; @@ -2918,7 +2946,9 @@ public: for (auto const& kv : coeffs) { g = gcd(g, kv.m_value); } - if (!g.is_one() && !g.is_zero()) { + if (g.is_zero()) + return rational::one(); + if (!g.is_one()) { for (auto& kv : coeffs) { kv.m_value /= g; } From 67a2a26009f145fdcf010d99814807cedcc4a7a7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 Sep 2018 14:26:46 -0700 Subject: [PATCH 03/10] fixing bound detection (#86) * fixing bound detection Signed-off-by: Nikolaj Bjorner * check-idiv bounds Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 236 +++++++++++++++++++++++++++++++++++------ 1 file changed, 202 insertions(+), 34 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0f07eac7e..f1ffbf60c 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -129,6 +129,7 @@ class theory_lra::imp { struct scope { unsigned m_bounds_lim; + unsigned m_idiv_lim; unsigned m_asserted_qhead; unsigned m_asserted_atoms_lim; unsigned m_underspecified_lim; @@ -230,6 +231,7 @@ class theory_lra::imp { svector m_asserted_atoms; expr* m_not_handled; ptr_vector m_underspecified; + ptr_vector m_idiv_terms; unsigned_vector m_var_trail; vector > m_use_list; // bounds where variables are used. @@ -443,6 +445,7 @@ class theory_lra::imp { } else if (a.is_idiv(n, n1, n2)) { if (!a.is_numeral(n2, r) || r.is_zero()) found_not_handled(n); + m_idiv_terms.push_back(n); app * mod = a.mk_mod(n1, n2); ctx().internalize(mod, false); if (ctx().relevancy()) ctx().add_relevancy_dependency(n, mod); @@ -452,6 +455,7 @@ class theory_lra::imp { if (!is_num) { found_not_handled(n); } +#if 0 else { app_ref div(a.mk_idiv(n1, n2), m); mk_enode(div); @@ -462,7 +466,8 @@ class theory_lra::imp { // abs(r) > v >= 0 assert_idiv_mod_axioms(u, v, w, r); } - if (!ctx().relevancy() && !is_num) mk_idiv_mod_axioms(n1, n2); +#endif + if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2); } else if (a.is_rem(n, n1, n2)) { if (!a.is_numeral(n2, r) || r.is_zero()) found_not_handled(n); @@ -803,7 +808,7 @@ public: m_has_int(false), m_arith_eq_adapter(th, ap, a), m_internalize_head(0), - m_not_handled(0), + m_not_handled(nullptr), m_asserted_qhead(0), m_assume_eq_head(0), m_num_conflicts(0), @@ -913,6 +918,7 @@ public: scope& s = m_scopes.back(); s.m_bounds_lim = m_bounds_trail.size(); s.m_asserted_qhead = m_asserted_qhead; + s.m_idiv_lim = m_idiv_terms.size(); s.m_asserted_atoms_lim = m_asserted_atoms.size(); s.m_not_handled = m_not_handled; s.m_underspecified_lim = m_underspecified.size(); @@ -938,6 +944,7 @@ public: } m_theory_var2var_index[m_var_trail[i]] = UINT_MAX; } + m_idiv_terms.shrink(m_scopes[old_size].m_idiv_lim); m_asserted_atoms.shrink(m_scopes[old_size].m_asserted_atoms_lim); m_asserted_qhead = m_scopes[old_size].m_asserted_qhead; m_underspecified.shrink(m_scopes[old_size].m_underspecified_lim); @@ -1033,37 +1040,74 @@ public: add_def_constraint(m_solver->add_var_bound(vi, lp::LE, rational::zero())); add_def_constraint(m_solver->add_var_bound(get_var_index(v), lp::GE, rational::zero())); add_def_constraint(m_solver->add_var_bound(get_var_index(v), lp::LT, abs(r))); + TRACE("arith", m_solver->print_constraints(tout << term << "\n");); } void mk_idiv_mod_axioms(expr * p, expr * q) { if (a.is_zero(q)) { return; } + TRACE("arith", tout << expr_ref(p, m) << " " << expr_ref(q, m) << "\n";); // if q is zero, then idiv and mod are uninterpreted functions. expr_ref div(a.mk_idiv(p, q), m); expr_ref mod(a.mk_mod(p, q), m); expr_ref zero(a.mk_int(0), m); - literal q_ge_0 = mk_literal(a.mk_ge(q, zero)); - literal q_le_0 = mk_literal(a.mk_le(q, zero)); - // literal eqz = th.mk_eq(q, zero, false); literal eq = th.mk_eq(a.mk_add(a.mk_mul(q, div), mod), p, false); literal mod_ge_0 = mk_literal(a.mk_ge(mod, zero)); - // q >= 0 or p = (p mod q) + q * (p div q) - // q <= 0 or p = (p mod q) + q * (p div q) - // q >= 0 or (p mod q) >= 0 - // q <= 0 or (p mod q) >= 0 - // q <= 0 or (p mod q) < q - // q >= 0 or (p mod q) < -q - // enable_trace("mk_bool_var"); - mk_axiom(q_ge_0, eq); - mk_axiom(q_le_0, eq); - mk_axiom(q_ge_0, mod_ge_0); - mk_axiom(q_le_0, mod_ge_0); - mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero))); - mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero))); - rational k; - if (m_arith_params.m_arith_enum_const_mod && a.is_numeral(q, k) && - k.is_pos() && k < rational(8)) { + literal div_ge_0 = mk_literal(a.mk_ge(div, zero)); + literal div_le_0 = mk_literal(a.mk_le(div, zero)); + literal p_ge_0 = mk_literal(a.mk_ge(p, zero)); + literal p_le_0 = mk_literal(a.mk_le(p, zero)); + + rational k(0); + expr_ref upper(m); + + if (a.is_numeral(q, k)) { + if (k.is_pos()) { + upper = a.mk_numeral(k - 1, true); + } + else if (k.is_neg()) { + upper = a.mk_numeral(-k - 1, true); + } + } + else { + k = rational::zero(); + } + + if (!k.is_zero()) { + mk_axiom(eq); + mk_axiom(mod_ge_0); + mk_axiom(mk_literal(a.mk_le(mod, upper))); + if (k.is_pos()) { + mk_axiom(~p_ge_0, div_ge_0); + mk_axiom(~p_le_0, div_le_0); + } + else { + mk_axiom(~p_ge_0, div_le_0); + mk_axiom(~p_le_0, div_ge_0); + } + } + else { + // q >= 0 or p = (p mod q) + q * (p div q) + // q <= 0 or p = (p mod q) + q * (p div q) + // q >= 0 or (p mod q) >= 0 + // q <= 0 or (p mod q) >= 0 + // q <= 0 or (p mod q) < q + // q >= 0 or (p mod q) < -q + literal q_ge_0 = mk_literal(a.mk_ge(q, zero)); + literal q_le_0 = mk_literal(a.mk_le(q, zero)); + mk_axiom(q_ge_0, eq); + mk_axiom(q_le_0, eq); + mk_axiom(q_ge_0, mod_ge_0); + mk_axiom(q_le_0, mod_ge_0); + mk_axiom(q_le_0, ~mk_literal(a.mk_ge(a.mk_sub(mod, q), zero))); + mk_axiom(q_ge_0, ~mk_literal(a.mk_ge(a.mk_add(mod, q), zero))); + mk_axiom(q_le_0, ~p_ge_0, div_ge_0); + mk_axiom(q_le_0, ~p_le_0, div_le_0); + mk_axiom(q_ge_0, ~p_ge_0, div_le_0); + mk_axiom(q_ge_0, ~p_le_0, div_ge_0); + } + if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) { unsigned _k = k.get_unsigned(); literal_buffer lits; for (unsigned j = 0; j < _k; ++j) { @@ -1211,10 +1255,9 @@ public: } void init_variable_values() { + reset_variable_values(); if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) { - reset_variable_values(); m_solver->get_model(m_variable_values); - TRACE("arith", display(tout);); } } @@ -1317,6 +1360,7 @@ public: } final_check_status final_check_eh() { + IF_VERBOSE(2, verbose_stream() << "final-check\n"); m_use_nra_model = false; lbool is_sat = l_true; if (m_solver->get_status() != lp::lp_status::OPTIMAL) { @@ -1331,7 +1375,7 @@ public: } if (assume_eqs()) { return FC_CONTINUE; - } + } switch (check_lia()) { case l_true: @@ -1343,7 +1387,7 @@ public: st = FC_CONTINUE; break; } - + switch (check_nra()) { case l_true: break; @@ -1422,20 +1466,126 @@ public: return true; } unsigned nv = th.get_num_vars(); - bool added_bound = false; + bool all_bounded = true; for (unsigned v = 0; v < nv; ++v) { - lp::constraint_index ci; - rational bound; lp::var_index vi = m_theory_var2var_index[v]; - if (!has_upper_bound(vi, ci, bound) && !has_lower_bound(vi, ci, bound)) { + if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) { lp::lar_term term; term.add_monomial(rational::one(), vi); - app_ref b = mk_bound(term, rational::zero(), false); + app_ref b = mk_bound(term, rational::zero(), true); TRACE("arith", tout << "added bound " << b << "\n";); - added_bound = true; + IF_VERBOSE(2, verbose_stream() << "bound: " << b << "\n"); + all_bounded = false; } } - return !added_bound; + return all_bounded; + } + + /** + * n = (div p q) + * + * (div p q) * q + (mod p q) = p, (mod p q) >= 0 + * + * 0 < q => (p/q <= v(p)/v(q) => n <= floor(v(p)/v(q))) + * 0 < q => (v(p)/v(q) <= p/q => v(p)/v(q) - 1 < n) + * + */ + bool check_idiv_bounds() { + if (m_idiv_terms.empty()) { + return true; + } + bool all_divs_valid = true; + init_variable_values(); + for (expr* n : m_idiv_terms) { + expr* p = nullptr, *q = nullptr; + VERIFY(a.is_idiv(n, p, q)); + theory_var v = mk_var(n); + theory_var v1 = mk_var(p); + theory_var v2 = mk_var(q); + rational r = get_value(v); + rational r1 = get_value(v1); + rational r2 = get_value(v2); + rational r3; + if (r2.is_zero()) { + continue; + } + if (r1.is_int() && r2.is_int() && r == div(r1, r2)) { + continue; + } + if (r2.is_neg()) { + // TBD + continue; + } + + if (a.is_numeral(q, r3)) { + + SASSERT(r3 == r2 && r2.is_int()); + // p <= r1 => n <= div(r1, r2) + // r1 <= p => div(r1, r2) <= n + literal p_le_r1 = mk_literal(a.mk_le(p, a.mk_numeral(ceil(r1), true))); + literal p_ge_r1 = mk_literal(a.mk_ge(p, a.mk_numeral(floor(r1), true))); + literal n_le_div = mk_literal(a.mk_le(n, a.mk_numeral(div(ceil(r1), r2), true))); + literal n_ge_div = mk_literal(a.mk_ge(n, a.mk_numeral(div(floor(r1), r2), true))); + mk_axiom(~p_le_r1, n_le_div); + mk_axiom(~p_ge_r1, n_ge_div); + + all_divs_valid = false; + + TRACE("arith", + literal_vector lits; + lits.push_back(~p_le_r1); + lits.push_back(n_le_div); + ctx().display_literals_verbose(tout, lits) << "\n"; + lits[0] = ~p_ge_r1; + lits[1] = n_ge_div; + ctx().display_literals_verbose(tout, lits) << "\n";); + continue; + } + + if (!r1.is_int() || !r2.is_int()) { + // std::cout << r1 << " " << r2 << " " << r << " " << expr_ref(n, m) << "\n"; + // TBD + // r1 = 223/4, r2 = 2, r = 219/8 + // take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0 + // then + // p/q <= ceil(r1)/floor(r2) => n <= div(ceil(r1), floor(r2)) + // p/q >= floor(r1)/ceil(r2) => n >= div(floor(r1), ceil(r2)) + continue; + } + + + all_divs_valid = false; + + + // + // p/q <= r1/r2 => n <= div(r1, r2) + // <=> + // p*r2 <= q*r1 => n <= div(r1, r2) + // + // p/q >= r1/r2 => n >= div(r1, r2) + // <=> + // p*r2 >= r1*q => n >= div(r1, r2) + // + expr_ref zero(a.mk_int(0), m); + expr_ref divc(a.mk_numeral(div(r1, r2), true), m); + expr_ref pqr(a.mk_sub(a.mk_mul(a.mk_numeral(r2, true), p), a.mk_mul(a.mk_numeral(r1, true), q)), m); + literal pq_lhs = ~mk_literal(a.mk_le(pqr, zero)); + literal pq_rhs = ~mk_literal(a.mk_ge(pqr, zero)); + literal n_le_div = mk_literal(a.mk_le(n, divc)); + literal n_ge_div = mk_literal(a.mk_ge(n, divc)); + mk_axiom(pq_lhs, n_le_div); + mk_axiom(pq_rhs, n_ge_div); + TRACE("arith", + literal_vector lits; + lits.push_back(pq_lhs); + lits.push_back(n_le_div); + ctx().display_literals_verbose(tout, lits) << "\n"; + lits[0] = pq_rhs; + lits[1] = n_ge_div; + ctx().display_literals_verbose(tout, lits) << "\n";); + } + + return all_divs_valid; } lbool check_lia() { @@ -1444,19 +1594,24 @@ public: return l_undef; } if (!all_variables_have_bounds()) { + TRACE("arith", tout << "not all variables have bounds\n";); + return l_false; + } + if (!check_idiv_bounds()) { + TRACE("arith", tout << "idiv bounds check\n";); return l_false; } lp::lar_term term; lp::mpq k; lp::explanation ex; // TBD, this should be streamlined accross different explanations bool upper; - std::cout << "."; switch(m_lia->check(term, k, ex, upper)) { case lp::lia_move::sat: return l_true; case lp::lia_move::branch: { TRACE("arith", tout << "branch\n";); app_ref b = mk_bound(term, k, !upper); + IF_VERBOSE(2, verbose_stream() << "branch " << b << "\n";); // branch on term >= k + 1 // branch on term <= k // TBD: ctx().force_phase(ctx().get_literal(b)); @@ -1469,6 +1624,7 @@ public: ++m_stats.m_gomory_cuts; // m_explanation implies term <= k app_ref b = mk_bound(term, k, !upper); + IF_VERBOSE(2, verbose_stream() << "cut " << b << "\n";); m_eqs.reset(); m_core.reset(); m_params.reset(); @@ -2411,6 +2567,18 @@ public: } } + bool var_has_bound(lp::var_index vi, bool is_lower) { + bool is_strict = false; + rational b; + lp::constraint_index ci; + if (is_lower) { + return m_solver->has_lower_bound(vi, ci, b, is_strict); + } + else { + return m_solver->has_upper_bound(vi, ci, b, is_strict); + } + } + bool has_upper_bound(lp::var_index vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, false); } bool has_lower_bound(lp::var_index vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, true); } @@ -2981,7 +3149,7 @@ public: } if (!ctx().b_internalized(b)) { fm.hide(b->get_decl()); - bool_var bv = ctx().mk_bool_var(b); + bool_var bv = ctx().mk_bool_var(b); ctx().set_var_theory(bv, get_id()); // ctx().set_enode_flag(bv, true); lp_api::bound_kind bkind = lp_api::bound_kind::lower_t; From fae66671d8b7edf22e1508796f063caf3d0b9497 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Sep 2018 08:57:35 -0700 Subject: [PATCH 04/10] fix #1817 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 41 +++++++++++++++++------------------- src/smt/theory_arith_core.h | 1 - src/smt/theory_lra.cpp | 8 +++---- 3 files changed, 22 insertions(+), 28 deletions(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 1414cb522..618450f9d 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -216,13 +216,17 @@ namespace smt { SASSERT(m_manager.is_bool(n)); if (is_gate(m_manager, n)) { switch(to_app(n)->get_decl_kind()) { - case OP_AND: - UNREACHABLE(); + case OP_AND: { + for (expr * arg : *to_app(n)) { + internalize(arg, true); + literal lit = get_literal(arg); + mk_root_clause(1, &lit, pr); + } + break; + } case OP_OR: { literal_buffer lits; - unsigned num = to_app(n)->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * arg = to_app(n)->get_arg(i); + for (expr * arg : *to_app(n)) { internalize(arg, true); lits.push_back(get_literal(arg)); } @@ -294,8 +298,7 @@ namespace smt { sort * s = m_manager.get_sort(n->get_arg(0)); sort_ref u(m_manager.mk_fresh_sort("distinct-elems"), m_manager); func_decl_ref f(m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m_manager); - for (unsigned i = 0; i < num_args; i++) { - expr * arg = n->get_arg(i); + for (expr * arg : *n) { app_ref fapp(m_manager.mk_app(f, arg), m_manager); app_ref val(m_manager.mk_fresh_const("unique-value", u), m_manager); enode * e = mk_enode(val, false, false, true); @@ -826,9 +829,7 @@ namespace smt { void context::internalize_uninterpreted(app * n) { SASSERT(!e_internalized(n)); // process args - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * arg = n->get_arg(i); + for (expr * arg : *n) { internalize(arg, false); SASSERT(e_internalized(arg)); } @@ -1542,10 +1543,9 @@ namespace smt { void context::add_and_rel_watches(app * n) { if (relevancy()) { relevancy_eh * eh = m_relevancy_propagator->mk_and_relevancy_eh(n); - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { + for (expr * arg : *n) { // if one child is assigned to false, the and-parent must be notified - literal l = get_literal(n->get_arg(i)); + literal l = get_literal(arg); add_rel_watch(~l, eh); } } @@ -1554,10 +1554,9 @@ namespace smt { void context::add_or_rel_watches(app * n) { if (relevancy()) { relevancy_eh * eh = m_relevancy_propagator->mk_or_relevancy_eh(n); - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { + for (expr * arg : *n) { // if one child is assigned to true, the or-parent must be notified - literal l = get_literal(n->get_arg(i)); + literal l = get_literal(arg); add_rel_watch(l, eh); } } @@ -1588,9 +1587,8 @@ namespace smt { TRACE("mk_and_cnstr", tout << "l: "; display_literal(tout, l); tout << "\n";); literal_buffer buffer; buffer.push_back(l); - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - literal l_arg = get_literal(n->get_arg(i)); + for (expr * arg : *n) { + literal l_arg = get_literal(arg); TRACE("mk_and_cnstr", tout << "l_arg: "; display_literal(tout, l_arg); tout << "\n";); mk_gate_clause(~l, l_arg); buffer.push_back(~l_arg); @@ -1602,9 +1600,8 @@ namespace smt { literal l = get_literal(n); literal_buffer buffer; buffer.push_back(~l); - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - literal l_arg = get_literal(n->get_arg(i)); + for (expr * arg : *n) { + literal l_arg = get_literal(arg); mk_gate_clause(l, ~l_arg); buffer.push_back(l_arg); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index f96b6228b..67271ad4f 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -484,7 +484,6 @@ namespace smt { void theory_arith::mk_idiv_mod_axioms(expr * dividend, expr * divisor) { if (!m_util.is_zero(divisor)) { ast_manager & m = get_manager(); - bool is_numeral = m_util.is_numeral(divisor); // if divisor is zero, then idiv and mod are uninterpreted functions. expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m); expr_ref eqz(m), eq(m), lower(m), upper(m); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 267412da6..b7f8549fb 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -692,9 +692,7 @@ class theory_lra::imp { ++m_stats.m_add_rows; } - void internalize_eq(theory_var v1, theory_var v2) { - enode* n1 = get_enode(v1); - enode* n2 = get_enode(v2); + void internalize_eq(theory_var v1, theory_var v2) { app_ref term(m.mk_fresh_const("eq", a.mk_real()), m); scoped_internalize_state st(*this); st.vars().push_back(v1); @@ -707,8 +705,8 @@ class theory_lra::imp { add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero())); TRACE("arith", { - expr* o1 = n1->get_owner(); - expr* o2 = n2->get_owner(); + expr* o1 = get_enode(v1)->get_owner(); + expr* o2 = get_enode(v2)->get_owner(); tout << "v" << v1 << " = " << "v" << v2 << ": " << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n"; }); From 8068c64cab45f53fb95d807fe6a68941b2cf2985 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 10 Sep 2018 11:02:38 -0700 Subject: [PATCH 05/10] avoid using not initialized variables in theory_lra Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 4 +++- src/util/lp/lp_settings.h | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index f1ffbf60c..b0ba51129 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1465,10 +1465,12 @@ public: if (!m_has_int) { return true; } - unsigned nv = th.get_num_vars(); + unsigned nv = std::min(th.get_num_vars(), m_theory_var2var_index.size()); bool all_bounded = true; for (unsigned v = 0; v < nv; ++v) { lp::var_index vi = m_theory_var2var_index[v]; + if (vi == UINT_MAX) + continue; if (!m_solver->is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) { lp::lar_term term; term.add_monomial(rational::one(), vi); diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h index dd19df23a..71be7258a 100644 --- a/src/util/lp/lp_settings.h +++ b/src/util/lp/lp_settings.h @@ -357,7 +357,7 @@ public: } #ifdef Z3DEBUG - static unsigned ddd; // used for debugging +static unsigned ddd; // used for debugging #endif }; // end of lp_settings class From 813b9063417fcaef8dd4068f8e5d9f849f68724b Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 10 Sep 2018 13:43:29 -0700 Subject: [PATCH 06/10] do not bound all free vars Signed-off-by: Lev Nachmanson --- src/smt/theory_lra.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b0ba51129..9c6d3f89a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1461,7 +1461,7 @@ public: return atom; } - bool all_variables_have_bounds() { + bool make_sure_all_vars_have_bounds() { if (!m_has_int) { return true; } @@ -1595,10 +1595,6 @@ public: TRACE("arith", tout << "canceled\n";); return l_undef; } - if (!all_variables_have_bounds()) { - TRACE("arith", tout << "not all variables have bounds\n";); - return l_false; - } if (!check_idiv_bounds()) { TRACE("arith", tout << "idiv bounds check\n";); return l_false; From a37d05d54b9ca10d4c613a4bb3a980f1bb0c1c4a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Sep 2018 13:53:44 -0700 Subject: [PATCH 07/10] fix #1819 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_int.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index ee3bd5e2e..afe527a98 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -396,7 +396,9 @@ namespace smt { for (; it != end; ++it) { if (!it->is_dead() && it->m_var != b && is_free(it->m_var)) { theory_var v = it->m_var; - expr * bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(rational::zero(), is_int(v))); + expr* e = get_enode(v)->get_owner(); + bool _is_int = m_util.is_int(e); + expr * bound = m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int)); context & ctx = get_context(); ctx.internalize(bound, true); ctx.mark_as_relevant(bound); From e818b7bd2732c87dbbee30b17e6563b9c652427c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Sep 2018 15:15:00 -0700 Subject: [PATCH 08/10] fix #1812 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 6 +++++ src/ast/ast.h | 1 + src/smt/smt_model_checker.cpp | 45 +++++++++++++++++++++++++++++++---- src/smt/smt_model_checker.h | 3 +++ 4 files changed, 51 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 11a15492c..65d3c7821 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1656,6 +1656,12 @@ bool ast_manager::are_distinct(expr* a, expr* b) const { return false; } +func_decl* ast_manager::get_rec_fun_decl(quantifier* q) const { + SASSERT(is_rec_fun_def(q)); + return to_app(to_app(q->get_pattern(0))->get_arg(0))->get_decl(); +} + + void ast_manager::register_plugin(family_id id, decl_plugin * plugin) { SASSERT(m_plugins.get(id, 0) == 0); m_plugins.setx(id, plugin, 0); diff --git a/src/ast/ast.h b/src/ast/ast.h index 89df04961..c1193dfbd 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1632,6 +1632,7 @@ public: bool is_rec_fun_def(quantifier* q) const { return q->get_qid() == m_rec_fun; } bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; } + func_decl* get_rec_fun_decl(quantifier* q) const; symbol const& rec_fun_qid() const { return m_rec_fun; } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 0fea4d13d..c3af41dcf 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -47,6 +47,7 @@ namespace smt { m_model_finder(mf), m_max_cexs(1), m_iteration_idx(0), + m_has_rec_fun(false), m_curr_model(nullptr), m_pinned_exprs(m) { } @@ -351,9 +352,7 @@ namespace smt { bool model_checker::check_rec_fun(quantifier* q, bool strict_rec_fun) { TRACE("model_checker", tout << mk_pp(q, m) << "\n";); SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body. - expr* fn = to_app(q->get_pattern(0))->get_arg(0); - SASSERT(is_app(fn)); - func_decl* f = to_app(fn)->get_decl(); + func_decl* f = m.get_rec_fun_decl(q); expr_ref_vector args(m); unsigned num_decls = q->get_num_decls(); @@ -433,7 +432,7 @@ namespace smt { TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";); m_max_cexs += m_params.m_mbqi_max_cexs; - if (num_failures == 0 && !m_context->validate_model()) { + if (num_failures == 0 && (!m_context->validate_model() || has_rec_under_quantifiers())) { num_failures = 1; // this time force expanding recursive function definitions // that are not forced true in the current model. @@ -450,6 +449,43 @@ namespace smt { return num_failures == 0; } + struct has_rec_fun_proc { + obj_hashtable& m_rec_funs; + bool m_has_rec_fun; + + bool has_rec_fun() const { return m_has_rec_fun; } + + has_rec_fun_proc(obj_hashtable& rec_funs): + m_rec_funs(rec_funs), + m_has_rec_fun(false) {} + + void operator()(app* fn) { + m_has_rec_fun |= m_rec_funs.contains(fn->get_decl()); + } + void operator()(expr*) {} + }; + + bool model_checker::has_rec_under_quantifiers() { + if (!m_has_rec_fun) { + return false; + } + obj_hashtable rec_funs; + for (quantifier * q : *m_qm) { + if (m.is_rec_fun_def(q)) { + rec_funs.insert(m.get_rec_fun_decl(q)); + } + } + expr_fast_mark1 visited; + has_rec_fun_proc proc(rec_funs); + for (quantifier * q : *m_qm) { + if (!m.is_rec_fun_def(q)) { + quick_for_each_expr(proc, visited, q); + if (proc.has_rec_fun()) return true; + } + } + return false; + } + // // (repeated from defined_names.cpp) // NB. The pattern for lambdas is incomplete. @@ -479,6 +515,7 @@ namespace smt { } found_relevant = true; if (m.is_rec_fun_def(q)) { + m_has_rec_fun = true; if (!check_rec_fun(q, strict_rec_fun)) { TRACE("model_checker", tout << "checking recursive function failed\n";); num_failures++; diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h index 40a58efea..57edf3034 100644 --- a/src/smt/smt_model_checker.h +++ b/src/smt/smt_model_checker.h @@ -51,8 +51,10 @@ namespace smt { scoped_ptr m_aux_context; // Auxiliary context used for model checking quantifiers. unsigned m_max_cexs; unsigned m_iteration_idx; + bool m_has_rec_fun; proto_model * m_curr_model; obj_map m_value2expr; + friend class instantiation_set; void init_aux_context(); @@ -64,6 +66,7 @@ namespace smt { bool add_blocking_clause(model * cex, expr_ref_vector & sks); bool check(quantifier * q); bool check_rec_fun(quantifier* q, bool strict_rec_fun); + bool has_rec_under_quantifiers(); void check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures); struct instance { From f810a5d8c33363533bd9713f6a7e1482e9986163 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 10 Sep 2018 15:22:48 -0700 Subject: [PATCH 09/10] remove an assert Signed-off-by: Lev Nachmanson --- src/util/lp/lar_solver.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 654eb7017..d4db0bc91 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -1964,7 +1964,6 @@ void lar_solver::update_boxed_column_type_and_bound(var_index j, lconstraint_kin if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) { m_status = lp_status::INFEASIBLE; - lp_assert(false); m_infeasible_column_index = j; } else { From 18bec88a8af07410c8b0e3bec9e89aa5d54556c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Sep 2018 15:52:02 -0700 Subject: [PATCH 10/10] purify non-constant terms by default to enforce theory #1820 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 5d4eb3fc5..b1296f71e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1084,11 +1084,7 @@ namespace opt { } term = m_arith.mk_add(args.size(), args.c_ptr()); } - else if (m_arith.is_arith_expr(term) && !is_mul_const(term)) { - TRACE("opt", tout << "Purifying " << term << "\n";); - term = purify(fm, term); - } - else if (m.is_ite(term)) { + else if (m.is_ite(term) || !is_mul_const(term)) { TRACE("opt", tout << "Purifying " << term << "\n";); term = purify(fm, term); }