From 60d7872cc810767a261ca026c4dc06ab3e21f573 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 29 Sep 2014 18:00:34 -0700
Subject: [PATCH 01/10] adding simple BCE

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_bceq.cpp       | 116 +++++++++++++++++++++++++++++++------
 src/sat/sat_bceq.h         |   2 +
 src/sat/sat_simplifier.cpp |   2 +-
 src/sat/sat_solver.cpp     |   2 +
 src/util/union_find.h      |  12 ++++
 5 files changed, 115 insertions(+), 19 deletions(-)

diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp
index 54e8d086a..de050525f 100644
--- a/src/sat/sat_bceq.cpp
+++ b/src/sat/sat_bceq.cpp
@@ -64,6 +64,11 @@ namespace sat {
             m_bin_clauses.push_back(cls);
             register_clause(cls);
         }
+        TRACE("sat",
+              for (unsigned i = 0; i < m_clauses.size(); ++i) {
+                  clause const* cls = m_clauses[i];
+                  if (cls) tout << *cls << "\n";
+              });
     }
 
     void bceq::pure_decompose() {
@@ -109,7 +114,7 @@ namespace sat {
             m_L_blits.resize(sz1+delta1,  lit);
             m_R_blits.resize(sz2+delta2, ~lit);
         }
-        std::cout << lit << " " << "pos: " << delta1 << " " << "neg: " << delta2 << "\n";
+        TRACE("bceq", tout << lit << " " << "pos: " << delta1 << " " << "neg: " << delta2 << "\n";);
     }
     
     void bceq::pure_decompose(clause_use_list& uses, svector<clause*>& clauses) {
@@ -134,24 +139,88 @@ namespace sat {
         for (unsigned i = 0; i < m_L.size(); ++i) {
             ul.insert(*m_L[i]);
         }
+#define MOVE_R_TO_L                             \
+
+        // cheap pass: add clauses from R in order
+        // such that they are blocked with respect to
+        // predecessors.
+        m_removed.reset();
         for (unsigned i = 0; i < m_R.size(); ++i) {
             literal lit = find_blocked(*m_R[i]);
             if (lit != null_literal) {
-                m_L.push_back(m_R[i]);
-                m_L_blits.push_back(lit);
-                ul.insert(*m_R[i]);
+                m_L.push_back(m_R[i]);                  
+                m_L_blits.push_back(lit);               
+                ul.insert(*m_R[i]);                     
+                m_R[i] = m_R.back();                    
+                m_R_blits[i] = m_R_blits.back();        
+                m_R.pop_back();                         
+                m_R_blits.pop_back();                   
+                --i;                                    
+            }
+        }
+        // expensive pass: add clauses from R as long
+        // as BCE produces the empty set of clauses.
+        for (unsigned i = 0; i < m_R.size(); ++i) {
+            if (bce(*m_R[i])) {
                 m_R[i] = m_R.back();
                 m_R_blits[i] = m_R_blits.back();
                 m_R.pop_back();
                 m_R_blits.pop_back();
                 --i;
             }
-        }
+        }        
         m_use_list = save;
     }
 
