From 211210338a4fac1a26073c6a2a7edf180c2b9ddc Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 7 Sep 2018 22:00:25 -0700 Subject: [PATCH 1/5] 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 2/5] 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 8068c64cab45f53fb95d807fe6a68941b2cf2985 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 10 Sep 2018 11:02:38 -0700 Subject: [PATCH 3/5] 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 4/5] 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 f810a5d8c33363533bd9713f6a7e1482e9986163 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 10 Sep 2018 15:22:48 -0700 Subject: [PATCH 5/5] 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 {