From 94cc4ead7249af4b8a9fbca635484f5a3b428a99 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 5 Oct 2021 10:55:38 -0700
Subject: [PATCH] remove arith_lhs simplification from preamble tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/smt/q_ematch.cpp | 4 +-
src/tactic/smtlogics/qflia_tactic.cpp | 54 ++++++++++++---------------
2 files changed, 26 insertions(+), 32 deletions(-)
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 1cfc1f678..6f200680a 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -80,7 +80,7 @@ namespace q {
unsigned num_patterns = q->get_num_patterns();
for (unsigned i = 0; i < num_patterns; 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.rhs);
}
@@ -186,7 +186,7 @@ namespace q {
void ematch::init_watch(clause& c) {
unsigned idx = c.index();
- for (auto lit : c.m_lits) {
+ for (auto const& lit : c.m_lits) {
if (!is_ground(lit.lhs))
init_watch(lit.lhs, idx);
if (!is_ground(lit.rhs))
diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp
index 8673b6380..b8ebbd8a9 100644
--- a/src/tactic/smtlogics/qflia_tactic.cpp
+++ b/src/tactic/smtlogics/qflia_tactic.cpp
@@ -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_steps", 5000000);
- params_ref lhs_p;
- lhs_p.set_bool("arith_lhs", true);
-
- tactic * preamble_st = and_then(mk_simplify_tactic(m),
- mk_propagate_values_tactic(m),
- using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
- using_params(mk_simplify_tactic(m), pull_ite_p)
- );
-
- 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;
+ return
+ and_then(
+ mk_simplify_tactic(m),
+ mk_propagate_values_tactic(m),
+ using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
+ using_params(mk_simplify_tactic(m), pull_ite_p),
+ mk_solve_eqs_tactic(m),
+ mk_elim_uncnstr_tactic(m));
}
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_uint("blast_distinct_threshold", 128);
// main_p.set_bool("push_ite_arith", true);
-
-
-
+
params_ref quasi_pb_p;
quasi_pb_p.set_uint("lia2pb_max_bits", 64);
-
- tactic * preamble_st = mk_preamble_tactic(m);
- tactic * st = using_params(and_then(preamble_st,
- or_else(mk_ilp_model_finder_tactic(m),
- 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);
+ params_ref lhs_p;
+ lhs_p.set_bool("arith_lhs", true);
+
+ tactic* st = using_params(
+ and_then(
+ mk_preamble_tactic(m),
+ using_params(mk_simplify_tactic(m), lhs_p),
+ or_else(mk_ilp_model_finder_tactic(m),
+ 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);