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

@@ -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;
                 }
             }

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

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 {

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;

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

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