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/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); 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); } 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/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 { 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_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); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 267412da6..13d1ab53e 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; @@ -154,6 +155,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; @@ -229,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. @@ -442,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); @@ -451,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); @@ -461,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); @@ -624,6 +630,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); @@ -692,9 +699,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 +712,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"; }); @@ -798,9 +803,10 @@ 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), + m_not_handled(nullptr), m_asserted_qhead(0), m_assume_eq_head(0), m_num_conflicts(0), @@ -910,6 +916,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(); @@ -935,6 +942,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); @@ -1030,37 +1038,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) { @@ -1208,10 +1253,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);); } } @@ -1314,6 +1358,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) { @@ -1328,7 +1373,7 @@ public: } if (assume_eqs()) { return FC_CONTINUE; - } + } switch (check_lia()) { case l_true: @@ -1340,7 +1385,7 @@ public: st = FC_CONTINUE; break; } - + switch (check_nra()) { case l_true: break; @@ -1414,11 +1459,144 @@ public: return atom; } + bool make_sure_all_vars_have_bounds() { + if (!m_has_int) { + return true; + } + 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); + app_ref b = mk_bound(term, rational::zero(), true); + TRACE("arith", tout << "added bound " << b << "\n";); + IF_VERBOSE(2, verbose_stream() << "bound: " << b << "\n"); + all_bounded = false; + } + } + 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() { if (m.canceled()) { TRACE("arith", tout << "canceled\n";); return l_undef; } + 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 @@ -1429,6 +1607,7 @@ public: 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)); @@ -1441,6 +1620,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(); @@ -2383,6 +2563,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); } @@ -2918,7 +3110,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; } @@ -2951,7 +3145,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; 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 { 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