mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 21:39:13 +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 07:49:05 -07:00
parent cb7c06ddd6
commit b9ccd8647c
5 changed files with 104 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/euf/euf_ac_plugin.cpp
View file

@ -1411,8 +1411,10 @@ namespace euf {
m_monomial_table.insert(s1.m, s1); m_monomial_table.insert(s1.m, s1);
else if (s2.n->get_root() != s1.n->get_root()) { else if (s2.n->get_root() != s1.n->get_root()) {
TRACE(plugin, tout << "merge shared " << g.bpp(s1.n->get_root()) << " and " << g.bpp(s2.n->get_root()) << "\n"); TRACE(plugin, tout << "merge shared " << g.bpp(s1.n->get_root()) << " and " << g.bpp(s2.n->get_root()) << "\n");
// TODO: non-deterministic parameter evaluation auto dep1 = m_dep_manager.mk_leaf(s1.j);
push_merge(s1.n, s2.n, justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(s1.j), m_dep_manager.mk_leaf(s2.j)))); auto dep2 = m_dep_manager.mk_leaf(s2.j);
auto joined = m_dep_manager.mk_join(dep1, dep2);
push_merge(s1.n, s2.n, justification::dependent(joined));
} }
} }
} }
@ -1464,8 +1466,10 @@ namespace euf {
} }
justification ac_plugin::join(justification j, eq const& eq) { justification ac_plugin::join(justification j, eq const& eq) {
// TODO: non-deterministic parameter evaluation auto* dep1 = m_dep_manager.mk_leaf(j);
return justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(j), m_dep_manager.mk_leaf(eq.j))); auto* dep2 = m_dep_manager.mk_leaf(eq.j);
auto* joined = m_dep_manager.mk_join(dep1, dep2);
return justification::dependent(joined);
} }
} }

19
src/ast/euf/euf_bv_plugin.cpp
View file

