mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 13:07:53 +00:00
Code Activity

fix param evaluation non-determinism

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-30 08:09:06 -07:00
parent b9ccd8647c
commit 657e8c9da7
14 changed files with 274 additions and 166 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/ast/rewriter/arith_rewriter.cpp
View file

@ -1295,8 +1295,9 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
}
if (get_divides(arg1, arg2, result)) {
expr_ref zero(m_util.mk_int(0), m);
// TODO: non-deterministic parameter evaluation
result = m.mk_ite(m.mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result);
expr_ref eq_zero(m.mk_eq(zero, arg2), m);
expr_ref div_expr(m_util.mk_idiv(arg1, zero), m);
result = m.mk_ite(eq_zero, div_expr, result);
return BR_REWRITE_FULL;
}
#if 0
@ -1429,8 +1430,9 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
if (arg1 == arg2 && !is_num2) {
expr_ref zero(m_util.mk_int(0), m);
// TODO: non-deterministic parameter evaluation
result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero);
expr_ref eq_zero(m.mk_eq(arg2, zero), m);
expr_ref mod_zero(m_util.mk_mod(zero, zero), m);
result = m.mk_ite(eq_zero, mod_zero, zero);
return BR_DONE;
}
@ -1769,10 +1771,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
if (is_num_y && y.is_minus_one()) {
result = m_util.mk_div(m_util.mk_real(1), ensure_real(arg1));
// TODO: non-deterministic parameter evaluation
result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))),
m_util.mk_real(0),
result);
expr_ref zero_term(m_util.mk_numeral(rational(0), m_util.is_int(arg1)), m);
expr_ref eq_zero(m.mk_eq(arg1, zero_term), m);
expr_ref zero_real(m_util.mk_real(0), m);
result = m.mk_ite(eq_zero, zero_real, result);
return BR_REWRITE2;
}
@ -1780,10 +1782,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
// (^ t -k) --> (^ (/ 1 t) k)
result = m_util.mk_power(m_util.mk_div(m_util.mk_numeral(rational(1), false), arg1),
m_util.mk_numeral(-y, false));
// TODO: non-deterministic parameter evaluation
result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))),
m_util.mk_real(0),
result);
expr_ref zero_term(m_util.mk_numeral(rational(0), m_util.is_int(arg1)), m);
expr_ref eq_zero(m.mk_eq(arg1, zero_term), m);
expr_ref zero_real(m_util.mk_real(0), m);
result = m.mk_ite(eq_zero, zero_real, result);
return BR_REWRITE3;
}

24
src/ast/rewriter/bv2int_translator.cpp
View file

