move doc code to rel, adding unit test

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/muz/rel/dl_relation_manager.cpp

@@ -206,6 +206,7 @@ namespace datalog {
     }
 
     void relation_manager::register_relation_plugin_impl(relation_plugin * plugin) {
+        TRACE("dl", tout << "register: " << plugin->get_name() << "\n";);
         m_relation_plugins.push_back(plugin);
         plugin->initialize(get_next_relation_fid(*plugin));
         if (plugin->get_name() == get_context().default_relation()) {

src/muz/rel/doc.cpp

@@ -0,0 +1,463 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    doc.cpp
+
+Abstract:
+
+    difference of cubes.
+
+Author:
+
+    Nuno Lopes (a-nlopes) 2013-03-01
+    Nikolaj Bjorner (nbjorner) 2014-09-15
+
+Revision History:
+
+    Based on ternary_diff_bitvector by Nuno Lopes.
+
+--*/
+
+#include "doc.h"
+
+doc_manager::doc_manager(unsigned n): m(n), m_alloc("doc") {
+    m_full = m.allocateX();
+}
+
+doc_manager::~doc_manager() {
+    m.deallocate(m_full);
+}
+
+doc* doc_manager::allocate() {
+    return allocate(m.allocate());
+}
+doc* doc_manager::allocate1() {
+    return allocate(m.allocate1());
+}
+doc* doc_manager::allocate0() {
+    return allocate(m.allocate0());
+}
+doc* doc_manager::allocateX() {
+    return allocate(m.allocateX());
+}
+doc* doc_manager::allocate(doc const& src) {
+    doc* r = allocate(m.allocate(src.pos()));
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        r->neg().push_back(m.allocate(src.neg()[i]));
+    }
+    return r;
+}
+doc* doc_manager::allocate(tbv* t) {
+    void* mm = m_alloc.allocate(sizeof(doc));
+    return new (mm) doc(t);
+}
+doc* doc_manager::allocate(tbv const& src) {
+    return allocate(m.allocate(src));
+}
+doc* doc_manager::allocate(uint64 n) {
+    return allocate(m.allocate(n));
+}
+doc* doc_manager::allocate(rational const& r) {
+    return allocate(m.allocate(r));
+}
+doc* doc_manager::allocate(uint64 n, unsigned hi, unsigned lo) {
+    return allocate(m.allocate(n, hi, lo));
+}
+doc* doc_manager::allocate(doc const& src, unsigned const* permutation) {
+    doc* r = allocate(m.allocate(src.pos(), permutation));
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        r->neg().push_back(m.allocate(src.neg()[i], permutation));
+    }
+    return r;
+}
+void doc_manager::deallocate(doc* src) {
+    if (!src) return;
+    m.deallocate(&src->pos());
+    src->neg().reset(m);
+    m_alloc.deallocate(sizeof(doc), src);
+    //    dealloc(src);
+}
+void doc_manager::copy(doc& dst, doc const& src)  {
+    m.copy(dst.pos(), src.pos());
+    unsigned n = std::min(src.neg().size(), dst.neg().size());
+    for (unsigned i = 0; i < n; ++i) {
+        m.copy(dst.neg()[i], src.neg()[i]);
+    }
+    for (unsigned i = n; i < dst.neg().size(); ++i) {
+        dst.neg().erase(m, dst.neg().size()-1);
+    }
+    for (unsigned i = n; i < src.neg().size(); ++i) {
+        dst.neg().push_back(m.allocate(src.neg()[i]));
+    }
+}
+doc& doc_manager::fill0(doc& src) {
+    src.neg().reset(m);
+    m.fill0(src.pos());
+    return src;
+}
+doc& doc_manager::fill1(doc& src) {
+    src.neg().reset(m);
+    m.fill1(src.pos());
+    return src;
+}
+doc& doc_manager::fillX(doc& src) {
+    src.neg().reset(m);
+    m.fillX(src.pos());
+    return src;
+}
+bool doc_manager::set_and(doc& dst, doc const& src)  {
+    // (A \ B) & (C \ D) = (A & C) \ (B u D)
+    if (!m.set_and(dst.pos(), src.pos())) return false;
+    for (unsigned i = 0; i < dst.neg().size(); ++i) {
+        if (!m.set_and(dst.neg()[i], dst.pos())) {
+            dst.neg().erase(m, i);
+            --i;
+        }
+    }
+    tbv_ref t(m);
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        t = m.allocate(src.neg()[i]);
+        if (m.set_and(*t, dst.pos())) {
+            dst.neg().insert(m, t.detach());
+        }
+    }
+    return (src.neg().is_empty() || fold_neg(dst));
+}
+
+bool doc_manager::well_formed(doc const& d) const {
+    if (!m.is_well_formed(d.pos())) return false;
+    for (unsigned i = 0; i < d.neg().size(); ++i) {
+        if (!m.is_well_formed(d.neg()[i])) return false;
+        if (!m.contains(d.pos(), d.neg()[i])) return false;
+    }
+    return true;
+}
+
+bool doc_manager::fold_neg(doc& dst) {
+ start_over:
+    for (unsigned i = 0; i < dst.neg().size(); ++i) {
+        unsigned index;
+        unsigned count = diff_by_012(dst.pos(), dst.neg()[i], index);
+        if (count != 2) {
+            if (count == 0) {
+                return false;
+            }
+            else if (count == 3) {
+                dst.neg().erase(tbvm(), i);
+                --i;
+            }
+            else { // count == 1:
+                dst.pos().set(index, neg(dst.neg()[i][index]));
+                dst.neg().erase(tbvm(), i);
+                goto start_over;
+            }
+        }
+    }
+    return true;
+}
+
+unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& index) {
+    unsigned n = num_tbits();
+    unsigned count = 0;
+    for (unsigned i = 0; i < n; ++i) {
+        tbit b1 = pos[i];
+        tbit b2 = neg[i];
+        SASSERT(b1 != BIT_z && b2 != BIT_z);
+        if (b1 != b2) {
+            if (count == 1) return 2;
+            if (b1 == BIT_x) {
+                index = i;
+                count = 1;
+            }
+            else if (b2 != BIT_x) {
+                return 3;
+            }
+        }
+    }
+    return count;
+}
+
+void doc_manager::set(doc& d, unsigned idx, tbit value) {
+    d.pos().set(idx, value);
+    for (unsigned i = 0; i < d.neg().size(); ++i) {
+        d.neg()[i].set(idx, value);
+    }
+}
+
+//
+// merge range from [lo:lo+length-1] with each index in equivalence class.
+// under assumption of equalities and columns that are discarded.
+//
+bool doc_manager::merge(
+    doc& d, unsigned lo, unsigned length, 
+    subset_ints& equalities, bit_vector const& discard_cols) {
+    for (unsigned i = 0; i < length; ++i) {
+        unsigned idx = lo + i;
+        if (!merge(d, lo + i, equalities, discard_cols)) return false;
+    }
+    return true;
+}
+bool doc_manager::merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols) {
+    unsigned root = equalities.find(idx);
+    idx = root;
+    unsigned num_x = 0;
+    unsigned root1;
+    tbit value = BIT_x;
+    do {
+        switch (d[idx]) {
+        case BIT_0:
+            if (value == BIT_1) return false;
+            value = BIT_0;
+            break;
+        case BIT_1:
+            if (value == BIT_0) return false;
+            value = BIT_1;
+            break;
+        case BIT_x:
+            if (!discard_cols.get(idx)) {
+                ++num_x;
+                root1 = idx;
+            }
+            break;
+        default:
+            break;
+        }
+        idx = equalities.next(idx);
+    }
+    while (idx != root);
+
+    if (num_x == 0) {
+        // nothing to do.
+    }
+    else if (value != BIT_x) {
+        do {
+            if (d[idx] == BIT_x) {
+                set(d, idx, value);
+            }
+            idx = equalities.next(idx);
+        }
+        while (idx != root);
+    }
+    else {
+        do {
+            if (!discard_cols.get(idx) && idx != root1) {
+                tbv* t = tbvm().allocate(d.pos());
+                t->set(idx, BIT_0);
+                t->set(root1, BIT_1);
+                d.neg().insert(tbvm(), t);
+                t = tbvm().allocate(d.pos());
+                t->set(idx, BIT_1);
+                t->set(root1, BIT_0);
+                d.neg().insert(tbvm(), t);                
+            }
+            idx = equalities.next(idx);
+        }
+        while (idx != root);
+    }
+    return true;
+}
+
+bool doc_manager::intersect(doc const& A, doc const& B, doc& result) {
+    copy(result, A);
+    return set_and(result, B);
+}
+
+//
+// 1. If n = 0,1: can project directly.
+// 2. If tbv_i uses X in all positions with vars or constant where tbv is constant: can project directly.
+// 3. Perform resolution on remaining tbv_i 
+//
+// tbv & ~tbv1 & ~tbv2 & .. & ~tbv_n
+// Semantics of ~tbv1 is that it is a clause of literals.
+//   indices where BIT_1 is set are negative.
+//   indices where BIT_0 is set are positive.
+//
+
+doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src) {
+    tbv_manager& dstt = dstm.m;
+    doc* r = dstm.allocate(dstt.project(n, to_delete, src.pos()));
+
+    if (src.neg().is_empty()) {
+        return r;
+    }
+    if (src.neg().size() == 1) {
+        r->neg().push_back(dstt.project(n, to_delete, src.neg()[0]));
+        return r;
+    }
+    
+    //
+    // All negations can be projected if they are sign compatible.
+    //
+    tbv_ref bits(tbvm(), tbvm().allocateX());
+    for (unsigned i = 0; i < src.neg().size(); ++i) {        
+        tbvm().set_and(*bits, src.neg()[i]);
+    }
+    bool can_project_const = true;
+    for (unsigned i = 0; can_project_const && i < n; ++i) {
+        can_project_const = !to_delete[i] || (*bits)[i] == BIT_x;
+    }
+    if (can_project_const) {
+        for (unsigned i = 0; i < src.neg().size(); ++i) {        
+            r->neg().push_back(dstt.project(n, to_delete, src.neg()[i]));
+        }
+        return r;
+    }
+
+    // 
+    // A negation can be projected directly if it does not constrain
+    // deleted variables.
+    // 
+    ptr_vector<tbv> todo;
+    for (unsigned i = 0; i < src.neg().size(); ++i) {        
+        if (can_project_neg(src.pos(), n, to_delete, src.neg()[i])) {
+            r->neg().push_back(dstt.project(n, to_delete, src.neg()[i]));
+        }
+        else {
+            todo.push_back(tbvm().allocate(src.neg()[i]));
+        }
+    }
+    if (todo.empty()) {
+        return r;
+    }
+    ptr_vector<tbv> new_todo;
+    utbv pos, neg;
+    tbv_ref t1(tbvm()), t2(tbvm());
+    for (unsigned i = 0; i < n; ++i) {
+        if (to_delete[i] && (*bits)[i] != BIT_x) {
+            TRACE("doc", tout << "delete " << i << " ";
+                  for (unsigned j = 0; j < todo.size(); ++j) {
+                      tbvm().display(tout, *todo[j]) << " ";
+                  }
+                  tout << "\n";);
+            SASSERT(pos.is_empty());
+            SASSERT(neg.is_empty());
+            SASSERT(new_todo.empty());
+            while (!todo.empty()) {
+                tbv* t = todo.back();
+                todo.pop_back();
+                switch((*t)[i]) {
+                case BIT_x: new_todo.push_back(t); break;
+                case BIT_0: neg.push_back(t); break;
+                case BIT_1: pos.push_back(t); break;
+                default: UNREACHABLE(); break;                    
+                }
+            }
+            if (pos.is_empty() || neg.is_empty()) {
+                std::swap(new_todo, todo);
+                pos.reset(tbvm());
+                neg.reset(tbvm());
+                continue;
+            }
+            TRACE("doc",
+                  tout << "pos: ";
+                  for (unsigned i = 0; i < pos.size(); ++i) {
+                      tbvm().display(tout, pos[i]) << " ";
+                  }
+                  tout << "\nneg: ";
+                  for (unsigned i = 0; i < neg.size(); ++i) {
+                      tbvm().display(tout, neg[i]) << " ";
+                  }
+                  tout << "\n";
+                  );
+                  
+            for (unsigned j = 0; j < pos.size(); ++j) {
+                for (unsigned k = 0; k < neg.size(); ++k) {
+                    t1 = tbvm().allocate(pos[j]);
+                    (*t1).set(i, BIT_x);
+                    if (tbvm().set_and(*t1, neg[k])) {
+                        (*t1).set(i, BIT_x);
+                        new_todo.push_back(t1.detach());
+                    }
+                }                
+            }
+            pos.reset(tbvm());
+            neg.reset(tbvm());
+            std::swap(todo, new_todo);
+        }
+    }
+    for (unsigned i = 0; i < todo.size(); ++i) {
+        r->neg().push_back(dstt.project(n, to_delete, *todo[i]));
+        tbvm().deallocate(todo[i]);
+    }
+    return r;
+}
+
+bool doc_manager::can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg) {
+    for (unsigned i = 0; i < n; ++i) {
+        if (to_delete[i] && BIT_x != neg[i] && BIT_x == pos[i]) return false;
+    }
+    return true;
+}
+    
+
+void doc_manager::complement(doc const& src, ptr_vector<doc>& result) {
+    result.reset();
+    if (is_full(src)) {
+        return;
+    }
+    doc* r = allocateX();
+    r->neg().push_back(m.allocate(src.pos()));
+    result.push_back(r);
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        result.push_back(allocate(src.neg()[i]));
+    }
+}
+void doc_manager::subtract(doc const& A, doc const& B, ptr_vector<doc>& result) {
+    doc_ref r(*this), r2(*this);
+    r = allocate(A);
+    if (r->neg().insert(m, m.allocate(B.pos()))) {
+        result.push_back(r.detach());
+        r = allocate(A);
+    }
+    for (unsigned i = 0; i < B.neg().size(); ++i) {
+        r2 = allocate(B.neg()[i]);
+        if (set_and(*r, *r2)) {
+            result.push_back(r.detach());
+            r = allocate(A);
+        }
+    }
+}
+bool doc_manager::equals(doc const& a, doc const& b) const {
+    if (!m.equals(a.pos(), b.pos())) return false;
+    if (a.neg().size() != b.neg().size()) return false;
+    for (unsigned i = 0; i < a.neg().size(); ++i) {
+        if (!m.equals(a.neg()[i], b.neg()[i])) return false;
+    }
+    return true;
+}
+bool doc_manager::is_full(doc const& src) const {
+    return src.neg().is_empty() && m.equals(src.pos(), *m_full);
+}
+unsigned doc_manager::hash(doc const& src) const {
+    unsigned r = 0;
+    for (unsigned i = 0; i < src.neg().size(); ++i) {
+        r = 2*r + m.hash(src.neg()[i]);
+    }
+    return r + m.hash(src.pos());
+}
+// approximation
+// A \ (A1 u A2) contains B \ (B1 u B2)
+// if
+// A contains B
+// B1 contains A1 or A2
+bool doc_manager::contains(doc const& a, doc const& b) const {
+    if (!m.contains(a.pos(), b.pos())) return false;
+    for (unsigned i = 0; i < b.neg().size(); ++i) {
+        bool found = false;
+        for (unsigned j = 0; !found && j < a.neg().size(); ++j) {
+            found = m.contains(b.neg()[i],a.neg()[j]);
+        }
+        if (!found) return false;
+    }
+    return true;
+}
+std::ostream& doc_manager::display(std::ostream& out, doc const& b) const {
+    m.display(out, b.pos());
+    if (b.neg().is_empty()) return out;
+    out << " \\ ";
+    b.neg().display(m, out);
+    return out;
+}
+

