mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

re-introduce eq2ineq name for rewriting parameter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-04 11:03:57 -07:00
parent 93474c0263
commit 5492d0e135
9 changed files with 28 additions and 53 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/arith_rewriter.cpp
View file

@ -35,7 +35,7 @@ void arith_rewriter::updt_local_params(params_ref const & _p) {
m_mul2power = p.mul_to_power();
m_elim_rem = p.elim_rem();
m_expand_tan = p.expand_tan();
m_expand_eqs = p.expand_eqs();
m_eq2ineq = p.eq2ineq();
set_sort_sums(p.sort_sums());
}
@ -501,7 +501,7 @@ bool arith_rewriter::is_arith_term(expr * n) const {
}
br_status arith_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
if (m_expand_eqs) {
if (m_eq2ineq) {
result = m().mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2));
return BR_REWRITE2;
}

2
src/ast/rewriter/arith_rewriter.h
View file

@ -55,7 +55,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
bool m_push_to_real;
bool m_anum_simp;
bool m_elim_rem;
bool m_expand_eqs;
bool m_eq2ineq;
bool m_process_all_eqs;
unsigned m_max_degree;

2
src/ast/rewriter/arith_rewriter_params.pyg
View file

@ -12,5 +12,5 @@ def_module_params(module_name='rewriter',
("arith_ineq_lhs", BOOL, False, "rewrite inequalities so that right-hand-side is a constant."),
("elim_to_real", BOOL, False, "eliminate to_real from arithmetic predicates that contain only integers."),
("push_to_real", BOOL, True, "distribute to_real over * and +."),
("expand_eqs", BOOL, False, "expand equalities into two inequalities"),
("eq2ineq", BOOL, False, "expand equalities into two inequalities"),
("elim_rem", BOOL, False, "replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y))).")))

25
src/cmd_context/pdecl.cpp
View file

@ -292,27 +292,6 @@ sort * psort_decl::find(sort * const * s) {
return m_inst_cache->find(s);
}
#if 0
psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager& m, symbol const& n):
psort_decl(id, num_params, m, n) {
}
void psort_dt_decl::finalize(pdecl_manager& m) {
psort_decl::finalize(m);
}
sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) {
UNREACHABLE();
return 0;
}
void psort_dt_decl::display(std::ostream & out) const {
out << get_name() << " " << get_num_params();
}
#endif
psort_user_decl::psort_user_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, psort * p) :
psort_decl(id, num_params, m, n),
m_def(p) {
@ -859,10 +838,6 @@ psort_decl * pdecl_manager::mk_psort_user_decl(unsigned num_params, symbol const
}
//psort_decl * pdecl_manager::mk_psort_dt_decl(unsigned num_params, symbol const & n) {
// return new (a().allocate(sizeof(psort_dt_decl))) psort_dt_decl(m_id_gen.mk(), num_params, *this, n);
//}
psort_decl * pdecl_manager::mk_psort_builtin_decl(symbol const & n, family_id fid, decl_kind k) {
return new (a().allocate(sizeof(psort_builtin_decl))) psort_builtin_decl(m_id_gen.mk(), *this, n, fid, k);
}

6
src/muz/pdr/pdr_context.cpp
View file

@ -1835,16 +1835,16 @@ namespace pdr {
!m_params.pdr_use_convex_interior_generalizer()) {
if (classify.is_dl()) {
m_fparams.m_arith_mode = AS_DIFF_LOGIC;
m_fparams.m_arith_expand_eqs = true;
m_fparams.m_arith_eq2ineq = true;
}
else if (classify.is_utvpi()) {
IF_VERBOSE(1, verbose_stream() << "UTVPI\n";);
m_fparams.m_arith_mode = AS_UTVPI;
m_fparams.m_arith_expand_eqs = true;
m_fparams.m_arith_eq2ineq = true;
}
else {
m_fparams.m_arith_mode = AS_ARITH;
m_fparams.m_arith_expand_eqs = false;
m_fparams.m_arith_eq2ineq = false;
}
}
}

2
src/smt/asserted_formulas.cpp
View file

@ -123,7 +123,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
p.set_bool("arith_ineq_lhs", true);
p.set_bool("sort_sums", true);
p.set_bool("rewrite_patterns", true);
p.set_bool("expand_eqs", m_params.m_arith_expand_eqs);
p.set_bool("eq2ineq", m_params.m_arith_eq2ineq);
p.set_bool("gcd_rounding", true);
m_rewriter.updt_params(p);
flush_cache();

4
src/smt/params/theory_arith_params.cpp
View file

@ -38,14 +38,14 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_dump_lemmas = p.arith_dump_lemmas();
m_arith_reflect = p.arith_reflect();
arith_rewriter_params ap(_p);
m_arith_expand_eqs = ap.expand_eqs();
m_arith_eq2ineq = ap.eq2ineq();
}
#define DISPLAY_PARAM(X) out << #X"=" << X << std::endl;
void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_arith_expand_eqs);
DISPLAY_PARAM(m_arith_eq2ineq);
DISPLAY_PARAM(m_arith_process_all_eqs);
DISPLAY_PARAM(m_arith_mode);
DISPLAY_PARAM(m_arith_auto_config_simplex); //!< force simplex solver in auto_config