@ -320,8 +320,9 @@ void bv2int_translator::translate_bv(app* e) {
case OP_BUDIV:
case OP_BUDIV_I: {
expr* x = umod(e, 0), * y = umod(e, 1);
// TODO: non-deterministic parameter evaluation
r = if_eq(y, 0, a.mk_int(-1), a.mk_idiv(x, y));
expr_ref minus_one(a.mk_int(-1), m);
expr_ref div_expr(a.mk_idiv(x, y), m);
r = if_eq(y, 0, minus_one.get(), div_expr.get());
break;
}
case OP_BUMUL_NO_OVFL: {
@ -399,10 +400,12 @@ void bv2int_translator::translate_bv(app* e) {
unsigned sz = bv.get_bv_size(e);
IF_VERBOSE(4, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n");
r = arg(0);
expr_ref two(a.mk_int(2), m);
for (unsigned i = 1; i < args.size(); ++i) {
expr* q = arg(i);
// TODO: non-deterministic parameter evaluation
r = a.mk_sub(add(r, q), mul(a.mk_int(2), a.mk_band(sz, r, q)));
expr_ref band_expr(a.mk_band(sz, r, q), m);
expr_ref mul_expr(mul(two.get(), band_expr.get()), m);
r = a.mk_sub(add(r, q), mul_expr.get());
}
if (e->get_decl_kind() == OP_BXNOR)
r = bnot(r);
@ -440,8 +443,9 @@ void bv2int_translator::translate_bv(app* e) {
expr* lhs = umod(bv_expr, 0);
expr* rhs = umod(bv_expr, 1);
expr* eq = m.mk_eq(lhs, rhs);
// TODO: non-deterministic parameter evaluation
r = m.mk_ite(eq, a.mk_int(1), a.mk_int(0));
expr_ref one(a.mk_int(1), m);
expr_ref zero(a.mk_int(0), m);
r = m.mk_ite(eq, one.get(), zero.get());
break;
}
case OP_BSMOD_I:
@ -460,7 +464,6 @@ void bv2int_translator::translate_bv(app* e) {
r = a.mk_uminus(u);
expr* pos_neg = m.mk_and(m.mk_not(signx), signy);
expr* neg_pos = m.mk_and(signx, m.mk_not(signy));
// TODO: non-deterministic parameter evaluation
expr* pos_pos = m.mk_and(m.mk_not(signx), m.mk_not(signy));
expr_ref add_u_y(m);
add_u_y = add(u, y);
@ -489,9 +492,10 @@ void bv2int_translator::translate_bv(app* e) {
y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y);
expr* d = a.mk_idiv(x, y);
r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d));
// TODO: non-deterministic parameter evaluation
expr* zero_case = m.mk_ite(signx, a.mk_int(1), a.mk_int(-1));
r = if_eq(y, 0, zero_case, r);
expr_ref pos_case(a.mk_int(1), m);
expr_ref neg_case(a.mk_int(-1), m);
expr_ref zero_case(m.mk_ite(signx, pos_case.get(), neg_case.get()), m);
r = if_eq(y, 0, zero_case.get(), r);
break;
}
case OP_BSREM_I:

7
src/ast/rewriter/bv_rewriter.cpp
View file

@ -945,10 +945,11 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
if (m_util.is_bv_shl(arg1, x, y)) {
expr_ref sum(m_util.mk_bv_add(y, arg2), m);
expr_ref cond(m_util.mk_ule(y, sum), m);
// TODO: non-deterministic parameter evaluation
expr_ref shl_expr(m_util.mk_bv_shl(x, sum), m);
expr* zero = mk_zero(bv_size);
result = m.mk_ite(cond,
m_util.mk_bv_shl(x, sum),
mk_zero(bv_size));
shl_expr,
zero);
return BR_REWRITE3;
}

5
src/ast/rewriter/enum2bv_rewriter.cpp
View file

@ -170,8 +170,9 @@ struct enum2bv_rewriter::imp {
ptr_vector<func_decl> const& cs = *m_dt.get_datatype_constructors(s);
f_def = m.mk_const(cs[nc-1]);
for (unsigned i = nc - 1; i-- > 0; ) {
// TODO: non-deterministic parameter evaluation
f_def = m.mk_ite(m.mk_eq(result, value2bv(i, s)), m.mk_const(cs[i]), f_def);
expr_ref eq_expr(m.mk_eq(result, value2bv(i, s)), m);
expr_ref ctor_expr(m.mk_const(cs[i]), m);
f_def = m.mk_ite(eq_expr, ctor_expr, f_def);
}
m_imp.m_enum2def.insert(f, f_def);
m_imp.m_enum2bv.insert(f, f_fresh);

59
src/ast/rewriter/seq_axioms.cpp
View file

@ -747,34 +747,47 @@ namespace seq {
VERIFY (seq.str.is_stoi(e, _s));
expr_ref s(_s, m);
m_rewrite(s);
// TODO: non-deterministic parameter evaluation
auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); };
auto digit = [&](unsigned j) { return mk_digit2int(mk_nth(s, j)); };
auto is_digit_ = [&](unsigned j) { return is_digit(mk_nth(s, j)); };
expr_ref len = mk_len(s);
expr_ref ge0 = mk_ge(e, 0);
expr_ref lek = mk_le(len, k);
add_clause(~lek, mk_eq(e, stoi2(k-1))); // len(s) <= k => stoi(s) = stoi(s, k-1)
// TODO: non-deterministic parameter evaluation
add_clause(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0))); // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0)
// TODO: non-deterministic parameter evaluation
add_clause(mk_le(len, 0), is_digit_(0), mk_eq(stoi2(0), a.mk_int(-1))); // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1
expr_ref stoi_k_1(stoi2(k-1), m);
add_clause(~lek, mk_eq(e, stoi_k_1)); // len(s) <= k => stoi(s) = stoi(s, k-1)
expr_ref len_le0(mk_le(len, 0), m);
expr_ref digit0(digit(0), m);
expr_ref is_digit0(is_digit_(0), m);
expr_ref not_is_digit0(m.mk_not(is_digit0), m);
expr_ref stoi0(stoi2(0), m);
add_clause(len_le0, not_is_digit0, mk_eq(stoi0, digit0)); // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0)
expr_ref minus_one_int(a.mk_int(-1), m);
add_clause(len_le0, is_digit0, mk_eq(stoi0, minus_one_int)); // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1
for (unsigned i = 1; i < k; ++i) {
// len(s) <= i => stoi(s, i) = stoi(s, i - 1)
add_clause(~mk_le(len, i), mk_eq(stoi2(i), stoi2(i-1)));
expr_ref len_le_i(mk_le(len, i), m);
expr_ref stoi_i(stoi2(i), m);
expr_ref stoi_prev(stoi2(i-1), m);
add_clause(~len_le_i, mk_eq(stoi_i, stoi_prev));
// len(s) > i, stoi(s, i - 1) >= 0, is_digit(nth(s, i)) => stoi(s, i) = 10*stoi(s, i - 1) + digit(i)
// len(s) > i, stoi(s, i - 1) < 0 => stoi(s, i) = -1
// len(s) > i, ~is_digit(nth(s, i)) => stoi(s, i) = -1
// TODO: non-deterministic parameter evaluation
add_clause(mk_le(len, i), ~mk_ge(stoi2(i-1), 0), ~is_digit_(i), mk_eq(stoi2(i), a.mk_add(a.mk_mul(a.mk_int(10), stoi2(i-1)), digit(i))));
// TODO: non-deterministic parameter evaluation
add_clause(mk_le(len, i), is_digit_(i), mk_eq(stoi2(i), a.mk_int(-1)));
// TODO: non-deterministic parameter evaluation
add_clause(mk_le(len, i), mk_ge(stoi2(i-1), 0), mk_eq(stoi2(i), a.mk_int(-1)));
expr_ref ge_stoi_prev(mk_ge(stoi_prev, 0), m);
expr_ref not_ge_stoi_prev(m.mk_not(ge_stoi_prev), m);
expr_ref is_digit_i(is_digit_(i), m);
expr_ref not_is_digit_i(m.mk_not(is_digit_i), m);
expr_ref digit_i(digit(i), m);
expr_ref ten(a.mk_int(10), m);
expr_ref mul_expr(a.mk_mul(ten, stoi_prev), m);
expr_ref sum_expr(a.mk_add(mul_expr, digit_i), m);
add_clause(len_le_i, not_ge_stoi_prev, not_is_digit_i, mk_eq(stoi_i, sum_expr));
add_clause(len_le_i, is_digit_i, mk_eq(stoi_i, minus_one_int));
add_clause(len_le_i, ge_stoi_prev, mk_eq(stoi_i, minus_one_int));
// stoi(s) >= 0, i < len(s) => is_digit(nth(s, i))
@ -912,17 +925,21 @@ namespace seq {
expr* e = nullptr;
VERIFY(seq.str.is_itos(s, e));
expr_ref len = mk_len(s);
// TODO: non-deterministic parameter evaluation
add_clause(mk_ge(e, 10), mk_le(len, 1));
// TODO: non-deterministic parameter evaluation
add_clause(mk_le(e, -1), mk_ge(len, 1));
expr_ref ge_e_10(mk_ge(e, 10), m);
expr_ref len_le1(mk_le(len, 1), m);
add_clause(ge_e_10, len_le1);
expr_ref le_e_minus1(mk_le(e, -1), m);
expr_ref len_ge1(mk_ge(len, 1), m);
add_clause(le_e_minus1, len_ge1);
rational lo(1);
for (unsigned i = 1; i <= k; ++i) {
lo *= rational(10);
// TODO: non-deterministic parameter evaluation
add_clause(mk_ge(e, lo), mk_le(len, i));
// TODO: non-deterministic parameter evaluation
add_clause(mk_le(e, lo - 1), mk_ge(len, i + 1));
expr_ref ge_e_lo(mk_ge(e, lo), m);
expr_ref len_le_i(mk_le(len, i), m);
add_clause(ge_e_lo, len_le_i);
expr_ref le_e_lo_minus(mk_le(e, lo - 1), m);
expr_ref len_ge_ip1(mk_ge(len, i + 1), m);
add_clause(le_e_lo_minus, len_ge_ip1);
}
}

29
src/ast/rewriter/seq_rewriter.cpp
View file

@ -1640,13 +1640,17 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
return BR_DONE;
}
break;
case same_length_c:
result = m().mk_ite(m_autil.mk_le(c, minus_one()), minus_one(),
// TODO: non-deterministic parameter evaluation
m().mk_ite(m().mk_eq(c, zero()),
m().mk_ite(m().mk_eq(a, b), zero(), minus_one()),
minus_one()));
case same_length_c: {
expr* zero_ptr = zero();
expr* minus_one_ptr = minus_one();
expr* cond_le = m_autil.mk_le(c, minus_one_ptr);
expr* cond_eq_c = m().mk_eq(c, zero_ptr);
expr* cond_eq_ab = m().mk_eq(a, b);
expr* inner = m().mk_ite(cond_eq_ab, zero_ptr, minus_one_ptr);
expr* middle = m().mk_ite(cond_eq_c, inner, minus_one_ptr);
result = m().mk_ite(cond_le, minus_one_ptr, middle);
return BR_REWRITE_FULL;
}
default:
break;
}
@ -2996,8 +3000,12 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
else if (neq_char(e, h))
result = nothing();
else
// TODO: non-deterministic parameter evaluation
result = re().mk_ite_simplify(m().mk_eq(e, h), re().mk_to_re(t), nothing());
{
expr_ref cond(m().mk_eq(e, h), m());
expr_ref to_re_expr(re().mk_to_re(t), m());
expr_ref nothing_expr = nothing();
result = re().mk_ite_simplify(cond, to_re_expr, nothing_expr);
}
}
else {
// observe that the precondition |r1|>0 is is implied by c1 for use of mk_seq_first
@ -4069,8 +4077,9 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
// recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence
// construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else []))
hd = mk_seq_first(r1);
// TODO: non-deterministic parameter evaluation
m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result);
expr_ref not_empty(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m());
expr_ref eq_head(m().mk_eq(hd, ele), m());
m_br.mk_and(not_empty, eq_head, result);
tl = re().mk_to_re(mk_seq_rest(r1));
return re_and(result, tl);
}