src/muz/rel/doc.h

@@ -0,0 +1,306 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    doc.h
+
+Abstract:
+
+    difference of cubes.
+
+Author:
+
+    Nuno Lopes (a-nlopes) 2013-03-01
+    Nikolaj Bjorner (nbjorner) 2014-09-15
+
+Revision History:
+
+    Based on ternary_diff_bitvector by Nuno Lopes.
+
+--*/
+
+#ifndef _DOC_H_
+#define _DOC_H_
+
+#include "tbv.h"
+#include "union_find.h"
+
+
+class doc;
+template<typename M, typename T> class union_bvec;
+typedef union_find<> subset_ints;
+
+class doc_manager {
+    tbv_manager m;
+    tbv*        m_full;
+    small_object_allocator m_alloc;
+public:
+    doc_manager(unsigned num_bits);
+    ~doc_manager();
+    tbv_manager& tbvm() { return m; }
+    doc* allocate();
+    doc* allocate1();
+    doc* allocate0();
+    doc* allocateX();
+    doc* allocate(doc const& src);
+    doc* allocate(tbv const& src);
+    doc* allocate(tbv * src);
+    doc* allocate(uint64 n);
+    doc* allocate(rational const& r);
+    doc* allocate(uint64 n, unsigned hi, unsigned lo);
+    doc* allocate(doc const& src, unsigned const* permutation);
+    void deallocate(doc* src);        
+    void copy(doc& dst, doc const& src);
+    doc& reset(doc& src) { return fill0(src); }
+    doc& fill0(doc& src);
+    doc& fill1(doc& src);
+    doc& fillX(doc& src);
+    bool is_full(doc const& src) const;
+    bool set_and(doc& dst, doc const& src);
+    bool fold_neg(doc& dst);
+    bool intersect(doc const& A, doc const& B, doc& result);
+    void complement(doc const& src, ptr_vector<doc>& result);
+    void subtract(doc const& A, doc const& B, ptr_vector<doc>& result);
+    bool equals(doc const& a, doc const& b) const;
+    unsigned hash(doc const& src) const;
+    bool contains(doc const& a, doc const& b) const;
+    std::ostream& display(std::ostream& out, doc const& b) const;
+    unsigned num_tbits() const { return m.num_tbits(); }
+    doc* project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src);
+    bool well_formed(doc const& d) const;
+    bool merge(doc& d, unsigned lo, unsigned length, subset_ints& equalities, bit_vector const& discard_cols);
+    void set(doc& d, unsigned idx, tbit value);
+private:
+    unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
+    bool merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols);
+    bool can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg);
+};
+
+
+// union of tbv*, union of doc*
+template<typename M, typename T>
+class union_bvec { 
+    ptr_vector<T> m_elems; // TBD: reuse allocator of M
+
+    enum fix_bit_result_t {
+        e_row_removed, // = 1
+        e_duplicate_row, // = 2
+        e_fixed
+    };
+
+
+public:
+    unsigned size() const { return m_elems.size(); }
+    T& operator[](unsigned idx) const { return *m_elems[idx]; }
+    bool is_empty() const { return m_elems.empty(); }    
+    bool is_full(M& m) const { return size() == 1 && m.is_full(*m_elems[0]); }
+    bool contains(M& m, T& t) const {
+        for (unsigned i = 0; i < m_elems.size(); ++i) {
+            if (m.contains(*m_elems[i], t)) return true;
+        }
+        return false;
+    }
+    std::ostream& display(M const& m, std::ostream& out) const {
+        out << "{";
+        for (unsigned i = 0; i < size(); ++i) {
+            m.display(out, *m_elems[i]);
+            if (i + 1 < size()) out << ", ";
+        }
+        return out << "}";
+    }
+
+    void push_back(T* t) {
+        m_elems.push_back(t);
+    }
+    void erase(M& m, unsigned idx) {
+        T* t = m_elems[idx];
+        m_elems.erase(t);
+        m.deallocate(t);
+    }
+    void reset(M& m) {
+        for (unsigned i = 0; i < m_elems.size(); ++i) {
+            m.deallocate(m_elems[i]);
+        }
+        m_elems.reset(); 
+    }    
+    bool insert(M& m, T* t) {
+        unsigned sz = size(), j = 0;
+        bool found = false;
+        for (unsigned i = 0; i < sz; ++i, ++j) {
+            if (!found && m.contains(*t, *m_elems[i])) {
+                m.deallocate(m_elems[i]);
+                --j;
+            }
+            else {
+                if (m.contains(*m_elems[i], *t)) {
+                    found = true;
+                }
+                if (i != j) {                
+                    m_elems[j] = m_elems[i];
+                }       
+            }         
+        }
+        if (j != sz) m_elems.resize(j);
+        if (found) {
+            m.deallocate(t);
+        }
+        else {
+            m_elems.push_back(t);
+        }
+        return !found;
+    }
+    void intersect(M& m, T& t) {
+        unsigned sz = size();
+        unsigned j = 0;
+        for (unsigned i = 0; i < sz; ++i, ++j) {
+            if (!m.set_and(*m_elems[i], t)) {
+                m.deallocate(m_elems[i]);
+                --j;
+            }
+            else if (i != j) {
+                m_elems[i] = m_elems[j];
+            }
+        }
+        if (j != sz) m_elems.resize(j);
+    }
+    void insert(M& m, union_bvec const& other) {
+        for (unsigned i = 0; i < other.size(); ++i) {
+            insert(m, other[i]);
+        }
+    }
+    void intersect(M& m, union_bvec const& other) {
+        union_bvec result;
+        unsigned sz1 = size();
+        unsigned sz2 = other.size();
+        T* inter = m.allocate();
+        for (unsigned i = 0; i < sz1; ++i) {
+            for (unsigned j = 0; j < sz2; ++j) {
+                if (m.intersect(*m_elems[i], other[j], *inter)) {
+                    result.push_back(inter);
+                    inter = m.allocate();
+                }
+            }
+        }
+        m.deallocate(inter);
+        std::swap(result, *this);
+        result.reset(m);
+    }
+    void subtract(M& m, union_bvec const& other) {
+        unsigned sz = other.size();
+        for (unsigned i = 0; !is_empty() && i < sz; ++i) {
+            subtract(m, other[i]);
+        }
+        // TBD compress?
+    }
+    void subtract(M& m, T& t) {
+        unsigned sz = size();
+        bool found = false;
+        union_bvec result;
+        for (unsigned i = 0; i < sz; ++i) {
+            m.subtract(*m_elems[i], t, result.m_elems);
+        }
+        std::swap(m_elems, result.m_elems);
+        result.reset(m);
+    }
+    void complement(M& m, union_bvec& result) const {     
+        union_bvec negated;
+        result.reset(m);
+        result.push_back(m.allocateX());
+        unsigned sz = size();
+        for (unsigned i = 0; !is_empty() && i < sz; ++i) {
+            m.complement(*m_elems[i], negated.m_elems);
+            result.intersect(m, negated);
+            negated.reset(m);
+        }
+    }
+    void copy(M& m, union_bvec const& other) {
+        reset(m);
+        for (unsigned i = 0; i < other.size(); ++i) {
+            push_back(m.allocate(other[i]));
+        }
+    }
+
+    void merge(M& m, unsigned lo, unsigned length, subset_ints & equalities, bit_vector const& discard_cols) {
+        for (unsigned i = 0; i < size(); ++i) {
+            if (!m.merge(*m_elems[i], lo, length, equalities, discard_cols)) {
+                erase(m, i);
+                --i;
+            }
+        }
+    }
+
+    void merge(M& m, unsigned lo1, unsigned lo2, unsigned length, bit_vector const& discard_cols) {
+        union_find_default_ctx union_ctx;
+        subset_ints equalities(union_ctx);
+        for (unsigned i = 0; i < discard_cols.size(); ++i) {
+            equalities.mk_var();
+        }
+        for (unsigned j = 0; j < length; ++j) {
+            equalities.merge(lo1 + j, lo2 + j);
+        }
+        merge(m, lo1, length, equalities, discard_cols);
+    }
+
+
+private:
+
+
+};
+
+typedef union_bvec<tbv_manager, tbv> utbv;
+
+class doc {
+    // pos \ (neg_0 \/ ... \/ neg_n)
+    friend class doc_manager;
+    tbv*                         m_pos;
+    utbv                         m_neg;
+public:
+
+    struct eq {
+        doc_manager& m;
+        eq(doc_manager& m):m(m) {}
+        bool operator()(doc const& d1, doc const& d2) const {
+            return m.equals(d1, d2);
+        }
+    };
+
+    struct hash {
+        doc_manager& m;
+        hash(doc_manager& m):m(m) {}
+        unsigned operator()(doc const& d) const {
+            return m.hash(d);
+        }
+    };
+
+    doc(tbv* t): m_pos(t) {}
+    tbv& pos() { return *m_pos; }
+    utbv& neg() { return m_neg; }
+    tbv const& pos() const { return *m_pos; }
+    utbv const& neg() const { return m_neg; }
+    tbit operator[](unsigned idx) const { return pos()[idx]; }        
+};
+
+typedef union_bvec<doc_manager, doc> udoc;
+
+class doc_ref {
+    doc_manager& dm;
+    doc* d;
+public:
+    doc_ref(doc_manager& dm):dm(dm),d(0) {}
+    doc_ref(doc_manager& dm, doc* d):dm(dm),d(d) {}
+    ~doc_ref() {
+        if (d) dm.deallocate(d);
+    }
+    doc_ref& operator=(doc* d2) {
+        if (d) dm.deallocate(d);
+        d = d2;
+        return *this;
+    }
+    doc& operator*() { return *d; }
+    doc* operator->() { return d; }
+    doc* detach() { doc* r = d; d = 0; return r; }
+};
+
+#endif /* _DOC_H_ */
+

