diff --git a/src/muz/ddnf/tbv.cpp b/src/muz/ddnf/tbv.cpp
new file mode 100644
index 000000000..f96a7078b
--- /dev/null
+++ b/src/muz/ddnf/tbv.cpp
@@ -0,0 +1,141 @@
+/*++
+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"
+
+tbv* tbv_manager::allocate() {
+    return reinterpret_cast<tbv*>(m.allocate());
+}
+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) {
+    return reinterpret_cast<tbv*>(m.allocate(bv));
+}
+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(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) {
+    m.deallocate(bv);
+}    
+void tbv_manager::copy(tbv& dst, tbv const& src) const {
+    m.copy(dst, src);
+}    
+tbv& tbv_manager::fill0(tbv& bv) const { 
+    // 01010101 = 1 + 4 + 16 + 64
+    memset(bv.m_data, 1 + 4 + 16 + 64, m.num_bytes());
+    return bv; 
+}
+tbv& tbv_manager::fill1(tbv& bv) const { 
+    // 10101010 = 2 + 8 + 32 + 128
+    memset(bv.m_data, 2 + 8 + 32 + 128, m.num_bytes());
+    return bv; 
+}
+tbv& tbv_manager::fillX(tbv& bv) const { 
+    m.fill1(bv); 
+    return bv; 
+}
+tbv& tbv_manager::set_and(tbv& dst, tbv const& src) const {
+    m.set_and(dst, src); 
+    return dst;
+}
+tbv& tbv_manager::set_or(tbv& dst,  tbv const& src) const {
+    m.set_or(dst, src); 
+    return dst;
+}
+tbv& tbv_manager::set_neg(tbv& dst) const {
+    m.set_neg(dst); 
+    return dst;
+}
+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);
+    set_and(result, b);
+    for (unsigned i = 0; i < num_tbits(); ++i) {
+        if (result.get(i) == BIT_z) return false;
+    }
+    return true;
+}
+
+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;
+}
diff --git a/src/muz/ddnf/tbv.h b/src/muz/ddnf/tbv.h
new file mode 100644
index 000000000..a5c282865
--- /dev/null
+++ b/src/muz/ddnf/tbv.h
@@ -0,0 +1,97 @@
+/*++
+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;
+
+class tbv_manager {
+    static const unsigned BIT_0 = 0x1;
+    static const unsigned BIT_1 = 0x2;
+    static const unsigned BIT_x = 0x3;
+    static const unsigned BIT_z = 0x0;
+    fixed_bit_vector_manager m;
+public:
+    tbv_manager(unsigned n): m(2*n) {}
+    tbv* allocate();
+    tbv* allocate1();
+    tbv* allocate0();
+    tbv* allocateX();
+    tbv* allocate(tbv const& bv);
+    tbv* allocate(uint64 n);
+    tbv* allocate(rational const& r);
+    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;
+    tbv& set_and(tbv& dst, tbv const& src) const;
+    tbv& set_or(tbv& dst,  tbv const& src) const;
+    tbv& set_neg(tbv& dst) const;
+    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;
+};
+
+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);
+        }
+    };
+        
+private:
+    void set(unsigned index, unsigned value) {
+        SASSERT(value <= 3);
+        fixed_bit_vector::set(2*index,   (value & 2) != 0);
+        fixed_bit_vector::set(2*index+1, (value & 1) != 0);
+    }
+
+    unsigned get(unsigned index) const {
+        index *= 2;
+        return (fixed_bit_vector::get(index) << 1) | (unsigned)fixed_bit_vector::get(index+1);
+    }
+};
+
+
+#endif /* _TBV_H_ */
diff --git a/src/test/main.cpp b/src/test/main.cpp
index e58845bcf..5d30bb0af 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -141,6 +141,7 @@ int main(int argc, char ** argv) {
     TST(optional);
     TST(bit_vector);
     TST(fixed_bit_vector);
+    TST(tbv);
     TST(string_buffer);
     TST(map);
     TST(diff_logic);
diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp
new file mode 100644
index 000000000..21ecdd697
--- /dev/null
+++ b/src/test/tbv.cpp
@@ -0,0 +1,39 @@
+#include "tbv.h"
+
+static void tst1(unsigned num_bits) {
+    tbv_manager m(num_bits);
+    
+    tbv* b1 = m.allocate1();
+    tbv* b0 = m.allocate0();
+    tbv* bX = m.allocateX();
+    tbv* bN = m.allocate(31);
+    m.display(std::cout, *b0) << "\n";
+    m.display(std::cout, *b1) << "\n";
+    m.display(std::cout, *bX) << "\n";
+    m.display(std::cout, *bN) << "\n";
+    SASSERT(!m.equals(*b1,*b0));
+    SASSERT(!m.equals(*b1,*bX));
+    SASSERT(!m.equals(*b0,*bX));
+    m.set_and(*bX,*b0);
+    SASSERT(m.equals(*b0,*bX));
+    SASSERT(!m.equals(*b1,*bX));
+    m.copy(*bX,*b1);
+    SASSERT(m.equals(*b1,*bX));
+    SASSERT(!m.equals(*b0,*bX));
+    m.fillX(*bX);
+    VERIFY(m.intersect(*bX,*b0,*bN));
+    SASSERT(m.equals(*b0, *bN));
+    VERIFY(!m.intersect(*b0,*b1,*bN));
+    m.deallocate(b0);
+    m.deallocate(b1);
+    m.deallocate(bX);
+    m.deallocate(bN);
+}
+
+void tst_tbv() {
+    tst1(31);
+    tst1(11);
+    tst1(15);
+    tst1(16);
+    tst1(17);
+}
diff --git a/src/util/fixed_bit_vector.cpp b/src/util/fixed_bit_vector.cpp
index c674bafda..f2af843c7 100644
--- a/src/util/fixed_bit_vector.cpp
+++ b/src/util/fixed_bit_vector.cpp
@@ -52,7 +52,7 @@ fixed_bit_vector* fixed_bit_vector_manager::allocate1() {
     return result;
 }
 
-fixed_bit_vector* fixed_bit_vector_manager::allocate(fixed_bit_vector& bv) {
+fixed_bit_vector* fixed_bit_vector_manager::allocate(fixed_bit_vector const& bv) {
     fixed_bit_vector* result = allocate();
     copy(*result, bv);
     return result;
diff --git a/src/util/fixed_bit_vector.h b/src/util/fixed_bit_vector.h
index 636c03e1b..390faa504 100644
--- a/src/util/fixed_bit_vector.h
+++ b/src/util/fixed_bit_vector.h
@@ -33,7 +33,6 @@ class fixed_bit_vector_manager {
     unsigned               m_num_bytes;
     unsigned               m_num_words;
     unsigned               m_mask;
-    unsigned num_bytes() const { return m_num_bytes; }
 
     static unsigned num_words(unsigned num_bits) { 
         return (num_bits + 31) / 32;
@@ -45,11 +44,12 @@ public:
     fixed_bit_vector* allocate();
     fixed_bit_vector* allocate1();
     fixed_bit_vector* allocate0();
-    fixed_bit_vector* allocate(fixed_bit_vector& bv);
+    fixed_bit_vector* allocate(fixed_bit_vector const& bv);
     void deallocate(fixed_bit_vector* bv);
 
     void copy(fixed_bit_vector& dst, fixed_bit_vector const& src) const;
     unsigned num_words() const { return m_num_words; }
+    unsigned num_bytes() const { return m_num_bytes; }
     unsigned num_bits() const { return m_num_bits; }
     fixed_bit_vector& reset(fixed_bit_vector& bv) const { return fill0(bv); }
     fixed_bit_vector& fill0(fixed_bit_vector& bv) const;
@@ -66,6 +66,7 @@ public:
 
 class fixed_bit_vector {
     friend class fixed_bit_vector_manager;
+    friend class tbv_manager;
     unsigned    m_data[1];
 
     static unsigned get_pos_mask(unsigned bit_idx) {