From f151879c0bb3b78155455893b3efc377a18500a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Sep 2014 16:25:41 -0700 Subject: [PATCH] enable neat vs. less neat pretty priting as an option Signed-off-by: Nikolaj Bjorner --- src/api/python/z3printer.py | 2 + src/opt/opt_context.cpp | 9 +++- src/opt/opt_context.h | 1 + src/opt/opt_params.pyg | 1 + src/smt/smt_internalizer.cpp | 2 +- src/smt/smt_setup.cpp | 14 ++++++- src/smt/theory_arith.h | 9 +++- src/smt/theory_arith_core.h | 73 +++++++++++++++++++++++++-------- src/smt/theory_diff_logic_def.h | 9 ++++ 9 files changed, 98 insertions(+), 22 deletions(-) diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py index d1d85d30e..bd4c72477 100644 --- a/src/api/python/z3printer.py +++ b/src/api/python/z3printer.py @@ -842,6 +842,8 @@ class Formatter: return self.pp_seq(a.assertions(), 0, []) elif isinstance(a, z3.Fixedpoint): return a.sexpr() + elif isinstance(a, z3.Optimize): + return a.sexpr() elif isinstance(a, z3.ApplyResult): return self.pp_seq_seq(a, 0, []) elif isinstance(a, z3.ModelRef): diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 79986067e..db373494a 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -38,6 +38,7 @@ Notes: #include "inc_sat_solver.h" #include "bv_decl_plugin.h" #include "pb_decl_plugin.h" +#include "ast_smt_pp.h" namespace opt { @@ -122,7 +123,8 @@ namespace opt { m_fm(m), m_objective_refs(m), m_enable_sat(false), - m_enable_sls(false) + m_enable_sls(false), + m_pp_neat(false) { params_ref p; p.set_bool("model", true); @@ -1063,6 +1065,7 @@ namespace opt { m_enable_sat = _p.enable_sat(); m_enable_sls = _p.enable_sls(); m_maxsat_engine = _p.maxsat_engine(); + m_pp_neat = _p.pp_neat(); } typedef obj_hashtable func_decl_set; @@ -1095,9 +1098,11 @@ namespace opt { std::string context::to_string() const { smt2_pp_environment_dbg env(m); + ast_smt_pp ll_smt2_pp(m); free_func_visitor visitor(m); std::ostringstream out; #define PP(_e_) ast_smt2_pp(out, _e_, env); +#define PPE(_e_) if (m_pp_neat) ast_smt2_pp(out, _e_, env); else ll_smt2_pp.display_expr_smt2(out, _e_); for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) { visitor.collect(m_scoped_state.m_hard[i]); } @@ -1132,7 +1137,7 @@ namespace opt { } for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) { out << "(assert "; - PP(m_scoped_state.m_hard[i]); + PPE(m_scoped_state.m_hard[i]); out << ")\n"; } for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) { diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index bbecb4996..a22c18373 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -127,6 +127,7 @@ namespace opt { tactic_ref m_simplify; bool m_enable_sat; bool m_enable_sls; + bool m_pp_neat; symbol m_maxsat_engine; symbol m_logic; public: diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index fd291336c..9d20dcb33 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -10,6 +10,7 @@ def_module_params('opt', ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), ('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), + ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'), ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'), ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'), diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index bfe1a3bb1..74f2e09fa 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -814,7 +814,7 @@ namespace smt { */ bool_var context::mk_bool_var(expr * n) { SASSERT(!b_internalized(n)); - SASSERT(!m_manager.is_not(n)); + //SASSERT(!m_manager.is_not(n)); unsigned id = n->get_id(); bool_var v = m_b_internalized_stack.size(); #ifndef _EXTERNAL_RELEASE diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index a392f8959..092db9f1a 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -411,6 +411,15 @@ namespace smt { return; } } +#if 0 + switch (m_params.m_arith_mode) { + case AS_DIFF_LOGIC: + case AS_DENSE_DIFF_LOGIC: + case AS_UTVPI: + setup_arith(); + return; + } +#endif m_params.m_arith_eq_bounds = true; m_params.m_phase_selection = PS_ALWAYS_FALSE; m_params.m_restart_strategy = RS_GEOMETRIC; @@ -420,7 +429,7 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); } // else if (st.m_arith_k_sum < rational(INT_MAX / 8)) - // m_context.register_plugin(alloc(smt::theory_si_arith, m_manager, m_params)); + // m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params)); else m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); } @@ -703,6 +712,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; if (m_params.m_arith_fixnum) { if (m_params.m_arith_int_only) m_context.register_plugin(alloc(smt::theory_fidl, m_manager, m_params)); @@ -717,6 +727,7 @@ namespace smt { } break; case AS_DENSE_DIFF_LOGIC: + m_params.m_arith_expand_eqs = true; if (m_params.m_arith_fixnum) { if (m_params.m_arith_int_only) m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params)); @@ -731,6 +742,7 @@ namespace smt { } break; case AS_UTVPI: + m_params.m_arith_expand_eqs = true; if (m_params.m_arith_int_only) m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager)); else diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 638d3c6b0..1c38ca343 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -578,10 +578,15 @@ namespace smt { void flush_bound_axioms(); typename atoms::iterator next_sup(atom* a1, atom_kind kind, typename atoms::iterator it, - typename atoms::iterator end); + typename atoms::iterator end, + bool& found_compatible); typename atoms::iterator next_inf(atom* a1, atom_kind kind, typename atoms::iterator it, - typename atoms::iterator end); + typename atoms::iterator end, + bool& found_compatible); + typename atoms::iterator first(atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end); struct compare_atoms { bool operator()(atom* a1, atom* a2) const { return a1->get_k() < a2->get_k(); } }; diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 3f6597a37..f5f446095 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -810,6 +810,8 @@ namespace smt { template void theory_arith::mk_bound_axioms(atom * a1) { + theory_var v = a1->get_var(); + atoms & occs = m_var_occs[v]; if (!get_context().is_searching()) { // // NB. We make an assumption that user push calls propagation @@ -819,11 +821,9 @@ namespace smt { m_new_atoms.push_back(a1); return; } - theory_var v = a1->get_var(); inf_numeral const & k1(a1->get_k()); atom_kind kind1 = a1->get_atom_kind(); TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";); - atoms & occs = m_var_occs[v]; typename atoms::iterator it = occs.begin(); typename atoms::iterator end = occs.end(); @@ -874,6 +874,9 @@ namespace smt { parameter coeffs[3] = { parameter(symbol("farkas")), parameter(rational(1)), parameter(rational(1)) }; + //std::cout << "v" << v << " " << ((kind1==A_LOWER)?"<= ":">= ") << k1 << "\t "; + //std::cout << "v" << v << " " << ((kind2==A_LOWER)?"<= ":">= ") << k2 << "\n"; + if (kind1 == A_LOWER) { if (kind2 == A_LOWER) { if (k2 <= k1) { @@ -944,39 +947,74 @@ namespace smt { std::sort(atoms.begin(), atoms.end(), compare_atoms()); std::sort(occs.begin(), occs.end(), compare_atoms()); - typename atoms::iterator begin = occs.begin(); + typename atoms::iterator begin1 = occs.begin(); + typename atoms::iterator begin2 = occs.begin(); typename atoms::iterator end = occs.end(); - typename atoms::iterator lo_inf = begin, lo_sup = begin; - typename atoms::iterator hi_inf = begin, hi_sup = begin; + begin1 = first(A_LOWER, begin1, end); + begin2 = first(A_UPPER, begin2, end); + typename atoms::iterator lo_inf = begin1, lo_sup = begin1; + typename atoms::iterator hi_inf = begin2, hi_sup = begin2; + typename atoms::iterator lo_inf1 = begin1, lo_sup1 = begin1; + typename atoms::iterator hi_inf1 = begin2, hi_sup1 = begin2; + bool flo_inf, fhi_inf, flo_sup, fhi_sup; + //std::cout << atoms.size() << "\n"; + ptr_addr_hashtable visited; for (unsigned i = 0; i < atoms.size(); ++i) { atom* a1 = atoms[i]; - lo_inf = next_inf(a1, A_LOWER, lo_inf, end); - hi_inf = next_inf(a1, A_UPPER, hi_inf, end); - lo_sup = next_sup(a1, A_LOWER, lo_sup, end); - hi_sup = next_sup(a1, A_UPPER, hi_sup, end); - if (lo_inf != end) mk_bound_axiom(a1, *lo_inf); - if (lo_sup != end) mk_bound_axiom(a1, *lo_sup); - if (hi_inf != end) mk_bound_axiom(a1, *hi_inf); - if (hi_sup != end) mk_bound_axiom(a1, *hi_sup); + lo_inf1 = next_inf(a1, A_LOWER, lo_inf, end, flo_inf); + hi_inf1 = next_inf(a1, A_UPPER, hi_inf, end, fhi_inf); + lo_sup1 = next_sup(a1, A_LOWER, lo_sup, end, flo_sup); + hi_sup1 = next_sup(a1, A_UPPER, hi_sup, end, fhi_sup); + //std::cout << "v" << a1->get_var() << ((a1->get_atom_kind()==A_LOWER)?" <= ":" >= ") << a1->get_k() << "\n"; + //std::cout << (lo_inf1 != end) << " " << (lo_sup1 != end) << " " << (hi_inf1 != end) << " " << (hi_sup1 != end) << "\n"; + if (lo_inf1 != end) lo_inf = lo_inf1; + if (lo_sup1 != end) lo_sup = lo_sup1; + if (hi_inf1 != end) hi_inf = hi_inf1; + if (hi_sup1 != end) hi_sup = hi_sup1; + if (!flo_inf) lo_inf = end; + if (!fhi_inf) hi_inf = end; + if (!flo_sup) lo_sup = end; + if (!fhi_sup) hi_sup = end; + visited.insert(a1); + if (lo_inf1 != end && lo_inf != end && !visited.contains(*lo_inf)) mk_bound_axiom(a1, *lo_inf); + if (lo_sup1 != end && lo_sup != end && !visited.contains(*lo_sup)) mk_bound_axiom(a1, *lo_sup); + if (hi_inf1 != end && hi_inf != end && !visited.contains(*hi_inf)) mk_bound_axiom(a1, *hi_inf); + if (hi_sup1 != end && hi_sup != end && !visited.contains(*hi_sup)) mk_bound_axiom(a1, *hi_sup); } } } + template + typename theory_arith::atoms::iterator + theory_arith::first( + atom_kind kind, + typename atoms::iterator it, + typename atoms::iterator end) { + for (; it != end; ++it) { + atom* a = *it; + if (a->get_atom_kind() == kind) return it; + } + return end; + } + template typename theory_arith::atoms::iterator theory_arith::next_inf( atom* a1, atom_kind kind, typename atoms::iterator it, - typename atoms::iterator end) { + typename atoms::iterator end, + bool& found_compatible) { inf_numeral const & k1(a1->get_k()); typename atoms::iterator result = end; + found_compatible = false; for (; it != end; ++it) { atom * a2 = *it; if (a1 == a2) continue; if (a2->get_atom_kind() != kind) continue; inf_numeral const & k2(a2->get_k()); + found_compatible = true; if (k2 <= k1) { result = it; } @@ -993,14 +1031,17 @@ namespace smt { atom* a1, atom_kind kind, typename atoms::iterator it, - typename atoms::iterator end) { + typename atoms::iterator end, + bool& found_compatible) { inf_numeral const & k1(a1->get_k()); + found_compatible = false; for (; it != end; ++it) { atom * a2 = *it; if (a1 == a2) continue; if (a2->get_atom_kind() != kind) continue; inf_numeral const & k2(a2->get_k()); - if (k2 > k1) { + found_compatible = true; + if (k1 < k2) { return it; } } diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 7189ee219..85f7f948a 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -722,6 +722,7 @@ theory_var theory_diff_logic::mk_term(app* n) { app* a, *offset; theory_var source, target; enode* e; + context& ctx = get_context(); TRACE("arith", tout << mk_pp(n, get_manager()) << "\n";); @@ -732,6 +733,13 @@ theory_var theory_diff_logic::mk_term(app* n) { else if (is_offset(n, a, offset, r)) { // n = a + k source = mk_var(a); + for (unsigned i = 0; i < n->get_num_args(); ++i) { + expr* arg = n->get_arg(i); + std::cout << "internalize: " << mk_pp(arg, get_manager()) << " " << ctx.e_internalized(arg) << "\n"; + if (!ctx.e_internalized(arg)) { + ctx.internalize(arg, false); + } + } e = get_context().mk_enode(n, false, false, true); target = mk_var(e); numeral k(r); @@ -779,6 +787,7 @@ theory_var theory_diff_logic::mk_num(app* n, rational const& r) { } else { theory_var zero = get_zero(); + SASSERT(n->get_num_args() == 0); e = ctx.mk_enode(n, false, false, true); v = mk_var(e); // internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.