src/muz/rel/rel_context.cpp

@@ -32,6 +32,7 @@ Revision History:
 #include"karr_relation.h"
 #include"dl_finite_product_relation.h"
 #include"product_set.h"
+#include"udoc_relation.h"
 #include"dl_lazy_table.h"
 #include"dl_sparse_table.h"
 #include"dl_table.h"
@@ -114,6 +115,7 @@ namespace datalog {
         rm.register_plugin(alloc(interval_relation_plugin, rm));
         rm.register_plugin(alloc(karr_relation_plugin, rm));
         rm.register_plugin(alloc(product_set_plugin, rm));
+        rm.register_plugin(alloc(udoc_plugin, rm));
     }
 
     rel_context::~rel_context() {

src/muz/rel/tbv.cpp

@@ -0,0 +1,247 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    tbv.cpp
+
+Abstract:
+
+    ternary bit-vector utilities.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2014-09-15
+
+Revision History:
+
+
+--*/
+
+#include "tbv.h"
+#include "hashtable.h"
+
+
+//#define _DEBUG_MEM 1
+#define _DEBUG_MEM 0
+
+tbv_manager::~tbv_manager() {    
+#if _DEBUG_MEM
+    ptr_vector<tbv>::iterator it = allocated_tbvs.begin(), end = allocated_tbvs.end();
+    for (; it != end; ++it) {
+        std::cout << "dangling: " << (*it) << "\n";
+    }
+#endif
+}
+
+void tbv_manager::reset() {
+    m.reset();
+}
+tbv* tbv_manager::allocate() {
+    tbv* r = reinterpret_cast<tbv*>(m.allocate());
+#if _DEBUG_MEM
+    std::cout << allocated_tbvs.size() << " " << r << "\n";
+    allocated_tbvs.insert(r);
+#endif
+    return r;
+}
+tbv* tbv_manager::allocate1() {
+    tbv* v = allocate();
+    fill1(*v);
+    return v;
+}
+tbv* tbv_manager::allocate0() {
+    tbv* v = allocate();
+    fill0(*v);
+    return v;
+}
+tbv* tbv_manager::allocateX() {
+    tbv* v = allocate();
+    fillX(*v);
+    return v;
+}
+tbv* tbv_manager::allocate(tbv const& bv) {
+    tbv* r = allocate();
+    copy(*r, bv);
+    return r;
+}
+tbv* tbv_manager::allocate(uint64 val) {
+    tbv* v = allocate0();
+    for (unsigned bit = num_tbits(); bit > 0;) {
+        --bit;
+        if (val & (1ULL << bit)) {                        
+            v->set(bit, BIT_1);
+        } else {
+            v->set(bit, BIT_0);
+        }
+    }
+    return v;
+}
+
+tbv* tbv_manager::allocate(uint64 val, unsigned hi, unsigned lo) {
+    tbv* v = allocateX();
+    SASSERT(64 >= num_tbits() && num_tbits() > hi && hi >= lo);
+    v->set(val, hi, lo);
+    return v;
+}
+tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) {
+    tbv* r = allocate();
+    for (unsigned i = 0; i < num_tbits(); ++i) {
+        r->set(permutation[i], bv[i]);
+    }
+    return r;
+}
+tbv* tbv_manager::project(unsigned n, bool const* to_delete, tbv const& src) {
+    tbv* r = allocate();
+    unsigned i, j;
+    for (i = 0, j = 0; i < n; ++i) {
+        if (!to_delete[i]) {
+            r->set(j, src[i]);
+            ++j;
+        }
+    }
+    SASSERT(num_tbits() == j);
+    return r;
+}
+
+void tbv::set(uint64 val, unsigned hi, unsigned lo) {
+    for (unsigned i = 0; i < hi - lo + 1; ++i) {
+        set(lo + i, (val & (1ULL << i))?BIT_1:BIT_0);
+    }
+}
+void tbv::set(rational const& r, unsigned hi, unsigned lo) {
+    if (r.is_uint64()) {
+        set(r.get_uint64(), hi, lo);
+        return;
+    }
+    for (unsigned i = 0; i < hi - lo + 1; ++i) {
+        if (bitwise_and(r, rational::power_of_two(i)).is_zero())
+            set(lo + i, BIT_0);
+        else
+            set(lo + i, BIT_1);
+    }
+}
+
+void tbv::set(tbv const& other, unsigned hi, unsigned lo) {
+    for (unsigned i = 0; i < hi - lo + 1; ++i) {
+        set(lo + i, other[i]);
+    }
+}
+
+
+tbv* tbv_manager::allocate(rational const& r) {
+    if (r.is_uint64()) {
+        return allocate(r.get_uint64());
+    }
+    tbv* v = allocate0();
+    for (unsigned bit = num_tbits(); bit > 0; ) {
+        --bit;
+        if (bitwise_and(r, rational::power_of_two(bit)).is_zero()) {
+            v->set(bit, BIT_0);
+        } else {
+            v->set(bit, BIT_1);
+        }
+    }            
+    return v;
+}
+void tbv_manager::deallocate(tbv* bv) {
+#if _DEBUG_MEM
+    if (!allocated_tbvs.contains(bv)) {
+        std::cout << "double deallocate: " << bv << "\n";
+        UNREACHABLE();
+    }
+    std::cout << "deallocate: " << bv << "\n";
+    allocated_tbvs.erase(bv);
+#endif
+    m.deallocate(bv);
+}    
+void tbv_manager::copy(tbv& dst, tbv const& src) const {
+    m.copy(dst, src);
+}    
+tbv& tbv_manager::fill0(tbv& bv) const { 
+    // 10101010 = 2 + 8 + 32 + 128
+    memset(bv.m_data, 2 + 8 + 32 + 128, m.num_bytes());
+    return bv; 
+}
+tbv& tbv_manager::fill1(tbv& bv) const {  
+    // 01010101 = 1 + 4 + 16 + 64
+    memset(bv.m_data, 1 + 4 + 16 + 64, m.num_bytes());
+    return bv; 
+}
+tbv& tbv_manager::fillX(tbv& bv) const { 
+    m.fill1(bv); 
+    return bv; 
+}
+
+tbv& tbv_manager::set_or(tbv& dst,  tbv const& src) const {
+    m.set_or(dst, src); 
+    return dst;
+}
+bool tbv_manager::set_and(tbv& dst,  tbv const& src) const {
+    m.set_and(dst, src); 
+    return is_well_formed(dst);
+}
+
+bool tbv_manager::is_well_formed(tbv const& dst) const {
+    for (unsigned i = 0; i < num_tbits(); ++i) {
+        if (dst[i] == BIT_z) return false;
+    }
+    return true;
+}
+
+void tbv_manager::complement(tbv const& src, ptr_vector<tbv>& result) {
+    tbv* r;
+    unsigned n = num_tbits();
+    for (unsigned i = 0; i < n; ++i) {
+        switch (src.get(i)) {
+        case BIT_0:
+            r = allocate(src);
+            r->set(i, BIT_1);
+            result.push_back(r);
+            break;
+        case BIT_1:
+            r = allocate(src);
+            r->set(i, BIT_0);
+            result.push_back(r);
+            break;
+        default:
+            break;
+        }
+    }
+}
+
+bool tbv_manager::equals(tbv const& a, tbv const& b) const {
+    return m.equals(a, b);
+}
+unsigned tbv_manager::hash(tbv const& src) const {
+    return m.hash(src);
+}
+bool tbv_manager::contains(tbv const& a, tbv const& b) const {
+    return m.contains(a, b);
+}
+bool tbv_manager::intersect(tbv const& a, tbv const& b, tbv& result) {
+    copy(result, a);
+    return set_and(result, b);
+}
+
+std::ostream& tbv_manager::display(std::ostream& out, tbv const& b) const {
+    for (unsigned i = 0; i < num_tbits(); ++i) {
+        switch (b.get(i)) {
+        case BIT_0:
+            out << '0';
+            break;
+        case BIT_1:
+            out << '1';
+            break;
+        case BIT_x:
+            out << 'x';
+            break;
+        case BIT_z:
+            out << 'z';
+            break;
+        default:
+            UNREACHABLE();
+        }
+    }
+    return out;
+}

