mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +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:04:16 -07:00
parent b812c15723
commit 4b2a4a902d
6 changed files with 78 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/polynomial/polynomial.cpp
View file

@ -2995,16 +2995,18 @@ namespace polynomial {
polynomial * add(polynomial const * p1, polynomial const * p2) {
numeral one(1);
// TODO: non-deterministic parameter evaluation
return addmul(one, mk_unit(), p1, one, mk_unit(), p2);
monomial* unit1 = mk_unit();
monomial* unit2 = mk_unit();
return addmul(one, unit1, p1, one, unit2, p2);
}
polynomial * sub(polynomial const * p1, polynomial const * p2) {
numeral one(1);
numeral minus_one; // It is incorrect to initialize with -1 when numeral_manager is GF_2
m_manager.set(minus_one, -1);
// TODO: non-deterministic parameter evaluation
return addmul(one, mk_unit(), p1, minus_one, mk_unit(), p2);
monomial* unit1 = mk_unit();
monomial* unit2 = mk_unit();
return addmul(one, unit1, p1, minus_one, unit2, p2);
}

6
src/model/model.cpp
View file

@ -625,8 +625,10 @@ void model::add_rec_funs() {
expr_safe_replace subst(m);
unsigned arity = f->get_arity();
for (unsigned i = 0; i < arity; ++i) {
// TODO: non-deterministic parameter evaluation
subst.insert(m.mk_var(arity - i - 1, f->get_domain(i)), m.mk_var(i, f->get_domain(i)));
sort* dom = f->get_domain(i);
expr* lhs = m.mk_var(arity - i - 1, dom);
expr* rhs = m.mk_var(i, dom);
subst.insert(lhs, rhs);
}
expr_ref bodyr(m);
subst(rhs, bodyr);

8
src/model/model_evaluator.cpp
View file

@ -457,8 +457,12 @@ struct evaluator_cfg : public default_rewriter_cfg {
if (interp) {
var_subst vs(m, false);
result = vs(fi->get_interp(), num, args);
// TODO: non-deterministic parameter evaluation
result = m.mk_ite(m.mk_eq(m_au.mk_numeral(rational(0), args[1]->get_sort()), args[1]), result, m.mk_app(f, num, args));
expr_ref zero(m_au.mk_numeral(rational(0), args[1]->get_sort()), m);
expr_ref is_zero(m);
is_zero = m.mk_eq(zero, args[1]);
expr_ref app_expr(m);
app_expr = m.mk_app(f, num, args);
result = m.mk_ite(is_zero, result, app_expr);
return BR_DONE;
}
}

14
src/opt/opt_context.cpp
View file

@ -891,12 +891,14 @@ namespace opt {
g->assert_expr(fml);
for (expr * a : asms)
g->assert_expr(a, a);
tactic_ref tac0 =
// TODO: non-deterministic parameter evaluation
and_then(mk_simplify_tactic(m, m_params),
mk_propagate_values_tactic(m),
m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m),
mk_simplify_tactic(m));
tactic* simplify_with_params = mk_simplify_tactic(m, m_params);
tactic* propagate_values = mk_propagate_values_tactic(m);
tactic* solve_or_skip = m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m);
tactic* simplify_plain = mk_simplify_tactic(m);
tactic_ref tac0 = and_then(simplify_with_params,
propagate_values,
solve_or_skip,
simplify_plain);
opt_params optp(m_params);
tactic_ref tac1, tac2, tac3, tac4;
bool has_dep = false;

39
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -653,22 +653,29 @@ public:
simp2_p.set_bool("flat", false);
sat_params sp(m_params);
if (sp.euf())
m_preprocess =
// TODO: non-deterministic parameter evaluation
and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m));
else
m_preprocess =
// TODO: non-deterministic parameter evaluation
and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
mk_card2bv_tactic(m, m_params), // updates model converter
using_params(mk_simplify_tactic(m), simp1_p),
mk_max_bv_sharing_tactic(m),
mk_bit_blaster_tactic(m, m_bb_rewriter.get()),
using_params(mk_simplify_tactic(m), simp2_p)
);
if (sp.euf()) {
tactic* simplify = mk_simplify_tactic(m);
tactic* propagate = mk_propagate_values_tactic(m);
m_preprocess = and_then(simplify, propagate);
}
else {
tactic* simplify1 = mk_simplify_tactic(m);
tactic* propagate = mk_propagate_values_tactic(m);
tactic* card2bv = mk_card2bv_tactic(m, m_params); // updates model converter
tactic* simplify_param1 = mk_simplify_tactic(m);
tactic* simplify_with_params1 = using_params(simplify_param1, simp1_p);
tactic* max_sharing = mk_max_bv_sharing_tactic(m);
tactic* bit_blaster = mk_bit_blaster_tactic(m, m_bb_rewriter.get());
tactic* simplify_param2 = mk_simplify_tactic(m);
tactic* simplify_with_params2 = using_params(simplify_param2, simp2_p);
m_preprocess = and_then(simplify1,
propagate,
card2bv,
simplify_with_params1,
max_sharing,
bit_blaster,
simplify_with_params2);
}
while (m_bb_rewriter->get_num_scopes() < m_num_scopes) {
m_bb_rewriter->push();
}

