From f82f7f83b9f740c22931b122308741e89a465145 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 14 Mar 2014 14:42:01 -0700 Subject: [PATCH] adding optimization to dense difference logic Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 13 ++ src/smt/params/smt_params_helper.pyg | 1 + src/smt/params/theory_arith_params.cpp | 1 + src/smt/smt_context_pp.cpp | 12 +- src/smt/smt_setup.cpp | 5 +- src/smt/theory_dense_diff_logic.h | 22 ++- src/smt/theory_dense_diff_logic_def.h | 208 +++++++++++++++++++++++++ 7 files changed, 253 insertions(+), 9 deletions(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index bf5fe0765..29cef424d 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -23,6 +23,7 @@ Notes: #include "smt_context.h" #include "theory_arith.h" #include "theory_diff_logic.h" +#include "theory_dense_diff_logic.h" #include "theory_pb.h" #include "ast_pp.h" #include "ast_smt_pp.h" @@ -97,6 +98,18 @@ namespace opt { else if (typeid(smt::theory_idl&) == typeid(*arith_theory)) { return dynamic_cast(*arith_theory); } + else if (typeid(smt::theory_dense_mi&) == typeid(*arith_theory)) { + return dynamic_cast(*arith_theory); + } + else if (typeid(smt::theory_dense_i&) == typeid(*arith_theory)) { + return dynamic_cast(*arith_theory); + } + else if (typeid(smt::theory_dense_smi&) == typeid(*arith_theory)) { + return dynamic_cast(*arith_theory); + } + else if (typeid(smt::theory_dense_si&) == typeid(*arith_theory)) { + return dynamic_cast(*arith_theory); + } else { UNREACHABLE(); return dynamic_cast(*arith_theory); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index cf9b8f57e..96ee7f5fc 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -43,6 +43,7 @@ def_module_params(module_name='smt', ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'), ('arith.ignore_int', BOOL, False, 'treat integer variables as real'), + ('arith.dump_lemmas', BOOL, False, 'dump arithmetic theory lemmas to files'), ('pb.conflict_frequency', UINT, 0, 'conflict frequency for Pseudo-Boolean theory'), ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), ('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean'), diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index 7281a5daa..370b296d1 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -33,6 +33,7 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_int_eq_branching = p.arith_int_eq_branch(); m_arith_ignore_int = p.arith_ignore_int(); m_arith_bound_prop = static_cast(p.arith_propagation_mode()); + m_arith_dump_lemmas = p.arith_dump_lemmas(); } diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 9ce684440..305e84518 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -427,7 +427,7 @@ namespace smt { } expr_ref n(m_manager); literal2expr(~consequent, n); - pp.display(out, n); + pp.display_smt2(out, n); } static unsigned g_lemma_id = 0; @@ -437,9 +437,9 @@ namespace smt { void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, const char * logic) const { char buffer[BUFFER_SZ]; #ifdef _WINDOWS - sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt", g_lemma_id); + sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt2", g_lemma_id); #else - sprintf(buffer, "lemma_%d.smt", g_lemma_id); + sprintf(buffer, "lemma_%d.smt2", g_lemma_id); #endif std::ofstream out(buffer); display_lemma_as_smt_problem(out, num_antecedents, antecedents, consequent, logic); @@ -468,7 +468,7 @@ namespace smt { } expr_ref n(m_manager); literal2expr(~consequent, n); - pp.display(out, n); + pp.display_smt2(out, n); } void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, @@ -476,9 +476,9 @@ namespace smt { literal consequent, const char * logic) const { char buffer[BUFFER_SZ]; #ifdef _WINDOWS - sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt", g_lemma_id); + sprintf_s(buffer, BUFFER_SZ, "lemma_%d.smt2", g_lemma_id); #else - sprintf(buffer, "lemma_%d.smt", g_lemma_id); + sprintf(buffer, "lemma_%d.smt2", g_lemma_id); #endif std::ofstream out(buffer); display_lemma_as_smt_problem(out, num_antecedents, antecedents, num_eq_antecedents, eq_antecedents, consequent, logic); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 02ac07cc2..3508d3d84 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -352,8 +352,9 @@ namespace smt { else if (!m_params.m_arith_auto_config_simplex && is_dense(st)) { TRACE("setup", tout << "using dense diff logic...\n";); m_params.m_phase_selection = PS_CACHING_CONSERVATIVE; - //m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params)); -#if 1 +#if 0 + m_context.register_plugin(alloc(smt::theory_idl, m_manager, m_params)); +#else if (st.m_arith_k_sum < rational(INT_MAX / 8)) m_context.register_plugin(alloc(smt::theory_dense_si, m_manager, m_params)); else diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h index db29dc988..48755d07f 100644 --- a/src/smt/theory_dense_diff_logic.h +++ b/src/smt/theory_dense_diff_logic.h @@ -25,6 +25,8 @@ TODO: eager equality propagation #include"theory_arith_params.h" #include"arith_decl_plugin.h" #include"arith_eq_adapter.h" +#include"theory_opt.h" + namespace smt { @@ -41,7 +43,7 @@ namespace smt { }; template - class theory_dense_diff_logic : public theory, private Ext { + class theory_dense_diff_logic : public theory, public theory_opt, private Ext { public: theory_dense_diff_logic_statistics m_stats; @@ -127,6 +129,12 @@ namespace smt { svector m_scopes; bool m_non_diff_logic_exprs; + // For optimization purpose + typedef vector > objective_term; + vector m_objectives; + vector m_objective_consts; + vector m_objective_assignments; + struct f_target { theory_var m_target; numeral m_new_distance; @@ -189,6 +197,7 @@ namespace smt { void del_atoms(unsigned old_size); void del_vars(unsigned old_num_vars); void init_model(); + bool internalize_objective(expr * n, rational const& m, rational& r, objective_term & objective); #ifdef Z3DEBUG bool check_vector_sizes() const; bool check_matrix() const; @@ -251,6 +260,17 @@ namespace smt { virtual void init_model(model_generator & m); virtual model_value_proc * mk_value(enode * n, model_generator & mg); + // ----------------------------------- + // + // Optimization + // + // ----------------------------------- + + virtual inf_eps_rational maximize(theory_var v, expr_ref& blocker); + virtual theory_var add_objective(app* term); + virtual expr_ref mk_gt(theory_var v, inf_rational const& val); + virtual expr* mk_ge(theory_var v, inf_rational const& val) { return 0; } + // ----------------------------------- // // Main diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 1febe4216..3c0cb7cb6 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -23,6 +23,8 @@ Revision History: #include"theory_dense_diff_logic.h" #include"ast_pp.h" #include"smt_model_generator.h" +#include"simplex.h" +#include"simplex_def.h" namespace smt { @@ -824,6 +826,212 @@ namespace smt { return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v))); } + template + bool theory_dense_diff_logic::internalize_objective(expr * n, rational const& m, rational& q, objective_term & objective) { + + // Compile term into objective_term format + rational r; + expr* x, *y; + if (m_autil.is_numeral(n, r)) { + q += r; + } + else if (m_autil.is_add(n)) { + for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) { + if (!internalize_objective(to_app(n)->get_arg(i), m, q, objective)) { + return false; + } + } + } + else if (m_autil.is_mul(n, x, y) && m_autil.is_numeral(x, r)) { + return internalize_objective(y, m*r, q, objective); + } + else if (m_autil.is_mul(n, y, x) && m_autil.is_numeral(x, r)) { + return internalize_objective(y, m*r, q, objective); + } + else if (!is_app(n)) { + return false; + } + else if (to_app(n)->get_family_id() == m_autil.get_family_id()) { + return false; + } + else { + enode * e = get_context().mk_enode(to_app(n), false, false, true); + theory_var v = mk_var(e); + objective.push_back(std::make_pair(v, m)); + } + return true; + } + + template + inf_eps_rational theory_dense_diff_logic::maximize(theory_var v, expr_ref& blocker) { + return inf_eps(); + typedef simplex::simplex Simplex; + Simplex S; + ast_manager& m = get_manager(); + objective_term const& objective = m_objectives[v]; + + IF_VERBOSE(1, + for (unsigned i = 0; i < objective.size(); ++i) { + verbose_stream() << "Coefficient " << objective[i].second + << " of theory_var " << objective[i].first << "\n"; + } + verbose_stream() << "Free coefficient " << m_objective_consts[v] << "\n";); + + unsigned num_nodes = get_num_vars(); + unsigned num_edges = m_edges.size(); + S.ensure_var(num_nodes + num_edges + m_objectives.size()); + for (unsigned i = 0; i < num_nodes; ++i) { + numeral const& a = m_assignment[i]; + rational fin = a.get_rational().to_rational(); + rational inf = a.get_infinitesimal().to_rational(); + mpq_inf q(fin.to_mpq(), inf.to_mpq()); + S.set_value(i, q); + } + for (unsigned i = 0; i < num_nodes; ++i) { + enode * n = get_enode(i); + if (m_autil.is_zero(n->get_owner())) { + S.set_lower(v, mpq_inf(mpq(0), mpq(0))); + S.set_upper(v, mpq_inf(mpq(0), mpq(0))); + break; + } + } + svector vars; + unsynch_mpq_manager mgr; + scoped_mpq_vector coeffs(mgr); + coeffs.push_back(mpq(1)); + coeffs.push_back(mpq(-1)); + coeffs.push_back(mpq(-1)); + vars.resize(3); + for (unsigned i = 0; i < num_edges; ++i) { + edge const& e = m_edges[i]; + if (e.m_source == null_theory_var || e.m_target == null_theory_var) { + continue; + } + unsigned base_var = num_nodes + i; + vars[0] = e.m_target; + vars[1] = e.m_source; + vars[2] = base_var; + S.add_row(base_var, 3, vars.c_ptr(), coeffs.c_ptr()); + // t - s <= w + // t - s - b = 0, b >= w + numeral const& w = e.m_offset; + rational fin = w.get_rational().to_rational(); + rational inf = w.get_infinitesimal().to_rational(); + mpq_inf q(fin.to_mpq(),inf.to_mpq()); + S.set_upper(base_var, q); + } + unsigned w = num_nodes + num_edges + v; + + // add objective function as row. + coeffs.reset(); + vars.reset(); + for (unsigned i = 0; i < objective.size(); ++i) { + coeffs.push_back(objective[i].second.to_mpq()); + vars.push_back(objective[i].first); + } + coeffs.push_back(mpq(1)); + vars.push_back(w); + Simplex::row row = S.add_row(w, vars.size(), vars.c_ptr(), coeffs.c_ptr()); + + TRACE("opt", S.display(tout); display(tout);); + + // optimize + lbool is_sat = S.make_feasible(); + if (is_sat == l_undef) { + blocker = m.mk_false(); + return inf_eps::infinity(); + } + TRACE("opt", S.display(tout); ); + SASSERT(is_sat != l_false); + lbool is_fin = S.minimize(w); + + switch (is_fin) { + case l_true: { + simplex::mpq_ext::eps_numeral const& val = S.get_value(w); + inf_rational r(-rational(val.first), -rational(val.second)); + TRACE("opt", tout << r << " " << "\n"; + S.display_row(tout, row, true);); + Simplex::row_iterator it = S.row_begin(row), end = S.row_end(row); + expr_ref_vector& core = m_objective_assignments[v]; + expr_ref tmp(m); + core.reset(); + for (; it != end; ++it) { + unsigned v = it->m_var; + if (num_nodes <= v && v < num_nodes + num_edges) { + unsigned edge_id = v - num_nodes; + literal lit = m_edges[edge_id].m_justification; + get_context().literal2expr(lit, tmp); + core.push_back(tmp); + } + } + blocker = mk_gt(v, r); + return inf_eps(rational(0), r); + } + default: + TRACE("opt", tout << "unbounded\n"; ); + blocker = m.mk_false(); + return inf_eps::infinity(); + } + } + + template + theory_var theory_dense_diff_logic::add_objective(app* term) { + objective_term objective; + theory_var result = m_objectives.size(); + rational q(1), r(0); + expr_ref_vector vr(get_manager()); + if (internalize_objective(term, q, r, objective)) { + m_objectives.push_back(objective); + m_objective_consts.push_back(r); + m_objective_assignments.push_back(vr); + } + else { + result = null_theory_var; + } + return result; + } + + template + expr_ref theory_dense_diff_logic::mk_gt(theory_var v, inf_rational const& val) { + ast_manager& m = get_manager(); + objective_term const& t = m_objectives[v]; + expr_ref e(m), f(m), f2(m); + if (t.size() == 1 && t[0].second.is_one()) { + f = get_enode(t[0].first)->get_owner(); + } + else if (t.size() == 1 && t[0].second.is_minus_one()) { + f = m_autil.mk_uminus(get_enode(t[0].first)->get_owner()); + } + else if (t.size() == 2 && t[0].second.is_one() && t[1].second.is_minus_one()) { + f = get_enode(t[0].first)->get_owner(); + f2 = get_enode(t[1].first)->get_owner(); + f = m_autil.mk_sub(f, f2); + } + else if (t.size() == 2 && t[1].second.is_one() && t[0].second.is_minus_one()) { + f = get_enode(t[1].first)->get_owner(); + f2 = get_enode(t[0].first)->get_owner(); + f = m_autil.mk_sub(f, f2); + } + else { + // + expr_ref_vector const& core = m_objective_assignments[v]; + f = m.mk_not(m.mk_and(core.size(), core.c_ptr())); + TRACE("arith", tout << "block: " << f << "\n";); + return f; + } + + inf_rational new_val = val - inf_rational(m_objective_consts[v]); + e = m_autil.mk_numeral(new_val.get_rational(), m.get_sort(f)); + + if (new_val.get_infinitesimal().is_neg()) { + f = m_autil.mk_ge(f, e); + } + else { + f = m_autil.mk_gt(f, e); + } + return f; + } + }; #endif /* _THEORY_DENSE_DIFF_LOGIC_DEF_H_ */