mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

setting defaults in AUFLIRA and AUFLIA to conservative ite-lifting. Fixing conservative setting to be after constructor in asserted_formulas. fixes #4586

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-23 13:43:54 -07:00
parent 71a32f5bb2
commit a6a041ec5d
5 changed files with 21 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/push_app_ite.cpp
View file

@ -48,9 +48,10 @@ bool push_app_ite_cfg::is_target(func_decl * decl, unsigned num_args, expr * con
} }
} }
CTRACE("push_app_ite", found_ite, tout << "found target for push app ite:\n"; CTRACE("push_app_ite", found_ite, tout << "found target for push app ite:\n";
tout << decl->get_name(); tout << "conservative " << m_conservative << "\n";
for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m); tout << decl->get_name();
tout << "\n";); for (unsigned i = 0; i < num_args; i++) tout << " " << mk_pp(args[i], m);
tout << "\n";);
return found_ite; return found_ite;
} }

15
src/ast/rewriter/push_app_ite.h
View file

@ -32,7 +32,8 @@ struct push_app_ite_cfg : public default_rewriter_cfg {
bool m_conservative; bool m_conservative;
virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args); virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args);
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr); br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
push_app_ite_cfg(ast_manager& m, bool conservative = true): m(m), m_conservative(conservative) {} push_app_ite_cfg(ast_manager& m): m(m), m_conservative(true) {}
void set_conservative(bool c) { m_conservative = c; }
bool rewrite_patterns() const { return false; } bool rewrite_patterns() const { return false; }
}; };
@ -46,26 +47,28 @@ class ng_push_app_ite_cfg : public push_app_ite_cfg {
protected: protected:
bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override; bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override;
public: public:
ng_push_app_ite_cfg(ast_manager& m, bool conservative = true): push_app_ite_cfg(m, conservative) {} ng_push_app_ite_cfg(ast_manager& m): push_app_ite_cfg(m) {}
virtual ~ng_push_app_ite_cfg() {} virtual ~ng_push_app_ite_cfg() {}
}; };
struct push_app_ite_rw : public rewriter_tpl<push_app_ite_cfg> { struct push_app_ite_rw : public rewriter_tpl<push_app_ite_cfg> {
push_app_ite_cfg m_cfg; push_app_ite_cfg m_cfg;
public: public:
push_app_ite_rw(ast_manager& m, bool conservative = true): push_app_ite_rw(ast_manager& m):
rewriter_tpl<push_app_ite_cfg>(m, m.proofs_enabled(), m_cfg), rewriter_tpl<push_app_ite_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, conservative) m_cfg(m)
{} {}
void set_conservative(bool c) { m_cfg.set_conservative(c); }
}; };
struct ng_push_app_ite_rw : public rewriter_tpl<ng_push_app_ite_cfg> { struct ng_push_app_ite_rw : public rewriter_tpl<ng_push_app_ite_cfg> {
ng_push_app_ite_cfg m_cfg; ng_push_app_ite_cfg m_cfg;
public: public:
ng_push_app_ite_rw(ast_manager& m, bool conservative = true): ng_push_app_ite_rw(ast_manager& m):
rewriter_tpl<ng_push_app_ite_cfg>(m, m.proofs_enabled(), m_cfg), rewriter_tpl<ng_push_app_ite_cfg>(m, m.proofs_enabled(), m_cfg),
m_cfg(m, conservative) m_cfg(m)
{} {}
void set_conservative(bool c) { m_cfg.set_conservative(c); }
}; };

2
src/smt/asserted_formulas.cpp
View file

@ -260,6 +260,8 @@ void asserted_formulas::reduce() {
if (!invoke(m_reduce_asserted_formulas)) return; if (!invoke(m_reduce_asserted_formulas)) return;
if (!invoke(m_pull_nested_quantifiers)) return; if (!invoke(m_pull_nested_quantifiers)) return;
if (!invoke(m_lift_ite)) return; if (!invoke(m_lift_ite)) return;
m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == LI_CONSERVATIVE);
m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE);
if (!invoke(m_ng_lift_ite)) return; if (!invoke(m_ng_lift_ite)) return;
if (!invoke(m_elim_term_ite)) return; if (!invoke(m_elim_term_ite)) return;
if (!invoke(m_refine_inj_axiom)) return; if (!invoke(m_refine_inj_axiom)) return;

6
src/smt/asserted_formulas.h
View file