34
src/ast/rewriter/th_rewriter.cpp
View file

@ -258,25 +258,25 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
template<bool SWAP>
br_status pull_ite_core(func_decl * p, app * ite, app * value, expr_ref & result) {
if (m().is_eq(p)) {
// TODO: non-deterministic parameter evaluation
result = m().mk_ite(ite->get_arg(0),
mk_eq_value(ite->get_arg(1), value),
mk_eq_value(ite->get_arg(2), value));
expr* cond = ite->get_arg(0);
expr* then_branch = mk_eq_value(ite->get_arg(1), value);
expr* else_branch = mk_eq_value(ite->get_arg(2), value);
result = m().mk_ite(cond, then_branch, else_branch);
return BR_REWRITE2;
}
else {
if (SWAP) {
// TODO: non-deterministic parameter evaluation
result = m().mk_ite(ite->get_arg(0),
m().mk_app(p, value, ite->get_arg(1)),
m().mk_app(p, value, ite->get_arg(2)));
expr* cond = ite->get_arg(0);
expr* then_branch = m().mk_app(p, value, ite->get_arg(1));
expr* else_branch = m().mk_app(p, value, ite->get_arg(2));
result = m().mk_ite(cond, then_branch, else_branch);
return BR_REWRITE2;
}
else {
// TODO: non-deterministic parameter evaluation
result = m().mk_ite(ite->get_arg(0),
m().mk_app(p, ite->get_arg(1), value),
m().mk_app(p, ite->get_arg(2), value));
expr* cond = ite->get_arg(0);
expr* then_branch = m().mk_app(p, ite->get_arg(1), value);
expr* else_branch = m().mk_app(p, ite->get_arg(2), value);
result = m().mk_ite(cond, then_branch, else_branch);
return BR_REWRITE2;
}
}
@ -320,10 +320,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return pull_ite_core<false>(f, to_app(args[0]), to_app(args[1]), result);
if (m().is_ite(args[1]) && to_app(args[0])->get_arg(0) == to_app(args[1])->get_arg(0)) {
// (p (ite C A1 B1) (ite C A2 B2)) --> (ite (p A1 A2) (p B1 B2))
// TODO: non-deterministic parameter evaluation
result = m().mk_ite(to_app(args[0])->get_arg(0),
m().mk_app(f, to_app(args[0])->get_arg(1), to_app(args[1])->get_arg(1)),
m().mk_app(f, to_app(args[0])->get_arg(2), to_app(args[1])->get_arg(2)));
expr* cond = to_app(args[0])->get_arg(0);
expr* then_branch = m().mk_app(f, to_app(args[0])->get_arg(1), to_app(args[1])->get_arg(1));
expr* else_branch = m().mk_app(f, to_app(args[0])->get_arg(2), to_app(args[1])->get_arg(2));
result = m().mk_ite(cond,
then_branch,
else_branch);
return BR_REWRITE2;
}
}

