mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

remove arith_lhs simplification from preamble tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-10-05 10:55:38 -07:00
parent 33f4e65fa9
commit 94cc4ead72
2 changed files with 26 additions and 32 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/q_ematch.cpp
View file

@ -80,7 +80,7 @@ namespace q {
unsigned num_patterns = q->get_num_patterns(); unsigned num_patterns = q->get_num_patterns();
for (unsigned i = 0; i < num_patterns; i++) for (unsigned i = 0; i < num_patterns; i++)
ensure_ground_enodes(q->get_pattern(i)); ensure_ground_enodes(q->get_pattern(i));
for (auto lit : c.m_lits) { for (auto const& lit : c.m_lits) {
ensure_ground_enodes(lit.lhs); ensure_ground_enodes(lit.lhs);
ensure_ground_enodes(lit.rhs); ensure_ground_enodes(lit.rhs);
} }
@ -186,7 +186,7 @@ namespace q {
void ematch::init_watch(clause& c) { void ematch::init_watch(clause& c) {
unsigned idx = c.index(); unsigned idx = c.index();
for (auto lit : c.m_lits) { for (auto const& lit : c.m_lits) {
if (!is_ground(lit.lhs)) if (!is_ground(lit.lhs))
init_watch(lit.lhs, idx); init_watch(lit.lhs, idx);
if (!is_ground(lit.rhs)) if (!is_ground(lit.rhs))

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

@ -190,22 +190,14 @@ tactic * mk_preamble_tactic(ast_manager& m) {
ctx_simp_p.set_uint("max_depth", 30); ctx_simp_p.set_uint("max_depth", 30);
ctx_simp_p.set_uint("max_steps", 5000000); ctx_simp_p.set_uint("max_steps", 5000000);
params_ref lhs_p; return
lhs_p.set_bool("arith_lhs", true); and_then(
mk_simplify_tactic(m),
tactic * preamble_st = and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m),
mk_propagate_values_tactic(m), using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), using_params(mk_simplify_tactic(m), pull_ite_p),
using_params(mk_simplify_tactic(m), pull_ite_p) mk_solve_eqs_tactic(m),
); mk_elim_uncnstr_tactic(m));
preamble_st = and_then(preamble_st,
mk_solve_eqs_tactic(m),
mk_elim_uncnstr_tactic(m),
using_params(mk_simplify_tactic(m), lhs_p)
);
return preamble_st;
} }
tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
@ -215,23 +207,25 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) {
main_p.set_bool("blast_distinct", true); main_p.set_bool("blast_distinct", true);
main_p.set_uint("blast_distinct_threshold", 128); main_p.set_uint("blast_distinct_threshold", 128);
// main_p.set_bool("push_ite_arith", true); // main_p.set_bool("push_ite_arith", true);
params_ref quasi_pb_p; params_ref quasi_pb_p;
quasi_pb_p.set_uint("lia2pb_max_bits", 64); quasi_pb_p.set_uint("lia2pb_max_bits", 64);
tactic * preamble_st = mk_preamble_tactic(m);
tactic * st = using_params(and_then(preamble_st, params_ref lhs_p;
or_else(mk_ilp_model_finder_tactic(m), lhs_p.set_bool("arith_lhs", true);
mk_pb_tactic(m),
and_then(fail_if_not(mk_is_quasi_pb_probe()), tactic* st = using_params(
using_params(mk_lia2sat_tactic(m), quasi_pb_p), and_then(
mk_fail_if_undecided_tactic()), mk_preamble_tactic(m),
mk_bounded_tactic(m), using_params(mk_simplify_tactic(m), lhs_p),
mk_smt_tactic(m))), or_else(mk_ilp_model_finder_tactic(m),
main_p); 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);
st->updt_params(p); st->updt_params(p);