+    bool bceq::bce(clause& cls) {
+        svector<bool> live_clauses;
+        use_list ul;
+        use_list* save = m_use_list;
+        m_use_list = &ul;
+        ul.init(m_solver.num_vars());
+        for (unsigned i = 0; i < m_L.size(); ++i) {
+            ul.insert(*m_L[i]);
+        }
+        ul.insert(cls);
+        svector<clause*> clauses(m_L), new_clauses;
+        literal_vector blits(m_L_blits), new_blits;
+        clauses.push_back(&cls);
+        blits.push_back(null_literal);
+        bool removed = false;
+        m_removed.reset();
+        do {
+            removed = false;
+            for (unsigned i = 0; i < clauses.size(); ++i) {
+                clause& cls = *clauses[i];
+                literal lit = find_blocked(cls);
+                if (lit != null_literal) {
+                    m_removed.setx(cls.id(), true, false);
+                    new_clauses.push_back(&cls);
+                    new_blits.push_back(lit);
+                    removed = true;
+                    clauses[i] = clauses.back();
+                    blits[i] = blits.back();
+                    clauses.pop_back();
+                    blits.pop_back();                    
+                    --i;
+                }
+            }
+        }
+        while (removed);
+        if (clauses.empty()) {
+            m_L.reset();
+            m_L_blits.reset();
+            new_clauses.reverse();
+            new_blits.reverse();
+            m_L.append(new_clauses);
+            m_L_blits.append(new_blits);
+        }
+        std::cout << "Number left after BCE: " << clauses.size() << "\n";
+        return clauses.empty();
+    }
+
     literal bceq::find_blocked(clause const& cls) {
-        std::cout << "find blocker for: " << cls << "\n";
+        TRACE("bceq", tout << cls << "\n";);
 
         unsigned sz = cls.size();
         for (unsigned i = 0; i < sz; ++i) {
@@ -161,7 +230,7 @@ namespace sat {
         for (unsigned i = 0; i < sz; ++i) {
             literal lit = cls[i];
             if (is_blocked(lit)) {
-                std::cout << "is blocked " << lit << " : " << cls << "\n";
+                TRACE("bceq", tout << "is blocked " << lit << " : " << cls << "\n";);
                 result = lit;
                 break;
             }
@@ -178,12 +247,12 @@ namespace sat {
         while (!it.at_end()) {
             clause const& cls = it.curr();
             unsigned sz = cls.size();
-            bool is_axiom = false;
+            bool is_axiom = m_removed.get(cls.id(), false);
             for (unsigned i = 0; !is_axiom && i < sz; ++i) {
                 is_axiom = m_marked[cls[i].index()] && cls[i] != ~lit;
             }
 
-            std::cout << "resolvent " << lit << " : " << cls << " " << (is_axiom?"axiom":"non-axiom") << "\n";            
+            TRACE("bceq", tout << "resolvent " << lit << " : " << cls << " " << (is_axiom?"axiom":"non-axiom") << "\n";);
             if (!is_axiom) {
                 return false;
             }
@@ -231,8 +300,6 @@ namespace sat {
             clause const& cls = *m_rstack[i];
             literal block_lit = m_bstack[i];
             uint64 b = eval_clause(cls);
-            // std::cout << "Eval: " << block_lit << " " << std::hex << " ";
-            // std::cout << m_rbits[block_lit.var()] << " " << b << std::dec << "\n";
             // v = 0, b = 0 -> v := 1
             // v = 0, b = 1 -> v := 0
             // v = 1, b = 0 -> v := 0
@@ -278,7 +345,7 @@ namespace sat {
                 table.insert(val, i);
             }
         }
-        union_find.display(std::cout);
+        TRACE("sat", union_find.display(tout););
 
         //
         // Preliminary version:
@@ -305,7 +372,7 @@ namespace sat {
     }
 
     void bceq::check_equality(unsigned v1, unsigned v2) {
-        std::cout << "check: " << v1 << " = " << v2 << "\n";
+        TRACE("sat", tout << "check: " << v1 << " = " << v2 << "\n";);
         uint64 val1 = m_rbits[v1];
         uint64 val2 = m_rbits[v2];
         literal l1 = literal(v1, false);
@@ -315,7 +382,7 @@ namespace sat {
             l2.neg();
         }
         if (is_equiv(l1, l2)) {
-            std::cout << "Already equivalent: " << l1 << " " << l2 << "\n";
+            TRACE("sat", tout << "Already equivalent: " << l1 << " " << l2 << "\n";);
             return;
         }
 
@@ -329,10 +396,10 @@ namespace sat {
             is_sat = m_s->check(2, lits);
         }
         if (is_sat == l_false) {
-            std::cout << "Found equivalent: " << l1 << " " << l2 << "\n";
+            TRACE("sat", tout << "Found equivalent: " << l1 << " " << l2 << "\n";);
         }
         else {
-            std::cout << "Not equivalent\n";
+            TRACE("sat", tout << "Not equivalent: " << l1 << " " << l2 << "\n";);
         }
     }
 
@@ -344,7 +411,7 @@ namespace sat {
             found = w.is_binary_clause() && w.get_literal() == ~l2;
         }
         if (!found) return false;
-        found = true;
+        found = false;
         watch_list const& w2 = m_solver.get_wlist(~l1);
         for (unsigned i = 0; !found && i < w2.size(); ++i) {
             watched const& w = w2[i];            
@@ -369,7 +436,20 @@ namespace sat {
         init();
         pure_decompose();
         post_decompose();
-        std::cout << m_L.size() << " vs "  << m_R.size() << "\n";
+        std::cout << "Decomposed set " << m_L.size() << "\n";
+
+        TRACE("sat",
+              tout << "Decomposed set " << m_L.size() << "\n";
+              for (unsigned i = 0; i < m_L.size(); ++i) {
+                  clause const* cls = m_L[i];
+                  if (cls) tout << *cls << "\n";
+              }
+              tout << "remainder " << m_R.size() << "\n";
+              for (unsigned i = 0; i < m_R.size(); ++i) {
+                  clause const* cls = m_R[i];
+                  if (cls) tout << *cls << "\n";
+              }
+              );
         sat_sweep();
         extract_partition();
         cleanup();
diff --git a/src/sat/sat_bceq.h b/src/sat/sat_bceq.h
index 7e9a1f632..5552fb255 100644
--- a/src/sat/sat_bceq.h
+++ b/src/sat/sat_bceq.h
@@ -45,6 +45,7 @@ namespace sat {
         svector<clause*>  m_rstack; // stack of blocked clauses
         literal_vector    m_bstack; // stack of blocking literals
         svector<bool>     m_marked;
+        svector<bool>     m_removed; // set of clauses removed (not considered in clause set during BCE)
         union_find_default_ctx m_union_find_ctx;
 
         void init();
@@ -55,6 +56,7 @@ namespace sat {
         void pure_decompose(clause_use_list& uses, svector<clause*>& clauses);
         void post_decompose();
         literal find_blocked(clause const& cls);
+        bool bce(clause& cls);
         bool is_blocked(literal lit) const;
         void init_rbits();
         void init_reconstruction_stack();
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 3bb914ad0..937c7735f 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -157,7 +157,7 @@ namespace sat {
         if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
             elim_blocked_clauses();
 
-#if 0
+#if 1
         // experiment is disabled.
         if (!learned) { // && m_equality_inference
             bceq bc(s);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index b81f07e95..d97ebed46 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -20,6 +20,7 @@ Revision History:
 #include"sat_integrity_checker.h"
 #include"luby.h"
 #include"trace.h"
+#include"sat_bceq.h"
 
 // define to update glue during propagation
 #define UPDATE_GLUE
@@ -959,6 +960,7 @@ namespace sat {
         m_stopwatch.start();
         m_core.reset();
         TRACE("sat", display(tout););
+
     }
 
     /**
diff --git a/src/util/union_find.h b/src/util/union_find.h
index a5c897656..c98ca3fce 100644
--- a/src/util/union_find.h
+++ b/src/util/union_find.h
@@ -132,6 +132,18 @@ public:
         CASSERT("union_find", check_invariant());
     }
 
+    // dissolve equivalence class of v
+    // this method cannot be used with backtracking.
+    void dissolve(unsigned v) {
+        do {
+            w = next(v);                        
+            m_size[v] = 1;
+            m_find[v] = v;
+            m_next[v] = v;            
+        }
+        while (w != v);
+    }
+
     void display(std::ostream & out) const {
         unsigned num = get_num_vars(); 
         for (unsigned v = 0; v < num; v++) {

From 83a0611cb952167884654baedc267ab0e30a8e8f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 29 Sep 2014 22:15:24 -0700
Subject: [PATCH 02/10] adding option to selectively enable bcd

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_bceq.cpp   | 2 ++
 src/sat/sat_config.cpp | 1 +
 src/sat/sat_config.h   | 1 +
 src/sat/sat_params.pyg | 1 +
 4 files changed, 5 insertions(+)

diff --git a/src/sat/sat_bceq.cpp b/src/sat/sat_bceq.cpp
index de050525f..65377caed 100644
--- a/src/sat/sat_bceq.cpp
+++ b/src/sat/sat_bceq.cpp
@@ -428,6 +428,8 @@ namespace sat {
 
 
     void bceq::operator()() {
+        if (!m_solver.m_config.m_bcd) return;
+        flet<bool> _disable_bcd(m_solver.m_config.m_bcd, false);
         use_list     ul;        
         solver       s(m_solver.m_params, 0);
         m_use_list = &ul;
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 17eda1707..d2a662b64 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -107,6 +107,7 @@ namespace sat {
         m_minimize_core   = p.minimize_core();
         m_minimize_core_partial   = p.minimize_core_partial();
         m_optimize_model  = p.optimize_model();
+        m_bcd             = p.bcd();
         m_dyn_sub_res     = p.dyn_sub_res();
     }
 
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 044c91989..021810f3d 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -71,6 +71,7 @@ namespace sat {
         bool               m_minimize_core;
         bool               m_minimize_core_partial;
         bool               m_optimize_model;
+        bool               m_bcd;
 
 
         symbol             m_always_true;
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index b0be62eef..1e2551740 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -21,4 +21,5 @@ def_module_params('sat',
                           ('minimize_core', BOOL, False, 'minimize computed core'),
                           ('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'),
                           ('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
+                          ('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

From 5176cbeefb93d74d99a5b3fa0ef520938ad6b9f7 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 30 Sep 2014 11:26:49 +0100
Subject: [PATCH 03/10] fix printing of TBVs

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/tbv.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 739443ea0..4ea8f48f6 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -268,7 +268,7 @@ bool tbv_manager::intersect(tbv const& a, tbv const& b, tbv& result) {
 
 std::ostream& tbv_manager::display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const {
     SASSERT(lo <= hi && hi < num_tbits());
-    for (unsigned i = lo; i <= hi; ++i) {
+    for (unsigned i = hi+1; i-- > lo; ) {
         switch (b.get(i)) {
         case BIT_0:
             out << '0';

From 938a5adafa4d9cda95274fefc64d5ba73af92441 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 30 Sep 2014 13:00:29 +0100
Subject: [PATCH 04/10] DoC: make fold_neg detect empty TBVs

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/doc.cpp | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index e2c0ab162..817317f9f 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -110,12 +110,11 @@ doc& doc_manager::fillX(doc& 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;
-    dst.neg().intersect(m, dst.pos());    
+    dst.neg().intersect(m, dst.pos());
     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())) {
-            if (m.equals(*t, dst.pos())) return false;
             dst.neg().insert(m, t.detach());
         }
     }
@@ -123,10 +122,10 @@ bool doc_manager::set_and(doc& dst, doc const& src)  {
     return fold_neg(dst);
 }
 bool doc_manager::set_and(doc& dst, tbv const& src)  {
-    // (A \ B) & C  = (A & C) \ B
+    // (A \ B) & C  = (A & C) \ (B & C)
     if (!m.set_and(dst.pos(), src)) return false;
     dst.neg().intersect(m, src);
-    return true;
+    return fold_neg(dst);
 }
 
 bool doc_manager::well_formed(doc const& d) const {
@@ -141,6 +140,9 @@ bool doc_manager::well_formed(doc const& d) const {
 bool doc_manager::fold_neg(doc& dst) {
  start_over:
     for (unsigned i = 0; i < dst.neg().size(); ++i) {
+        if (m.contains(dst.neg()[i], dst.pos()))
+            return false;
+
         unsigned index;
         unsigned count = diff_by_012(dst.pos(), dst.neg()[i], index);
         if (count != 2) {
@@ -498,9 +500,6 @@ bool doc_manager::is_full(doc const& src) const {
 }
 bool doc_manager::is_empty(doc const& src)  {
     if (src.neg().size() == 0) return false;
-    if (src.neg().size() == 1) {
-        return m.equals(src.pos(), src.neg()[0]);
-    }
     return false;
 #if 0
     // buggy:

From 1606359dc9ca77091926c00d33ff18eb88a82e4b Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 30 Sep 2014 15:58:38 +0100
Subject: [PATCH 05/10] DoC: add slow path to emptiness detection that uses SMT
 solving

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/dl_instruction.cpp      |  2 +-
 src/muz/rel/dl_relation_manager.cpp |  2 +-
 src/muz/rel/doc.cpp                 | 36 ++++++++---------------------
 src/muz/rel/doc.h                   | 13 ++++++++---
 src/muz/rel/rel_context.cpp         |  4 ++--
 src/muz/rel/udoc_relation.cpp       | 11 +--------
 6 files changed, 25 insertions(+), 43 deletions(-)

diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index bf2f09d56..b2837c710 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -307,7 +307,7 @@ namespace datalog {
             idx_vector::const_iterator end=m_controls.end();
             for(; it != end; ++it) {
                 reg_idx r = *it;
-                if (ctx.reg(r) && !ctx.reg(r)->empty()) {
+                if (ctx.reg(r) && !ctx.reg(r)->fast_empty()) {
                     return false;
                 }
             }
diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp
index e227e469a..a2b16bcf9 100644
--- a/src/muz/rel/dl_relation_manager.cpp
+++ b/src/muz/rel/dl_relation_manager.cpp
@@ -122,7 +122,7 @@ namespace datalog {
         relation_map::iterator it = m_relations.begin();
         relation_map::iterator end = m_relations.end();
         for(; it!=end; ++it) {
-            if(!it->m_value->empty()) {
+            if(!it->m_value->fast_empty()) {
                 res.insert(it->m_key);
             }
         }
diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 817317f9f..cc35227cd 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -83,7 +83,6 @@ void doc_manager::deallocate(doc* src) {
     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());
@@ -118,7 +117,6 @@ bool doc_manager::set_and(doc& dst, doc const& src)  {
             dst.neg().insert(m, t.detach());
         }
     }
-    SASSERT(well_formed(dst));
     return fold_neg(dst);
 }
 bool doc_manager::set_and(doc& dst, tbv const& src)  {
@@ -498,33 +496,19 @@ bool doc_manager::equals(doc const& a, doc const& b) const {
 bool doc_manager::is_full(doc const& src) const {
     return src.neg().is_empty() && m.equals(src.pos(), *m_full);
 }
-bool doc_manager::is_empty(doc const& src)  {
+bool doc_manager::is_empty_complete(ast_manager& m, doc const& src)  {
     if (src.neg().size() == 0) return false;
-    return false;
-#if 0
-    // buggy:
-    tbv_ref pos(m, m.allocate(src.pos()));
-    for (unsigned i = 0; i < src.neg().size(); ++i) {
-        bool found = false;
-        for (unsigned j = 0; !found && j < num_tbits(); ++j) {
-            tbit b1 = (*pos)[j];
-            tbit b2 = src.neg()[i][j];
-            found = (b1 != BIT_x && b2 != BIT_x && b1 != b2);
-        }
-        for (unsigned j = 0; !found && j < num_tbits(); ++j) {
-            tbit b1 = (*pos)[j];
-            tbit b2 = src.neg()[i][j];
-            found = (b1 == BIT_x && b2 != BIT_x);
-            if (found) {
-                m.set(*pos, j, neg(b2));
-            }
-        }
-        if (!found) {
-            return false; // TBD make complete SAT check.
-        }
+
+    smt_params fp;
+    smt::kernel s(m, fp);
+    expr_ref fml = to_formula(m, src);
+    s.assert_expr(fml);
+    lbool res = s.check();
+    if (res == l_true) {
+        return false;
     }
+    SASSERT(res == l_false);
     return true;
-#endif
 }
 
 unsigned doc_manager::hash(doc const& src) const {
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index 16e7c5f28..eccdd75b0 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -72,7 +72,7 @@ public:
     doc& fill1(doc& src);
     doc& fillX(doc& src);
     bool is_full(doc const& src) const;
-    bool is_empty(doc const& src);
+    bool is_empty_complete(ast_manager& m, doc const& src);
     bool set_and(doc& dst, doc const& src);
     bool set_and(doc& dst, tbv const& src);
     bool fold_neg(doc& dst);
@@ -119,10 +119,17 @@ class union_bvec {
 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_empty() const { return m_elems.empty(); }
+    bool is_empty_complete(ast_manager& m, doc_manager& dm) const {
+        for (unsigned i = 0; i < size(); ++i) {
+            if (!dm.is_empty_complete(m, *m_elems[i]))
+                return false;
+        }
+        return true;
+    }
     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) {
+        for (unsigned i = 0; i < size(); ++i) {
             if (m.contains(*m_elems[i], t)) return true;
         }
         return false;
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index 4b099c9b4..c5c4d6d95 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -375,7 +375,7 @@ namespace datalog {
             for (; it != end; ++it) {
                 func_decl* pred = *it;
                 relation_base & rel = get_relation(pred);
-                if (!rel.empty()) {
+                if (!rel.fast_empty()) {
                     non_empty = true;
                     break;
                 }
@@ -449,7 +449,7 @@ namespace datalog {
 
     bool rel_context::is_empty_relation(func_decl* pred) const {
         relation_base* rb = try_get_relation(pred);
-        return !rb || rb->empty();
+        return !rb || rb->fast_empty();
     }
 
     relation_manager & rel_context::get_rmanager() { return m_rmanager; }
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 51e4c33af..4e46a463f 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -21,10 +21,6 @@ Revision History:
 Notes:
 
     Current pending items:
-    - Fix the incomplete non-emptiness check in doc.cpp
-      It can fall back to a sat_solver call in the worst case.
-      The sat_solver.h interface gives a way to add clauses to a sat solver
-      and check for satisfiability. It can be used from scratch each time.
     - Profile and fix bottlnecks:
       - Potential bottleneck in projection exercised in some benchmarks.
         Projection is asymptotically very expensive. We are here interested in 
@@ -127,12 +123,7 @@ namespace datalog {
         m_elems.push_back(fact2doc(f));
     }
     bool udoc_relation::empty() const {
-        if (m_elems.is_empty()) return true;
-        // TBD: make this a complete check
-        for (unsigned i = 0; i < m_elems.size(); ++i) {
-            if (!dm.is_empty(m_elems[i])) return false;
-        }
-        return true;
+        return m_elems.is_empty_complete(get_plugin().m, dm);
     }
     bool udoc_relation::contains_fact(const relation_fact & f) const {
         doc_ref d(dm, fact2doc(f));

From 8d1177bf3f972f038a6e116574942d8beda9fe68 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 30 Sep 2014 16:24:59 +0100
Subject: [PATCH 06/10] DoC: compact result of substract and maintain invariant

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/doc.cpp | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index cc35227cd..03f69bf5f 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -472,15 +472,15 @@ void doc_manager::subtract(doc const& A, doc const& B, doc_vector& result) {
     tbv_ref t(m);
     r = allocate(A);
     t = m.allocate(B.pos());
-    if (m.set_and(*t, A.pos()) && r->neg().insert(m, t.detach())) {
-        result.push_back(r.detach());
-    }
-    else {
-        result.push_back(allocate(A));
+    if (m.set_and(*t, A.pos())) {
+        r->neg().insert(m, t.detach());
     }
+    result.push_back(r.detach());
+
     for (unsigned i = 0; i < B.neg().size(); ++i) {
         r = allocate(A);
         if (set_and(*r, B.neg()[i])) {
+            r->neg().intersect(m, r->pos());
             result.push_back(r.detach());
         }
     }

From 115ab12ade507eab412fd4c9d2a343b455d43b59 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Tue, 30 Sep 2014 17:16:14 +0100
Subject: [PATCH 07/10] DoC: code cleanups

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/doc.cpp           | 17 ++++++++---------
 src/muz/rel/doc.h             | 17 ++++++++++-------
 src/muz/rel/tbv.cpp           |  4 ++--
 src/muz/rel/tbv.h             |  2 +-
 src/muz/rel/udoc_relation.cpp | 24 +++++++++---------------
 5 files changed, 30 insertions(+), 34 deletions(-)

diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 03f69bf5f..c8cef5c95 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -280,7 +280,7 @@ bool doc_manager::intersect(doc const& A, doc const& B, doc& result) {
 //   indices where BIT_0 is set are positive.
 //
 
-doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src) {
+doc* doc_manager::project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src) {
     tbv_manager& dstt = dstm.m;    
     tbv_ref t(dstt);
     t = dstt.project(n, to_delete, src.pos());
@@ -391,7 +391,7 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
 
 doc_manager::project_action_t 
 doc_manager::pick_resolvent(
-    tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx) {
+    tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx) {
     if (neg.empty()) return project_done;
     for (unsigned j = 0; j < neg.size(); ++j) {
         if (m.equals(pos, *neg[j])) return project_is_empty;   
@@ -401,7 +401,7 @@ doc_manager::pick_resolvent(
     unsigned best_neg = UINT_MAX;
     unsigned best_idx = UINT_MAX;
     for (unsigned i = 0; i < num_tbits(); ++i) {
-        if (!to_delete[i]) continue;
+        if (!to_delete.get(i)) continue;
         if (pos[i] != BIT_x) continue;
         unsigned num_pos = 0, num_neg = 0;
         tbit b1 = (*neg[0])[i];
@@ -480,7 +480,6 @@ void doc_manager::subtract(doc const& A, doc const& B, doc_vector& result) {
     for (unsigned i = 0; i < B.neg().size(); ++i) {
         r = allocate(A);
         if (set_and(*r, B.neg()[i])) {
-            r->neg().intersect(m, r->pos());
             result.push_back(r.detach());
         }
     }
@@ -566,7 +565,7 @@ std::ostream& doc_manager::display(std::ostream& out, doc const& b, unsigned hi,
 }
 
 
-void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst) {
+void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst) {
     expr_ref fml1 = to_formula(m, src);
     expr_ref fml2 = dstm.to_formula(m, dst);
     project_rename(fml2, to_delete);
@@ -603,11 +602,11 @@ expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) {
     return result;
 }
     
-void doc_manager::project_expand(expr_ref& fml, bool const* to_delete) {
+void doc_manager::project_expand(expr_ref& fml, bit_vector const& to_delete) {
     ast_manager& m = fml.get_manager();
     expr_ref tmp1(m), tmp2(m);
     for (unsigned i = 0; i < num_tbits(); ++i) {
-        if (to_delete[i]) {
+        if (to_delete.get(i)) {
             expr_safe_replace rep1(m), rep2(m);
             rep1.insert(tbvm().mk_var(m, i), m.mk_true());
             rep1(fml, tmp1);
@@ -623,11 +622,11 @@ void doc_manager::project_expand(expr_ref& fml, bool const* to_delete) {
     }
 }
 
-void doc_manager::project_rename(expr_ref& fml, bool const* to_delete) {
+void doc_manager::project_rename(expr_ref& fml, bit_vector const& to_delete) {
     ast_manager& m = fml.get_manager();
     expr_safe_replace rep(m);
     for (unsigned i = 0, j = 0; i < num_tbits(); ++i) {
-        if (!to_delete[i]) {
+        if (!to_delete.get(i)) {
             rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i));
             ++j;
         }
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index eccdd75b0..145f8d456 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -48,7 +48,7 @@ class doc_manager {
         project_resolve        
     };
     project_action_t pick_resolvent(
-        tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx);
+        tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx);
 public:
     doc_manager(unsigned num_bits);
     ~doc_manager();
@@ -88,17 +88,17 @@ public:
     std::ostream& display(std::ostream& out, doc const& b) const;
     std::ostream& display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const;
     unsigned num_tbits() const { return m.num_tbits(); }
-    doc* project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src);
+    doc* project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src);
     bool well_formed(doc const& d) const;
     bool merge(doc& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
     void set(doc& d, unsigned idx, tbit value);
 
-    void verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst);
+    void verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst);
 private:
     unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
     bool merge(doc& d, unsigned idx, subset_ints const& equalities, bit_vector const& discard_cols);
-    void project_rename(expr_ref& fml, bool const* to_delete);
-    void project_expand(expr_ref& fml, bool const* to_delete);
+    void project_rename(expr_ref& fml, bit_vector const& to_delete);
+    void project_expand(expr_ref& fml, bit_vector const& to_delete);
     expr_ref to_formula(ast_manager& m, doc const& src);
     void check_equiv(ast_manager& m, expr* fml1, expr* fml2);
 };
@@ -171,11 +171,13 @@ public:
         SASSERT(t);
         unsigned sz = size(), j = 0;
         bool found = false;
-        for (unsigned i = 0; i < sz; ++i, ++j) {
+        unsigned i = 0;
+        for ( ; i < sz; ++i, ++j) {
             if (m.contains(*m_elems[i], *t)) {
                 found = true;
+                break;
             }
-            if (!found && m.contains(*t, *m_elems[i])) {
+            if (m.contains(*t, *m_elems[i])) {
                 m.deallocate(m_elems[i]);
                 --j;
             }
@@ -185,6 +187,7 @@ public:
         }
         if (j != sz) m_elems.resize(j);
         if (found) {
+            SASSERT(j == i);
             m.deallocate(t);
         }
         else {
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 4ea8f48f6..8e213fadc 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -99,11 +99,11 @@ tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) {
     }
     return r;
 }
-tbv* tbv_manager::project(unsigned n, bool const* to_delete, tbv const& src) {
+tbv* tbv_manager::project(unsigned n, bit_vector const& to_delete, tbv const& src) {
     tbv* r = allocate();
     unsigned i, j;
     for (i = 0, j = 0; i < n; ++i) {
-        if (!to_delete[i]) {
+        if (!to_delete.get(i)) {
             set(*r, j, src[i]);
             ++j;
         }
diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h
index 9663f7d04..39067c64c 100644
--- a/src/muz/rel/tbv.h
+++ b/src/muz/rel/tbv.h
@@ -76,7 +76,7 @@ public:
     bool intersect(tbv const& a, tbv const& b, tbv& result);
     std::ostream& display(std::ostream& out, tbv const& b) const;
     std::ostream& display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const;
-    tbv* project(unsigned n, bool const* to_delete, tbv const& src);
+    tbv* project(unsigned n, bit_vector const& to_delete, tbv const& src);
     bool is_well_formed(tbv const& b) const; // - does not contain BIT_z;
     void set(tbv& dst, uint64 n, unsigned hi, unsigned lo);
     void set(tbv& dst, rational const& r, unsigned hi, unsigned lo);
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 4e46a463f..459b94101 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -54,9 +54,6 @@ Notes:
      return tgt \ join_project(tgt, neg, c1, .., cN, d1, .. , dN)
      We have most of the facilities required for a join project operation.
      For example, the filter_project function uses both equalities and deleted columns.
-   - Lipstick service:
-     - filter_proj_fn uses both a bit_vector and a svector<bool> for representing removed bits. 
-       This is due to underlying routines using different types for the same purpose. 
 --*/
 #include "udoc_relation.h"
 #include "dl_relation_manager.h"
@@ -473,7 +470,7 @@ namespace datalog {
     }
 
     class udoc_plugin::project_fn : public convenient_relation_project_fn {
-        svector<bool> m_to_delete;
+        bit_vector 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) {
@@ -481,7 +478,7 @@ namespace datalog {
             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;
+                m_to_delete.set(m_removed_cols[i], true);
             }
         }
 
@@ -496,7 +493,7 @@ namespace datalog {
             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]);
+                d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete, ud1[i]);
                 ud2.push_back(d2.detach());
             }
             TRACE("doc", tout << "final size: " << r->get_size_estimate_rows() << '\n';);
@@ -1198,8 +1195,7 @@ namespace datalog {
         expr_ref     m_reduced_condition;
         udoc         m_udoc;
         udoc         m_udoc2;
-        bit_vector   m_col_list; // map: col idx -> bool (whether the column is to be removed)
-        svector<bool> m_to_delete; // same
+        bit_vector   m_to_delete; // map: col idx -> bool (whether the column is to be removed)
         subset_ints  m_equalities;
         unsigned_vector m_roots;
 
@@ -1213,19 +1209,17 @@ namespace datalog {
             m_equalities(union_ctx) {
             unsigned num_bits = t.get_num_bits();
             t.expand_column_vector(m_removed_cols);
-            m_col_list.resize(num_bits,  false);
             m_to_delete.resize(num_bits, false);
             for (unsigned i = 0; i < num_bits; ++i) {
                 m_equalities.mk_var();
             }        
             for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
-                m_col_list.set(m_removed_cols[i], true);
-                m_to_delete[m_removed_cols[i]] = true;
+                m_to_delete.set(m_removed_cols[i], true);
             }
             expr_ref guard(m), non_eq_cond(condition, m);
             t.extract_equalities(condition, non_eq_cond, m_equalities, m_roots);
             t.extract_guard(non_eq_cond, guard, m_reduced_condition);            
-            t.compile_guard(guard, m_udoc, m_col_list);
+            t.compile_guard(guard, m_udoc, m_to_delete);
         }
         
         virtual ~filter_proj_fn() {
@@ -1238,13 +1232,13 @@ namespace datalog {
             ast_manager& m = m_reduced_condition.get_manager();
             m_udoc2.copy(dm, u1);
             m_udoc2.intersect(dm, m_udoc);
-            t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_col_list);
-            m_udoc2.merge(dm, m_roots, m_equalities, m_col_list);
+            t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_to_delete);
+            m_udoc2.merge(dm, m_roots, m_equalities, m_to_delete);
             SASSERT(m_udoc2.well_formed(dm));  
             udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature()));
             doc_manager& dm2 = r->get_dm();
             for (unsigned i = 0; i < m_udoc2.size(); ++i) {
-                doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), m_udoc2[i]);
+                doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete, m_udoc2[i]);
                 r->get_udoc().insert(dm2, d);
                 SASSERT(r->get_udoc().well_formed(dm2));
             }

From cbe23c428fd3cd9340b07e6fe96fd67f0bcb90a9 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Wed, 1 Oct 2014 16:08:44 +0100
Subject: [PATCH 08/10] fix build of unit tests

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/test/doc.cpp | 51 +++++++++++++++++++++++++-----------------------
 src/test/tbv.cpp |  9 +++++----
 2 files changed, 32 insertions(+), 28 deletions(-)

diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index 3dcf57613..731bc100f 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -73,23 +73,24 @@ static void tst_doc1(unsigned n) {
     m.display(std::cout, *d1) << "\n";
 
 
-    svector<bool> to_delete(n, false);
-    to_delete[1] = true;
-    to_delete[3] = true;
+    bit_vector to_delete;
+    to_delete.resize(n, false);
+    to_delete.set(1);
+    to_delete.set(3);
     doc_manager m1(n-2);
-    doc_ref d1_1(m1, m.project(m1, n, to_delete.c_ptr(), *d1));
+    doc_ref d1_1(m1, m.project(m1, n, to_delete, *d1));
     doc_ref d1_2(m1, m1.allocate1());
     m.display(std::cout, *d1) << " -> ";
     m1.display(std::cout, *d1_1) << "\n";
     SASSERT(m1.equals(*d1_1,*d1_2));
     m.set(*d1,2,BIT_x);
     m.set(*d1,4,BIT_x);
-    d1_1 = m.project(m1, n, to_delete.c_ptr(), *d1);
+    d1_1 = m.project(m1, n, to_delete, *d1);
     m.display(std::cout, *d1) << " -> ";
     m1.display(std::cout, *d1_1) << "\n";
     d1->neg().push_back(m.tbvm().allocate1());
     SASSERT(m.well_formed(*d1));
-    d1_1 = m.project(m1, n, to_delete.c_ptr(), *d1);
+    d1_1 = m.project(m1, n, to_delete, *d1);
     m.display(std::cout, *d1) << " -> ";
     m1.display(std::cout, *d1_1) << "\n";    
 }
@@ -216,11 +217,11 @@ class test_doc_cls {
         return result;
     }
 
-    void project(doc const& d, doc_manager& m2, bool const* to_delete, doc_ref& result) {
+    void project(doc const& d, doc_manager& m2, const bit_vector& to_delete, doc_ref& result) {
         result = dm.project(m2, m_vars.size(), to_delete, d);
         TRACE("doc",
               for (unsigned i = 0; i < m_vars.size(); ++i) {
-                  tout << (to_delete[i]?"0":"1");
+                  tout << (to_delete.get(i)?"0":"1");
               }
               tout << " ";
               dm.display(tout, d) << " -> ";
@@ -234,28 +235,29 @@ class test_doc_cls {
         d = mk_rand_doc(3);
         expr_ref fml1(m), fml2(m), fml3(m), tmp1(m), tmp2(m), fml(m);
         fml1 = to_formula(*d, dm);
-        svector<bool> to_delete(m_vars.size(), false);
+        bit_vector to_delete;
+        to_delete.reserve(m_vars.size(), false);
         unsigned num_bits = 1;
         for (unsigned i = 1; i < to_delete.size(); ++i) {
-            to_delete[i] = (m_ran(2) == 0);
-            if (!to_delete[i]) ++num_bits;
+            to_delete.set(i, m_ran(2) == 0);
+            if (!to_delete.get(i)) ++num_bits;
         }
         doc_manager m2(num_bits);
         doc_ref result(m2);
-        project(*d, m2, to_delete.c_ptr(), result);
+        project(*d, m2, to_delete, result);
         TRACE("doc",              
               dm.display(tout, *d) << "\n";
               m2.display(tout, *result) << "\n";);
         fml2 = to_formula(*result, m2);
-        project_expand(fml1, to_delete.c_ptr());
-        project_rename(fml2, to_delete.c_ptr());
+        project_expand(fml1, to_delete);
+        project_rename(fml2, to_delete);
         check_equiv(fml1, fml2);
     }
 
-    void project_expand(expr_ref& fml, bool const* to_delete) {
+    void project_expand(expr_ref& fml, bit_vector const& to_delete) {
         expr_ref tmp1(m), tmp2(m);
         for (unsigned i = 0; i < m_vars.size(); ++i) {
-            if (to_delete[i]) {
+            if (to_delete.get(i)) {
                 expr_safe_replace rep1(m), rep2(m);
                 rep1.insert(m_vars[i].get(), m.mk_true());
                 rep1(fml, tmp1);
@@ -271,10 +273,10 @@ class test_doc_cls {
         }
     }
 
-    void project_rename(expr_ref& fml, bool const* to_delete) {
+    void project_rename(expr_ref& fml, bit_vector const& to_delete) {
         expr_safe_replace rep(m);
         for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
-            if (!to_delete[i]) {
+            if (!to_delete.get(i)) {
                 rep.insert(m_vars[j].get(), m_vars[i].get());
                 ++j;
             }
@@ -293,7 +295,7 @@ class test_doc_cls {
             d->neg().push_back(t);
         }
         fml1 = mk_and(m, fmls.size(), fmls.c_ptr());
-        svector<bool> to_merge(N, false), to_delete(N, false);
+        svector<bool> to_merge(N, false);
         bit_vector discard_cols;
         discard_cols.resize(N, false);
         unsigned num_bits = 1;
@@ -371,17 +373,18 @@ public:
         dm.tbvm().set(*t, 0, BIT_0);
         d->neg().push_back(t.detach());
         unsigned num_bits = dm.num_tbits();
-        svector<bool> to_delete(num_bits, false);
+        bit_vector to_delete;
+        to_delete.reserve(num_bits, false);
         fml1 = to_formula(*d, dm);
-        to_delete[0] = true;
+        to_delete.set(0, true);
         doc_manager m2(num_bits-1);
         doc_ref result(m2);
-        project(*d, m2, to_delete.c_ptr(), result);
+        project(*d, m2, to_delete, result);
         dm.display(std::cout, *d) << "\n";
         m2.display(std::cout, *result) << "\n";
         fml2 = to_formula(*result, m2);
-        project_rename(fml2, to_delete.c_ptr());
-        project_expand(fml1, to_delete.c_ptr());
+        project_rename(fml2, to_delete);
+        project_expand(fml1, to_delete);
         std::cout << fml1 << " " << fml2 << "\n";
         check_equiv(fml1, fml2);
     }
diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp
index 70a07d3f5..dc2867f58 100644
--- a/src/test/tbv.cpp
+++ b/src/test/tbv.cpp
@@ -25,13 +25,14 @@ static void tst1(unsigned num_bits) {
     SASSERT(m.equals(*b0, *bN));
     VERIFY(!m.intersect(*b0,*b1,*bN));
     m.fill1(*b1);
-    svector<bool> to_delete(num_bits, false);
+    bit_vector to_delete;
+    to_delete.reserve(num_bits, false);
     tbv_manager m2(num_bits-2);
-    to_delete[1] = true;
-    to_delete[3] = true;
+    to_delete.set(1);
+    to_delete.set(3);
     m.set(*b1, 2, BIT_0);
     m.set(*b1, 4, BIT_x);
-    tbv_ref b2(m2, m2.project(num_bits, to_delete.c_ptr(), *b1));
+    tbv_ref b2(m2, m2.project(num_bits, to_delete, *b1));
     m.display(std::cout, *b1) << " -> ";
     m2.display(std::cout, *b2) << "\n";
     m.deallocate(b0);

From 5211e9aa1a4dc41900680eefb4e8709120c44703 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Wed, 1 Oct 2014 17:10:35 +0100
Subject: [PATCH 09/10] DoC: compact result of subtract

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/doc.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index c8cef5c95..9668039cf 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -475,7 +475,8 @@ void doc_manager::subtract(doc const& A, doc const& B, doc_vector& result) {
     if (m.set_and(*t, A.pos())) {
         r->neg().insert(m, t.detach());
     }
-    result.push_back(r.detach());
+    if (fold_neg(*r))
+        result.push_back(r.detach());
 
     for (unsigned i = 0; i < B.neg().size(); ++i) {
         r = allocate(A);

From 04b5d436b3f0df6f512f25606dfac3735eede2b5 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Wed, 1 Oct 2014 18:03:59 +0100
Subject: [PATCH 10/10] DoC: fix fast path of filter_negated

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/muz/rel/doc.cpp           | 13 +++++----
 src/muz/rel/doc.h             |  5 ++--
 src/muz/rel/tbv.cpp           | 16 ++++-------
 src/muz/rel/tbv.h             |  5 ++--
 src/muz/rel/udoc_relation.cpp | 34 ++++++++----------------
 src/test/udoc_relation.cpp    | 50 +++++++++++++++++++++++++++++++++++
 6 files changed, 76 insertions(+), 47 deletions(-)

diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp
index 9668039cf..e5a6fd97f 100644
--- a/src/muz/rel/doc.cpp
+++ b/src/muz/rel/doc.cpp
@@ -536,16 +536,15 @@ bool doc_manager::contains(doc const& a, doc const& b) const {
     return true;
 }
 
-bool doc_manager::contains(
-    unsigned offset_a, doc const& a,
-    doc_manager const& dm_b,
-    unsigned offset_b, doc const& b,
-    unsigned length) const {
-    if (!m.contains(offset_a, a.pos(), dm_b.tbvm(), offset_b, b.pos(), length)) return false;
+bool doc_manager::contains(doc const& a, unsigned_vector const& colsa,
+                           doc const& b, unsigned_vector const& colsb) const {
+    if (!m.contains(a.pos(), colsa, b.pos(), colsb))
+        return false;
+
     for (unsigned i = 0; i < a.neg().size(); ++i) {
         bool found = false;
         for (unsigned j = 0; !found && j < b.neg().size(); ++j) {
-            found = dm_b.tbvm().contains(offset_b, b.neg()[j], tbvm(), offset_a, a.neg()[i], length);
+            found = m.contains(b.neg()[j], colsb, a.neg()[i], colsa);
         }
         if (!found) return false;
     }
diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index 145f8d456..75b4e9499 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -82,9 +82,8 @@ public:
     bool equals(doc const& a, doc const& b) const;
     unsigned hash(doc const& src) const;
     bool contains(doc const& a, doc const& b) const;
-    bool contains(unsigned offset_a, doc const& a,
-                  doc_manager const& dm_b, unsigned offset_b, doc const& b,
-                  unsigned length) const;
+    bool contains(doc const& a, unsigned_vector const& colsa,
+                  doc const& b, unsigned_vector const& colsb) const;
     std::ostream& display(std::ostream& out, doc const& b) const;
     std::ostream& display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const;
     unsigned num_tbits() const { return m.num_tbits(); }
diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp
index 8e213fadc..9c71b826c 100644
--- a/src/muz/rel/tbv.cpp
+++ b/src/muz/rel/tbv.cpp
@@ -245,18 +245,12 @@ bool tbv_manager::contains(tbv const& a, tbv const& b) const {
     return m.contains(a, b);
 }
 
-bool tbv_manager::contains(unsigned offset_a, tbv const& a,
-                           tbv_manager const& dm_b, unsigned offset_b, tbv const& b,
-                           unsigned length) const {
-    if (this == &dm_b && length == num_tbits()) {
-        SASSERT(offset_a == 0);
-        SASSERT(offset_b == 0);
-        return m.contains(a, b);
-    }
-    for (unsigned i = 0; i < length; ++i) {
-        tbit bit_a = a[offset_a + i];
+bool tbv_manager::contains(tbv const& a, unsigned_vector const& colsa,
+                           tbv const& b, unsigned_vector const& colsb) const {
+    for (unsigned i = 0; i < colsa.size(); ++i) {
+        tbit bit_a = a[colsa[i]];
         if (bit_a == BIT_x) continue;
-        if (bit_a != b[offset_b + i]) return false;
+        if (bit_a != b[colsb[i]]) return false;
     }
     return true;
 }
diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h
index 39067c64c..941853a1b 100644
--- a/src/muz/rel/tbv.h
+++ b/src/muz/rel/tbv.h
@@ -70,9 +70,8 @@ public:
     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 contains(unsigned offset_a, tbv const& a,
-                  tbv_manager const& dm_b, unsigned offset_b, tbv const& b,
-                  unsigned length) const;
+    bool contains(tbv const& a, unsigned_vector const& colsa,
+                  tbv const& b, unsigned_vector const& colsb) const;
     bool intersect(tbv const& a, tbv const& b, tbv& result);
     std::ostream& display(std::ostream& out, tbv const& b) const;
     std::ostream& display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const;
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 459b94101..10c01ccdd 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -1064,14 +1064,16 @@ namespace datalog {
     // 4. Unit/stress test cases are needed.
     // 
     class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn {
-        const unsigned_vector m_t_cols;
-        const unsigned_vector m_neg_cols;
+        unsigned_vector m_t_cols;
+        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);
+            r.expand_column_vector(m_t_cols);
+            neg.expand_column_vector(m_neg_cols);
         }
         
         virtual void operator()(relation_base& tb, const relation_base& negb) {
@@ -1086,30 +1088,16 @@ namespace datalog {
 
             udoc result;
             for (unsigned i = 0; i < dst.size(); ++i) {
+                bool subsumed = false;
                 for (unsigned j = 0; j < neg.size(); ++j) {
-                    for (unsigned c = 0; 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);
-                        bool cont = dmn.contains(n_idx, neg[j], dmt, t_idx, dst[i], num_bits);
-                        IF_VERBOSE(
-                            3, 
-                            dmt.display(verbose_stream() << "dst:", dst[i], t_idx+num_bits-1,t_idx) << "\n";
-                            dmn.display(verbose_stream() << "neg:", neg[j], n_idx+num_bits-1,n_idx) << "\n";
-                            verbose_stream() << "contains: " << (cont?"true":"false") << "\n";);
-                        if (!cont) {
-                            goto next_neg_disj;
-                        }
+                    if (dmn.contains(neg[j], m_neg_cols, dst[i], m_t_cols)) {
+                        dmt.deallocate(&dst[i]);
+                        subsumed = true;
+                        break;
                     }
-                    dmt.deallocate(&dst[i]);
-                    goto next_disj;
-                next_neg_disj:;
                 }
-                result.push_back(&dst[i]);
-            next_disj:;
+                if (!subsumed)
+                    result.push_back(&dst[i]);
             }
             std::swap(dst, result);
             if (dst.is_empty()) {
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index 523d4e4db..094e755ac 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -148,6 +148,7 @@ public:
 
         test_rename();
         test_filter_neg();
+        test_filter_neg2();
 
 
         // empty
@@ -551,6 +552,55 @@ public:
         t2->deallocate();
     }
 
+    void test_filter_neg2() {
+        // filter_by_negation
+        relation_signature sig4;
+        sig4.push_back(bv.mk_sort(1));
+        sig4.push_back(bv.mk_sort(1));
+        sig4.push_back(bv.mk_sort(1));
+        unsigned_vector cols, allcols;
+
+        cols.push_back(0);
+        cols.push_back(2);
+        allcols.push_back(0);
+        allcols.push_back(1);
+        allcols.push_back(2);
+
+        /// xxx \ 1x0
+        udoc_relation* t1 = mk_full(sig4);
+        {
+            udoc_relation* neg = mk_full(sig4);
+            doc& n = neg->get_udoc()[0];
+            neg->get_dm().set(n, 0, BIT_1);
+            neg->get_dm().set(n, 2, BIT_0);
+            apply_filter_neg(*t1, *neg, allcols, allcols);
+            neg->deallocate();
+        }
+
+        /// xxx \ (1x1 u 0x0)
+        udoc_relation* t2 = mk_full(sig4);
+        {
+            udoc_relation* neg = mk_full(sig4);
+            doc& n = neg->get_udoc()[0];
+            neg->get_dm().set(n, 0, BIT_0);
+            neg->get_dm().set(n, 2, BIT_0);
+            apply_filter_neg(*t2, *neg, allcols, allcols);
+            neg->deallocate();
+        }
+        {
+            udoc_relation* neg = mk_full(sig4);
+            doc& n = neg->get_udoc()[0];
+            neg->get_dm().set(n, 0, BIT_1);
+            neg->get_dm().set(n, 2, BIT_1);
+            apply_filter_neg(*t2, *neg, allcols, allcols);
+            neg->deallocate();
+        }
+
+        apply_filter_neg(*t2, *t1, cols, cols);
+        t1->deallocate();
+        t2->deallocate();
+    }
+
     void set_random(udoc_relation& r, unsigned num_vals) {
         unsigned num_bits = r.get_dm().num_tbits();
         udoc_relation* full = mk_full(r.get_signature());