src/muz/rel/tbv.h

@@ -0,0 +1,140 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    tbv.h
+
+Abstract:
+
+    ternary bit-vector utilities.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2014-09-15
+
+Revision History:
+
+
+--*/
+
+#ifndef _TBV_H_
+#define _TBV_H_
+
+#include "fixed_bit_vector.h"
+#include "rational.h"
+
+class tbv;
+
+enum tbit {
+    BIT_z = 0x0,
+    BIT_0 = 0x1,
+    BIT_1 = 0x2,
+    BIT_x = 0x3
+};
+
+inline tbit neg(tbit t) {
+    return (tbit)(t ^ 0x3);
+}
+
+class tbv_manager {
+    friend class tbv;
+    fixed_bit_vector_manager m;
+    ptr_vector<tbv> allocated_tbvs;
+public:
+    tbv_manager(unsigned n): m(2*n) {}
+    ~tbv_manager();
+    void reset();
+    tbv* allocate();
+    tbv* allocate1();
+    tbv* allocate0();
+    tbv* allocateX();
+    tbv* allocate(tbv const& bv);
+    tbv* allocate(uint64 n);
+    tbv* allocate(rational const& r);
+    tbv* allocate(uint64 n, unsigned hi, unsigned lo);
+    tbv* allocate(tbv const& bv, unsigned const* permutation);
+
+    void deallocate(tbv* bv);
+        
+    void copy(tbv& dst, tbv const& src) const;
+    unsigned num_tbits() const { return m.num_bits()/2; }
+    tbv& reset(tbv& bv) const { return fill0(bv); }
+    tbv& fill0(tbv& bv) const;
+    tbv& fill1(tbv& bv) const;
+    tbv& fillX(tbv& bv) const;
+    bool set_and(tbv& dst,  tbv const& src) const;
+    tbv& set_or(tbv& dst,  tbv const& src) const;
+    void complement(tbv const& src, ptr_vector<tbv>& result);
+    bool equals(tbv const& a, tbv const& b) const;
+    unsigned hash(tbv const& src) const;
+    bool contains(tbv const& a, tbv const& b) const;
+    bool intersect(tbv const& a, tbv const& b, tbv& result);
+    std::ostream& display(std::ostream& out, tbv const& b) const;
+    tbv* project(unsigned n, bool const* to_delete, tbv const& src);
+    bool is_well_formed(tbv const& b) const; // - does not contain BIT_z;
+};
+
+class tbv: private fixed_bit_vector {
+    friend class fixed_bit_vector_manager;
+    friend class tbv_manager;
+
+public:
+
+    struct eq {
+        tbv_manager& m;
+        eq(tbv_manager& m):m(m) {}
+        bool operator()(tbv const& d1, tbv const& d2) const {
+            return m.equals(d1, d2);
+        }
+    };
+
+    struct hash {
+        tbv_manager& m;
+        hash(tbv_manager& m):m(m) {}
+        unsigned operator()(tbv const& d) const {
+            return m.hash(d);
+        }
+    };
+        
+    void set(uint64 n, unsigned hi, unsigned lo);
+    void set(rational const& r, unsigned hi, unsigned lo);
+    void set(tbv const& other, unsigned hi, unsigned lo);
+
+    tbit operator[](unsigned idx) const { return (tbit)get(idx); }
+    void set(unsigned index, tbit value) {
+        SASSERT(value <= 3);
+        fixed_bit_vector::set(2*index,   (value & 2) != 0);
+        fixed_bit_vector::set(2*index+1, (value & 1) != 0);
+    }
+
+
+private:
+
+    unsigned get(unsigned index) const {
+        index *= 2;
+        return (fixed_bit_vector::get(index) << 1) | (unsigned)fixed_bit_vector::get(index+1);
+    }
+};
+
+class tbv_ref {
+    tbv_manager& mgr;
+    tbv* d;
+public:
+    tbv_ref(tbv_manager& mgr):mgr(mgr),d(0) {}
+    tbv_ref(tbv_manager& mgr, tbv* d):mgr(mgr),d(d) {}
+    ~tbv_ref() {
+        if (d) mgr.deallocate(d);
+    }
+    tbv_ref& operator=(tbv* d2) {
+        if (d) mgr.deallocate(d);
+        d = d2;
+        return *this;
+    }
+    tbv& operator*() { return *d; }
+    tbv* get() { return d; }
+    tbv* detach() { tbv* result = d; d = 0; return result; }
+};
+
+
+#endif /* _TBV_H_ */

src/muz/rel/udoc_relation.cpp

