diff --git a/src/muz_qe/dl_base.h b/src/muz_qe/dl_base.h index 491bb261d..200ce2d83 100644 --- a/src/muz_qe/dl_base.h +++ b/src/muz_qe/dl_base.h @@ -331,6 +331,10 @@ namespace datalog { virtual mutator_fn * mk_filter_interpreted_fn(const base_object & t, app * condition) { return 0; } + virtual transformer_fn * mk_filter_interpreted_and_project_fn(const base_object & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) + { return 0; } + virtual transformer_fn * mk_select_equal_and_project_fn(const base_object & t, const element & value, unsigned col) { return 0; } @@ -454,8 +458,8 @@ namespace datalog { class convenient_join_fn : public join_fn { signature m_result_sig; protected: - const unsigned_vector m_cols1; - const unsigned_vector m_cols2; + unsigned_vector m_cols1; + unsigned_vector m_cols2; convenient_join_fn(const signature & o1_sig, const signature & o2_sig, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) @@ -470,8 +474,8 @@ namespace datalog { class convenient_join_project_fn : public join_fn { signature m_result_sig; protected: - const unsigned_vector m_cols1; - const unsigned_vector m_cols2; + unsigned_vector m_cols1; + unsigned_vector m_cols2; //it is non-const because it needs to be modified in sparse_table version of the join_project operator unsigned_vector m_removed_cols; @@ -498,7 +502,7 @@ namespace datalog { class convenient_project_fn : public convenient_transformer_fn { protected: - const unsigned_vector m_removed_cols; + unsigned_vector m_removed_cols; convenient_project_fn(const signature & orig_sig, unsigned col_cnt, const unsigned * removed_cols) : m_removed_cols(col_cnt, removed_cols) { diff --git a/src/muz_qe/dl_check_table.cpp b/src/muz_qe/dl_check_table.cpp index 5081654b5..ea4003e5f 100644 --- a/src/muz_qe/dl_check_table.cpp +++ b/src/muz_qe/dl_check_table.cpp @@ -82,6 +82,34 @@ namespace datalog { return alloc(join_fn, *this, t1, t2, col_cnt, cols1, cols2); } + class check_table_plugin::join_project_fn : public table_join_fn { + scoped_ptr m_tocheck; + scoped_ptr m_checker; + public: + join_project_fn(check_table_plugin& p, const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, + unsigned removed_col_cnt, const unsigned * removed_cols) { + m_tocheck = p.get_manager().mk_join_project_fn(tocheck(t1), tocheck(t2), col_cnt, cols1, cols2, removed_col_cnt, removed_cols); + m_checker = p.get_manager().mk_join_project_fn(checker(t1), checker(t2), col_cnt, cols1, cols2, removed_col_cnt, removed_cols); + } + + virtual table_base* operator()(const table_base & t1, const table_base & t2) { + table_base* ttocheck = (*m_tocheck)(tocheck(t1), tocheck(t2)); + table_base* tchecker = (*m_checker)(checker(t1), checker(t2)); + check_table* result = alloc(check_table, get(t1).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker); + return result; + } + }; + + table_join_fn * check_table_plugin::mk_join_project_fn(const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, + const unsigned * removed_cols) { + if (!check_kind(t1) || !check_kind(t2)) { + return 0; + } + return alloc(join_project_fn, *this, t1, t2, col_cnt, cols1, cols2, removed_col_cnt, removed_cols); + } + class check_table_plugin::union_fn : public table_union_fn { scoped_ptr m_tocheck; scoped_ptr m_checker; @@ -120,7 +148,6 @@ namespace datalog { } table_base* operator()(table_base const& src) { - IF_VERBOSE(1, verbose_stream() << __FUNCTION__ << "\n";); table_base* tchecker = (*m_checker)(checker(src)); table_base* ttocheck = (*m_tocheck)(tocheck(src)); check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker); @@ -135,6 +162,31 @@ namespace datalog { return alloc(project_fn, *this, t, col_cnt, removed_cols); } + class check_table_plugin::select_equal_and_project_fn : public table_transformer_fn { + scoped_ptr m_checker; + scoped_ptr m_tocheck; + public: + select_equal_and_project_fn(check_table_plugin& p, const table_base & t, const table_element & value, unsigned col) { + m_checker = p.get_manager().mk_select_equal_and_project_fn(checker(t), value, col); + m_tocheck = p.get_manager().mk_select_equal_and_project_fn(tocheck(t), value, col); + } + + table_base* operator()(table_base const& src) { + table_base* tchecker = (*m_checker)(checker(src)); + table_base* ttocheck = (*m_tocheck)(tocheck(src)); + check_table* result = alloc(check_table, get(src).get_plugin(), tchecker->get_signature(), ttocheck, tchecker); + return result; + } + }; + + table_transformer_fn * check_table_plugin::mk_select_equal_and_project_fn(const table_base & t, + const table_element & value, unsigned col) { + if (!check_kind(t)) { + return 0; + } + return alloc(select_equal_and_project_fn, *this, t, value, col); + } + class check_table_plugin::rename_fn : public table_transformer_fn { scoped_ptr m_checker; scoped_ptr m_tocheck; @@ -233,6 +285,33 @@ namespace datalog { return 0; } + class check_table_plugin::filter_interpreted_and_project_fn : public table_transformer_fn { + scoped_ptr m_checker; + scoped_ptr m_tocheck; + public: + filter_interpreted_and_project_fn(check_table_plugin& p, const table_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols) + { + m_checker = p.get_manager().mk_filter_interpreted_and_project_fn(checker(t), condition, removed_col_cnt, removed_cols); + m_tocheck = p.get_manager().mk_filter_interpreted_and_project_fn(tocheck(t), condition, removed_col_cnt, removed_cols); + } + + table_base* operator()(table_base const& src) { + table_base* tchecker = (*m_checker)(checker(src)); + table_base* ttocheck = (*m_tocheck)(tocheck(src)); + check_table* result = alloc(check_table, get(src).get_plugin(), ttocheck->get_signature(), ttocheck, tchecker); + return result; + } + }; + + table_transformer_fn * check_table_plugin::mk_filter_interpreted_and_project_fn(const table_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) { + if (check_kind(t)) { + return alloc(filter_interpreted_and_project_fn, *this, t, condition, removed_col_cnt, removed_cols); + } + return 0; + } + class check_table_plugin::filter_by_negation_fn : public table_intersection_filter_fn { scoped_ptr m_checker; scoped_ptr m_tocheck; diff --git a/src/muz_qe/dl_check_table.h b/src/muz_qe/dl_check_table.h index 40a3d5207..e4f439590 100644 --- a/src/muz_qe/dl_check_table.h +++ b/src/muz_qe/dl_check_table.h @@ -35,13 +35,16 @@ namespace datalog { unsigned m_count; protected: class join_fn; + class join_project_fn; class union_fn; class transformer_fn; class rename_fn; class project_fn; + class select_equal_and_project_fn; class filter_equal_fn; class filter_identical_fn; class filter_interpreted_fn; + class filter_interpreted_and_project_fn; class filter_by_negation_fn; public: @@ -54,10 +57,15 @@ namespace datalog { virtual table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2, unsigned col_cnt, const unsigned * cols1, const unsigned * cols2); + virtual table_join_fn * mk_join_project_fn(const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, + const unsigned * removed_cols); virtual table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src, const table_base * delta); virtual table_transformer_fn * mk_project_fn(const table_base & t, unsigned col_cnt, const unsigned * removed_cols); + virtual table_transformer_fn * mk_select_equal_and_project_fn(const table_base & t, + const table_element & value, unsigned col); virtual table_transformer_fn * mk_rename_fn(const table_base & t, unsigned permutation_cycle_len, const unsigned * permutation_cycle); virtual table_mutator_fn * mk_filter_identical_fn(const table_base & t, unsigned col_cnt, @@ -65,6 +73,8 @@ namespace datalog { virtual table_mutator_fn * mk_filter_equal_fn(const table_base & t, const table_element & value, unsigned col); virtual table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition); + virtual table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols); virtual table_intersection_filter_fn * mk_filter_by_negation_fn( const table_base & t, const table_base & negated_obj, unsigned joined_col_cnt, diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 05a0d24b2..3f16d0dab 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -73,6 +73,18 @@ namespace datalog { vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result)); } + void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond, + const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) { + SASSERT(!removed_cols.empty()); + relation_signature res_sig; + relation_signature::from_project(m_reg_signatures[src], removed_cols.size(), + removed_cols.c_ptr(), res_sig); + result = get_fresh_register(res_sig); + + acc.push_back(instruction::mk_filter_interpreted_and_project(src, cond, + removed_cols.size(), removed_cols.c_ptr(), result)); + } + void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, reg_idx & result, instruction_block & acc) { relation_signature res_sig; @@ -619,6 +631,116 @@ namespace datalog { } // enforce interpreted tail predicates + unsigned ft_len = r->get_tail_size(); // full tail + ptr_vector tail; + for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { + tail.push_back(r->get_tail(tail_index)); + } + + if (!tail.empty()) { + app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.c_ptr()), m); + ptr_vector filter_vars; + get_free_vars(filter_cond, filter_vars); + + // create binding + expr_ref_vector binding(m); + binding.resize(filter_vars.size()+1); + + for (unsigned v = 0; v < filter_vars.size(); ++v) { + if (!filter_vars[v]) + continue; + + int2ints::entry * entry = var_indexes.find_core(v); + unsigned src_col; + if (entry) { + src_col = entry->get_data().m_value.back(); + } else { + // we have an unbound variable, so we add an unbound column for it + relation_sort unbound_sort = filter_vars[v]; + + reg_idx new_reg; + bool new_dealloc; + make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc); + if (dealloc) + make_dealloc_non_void(filtered_res, acc); + dealloc = new_dealloc; + filtered_res = new_reg; + + src_col = single_res_expr.size(); + single_res_expr.push_back(m.mk_var(v, unbound_sort)); + + entry = var_indexes.insert_if_not_there2(v, unsigned_vector()); + entry->get_data().m_value.push_back(src_col); + } + relation_sort var_sort = m_reg_signatures[filtered_res][src_col]; + binding[filter_vars.size()-v] = m.mk_var(src_col, var_sort); + } + + // check if there are any columns to remove + unsigned_vector remove_columns; + { + unsigned_vector var_idx_to_remove; + ptr_vector vars; + get_free_vars(r->get_head(), vars); + for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end(); + I != E; ++I) { + unsigned var_idx = I->m_key; + if (!vars.get(var_idx, 0)) { + unsigned_vector & cols = I->m_value; + for (unsigned i = 0; i < cols.size(); ++i) { + remove_columns.push_back(cols[i]); + } + var_idx_to_remove.push_back(var_idx); + } + } + + for (unsigned i = 0; i < var_idx_to_remove.size(); ++i) { + var_indexes.remove(var_idx_to_remove[i]); + } + + // update column idx for after projection state + if (!remove_columns.empty()) { + unsigned_vector offsets; + offsets.resize(single_res_expr.size(), 0); + + for (unsigned i = 0; i < remove_columns.size(); ++i) { + for (unsigned col = remove_columns[i]; col < offsets.size(); ++col) { + ++offsets[col]; + } + } + + for (int2ints::iterator I = var_indexes.begin(), E = var_indexes.end(); + I != E; ++I) { + unsigned_vector & cols = I->m_value; + for (unsigned i = 0; i < cols.size(); ++i) { + cols[i] -= offsets[cols[i]]; + } + } + } + } + + expr_ref renamed(m); + m_context.get_var_subst()(filter_cond, binding.size(), binding.c_ptr(), renamed); + app_ref app_renamed(to_app(renamed), m); + if (remove_columns.empty()) { + if (!dealloc) + make_clone(filtered_res, filtered_res, acc); + acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); + } else { + reg_idx new_reg; + std::sort(remove_columns.begin(), remove_columns.end()); + make_filter_interpreted_and_project(filtered_res, app_renamed, remove_columns, new_reg, acc); + if (dealloc) + make_dealloc_non_void(filtered_res, acc); + filtered_res = new_reg; + } + dealloc = true; + } + +#if 0 + // this version is potentially better for non-symbolic tables, + // since it constraints each unbound column at a time (reducing the + // size of intermediate results). unsigned ft_len=r->get_tail_size(); //full tail for(unsigned tail_index=ut_len; tail_indexget_tail(tail_index); @@ -686,6 +808,7 @@ namespace datalog { acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); dealloc = true; } +#endif { //put together the columns of head relation @@ -737,7 +860,7 @@ namespace datalog { make_dealloc_non_void(new_head_reg, acc); } - finish: +// finish: m_instruction_observer.finish_rule(); } diff --git a/src/muz_qe/dl_compiler.h b/src/muz_qe/dl_compiler.h index 78b4623de..e0f9af424 100644 --- a/src/muz_qe/dl_compiler.h +++ b/src/muz_qe/dl_compiler.h @@ -145,6 +145,8 @@ namespace datalog { instruction_block & acc); void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc); + void make_filter_interpreted_and_project(reg_idx src, app_ref & cond, + const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc); void make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, reg_idx & result, instruction_block & acc); /** diff --git a/src/muz_qe/dl_hassel_common.cpp b/src/muz_qe/dl_hassel_common.cpp new file mode 100755 index 000000000..6201868ca --- /dev/null +++ b/src/muz_qe/dl_hassel_common.cpp @@ -0,0 +1,434 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_common.cpp + +Abstract: + + + +Revision History: + +--*/ + +#include "dl_hassel_common.h" +#include "dl_context.h" + +#include + +namespace datalog { + + static void formula_to_dnf_aux(app *and, unsigned idx, std::set& conjexpr, std::set& toplevel, ast_manager& m) { + if (idx == and->get_num_args()) { + std::vector v(conjexpr.begin(), conjexpr.end()); + toplevel.insert(m.mk_and((unsigned)v.size(), &v[0])); + return; + } + + expr *e = and->get_arg(idx); + if (is_app(e) && to_app(e)->get_decl_kind() == OP_OR) { + app *or = to_app(e); + // quick subsumption test: if any of the elements of the OR is already ANDed, then we skip this OR + for (unsigned i = 0; i < or->get_num_args(); ++i) { + if (conjexpr.count(or->get_arg(i))) { + formula_to_dnf_aux(and, idx+1, conjexpr, toplevel, m); + return; + } + } + + for (unsigned i = 0; i < or->get_num_args(); ++i) { + std::set conjexpr2(conjexpr); + conjexpr2.insert(or->get_arg(i)); + formula_to_dnf_aux(and, idx+1, conjexpr2, toplevel, m); + } + } else { + conjexpr.insert(e); + formula_to_dnf_aux(and, idx+1, conjexpr, toplevel, m); + } + } + + expr_ref formula_to_dnf(expr_ref f) { + app *a = to_app(f); + SASSERT(a->get_decl_kind() == OP_AND); + std::set toplevel, conjexpr; + formula_to_dnf_aux(a, 0, conjexpr, toplevel, f.m()); + + if (toplevel.size() > 1) { + std::vector v(toplevel.begin(), toplevel.end()); + return expr_ref(f.m().mk_or((unsigned)v.size(), &v[0]), f.m()); + } else { + return expr_ref(*toplevel.begin(), f.m()); + } + } + + bool bit_vector::contains(const bit_vector & other) const { + unsigned n = num_words(); + if (n == 0) + return true; + + for (unsigned i = 0; i < n - 1; ++i) { + if ((m_data[i] & other.m_data[i]) != other.m_data[i]) + return false; + } + unsigned bit_rest = m_num_bits % 32; + unsigned mask = (1 << bit_rest) - 1; + if (mask == 0) mask = UINT_MAX; + unsigned other_data = other.m_data[n-1] & mask; + return (m_data[n-1] & other_data) == other_data; + } + + bool bit_vector::contains(const bit_vector & other, unsigned idx) const { + // TODO: optimize this to avoid copy + return slice(idx, other.size()).contains(other); + } + + bool bit_vector::contains_consecutive_zeros() const { + unsigned n = num_words(); + if (n == 0) + return false; + + for (unsigned i = 0; i < n - 1; ++i) { + if ((((m_data[i] << 1) | m_data[i]) & 0xAAAAAAAA) != 0xAAAAAAAA) + return true; + } + unsigned bit_rest = m_num_bits % 32; + unsigned mask = (1 << bit_rest) - 1; + if (mask == 0) mask = UINT_MAX; + mask &= 0xAAAAAAAA; + return ((((m_data[n-1] << 1) | m_data[n-1]) & mask) != mask); + } + + bit_vector bit_vector::slice(unsigned idx, unsigned length) const { + bit_vector Res(length); + // TODO: optimize w/ memcpy when possible + for (unsigned i = idx; i < idx + length; ++i) { + Res.push_back(get(i)); + } + SASSERT(Res.size() == length); + return Res; + } + + void bit_vector::append(const bit_vector & other) { + if (other.empty()) + return; + + if ((m_num_bits % 32) == 0) { + unsigned prev_num_bits = m_num_bits; + resize(m_num_bits + other.m_num_bits); + memcpy(&get_bit_word(prev_num_bits), other.m_data, other.num_words() * sizeof(unsigned)); + return; + } + + // TODO: optimize the other cases. + for (unsigned i = 0; i < other.m_num_bits; ++i) { + push_back(other.get(i)); + } + } + + uint64 bit_vector::to_number(unsigned idx, unsigned length) const { + SASSERT(length <= 64); + uint64 r = 0; + for (unsigned i = 0; i < length; ++i) { + r = (r << 1) | (uint64)get(idx+i); + } + return r; + } + + bool bit_vector::operator<(bit_vector const & other) const { + SASSERT(m_num_bits == other.m_num_bits); + unsigned n = num_words(); + if (n == 0) + return false; + + for (unsigned i = 0; i < n - 1; ++i) { + if (m_data[i] > other.m_data[i]) + return false; + if (m_data[i] < other.m_data[i]) + return true; + } + + unsigned bit_rest = m_num_bits % 32; + unsigned mask = (1 << bit_rest) - 1; + if (mask == 0) mask = UINT_MAX; + return (m_data[n-1] & mask) < (other.m_data[n-1] & mask); + } + + table_information::table_information(table_plugin & p, const table_signature& sig) : + m_column_info(sig.size()+1), + m_bv_util(p.get_context().get_manager()), + m_decl_util(p.get_context().get_manager()) { + + unsigned column = 0; + for (unsigned i = 0; i < sig.size(); ++i) { + unsigned num_bits = uint64_log2(sig[i]); + SASSERT(num_bits == 64 || (1ULL << num_bits) == sig[i]); + m_column_info[i] = column; + column += num_bits; + } + m_column_info[sig.size()] = column; + } + + void table_information::expand_column_vector(unsigned_vector& v, const table_information *other) const { + unsigned_vector orig; + orig.swap(v); + + for (unsigned i = 0; i < orig.size(); ++i) { + unsigned col, limit; + if (orig[i] < get_num_cols()) { + col = column_idx(orig[i]); + limit = col + column_num_bits(orig[i]); + } else { + unsigned idx = orig[i] - get_num_cols(); + col = get_num_bits() + other->column_idx(idx); + limit = col + other->column_num_bits(idx); + } + + for (; col < limit; ++col) { + v.push_back(col); + } + } + } + + void table_information::display(std::ostream & out) const { + out << '<'; + for (unsigned i = 0; i < get_num_cols(); ++i) { + if (i > 0) + out << ", "; + out << column_num_bits(i); + } + out << ">\n"; + } + + ternary_bitvector::ternary_bitvector(unsigned size, bool full) : + bit_vector() { + resize(size, full); + } + + ternary_bitvector::ternary_bitvector(uint64 n, unsigned num_bits) : + bit_vector(2 * num_bits) { + append_number(n, num_bits); + } + + ternary_bitvector::ternary_bitvector(const table_fact& f, const table_information& t) : + bit_vector(2 * t.get_num_bits()) { + for (unsigned i = 0; i < f.size(); ++i) { + SASSERT(t.column_idx(i) == size()); + append_number(f[i], t.column_num_bits(i)); + } + SASSERT(size() == t.get_num_bits()); + } + + void ternary_bitvector::fill1() { + memset(m_data, 0xFF, m_capacity * sizeof(unsigned)); + } + + unsigned ternary_bitvector::get(unsigned idx) const { + idx *= 2; + return (bit_vector::get(idx) << 1) | (unsigned)bit_vector::get(idx+1); + } + + void ternary_bitvector::set(unsigned idx, unsigned val) { + SASSERT(val == BIT_0 || val == BIT_1 || val == BIT_x); + idx *= 2; + bit_vector::set(idx, (val >> 1) != 0); + bit_vector::set(idx+1, (val & 1) != 0); + } + + void ternary_bitvector::push_back(unsigned val) { + SASSERT(val == BIT_0 || val == BIT_1 || val == BIT_x); + bit_vector::push_back((val >> 1) != 0); + bit_vector::push_back((val & 1) != 0); + } + + void ternary_bitvector::append_number(uint64 n, unsigned num_bits) { + SASSERT(num_bits <= 64); + for (int bit = num_bits-1; bit >= 0; --bit) { + if (n & (1ULL << bit)) { + push_back(BIT_1); + } else { + push_back(BIT_0); + } + } + } + + void ternary_bitvector::mk_idx_eq(unsigned idx, ternary_bitvector& val) { + for (unsigned i = 0; i < val.size(); ++i) { + set(idx+i, val.get(i)); + } + } + + ternary_bitvector ternary_bitvector::and(const ternary_bitvector& other) const{ + ternary_bitvector result(*this); + result &= other; + return result; + } + + void ternary_bitvector::neg(union_ternary_bitvector& result) const { + ternary_bitvector negated; + negated.resize(size()); + + for (unsigned i = 0; i < size(); ++i) { + switch (get(i)) { + case BIT_0: + negated.fill1(); + negated.set(i, BIT_1); + break; + case BIT_1: + negated.fill1(); + negated.set(i, BIT_0); + break; + default: + continue; + } + result.add_fact(negated); + } + } + + static void join_fix_eqs(ternary_bitvector& TBV, unsigned idx, unsigned col2_offset, + const unsigned_vector& cols1, const unsigned_vector& cols2, + union_ternary_bitvector& result) { + if (idx == cols1.size()) { + result.add_fact(TBV); + return; + } + + unsigned idx1 = cols1[idx]; + unsigned idx2 = cols2[idx] + col2_offset; + unsigned v1 = TBV.get(idx1); + unsigned v2 = TBV.get(idx2); + + if (v1 == BIT_x) { + if (v2 == BIT_x) { + // both x: duplicate row + ternary_bitvector TBV2(TBV); + TBV2.set(idx1, BIT_0); + TBV2.set(idx2, BIT_0); + join_fix_eqs(TBV2, idx+1, col2_offset, cols1, cols2, result); + + TBV.set(idx1, BIT_1); + TBV.set(idx2, BIT_1); + } else { + TBV.set(idx1, v2); + } + } else if (v2 == BIT_x) { + TBV.set(idx2, v1); + } else if (v1 != v2) { + // columns don't match + return; + } + join_fix_eqs(TBV, idx+1, col2_offset, cols1, cols2, result); + } + + void ternary_bitvector::join(const ternary_bitvector& other, + const unsigned_vector& cols1, + const unsigned_vector& cols2, + union_ternary_bitvector& result) const { + ternary_bitvector TBV(*this); + TBV.append(other); + join_fix_eqs(TBV, 0, size(), cols1, cols2, result); + } + + bool ternary_bitvector::project(const unsigned_vector& delcols, ternary_bitvector& result) const { + unsigned *rm_cols = delcols.c_ptr(); + + for (unsigned i = 0; i < size(); ++i) { + if (*rm_cols == i) { + ++rm_cols; + continue; + } + result.push_back(get(i)); + } + return true; + } + + static void copy_column(ternary_bitvector& CopyTo, const ternary_bitvector& CopyFrom, + unsigned col_dst, unsigned col_src, const table_information& src_table, + const table_information& dst_table) { + unsigned idx_dst = dst_table.column_idx(col_dst); + unsigned idx_src = src_table.column_idx(col_src); + unsigned num_bits = dst_table.column_num_bits(col_dst); + SASSERT(num_bits == src_table.column_num_bits(col_src)); + + for (unsigned i = 0; i < num_bits; ++i) { + CopyTo.set(idx_dst+i, CopyFrom.get(idx_src+i)); + } + } + + void ternary_bitvector::rename(const unsigned_vector& cyclecols, + const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, + const table_information& dst_table, + ternary_bitvector& result) const { + result.resize(dst_table.get_num_bits()); + + for (unsigned i = 1; i < cyclecols.size(); ++i) { + copy_column(result, *this, cyclecols[i-1], cyclecols[i], src_table, dst_table); + } + copy_column(result, *this, cyclecols[cyclecols.size()-1], cyclecols[0], src_table, dst_table); + + for (unsigned i = 0; i < out_of_cycle_cols.size(); ++i) { + unsigned col = out_of_cycle_cols[i]; + copy_column(result, *this, col, col, src_table, dst_table); + } + } + + unsigned ternary_bitvector::size_in_bytes() const { + return sizeof(*this) + m_capacity; + } + + void ternary_bitvector::display(std::ostream & out) const { + for (unsigned i = 0; i < size(); ++i) { + switch (get(i)) { + case BIT_0: + out << '0'; + break; + case BIT_1: + out << '1'; + break; + case BIT_x: + out << 'x'; + break; + default: + UNREACHABLE(); + } + } + } + +#if Z3DEBUG + void ternary_bitvector::expand(std::set & BVs) const { + bit_vector BV(m_num_bits); + expand(BVs, BV, 0); + } + + void ternary_bitvector::expand(std::set & BVs, bit_vector &BV, unsigned idx) const { + if (idx == size()) { + BVs.insert(BV); + return; + } + + switch (get(idx)) { + case BIT_0: + BV.push_back(false); + expand(BVs, BV, idx+1); + break; + case BIT_1: + BV.push_back(true); + expand(BVs, BV, idx+1); + break; + case BIT_x: { // x: duplicate + bit_vector BV2(BV); + BV.push_back(false); + BV2.push_back(true); + expand(BVs, BV, idx+1); + expand(BVs, BV2, idx+1); + } + break; + default: + UNREACHABLE(); + } + } +#endif + +} diff --git a/src/muz_qe/dl_hassel_common.h b/src/muz_qe/dl_hassel_common.h new file mode 100755 index 000000000..7c1d1e614 --- /dev/null +++ b/src/muz_qe/dl_hassel_common.h @@ -0,0 +1,1079 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_common.h + +Abstract: + + + +Revision History: + +--*/ + +#ifndef _DL_HASSEL_COMMON_H_ +#define _DL_HASSEL_COMMON_H_ + +#include "bit_vector.h" +#include "dl_base.h" +#include "bv_decl_plugin.h" +#include "union_find.h" +#include +#include + +#define BIT_0 ((0<<1)|1) +#define BIT_1 ((1<<1)|0) +#define BIT_x ((1<<1)|1) + +namespace datalog { + + expr_ref formula_to_dnf(expr_ref f); + + class bit_vector : public ::bit_vector { + public: + bit_vector() : ::bit_vector() {} + bit_vector(unsigned bits) : ::bit_vector(bits) {} + + bool contains(const bit_vector & other) const; + bool contains(const bit_vector & other, unsigned idx) const; + bool contains_consecutive_zeros() const; + + bit_vector slice(unsigned idx, unsigned length) const; + void append(const bit_vector & other); + + uint64 to_number(unsigned idx, unsigned length) const; + + // for std::less operations + bool operator<(bit_vector const & other) const; + }; + + + class table_information { + unsigned_vector m_column_info; + bv_util m_bv_util; + dl_decl_util m_decl_util; + + public: + table_information(table_plugin & p, const table_signature& sig); + + unsigned get_num_bits() const { + return m_column_info.back(); + } + + unsigned get_num_cols() const { + return m_column_info.size()-1; + } + + unsigned column_idx(unsigned col) const { + return m_column_info[col]; + } + + unsigned column_num_bits(unsigned col) const { + return m_column_info[col+1] - m_column_info[col]; + } + + void expand_column_vector(unsigned_vector& v, const table_information *other = 0) const; + + void display(std::ostream & out) const; + + const bv_util& get_bv_util() const { return m_bv_util; } + const dl_decl_util& get_decl_util() const { return m_decl_util; } + }; + + + template class union_ternary_bitvector; + + + class ternary_bitvector : private bit_vector { + public: + ternary_bitvector() : bit_vector() {} + ternary_bitvector(unsigned size) : bit_vector(2 * size) {} + + ternary_bitvector(unsigned size, bool full); + ternary_bitvector(uint64 n, unsigned num_bits); + ternary_bitvector(const table_fact& f, const table_information& t); + + void swap(ternary_bitvector& other) { + SASSERT(size() == other.size()); + bit_vector::swap(other); + } + + void resize(unsigned new_size, bool val = false) { + bit_vector::resize(2 * new_size, val); + } + + void reset() { + m_num_bits = 0; + } + + unsigned size() const { + SASSERT((m_num_bits % 2) == 0); + return m_num_bits/2; + } + + void fill1(); + + void append(const ternary_bitvector & other) { bit_vector::append(other); } + bool contains(const ternary_bitvector & other) const { return bit_vector::contains(other); } + + bool is_empty() const { return contains_consecutive_zeros(); } + + unsigned get(unsigned idx) const; + void set(unsigned idx, unsigned val); + void push_back(unsigned val); + void append_number(uint64 n, unsigned num_bits); + void mk_idx_eq(unsigned idx, ternary_bitvector& val); + + ternary_bitvector and(const ternary_bitvector& other) const; + void neg(union_ternary_bitvector& result) const; + + void join(const ternary_bitvector& other, const unsigned_vector& cols1, + const unsigned_vector& cols2, union_ternary_bitvector& result) const; + + bool project(const unsigned_vector& delcols, ternary_bitvector& result) const; + + void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, const table_information& dst_table, + ternary_bitvector& result) const; + + static bool has_subtract() { return false; } + void subtract(const union_ternary_bitvector& other, + union_ternary_bitvector& result) const { UNREACHABLE(); } + + void display(std::ostream & out) const; + unsigned size_in_bytes() const; + +#if Z3DEBUG + void expand(std::set & BVs) const; +#endif + + private: +#if Z3DEBUG + void expand(std::set & BVs, bit_vector &BV, unsigned idx) const; +#endif + }; + + + template + class union_ternary_bitvector { + typedef std::list union_t; + + union_t m_bitvectors; + unsigned m_bv_size; //!< number of ternary bits + + public: + union_ternary_bitvector(unsigned bv_size) : m_bv_size(bv_size) {} + + union_ternary_bitvector(unsigned bv_size, bool full) : m_bv_size(bv_size) { + if (full) + mk_full(); + } + + union_ternary_bitvector and(const union_ternary_bitvector & Other) const { + if (empty()) + return *this; + if (Other.empty()) + return Other; + + union_ternary_bitvector Ret(m_bv_size); + + for (const_iterator I = begin(), E = end(); I != E; ++I) { + for (const_iterator II = Other.begin(), EE = Other.end(); II != EE; ++II) { + T row(I->and(*II)); + if (!row.is_empty()) + Ret.add_fact(row); + } + } + return Ret; + } + + union_ternary_bitvector or(const union_ternary_bitvector & Other) const { + if (empty()) + return Other; + if (Other.empty()) + return *this; + + union_ternary_bitvector Ret(*this); + Ret.add_facts(Other); + return Ret; + } + + union_ternary_bitvector neg() const { + union_ternary_bitvector Ret(m_bv_size); + Ret.mk_full(); + + union_ternary_bitvector negated(m_bv_size); + for (const_iterator I = begin(), E = end(); I != E; ++I) { + negated.reset(); + I->neg(negated); + Ret.swap(Ret.and(negated)); + } + return Ret; + } + + void subtract(const union_ternary_bitvector& other) { + if (!T::has_subtract()) { + swap(this->and(other.neg())); + return; + } + + union_ternary_bitvector subtracted(m_bv_size); + for (const_iterator I = begin(), E = end(); I != E; ++I) { + I->subtract(other, subtracted); + } + swap(subtracted); + } + +#if 0 + union_ternary_bitvector gc() const { + // Simple subsumption-based cleaning. + union_ternary_bitvector Ret(m_bv_size); + for (union_t::const_reverse_iterator I = m_bitvectors.rbegin(), E = m_bitvectors.rend(); I != E; ++I) { + Ret.add_fact(*I); + } + return Ret; + } +#endif + + void join(const union_ternary_bitvector& other, const unsigned_vector& cols1, + const unsigned_vector& cols2, union_ternary_bitvector& result) const { + for (const_iterator I = begin(), E = end(); I != E; ++I) { + for (const_iterator II = other.begin(), EE = other.end(); II != EE; ++II) { + I->join(*II, cols1, cols2, result); + } + } + } + + void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, const table_information& dst_table, + union_ternary_bitvector& result) const { + T row(m_bv_size); + for (const_iterator I = begin(), E = end(); I != E; ++I) { + row.reset(); + I->rename(cyclecols, out_of_cycle_cols, src_table, dst_table, row); + result.add_new_fact(row); + } + } + + void project(const unsigned_vector& delcols, union_ternary_bitvector& result) const { + unsigned new_size = m_bv_size - (delcols.size()-1); + T row(new_size); + + for (const_iterator I = begin(), E = end(); I != E; ++I) { + row.reset(); + if (I->project(delcols, row)) { + SASSERT(!row.is_empty()); + result.add_fact(row); + } + } + } + + private: + typedef union_find<> subset_ints; + + // returns 1 if row should be removed, 0 otherwise + static int fix_single_bit(T & BV, unsigned idx, unsigned value, const subset_ints& equalities) { + unsigned root = equalities.find(idx); + idx = root; + do { + unsigned bitval = BV.get(idx); + if (bitval == BIT_x) { + BV.set(idx, value); + } else if (bitval != value) { + return 1; + } + idx = equalities.next(idx); + } while (idx != root); + return 0; + } + + static int fix_single_bit(T & BV1, unsigned idx1, T & BV2, unsigned idx2, + subset_ints& equalities, bool discard_col) { + unsigned A = BV1.get(idx1); + unsigned B = BV2.get(idx2); + + if (A == BIT_x) { + if (B == BIT_x) { + // Both are don't cares. + /////// FIXME::: don't duplicate rows with diff table + if (!discard_col) + return 2; // duplicate row + equalities.merge(idx1, idx2); + return 0; + } else { + // only A is don't care. + return fix_single_bit(BV1, idx1, B, equalities); + } + } else if (B == BIT_x) { + // Only B is don't care. + return fix_single_bit(BV2, idx2, A, equalities); + } else if (A == B) { + return 0; + } else { + return 1; // remove row + } + } + + void fix_eq_bits(unsigned idx1, const T *BV, unsigned idx2, unsigned length, + subset_ints& equalities, const bit_vector& discard_cols) { + for (unsigned i = 0; i < length; ++i) { + for (union_t::iterator I = m_bitvectors.begin(), E = m_bitvectors.end(); I != E; ) { + T *eqBV = BV ? const_cast(BV) : &*I; + bool discard_col = discard_cols.get(idx1+i) || (!BV && discard_cols.get(idx2+i)); + + switch (fix_single_bit(*I, idx1+i, *eqBV, idx2+i, equalities, discard_col)) { + case 1: + // remove row + I = m_bitvectors.erase(I); + break; + + case 2: { + // duplicate row + T BV2(*I); + I->set(idx1+i, BIT_0); + I->set(idx2+i, BIT_0); + + BV2.set(idx1+i, BIT_1); + BV2.set(idx2+i, BIT_1); + m_bitvectors.insert(I, BV2); + ++I; + break;} + + default: + // bits fixed + ++I; + } + } + } + } + + /// make bits of table [idx,idx+max_length] equal to e sliced starting at idx2 + unsigned fix_eq_bits(unsigned idx, const expr *e, unsigned idx2, unsigned max_length, + const table_information& t, subset_ints& equalities, + const bit_vector & discard_cols) { + const bv_util& bvu = t.get_bv_util(); + const dl_decl_util& dutil = t.get_decl_util(); + + rational n; + unsigned bv_size; + if (bvu.is_numeral(e, n, bv_size)) { + T num(n.get_int64(), bv_size); + SASSERT(idx2 < bv_size); + max_length = std::min(max_length, bv_size - idx2); + fix_eq_bits(idx, &num, idx2, max_length, equalities, discard_cols); + return idx + max_length; + } + + uint64 num; + if (dutil.is_numeral(e, num)) { + T num_bv(num, max_length); + fix_eq_bits(idx, &num_bv, idx2, max_length, equalities, discard_cols); + return idx + max_length; + } + + if (bvu.is_concat(e)) { + const app *a = to_app(e); + + // skip the first elements of the concat if e.g. we have a top level extract + unsigned i = 0; + for (; i < a->get_num_args(); ++i) { + unsigned arg_size = bvu.get_bv_size(a->get_arg(i)); + if (idx2 < arg_size) + break; + idx2 -= arg_size; + } + + SASSERT(i < a->get_num_args()); + for (; max_length > 0 && i < a->get_num_args(); ++i) { + unsigned idx0 = idx; + idx = fix_eq_bits(idx, a->get_arg(i), idx2, max_length, t, equalities, discard_cols); + idx2 = 0; + SASSERT((idx - idx0) <= max_length); + max_length = max_length - (idx - idx0); + } + return idx; + } + + unsigned low, high; + expr *e2; + if (bvu.is_extract(e, low, high, e2)) { + SASSERT(low <= high); + unsigned size = bvu.get_bv_size(e2); + unsigned offset = size - (high+1) + idx2; + SASSERT(idx2 < (high-low+1)); + max_length = std::min(max_length, high - low + 1 - idx2); + return fix_eq_bits(idx, e2, offset, max_length, t, equalities, discard_cols); + } + + if (e->get_kind() == AST_VAR) { + unsigned idx_var = idx2 + t.column_idx(to_var(e)->get_idx()); + SASSERT(idx2 < t.column_num_bits(to_var(e)->get_idx())); + max_length = std::min(max_length, t.column_num_bits(to_var(e)->get_idx()) - idx2); + fix_eq_bits(idx, 0, idx_var, max_length, equalities, discard_cols); + return idx + max_length; + } + + NOT_IMPLEMENTED_YET(); + return 0; + } + + void filter(const expr *e, subset_ints& equalities, const bit_vector& discard_cols, + const table_information& t) { + switch (e->get_kind()) { + case AST_APP: { + const app *app = to_app(e); + switch (app->get_decl_kind()) { + case OP_AND: + for (unsigned i = 0; i < app->get_num_args(); ++i) { + filter(app->get_arg(i), equalities, discard_cols, t); + } + return; + + case OP_EQ: { + const expr *a = app->get_arg(0); + const var *v; + unsigned vidx = 0; + unsigned length; + + unsigned low, high; + expr *e2; + if (is_var(a)) { + v = to_var(a); + length = t.column_num_bits(v->get_idx()); + } else if (t.get_bv_util().is_extract(a, low, high, e2)) { + vidx = t.get_bv_util().get_bv_size(e2) - high - 1; + length = high - low + 1; + SASSERT(is_var(e2)); + v = to_var(e2); + } else { + NOT_IMPLEMENTED_YET(); + } + vidx += t.column_idx(v->get_idx()); + + unsigned final_idx = fix_eq_bits(vidx, app->get_arg(1), 0, length, t, equalities, discard_cols); + SASSERT(final_idx == vidx + length); + (void)final_idx; + return;} + + case OP_FALSE: + reset(); + return; + + case OP_NOT: { + union_ternary_bitvector sub(m_bv_size, true); + sub.filter(app->get_arg(0), equalities, discard_cols, t); + this->subtract(sub); + return;} + + case OP_OR: { + union_ternary_bitvector orig(m_bv_size); + swap(orig); + for (unsigned i = 0; i < app->get_num_args(); ++i) { + union_ternary_bitvector tmp(orig); + subset_ints eqs(equalities); + tmp.filter(app->get_arg(i), eqs, discard_cols, t); + add_facts(tmp); + } + return;} + + case OP_TRUE: + return; + + default: + std::cerr << "app decl: " << app->get_decl()->get_name() << " (" << app->get_decl_kind() << ")\n"; + NOT_IMPLEMENTED_YET(); + } + break;} + + case AST_VAR: { + // boolean var must be true (10) + SASSERT(t.column_num_bits(to_var(e)->get_idx()) == 1); + unsigned idx = t.column_idx(to_var(e)->get_idx()); + ternary_bitvector BV(1); + BV.push_back(BIT_1); + T BV2(BV); + fix_eq_bits(idx, &BV2, 0, 2, equalities, discard_cols); + return;} + + default: + break; + } + std::cerr << "expr kind: " << get_ast_kind_name(e->get_kind()) << '\n'; + NOT_IMPLEMENTED_YET(); + } + + public: + void filter(const expr *cond, const bit_vector& discard_cols, const table_information& table) { + // datastructure to store equalities with columns that will be projected out + union_find_default_ctx union_ctx; + subset_ints equalities(union_ctx); + for (unsigned i = 0, e = discard_cols.size(); i < e; ++i) { + equalities.mk_var(); + } + + filter(cond, equalities, discard_cols, table); + } + + bool contains(const T & fact) const { + for (const_iterator I = begin(), E = end(); I != E; ++I) { + if (I->contains(fact)) + return true; + } + return false; + } + + bool contains(const union_ternary_bitvector & other) const { + for (const_iterator I = other.begin(), E = other.end(); I != E; ++I) { + for (const_iterator II = begin(), EE = end(); II != EE; ++II) { + if (II->contains(*I)) + goto next_iter; + } + return false; +next_iter: ; + } + return true; + } + + unsigned num_disjs() const { + return (unsigned)m_bitvectors.size(); + } + + unsigned num_bytes() const { + unsigned size = sizeof(*this); + for (const_iterator I = begin(), E = end(); I != E; ++I) { + size += I->size_in_bytes(); + } + return size; + } + +#if Z3DEBUG + void expand(std::set & BVs) const { + for (const_iterator I = begin(), E = end(); I != E; ++I) { + I->expand(BVs); + } + } +#endif + + void add_facts(const union_ternary_bitvector & Other, union_ternary_bitvector *Delta = 0) { + for (const_iterator I = Other.begin(), E = Other.end(); I != E; ++I) { + if (add_fact(*I) && Delta) + Delta->add_fact(*I); + } + } + + bool add_fact(const T & fact) { + if (contains(fact)) + return false; + add_new_fact(fact); + return true; + } + + void add_new_fact(const T & fact) { + SASSERT(m_bv_size == fact.size()); + + // TODO: optimize sequence (karnaugh maps??) + // At least join 1-bit different BVs + m_bitvectors.push_back(fact); + } + + void mk_full() { + reset(); + add_new_fact(T(m_bv_size, true)); + } + + typedef typename union_t::const_iterator const_iterator; + + const_iterator begin() const { return m_bitvectors.begin(); } + const_iterator end() const { return m_bitvectors.end(); } + + bool empty() const { return m_bitvectors.empty(); } + void reset() { m_bitvectors.clear(); } + + void swap(union_ternary_bitvector& other) { + SASSERT(m_bv_size == other.m_bv_size); + m_bitvectors.swap(other.m_bitvectors); + } + + void display(std::ostream & out) const { + out << '#' << num_disjs() << " (bv" << m_bv_size << ") "; + + bool first = true; + for (const_iterator I = begin(), E = end(); I != E; ++I) { + if (!first) + out << " \\/ "; + first = false; + I->display(out); + } + out << '\n'; + } + }; + + + template + class common_hassel_table_plugin : public table_plugin { + public: + common_hassel_table_plugin(symbol &s, relation_manager & manager) : + table_plugin(s, manager) { } + + virtual table_base * mk_empty(const table_signature & s) { + return alloc(T, *this, s); + } + + virtual table_base * mk_full(func_decl* p, const table_signature & s) { + T *t = static_cast(mk_empty(s)); + t->mk_full(); + return t; + } + + virtual bool can_handle_signature(const table_signature & s) { + return s.functional_columns() == 0; + } + + private: + ast_manager& get_ast_manager() { return get_context().get_manager(); } + + class join_fn : public convenient_table_join_fn { + public: + join_fn(const T & t1, const T & t2, unsigned col_cnt, const unsigned *cols1, const unsigned *cols2) + : convenient_table_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2) { + t1.expand_column_vector(m_cols1); + t2.expand_column_vector(m_cols2); + } + + virtual table_base * operator()(const table_base & tb1, const table_base & tb2) { + const T & T1 = static_cast(tb1); + const T & T2 = static_cast(tb2); + T * Res = static_cast(T1.get_plugin().mk_empty(get_result_signature())); + T1.m_bitsets.join(T2.m_bitsets, m_cols1, m_cols2, Res->m_bitsets); + TRACE("dl_hassel", tout << "final size: " << Res->get_size_estimate_rows() << '\n';); + return Res; + } + }; + + public: + virtual table_join_fn * mk_join_fn(const table_base & t1, const table_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { + if (!check_kind(t1) || !check_kind(t2)) + return 0; + return alloc(join_fn, static_cast(t1), static_cast(t2), col_cnt, cols1, cols2); + } + + private: + class union_fn : public table_union_fn { + public: + virtual void operator()(table_base & tgt0, const table_base & src0, table_base * delta0) { + T & tgt = static_cast(tgt0); + const T & src = static_cast(src0); + T * delta = static_cast(delta0); + tgt.m_bitsets.add_facts(src.m_bitsets, delta ? &delta->m_bitsets : 0); + TRACE("dl_hassel", tout << "final size: " << tgt.get_size_estimate_rows() << '\n';); + } + }; + + public: + virtual table_union_fn * mk_union_fn(const table_base & tgt, const table_base & src, + const table_base * delta) { + if (!check_kind(tgt) || !check_kind(src)) + return 0; + return alloc(union_fn); + } + + private: + class project_fn : public convenient_table_project_fn { + public: + project_fn(const T & t, unsigned removed_col_cnt, const unsigned * removed_cols) + : convenient_table_project_fn(t.get_signature(), removed_col_cnt, removed_cols) { + t.expand_column_vector(m_removed_cols); + m_removed_cols.push_back(UINT_MAX); + } + + virtual table_base * operator()(const table_base & tb) { + const T & t = static_cast(tb); + T * res = static_cast(t.get_plugin().mk_empty(get_result_signature())); + t.m_bitsets.project(m_removed_cols, res->m_bitsets); + TRACE("dl_hassel", tout << "final size: " << res->get_size_estimate_rows() << '\n';); + return res; + } + }; + + public: + virtual table_transformer_fn * mk_project_fn(const table_base & t, unsigned col_cnt, + const unsigned * removed_cols) { + if (!check_kind(t)) + return 0; + return alloc(project_fn, static_cast(t), col_cnt, removed_cols); + } + + private: + class rename_fn : public convenient_table_rename_fn { + unsigned_vector m_out_of_cycle; + public: + rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len, const unsigned * permutation_cycle) + : convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) { + SASSERT(permutation_cycle_len >= 2); + idx_set cycle_cols; + for (unsigned i = 0; i < permutation_cycle_len; ++i) { + cycle_cols.insert(permutation_cycle[i]); + } + for (unsigned i = 0; i < orig_sig.size(); ++i) { + if (!cycle_cols.contains(i)) + m_out_of_cycle.push_back(i); + } + } + + virtual table_base * operator()(const table_base & tb) { + const T & t = static_cast(tb); + T * res = static_cast(t.get_plugin().mk_empty(get_result_signature())); + t.m_bitsets.rename(m_cycle, m_out_of_cycle, t, *res, res->m_bitsets); + TRACE("dl_hassel", tout << "final size: " << res->get_size_estimate_rows() << '\n';); + return res; + } + }; + + public: + virtual table_transformer_fn * mk_rename_fn(const table_base & t, unsigned permutation_cycle_len, + const unsigned * permutation_cycle) { + if (!check_kind(t)) + return 0; + return alloc(rename_fn, t.get_signature(), permutation_cycle_len, permutation_cycle); + } + + private: + class filter_equal_fn : public table_mutator_fn { + typename T::bitset_t m_filter; + public: + filter_equal_fn(const T & t, const table_element val, unsigned col) : + m_filter(t.get_num_bits()) { + ternary_bitvector filter_row(t.get_num_bits(), true); + ternary_bitvector column(val, t.column_num_bits(col)); + filter_row.mk_idx_eq(t.column_idx(col), column); + m_filter.add_new_fact(filter_row); + } + + virtual void operator()(table_base & tb) { + T & t = static_cast(tb); + t.m_bitsets.swap(m_filter.and(t.m_bitsets)); + TRACE("dl_hassel", tout << "final size: " << t.get_size_estimate_rows() << '\n';); + } + }; + + public: + virtual table_mutator_fn * mk_filter_equal_fn(const table_base & t, const table_element & value, + unsigned col) { + if (!check_kind(t)) + return 0; + return alloc(filter_equal_fn, static_cast(t), value, col); + } + + private: + static bool cond_is_guard(const expr *e, const table_information& t) { + switch (e->get_kind()) { + case AST_APP: { + const app *app = to_app(e); + switch (app->get_decl_kind()) { + case OP_AND: + case OP_OR: + case OP_NOT: + for (unsigned i = 0; i < app->get_num_args(); ++i) { + if (!cond_is_guard(app->get_arg(i), t)) + return false; + } + return true; + + case OP_EQ: { + const expr *a = app->get_arg(0), *b = app->get_arg(1); + + // column equality is not succinctly representable with TBVs + if (is_var(a) && is_var(b)) + return false; + + // (= var (concat var foo)) + if (t.get_bv_util().is_concat(b)) + return false; + + return true;} + + case OP_FALSE: + case OP_TRUE: + return true; + + default: + return false; + } + break;} + + case AST_VAR: + return true; + + default: + break; + } + return false; + } + + static void split_cond_guard(app *cond, expr_ref& guard, expr_ref& leftover, const table_information& t) { + expr_ref_vector guards(guard.m()); + expr_ref_vector leftovers(leftover.m()); + + if (is_app(cond) && to_app(cond)->get_decl_kind() == OP_AND) { + app *a = to_app(cond); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr *arg = a->get_arg(i); + if (cond_is_guard(arg, t)) { + guards.push_back(arg); + } else { + leftovers.push_back(arg); + } + } + } else if (cond_is_guard(cond, t)) { + guard = cond; + return; + } else { + leftover = cond; + return; + } + + if (guards.size() > 1) { + guard = formula_to_dnf(expr_ref(guard.m().mk_and(guards.size(), guards.c_ptr()), guard.m())); + } else if (guards.size() == 1) { + guard = guards.get(0); + } + + if (leftovers.size() > 1) { + leftover = formula_to_dnf(expr_ref(leftover.m().mk_and(leftovers.size(), leftovers.c_ptr()), leftover.m())); + } else if (leftovers.size() == 1) { + leftover = leftovers.get(0); + } + } + + class filter_fn : public table_mutator_fn { + expr_ref m_condition; + typename T::bitset_t m_filter; + bit_vector m_empty_bv; + public: + filter_fn(const T & t, ast_manager& m, app *condition) : + m_condition(m), m_filter(t.get_num_bits(), true) { + m_empty_bv.resize(t.get_num_bits(), false); + + expr_ref guard(m); + split_cond_guard(condition, guard, m_condition, t); + if (guard) + m_filter.filter(guard, m_empty_bv, t); + } + + virtual void operator()(table_base & tb) { + T & t = static_cast(tb); + // first apply guard and then run the interpreter on the leftover + t.m_bitsets.swap(m_filter.and(t.m_bitsets)); + if (m_condition) + t.m_bitsets.filter(m_condition, m_empty_bv, t); + TRACE("dl_hassel", tout << "final size: " << t.get_size_estimate_rows() << '\n';); + } + }; + + public: + virtual table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition) { + if (!check_kind(t)) + return 0; + TRACE("dl_hassel", tout << mk_pp(condition, get_ast_manager()) << '\n';); + return alloc(filter_fn, static_cast(t), get_ast_manager(), condition); + } + + private: + class filter_proj_fn : public convenient_table_project_fn { + expr_ref m_condition; + typename T::bitset_t m_filter; + bit_vector m_col_list; // map: col idx -> bool (whether the column is to be removed) + public: + filter_proj_fn(const T & t, ast_manager& m, app *condition, + unsigned col_cnt, const unsigned * removed_cols) : + convenient_table_project_fn(t.get_signature(), col_cnt, removed_cols), + m_condition(m), m_filter(t.get_num_bits(), true) { + 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); + split_cond_guard(condition, guard, m_condition, t); + if (guard) + m_filter.filter(guard, m_col_list, t); + } + + virtual table_base* operator()(const table_base & tb) { + const T & t = static_cast(tb); + // first apply guard and then run the interpreter on the leftover + typename T::bitset_t filtered(t.get_num_bits()); + filtered.swap(m_filter.and(t.m_bitsets)); + if (m_condition) + filtered.filter(m_condition, m_col_list, t); + + T * res = static_cast(t.get_plugin().mk_empty(get_result_signature())); + filtered.project(m_removed_cols, res->m_bitsets); + TRACE("dl_hassel", tout << "final size: " << res->get_size_estimate_rows() << '\n';); + return res; + } + }; + + public: + virtual table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols) { + if (!check_kind(t)) + return 0; + TRACE("dl_hassel", tout << mk_pp(condition, get_ast_manager()) << '\n';); + return alloc(filter_proj_fn, static_cast(t), get_ast_manager(), + condition, removed_col_cnt, removed_cols); + } + + + virtual table_intersection_filter_fn * mk_filter_by_negation_fn(const table_base & t, + const table_base & negated_obj, unsigned joined_col_cnt, const unsigned * t_cols, + const unsigned * negated_cols) { + NOT_IMPLEMENTED_YET(); + } + }; + + template + class common_hassel_table : public table_base, public table_information { + public: + typedef T bitset_t; + + common_hassel_table(table_plugin & p, const table_signature & sig) : + table_base(p, sig), table_information(p, sig), m_bitsets(get_num_bits()) { } + + virtual table_base * complement(func_decl* p, const table_element * func_columns = 0) const { + SASSERT(!func_columns); + + if (empty()) + return get_plugin().mk_full(p, get_signature()); + + common_hassel_table *res = static_cast(get_plugin().mk_empty(get_signature())); + res->m_bitsets.swap(m_bitsets.neg()); + return res; + } + + virtual void add_fact(const table_fact & f) { + m_bitsets.add_fact(ternary_bitvector(f, *this)); + } + + virtual void add_new_fact(const table_fact & f) { + m_bitsets.add_new_fact(ternary_bitvector(f, *this)); + } + + virtual void remove_fact(table_element const* fact) { + NOT_IMPLEMENTED_YET(); + } + + virtual void reset() { + m_bitsets.reset(); + } + + void mk_full() { + m_bitsets.mk_full(); + } + + virtual table_base * clone() const { + common_hassel_table *res = static_cast(get_plugin().mk_empty(get_signature())); + res->m_bitsets = m_bitsets; + return res; + } + + virtual bool contains_fact(const table_fact & f) { + return m_bitsets.contains(ternary_bitvector(f, *this)); + } + + virtual bool empty() const { + return m_bitsets.empty(); + } + +#if Z3DEBUG + class our_iterator_core : public iterator_core { + class our_row : public row_interface { + const our_iterator_core & m_parent; + const table_information& m_table; + public: + our_row(const common_hassel_table & t, const our_iterator_core & parent) : + row_interface(t), m_parent(parent), m_table(t) {} + + virtual table_element operator[](unsigned col) const { + return m_parent.it->to_number(m_table.column_idx(col), m_table.column_num_bits(col)); + } + }; + + our_row m_row_obj; + std::set BVs; + std::set::iterator it; + + public: + our_iterator_core(const common_hassel_table & t, bool finished) : + m_row_obj(t, *this) { + if (finished) { + it = BVs.end(); + return; + } + t.m_bitsets.expand(BVs); + it = BVs.begin(); + } + + virtual bool is_finished() const { + return it == BVs.end(); + } + + virtual row_interface & operator*() { + SASSERT(!is_finished()); + return m_row_obj; + } + + virtual void operator++() { + SASSERT(!is_finished()); + ++it; + } + }; +#endif + + virtual iterator begin() const { +#if Z3DEBUG + return mk_iterator(alloc(our_iterator_core, *this, false)); +#else + SASSERT(0 && "begin() disabled"); + return mk_iterator(0); +#endif + } + + virtual iterator end() const { +#if Z3DEBUG + return mk_iterator(alloc(our_iterator_core, *this, true)); +#else + SASSERT(0 && "end() disabled"); + return mk_iterator(0); +#endif + } + + virtual void display(std::ostream & out) const { + table_information::display(out); + m_bitsets.display(out); + } + + virtual void to_formula(relation_signature const& sig, expr_ref& fml) const { + // TODO + } + + virtual unsigned get_size_estimate_rows() const { + return m_bitsets.num_disjs(); + } + + virtual unsigned get_size_estimate_bytes() const { + return m_bitsets.num_bytes(); + } + + T m_bitsets; + }; + +} + +#endif diff --git a/src/muz_qe/dl_hassel_diff_table.cpp b/src/muz_qe/dl_hassel_diff_table.cpp new file mode 100755 index 000000000..3ddcb3bbe --- /dev/null +++ b/src/muz_qe/dl_hassel_diff_table.cpp @@ -0,0 +1,219 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_diff_table.cpp + +Abstract: + + + +Revision History: + +--*/ + +#include "ast_printer.h" +#include "dl_context.h" +#include "dl_util.h" +#include "dl_hassel_diff_table.h" + + +namespace datalog { + + ternary_diff_bitvector::ternary_diff_bitvector(unsigned size, bool full) : + m_pos(size, full), m_neg(size) { } + + ternary_diff_bitvector::ternary_diff_bitvector(uint64 n, unsigned num_bits) : + m_pos(n, num_bits), m_neg(num_bits) { } + + ternary_diff_bitvector::ternary_diff_bitvector(const ternary_bitvector & tbv) : + m_pos(tbv), m_neg(tbv.size()) { } + + bool ternary_diff_bitvector::contains(const ternary_diff_bitvector & other) const { + return m_pos.contains(other.m_pos) && other.m_neg.contains(m_neg); + } + + bool ternary_diff_bitvector::is_empty() const { + if (m_pos.is_empty()) + return true; + + return m_neg.contains(m_pos); + } + + ternary_diff_bitvector ternary_diff_bitvector::and(const ternary_diff_bitvector& other) const { + ternary_diff_bitvector result(m_pos.and(other.m_pos)); + result.m_neg.swap(m_neg.or(other.m_neg)); + return result; + } + + void ternary_diff_bitvector::neg(union_ternary_bitvector& result) const { + // not(A\B) <-> (T\A) U B + ternary_diff_bitvector negated(size(), true); + negated.m_neg.add_new_fact(m_pos); + result.add_fact(negated); + + for (union_ternary_bitvector::const_iterator I = m_neg.begin(), + E = m_neg.end(); I != E; ++I) { + result.add_fact(*I); + } + } + + void ternary_diff_bitvector::subtract(const union_ternary_bitvector& other, + union_ternary_bitvector& result) const { + ternary_diff_bitvector newfact(*this); + for (union_ternary_bitvector::const_iterator I = other.begin(), + E = other.end(); I != E; ++I) { + if (!I->m_neg.empty()) { + NOT_IMPLEMENTED_YET(); + } + newfact.m_neg.add_fact(I->m_pos); + } + + if (!newfact.is_empty()) + result.add_fact(newfact); + } + + void ternary_diff_bitvector::join(const ternary_diff_bitvector& other, + const unsigned_vector& cols1, + const unsigned_vector& cols2, + union_ternary_bitvector& result) const { + unsigned new_size = size() + other.size(); + ternary_diff_bitvector res(new_size); + + res.m_pos = m_pos; + res.m_pos.append(other.m_pos); + + for (unsigned i = 0; i < cols1.size(); ++i) { + unsigned idx1 = cols1[i]; + unsigned idx2 = size() + cols2[i]; + unsigned v1 = res.m_pos.get(idx1); + unsigned v2 = res.m_pos.get(idx2); + + if (v1 == BIT_x) { + if (v2 == BIT_x) { + // add to subtracted TBVs: 1xx0 and 0xx1 + { + ternary_bitvector r(new_size, true); + r.set(idx1, BIT_0); + r.set(idx2, BIT_1); + res.m_neg.add_new_fact(r); + } + { + ternary_bitvector r(new_size, true); + r.set(idx1, BIT_1); + r.set(idx2, BIT_0); + res.m_neg.add_new_fact(r); + } + } else { + res.m_pos.set(idx1, v2); + } + } else if (v2 == BIT_x) { + res.m_pos.set(idx2, v1); + } else if (v1 != v2) { + // columns don't match + return; + } + } + + // handle subtracted TBVs: 1010 -> 1010xxx + if (!m_neg.empty()) { + ternary_bitvector padding(other.size(), true); + for (union_ternary_bitvector::const_iterator I = m_neg.begin(), + E = m_neg.end(); I != E; ++I) { + ternary_bitvector BV(*I); + BV.append(padding); + res.m_neg.add_new_fact(BV); + } + } + + if (!other.m_neg.empty()) { + ternary_bitvector padding(size(), true); + for (union_ternary_bitvector::const_iterator I = other.m_neg.begin(), + E = other.m_neg.end(); I != E; ++I) { + ternary_bitvector BV(padding); + BV.append(*I); + res.m_neg.add_new_fact(BV); + } + } + + result.add_fact(res); + } + + bool ternary_diff_bitvector::project(const unsigned_vector& delcols, ternary_diff_bitvector& result) const { + m_pos.project(delcols, result.m_pos); + if (m_neg.empty()) + return true; + + ternary_bitvector newneg; + for (union_ternary_bitvector::const_iterator I = m_neg.begin(), + E = m_neg.end(); I != E; ++I) { + for (unsigned i = 0; i < delcols.size()-1; ++i) { + unsigned idx = delcols[i]; + if (I->get(idx) != BIT_x && m_pos.get(idx) == BIT_x) + goto skip_row; + } + newneg.reset(); + I->project(delcols, newneg); + result.m_neg.add_fact(newneg); +skip_row: ; + } + return !result.is_empty(); + } + + void ternary_diff_bitvector::rename(const unsigned_vector& cyclecols, + const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, + const table_information& dst_table, + ternary_diff_bitvector& result) const { + m_pos.rename(cyclecols, out_of_cycle_cols, src_table, dst_table, result.m_pos); + m_neg.rename(cyclecols, out_of_cycle_cols, src_table, dst_table, result.m_neg); + } + + unsigned ternary_diff_bitvector::get(unsigned idx) { + return m_pos.get(idx); + } + + void ternary_diff_bitvector::set(unsigned idx, unsigned val) { + m_pos.set(idx, val); + } + + void ternary_diff_bitvector::swap(ternary_diff_bitvector & other) { + m_pos.swap(other.m_pos); + m_neg.swap(other.m_neg); + } + + void ternary_diff_bitvector::reset() { + m_pos.reset(); + m_neg.reset(); + } + + void ternary_diff_bitvector::display(std::ostream & out) const { + m_pos.display(out); + if (!m_neg.empty()) { + out << " \\ "; + if (m_neg.num_disjs() > 1) out << '('; + m_neg.display(out); + if (m_neg.num_disjs() > 1) out << ')'; + } + } + + unsigned ternary_diff_bitvector::size_in_bytes() const { + return m_pos.size_in_bytes() + m_neg.num_bytes(); + } + +#if Z3DEBUG + void ternary_diff_bitvector::expand(std::set & BVs) const { + m_pos.expand(BVs); + SASSERT(!BVs.empty()); + + std::set NegBVs; + m_neg.expand(NegBVs); + BVs.erase(NegBVs.begin(), NegBVs.end()); + } +#endif + + hassel_diff_table_plugin::hassel_diff_table_plugin(relation_manager & manager) + : common_hassel_table_plugin(symbol("hassel_diff"), manager) {} + +} diff --git a/src/muz_qe/dl_hassel_diff_table.h b/src/muz_qe/dl_hassel_diff_table.h new file mode 100755 index 000000000..07340c7e8 --- /dev/null +++ b/src/muz_qe/dl_hassel_diff_table.h @@ -0,0 +1,87 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_diff_table.h + +Abstract: + + + +Revision History: + +--*/ + +#ifndef _DL_HASSEL_DIFF_TABLE_H_ +#define _DL_HASSEL_DIFF_TABLE_H_ + +#include "dl_hassel_common.h" + +namespace datalog { + + class hassel_diff_table; + + class ternary_diff_bitvector { + // pos \ (neg0 \/ ... \/ negn) + ternary_bitvector m_pos; + union_ternary_bitvector m_neg; + + public: + ternary_diff_bitvector() : m_pos(), m_neg(0) {} + ternary_diff_bitvector(unsigned size) : m_pos(size), m_neg(size) {} + ternary_diff_bitvector(unsigned size, bool full); + ternary_diff_bitvector(uint64 n, unsigned num_bits); + ternary_diff_bitvector(const ternary_bitvector & tbv); + + bool contains(const ternary_diff_bitvector & other) const; + bool is_empty() const; + + ternary_diff_bitvector and(const ternary_diff_bitvector& other) const; + void neg(union_ternary_bitvector& result) const; + + static bool has_subtract() { return true; } + void subtract(const union_ternary_bitvector& other, + union_ternary_bitvector& result) const; + + void join(const ternary_diff_bitvector& other, const unsigned_vector& cols1, + const unsigned_vector& cols2, union_ternary_bitvector& result) const; + + bool project(const unsigned_vector& delcols, ternary_diff_bitvector& result) const; + + void rename(const unsigned_vector& cyclecols, const unsigned_vector& out_of_cycle_cols, + const table_information& src_table, const table_information& dst_table, + ternary_diff_bitvector& result) const; + + unsigned get(unsigned idx); + void set(unsigned idx, unsigned val); + + void swap(ternary_diff_bitvector & other); + void reset(); + + unsigned size() const { return m_pos.size(); } + + void display(std::ostream & out) const; + unsigned size_in_bytes() const; + +#if Z3DEBUG + void expand(std::set & BVs) const; +#endif + }; + + typedef union_ternary_bitvector union_ternary_diff_bitvector; + + class hassel_diff_table : public common_hassel_table { + public: + hassel_diff_table(table_plugin & p, const table_signature & sig) : + common_hassel_table(p, sig) {} + }; + + class hassel_diff_table_plugin : public common_hassel_table_plugin { + public: + hassel_diff_table_plugin(relation_manager & manager); + }; + +} + +#endif diff --git a/src/muz_qe/dl_hassel_table.cpp b/src/muz_qe/dl_hassel_table.cpp new file mode 100644 index 000000000..6ec28df87 --- /dev/null +++ b/src/muz_qe/dl_hassel_table.cpp @@ -0,0 +1,27 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_table.cpp + +Abstract: + + + +Revision History: + +--*/ + +#include "ast_printer.h" +#include "dl_context.h" +#include "dl_util.h" +#include "dl_hassel_table.h" + + +namespace datalog { + + hassel_table_plugin::hassel_table_plugin(relation_manager & manager) + : common_hassel_table_plugin(symbol("hassel"), manager) {} + +} diff --git a/src/muz_qe/dl_hassel_table.h b/src/muz_qe/dl_hassel_table.h new file mode 100644 index 000000000..6c4e9c1fe --- /dev/null +++ b/src/muz_qe/dl_hassel_table.h @@ -0,0 +1,39 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_hassel_table.h + +Abstract: + + + +Revision History: + +--*/ + +#ifndef _DL_HASSEL_TABLE_H_ +#define _DL_HASSEL_TABLE_H_ + +#include "dl_hassel_common.h" + +namespace datalog { + + class hassel_table; + typedef union_ternary_bitvector union_ternary_bitvectors; + + class hassel_table : public common_hassel_table { + public: + hassel_table(table_plugin & p, const table_signature & sig) : + common_hassel_table(p, sig) {} + }; + + class hassel_table_plugin : public common_hassel_table_plugin { + public: + hassel_table_plugin(relation_manager & manager); + }; + +} + +#endif diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index b103d743e..6b16968c2 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -526,6 +526,64 @@ namespace datalog { return alloc(instr_filter_interpreted, reg, condition); } + class instr_filter_interpreted_and_project : public instruction { + reg_idx m_src; + reg_idx m_res; + app_ref m_cond; + unsigned_vector m_cols; + public: + instr_filter_interpreted_and_project(reg_idx src, app_ref & condition, + unsigned col_cnt, const unsigned * removed_cols, reg_idx result) + : m_src(src), m_cond(condition), m_cols(col_cnt, removed_cols), + m_res(result) {} + + virtual bool perform(execution_context & ctx) { + if (!ctx.reg(m_src)) { + ctx.make_empty(m_res); + return true; + } + + relation_transformer_fn * fn; + relation_base & reg = *ctx.reg(m_src); + if (!find_fn(reg, fn)) { + fn = reg.get_manager().mk_filter_interpreted_and_project_fn(reg, m_cond, m_cols.size(), m_cols.c_ptr()); + if (!fn) { + throw default_exception( + "trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s", + reg.get_plugin().get_name().bare_str()); + } + store_fn(reg, fn); + } + + ctx.set_reg(m_res, (*fn)(reg)); + + if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) { + ctx.make_empty(m_res); + } + return true; + } + + virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const { + out << "filter_interpreted_and_project " << m_src << " into " << m_res; + out << " using " << mk_pp(m_cond, m_cond.get_manager()); + out << " deleting columns "; + print_container(m_cols, out); + } + + virtual void make_annotations(execution_context & ctx) { + std::stringstream s; + std::string a = "rel_src"; + ctx.get_register_annotation(m_src, a); + s << "filter_interpreted_and_project " << mk_pp(m_cond, m_cond.get_manager()); + ctx.set_register_annotation(m_res, s.str()); + } + }; + + instruction * instruction::mk_filter_interpreted_and_project(reg_idx reg, app_ref & condition, + unsigned col_cnt, const unsigned * removed_cols, reg_idx result) { + return alloc(instr_filter_interpreted_and_project, reg, condition, col_cnt, removed_cols, result); + } + class instr_union : public instruction { reg_idx m_src; @@ -592,6 +650,7 @@ namespace datalog { } } + SASSERT(r_src.get_signature().size() == r_tgt.get_signature().size()); TRACE("dl_verbose", r_tgt.display(tout <<"pre-union:");); (*fn)(r_tgt, r_src, r_delta); diff --git a/src/muz_qe/dl_instruction.h b/src/muz_qe/dl_instruction.h index ae6310ba6..97622c6f3 100644 --- a/src/muz_qe/dl_instruction.h +++ b/src/muz_qe/dl_instruction.h @@ -260,6 +260,8 @@ namespace datalog { static instruction * mk_filter_equal(ast_manager & m, reg_idx reg, const relation_element & value, unsigned col); static instruction * mk_filter_identical(reg_idx reg, unsigned col_cnt, const unsigned * identical_cols); static instruction * mk_filter_interpreted(reg_idx reg, app_ref & condition); + static instruction * mk_filter_interpreted_and_project(reg_idx src, app_ref & condition, + unsigned col_cnt, const unsigned * removed_cols, reg_idx result); static instruction * mk_union(reg_idx src, reg_idx tgt, reg_idx delta); static instruction * mk_widen(reg_idx src, reg_idx tgt, reg_idx delta); static instruction * mk_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp index 986a1f2c4..ce20961f1 100644 --- a/src/muz_qe/dl_relation_manager.cpp +++ b/src/muz_qe/dl_relation_manager.cpp @@ -720,6 +720,13 @@ namespace datalog { return t.get_plugin().mk_filter_interpreted_fn(t, condition); } + relation_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const relation_base & t, + app * condition, + unsigned removed_col_cnt, + const unsigned * removed_cols) { + return t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols); + } + class relation_manager::default_relation_select_equal_and_project_fn : public relation_transformer_fn { scoped_ptr m_filter; @@ -1387,6 +1394,45 @@ namespace datalog { } + class relation_manager::default_table_filter_interpreted_and_project_fn + : public table_transformer_fn { + scoped_ptr m_filter; + scoped_ptr m_project; + app_ref m_condition; + unsigned_vector m_removed_cols; + public: + default_table_filter_interpreted_and_project_fn(context & ctx, table_mutator_fn * filter, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) + : m_filter(filter), m_condition(condition, ctx.get_manager()), + m_removed_cols(removed_col_cnt, removed_cols) {} + + virtual table_base* operator()(const table_base & tb) { + table_base *t2 = tb.clone(); + (*m_filter)(*t2); + if (!m_project) { + relation_manager & rmgr = t2->get_plugin().get_manager(); + m_project = rmgr.mk_project_fn(*t2, m_removed_cols.size(), m_removed_cols.c_ptr()); + if (!m_project) { + throw default_exception("projection does not exist"); + } + } + return (*m_project)(*t2); + } + }; + + table_transformer_fn * relation_manager::mk_filter_interpreted_and_project_fn(const table_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) { + table_transformer_fn * res = t.get_plugin().mk_filter_interpreted_and_project_fn(t, condition, removed_col_cnt, removed_cols); + if (res) + return res; + + table_mutator_fn * filter = mk_filter_interpreted_fn(t, condition); + SASSERT(filter); + res = alloc(default_table_filter_interpreted_and_project_fn, get_context(), filter, condition, removed_col_cnt, removed_cols); + return res; + } + + table_intersection_filter_fn * relation_manager::mk_filter_by_intersection_fn(const table_base & t, const table_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols) { table_intersection_filter_fn * res = t.get_plugin().mk_filter_by_negation_fn(t, src, joined_col_cnt, diff --git a/src/muz_qe/dl_relation_manager.h b/src/muz_qe/dl_relation_manager.h index f22ae7923..ccdba2783 100644 --- a/src/muz_qe/dl_relation_manager.h +++ b/src/muz_qe/dl_relation_manager.h @@ -55,6 +55,7 @@ namespace datalog { class default_table_filter_equal_fn; class default_table_filter_identical_fn; class default_table_filter_interpreted_fn; + class default_table_filter_interpreted_and_project_fn; class default_table_negation_filter_fn; class default_table_filter_not_equal_fn; class default_table_select_equal_and_project_fn; @@ -350,6 +351,9 @@ namespace datalog { relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition); + relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols); + /** \brief Operations that returns all rows of \c t for which is column \c col equal to \c value with the column \c col removed. @@ -522,6 +526,9 @@ namespace datalog { table_mutator_fn * mk_filter_interpreted_fn(const table_base & t, app * condition); + table_transformer_fn * mk_filter_interpreted_and_project_fn(const table_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols); + /** \brief Operations that returns all rows of \c t for which is column \c col equal to \c value with the column \c col removed. diff --git a/src/muz_qe/dl_table_relation.cpp b/src/muz_qe/dl_table_relation.cpp index fc661366d..3c30c58bb 100644 --- a/src/muz_qe/dl_table_relation.cpp +++ b/src/muz_qe/dl_table_relation.cpp @@ -354,6 +354,21 @@ namespace datalog { return alloc(tr_mutator_fn, tfun); } + relation_transformer_fn * table_relation_plugin::mk_filter_interpreted_and_project_fn(const relation_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols) { + if (!t.from_table()) + return 0; + + const table_relation & tr = static_cast(t); + table_transformer_fn * tfun = get_manager().mk_filter_interpreted_and_project_fn(tr.get_table(), + condition, removed_col_cnt, removed_cols); + SASSERT(tfun); + + relation_signature sig; + relation_signature::from_project(t.get_signature(), removed_col_cnt, removed_cols, sig); + return alloc(tr_transformer_fn, sig, tfun); + } + class table_relation_plugin::tr_intersection_filter_fn : public relation_intersection_filter_fn { scoped_ptr m_tfun; public: diff --git a/src/muz_qe/dl_table_relation.h b/src/muz_qe/dl_table_relation.h index 12f0d4eaa..f86143c0f 100644 --- a/src/muz_qe/dl_table_relation.h +++ b/src/muz_qe/dl_table_relation.h @@ -71,6 +71,8 @@ namespace datalog { virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, unsigned col); virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition); + virtual relation_transformer_fn * mk_filter_interpreted_and_project_fn(const relation_base & t, + app * condition, unsigned removed_col_cnt, const unsigned * removed_cols); virtual relation_intersection_filter_fn * mk_filter_by_intersection_fn(const relation_base & t, const relation_base & src, unsigned joined_col_cnt, const unsigned * t_cols, const unsigned * src_cols); virtual relation_intersection_filter_fn * mk_filter_by_negation_fn(const relation_base & t, diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index 63e8ba700..3d61c04f0 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -18,6 +18,9 @@ Revision History: Extracted from dl_context --*/ + +#define Z3_HASSEL_TABLE + #include"rel_context.h" #include"dl_context.h" #include"dl_compiler.h" @@ -30,6 +33,10 @@ Revision History: #include"dl_mk_karr_invariants.h" #include"dl_finite_product_relation.h" #include"dl_sparse_table.h" +#ifdef Z3_HASSEL_TABLE +# include"dl_hassel_table.h" +# include"dl_hassel_diff_table.h" +#endif #include"dl_table.h" #include"dl_table_relation.h" #include"aig_exporter.h" @@ -87,6 +94,10 @@ namespace datalog { get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager())); get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager())); +#ifdef Z3_HASSEL_TABLE + get_rmanager().register_plugin(alloc(hassel_table_plugin, get_rmanager())); + get_rmanager().register_plugin(alloc(hassel_diff_table_plugin, get_rmanager())); +#endif // register plugins for builtin relations diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 2c641c5a6..cbe7a0618 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -28,6 +28,7 @@ COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); #define BV_DEFAULT_CAPACITY 2 class bit_vector { +protected: unsigned m_num_bits; unsigned m_capacity; //!< in words unsigned * m_data; @@ -64,6 +65,12 @@ public: m_data(0) { } + bit_vector(unsigned reserve_num_bits) : + m_num_bits(0), + m_capacity(num_words(reserve_num_bits)), + m_data(alloc_svect(unsigned, m_capacity)) { + } + bit_vector(bit_vector const & source): m_num_bits(source.m_num_bits), m_capacity(source.m_capacity),