mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-09-11 03:14:41 -07:00
parent 36a14a354a da20d949c6
commit b1423e17a1
12 changed files with 304 additions and 68 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast.cpp
View file

@ -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);

1
src/ast/ast.h
View file

@ -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; }

4
src/ast/seq_decl_plugin.cpp
View file

@ -842,7 +842,9 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & 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, &param));
return m_manager->mk_const(f);

6
src/opt/opt_context.cpp
View file

@ -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);
}

41
src/smt/smt_internalizer.cpp
View file

@ -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);
}

45
src/smt/smt_model_checker.cpp
View file

@ -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<func_decl>& m_rec_funs;
bool m_has_rec_fun;
bool has_rec_fun() const { return m_has_rec_fun; }
has_rec_fun_proc(obj_hashtable<func_decl>& 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<func_decl> 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++;

3
src/smt/smt_model_checker.h
View file

@ -51,8 +51,10 @@ namespace smt {
scoped_ptr<context> 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<expr, expr *> 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 {

1
src/smt/theory_arith_core.h
View file

@ -484,7 +484,6 @@ namespace smt {
void theory_arith<Ext>::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);

4
src/smt/theory_arith_int.h
View file

@ -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);

258
src/smt/theory_lra.cpp
View file

@ -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<rational> m_columns;
@ -229,6 +231,7 @@ class theory_lra::imp {
svector<delayed_atom> m_asserted_atoms;
expr* m_not_handled;
ptr_vector<app> m_underspecified;
ptr_vector<expr> m_idiv_terms;
unsigned_vector m_var_trail;
vector<ptr_vector<lp_api::bound> > 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;

1
src/util/lp/lar_solver.cpp
View file

@ -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 {

2
src/util/lp/lp_settings.h
View file

@ -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