@@ -0,0 +1,893 @@
+#include "udoc_relation.h"
+#include "dl_relation_manager.h"
+#include "qe_util.h"
+#include "ast_util.h"
+
+namespace datalog {
+
+    udoc_relation::udoc_relation(udoc_plugin& p, relation_signature const& sig):
+        relation_base(p, sig),
+        dm(p.dm(p.num_signature_bits(sig))) {
+        unsigned column = 0;
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            m_column_info.push_back(column);
+            column += p.num_sort_bits(sig[i]);
+        }
+        m_column_info.push_back(column);
+    }
+    udoc_relation::~udoc_relation() {
+        reset();
+    }
+    void udoc_relation::reset() {
+        m_elems.reset(dm);
+    }
+    void udoc_relation::expand_column_vector(unsigned_vector& v, udoc_relation* 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);
+            }
+        }
+    }
+
+    doc* udoc_relation::fact2doc(const relation_fact & f) const {
+        doc* d = dm.allocate0();
+        for (unsigned i = 0; i < f.size(); ++i) {
+            unsigned bv_size;
+            rational val;
+            VERIFY(get_plugin().is_numeral(f[i], val, bv_size));
+            SASSERT(bv_size == column_num_bits(i));
+            unsigned lo = column_idx(i);
+            unsigned hi = column_idx(i + 1);
+            d->pos().set(val, hi, lo);
+        }
+        return d;
+    }
+    void udoc_relation::add_fact(const relation_fact & f) {
+        doc* d = fact2doc(f);
+        m_elems.insert(dm, d);
+    }
+    bool udoc_relation::contains_fact(const relation_fact & f) const {
+        doc_ref d(dm, fact2doc(f));
+        return m_elems.contains(dm, *d);
+    }
+    udoc_relation * udoc_relation::clone() const {
+        udoc_relation* result = udoc_plugin::get(get_plugin().mk_empty(get_signature()));
+        for (unsigned i = 0; i < m_elems.size(); ++i) {
+            result->m_elems.push_back(dm.allocate(m_elems[i]));
+        }
+        return result;
+    }
+    udoc_relation * udoc_relation::complement(func_decl* f) const {
+        udoc_relation* result = udoc_plugin::get(get_plugin().mk_empty(get_signature()));
+        m_elems.complement(dm, result->m_elems);
+        return result;
+    }
+    void udoc_relation::to_formula(expr_ref& fml) const {
+        ast_manager& m = fml.get_manager();
+        expr_ref_vector disj(m);
+        for (unsigned i = 0; i < m_elems.size(); ++i) {
+            disj.push_back(to_formula(m_elems[i]));
+        }
+        fml = mk_or(m, disj.size(), disj.c_ptr());
+    }
+    expr_ref udoc_relation::to_formula(doc const& d) const {
+        ast_manager& m = get_plugin().get_ast_manager();
+        expr_ref result(m);
+        expr_ref_vector conjs(m);
+        conjs.push_back(to_formula(d.pos()));
+        for (unsigned i = 0; i < d.neg().size(); ++i) {
+            conjs.push_back(m.mk_not(to_formula(d.neg()[i])));
+        }
+        result = mk_and(m, conjs.size(), conjs.c_ptr());
+        return result;
+    }
+    expr_ref udoc_relation::to_formula(tbv const& t) const {
+        udoc_plugin& p = get_plugin();
+        ast_manager& m = p.get_ast_manager();
+        expr_ref result(m);
+        expr_ref_vector conjs(m);
+        for (unsigned i = 0; i < get_num_cols(); ++i) {
+            var_ref v(m);
+            v = m.mk_var(i, get_signature()[i]);
+            unsigned lo = column_idx(i);
+            unsigned hi = column_idx(i+1);
+            rational r(0);
+            unsigned lo0 = lo;
+            bool is_x = true;
+            for (unsigned j = lo; j < hi; ++j) {
+                switch(t[j]) {
+                case BIT_0:
+                    if (is_x) is_x = false, lo0 = j, r.reset();
+                    break;
+                case BIT_1:
+                    if (is_x) is_x = false, lo0 = j, r.reset();
+                    r += rational::power_of_two(j - lo0);
+                    break;
+                case BIT_x:
+                    if (!is_x) {
+                        conjs.push_back(m.mk_eq(p.bv.mk_extract(j-1,lo0,v),
+                                                p.bv.mk_numeral(r,j-lo0)));
+                    }
+                    is_x = true;
+                    break;
+                default:
+                    UNREACHABLE();
+                }
+            }
+            if (!is_x) {
+                expr_ref num(m);
+                if (lo0 == lo) {
+                    num = p.mk_numeral(r, get_signature()[i]);
+                    conjs.push_back(m.mk_eq(v, num));
+                }
+                else {
+                    num = p.bv.mk_numeral(r, hi-lo0);
+                    conjs.push_back(m.mk_eq(p.bv.mk_extract(hi-1,lo0,v), num));
+                }
+            }
+        }
+        result = mk_and(m, conjs.size(), conjs.c_ptr());
+        return result;
+    }
+
+    udoc_plugin& udoc_relation::get_plugin() const {
+        return static_cast<udoc_plugin&>(relation_base::get_plugin());
+    }
+
+    void udoc_relation::display(std::ostream& out) const {
+        m_elems.display(dm, out);
+    }
+
+    // -------------
+
+    udoc_plugin::udoc_plugin(relation_manager& rm):
+        relation_plugin(udoc_plugin::get_name(), rm),
+        m(rm.get_context().get_manager()),
+        bv(m),
+        dl(m) {
+    }
+    udoc_plugin::~udoc_plugin() {
+        u_map<doc_manager*>::iterator it = m_dms.begin(), end = m_dms.end();
+        for (; it != end; ++it) {
+            dealloc(it->m_value);
+        }
+    }
+    udoc_relation& udoc_plugin::get(relation_base& r) {
+        return dynamic_cast<udoc_relation&>(r);
+    }
+    udoc_relation* udoc_plugin::get(relation_base* r) {
+        return r?dynamic_cast<udoc_relation*>(r):0;
+    }
+    udoc_relation const & udoc_plugin::get(relation_base const& r) {
+        return dynamic_cast<udoc_relation const&>(r);        
+    }
+
+    doc_manager& udoc_plugin::dm(relation_signature const& sig) {
+        return dm(num_signature_bits(sig));
+    }
+
+    doc_manager& udoc_plugin::dm(unsigned n) {
+        doc_manager* r;
+        if (!m_dms.find(n, r)) {
+            r = alloc(doc_manager, n);
+            m_dms.insert(n, r);
+        }
+        return *r;
+    }
+    expr* udoc_plugin::mk_numeral(rational const& r, sort* s) {
+        if (bv.is_bv_sort(s)) {
+            return bv.mk_numeral(r, s);
+        }
+        SASSERT(dl.is_finite_sort(s));
+        return dl.mk_numeral(r.get_uint64(), s);
+    }
+    bool udoc_plugin::is_numeral(expr* e, rational& r, unsigned& num_bits) {
+        if (bv.is_numeral(e, r, num_bits)) return true;
+        uint64 n, sz;
+        ast_manager& m = get_ast_manager();
+        if (dl.is_numeral(e, n) && dl.try_get_size(m.get_sort(e), sz)) {
+            num_bits = 0;
+            while (sz > 0) ++num_bits, sz = sz/2;
+            r = rational(n, rational::ui64());
+            return true;
+        }
+        return false;
+    }
+    unsigned udoc_plugin::num_sort_bits(sort* s) const {
+        unsigned num_bits = 0;
+        if (bv.is_bv_sort(s))
+            return bv.get_bv_size(s);
+        uint64 sz;
+        if (dl.try_get_size(s, sz)) {
+            while (sz > 0) ++num_bits, sz /= 2;
+            return num_bits;
+        }
+        UNREACHABLE();
+        return 0;
+    }
+    unsigned udoc_plugin::num_signature_bits(relation_signature const& sig) { 
+        unsigned result = 0;
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            result += num_sort_bits(sig[i]);
+        }
+        return result;
+    }
+
+    bool udoc_plugin::is_finite_sort(sort* s) const {
+        return bv.is_bv_sort(s) || dl.is_finite_sort(s);
+    }
+
+
+    bool udoc_plugin::can_handle_signature(const relation_signature & sig) {
+        for (unsigned i = 0; i < sig.size(); ++i) {
+            if (!is_finite_sort(sig[i]))
+                return false;
+        }
+        return true;
+    }
+    relation_base * udoc_plugin::mk_empty(const relation_signature & sig) {
+        return alloc(udoc_relation, *this, sig);
+    }
+    relation_base * udoc_plugin::mk_full(func_decl* p, const relation_signature & s) {
+        udoc_relation* r = get(mk_empty(s));
+        r->get_udoc().push_back(dm(s).allocateX());
+        return r;
+    }
+    class udoc_plugin::join_fn : public convenient_relation_join_fn {
+        doc_manager& dm;
+        doc_manager& dm1;
+        doc_manager& dm2;
+    public:
+        join_fn(udoc_plugin& p, udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt,
+                const unsigned * cols1, const unsigned * cols2) 
+            : convenient_relation_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2),
+              dm(p.dm(get_result_signature())),
+              dm1(t1.get_dm()),
+              dm2(t2.get_dm()) {
+            t1.expand_column_vector(m_cols1);
+            t2.expand_column_vector(m_cols2);
+        }
+
+        void join(doc const& d1, doc const& d2, udoc& result) {
+            doc* d = dm.allocateX();
+            tbv& pos = d->pos();
+            utbv& neg = d->neg();
+            unsigned mid = dm1.num_tbits();
+            unsigned hi  = dm.num_tbits();
+            pos.set(d1.pos(), mid-1, 0);
+            pos.set(d2.pos(), hi-1, mid);
+            // first fix bits
+            for (unsigned i = 0; i < m_cols1.size(); ++i) {
+                unsigned idx1 = m_cols1[i];
+                unsigned idx2 = mid + m_cols2[i];
+                tbit v1 = pos[idx1];
+                tbit v2 = pos[idx2];
+
+                if (v1 == BIT_x) {
+                    if (v2 != BIT_x)
+                        pos.set(idx1, v2);
+                } else if (v2 == BIT_x) {
+                    pos.set(idx2, v1);
+                } else if (v1 != v2) {
+                    dm.deallocate(d);
+                    // columns don't match
+                    return;
+                }
+            }
+            // fix equality of don't care columns
+            for (unsigned i = 0; i < m_cols1.size(); ++i) {
+                unsigned idx1 = m_cols1[i];
+                unsigned idx2 = mid + m_cols2[i];
+                unsigned v1 = pos[idx1];
+                unsigned v2 = pos[idx2];
+                
+                if (v1 == BIT_x && v2 == BIT_x) {
+                    // add to subtracted TBVs: 1xx0 and 0xx1
+                    tbv* r = dm.tbvm().allocate(pos);
+                    r->set(idx1, BIT_0);
+                    r->set(idx2, BIT_1);
+                    neg.push_back(r);
+                    
+                    r = dm.tbvm().allocate(pos);
+                    r->set(idx1, BIT_1);
+                    r->set(idx2, BIT_0);
+                    neg.push_back(r);
+                }
+            }
+
+            // handle subtracted TBVs:  1010 -> 1010xxx
+            for (unsigned i = 0; i < d1.neg().size(); ++i) {
+                tbv* t = dm.tbvm().allocate();
+                t->set(d1.neg()[i], mid-1, 0);
+                t->set(d2.pos(), hi - 1, mid);
+                neg.push_back(t);
+            }
+            for (unsigned i = 0; i < d2.neg().size(); ++i) {
+                tbv* t = dm.tbvm().allocate();
+                t->set(d1.pos(), mid-1, 0);
+                t->set(d2.neg()[i], hi - 1, mid);
+                neg.push_back(t);
+            }            
+            result.insert(dm, d);
+        }
+
+        virtual relation_base * operator()(const relation_base & _r1, const relation_base & _r2) {
+            udoc_relation const& r1 = get(_r1);
+            udoc_relation const& r2 = get(_r2);
+            TRACE("dl", r1.display(tout << "r1:\n"); r2.display(tout  << "r2:\n"););
+            udoc_plugin& p = r1.get_plugin();            
+            relation_signature const& sig = get_result_signature();
+            udoc_relation * result = alloc(udoc_relation, p, sig);
+            udoc const& d1 = r1.get_udoc();
+            udoc const& d2 = r2.get_udoc();
+            udoc& r = result->get_udoc();
+            for (unsigned i = 0; i < d1.size(); ++i) {
+                for (unsigned j = 0; j < d2.size(); ++j) {
+                    join(d1[i], d2[j], r);
+                }
+            }
+            TRACE("dl", result->display(tout << "result:\n"););
+            return result;
+        }
+    };
+    relation_join_fn * udoc_plugin::mk_join_fn(
+        const relation_base & t1, const relation_base & t2,
+        unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) {
+        if (!check_kind(t1) || !check_kind(t2)) {
+            return 0;
+        }
+        return alloc(join_fn, *this, get(t1), get(t2), col_cnt, cols1, cols2);
+    }
+    class udoc_plugin::project_fn : public convenient_relation_project_fn {
+        svector<bool> m_to_delete;
+    public:
+        project_fn(udoc_relation const & t, unsigned removed_col_cnt, const unsigned * removed_cols) 
+            : convenient_relation_project_fn(t.get_signature(), removed_col_cnt, removed_cols) {
+            t.expand_column_vector(m_removed_cols);
+            unsigned n = t.get_dm().num_tbits();
+            m_to_delete.resize(n, false);
+            for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
+                m_to_delete[m_removed_cols[i]] = true;
+            }
+        }
+
+        virtual relation_base * operator()(const relation_base & tb) {
+            TRACE("dl", tb.display(tout << "src:\n"););
+            udoc_relation const& t = get(tb);
+            udoc_plugin& p = t.get_plugin();
+            udoc_relation* r = udoc_plugin::get(p.mk_empty(get_result_signature()));
+            doc_manager& dm1 = t.get_dm();
+            doc_manager& dm2 = r->get_dm();
+            doc_ref d2(dm2);
+            udoc const& ud1 = t.get_udoc();
+            udoc& ud2 = r->get_udoc();
+            for (unsigned i = 0; i < ud1.size(); ++i) {
+                d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), ud1[i]);
+                ud2.push_back(d2.detach());
+            }
+            TRACE("dl", tout << "final size: " << r->get_size_estimate_rows() << '\n';);
+            return r;
+        }
+    };
+    
+
+    relation_transformer_fn * udoc_plugin::mk_project_fn(
+        const relation_base & t, unsigned col_cnt, 
+        const unsigned * removed_cols) {
+        if (!check_kind(t))
+            return 0;
+        return alloc(project_fn, get(t), col_cnt, removed_cols);
+    }
+
+    class udoc_plugin::rename_fn : public convenient_relation_rename_fn {
+        unsigned_vector m_permutation;
+    public:
+        rename_fn(udoc_relation const& t, unsigned cycle_len, const unsigned * cycle) 
+            : convenient_relation_rename_fn(t.get_signature(), cycle_len, cycle) {
+            udoc_plugin& p = t.get_plugin();
+            for (unsigned i = 0; i < t.get_num_bits(); ++i) {
+                m_permutation.push_back(i);
+            }
+            unsigned len = t.column_num_bits(cycle[0]);
+            for (unsigned i = 0; i < cycle_len; ++i) {
+                unsigned j = (i + 1)%cycle_len;
+                unsigned col1 = cycle[i];
+                unsigned col2 = cycle[j];
+                unsigned lo1 = t.column_idx(col1);
+                unsigned lo2 = t.column_idx(col2);
+                for (unsigned k = 0; k < len; ++k) {
+                    m_permutation[k + lo1] = k + lo2;
+                }
+                SASSERT(t.column_num_bits(col1) == t.column_num_bits(col2));
+            }
+        }
+
+        virtual relation_base * operator()(const relation_base & _r) {
+            udoc_relation const& r = get(_r);
+            TRACE("dl", r.display(tout << "r:\n"););
+            udoc_plugin& p = r.get_plugin();            
+            relation_signature const& sig = get_result_signature();
+            udoc_relation* result = alloc(udoc_relation, p, sig);
+            udoc const& src = r.get_udoc();
+            udoc& dst = result->get_udoc();
+            doc_manager& dm = r.get_dm();
+            for (unsigned i = 0; i < src.size(); ++i) {
+                dst.push_back(dm.allocate(src[i], m_permutation.c_ptr()));
+            }
+            TRACE("dl", result->display(tout << "result:\n"););
+            return result;
+        }
+    };
+    relation_transformer_fn * udoc_plugin::mk_rename_fn(
+        const relation_base & r, 
+        unsigned cycle_len, const unsigned * permutation_cycle) {
+        if (check_kind(r)) {
+            return alloc(rename_fn, get(r), cycle_len, permutation_cycle);
+        }
+        else {
+            return 0;
+        }
+    }
+    class udoc_plugin::union_fn : public relation_union_fn {
+    public:
+        union_fn() {}
+
+        virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) {
+            TRACE("dl", _r.display(tout << "dst:\n"); _src.display(tout  << "src:\n"););
+            udoc_relation& r = get(_r);
+            udoc_relation const& src = get(_src);
+            udoc_relation* d = get(_delta);
+            doc_manager& dm = r.get_dm();
+            udoc* d1 = 0;
+            if (d) d1 = &d->get_udoc();
+            if (d1) d1->reset(dm);
+            r.get_plugin().mk_union(dm, r.get_udoc(), src.get_udoc(), d1);
+            TRACE("dl", _r.display(tout << "dst':\n"););
+        }
+    };
+    void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) {
+        for (unsigned i = 0; i < src.size(); ++i) {
+            doc* d = dm.allocate(src[i]);
+            if (dst.insert(dm, d)) {
+                if (delta) {
+                    delta->insert(dm, dm.allocate(src[i]));
+                }
+            } 
+        }
+    }
+    relation_union_fn * udoc_plugin::mk_union_fn(
+        const relation_base & tgt, const relation_base & src, 
+        const relation_base * delta) {
+        if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
+            return 0;
+        }
+        return alloc(union_fn);
+    }
+    relation_union_fn * udoc_plugin::mk_widen_fn(
+        const relation_base & tgt, const relation_base & src, 
+        const relation_base * delta) {
+        return mk_union_fn(tgt, src, delta);
+    }
+
+    class udoc_plugin::filter_identical_fn : public relation_mutator_fn {
+        unsigned_vector        m_cols;
+        unsigned               m_size;
+        bit_vector             m_empty_bv;
+        union_find_default_ctx union_ctx;
+        union_find<>           m_equalities;
+    public:
+        filter_identical_fn(const relation_base & _r, unsigned col_cnt, const unsigned *identical_cols)
+            : m_cols(col_cnt), m_equalities(union_ctx) {
+            udoc_relation const& r = get(_r);
+            doc_manager& dm = r.get_dm();
+            unsigned num_bits = dm.num_tbits();
+            m_size = r.column_num_bits(identical_cols[0]);
+            m_empty_bv.resize(r.get_num_bits(), false);            
+            for (unsigned i = 0; i < col_cnt; ++i) {
+                m_cols[i] = r.column_idx(identical_cols[i]);
+            }            
+            for (unsigned i = 0, e = m_empty_bv.size(); i < e; ++i) {
+                m_equalities.mk_var();
+            }
+            for (unsigned i = 1; i < col_cnt; ++i) {
+                for (unsigned j = 0; j < m_size; ++j) {
+                    m_equalities.merge(m_cols[0]+j ,m_cols[i]+j);
+                }
+            }
+        }
+        
+        virtual void operator()(relation_base & _r) {
+            udoc_relation& r = get(_r);
+            udoc& d = r.get_udoc();
+            doc_manager& dm = r.get_dm();
+            d.merge(dm, m_cols[0], m_size, m_equalities, m_empty_bv);
+            TRACE("dl", tout << "final size: " << r.get_size_estimate_rows() << '\n';);
+        }
+    };
+    relation_mutator_fn * udoc_plugin::mk_filter_identical_fn(
+        const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) {
+        return check_kind(t)?alloc(filter_identical_fn, t, col_cnt, identical_cols):0;
+    }
+    class udoc_plugin::filter_equal_fn : public relation_mutator_fn {
+        doc_manager& dm;
+        doc*         m_filter;
+    public:
+        filter_equal_fn(udoc_plugin& p, const udoc_relation & t, const relation_element val, unsigned col):
+            dm(p.dm(t.get_signature())) {
+            rational r;
+            unsigned num_bits;
+            VERIFY(p.is_numeral(val, r, num_bits));
+            m_filter = dm.allocateX();
+            unsigned lo = t.column_idx(col);
+            unsigned hi = t.column_idx(col+1);
+            SASSERT(num_bits == hi - lo);
+            m_filter->pos().set(r, hi-1, lo);
+        }
+        virtual ~filter_equal_fn() {
+            dm.deallocate(m_filter);
+        }        
+        virtual void operator()(relation_base & tb) {
+            udoc_relation & t = get(tb);
+            t.get_udoc().intersect(dm, *m_filter);
+        }
+    };
+    relation_mutator_fn * udoc_plugin::mk_filter_equal_fn(
+        const relation_base & t, const relation_element & value, unsigned col) {
+        if (!check_kind(t))
+            return 0;
+        return alloc(filter_equal_fn, *this, get(t), value, col);
+    }
+
+    bool udoc_relation::is_guard(unsigned n, expr* const* gs) const {
+        for (unsigned i = 0; i < n; ++i) {
+            if (!is_guard(gs[i])) return false;
+        }
+        return true;
+    }
+    bool udoc_relation::is_guard(expr* g) const {
+        udoc_plugin& p = get_plugin();
+        ast_manager& m = p.get_ast_manager();
+        bv_util& bv = p.bv;
+        expr* e1, *e2, *e3;
+        unsigned hi, lo;
+        if (m.is_and(g) || m.is_or(g) || m.is_not(g) || m.is_true(g) || m.is_false(g)) {
+            return is_guard(to_app(g)->get_num_args(), to_app(g)->get_args());
+        }
+        if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
+            if (is_var(e1) && is_ground(e2)) return true;
+            if (is_var(e2) && is_ground(e1)) return true;
+            if (bv.is_extract(e1, lo, hi, e3) && is_var(e3) && is_ground(e2)) return true;
+            if (bv.is_extract(e2, lo, hi, e3) && is_var(e3) && is_ground(e1)) return true;
+        }
+        if (is_var(g)) {
+            return true;
+        }
+        return false;
+    }
+
+    void udoc_relation::extract_guard(expr* cond, expr_ref& guard, expr_ref& rest) const {
+        rest.reset();
+        ast_manager& m = get_plugin().get_ast_manager();
+        expr_ref_vector conds(m), guards(m), rests(m);
+        conds.push_back(cond);
+        qe::flatten_and(conds);
+        for (unsigned i = 0; i < conds.size(); ++i) {
+            expr* g = conds[i].get();
+            if (is_guard(g)) {
+                guards.push_back(g);
+            }
+            else {
+                rests.push_back(g);
+            }
+        }
+        guard = mk_and(m, guards.size(), guards.c_ptr());
+        rest  = mk_and(m, rests.size(),  rests.c_ptr());        
+    }
+    void udoc_relation::compile_guard(expr* g, udoc& d, bit_vector const& discard_cols) const {
+        d.reset(dm);
+        d.push_back(dm.allocateX()); 
+        apply_guard(g, d, discard_cols);
+    }
+    void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const {
+        // datastructure to store equalities with columns that will be projected out
+        union_find_default_ctx union_ctx;
+        subset_ints equalities(union_ctx);
+        for (unsigned i = 0, e = discard_cols.size(); i < e; ++i) {
+            equalities.mk_var();
+        }        
+        apply_guard(g, result, equalities, discard_cols);
+    }
+    bool udoc_relation::apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c) const {
+        udoc_plugin& p = get_plugin();
+        unsigned num_bits;
+        rational r;
+        unsigned idx = v->get_idx();
+        unsigned col = column_idx(idx);
+        lo += col;
+        hi += col;
+        if (p.is_numeral(c, r, num_bits)) {
+            doc_ref d(dm, dm.allocateX());
+            d->pos().set(r, hi, lo);
+            result.intersect(dm, *d);
+            return true;
+        }
+        // other cases?
+        return false;
+    }
+
+    void udoc_relation::apply_guard(
+        expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols) const {
+        ast_manager& m = get_plugin().get_ast_manager();
+        bv_util& bv = get_plugin().bv;
+        expr* e1, *e2;
+        if (result.is_empty()) {
+        }
+        else if (m.is_and(g)) {
+            for (unsigned i = 0; !result.is_empty() && i < to_app(g)->get_num_args(); ++i) {
+                apply_guard(to_app(g)->get_arg(i), result, equalities, discard_cols);
+            }
+        }
+        else if (m.is_not(g, e1)) {
+            // REVIEW: (not (= x y)) should not cause 
+            // the equivalence class to collapse.
+            // It seems the current organization with fix_eq_bits
+            // will merge the equivalence class as a side-effect.
+            udoc sub;
+            sub.push_back(dm.allocateX());
+            apply_guard(e1, sub, equalities, discard_cols);
+            result.subtract(dm, sub);
+        }
+        else if (m.is_or(g)) {
+            udoc sub;
+            sub.push_back(dm.allocateX());
+            for (unsigned i = 0; !sub.is_empty() && i < to_app(g)->get_num_args(); ++i) {
+                expr_ref arg(m);
+                arg = mk_not(m, to_app(g)->get_arg(i));
+                apply_guard(arg, result, equalities, discard_cols);
+            }
+            result.subtract(dm, sub);
+        }
+        else if (m.is_true(g)) {
+        }
+        else if (m.is_false(g)) {
+            result.reset(dm);
+        }
+        else if (is_var(g)) {
+            SASSERT(m.is_bool(g));
+            unsigned v = to_var(g)->get_idx();
+            unsigned idx = column_idx(v);
+            doc_ref d(dm);
+            d = dm.allocateX();
+            dm.set(*d, idx, BIT_1);
+            result.intersect(dm, *d);
+        }
+        else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
+            unsigned hi, lo;
+            expr* e3;
+            if (is_var(e1) && is_ground(e2) && 
+                apply_eq(g, result, to_var(e1), bv.get_bv_size(e1)-1, 0, e2)) {
+            }
+            else if (is_var(e2) && is_ground(e1) &&
+                     apply_eq(g, result, to_var(e2), bv.get_bv_size(e2)-1, 0, e1)) {
+            }
+            else if (bv.is_extract(e1, lo, hi, e3) && is_var(e3) && is_ground(e2) &&
+                     apply_eq(g, result, to_var(e3), hi, lo, e2)) {
+            }
+            else if (bv.is_extract(e2, lo, hi, e3) && is_var(e3) && is_ground(e1) &&
+                     apply_eq(g, result, to_var(e3), hi, lo, e1)) {
+            }
+            else if (is_var(e1) && is_var(e2)) {
+                var* v1 = to_var(e1);
+                var* v2 = to_var(e2);
+                unsigned idx1 = column_idx(v1->get_idx());
+                unsigned idx2 = column_idx(v2->get_idx());
+                unsigned length = column_num_bits(v1->get_idx());
+                result.merge(dm, idx1, idx2, length, discard_cols);
+            }   
+            else {
+                goto failure_case;
+            }            
+        }
+        else {
+        failure_case:
+            std::ostringstream strm;
+            strm << "Guard expression is not handled" << mk_pp(g, m);
+            throw default_exception(strm.str()); 
+        }
+    }
+
+    class udoc_plugin::filter_interpreted_fn : public relation_mutator_fn {
+        doc_manager& dm;
+        expr_ref     m_condition;
+        udoc         m_udoc;
+        bit_vector   m_empty_bv;
+    public:
+        filter_interpreted_fn(const udoc_relation & t, ast_manager& m, app *condition) :
+            dm(t.get_dm()),
+            m_condition(m) {
+            m_empty_bv.resize(t.get_num_bits(), false);
+            expr_ref guard(m), rest(m);
+            t.extract_guard(condition, guard, m_condition);            
+            t.compile_guard(guard, m_udoc, m_empty_bv);
+            if (m.is_true(m_condition)) {
+                m_condition = 0;
+            }
+            TRACE("dl", 
+                  tout << "condition: " << mk_pp(condition, m) << "\n";
+                  tout << m_condition << "\n"; m_udoc.display(dm, tout) << "\n";);
+        }
+
+        virtual ~filter_interpreted_fn() {
+            m_udoc.reset(dm);
+        }
+        
+        virtual void operator()(relation_base & tb) {
+            udoc_relation & t = get(tb);
+            udoc& u = t.get_udoc();
+            u.intersect(dm, m_udoc);
+            if (m_condition && !u.is_empty()) {
+                t.apply_guard(m_condition, u, m_empty_bv);
+            }
+            TRACE("dl", tout << "final size: " << t.get_size_estimate_rows() << '\n';);
+        }
+    };
+    relation_mutator_fn * udoc_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) {
+        return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):0;
+    }
+
+    class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn {
+        const unsigned_vector m_t_cols;
+        const unsigned_vector m_neg_cols;
+    public:
+        negation_filter_fn(const udoc_relation & r, const udoc_relation & neg, unsigned joined_col_cnt,
+                           const unsigned *t_cols, const unsigned *neg_cols)
+            : m_t_cols(joined_col_cnt, t_cols), m_neg_cols(joined_col_cnt, neg_cols) {
+            SASSERT(joined_col_cnt > 0);
+        }
+        
+        virtual void operator()(relation_base& tb, const relation_base& negb) {
+            udoc_relation& t = get(tb);
+            udoc_relation const& n = get(negb);
+            udoc & dst = t.get_udoc();
+            udoc const & neg = n.get_udoc();
+            doc_manager& dm = t.get_dm();
+            udoc result;
+            for (unsigned i = 0; i < dst.size(); ++i) {
+                bool done_i = false;
+                for (unsigned j = 0; !done_i && j < neg.size(); ++j) {
+                    bool done_j = false;
+                    for (unsigned c = 0; !done_i && !done_j && c < m_t_cols.size(); ++c) {
+                        unsigned t_col = m_t_cols[c];
+                        unsigned n_col = m_neg_cols[c];
+                        unsigned num_bits = t.column_num_bits(t_col);
+                        SASSERT(num_bits == n.column_num_bits(n_col));
+                        unsigned t_idx = t.column_idx(t_col);
+                        unsigned n_idx = n.column_idx(n_col);
+                        for (unsigned k = 0; !done_j && k < num_bits; ++k) {
+                            tbit n_bit = neg[j][n_idx + k];
+                            tbit d_bit = dst[i][t_idx + k];
+                            // neg does not contain dst.
+                            done_j = (n_bit != BIT_x && n_bit != d_bit);
+                        }
+                    }
+                    if (done_j) {
+                        result.push_back(&dst[i]);
+                    }
+                    else {
+                        dm.deallocate(&dst[i]);
+                        done_i = true;
+                    }
+                }
+            }
+            std::swap(dst, result);
+            if (dst.is_empty()) {
+                return;
+            }
+
+            // slow case
+            udoc renamed_neg;
+            for (unsigned i = 0; i < neg.size(); ++i) {
+                doc_ref newD(dm, dm.allocateX());
+                for (unsigned j = 0; j < m_neg_cols.size(); ++j) {
+                    copy_column(*newD, neg[i], m_t_cols[j], m_neg_cols[j], t, n);
+                }
+                renamed_neg.push_back(newD.detach());
+            }
+            dst.subtract(t.get_dm(), renamed_neg);
+        }
+        void copy_column(
+            doc& dst, doc const& src,
+            unsigned col_dst, unsigned col_src, 
+            udoc_relation const& dstt,
+            udoc_relation const& srct) {
+            doc_manager& dm = dstt.get_dm();
+            unsigned idx_dst = dstt.column_idx(col_dst);
+            unsigned idx_src = srct.column_idx(col_src);
+            unsigned num_bits = dstt.column_num_bits(col_dst);
+            SASSERT(num_bits == srct.column_num_bits(col_src));
+            for (unsigned i = 0; i < num_bits; ++i) {
+                dm.set(dst, idx_dst+i, src[idx_src+i]);
+            }            
+        }
+    };
+
+    relation_intersection_filter_fn * udoc_plugin::mk_filter_by_negation_fn(
+        const relation_base& t,
+        const relation_base& neg, unsigned joined_col_cnt, const unsigned *t_cols,
+        const unsigned *negated_cols) {
+        if (!check_kind(t) || !check_kind(neg))
+            return 0;
+        return alloc(negation_filter_fn, get(t), get(neg), joined_col_cnt, t_cols, negated_cols);
+    }
+
+    class udoc_plugin::filter_proj_fn : public convenient_relation_project_fn {
+        doc_manager& dm;
+        expr_ref     m_condition;
+        udoc         m_udoc;
+        bit_vector   m_col_list; // map: col idx -> bool (whether the column is to be removed)
+        svector<bool> m_to_delete; // same
+    public:
+        filter_proj_fn(const udoc_relation & t, ast_manager& m, app *condition,
+                       unsigned col_cnt, const unsigned * removed_cols) :
+            convenient_relation_project_fn(t.get_signature(), col_cnt, removed_cols),
+            dm(t.get_dm()),
+            m_condition(m) {
+            t.expand_column_vector(m_removed_cols);
+            m_col_list.resize(t.get_num_bits(), false);
+            for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
+                m_col_list.set(m_removed_cols[i], true);
+            }
+            m_to_delete.resize(m_removed_cols.size(), false);
+            for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
+                m_to_delete[m_removed_cols[i]] = true;
+            }
+            expr_ref guard(m), rest(m);
+            t.extract_guard(condition, guard, m_condition);            
+            t.compile_guard(guard, m_udoc, m_col_list);
+            if (m.is_true(m_condition)) {
+                m_condition = 0;
+            }
+        }
+        
+        virtual ~filter_proj_fn() {
+            m_udoc.reset(dm);
+        }
+        virtual relation_base* operator()(const relation_base & tb) {
+            udoc_relation const & t = get(tb);
+            udoc const& u1 = t.get_udoc();
+            doc_manager& dm = t.get_dm();
+            udoc  u2;
+            u2.copy(dm, u1);
+            u2.intersect(dm, m_udoc);
+            if (m_condition && !u2.is_empty()) {
+                t.apply_guard(m_condition, u2, m_col_list);
+            }
+            udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature()));
+            doc_manager& dm2 = r->get_dm();
+            for (unsigned i = 0; i < u2.size(); ++i) {
+                doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), u2[i]);
+                r->get_udoc().insert(dm2, d);
+            }
+            u2.reset(dm);
+            return r;
+        }
+    };
+    relation_transformer_fn * udoc_plugin::mk_filter_interpreted_and_project_fn(
+        const relation_base & t, app * condition,
+        unsigned removed_col_cnt, const unsigned * removed_cols) {
+        return check_kind(t)?alloc(filter_proj_fn, get(t), get_ast_manager(), condition, removed_col_cnt, removed_cols):0;
+    }
+
+
+}

