diff --git a/src/muz/rel/product_set.h b/src/muz/rel/product_set.h index 17f888ca4..ebfe339fe 100644 --- a/src/muz/rel/product_set.h +++ b/src/muz/rel/product_set.h @@ -122,10 +122,9 @@ namespace datalog { UNREACHABLE(); return t; } - - }; + typedef ptr_hashtable product_sets; class product_set_relation : public relation_base { @@ -215,6 +214,72 @@ namespace datalog { ptr_vector& mutators); }; + class product_set_factory; + + + class product_set2 { + friend class product_set_factory; + unsigned char m_data[0]; + public: + enum initial_t { + EMPTY_t, + FULL_t + }; + product_set2(product_set_factory& fac, initial_t init); + ~product_set2(); + unsigned get_hash(product_set_factory& fac) const; + bool equals(product_set_factory& fac, product_set2 const& other) const; + void add_fact(product_set_factory& fac, const relation_fact & f); + bool contains_fact(product_set_factory& fac, const relation_fact & f) const; + relation_base * clone(product_set_factory& fac) const; + void reset(product_set_factory& fac); + void mk_join(product_set_factory& fac, product_set2 const& r1, product_set2 const& r2, + unsigned num_cols, unsigned const* cols1, unsigned const* cols2); + void mk_project(product_set_factory& fac, + product_set2 const& r, unsigned col_cnt, unsigned const* removed_cols); + void mk_rename(product_set_factory& fac, + product_set2 const& r, unsigned col_cnt, unsigned const* cycle); + void mk_union(product_set_factory& fac, + product_set2 const& src, product_set2* delta, bool is_widen); + unsigned find(product_set_factory& fac, unsigned i); + void merge(product_set_factory& fac, unsigned i, unsigned j); + void display(product_set_factory& fac, std::ostream& out) const; + }; + + + class product_set_factory { + friend class product_set_factory; + unsigned char m_data[0]; + public: + enum initial_t { + EMPTY_t, + FULL_t + }; + product_set_factory(product_set_plugin& p, relation_signature const& sig); + ~product_set_factory(); + product_set2* create(); + void retire(product_set2*); + + unsigned get_hash(product_set2& ps) const; + bool equals(product_set2 const& p1, product_set2 const& p2); + void add_fact(product_set2& p, const relation_fact & f); + bool contains_fact(product_set2& p, const relation_fact & f) const; + relation_base * clone(product_set2& p) const; + void reset(product_set2& p); + void mk_join(product_set2& p, product_set2 const& r1, product_set2 const& r2, + unsigned num_cols, unsigned const* cols1, unsigned const* cols2); + void mk_project(product_set2& p, + product_set2 const& r, unsigned col_cnt, unsigned const* removed_cols); + void mk_rename(product_set2& p, + product_set2 const& r, unsigned col_cnt, unsigned const* cycle); + void mk_union(product_set2& p, + product_set2 const& src, product_set2* delta, bool is_widen); + unsigned find(product_set2& p, unsigned i); + void merge(product_set2& p, unsigned i, unsigned j); + void display(product_set2& p, std::ostream& out) const; + }; + + }; #endif diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index be3470ad8..c0bb1cd8f 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -70,6 +70,7 @@ public: enum strategy_t { s_mus, s_mus_mss, + s_mus_mss2, s_mss }; private: @@ -83,6 +84,7 @@ private: strategy_t m_st; rational m_max_upper; bool m_hill_climb; + bool m_all_cores; public: maxres(context& c, @@ -94,7 +96,8 @@ public: m_mss(m_s, m), m_trail(m), m_st(st), - m_hill_climb(true) + m_hill_climb(true), + m_all_cores(false) { } @@ -150,21 +153,9 @@ public: return l_undef; } switch (is_sat) { - case l_true: { - s().get_model(m_model); - expr_ref tmp(m); - DEBUG_CODE( - for (unsigned i = 0; i < m_asms.size(); ++i) { - VERIFY(m_model->eval(m_asms[i].get(), tmp)); - SASSERT(m.is_true(tmp)); - }); - for (unsigned i = 0; i < m_soft.size(); ++i) { - VERIFY(m_model->eval(m_soft[i].get(), tmp)); - m_assignment[i] = m.is_true(tmp); - } - m_upper = m_lower; + case l_true: + found_optimum(); return l_true; - } case l_false: is_sat = process_unsat(); if (is_sat != l_true) return is_sat; @@ -267,12 +258,104 @@ public: return l_true; } + /** + Plan: + - Get maximal set of disjoint cores. + - Update the lower bound using the cores. + - As a side-effect find a satisfying assignment that has maximal weight. + (during core minimization several queries are bound to be SAT, + those can be used to boot-strap the MCS search). + - Use the best satisfying assignment from the MUS search to find an MCS of least weight. + - Update the upper bound using the MCS. + - Update the soft constraints using first the cores. + - Then update the resulting soft constraints using the evaluation of the MCS/MSS + - Add a cardinality constraint to force new satisfying assignments to improve + the new upper bound. + - In every iteration, the lower bound is improved using the cores. + - In every iteration, the upper bound is improved using the MCS. + - Optionally: add a cardinality constraint to prune the upper bound. + + What are the corner cases: + - suppose that cost of cores adds up to current upper bound. + -> it means that each core is a unit (?) + + */ + lbool mus_mss2_solver() { + init(); + init_local(); + sls(); + m_all_cores = true; + NOT_IMPLEMENTED_YET(); + vector > cores; + return l_undef; + lbool is_sat = l_true; + while (m_lower < m_upper && is_sat == l_true) { + TRACE("opt", + display_vec(tout, m_asms.size(), m_asms.c_ptr()); + s().display(tout); + tout << "\n"; + display(tout); + ); + lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); + if (m_cancel) { + return l_undef; + } + switch (is_sat) { + case l_true: + found_optimum(); + return l_true; + case l_false: + is_sat = process_unsat(cores); + break; + default: + break; + } + if (is_sat == l_undef) { + return l_undef; + } + if (cores.empty()) { + SASSERT(is_sat == l_false); + break; + } + SASSERT(is_sat == l_true); + // there is some best model, + // extend it to a maximal assignment + // extracting the mss and mcs. + set_mus(false); + ptr_vector mss, mcs; + is_sat = m_mss(cores, mss, mcs); + set_mus(true); + if (is_sat != l_true) return is_sat; + // + } + m_lower = m_upper; + return l_true; + } + + void found_optimum() { + s().get_model(m_model); + expr_ref tmp(m); + DEBUG_CODE( + for (unsigned i = 0; i < m_asms.size(); ++i) { + VERIFY(m_model->eval(m_asms[i].get(), tmp)); + SASSERT(m.is_true(tmp)); + }); + for (unsigned i = 0; i < m_soft.size(); ++i) { + VERIFY(m_model->eval(m_soft[i].get(), tmp)); + m_assignment[i] = m.is_true(tmp); + } + m_upper = m_lower; + } + + lbool operator()() { switch(m_st) { case s_mus: return mus_solver(); case s_mus_mss: return mus_mss_solver(); + case s_mus_mss2: + return mus_mss2_solver(); case s_mss: return mss_solver(); } @@ -293,8 +376,7 @@ public: break; } cores.push_back(core); - // TBD: ad hoc to avoid searching for large cores.. - if (core.size() >= 3) { + if (!m_all_cores && core.size() >= 3) { break; } remove_soft(core, asms); @@ -361,7 +443,7 @@ public: return index; } - lbool process_sat(ptr_vector& corr_set) { + lbool process_sat(ptr_vector const& corr_set) { expr_ref fml(m), tmp(m); TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr());); if (corr_set.empty()) { @@ -377,6 +459,10 @@ public: lbool process_unsat() { vector > cores; + return process_unsat(cores); + } + + lbool process_unsat(vector >& cores) { lbool is_sat = get_cores(cores); if (is_sat != l_true) { return is_sat; @@ -390,7 +476,7 @@ public: return is_sat; } - lbool process_unsat(ptr_vector& core) { + lbool process_unsat(ptr_vector const& core) { expr_ref fml(m); remove_core(core); rational w = split_core(core); @@ -404,7 +490,7 @@ public: } lbool minimize_core(ptr_vector& core) { - if (m_c.sat_enabled()) { + if (m_c.sat_enabled() || core.empty()) { return l_true; } m_mus.reset(); @@ -473,7 +559,7 @@ public: } } - void max_resolve(ptr_vector& core, rational const& w) { + void max_resolve(ptr_vector const& core, rational const& w) { SASSERT(!core.empty()); expr_ref fml(m), asum(m); app_ref cls(m), d(m), dd(m); @@ -515,7 +601,7 @@ public: } // cs is a correction set (a complement of a (maximal) satisfying assignment). - void cs_max_resolve(ptr_vector& cs, rational const& w) { + void cs_max_resolve(ptr_vector const& cs, rational const& w) { TRACE("opt", display_vec(tout << "correction set: ", cs.size(), cs.c_ptr());); SASSERT(!cs.empty()); expr_ref fml(m), asum(m); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 9fe704942..8c9148e17 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -41,7 +41,7 @@ namespace opt { m_c(c), m_cancel(false), m_soft(m), m_assertions(m) { - m_s.get_model(m_model); + c.get_base_model(m_model); SASSERT(m_model); updt_params(c.params()); init_soft(ws, soft); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 327a636f7..59b0ee566 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -215,7 +215,7 @@ namespace opt { case 0: return is_sat; case 1: - return execute(m_objectives[0], true); + return execute(m_objectives[0], true, false); default: { opt_params optp(m_params); symbol pri = optp.priority(); @@ -232,6 +232,10 @@ namespace opt { } } + void context::get_base_model(model_ref& mdl) { + mdl = m_model; + } + void context::get_model(model_ref& mdl) { mdl = m_model; if (mdl) { @@ -242,27 +246,31 @@ namespace opt { } } - lbool context::execute_min_max(unsigned index, bool committed) { + lbool context::execute_min_max(unsigned index, bool committed, bool scoped) { + if (scoped) get_solver().push(); lbool result = m_optsmt.lex(index); - if (result == l_true && committed) m_optsmt.commit_assignment(index); if (result == l_true) m_optsmt.get_model(m_model); + if (scoped) get_solver().pop(1); + if (result == l_true && committed) m_optsmt.commit_assignment(index); return result; } - lbool context::execute_maxsat(symbol const& id, bool committed) { + lbool context::execute_maxsat(symbol const& id, bool committed, bool scoped) { model_ref tmp; maxsmt& ms = *m_maxsmts.find(id); + if (scoped) get_solver().push(); lbool result = ms(m_solver.get()); - if (result == l_true && committed) ms.commit_assignment(); if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model); + if (scoped) get_solver().pop(1); + if (result == l_true && committed) ms.commit_assignment(); return result; } - lbool context::execute(objective const& obj, bool committed) { + lbool context::execute(objective const& obj, bool committed, bool scoped) { switch(obj.m_type) { - case O_MAXIMIZE: return execute_min_max(obj.m_index, committed); - case O_MINIMIZE: return execute_min_max(obj.m_index, committed); - case O_MAXSMT: return execute_maxsat(obj.m_id, committed); + case O_MAXIMIZE: return execute_min_max(obj.m_index, committed, scoped); + case O_MINIMIZE: return execute_min_max(obj.m_index, committed, scoped); + case O_MAXSMT: return execute_maxsat(obj.m_id, committed, scoped); default: UNREACHABLE(); return l_undef; } } @@ -271,9 +279,7 @@ namespace opt { lbool r = l_true; for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) { bool is_last = i + 1 == m_objectives.size(); - if (!is_last) get_solver().push(); - r = execute(m_objectives[i], i + 1 < m_objectives.size()); - if (!is_last) get_solver().pop(1); + r = execute(m_objectives[i], i + 1 < m_objectives.size(), !is_last); if (r == l_true && !get_lower_as_num(i).is_finite()) { return r; } @@ -291,7 +297,7 @@ namespace opt { objective const& obj = m_objectives[i]; if (obj.m_type == O_MAXSMT) { solver::scoped_push _sp(get_solver()); - r = execute(obj, false); + r = execute(obj, false, false); } } return r; @@ -399,9 +405,6 @@ namespace opt { if (is_sat == l_true) { yield(); } - else { - m_solver->pop(1); - } return is_sat; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 5f3bd88cb..c2c9f46d8 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -179,14 +179,15 @@ namespace opt { void enable_sls(expr_ref_vector const& soft, weights_t& weights); void set_enable_sls(bool f) { m_enable_sls = f; } symbol const& maxsat_engine() const { return m_maxsat_engine; } + void get_base_model(model_ref& m); private: void validate_feasibility(maxsmt& ms); - lbool execute(objective const& obj, bool committed); - lbool execute_min_max(unsigned index, bool committed); - lbool execute_maxsat(symbol const& s, bool committed); + lbool execute(objective const& obj, bool committed, bool scoped); + lbool execute_min_max(unsigned index, bool committed, bool scoped); + lbool execute_maxsat(symbol const& s, bool committed, bool scoped); lbool execute_lex(); lbool execute_box(); lbool execute_pareto();