4
src/smt/params/theory_arith_params.h
View file

@ -49,7 +49,7 @@ enum arith_pivot_strategy {
};
struct theory_arith_params {
bool m_arith_expand_eqs;
bool m_arith_eq2ineq;
bool m_arith_process_all_eqs;
arith_solver_id m_arith_mode;
bool m_arith_auto_config_simplex; //!< force simplex solver in auto_config
@ -110,7 +110,7 @@ struct theory_arith_params {
theory_arith_params(params_ref const & p = params_ref()):
m_arith_expand_eqs(false),
m_arith_eq2ineq(false),
m_arith_process_all_eqs(false),
m_arith_mode(AS_ARITH),
m_arith_auto_config_simplex(false),

32
src/smt/smt_setup.cpp
View file

@ -226,7 +226,7 @@ namespace smt {
void setup::setup_QF_RDL() {
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_nnf_cnf = false;
@ -266,7 +266,7 @@ namespace smt {
TRACE("setup", tout << "setup_QF_RDL(st)\n";);
check_no_uninterpreted_functions(st, "QF_RDL");
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_nnf_cnf = false;
@ -318,7 +318,7 @@ namespace smt {
void setup::setup_QF_IDL() {
TRACE("setup", tout << "setup_QF_IDL()\n";);
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_arith_small_lemma_size = 30;
@ -336,7 +336,7 @@ namespace smt {
TRACE("setup", tout << "setup_QF_IDL(st)\n";);
check_no_uninterpreted_functions(st, "QF_IDL");
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_arith_small_lemma_size = 30;
@ -390,7 +390,7 @@ namespace smt {
m_params.m_arith_reflect = false;
m_params.m_nnf_cnf = false;
m_params.m_arith_eq_bounds = true;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
m_params.m_phase_selection = PS_ALWAYS_FALSE;
m_params.m_restart_strategy = RS_GEOMETRIC;
m_params.m_restart_factor = 1.5;
@ -406,8 +406,8 @@ namespace smt {
m_params.m_arith_reflect = false;
m_params.m_nnf_cnf = false;
if (st.m_num_uninterpreted_functions == 0) {
m_params.m_arith_expand_eqs = true;
m_params.m_arith_propagate_eqs = false;
m_params.m_arith_eq2ineq = true;
m_params.m_arith_propagate_eqs = false;
if (is_dense(st)) {
m_params.m_arith_small_lemma_size = 128;
m_params.m_lemma_gc_half = true;
@ -440,7 +440,7 @@ namespace smt {
void setup::setup_QF_LRA() {
TRACE("setup", tout << "setup_QF_LRA(st)\n";);
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_eliminate_term_ite = true;
@ -451,7 +451,7 @@ namespace smt {
void setup::setup_QF_LRA(static_features const & st) {
check_no_uninterpreted_functions(st, "QF_LRA");
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_eliminate_term_ite = true;
@ -480,7 +480,7 @@ namespace smt {
void setup::setup_QF_LIA() {
TRACE("setup", tout << "setup_QF_LIA(st)\n";);
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_nnf_cnf = false;
@ -492,12 +492,12 @@ namespace smt {
TRACE("setup", tout << "QF_LIA setup\n";);
m_params.m_relevancy_lvl = 0;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
m_params.m_arith_reflect = false;
m_params.m_arith_propagate_eqs = false;
m_params.m_nnf_cnf = false;
if (st.m_max_ite_tree_depth > 50) {
m_params.m_arith_expand_eqs = false;
m_params.m_arith_eq2ineq = false;
m_params.m_pull_cheap_ite_trees = true;
m_params.m_arith_propagate_eqs = true;
m_params.m_relevancy_lvl = 2;
@ -507,7 +507,7 @@ namespace smt {
m_params.m_arith_gcd_test = false;
m_params.m_arith_branch_cut_ratio = 4;
m_params.m_relevancy_lvl = 2;
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = 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 analsysis function to decide where lift ite is too expensive.
@ -755,7 +755,7 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_dummy, m_manager.mk_family_id("arith"), "no arithmetic"));
break;
case AS_DIFF_LOGIC:
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
if (fixnum) {
if (int_only)
m_context.register_plugin(alloc(smt::theory_fidl, m_manager, m_params));
@ -770,7 +770,7 @@ namespace smt {
}
break;
case AS_DENSE_DIFF_LOGIC:
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
if (fixnum) {
if (int_only)
m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params));
@ -785,7 +785,7 @@ namespace smt {
}
break;
case AS_UTVPI:
m_params.m_arith_expand_eqs = true;
m_params.m_arith_eq2ineq = true;
if (int_only)
m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager));
else