8
src/muz/spacer/spacer_context.cpp
View file

@ -714,9 +714,11 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head):
m_extend_lit0(m), m_extend_lit(m),
m_all_init(false), m_has_quantified_frame(false)
{
// TODO: non-deterministic parameter evaluation
m_solver = alloc(prop_solver, m, ctx.mk_solver0(), ctx.mk_solver1(),
ctx.get_params(), head->get_name());
solver* solver0 = ctx.mk_solver0();
solver* solver1 = ctx.mk_solver1();
auto const& params = ctx.get_params();
m_solver = alloc(prop_solver, m, solver0, solver1,
params, head->get_name());
init_sig ();
m_extend_lit = mk_extend_lit();

5
src/sat/smt/arith_solver.cpp
View file

@ -751,8 +751,9 @@ namespace arith {
reset_evidence();
m_explanation.clear();
auto& dm = lp().dep_manager();
// TODO: non-deterministic parameter evaluation
auto* d = dm.mk_join(dm.mk_join(ci1, ci2), dm.mk_join(ci3, ci4));
auto* join12 = dm.mk_join(ci1, ci2);
auto* join34 = dm.mk_join(ci3, ci4);
auto* d = dm.mk_join(join12, join34);
for (auto ci : lp().flatten(d))
consume(rational::one(), ci);
enode* x = var2enode(v1);

5
src/smt/seq_regex.cpp
View file

@ -487,8 +487,9 @@ namespace smt {
expr_ref emp(re().mk_empty(r->get_sort()), m);
expr_ref n(m.mk_fresh_const("re.char", seq_sort), m);
expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n);
// TODO: non-deterministic parameter evaluation
th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_non_empty));
literal eq_lit = th.mk_eq(r1, r2, false);
literal non_empty_lit = th.mk_literal(is_non_empty);
th.add_axiom(eq_lit, non_empty_lit);
}
bool seq_regex::is_member(expr* r, expr* u) {

4
src/smt/theory_seq.cpp
View file

@ -573,8 +573,8 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
m_sk.decompose(e, head, tail);
add_axiom(~mk_eq_empty(e), mk_eq_empty(tail));;
// TODO: non-deterministic parameter evaluation
add_axiom(mk_eq_empty(e), mk_eq(e, mk_concat(head, tail), false));
expr_ref concat_expr(mk_concat(head, tail), m);
add_axiom(mk_eq_empty(e), mk_eq(e, concat_expr, false));
}
/*

8
src/smt/theory_utvpi.h
View file

@ -171,8 +171,11 @@ namespace smt {
struct var_value_eq {
theory_utvpi & m_th;
var_value_eq(theory_utvpi & th):m_th(th) {}
// TODO: non-deterministic parameter evaluation
bool operator()(theory_var v1, theory_var v2) const { return m_th.mk_value(v1, false) == m_th.mk_value(v2, false) && m_th.is_int(v1) == m_th.is_int(v2); }
bool operator()(theory_var v1, theory_var v2) const {
auto value1 = m_th.mk_value(v1, false);
auto value2 = m_th.mk_value(v2, false);
return value1 == value2 && m_th.is_int(v1) == m_th.is_int(v2);
}
};
typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;
@ -363,4 +366,3 @@ namespace smt {

8
src/tactic/core/special_relations_tactic.cpp
View file

@ -77,11 +77,11 @@ void special_relations_tactic::initialize() {
expr* pats[1] = { pat };
expr* pats0[1] = { pat0 };
// TODO: non-deterministic parameter evaluation
fml = m.mk_or(m.mk_not(Rxy), m.mk_not(Ryz), Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
fml = m.mk_or(mk_not(Rxy & Ryz), Rxz);
expr_ref trans_cond(mk_not(Rxy & Ryz), m);
fml = m.mk_or(trans_cond, Rxz);
q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_transitive);
@ -92,7 +92,8 @@ void special_relations_tactic::initialize() {
fml = m.mk_or(nRxy, nRyx, m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
fml = m.mk_or(mk_not(Rxy & Ryx), m.mk_eq(x, y));
expr_ref antisym_cond(mk_not(Rxy & Ryx), m);
fml = m.mk_or(antisym_cond, m.mk_eq(x, y));
q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats);
register_pattern(m_pm.initialize(q), sr_antisymmetric);
@ -179,4 +180,3 @@ void special_relations_tactic::operator()(goal_ref const & g, goal_ref_buffer &
tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p) {
return alloc(special_relations_tactic, m, p);
}

218
src/tactic/smtlogics/qflia_tactic.cpp
View file

@ -86,15 +86,21 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) {
// dynamic psm seems to work well.
solver_p.set_sym("gc", symbol("dyn_psm"));
// TODO: non-deterministic parameter evaluation
return using_params(and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
mk_solve_eqs_tactic(m),
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m),
mk_aig_tactic(),
mk_sat_tactic(m, solver_p)),
solver_p);
tactic* simplify = mk_simplify_tactic(m);
tactic* propagate = mk_propagate_values_tactic(m);
tactic* solve_eqs = mk_solve_eqs_tactic(m);
tactic* max_sharing = mk_max_bv_sharing_tactic(m);
tactic* bit_blaster = mk_bit_blaster_tactic(m);
tactic* aig = mk_aig_tactic();
tactic* sat = mk_sat_tactic(m, solver_p);
tactic* core = and_then(simplify,
propagate,
solve_eqs,
max_sharing,
bit_blaster,
aig,
sat);
return using_params(core, solver_p);
}
#define SMALL_SIZE 80000
@ -106,19 +112,31 @@ static tactic * mk_pb_tactic(ast_manager & m) {
params_ref bv2sat_p;
bv2sat_p.set_bool("ite_extra", true);
return annotate_tactic(
"pb-tactic",
and_then(fail_if_not(mk_is_pb_probe()),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
// TODO: non-deterministic parameter evaluation
or_else(and_then(fail_if(mk_ge(mk_num_exprs_probe(), mk_const_probe(SMALL_SIZE))),
fail_if_not(mk_is_ilp_probe()),
// try_for(mk_mip_tactic(m), 8000),
mk_fail_if_undecided_tactic()),
and_then(using_params(mk_pb2bv_tactic(m), pb2bv_p),
fail_if_not(mk_is_qfbv_probe()),
using_params(mk_bv2sat_tactic(m), bv2sat_p)))));
probe* num_exprs = mk_num_exprs_probe();
probe* size_limit = mk_const_probe(SMALL_SIZE);
probe* too_large = mk_ge(num_exprs, size_limit);
tactic* fail_large = fail_if(too_large);
tactic* fail_not_ilp = fail_if_not(mk_is_ilp_probe());
tactic* fail_undecided = mk_fail_if_undecided_tactic();
tactic* branch1 = and_then(fail_large,
fail_not_ilp,
fail_undecided);
tactic* pb2bv = mk_pb2bv_tactic(m);
tactic* pb2bv_with_params = using_params(pb2bv, pb2bv_p);
tactic* fail_not_qfbv = fail_if_not(mk_is_qfbv_probe());
tactic* bv2sat = mk_bv2sat_tactic(m);
tactic* bv2sat_with_params = using_params(bv2sat, bv2sat_p);
tactic* branch2 = and_then(pb2bv_with_params,
fail_not_qfbv,
bv2sat_with_params);
tactic* core = and_then(fail_if_not(mk_is_pb_probe()),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
or_else(branch1, branch2));
return annotate_tactic("pb-tactic", core);
}
@ -129,18 +147,29 @@ static tactic * mk_lia2sat_tactic(ast_manager & m) {
params_ref bv2sat_p;
bv2sat_p.set_bool("ite_extra", true);
return annotate_tactic(
"lia2sat-tactic",
// TODO: non-deterministic parameter evaluation
and_then(fail_if(mk_is_unbounded_probe()),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
mk_propagate_ineqs_tactic(m),
mk_normalize_bounds_tactic(m),
mk_lia2pb_tactic(m),
using_params(mk_pb2bv_tactic(m), pb2bv_p),
fail_if_not(mk_is_qfbv_probe()),
using_params(mk_bv2sat_tactic(m), bv2sat_p)));
tactic* fail_unbounded = fail_if(mk_is_unbounded_probe());
tactic* fail_proofs = fail_if(mk_produce_proofs_probe());
tactic* fail_unsat = fail_if(mk_produce_unsat_cores_probe());
tactic* propagate_ineqs = mk_propagate_ineqs_tactic(m);
tactic* normalize_bounds = mk_normalize_bounds_tactic(m);
tactic* lia2pb = mk_lia2pb_tactic(m);
tactic* pb2bv = mk_pb2bv_tactic(m);
tactic* pb2bv_with_params = using_params(pb2bv, pb2bv_p);
tactic* fail_not_qfbv = fail_if_not(mk_is_qfbv_probe());
tactic* bv2sat = mk_bv2sat_tactic(m);
tactic* bv2sat_with_params = using_params(bv2sat, bv2sat_p);
tactic* core = and_then(fail_unbounded,
fail_proofs,
fail_unsat,
propagate_ineqs,
normalize_bounds,
lia2pb,
pb2bv_with_params,
fail_not_qfbv,
bv2sat_with_params);
return annotate_tactic("lia2sat-tactic", core);
}
// Try to find a model for an unbounded ILP problem.
@ -153,24 +182,41 @@ static tactic * mk_ilp_model_finder_tactic(ast_manager & m) {
add_bounds_p2.set_rat("add_bound_lower", rational(-32));
add_bounds_p2.set_rat("add_bound_upper", rational(31));
return annotate_tactic(
"ilp-model-finder-tactic",
// TODO: non-deterministic parameter evaluation
// TODO: non-deterministic parameter evaluation
and_then(fail_if_not(mk_and(mk_is_ilp_probe(), mk_is_unbounded_probe())),
fail_if(mk_produce_proofs_probe()),
fail_if(mk_produce_unsat_cores_probe()),
mk_propagate_ineqs_tactic(m),
or_else(// try_for(mk_mip_tactic(m), 5000),
try_for(mk_no_cut_smt_tactic(m, 100), 2000),
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p1),
try_for(mk_lia2sat_tactic(m), 5000)),
try_for(mk_no_cut_smt_tactic(m, 200), 5000),
and_then(using_params(mk_add_bounds_tactic(m), add_bounds_p2),
try_for(mk_lia2sat_tactic(m), 10000))
// , mk_mip_tactic(m)
),
mk_fail_if_undecided_tactic()));
probe* is_ilp = mk_is_ilp_probe();
probe* is_unbounded = mk_is_unbounded_probe();
probe* ilp_unbounded = mk_and(is_ilp, is_unbounded);
tactic* fail_not_ilp_unbounded = fail_if_not(ilp_unbounded);
tactic* fail_proofs = fail_if(mk_produce_proofs_probe());
tactic* fail_unsat = fail_if(mk_produce_unsat_cores_probe());
tactic* propagate_ineqs = mk_propagate_ineqs_tactic(m);
tactic* add_bounds1 = mk_add_bounds_tactic(m);
tactic* add_bounds1_params = using_params(add_bounds1, add_bounds_p1);
tactic* lia2sat1 = try_for(mk_lia2sat_tactic(m), 5000);
tactic* branch_bounds1 = and_then(add_bounds1_params, lia2sat1);
tactic* add_bounds2 = mk_add_bounds_tactic(m);
tactic* add_bounds2_params = using_params(add_bounds2, add_bounds_p2);
tactic* lia2sat2 = try_for(mk_lia2sat_tactic(m), 10000);
tactic* branch_bounds2 = and_then(add_bounds2_params, lia2sat2);
tactic* branch_no_cut1 = try_for(mk_no_cut_smt_tactic(m, 100), 2000);
tactic* branch_no_cut2 = try_for(mk_no_cut_smt_tactic(m, 200), 5000);
tactic* or_branch = or_else(branch_no_cut1,
branch_bounds1,
branch_no_cut2,
branch_bounds2);
tactic* fail_undecided = mk_fail_if_undecided_tactic();
tactic* core = and_then(fail_not_ilp_unbounded,
fail_proofs,
fail_unsat,
propagate_ineqs,
or_branch,
fail_undecided);
return annotate_tactic("ilp-model-finder-tactic", core);
}
static tactic * mk_bounded_tactic(ast_manager & m) {
@ -202,16 +248,24 @@ tactic * mk_preamble_tactic(ast_manager& m) {
lia2card_p.set_uint("lia2card.max_range", 1);
lia2card_p.set_uint("lia2card.max_ite_nesting", 1);
return
// TODO: non-deterministic parameter evaluation
and_then(
mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
using_params(mk_simplify_tactic(m), pull_ite_p),
mk_solve_eqs_tactic(m),
mk_lia2card_tactic(m, lia2card_p),
mk_elim_uncnstr_tactic(m));
tactic* simplify = mk_simplify_tactic(m);
tactic* propagate = mk_propagate_values_tactic(m);
tactic* ctx_simplify = mk_ctx_simplify_tactic(m);
tactic* ctx_simplify_with_params = using_params(ctx_simplify, ctx_simp_p);
tactic* simplify2 = mk_simplify_tactic(m);
tactic* simplify_with_pull = using_params(simplify2, pull_ite_p);
tactic* solve_eqs = mk_solve_eqs_tactic(m);
tactic* lia2card = mk_lia2card_tactic(m, lia2card_p);
tactic* elim_unc = mk_elim_uncnstr_tactic(m);
return and_then(
simplify,
propagate,
ctx_simplify_with_params,
simplify_with_pull,
solve_eqs,
lia2card,
elim_unc);
}
tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
@ -230,22 +284,34 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
params_ref lhs_p;
lhs_p.set_bool("arith_lhs", true);
tactic* st = using_params(
and_then(
mk_preamble_tactic(m),
using_params(mk_simplify_tactic(m), lhs_p),
// TODO: non-deterministic parameter evaluation
or_else(mk_ilp_model_finder_tactic(m),
mk_pb_tactic(m),
and_then(fail_if_not(mk_is_quasi_pb_probe()),
using_params(mk_lia2sat_tactic(m), quasi_pb_p),
mk_fail_if_undecided_tactic()),
mk_bounded_tactic(m),
mk_smt_tactic(m))),
main_p);
tactic* preamble = mk_preamble_tactic(m);
tactic* simplify_lhs = using_params(mk_simplify_tactic(m), lhs_p);
tactic* ilp_finder = mk_ilp_model_finder_tactic(m);
tactic* pb_tac = mk_pb_tactic(m);
tactic* fail_not_quasi = fail_if_not(mk_is_quasi_pb_probe());
tactic* lia2sat = mk_lia2sat_tactic(m);
tactic* lia2sat_with_params = using_params(lia2sat, quasi_pb_p);
tactic* fail_undecided = mk_fail_if_undecided_tactic();
tactic* quasi_branch = and_then(fail_not_quasi,
lia2sat_with_params,
fail_undecided);
tactic* bounded = mk_bounded_tactic(m);
tactic* smt = mk_smt_tactic(m);
tactic* branches = or_else(ilp_finder,
pb_tac,
quasi_branch,
bounded,
smt);
tactic* core = and_then(preamble,
simplify_lhs,
branches);
tactic* st = using_params(core, main_p);
st->updt_params(p);
return st;
}