@ -170,8 +170,8 @@ class asserted_formulas {
#define MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, ARG, REDUCE) \ #define MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, ARG, REDUCE) \
class NAME : public simplify_fmls { \ class NAME : public simplify_fmls { \
FUNCTOR m_functor; \
public: \ public: \
FUNCTOR m_functor; \
NAME(asserted_formulas& af):simplify_fmls(af, MSG), m_functor ARG {} \ NAME(asserted_formulas& af):simplify_fmls(af, MSG), m_functor ARG {} \
virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \ virtual void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) { \
m_functor(j.get_fml(), n, p); \ m_functor(j.get_fml(), n, p); \
@ -186,8 +186,8 @@ class asserted_formulas {
MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true); MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true);
MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true); MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true);
MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true); MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true);
MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_lift_ite == LI_CONSERVATIVE), true); MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, true);
MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE), true); MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, true);
reduce_asserted_formulas_fn m_reduce_asserted_formulas; reduce_asserted_formulas_fn m_reduce_asserted_formulas;

11
src/smt/smt_setup.cpp
View file

@ -521,10 +521,6 @@ namespace smt {
m_params.m_relevancy_lvl = 2; m_params.m_relevancy_lvl = 2;
m_params.m_arith_eq2ineq = true; m_params.m_arith_eq2ineq = true;
m_params.m_eliminate_term_ite = true; m_params.m_eliminate_term_ite = true;
// if (st.m_num_exprs < 5000 && st.m_num_ite_terms < 50) { // safeguard to avoid high memory consumption
// TODO: implement analysis function to decide where lift ite is too expensive.
// m_params.m_lift_ite = LI_FULL;
// }
} }
else { else {
m_params.m_eliminate_term_ite = true; m_params.m_eliminate_term_ite = true;
@ -643,15 +639,13 @@ namespace smt {
m_params.m_eliminate_bounds = true; m_params.m_eliminate_bounds = true;
m_params.m_qi_quick_checker = MC_UNSAT; m_params.m_qi_quick_checker = MC_UNSAT;
m_params.m_qi_lazy_threshold = 20; m_params.m_qi_lazy_threshold = 20;
// m_params.m_qi_max_eager_multipatterns = 10; /// <<< HACK
m_params.m_mbqi = true; // enabling MBQI and MACRO_FINDER by default :-) m_params.m_mbqi = true; // enabling MBQI and MACRO_FINDER by default :-)
// MACRO_FINDER is a horrible for AUFLIA and UFNIA benchmarks (boogie benchmarks in general) // MACRO_FINDER is a horrible for AUFLIA and UFNIA benchmarks (boogie benchmarks in general)
// It destroys the existing patterns. // It destroys the existing patterns.
// m_params.m_macro_finder = true; // m_params.m_macro_finder = true;
// m_params.m_ng_lift_ite = LI_CONSERVATIVE;
m_params.m_ng_lift_ite = LI_FULL;
TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";); TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
m_context.register_plugin(alloc(smt::theory_i_arith, m_context)); m_context.register_plugin(alloc(smt::theory_i_arith, m_context));
setup_arrays(); setup_arrays();
@ -665,6 +659,7 @@ namespace smt {
} }
void setup::setup_AUFLIRA(bool simple_array) { void setup::setup_AUFLIRA(bool simple_array) {
TRACE("setup", tout << "AUFLIRA\n";);
m_params.m_array_mode = simple_array ? AR_SIMPLE : AR_FULL; m_params.m_array_mode = simple_array ? AR_SIMPLE : AR_FULL;
m_params.m_phase_selection = PS_ALWAYS_FALSE; m_params.m_phase_selection = PS_ALWAYS_FALSE;
m_params.m_eliminate_bounds = true; m_params.m_eliminate_bounds = true;
@ -674,7 +669,7 @@ namespace smt {
m_params.m_qi_lazy_threshold = 20; m_params.m_qi_lazy_threshold = 20;
// //
m_params.m_macro_finder = true; m_params.m_macro_finder = true;
m_params.m_ng_lift_ite = LI_FULL; m_params.m_ng_lift_ite = LI_CONSERVATIVE;
m_params.m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP m_params.m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP
m_params.m_array_lazy_ieq = true; m_params.m_array_lazy_ieq = true;
m_params.m_array_lazy_ieq_delay = 4; m_params.m_array_lazy_ieq_delay = 4;