@ -167,8 +167,11 @@ namespace euf {
unsigned lo, hi; unsigned lo, hi;
for (enode* p : enode_parents(x)) { for (enode* p : enode_parents(x)) {
if (is_concat(p, a, b) && is_value(a) && is_value(b)) if (is_concat(p, a, b) && is_value(a) && is_value(b))
// TODO: non-deterministic parameter evaluation {
push_merge(mk_concat(a->get_interpreted(), b->get_interpreted()), mk_value_concat(a, b)); enode* concat_interp = mk_concat(a->get_interpreted(), b->get_interpreted());
enode* concat_value = mk_value_concat(a, b);
push_merge(concat_interp, concat_value);
}
if (is_extract(p, lo, hi)) { if (is_extract(p, lo, hi)) {
auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1); auto val_p = mod2k(machine_div2k(val_x, lo), hi - lo + 1);
@ -182,8 +185,8 @@ namespace euf {
if (is_concat(sib, a, b)) { if (is_concat(sib, a, b)) {
auto val_a = machine_div2k(val_x, width(b)); auto val_a = machine_div2k(val_x, width(b));
auto val_b = mod2k(val_x, width(b)); auto val_b = mod2k(val_x, width(b));
// TODO: non-deterministic parameter evaluation enode* concat_value = mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b)));
push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted()); push_merge(concat_value, x->get_interpreted());
} }
} }
} }
@ -216,9 +219,11 @@ namespace euf {
if (is_extract(p1, lo_, hi_) && lo_ == lo && hi_ == hi && p1->get_arg(0)->get_root() == arg_r) if (is_extract(p1, lo_, hi_) && lo_ == lo && hi_ == hi && p1->get_arg(0)->get_root() == arg_r)
return; return;
// add the axiom instead of merge(p, mk_extract(arg, lo, hi)), which would require tracking justifications // add the axiom instead of merge(p, mk_extract(arg, lo, hi)), which would require tracking justifications
// TODO: non-deterministic parameter evaluation enode* high = mk_extract(arg, mid + 1, hi);
// TODO: non-deterministic parameter evaluation enode* low = mk_extract(arg, lo, mid);
push_merge(mk_concat(mk_extract(arg, mid + 1, hi), mk_extract(arg, lo, mid)), mk_extract(arg, lo, hi)); enode* concat = mk_concat(high, low);
enode* whole = mk_extract(arg, lo, hi);
push_merge(concat, whole);
}; };
auto propagate_above = [&](enode* b) { auto propagate_above = [&](enode* b) {

10
src/smt/dyn_ack.cpp
View file

@ -482,11 +482,13 @@ namespace smt {
clause_del_eh * del_eh = alloc(dyn_ack_clause_del_eh, *this); clause_del_eh * del_eh = alloc(dyn_ack_clause_del_eh, *this);
justification * js = nullptr; justification * js = nullptr;
if (m.proofs_enabled()) { if (m.proofs_enabled()) {
// TODO: non-deterministic parameter evaluation app_ref eq_n1_r(m.mk_eq(n1, r), m);
app_ref eq_n2_r(m.mk_eq(n2, r), m);
app_ref eq_n1_n2(m.mk_eq(n1, n2), m);
js = alloc(dyn_ack_eq_justification, n1, n2, r, js = alloc(dyn_ack_eq_justification, n1, n2, r,
m.mk_eq(n1, r), eq_n1_r.get(),
m.mk_eq(n2, r), eq_n2_r.get(),
m.mk_eq(n1, n2)); eq_n1_n2.get());
} }
ctx.mark_as_relevant(eq1); ctx.mark_as_relevant(eq1);
ctx.mark_as_relevant(eq2); ctx.mark_as_relevant(eq2);

18
src/tactic/smtlogics/qfauflia_tactic.cpp
View file

@ -29,16 +29,20 @@ tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p) {
main_p.set_bool("elim_and", true); main_p.set_bool("elim_and", true);
main_p.set_bool("som", true); main_p.set_bool("som", true);
main_p.set_bool("sort_store", true); main_p.set_bool("sort_store", true);
params_ref solver_p; params_ref solver_p;
solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module
// TODO: non-deterministic parameter evaluation tactic* simplify1 = mk_simplify_tactic(m);
tactic * preamble_st = and_then(mk_simplify_tactic(m), tactic* propagate = mk_propagate_values_tactic(m);
mk_propagate_values_tactic(m), tactic* solve_eqs = mk_solve_eqs_tactic(m);
mk_solve_eqs_tactic(m), tactic* elim_unc = mk_elim_uncnstr_tactic(m);
mk_elim_uncnstr_tactic(m), tactic* simplify2 = mk_simplify_tactic(m);
mk_simplify_tactic(m) tactic * preamble_st = and_then(simplify1,
propagate,
solve_eqs,
elim_unc,
simplify2
); );
tactic * st = and_then(using_params(preamble_st, main_p), tactic * st = and_then(using_params(preamble_st, main_p),

109
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -57,26 +57,40 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
hoist_p.set_bool("som", false); hoist_p.set_bool("som", false);
hoist_p.set_bool("flat_and_or", false); hoist_p.set_bool("flat_and_or", false);
return tactic* simplify1 = mk_simplify_tactic(m);
// TODO: non-deterministic parameter evaluation tactic* simplify1_param = using_params(simplify1, flat_and_or_p);
and_then( tactic* propagate = mk_propagate_values_tactic(m);
using_params(mk_simplify_tactic(m), flat_and_or_p), tactic* propagate_param = using_params(propagate, flat_and_or_p);
using_params(mk_propagate_values_tactic(m), flat_and_or_p), tactic* solve_eqs = mk_solve_eqs_tactic(m);
using_params(mk_solve_eqs_tactic(m), solve_eq_p), tactic* solve_eqs_param = using_params(solve_eqs, solve_eq_p);
mk_elim_uncnstr_tactic(m), tactic* elim_unc = mk_elim_uncnstr_tactic(m);
if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))), tactic* size_reduction = mk_bv_size_reduction_tactic(m);
using_params(mk_simplify_tactic(m), simp2_p), tactic* guarded_size = if_no_proofs(if_no_unsat_cores(size_reduction));
tactic* simplify2 = mk_simplify_tactic(m);
tactic* simplify2_param = using_params(simplify2, simp2_p);
tactic* simplify3 = mk_simplify_tactic(m);
tactic* simplify3_param = using_params(simplify3, hoist_p);
tactic* max_sharing = mk_max_bv_sharing_tactic(m);
tactic* ackermann = mk_ackermannize_bv_tactic(m,p);
tactic* guarded_ackermann = if_no_proofs(if_no_unsat_cores(ackermann));
// //
// Z3 can solve a couple of extra benchmarks by using hoist_mul // Z3 can solve a couple of extra benchmarks by using hoist_mul
// but the timeout in SMT-COMP is too small. // but the timeout in SMT-COMP is too small.
// Moreover, it impacted negatively some easy benchmarks. // Moreover, it impacted negatively some easy benchmarks.
// We should decide later, if we keep it or not. // We should decide later, if we keep it or not.
// //
using_params(mk_simplify_tactic(m), hoist_p), return and_then(
mk_max_bv_sharing_tactic(m), simplify1_param,
if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m,p))) propagate_param,
); solve_eqs_param,
elim_unc,
guarded_size,
simplify2_param,
simplify3_param,
max_sharing,
guarded_ackermann
);
} }
static tactic * main_p(tactic* t) { static tactic * main_p(tactic* t) {
@ -99,24 +113,32 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed. solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed.
tactic* preamble_st = mk_qfbv_preamble(m, p); tactic* preamble_st = mk_qfbv_preamble(m, p);
tactic * st = main_p(and_then(preamble_st, tactic* bv1_blaster = mk_bv1_blaster_tactic(m);
// If the user sets HI_DIV0=false, then the formula may contain uninterpreted function tactic* smt_with_solver = using_params(smt, solver_p);
// symbols. In this case, we should not use the `sat', but instead `smt'. Alternatively, tactic* eq_branch = and_then(bv1_blaster, smt_with_solver);
// the UFs can be eliminated by eager ackermannization in the preamble.
cond(mk_is_qfbv_eq_probe(), tactic* bit_blaster = mk_bit_blaster_tactic(m);
and_then(mk_bv1_blaster_tactic(m), probe* memory_probe = mk_memory_probe();
using_params(smt, solver_p)), probe* mem_limit = mk_const_probe(MEMLIMIT);
cond(mk_is_qfbv_probe(), probe* memory_ok = mk_lt(memory_probe, mem_limit);
and_then(mk_bit_blaster_tactic(m),
// TODO: non-deterministic parameter evaluation tactic* simplify4 = mk_simplify_tactic(m);
when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), tactic* solve_eqs4 = mk_solve_eqs_tactic(m);
// TODO: non-deterministic parameter evaluation tactic* simplify_and_solve = and_then(simplify4, solve_eqs4);
and_then(using_params(and_then(mk_simplify_tactic(m), tactic* simplify_and_solve_with_params = using_params(simplify_and_solve, local_ctx_p);
mk_solve_eqs_tactic(m)), tactic* aig = mk_aig_tactic();
local_ctx_p), tactic* guarded_aig = if_no_proofs(aig);
if_no_proofs(mk_aig_tactic()))), tactic* memory_branch = and_then(simplify_and_solve_with_params, guarded_aig);
sat), tactic* when_memory = when(memory_ok, memory_branch);
smt))));
tactic* bit_branch = and_then(bit_blaster, when_memory, sat);
tactic* standard_branch = cond(mk_is_qfbv_probe(), bit_branch, smt);
tactic* combined = cond(mk_is_qfbv_eq_probe(),
eq_branch,
standard_branch);
tactic * st = main_p(and_then(preamble_st, combined));
st->updt_params(p); st->updt_params(p);
return st; return st;
@ -125,11 +147,14 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
// TODO: non-deterministic parameter evaluation tactic* simplify = mk_simplify_tactic(m);
tactic * new_sat = cond(mk_produce_proofs_probe(), tactic* smt = mk_smt_tactic(m, p);
// TODO: non-deterministic parameter evaluation tactic* simplify_then_smt = and_then(simplify, smt);
and_then(mk_simplify_tactic(m), mk_smt_tactic(m, p)), probe* produce_proofs = mk_produce_proofs_probe();
mk_psat_tactic(m, p)); tactic* psat = mk_psat_tactic(m, p);
tactic * new_sat = cond(produce_proofs,
simplify_then_smt,
psat);
return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic(m, p)); return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic(m, p));
} }