49
src/tactic/fpa/qffp_tactic.cpp
View file

@ -82,26 +82,39 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) {
simp_p.set_bool("arith_lhs", true);
simp_p.set_bool("elim_and", true);
// TODO: non-deterministic parameter evaluation
tactic * preamble = and_then(mk_simplify_tactic(m, simp_p),
mk_propagate_values_tactic(m, p),
mk_fpa2bv_tactic(m, p),
mk_propagate_values_tactic(m, p),
using_params(mk_simplify_tactic(m, p), simp_p),
if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m, p))));
tactic* simplify_simp = mk_simplify_tactic(m, simp_p);
tactic* propagate1 = mk_propagate_values_tactic(m, p);
tactic* fpa2bv = mk_fpa2bv_tactic(m, p);
tactic* propagate2 = mk_propagate_values_tactic(m, p);
tactic* simplify_for_params = mk_simplify_tactic(m, p);
tactic* simplify_with_params = using_params(simplify_for_params, simp_p);
tactic* ackermann = mk_ackermannize_bv_tactic(m, p);
tactic* ackermann_guard = if_no_proofs(if_no_unsat_cores(ackermann));
tactic * preamble = and_then(simplify_simp,
propagate1,
fpa2bv,
propagate2,
simplify_with_params,
ackermann_guard);
tactic* bit_blaster = mk_bit_blaster_tactic(m, p);
tactic* simplify_post_bb = mk_simplify_tactic(m, p);
tactic* simplify_post_bb_params = using_params(simplify_post_bb, simp_p);
probe* propositional_probe = mk_is_propositional_probe();
probe* produce_proofs_probe = mk_produce_proofs_probe();
tactic* smt_with_proofs = mk_smt_tactic(m, p); // `sat' does not support proofs.
tactic* psat = mk_psat_tactic(m, p);
tactic* proofs_branch = cond(produce_proofs_probe, smt_with_proofs, psat);
probe* fp_qfnra_probe = mk_is_fp_qfnra_probe();
tactic* qfnra = mk_qfnra_tactic(m, p);
tactic* smt_default = mk_smt_tactic(m, p);
tactic* fp_branch = cond(fp_qfnra_probe, qfnra, smt_default);
tactic* top_branch = cond(propositional_probe, proofs_branch, fp_branch);
tactic * st = and_then(preamble,
mk_bit_blaster_tactic(m, p),
using_params(mk_simplify_tactic(m, p), simp_p),
cond(mk_is_propositional_probe(),
// TODO: non-deterministic parameter evaluation
cond(mk_produce_proofs_probe(),
mk_smt_tactic(m, p), // `sat' does not support proofs.
mk_psat_tactic(m, p)),
// TODO: non-deterministic parameter evaluation
cond(mk_is_fp_qfnra_probe(),
mk_qfnra_tactic(m, p),
mk_smt_tactic(m, p))));
bit_blaster,
simplify_post_bb_params,
top_branch);
st->updt_params(p);
return st;