src/muz/rel/udoc_relation.h

@@ -0,0 +1,135 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    udoc_relation.h
+
+Abstract:
+
+    Relation based on union of DOCs.
+
+Author:
+
+    Nuno Lopes (a-nlopes) 2013-03-01
+    Nikolaj Bjorner (nbjorner) 2014-09-15
+
+Revision History:
+
+
+--*/
+
+#ifndef _UDOC_RELATION_H_
+#define _UDOC_RELATION_H_
+
+#include "doc.h"
+#include "dl_base.h"
+
+namespace datalog {
+    class udoc_plugin;
+    class udoc_relation;
+    
+    class udoc_relation : public relation_base {
+        friend class udoc_plugin;
+        doc_manager&    dm;
+        udoc            m_elems;
+        unsigned_vector m_column_info;
+        doc* fact2doc(relation_fact const& f) const;        
+        expr_ref to_formula(tbv const& t) const;
+        expr_ref to_formula(doc const& d) const;
+    public:
+        udoc_relation(udoc_plugin& p, relation_signature const& s);
+        virtual ~udoc_relation();
+        virtual void reset();
+        virtual void add_fact(const relation_fact & f);
+        virtual bool contains_fact(const relation_fact & f) const;
+        virtual udoc_relation * clone() const;
+        virtual udoc_relation * complement(func_decl*) const;
+        virtual void to_formula(expr_ref& fml) const;
+        udoc_plugin& get_plugin() const; 
+        virtual bool empty() const { return m_elems.is_empty(); }
+        virtual void display(std::ostream& out) const;
+        virtual bool is_precise() const { return true; }
+        virtual unsigned get_size_estimate_rows() const { return m_elems.size(); }
+
+        doc_manager& get_dm() const { return dm; }
+        udoc const& get_udoc() const { return m_elems; }
+        udoc& get_udoc() { return m_elems; }
+        unsigned get_num_records() const { return m_elems.size(); }
+        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, udoc_relation* other = 0) const;
+        void extract_guard(expr* condition, expr_ref& guard, expr_ref& rest) const;
+        bool is_guard(expr* g) const;
+        bool is_guard(unsigned n, expr* const *g) const;
+        void compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
+        void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
+        void apply_guard(expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols) const;
+        bool apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c) const;
+    };
+
+    class udoc_plugin : public relation_plugin {
+        friend class udoc_relation;
+        class join_fn;
+        class project_fn;
+        class union_fn;
+        class rename_fn;
+        class filter_equal_fn;
+        class filter_identical_fn;
+        class filter_interpreted_fn;
+        class filter_by_negation_fn;        
+        class filter_by_union_fn;
+        class filter_proj_fn;
+        class negation_filter_fn;
+        ast_manager& m;
+        bv_util      bv;
+        dl_decl_util dl;
+        u_map<doc_manager*> m_dms;
+        doc_manager& dm(unsigned sz);
+        doc_manager& dm(relation_signature const& sig);
+        static udoc_relation& get(relation_base& r);
+        static udoc_relation* get(relation_base* r);
+        static udoc_relation const & get(relation_base const& r);   
+        void mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta);
+        bool is_numeral(expr* e, rational& r, unsigned& num_bits);
+        unsigned num_sort_bits(expr* e) const { return num_sort_bits(get_ast_manager().get_sort(e)); }
+        unsigned num_sort_bits(sort* s) const;
+        bool     is_finite_sort(sort* s) const;
+        unsigned num_signature_bits(relation_signature const& sig);
+        expr* mk_numeral(rational const& r, sort* s);
+    public:
+        udoc_plugin(relation_manager& rm);
+        ~udoc_plugin();
+        virtual bool can_handle_signature(const relation_signature & s);
+        static symbol get_name() { return symbol("doc"); }
+        virtual relation_base * mk_empty(const relation_signature & s);
+        virtual relation_base * mk_full(func_decl* p, const relation_signature & s);
+        virtual relation_join_fn * mk_join_fn(const relation_base & t1, const relation_base & t2,
+            unsigned col_cnt, const unsigned * cols1, const unsigned * cols2);
+        virtual relation_transformer_fn * mk_project_fn(const relation_base & t, unsigned col_cnt, 
+            const unsigned * removed_cols);
+        virtual relation_transformer_fn * mk_rename_fn(const relation_base & t, unsigned permutation_cycle_len, 
+            const unsigned * permutation_cycle);
+        virtual relation_union_fn * mk_union_fn(const relation_base & tgt, const relation_base & src, 
+            const relation_base * delta);
+        virtual relation_union_fn * mk_widen_fn(const relation_base & tgt, const relation_base & src, 
+            const relation_base * delta);
+        virtual relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, 
+            const unsigned * identical_cols);
+        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_intersection_filter_fn * mk_filter_by_negation_fn(
+            const relation_base& t,
+            const relation_base& neg, unsigned joined_col_cnt, const unsigned *t_cols,
+            const unsigned *negated_cols);
+        virtual relation_transformer_fn * mk_filter_interpreted_and_project_fn(
+            const relation_base & t, app * condition,
+            unsigned removed_col_cnt, const unsigned * removed_cols);
+    };
+};
+       
+#endif /* _UDOC_RELATION_H_ */
+