From 99ff13b651e428b111cf29d2bee9bdddccdcc915 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Sep 2014 11:39:25 -0700 Subject: [PATCH] opt + udoc Signed-off-by: Nikolaj Bjorner --- src/muz/ddnf/udoc_relation.cpp | 82 ++++++++++++++++++++++++++-------- src/muz/ddnf/udoc_relation.h | 8 ++-- src/opt/maxres.cpp | 50 ++++++++++++--------- 3 files changed, 96 insertions(+), 44 deletions(-) diff --git a/src/muz/ddnf/udoc_relation.cpp b/src/muz/ddnf/udoc_relation.cpp index 393b85d54..0490bd034 100644 --- a/src/muz/ddnf/udoc_relation.cpp +++ b/src/muz/ddnf/udoc_relation.cpp @@ -333,12 +333,10 @@ namespace datalog { doc_manager& dm = r.get_dm(); unsigned num_bits = dm.num_tbits(); m_size = r.column_num_bits(identical_cols[0]); - m_empty_bv.resize(r.get_num_bits(), false); - + m_empty_bv.resize(r.get_num_bits(), false); for (unsigned i = 0; i < col_cnt; ++i) { m_cols[i] = r.column_idx(identical_cols[i]); - } - + } for (unsigned i = 0, e = m_empty_bv.size(); i < e; ++i) { m_equalities.mk_var(); } @@ -354,11 +352,8 @@ namespace datalog { } }; relation_mutator_fn * udoc_plugin::mk_filter_identical_fn( - const relation_base & t, unsigned col_cnt, - const unsigned * identical_cols) { - if (!check_kind(t)) - return 0; - return alloc(filter_identical_fn, t, col_cnt, identical_cols); + const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) { + return check_kind(t)?alloc(filter_identical_fn, t, col_cnt, identical_cols):0; } class udoc_plugin::filter_equal_fn : public relation_mutator_fn { doc_manager& dm; @@ -434,7 +429,7 @@ namespace datalog { void udoc_relation::compile_guard(expr* g, udoc& d) const { NOT_IMPLEMENTED_YET(); } - void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) { + void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const { // datastructure to store equalities with columns that will be projected out union_find_default_ctx union_ctx; subset_ints equalities(union_ctx); @@ -443,9 +438,13 @@ namespace datalog { } apply_guard(g, result, equalities, discard_cols); } + void udoc_relation::apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c) const { + NOT_IMPLEMENTED_YET(); + } + void udoc_relation::apply_guard( expr* g, udoc& result, - subset_ints& equalities, bit_vector const& discard_cols) { + subset_ints& equalities, bit_vector const& discard_cols) const { ast_manager& m = get_plugin().get_ast_manager(); bv_util& bv = get_plugin().bv; expr* e1, *e2; @@ -489,6 +488,7 @@ namespace datalog { else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) { unsigned hi, lo; expr* e3; + NOT_IMPLEMENTED_YET(); // TBD: equalities and discard_cols? if (is_var(e1) && is_ground(e2)) { apply_eq(g, result, to_var(e1), bv.get_bv_size(e1)-1, 0, e2); @@ -506,6 +506,7 @@ namespace datalog { var* v1 = to_var(e1); var* v2 = to_var(e2); // TBD + NOT_IMPLEMENTED_YET(); } else { goto failure_case; @@ -551,14 +552,8 @@ namespace datalog { TRACE("dl", tout << "final size: " << t.get_size_estimate_rows() << '\n';); } }; - - - relation_mutator_fn * udoc_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) { - if (!check_kind(t)) - return 0; - TRACE("dl", tout << mk_pp(condition, get_ast_manager()) << '\n';); - return alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition); + return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):0; } class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn { @@ -588,4 +583,55 @@ namespace datalog { return alloc(negation_filter_fn, get(t), get(neg), joined_col_cnt, t_cols, negated_cols); } + class udoc_plugin::filter_proj_fn : public convenient_relation_project_fn { + doc_manager& dm; + expr_ref m_condition; + udoc m_udoc; + bit_vector m_col_list; // map: col idx -> bool (whether the column is to be removed) + public: + filter_proj_fn(const udoc_relation & t, ast_manager& m, app *condition, + unsigned col_cnt, const unsigned * removed_cols) : + convenient_relation_project_fn(t.get_signature(), col_cnt, removed_cols), + dm(t.get_dm()), + m_condition(m) { + t.expand_column_vector(m_removed_cols); + m_col_list.resize(t.get_num_bits(), false); + for (unsigned i = 0; i < m_removed_cols.size(); ++i) { + m_col_list.set(m_removed_cols[i]); + } + m_removed_cols.push_back(UINT_MAX); + expr_ref guard(m), rest(m); + t.extract_guard(condition, guard, m_condition); + t.compile_guard(guard, m_udoc); + if (m.is_true(m_condition)) { + m_condition = 0; + } + } + + virtual ~filter_proj_fn() { + m_udoc.reset(dm); + } + virtual relation_base* operator()(const relation_base & tb) { + udoc_relation const & t = get(tb); + udoc const& u1 = t.get_udoc(); + udoc u2; + // copy u1 -> u2; + NOT_IMPLEMENTED_YET(); + u2.intersect(dm, m_udoc); + if (m_condition && !u2.empty()) { + t.apply_guard(m_condition, u2, m_col_list); + } + udoc_relation* res = get(t.get_plugin().mk_empty(get_result_signature())); + NOT_IMPLEMENTED_YET(); + // u2.project(m_removed_cols, res->get_dm(), res->get_udoc()); + return res; + } + }; + relation_transformer_fn * udoc_plugin::mk_filter_interpreted_and_project_fn( + const relation_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols) { + return check_kind(t)?alloc(filter_proj_fn, get(t), get_ast_manager(), condition, removed_col_cnt, removed_cols):0; + } + + } diff --git a/src/muz/ddnf/udoc_relation.h b/src/muz/ddnf/udoc_relation.h index 197e16fb9..eaa653c83 100644 --- a/src/muz/ddnf/udoc_relation.h +++ b/src/muz/ddnf/udoc_relation.h @@ -64,9 +64,9 @@ namespace datalog { bool is_guard(expr* g) const; bool is_guard(unsigned n, expr* const *g) const; void compile_guard(expr* g, udoc& d) const; - void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols); - void apply_guard(expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols); - void apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c); + void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const; + void apply_guard(expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols) const; + void apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c) const; }; class udoc_plugin : public relation_plugin { @@ -120,8 +120,6 @@ namespace datalog { virtual relation_transformer_fn * mk_filter_interpreted_and_project_fn( const relation_base & t, app * condition, unsigned removed_col_cnt, const unsigned * removed_cols); - - // project join select }; }; diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index c2de70ad6..e032cb80e 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -163,7 +163,7 @@ public: tout << "\n"; display(tout); ); - lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); + lbool is_sat = check_sat_hill_climb(m_asms); if (m_cancel) { return l_undef; } @@ -276,7 +276,7 @@ public: tout << "\n"; display(tout); ); - lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr()); + lbool is_sat = check_sat_hill_climb(m_asms); if (m_cancel) { return l_undef; } @@ -339,6 +339,32 @@ public: return l_true; } + lbool check_sat_hill_climb(expr_ref_vector& asms1) { + expr_ref_vector asms(asms1); + lbool is_sat = l_true; + if (m_hill_climb) { + /** + Give preference to cores that have large minmal values. + */ + sort_assumptions(asms); + unsigned index = 0; + unsigned last_index = 0; + while (index < asms.size() && is_sat == l_true) { + while (asms.size() > 20*(index - last_index) && index < asms.size()) { + index = next_index(asms, index); + //std::cout << "weight: " << get_weight(asms[index-1].get()) << "\n"; + //break; + } + last_index = index; + is_sat = s().check_sat(index, asms.c_ptr()); + } + } + else { + is_sat = s().check_sat(asms.size(), asms.c_ptr()); + } + return is_sat; + } + void found_optimum() { s().get_model(m_model); DEBUG_CODE( @@ -392,25 +418,7 @@ public: TRACE("opt", display_vec(tout << "core: ", core.size(), core.c_ptr()); display_vec(tout << "assumptions: ", asms.size(), asms.c_ptr());); - - if (m_hill_climb) { - /** - Give preference to cores that have large minmal values. - */ - sort_assumptions(asms); - unsigned index = 0; - unsigned last_index = 0; - while (index < asms.size() && is_sat != l_false) { - while (asms.size() > 10*(index - last_index) && index < asms.size()) { - index = next_index(asms, index); - } - last_index = index; - is_sat = s().check_sat(index, asms.c_ptr()); - } - } - else { - is_sat = s().check_sat(asms.size(), asms.c_ptr()); - } + is_sat = check_sat_hill_climb(asms); } TRACE("opt", tout << "num cores: " << cores.size() << "\n";