merge hassel table code from branch

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>

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) {

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<table_join_fn> m_tocheck;
+        scoped_ptr<table_join_fn> 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<table_union_fn> m_tocheck;
         scoped_ptr<table_union_fn> 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<table_transformer_fn> m_checker;
+        scoped_ptr<table_transformer_fn> 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<table_transformer_fn> m_checker;
         scoped_ptr<table_transformer_fn> 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<table_transformer_fn> m_checker;
+        scoped_ptr<table_transformer_fn> 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<table_intersection_filter_fn> m_checker;
         scoped_ptr<table_intersection_filter_fn> m_tocheck;

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, 

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<expr> 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<sort> 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<sort> 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_index<ft_len; tail_index++) {
             app * t = r->get_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();
     }
 

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);
         /**

src/muz_qe/dl_hassel_common.cpp

@@ -0,0 +1,434 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_hassel_common.cpp
+
+Abstract:
+
+    <abstract>
+
+Revision History:
+
+--*/
+
+#include "dl_hassel_common.h"
+#include "dl_context.h"
+
+#include <vector>
+
+namespace datalog {
+
+    static void formula_to_dnf_aux(app *and, unsigned idx, std::set<expr*>& conjexpr, std::set<expr*>& toplevel, ast_manager& m) {
+        if (idx == and->get_num_args()) {
+            std::vector<expr*> 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<expr*> 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<expr*> toplevel, conjexpr;
+        formula_to_dnf_aux(a, 0, conjexpr, toplevel, f.m());
+
+        if (toplevel.size() > 1) {
+            std::vector<expr*> 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<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<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<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<bit_vector> & BVs) const {
+        bit_vector BV(m_num_bits);
+        expand(BVs, BV, 0);
+    }
+
+    void ternary_bitvector::expand(std::set<bit_vector> & 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
+
+}

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:
+
+    <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<ternary_diff_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<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<ternary_diff_bitvector>& other,
+        union_ternary_bitvector<ternary_diff_bitvector>& result) const {
+        ternary_diff_bitvector newfact(*this);
+        for (union_ternary_bitvector<ternary_diff_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<ternary_diff_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<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<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<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<bit_vector> & BVs) const {
+        m_pos.expand(BVs);
+        SASSERT(!BVs.empty());
+
+        std::set<bit_vector> 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) {}
+
+}

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:
+
+    <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<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<ternary_diff_bitvector>& result) const;
+
+        static bool has_subtract() { return true; }
+        void subtract(const union_ternary_bitvector<ternary_diff_bitvector>& other,
+            union_ternary_bitvector<ternary_diff_bitvector>& result) const;
+
+        void join(const ternary_diff_bitvector& other, const unsigned_vector& cols1,
+            const unsigned_vector& cols2, union_ternary_bitvector<ternary_diff_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<bit_vector> & BVs) const;
+#endif
+    };
+
+    typedef union_ternary_bitvector<ternary_diff_bitvector> union_ternary_diff_bitvector;
+
+    class hassel_diff_table : public common_hassel_table<union_ternary_diff_bitvector> {
+    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<hassel_diff_table> {
+    public:
+        hassel_diff_table_plugin(relation_manager & manager);
+    };
+
+}
+
+#endif

src/muz_qe/dl_hassel_table.cpp

@@ -0,0 +1,27 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_hassel_table.cpp
+
+Abstract:
+
+    <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) {}
+
+}

src/muz_qe/dl_hassel_table.h

@@ -0,0 +1,39 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    dl_hassel_table.h
+
+Abstract:
+
+    <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<ternary_bitvector> union_ternary_bitvectors;
+
+    class hassel_table : public common_hassel_table<union_ternary_bitvectors> {
+    public:
+        hassel_table(table_plugin & p, const table_signature & sig) :
+            common_hassel_table(p, sig) {}
+    };
+
+    class hassel_table_plugin : public common_hassel_table_plugin<hassel_table> {
+    public:
+        hassel_table_plugin(relation_manager & manager);
+    };
+
+}
+
+#endif

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);

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, 

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<relation_mutator_fn> m_filter;
@@ -1387,6 +1394,45 @@ namespace datalog {
     }
 
 
+    class relation_manager::default_table_filter_interpreted_and_project_fn 
+            : public table_transformer_fn {
+        scoped_ptr<table_mutator_fn> m_filter;
+        scoped_ptr<table_transformer_fn> 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, 

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.

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<const table_relation &>(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<table_intersection_filter_fn> m_tfun;
     public:

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, 

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
 

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),