From 5492d0e1355e0979eda801a3110224c6a040fdfc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Sep 2017 11:03:57 -0700 Subject: [PATCH] re-introduce eq2ineq name for rewriting parameter Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 4 +-- src/ast/rewriter/arith_rewriter.h | 2 +- src/ast/rewriter/arith_rewriter_params.pyg | 2 +- src/cmd_context/pdecl.cpp | 25 ----------------- src/muz/pdr/pdr_context.cpp | 6 ++-- src/smt/asserted_formulas.cpp | 2 +- src/smt/params/theory_arith_params.cpp | 4 +-- src/smt/params/theory_arith_params.h | 4 +-- src/smt/smt_setup.cpp | 32 +++++++++++----------- 9 files changed, 28 insertions(+), 53 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index fbfcabd78..275290665 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -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; } diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index af9d0e09d..1bef9a964 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -55,7 +55,7 @@ class arith_rewriter : public poly_rewriter { 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; diff --git a/src/ast/rewriter/arith_rewriter_params.pyg b/src/ast/rewriter/arith_rewriter_params.pyg index d40f46917..c7374105a 100644 --- a/src/ast/rewriter/arith_rewriter_params.pyg +++ b/src/ast/rewriter/arith_rewriter_params.pyg @@ -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)))."))) diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index a9ce0b69c..04456c076 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -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); } diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index 0190044b1..fd734ea66 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -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; } } } diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index f37cabde8..1581e70bd 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -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(); diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 9b8aa9b81..250848db4 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -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 diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 89c4fe46c..1fe7e1163 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -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), diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index f0c44a574..50b49f3b8 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -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