mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Merge pull request #282 from NikolajBjorner/master
enable further simplifications to reduce coercions
This commit is contained in:
commit
5489d60874
|
@ -323,7 +323,6 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
|
|||
if ((is_zero(arg1) && is_reduce_power_target(arg2, kind == EQ)) ||
|
||||
(is_zero(arg2) && is_reduce_power_target(arg1, kind == EQ)))
|
||||
return reduce_power(arg1, arg2, kind, result);
|
||||
CTRACE("elim_to_real", m_elim_to_real, tout << "after_elim_to_real\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";);
|
||||
br_status st = cancel_monomials(arg1, arg2, m_arith_lhs, new_arg1, new_arg2);
|
||||
TRACE("mk_le_bug", tout << "st: " << st << "\n";);
|
||||
if (st != BR_FAILED) {
|
||||
|
@ -335,6 +334,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
|
|||
if (m_elim_to_real && elim_to_real(arg1, arg2, new_new_arg1, new_new_arg2)) {
|
||||
arg1 = new_new_arg1;
|
||||
arg2 = new_new_arg2;
|
||||
CTRACE("elim_to_real", m_elim_to_real, tout << "after_elim_to_real\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";);
|
||||
if (st == BR_FAILED)
|
||||
st = BR_DONE;
|
||||
}
|
||||
|
|
|
@ -137,6 +137,7 @@ namespace opt {
|
|||
params_ref p;
|
||||
p.set_bool("model", true);
|
||||
p.set_bool("unsat_core", true);
|
||||
p.set_bool("elim_to_real", true);
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
|
@ -661,7 +662,7 @@ namespace opt {
|
|||
g->assert_expr(fmls[i].get());
|
||||
}
|
||||
tactic_ref tac0 =
|
||||
and_then(mk_simplify_tactic(m),
|
||||
and_then(mk_simplify_tactic(m, m_params),
|
||||
mk_propagate_values_tactic(m),
|
||||
mk_solve_eqs_tactic(m),
|
||||
// NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
|
||||
|
|
Loading…
Reference in a new issue