remove mk_or_reduced

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

src/ast/ast.cpp

@@ -2058,13 +2058,6 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
     return r;
 }
 
-expr* ast_manager::mk_or_reduced(unsigned n, expr* const* args) {
-    switch (n) {
-    case 0: return mk_false();
-    case 1: return args[0];
-    default: return mk_or(n, args);
-    }
-}
 
 
 func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity, 

src/ast/ast.h

@@ -2004,7 +2004,6 @@ public:
     app * mk_true() { return m_true; }
     app * mk_false() { return m_false; }
     app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
-    expr * mk_or_reduced(unsigned num_args, expr * const * args);
 
 
     func_decl* mk_and_decl() { 

src/muz/ddnf/doc.h

@@ -157,6 +157,23 @@ public:
         std::swap(result, *this);
         result.reset(m);
     }
+    void subtract(M& m, union_bvec const& other) {
+        unsigned sz = other.size();
+        for (unsigned i = 0; !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) {     
         union_bvec negated;
         result.reset(m);

src/muz/ddnf/udoc_relation.cpp

@@ -444,9 +444,10 @@ namespace datalog {
         apply_guard(g, result, equalities, discard_cols);
     }
     void udoc_relation::apply_guard(
-        expr* g, udoc& result, subset_ints& equalities, 
+        expr* g, udoc& result, 
-        bit_vector const& discard_cols) {
+        subset_ints& equalities, bit_vector const& discard_cols) {
         ast_manager& m = get_plugin().get_ast_manager();
+        bv_util& bv = get_plugin().bv;
         expr* e1, *e2;
         if (result.empty()) {
         }
@@ -459,23 +460,17 @@ namespace datalog {
             udoc sub;
             sub.push_back(dm.allocateX());
             apply_guard(e1, sub, equalities, discard_cols);
-            // TBD: result.subtract(dm, sub);
+            result.subtract(dm, sub);
         }
         else if (m.is_or(g)) {
             udoc sub;
             sub.push_back(dm.allocateX());
             for (unsigned i = 0; !sub.empty() && i < to_app(g)->get_num_args(); ++i) {
                 expr_ref arg(m);
-                arg = to_app(g)->get_arg(i);
+                arg = mk_not(m, to_app(g)->get_arg(i));
-                if (m.is_not(arg, e1)) {
-                    arg = e1;
-                }
-                else {
-                    arg = m.mk_not(arg);
-                }
                 apply_guard(arg, result, equalities, discard_cols);
             }
-            // TBD: result.subtract(dm, sub);
+            result.subtract(dm, sub);
         }
         else if (m.is_true(g)) {
         }
@@ -491,37 +486,36 @@ namespace datalog {
             bit1 = dm1.tbv().allocate1();
             result.fix_eq_bits(idx, bit1.get(), 0, 1, equalities, discard_cols);
         }
-        else if (m.is_eq(g, e1, e2)) {
+        else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
-#if 0
+            unsigned hi, lo;
-            const var *v;
+            expr* e3;
-            unsigned vidx = 0;
+            // TBD: equalities and discard_cols?
-            unsigned length;
+            if (is_var(e1) && is_ground(e2)) {
-            
+                apply_eq(g, result, to_var(e1), bv.get_bv_size(e1)-1, 0, e2); 
-            unsigned low, high;
-            expr *e2;
-            if (is_var(e1)) {
-                v = to_var(e1);
-                length = column_num_bits(v->get_idx());
-            } else if (bv.is_extract(e1, low, high, e11)) {
-                vidx = bv.get_bv_size(e11) - high - 1;
-                length = high - low + 1;
-                SASSERT(is_var(e11));
-                v = to_var(e11);
-            } else {
-                NOT_IMPLEMENTED_YET();
             }
-            vidx += t.column_idx(v->get_idx());
+            else if (is_var(e2) && is_ground(e1)) {
-            
+                apply_eq(g, result, to_var(e2), bv.get_bv_size(e2)-1, 0, e1); 
-            unsigned final_idx = fix_eq_bits(vidx, e2, 0, length, t, equalities, discard_cols);
+            }
-            SASSERT(final_idx == vidx + length);
+            else if (bv.is_extract(e1, lo, hi, e3) && is_var(e3) && is_ground(e2)) {
-            (void)final_idx;
+                apply_eq(g, result, to_var(e3), hi, lo, e2);
-#endif
+            }
+            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);
+                // TBD
+            }   
+            else {
+                goto failure_case;
+            }            
         }
         else {
-            // std::ostringstream strm;
+        failure_case:
-            // strm << "Guard expression is not handled" << mk_pp(g, m);
+            std::ostringstream strm;
-            // throw default_exception(strm.str()); 
+            strm << "Guard expression is not handled" << mk_pp(g, m);
-            throw 0; 
+            throw default_exception(strm.str()); 
         }
     }
 
@@ -594,76 +588,4 @@ namespace datalog {
         return alloc(negation_filter_fn, get(t), get(neg), joined_col_cnt, t_cols, negated_cols);
     }
 
-#if 0
-        /// make bits of table [idx,idx+max_length]  equal to e sliced starting at idx2
-        unsigned fix_eq_bits(unsigned idx, expr *e, unsigned idx2, unsigned max_length,
-                             const table_information& t, subset_ints& equalities,
-                             const bit_vector & discard_cols) {
-            const bv_util& bvu = t.get_bv_util();
-            const dl_decl_util& dutil = t.get_decl_util();
-
-            rational n;
-            unsigned bv_size;
-            if (bvu.is_numeral(e, n, bv_size)) {
-                SASSERT(idx2 < bv_size);
-                max_length = std::min(max_length, bv_size - idx2);
-                T num(n, max_length);
-                fix_eq_bits(idx, &num, idx2, max_length, equalities, discard_cols);
-                return idx + max_length;
-            }
-
-            uint64 num;
-            if (dutil.is_numeral(e, num)) {
-                T num_bv(rational(num,rational::ui64()), max_length);
-                fix_eq_bits(idx, &num_bv, idx2, max_length, equalities, discard_cols);
-                return idx + max_length;
-            }
-
-            if (bvu.is_concat(e)) {
-                const app *a = to_app(e);
-
-                // skip the first elements of the concat if e.g. we have a top level extract
-                unsigned i = 0;
-                for (; i < a->get_num_args(); ++i) {
-                    unsigned arg_size = bvu.get_bv_size(a->get_arg(i));
-                    if (idx2 < arg_size)
-                        break;
-                    idx2 -= arg_size;
-                }
-
-                SASSERT(i < a->get_num_args());
-                for (; max_length > 0 && i < a->get_num_args(); ++i) {
-                    unsigned idx0 = idx;
-                    idx = fix_eq_bits(idx, a->get_arg(i), idx2, max_length, t, equalities, discard_cols);
-                    idx2 = 0;
-                    SASSERT((idx - idx0) <= max_length);
-                    max_length = max_length - (idx - idx0);
-                }
-                return idx;
-            }
-
-            unsigned low, high;
-            expr *e2;
-            if (bvu.is_extract(e, low, high, e2)) {
-                SASSERT(low <= high);
-                unsigned size = bvu.get_bv_size(e2);
-                unsigned offset = size - (high+1) + idx2;
-                SASSERT(idx2 < (high-low+1));
-                max_length = std::min(max_length, high - low + 1 - idx2);
-                return fix_eq_bits(idx, e2, offset, max_length, t, equalities, discard_cols);
-            }
-
-            if (e->get_kind() == AST_VAR) {
-                unsigned idx_var = idx2 + t.column_idx(to_var(e)->get_idx());
-                SASSERT(idx2 < t.column_num_bits(to_var(e)->get_idx()));
-                max_length = std::min(max_length, t.column_num_bits(to_var(e)->get_idx()) - idx2);
-                fix_eq_bits(idx, 0, idx_var, max_length, equalities, discard_cols);
-                return idx + max_length;
-            }
-
-            NOT_IMPLEMENTED_YET();
-            return 0;
-        }
-#endif
-
 }

src/muz/ddnf/udoc_relation.h

@@ -66,6 +66,7 @@ namespace datalog {
         void compile_guard(expr* g, udoc& d) const;
         void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols);
         void apply_guard(expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols);
+        void apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c);
     };
 
     class udoc_plugin : public relation_plugin {

src/tactic/arith/card2bv_tactic.cpp

@@ -23,6 +23,7 @@ Notes:
 #include"expr_substitution.h"
 #include"card2bv_tactic.h"
 #include"pb_rewriter.h"
+#include"ast_util.h"
 
 namespace pb {
     unsigned card2bv_rewriter::get_num_bits(func_decl* f) {
@@ -85,7 +86,7 @@ namespace pb {
     }
 
     void card2bv_rewriter::mk_clause(unsigned n, literal const* lits) {
-        m_lemmas.push_back(m.mk_or_reduced(n, lits));
+        m_lemmas.push_back(mk_or(m, n, lits));
     }