mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 05:49: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:35:24 -07:00
parent 77962ff3bb
commit d628027884
2 changed files with 70 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/nla_common.cpp
View file

@ -80,8 +80,9 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_depende
if (!c().is_monic_var(j)) { if (!c().is_monic_var(j)) {
c().insert_to_active_var_set(j); c().insert_to_active_var_set(j);
// TODO: non-deterministic parameter evaluation nex* coeff_term = cn.mk_scalar(coeff);
return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); nex* var_term = cn.mk_var(j);
return cn.mk_mul(coeff_term, var_term);
} }
const monic& m = c().emons()[j]; const monic& m = c().emons()[j];
nex_creator::mul_factory mf(cn); nex_creator::mul_factory mf(cn);

107
src/tactic/smtlogics/quant_tactics.cpp
View file

@ -43,19 +43,29 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f
solve_eqs = mk_skip_tactic(); solve_eqs = mk_skip_tactic();
} }
else { else {
// TODO: non-deterministic parameter evaluation probe* has_pattern = mk_has_pattern_probe();
solve_eqs = when(mk_not(mk_has_pattern_probe()), mk_solve_eqs_tactic(m)); probe* no_pattern = mk_not(has_pattern);
tactic* solve_eqs_core = mk_solve_eqs_tactic(m);
solve_eqs = when(no_pattern, solve_eqs_core);
} }
// remark: investigate if gaussian elimination is useful when patterns are not provided. // remark: investigate if gaussian elimination is useful when patterns are not provided.
// TODO: non-deterministic parameter evaluation tactic* simplify1 = mk_simplify_tactic(m);
return and_then(mk_simplify_tactic(m), tactic* propagate = mk_propagate_values_tactic(m);
mk_propagate_values_tactic(m), tactic* ctx_simplify = mk_ctx_simplify_tactic(m);
using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), tactic* ctx_simplify_with_params = using_params(ctx_simplify, ctx_simp_p);
using_params(mk_simplify_tactic(m), pull_ite_p), tactic* simplify2 = mk_simplify_tactic(m);
tactic* simplify_with_pull_ite = using_params(simplify2, pull_ite_p);
tactic* elim_unc = mk_elim_uncnstr_tactic(m);
tactic* simplify3 = mk_simplify_tactic(m);
return and_then(simplify1,
propagate,
ctx_simplify_with_params,
simplify_with_pull_ite,
solve_eqs, solve_eqs,
mk_elim_uncnstr_tactic(m), elim_unc,
mk_simplify_tactic(m)); simplify3);
} }
static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) { static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) {
@ -63,18 +73,21 @@ static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) {
} }
tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) { tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) {
// TODO: non-deterministic parameter evaluation tactic* preprocessor = mk_no_solve_eq_preprocessor(m);
tactic * st = and_then(mk_no_solve_eq_preprocessor(m), tactic* qe = mk_qe_lite_tactic(m, p);
mk_qe_lite_tactic(m, p), tactic* smt = mk_smt_tactic(m);
mk_smt_tactic(m)); tactic * st = and_then(preprocessor,
qe,
smt);
st->updt_params(p); st->updt_params(p);
return st; return st;
} }
tactic * mk_uflra_tactic(ast_manager & m, params_ref const & p) { tactic * mk_uflra_tactic(ast_manager & m, params_ref const & p) {
// TODO: non-deterministic parameter evaluation tactic* preprocessor = mk_quant_preprocessor(m);
tactic * st = and_then(mk_quant_preprocessor(m), tactic* smt = mk_smt_tactic(m);
mk_smt_tactic(m)); tactic * st = and_then(preprocessor,
smt);
st->updt_params(p); st->updt_params(p);
return st; return st;
} }
@ -83,44 +96,59 @@ tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p) {
params_ref qi_p; params_ref qi_p;
qi_p.set_str("qi.cost", "0"); qi_p.set_str("qi.cost", "0");
TRACE(qi_cost, qi_p.display(tout); tout << "\n" << qi_p.get_str("qi.cost", "<null>") << "\n";); TRACE(qi_cost, qi_p.display(tout); tout << "\n" << qi_p.get_str("qi.cost", "<null>") << "\n";);
tactic * st = and_then(mk_no_solve_eq_preprocessor(m), tactic* preprocessor = mk_no_solve_eq_preprocessor(m);
// TODO: non-deterministic parameter evaluation probe* num_exprs = mk_num_exprs_probe();
or_else(and_then(fail_if(mk_gt(mk_num_exprs_probe(), mk_const_probe(static_cast<double>(128)))), probe* limit_probe = mk_const_probe(static_cast<double>(128));
using_params(mk_smt_tactic(m), qi_p), probe* gt_probe = mk_gt(num_exprs, limit_probe);
mk_fail_if_undecided_tactic()), tactic* fail_guard = fail_if(gt_probe);
mk_smt_tactic(m))); tactic* smt_with_params = using_params(mk_smt_tactic(m), qi_p);
tactic* fail_undecided = mk_fail_if_undecided_tactic();
tactic* guarded_branch = and_then(fail_guard, smt_with_params, fail_undecided);
tactic* default_smt = mk_smt_tactic(m);
tactic* branch = or_else(guarded_branch, default_smt);
tactic * st = and_then(preprocessor, branch);
st->updt_params(p); st->updt_params(p);
return st; return st;
} }
tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p) { tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p) {
// TODO: non-deterministic parameter evaluation tactic* preprocessor = mk_quant_preprocessor(m);
tactic * st = and_then(mk_quant_preprocessor(m), tactic* smt = mk_smt_tactic(m);
mk_smt_tactic(m)); tactic * st = and_then(preprocessor,
smt);
st->updt_params(p); st->updt_params(p);
return st; return st;
} }
tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) { tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) {
// TODO: non-deterministic parameter evaluation tactic* preprocessor = mk_quant_preprocessor(m);
tactic * st = and_then(mk_quant_preprocessor(m), tactic* smt = mk_smt_tactic(m);
mk_smt_tactic(m)); tactic * st = and_then(preprocessor,
smt);
st->updt_params(p); st->updt_params(p);
return st; return st;
} }
tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) {
// TODO: non-deterministic parameter evaluation tactic* preprocessor = mk_quant_preprocessor(m);
tactic * st = and_then(mk_quant_preprocessor(m), tactic* qe = mk_qe_lite_tactic(m, p);
mk_qe_lite_tactic(m, p),
// TODO: non-deterministic parameter evaluation probe* has_quant_probe = mk_has_quantifier_probe();
cond(mk_has_quantifier_probe(), probe* is_lira_probe = mk_is_lira_probe();
// TODO: non-deterministic parameter evaluation
cond(mk_is_lira_probe(), tactic* qsat = mk_qsat_tactic(m, p);
// TODO: non-deterministic parameter evaluation tactic* smt_for_qsat = mk_smt_tactic(m);
or_else(mk_qsat_tactic(m, p), mk_smt_tactic(m)), tactic* qsat_branch = or_else(qsat, smt_for_qsat);
mk_smt_tactic(m)),
mk_smt_tactic(m))); tactic* smt_after_lira = mk_smt_tactic(m);
tactic* lira_branch = cond(is_lira_probe, qsat_branch, smt_after_lira);
tactic* smt_no_quant = mk_smt_tactic(m);
tactic* quant_branch = cond(has_quant_probe, lira_branch, smt_no_quant);
tactic * st = and_then(preprocessor,
qe,
quant_branch);
st->updt_params(p); st->updt_params(p);
return st; return st;
} }
@ -132,4 +160,3 @@ tactic * mk_lia_tactic(ast_manager & m, params_ref const & p) {
tactic * mk_lira_tactic(ast_manager & m, params_ref const & p) { tactic * mk_lira_tactic(ast_manager & m, params_ref const & p) {
return mk_lra_tactic(m, p); return mk_lra_tactic(m, p);
} }