merge with Z3Prover/master

src/ast/rewriter/CMakeLists.txt

@@ -16,6 +16,7 @@ z3_add_component(rewriter
     enum2bv_rewriter.cpp
     expr_replacer.cpp
     expr_safe_replace.cpp
+    factor_equivs.cpp
     factor_rewriter.cpp
     fpa_rewriter.cpp
     inj_axiom.cpp
@@ -25,7 +26,6 @@ z3_add_component(rewriter
     pb_rewriter.cpp
     pb2bv_rewriter.cpp
     push_app_ite.cpp
-    pull_ite_tree.cpp
     quant_hoist.cpp
     rewriter.cpp
     seq_rewriter.cpp

src/ast/rewriter/arith_rewriter.cpp

@@ -800,9 +800,107 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu
         result = m_util.mk_numeral(div(v1, v2), is_int);
         return BR_DONE;
     }
+    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_one()) {
+        result = arg1;
+        return BR_DONE;
+    }
+    if (m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) {
+        return BR_FAILED;
+    }
+    if (arg1 == arg2) {
+        expr_ref zero(m_util.mk_int(0), m());
+        result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1));
+        return BR_REWRITE3;
+    }
+    if (divides(arg1, arg2, result)) {
+        return BR_REWRITE_FULL;
+    }
     return BR_FAILED;
 }
 
+
+// 
+// implement div ab ac = floor( ab / ac) = floor (b / c) = div b c
+//
+bool arith_rewriter::divides(expr* num, expr* den, expr_ref& result) {
+    expr_fast_mark1 mark;
+    rational num_r(1), den_r(1);
+    expr* num_e = nullptr, *den_e = nullptr;
+    ptr_buffer<expr> args1, args2;
+    flat_mul(num, args1);
+    flat_mul(den, args2);
+    for (expr * arg : args1) {
+        mark.mark(arg);
+        if (m_util.is_numeral(arg, num_r)) num_e = arg;
+    }
+    for (expr* arg : args2) {
+        if (mark.is_marked(arg)) {
+            result = remove_divisor(arg, num, den);
+            return true;
+        }
+        if (m_util.is_numeral(arg, den_r)) den_e = arg;
+    }
+    rational g = gcd(num_r, den_r);
+    if (!g.is_one()) {
+        SASSERT(g.is_pos());
+        // replace num_e, den_e by their gcd reduction.
+        for (unsigned i = 0; i < args1.size(); ++i) {
+            if (args1[i] == num_e) {
+                args1[i] = m_util.mk_numeral(num_r / g, true);
+                break;
+            }
+        }
+        for (unsigned i = 0; i < args2.size(); ++i) {
+            if (args2[i] == den_e) {
+                args2[i] = m_util.mk_numeral(den_r / g, true);
+                break;
+            }
+        }
+        
+        num = m_util.mk_mul(args1.size(), args1.c_ptr());
+        den = m_util.mk_mul(args2.size(), args2.c_ptr());
+        result = m_util.mk_idiv(num, den);
+        return true;
+    }
+    return false;
+}
+
+expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) {
+    ptr_buffer<expr> args1, args2;
+    flat_mul(num, args1);
+    flat_mul(den, args2);
+    remove_divisor(arg, args1);
+    remove_divisor(arg, args2);
+    expr_ref zero(m_util.mk_int(0), m());
+    num = args1.empty() ? m_util.mk_int(1) : m_util.mk_mul(args1.size(), args1.c_ptr());
+    den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.c_ptr());
+    return expr_ref(m().mk_ite(m().mk_eq(zero, arg), m_util.mk_idiv(zero, zero), m_util.mk_idiv(num, den)), m());
+}
+
+void arith_rewriter::flat_mul(expr* e, ptr_buffer<expr>& args) {
+    args.push_back(e);
+    for (unsigned i = 0; i < args.size(); ++i) {
+        e = args[i];
+        if (m_util.is_mul(e)) {
+            args.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+            args[i] = args.back();
+            args.shrink(args.size()-1);
+            --i;
+        }                
+    }
+}
+
+void arith_rewriter::remove_divisor(expr* d, ptr_buffer<expr>& args) {
+    for (unsigned i = 0; i < args.size(); ++i) {
+        if (args[i] == d) {
+            args[i] = args.back();
+            args.shrink(args.size()-1);
+            return;
+        }
+    }
+    UNREACHABLE();
+}
+
 br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
     set_curr_sort(m().get_sort(arg1));
     numeral v1, v2;
@@ -1056,7 +1154,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
 
 br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
     numeral a;
-    expr* x = 0;
+    expr* x = nullptr;
     if (m_util.is_numeral(arg, a)) {
         result = m_util.mk_numeral(floor(a), true);
         return BR_DONE;
@@ -1303,7 +1401,7 @@ expr * arith_rewriter::mk_sin_value(rational const & k) {
         expr * result = m_util.mk_div(m_util.mk_add(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false));
         return neg ? m_util.mk_uminus(result) : result;
     }
-    return 0;
+    return nullptr;
 }
 
 br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
@@ -1327,7 +1425,7 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
 
     if (is_pi_multiple(arg, k)) {
         result = mk_sin_value(k);
-        if (result.get() != 0)
+        if (result.get() != nullptr)
             return BR_REWRITE_FULL;
     }
 
@@ -1386,7 +1484,7 @@ br_status arith_rewriter::mk_cos_core(expr * arg, expr_ref & result) {
     if (is_pi_multiple(arg, k)) {
         k = k + rational(1, 2);
         result = mk_sin_value(k);
-        if (result.get() != 0)
+        if (result.get() != nullptr)
             return BR_REWRITE_FULL;
     }
 
@@ -1443,7 +1541,7 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) {
     if (is_pi_multiple(arg, k)) {
         expr_ref n(m()), d(m());
         n = mk_sin_value(k);
-        if (n.get() == 0)
+        if (n.get() == nullptr)
             goto end;
         if (is_zero(n)) {
             result = n;

src/ast/rewriter/arith_rewriter.h

@@ -95,6 +95,10 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
     expr_ref neg_monomial(expr * e) const;
     expr * mk_sin_value(rational const & k);
     app * mk_sqrt(rational const & k);
+    bool divides(expr* d, expr* n, expr_ref& result);
+    expr_ref remove_divisor(expr* arg, expr* num, expr* den);
+    void flat_mul(expr* e, ptr_buffer<expr>& args);
+    void remove_divisor(expr* d, ptr_buffer<expr>& args);
 
 public:
     arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):

src/ast/rewriter/bit2int.cpp

@@ -273,7 +273,7 @@ void bit2int::visit(app* n) {
     // bv2int(x) <= z - bv2int(y) -> bv2int(x) + bv2int(y) <= z
     //
     
-    expr* e1 = 0, *e2 = 0;
+    expr* e1 = nullptr, *e2 = nullptr;
     expr_ref tmp1(m_manager), tmp2(m_manager);
     expr_ref tmp3(m_manager);
     expr_ref pos1(m_manager), neg1(m_manager);

src/ast/rewriter/bit2int.h

@@ -77,7 +77,7 @@ protected:
     bool mk_add(expr* e1, expr* e2, expr_ref& result);
 
     expr * get_cached(expr * n) const;
-    bool is_cached(expr * n) const {  return get_cached(n) != 0; }
+    bool is_cached(expr * n) const {  return get_cached(n) != nullptr; }
     void cache_result(expr * n, expr * r);
     void reset_cache() { m_cache.reset(); }
     void flush_cache() { m_cache.cleanup(); }

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp

@@ -92,6 +92,8 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
     func_decl_ref_vector                     m_keys;
     expr_ref_vector                          m_values;
     unsigned_vector                          m_keyval_lim;
+    func_decl_ref_vector                     m_newbits;
+    unsigned_vector                          m_newbits_lim;
 
     bool                                     m_blast_mul;
     bool                                     m_blast_add;
@@ -118,7 +120,8 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
         m_out(m),
         m_bindings(m),
         m_keys(m),
-        m_values(m) {
+        m_values(m),
+        m_newbits(m) {
         updt_params(p);
     }
 
@@ -160,6 +163,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
 
     void push() {
         m_keyval_lim.push_back(m_keys.size());
+        m_newbits_lim.push_back(m_newbits.size());
     }
 
     unsigned get_num_scopes() const {
@@ -178,9 +182,27 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
             m_keys.resize(lim);
             m_values.resize(lim);
             m_keyval_lim.resize(new_sz);
+
+            lim = m_newbits_lim[new_sz];
+            m_newbits.shrink(lim);
+            m_newbits_lim.shrink(new_sz);
         }
     }
 
+    unsigned m_keypos;
+
+    void start_rewrite() {
+        m_keypos = m_keys.size();
+    }
+
+    void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
+        for (unsigned i = m_keypos; i < m_keys.size(); ++i) {
+            const2bits.insert(m_keys[i].get(), m_values[i].get());
+        }
+        for (func_decl* f : m_newbits) newbits.push_back(f);
+        
+    }
+
     template<typename V>
     app * mk_mkbv(V const & bits) {
         return m().mk_app(butil().get_family_id(), OP_MKBV, bits.size(), bits.c_ptr());
@@ -200,7 +222,8 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
         sort * b = m().mk_bool_sort();
         m_out.reset();
         for (unsigned i = 0; i < bv_size; i++) {
-            m_out.push_back(m().mk_fresh_const(0, b));
+            m_out.push_back(m().mk_fresh_const(nullptr, b));
+            m_newbits.push_back(to_app(m_out.back())->get_decl());
         }
         r = mk_mkbv(m_out);
         m_const2bits.insert(f, r);
@@ -342,11 +365,11 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             bits.push_back(m().mk_app(butil().get_family_id(), OP_BIT2BOOL, 1, &p, 1, &t));
         }
         result    = mk_mkbv(bits);
-        result_pr = 0;
+        result_pr = nullptr;
     }
 
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-        result_pr = 0;
+        result_pr = nullptr;
         TRACE("bit_blaster", tout << f->get_name() << " ";
               for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " ";
               tout << "\n";);
@@ -569,7 +592,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             if (t->get_idx() >= m_bindings.size())
                 return false;
             result = m_bindings.get(m_bindings.size() - t->get_idx() - 1);
-            result_pr = 0;
+            result_pr = nullptr;
             return true;
         }
 
@@ -616,7 +639,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
         result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
                                    new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
                                    old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
-        result_pr = 0;
+        result_pr = nullptr;
         m_bindings.shrink(old_sz);
         return true;
     }
@@ -635,6 +658,8 @@ struct bit_blaster_rewriter::imp : public rewriter_tpl<blaster_rewriter_cfg> {
     }
     void push() { m_cfg.push(); }
     void pop(unsigned s) { m_cfg.pop(s); }
+    void start_rewrite() { m_cfg.start_rewrite(); }
+    void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) { m_cfg.end_rewrite(const2bits, newbits); }
     unsigned get_num_scopes() const { return m_cfg.get_num_scopes(); }
 };
 
@@ -683,3 +708,10 @@ unsigned bit_blaster_rewriter::get_num_scopes() const {
     return m_imp->get_num_scopes();
 }
 
+void bit_blaster_rewriter::start_rewrite() {
+    m_imp->start_rewrite();
+}
+
+void bit_blaster_rewriter::end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits) {
+    m_imp->end_rewrite(const2bits, newbits);
+}

src/ast/rewriter/bit_blaster/bit_blaster_rewriter.h

@@ -33,11 +33,15 @@ public:
     ast_manager & m() const;
     unsigned get_num_steps() const;
     void cleanup();
-    obj_map<func_decl, expr*> const& const2bits() const; 
+    void start_rewrite();
+    void end_rewrite(obj_map<func_decl, expr*>& const2bits, ptr_vector<func_decl> & newbits);
     void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
     void push();
     void pop(unsigned num_scopes);
     unsigned get_num_scopes() const;
+private:
+    obj_map<func_decl, expr*> const& const2bits() const;     
+
 };
 
 #endif

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -1193,7 +1193,6 @@ bool bit_blaster_tpl<Cfg>::mk_const_case_multiplier(unsigned sz, expr * const *
         return false;
     }
     SASSERT(out_bits.empty());
-    
     ptr_buffer<expr, 128> na_bits;
     na_bits.append(sz, a_bits);
     ptr_buffer<expr, 128> nb_bits;

src/ast/rewriter/bool_rewriter.cpp

@@ -39,7 +39,6 @@ br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
     SASSERT(f->get_family_id() == m().get_basic_family_id());
     switch (f->get_decl_kind()) {
     case OP_EQ:
-    case OP_IFF:
         SASSERT(num_args == 2);
         return mk_eq_core(args[0], args[1], result);
     case OP_DISTINCT:
@@ -428,7 +427,7 @@ bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, exp
         neg = true;
         t = to_app(t)->get_arg(0);
     }
-    if (m().is_iff(t) || m().is_eq(t)) {
+    if (m().is_eq(t)) {
         bool modified = false;
         expr * new_lhs = simp_arg(to_app(t)->get_arg(0), neg_lits, pos_lits, modified);
         expr * new_rhs = simp_arg(to_app(t)->get_arg(1), neg_lits, pos_lits, modified);
@@ -585,7 +584,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
 
 */
 br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) {
-    expr* cond = 0, *t = 0, *e = 0;
+    expr* cond = nullptr, *t = nullptr, *e = nullptr;
     VERIFY(m().is_ite(ite, cond, t, e));
     SASSERT(m().is_value(val));
 
@@ -708,7 +707,7 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
 
         expr *la, *lb, *ra, *rb;
         // fold (iff (iff a b) (iff (not a) b)) to false
-        if (m().is_iff(lhs, la, lb) && m().is_iff(rhs, ra, rb)) {
+        if (m().is_eq(lhs, la, lb) && m().is_eq(rhs, ra, rb)) {
             expr *n;
             if ((la == ra && ((m().is_not(rb, n) && n == lb) ||
                 (m().is_not(lb, n) && n == rb))) ||

src/ast/rewriter/bool_rewriter.h

@@ -81,7 +81,7 @@ public:
     bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_local_ctx_cost(0) { updt_params(p); }
     ast_manager & m() const { return m_manager; }
     family_id get_fid() const { return m().get_basic_family_id(); }
-    bool is_eq(expr * t) const { return m().is_eq(t) || m().is_iff(t); }
+    bool is_eq(expr * t) const { return m().is_eq(t); }
     
     bool flat() const { return m_flat; }
     void set_flat(bool f) { m_flat = f; }
@@ -183,7 +183,7 @@ struct bool_rewriter_cfg : public default_rewriter_cfg {
     bool flat_assoc(func_decl * f) const { return m_r.flat() && (m_r.m().is_and(f) || m_r.m().is_or(f)); }
     bool rewrite_patterns() const { return false; }
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-        result_pr = 0;
+        result_pr = nullptr;
         if (f->get_family_id() != m_r.get_fid())
             return BR_FAILED;
         return m_r.mk_app_core(f, num, args, result);

src/ast/rewriter/bv_bounds.cpp

@@ -200,7 +200,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
         }
 
         // v + c1 <= v + c2
-        app * v1(NULL), *v2(NULL);
+        app * v1(nullptr), *v2(nullptr);
         numeral val1, val2;
         if (is_constant_add(bv_sz, lhs, v1, val1)
                 && is_constant_add(bv_sz, rhs, v2, val2)
@@ -412,7 +412,7 @@ bool bv_bounds::add_constraint(expr* e) {
         }
 
         // v + c1 <= v + c2
-        app * v1(NULL), *v2(NULL);
+        app * v1(nullptr), *v2(nullptr);
         numeral val1, val2;
         if (is_constant_add(bv_sz, lhs, v1, val1)
                 && is_constant_add(bv_sz, rhs, v2, val2)
@@ -449,7 +449,7 @@ bool bv_bounds::add_constraint(expr* e) {
     return m_okay;
 }
 
-bool bv_bounds::add_bound_unsigned(app * v, numeral a, numeral b, bool negate) {
+bool bv_bounds::add_bound_unsigned(app * v, const numeral& a, const numeral& b, bool negate) {
     TRACE("bv_bounds", tout << "bound_unsigned " << mk_ismt2_pp(v, m_m) << ": " << (negate ? "~[" : "[") << a << ";" << b << "]" << std::endl;);
     const unsigned bv_sz = m_bv_util.get_bv_size(v);
     const numeral& zero = numeral::zero();
@@ -472,7 +472,7 @@ bool bv_bounds::add_bound_unsigned(app * v, numeral a, numeral b, bool negate) {
     }
 }
 
-bv_bounds::conv_res bv_bounds::convert_signed(app * v, numeral a, numeral b, bool negate, vector<ninterval>& nis) {
+bv_bounds::conv_res bv_bounds::convert_signed(app * v, const numeral& a, const numeral& b, bool negate, vector<ninterval>& nis) {
     TRACE("bv_bounds", tout << "convert_signed " << mk_ismt2_pp(v, m_m) << ":" << (negate ? "~[" : "[") << a << ";" << b << "]" << std::endl;);
     const unsigned bv_sz = m_bv_util.get_bv_size(v);
     SASSERT(a <= b);
@@ -496,7 +496,7 @@ bv_bounds::conv_res bv_bounds::convert_signed(app * v, numeral a, numeral b, boo
     }
 }
 
-bool bv_bounds::add_bound_signed(app * v, numeral a, numeral b, bool negate) {
+bool bv_bounds::add_bound_signed(app * v, const numeral& a, const numeral& b, bool negate) {
     TRACE("bv_bounds", tout << "bound_signed " << mk_ismt2_pp(v, m_m) << ":" << (negate ? "~" : " ") << a << ";" << b << std::endl;);
     const unsigned bv_sz = m_bv_util.get_bv_size(v);
     SASSERT(a <= b);
@@ -519,7 +519,7 @@ bool bv_bounds::add_bound_signed(app * v, numeral a, numeral b, bool negate) {
     }
 }
 
-bool bv_bounds::bound_lo(app * v, numeral l) {
+bool bv_bounds::bound_lo(app * v, const numeral& l) {
     SASSERT(in_range(v, l));
     TRACE("bv_bounds", tout << "lower " << mk_ismt2_pp(v, m_m) << ":" << l << std::endl;);
     // l <= v
@@ -530,7 +530,7 @@ bool bv_bounds::bound_lo(app * v, numeral l) {
     return m_okay;
 }
 
-bool bv_bounds::bound_up(app * v, numeral u) {
+bool bv_bounds::bound_up(app * v, const numeral& u) {
     SASSERT(in_range(v, u));
     TRACE("bv_bounds", tout << "upper " << mk_ismt2_pp(v, m_m) << ":" << u << std::endl;);
     // v <= u
@@ -541,7 +541,7 @@ bool bv_bounds::bound_up(app * v, numeral u) {
     return m_okay;
 }
 
-bool bv_bounds::add_neg_bound(app * v, numeral a, numeral b) {
+bool bv_bounds::add_neg_bound(app * v, const numeral& a, const numeral& b) {
     TRACE("bv_bounds", tout << "negative bound " << mk_ismt2_pp(v, m_m) << ":" << a << ";" << b << std::endl;);
     bv_bounds::interval negative_interval(a, b);
     SASSERT(m_bv_util.is_bv(v));
@@ -550,8 +550,8 @@ bool bv_bounds::add_neg_bound(app * v, numeral a, numeral b) {
     SASSERT(a <= b);
 
     intervals_map::obj_map_entry * const e = m_negative_intervals.find_core(v);
-    intervals * ivs(NULL);
-    if (e == 0) {
+    intervals * ivs(nullptr);
+    if (e == nullptr) {
         ivs = alloc(intervals);
         m_negative_intervals.insert(v, ivs);
     }
@@ -621,7 +621,7 @@ bool bv_bounds::is_sat_core(app * v) {
     if (!has_lower) lower = numeral::zero();
     if (!has_upper) upper = (numeral::power_of_two(bv_sz) - one);
     TRACE("bv_bounds", tout << "is_sat bound:" << lower << "-" << upper << std::endl;);
-    intervals * negative_intervals(NULL);
+    intervals * negative_intervals(nullptr);
     const bool has_neg_intervals = m_negative_intervals.find(v, negative_intervals);
     bool is_sat(false);
     numeral new_lo = lower;

src/ast/rewriter/bv_bounds.h

@@ -49,11 +49,11 @@ public: // bounds addition methods
     **/
     bool add_constraint(expr* e);
 
-    bool bound_up(app * v, numeral u); // v <= u
-    bool bound_lo(app * v, numeral l); // l <= v
-    inline bool add_neg_bound(app * v, numeral a, numeral b); // not (a<=v<=b)
-    bool add_bound_signed(app * v, numeral a, numeral b, bool negate);
-    bool add_bound_unsigned(app * v, numeral a, numeral b, bool negate);
+    bool bound_up(app * v, const numeral& u); // v <= u
+    bool bound_lo(app * v, const numeral& l); // l <= v
+    inline bool add_neg_bound(app * v, const numeral& a, const numeral& b); // not (a<=v<=b)
+    bool add_bound_signed(app * v, const numeral& a, const numeral& b, bool negate);
+    bool add_bound_unsigned(app * v, const numeral& a, const numeral& b, bool negate);
 public:
     bool is_sat();  ///< Determine if the set of considered constraints is satisfiable.
     bool is_okay();
@@ -70,7 +70,7 @@ protected:
     enum conv_res { CONVERTED, UNSAT, UNDEF };
     conv_res convert(expr * e, vector<ninterval>& nis, bool negated);
     conv_res record(app * v, numeral lo, numeral hi, bool negated, vector<ninterval>& nis);
-    conv_res convert_signed(app * v, numeral a, numeral b, bool negate, vector<ninterval>& nis);
+    conv_res convert_signed(app * v, const numeral& a, const numeral& b, bool negate, vector<ninterval>& nis);
 
     typedef vector<interval>            intervals;
     typedef obj_map<app, intervals*>    intervals_map;
@@ -83,7 +83,7 @@ protected:
     bool                      m_okay;
     bool                      is_sat(app * v);
 bool                      is_sat_core(app * v);
-    inline bool               in_range(app *v, numeral l);
+    inline bool               in_range(app *v, const numeral& l);
     inline bool               is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val);
     void                      record_singleton(app * v,  numeral& singleton_value);
     inline bool               to_bound(const expr * e) const;
@@ -99,7 +99,7 @@ inline bool bv_bounds::to_bound(const expr * e) const {
        && !m_bv_util.is_numeral(e);
 }
 
-inline bool bv_bounds::in_range(app *v, bv_bounds::numeral n) {
+inline bool bv_bounds::in_range(app *v, const bv_bounds::numeral& n) {
     const unsigned bv_sz = m_bv_util.get_bv_size(v);
     const bv_bounds::numeral zero(0);
     const bv_bounds::numeral mod(rational::power_of_two(bv_sz));
@@ -109,7 +109,7 @@ inline bool bv_bounds::in_range(app *v, bv_bounds::numeral n) {
 inline bool bv_bounds::is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val) {
     SASSERT(e && !v);
     SASSERT(m_bv_util.get_bv_size(e) == bv_sz);
-    expr *lhs(NULL), *rhs(NULL);
+    expr *lhs(nullptr), *rhs(nullptr);
     if (!m_bv_util.is_bv_add(e, lhs, rhs)) {
         v = to_app(e);
         val = rational(0);

src/ast/rewriter/bv_elim.cpp

@@ -58,7 +58,7 @@ bool bv_elim_cfg::reduce_quantifier(quantifier * q,
                 _sorts.push_back(m.mk_bool_sort());
                 _names.push_back(symbol(new_name.str().c_str()));
             }
-            bv = m.mk_app(bfid, OP_MKBV, 0, 0, args.size(), args.c_ptr());
+            bv = m.mk_app(bfid, OP_MKBV, 0, nullptr, args.size(), args.c_ptr());
             _subst_map.push_back(bv.get());
         }
         else {

src/ast/rewriter/bv_rewriter.cpp

@@ -630,13 +630,13 @@ unsigned bv_rewriter::propagate_extract(unsigned high, expr * arg, expr_ref & re
         const bool curr_is_conc = m_util.is_concat(curr);
         if (curr_is_conc && to_app(curr)->get_num_args() == 0) continue;
         expr * const curr_first = curr_is_conc ? to_app(curr)->get_arg(0) : curr;
-        expr * new_first = NULL;
+        expr * new_first = nullptr;
         if (is_numeral(curr_first, val, curr_first_sz)) {
             SASSERT(curr_first_sz >= removable);
             const unsigned new_num_sz = curr_first_sz - removable;
-            new_first = new_num_sz ? mk_numeral(val, new_num_sz) : NULL;
+            new_first = new_num_sz ? mk_numeral(val, new_num_sz) : nullptr;
         }
-        expr * new_arg = NULL;
+        expr * new_arg = nullptr;
         if (curr_is_conc) {
             const unsigned conc_num = to_app(curr)->get_num_args();
             if (new_first) {
@@ -650,7 +650,7 @@ unsigned bv_rewriter::propagate_extract(unsigned high, expr * arg, expr_ref & re
                 expr * const * const old_conc_args = to_app(curr)->get_args();
                 switch (conc_num) {
                     case 0: UNREACHABLE(); break;
-                    case 1: new_arg = NULL; break;
+                    case 1: new_arg = nullptr; break;
                     case 2: new_arg = to_app(curr)->get_arg(1); break;
                     default: new_arg = m_util.mk_concat(conc_num - 1, old_conc_args + 1);
                 }
@@ -680,8 +680,8 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_
         if (v.is_neg())
             mod(v, rational::power_of_two(sz), v);
         if (v.is_uint64()) {
-            uint64 u  = v.get_uint64();
-            uint64 e  = shift_right(u, low) & (shift_left(1ull, sz) - 1ull);
+            uint64_t u  = v.get_uint64();
+            uint64_t e  = shift_right(u, low) & (shift_left(1ull, sz) - 1ull);
             result    = mk_numeral(numeral(e, numeral::ui64()), sz);
             return BR_DONE;
         }
@@ -811,7 +811,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) {
                 SASSERT(r1.is_uint64() && r2.is_uint64());
                 SASSERT(r2.get_uint64() < bv_size);
 
-                uint64 r = shift_left(r1.get_uint64(), r2.get_uint64());
+                uint64_t r = shift_left(r1.get_uint64(), r2.get_uint64());
                 numeral rn(r, numeral::ui64());
                 rn = m_util.norm(rn, bv_size);
                 result   = mk_numeral(rn, bv_size);
@@ -860,7 +860,7 @@ br_status bv_rewriter::mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result) {
             if (bv_size <= 64) {
                 SASSERT(r1.is_uint64());
                 SASSERT(r2.is_uint64());
-                uint64 r = shift_right(r1.get_uint64(), r2.get_uint64());
+                uint64_t r = shift_right(r1.get_uint64(), r2.get_uint64());
                 numeral rn(r, numeral::ui64());
                 rn = m_util.norm(rn, bv_size);
                 result = mk_numeral(rn, bv_size);
@@ -902,11 +902,11 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
     bool is_num1 = is_numeral(arg1, r1, bv_size);
 
     if (bv_size <= 64 && is_num1 && is_num2) {
-        uint64 n1      = r1.get_uint64();
-        uint64 n2_orig = r2.get_uint64();
-        uint64 n2      = n2_orig % bv_size;
+        uint64_t n1      = r1.get_uint64();
+        uint64_t n2_orig = r2.get_uint64();
+        uint64_t n2      = n2_orig % bv_size;
         SASSERT(n2 < bv_size);
-        uint64 r       = shift_right(n1, n2);
+        uint64_t r       = shift_right(n1, n2);
         bool   sign    = (n1 & shift_left(1ull, bv_size - 1ull)) != 0;
         if (n2_orig > n2) {
             if (sign) {
@@ -917,9 +917,9 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) {
             }
         }
         else if (sign) {
-            uint64 allone  = shift_left(1ull, bv_size) - 1ull;
-            uint64 mask    = ~(shift_left(1ull, bv_size - n2) - 1ull);
-            mask          &= allone;
+            uint64_t allone = shift_left(1ull, bv_size) - 1ull;
+            uint64_t mask   = ~(shift_left(1ull, bv_size - n2) - 1ull);
+            mask &= allone;
             r |= mask;
         }
         result = mk_numeral(numeral(r, numeral::ui64()), bv_size);
@@ -1458,10 +1458,10 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
     bool fused_extract = false;
     for (unsigned i = 0; i < num_args; i++) {
         expr * arg = args[i];
-        expr * prev = 0;
+        expr * prev = nullptr;
         if (i > 0)
             prev = new_args.back();
-        if (is_numeral(arg, v1, sz1) && prev != 0 && is_numeral(prev, v2, sz2)) {
+        if (is_numeral(arg, v1, sz1) && prev != nullptr && is_numeral(prev, v2, sz2)) {
             v2  *= rational::power_of_two(sz1);
             v2  += v1;
             new_args.pop_back();
@@ -1476,7 +1476,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
             expanded = true;
         }
         else if (m_util.is_extract(arg) &&
-                 prev != 0 &&
+                 prev != nullptr &&
                  m_util.is_extract(prev) &&
                  to_app(arg)->get_arg(0) == to_app(prev)->get_arg(0) &&
                  m_util.get_extract_low(prev) == m_util.get_extract_high(arg) + 1) {
@@ -1814,7 +1814,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
     //
     if (!v1.is_zero() && num_coeffs == num - 1) {
         // find argument that is not a numeral
-        expr * t = 0;
+        expr * t = nullptr;
         for (unsigned i = 0; i < num; i++) {
             t = args[i];
             if (!is_numeral(t))
@@ -1937,7 +1937,7 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
     }
 
     if (m_bvnot_simpl) {
-        expr *s(0), *t(0);
+        expr *s(nullptr), *t(nullptr);
         if (m_util.is_bv_mul(arg, s, t)) {
             // ~(-1 * x) --> (x - 1)
             bv_size = m_util.get_bv_size(s);
@@ -2021,7 +2021,7 @@ br_status bv_rewriter::mk_bv_ext_rotate_left(expr * arg1, expr * arg2, expr_ref
     numeral r2;
     unsigned bv_size;
     if (is_numeral(arg2, r2, bv_size)) {
-        unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64>(bv_size));
+        unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64_t>(bv_size));
         return mk_bv_rotate_left(shift, arg1, result);
     }
     return BR_FAILED;
@@ -2031,7 +2031,7 @@ br_status bv_rewriter::mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref
     numeral r2;
     unsigned bv_size;
     if (is_numeral(arg2, r2, bv_size)) {
-        unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64>(bv_size));
+        unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64_t>(bv_size));
         return mk_bv_rotate_right(shift, arg1, result);
     }
     return BR_FAILED;

src/ast/rewriter/bv_trailing.cpp

@@ -39,7 +39,7 @@ struct bv_trailing::imp {
         TRACE("bv-trailing", tout << "ctor\n";);
 
             for (unsigned i = 0; i <= TRAILING_DEPTH; ++i)
-                m_count_cache[i] = NULL;
+                m_count_cache[i] = nullptr;
     }
 
     virtual ~imp() {
@@ -116,7 +116,7 @@ struct bv_trailing::imp {
         const unsigned sz = m_util.get_bv_size(a);
 
         if (to_rm == sz) {
-            result = NULL;
+            result = nullptr;
             return sz;
         }
 
@@ -155,7 +155,7 @@ struct bv_trailing::imp {
         const unsigned new_sz = sz - retv;
 
         if (!new_sz) {
-            result = NULL;
+            result = nullptr;
             return retv;
         }
 
@@ -181,7 +181,7 @@ struct bv_trailing::imp {
         const unsigned num  = a->get_num_args();
         unsigned retv = 0;
         unsigned i = num;
-        expr_ref new_last(NULL, m);
+        expr_ref new_last(nullptr, m);
         while (i && retv < n) {
             i--;
             expr * const curr = a->get_arg(i);
@@ -197,7 +197,7 @@ struct bv_trailing::imp {
 
         if (!i && !new_last) {// all args eaten completely
             SASSERT(retv == m_util.get_bv_size(a));
-            result = NULL;
+            result = nullptr;
             return retv;
         }
 
@@ -230,7 +230,7 @@ struct bv_trailing::imp {
         if (m_util.is_numeral(e, e_val, sz)) {
             retv = remove_trailing(std::min(n, sz), e_val);
             const unsigned new_sz = sz - retv;
-            result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : NULL;
+            result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : nullptr;
             return retv;
         }
         if (m_util.is_bv_mul(e))
@@ -338,7 +338,7 @@ struct bv_trailing::imp {
     void cache(unsigned depth, expr * e, unsigned min, unsigned max) {
         SASSERT(depth <= TRAILING_DEPTH);
         if (depth == 0) return;
-        if (m_count_cache[depth] == NULL)
+        if (m_count_cache[depth] == nullptr)
             m_count_cache[depth] = alloc(map);
         SASSERT(!m_count_cache[depth]->contains(e));
         m.inc_ref(e);
@@ -353,10 +353,10 @@ struct bv_trailing::imp {
             max = m_util.get_bv_size(e);
             return true;
         }
-        if (m_count_cache[depth] == NULL)
+        if (m_count_cache[depth] == nullptr)
             return false;
         const map::obj_map_entry * const oe = m_count_cache[depth]->find_core(e);
-        if (oe == NULL) return false;
+        if (oe == nullptr) return false;
         min = oe->get_data().m_value.first;
         max = oe->get_data().m_value.second;
         TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
@@ -366,7 +366,7 @@ struct bv_trailing::imp {
     void reset_cache(const unsigned condition) {
         SASSERT(m_count_cache[0] == NULL);
         for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) {
-            if (m_count_cache[i] == NULL) continue;
+            if (m_count_cache[i] == nullptr) continue;
             TRACE("bv-trailing", tout << "may reset cache " << i << " " << condition <<  "\n";);
             if (condition && m_count_cache[i]->size() < condition) continue;
             TRACE("bv-trailing", tout << "reset cache " << i << "\n";);
@@ -374,7 +374,7 @@ struct bv_trailing::imp {
             map::iterator end = m_count_cache[i]->end();
             for (; it != end; ++it) m.dec_ref(it->m_key);
             dealloc(m_count_cache[i]);
-            m_count_cache[i] = NULL;
+            m_count_cache[i] = nullptr;
         }
     }
 

src/ast/rewriter/datatype_rewriter.cpp

@@ -23,6 +23,9 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
     switch(f->get_decl_kind()) {
     case OP_DT_CONSTRUCTOR: return BR_FAILED;
     case OP_DT_RECOGNISER:
+        SASSERT(num_args == 1);
+        result = m_util.mk_is(m_util.get_recognizer_constructor(f), args[0]);
+        return BR_REWRITE1;
     case OP_DT_IS:
         //
         // simplify is_cons(cons(x,y)) -> true

src/ast/rewriter/der.cpp

@@ -40,11 +40,8 @@ static bool is_neg_var(ast_manager & m, expr * e, unsigned num_decls) {
 */
 bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
     // (not (= VAR t)) and (not (iff VAR t)) cases
-    if (m_manager.is_not(e) && (m_manager.is_eq(to_app(e)->get_arg(0)) || m_manager.is_iff(to_app(e)->get_arg(0)))) {
-        app * eq   = to_app(to_app(e)->get_arg(0));
-        SASSERT(m_manager.is_eq(eq) || m_manager.is_iff(eq));
-        expr * lhs = eq->get_arg(0);
-        expr * rhs = eq->get_arg(1);
+    expr *eq, * lhs, *rhs;
+    if (m_manager.is_not(e, eq) && m_manager.is_eq(eq, lhs, rhs)) {
         if (!is_var(lhs, num_decls) && !is_var(rhs, num_decls))
             return false;
         if (!is_var(lhs, num_decls))
@@ -60,9 +57,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
         return true;
     }
     // (iff VAR t) and (iff (not VAR) t) cases
-    else if (m_manager.is_iff(e)) {
-        expr * lhs = to_app(e)->get_arg(0);
-        expr * rhs = to_app(e)->get_arg(1);
+    else if (m_manager.is_eq(e, lhs, rhs) && m_manager.is_bool(lhs)) {
         // (iff VAR t) case
         if (is_var(lhs, num_decls) || is_var(rhs, num_decls)) {
             if (!is_var(lhs, num_decls))
@@ -118,7 +113,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
 
 void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
     bool reduced = false;
-    pr = 0;
+    pr = nullptr;
     r  = q;
 
     TRACE("der", tout << mk_pp(q, m_manager) << "\n";);
@@ -149,14 +144,14 @@ void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
 
 void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
     if (!is_forall(q)) {
-        pr = 0;
+        pr = nullptr;
         r  = q;
         return;
     }
 
     expr * e = q->get_expr();
     unsigned num_decls = q->get_num_decls();
-    var * v = 0;
+    var * v = nullptr;
     expr_ref t(m_manager);
 
     if (m_manager.is_or(e)) {
@@ -211,7 +206,7 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
         r = q;
 
     if (m_manager.proofs_enabled()) {
-        pr = r == q ? 0 : m_manager.mk_der(q, r);
+        pr = r == q ? nullptr : m_manager.mk_der(q, r);
     }
 }
 
@@ -223,7 +218,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
     for (unsigned i = 0; i < definitions.size(); i++) {
         var * v  = vars[i];
         expr * t = definitions[i];
-        if (t == 0 || has_quantifiers(t) || occurs(v, t))
+        if (t == nullptr || has_quantifiers(t) || occurs(v, t))
             definitions[i] = 0;
         else
             found = true; // found at least one candidate
@@ -260,7 +255,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
                 vidx = to_var(t)->get_idx();
                 if (fr.second == 0) {
                     CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
-                    // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
+                    // Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
                     if (definitions.get(vidx, 0) != 0) {
                         if (visiting.is_marked(t)) {
                             // cycle detected: remove t
@@ -342,7 +337,7 @@ void der::get_elimination_order() {
 
 void der::create_substitution(unsigned sz) {
     m_subst_map.reset();
-    m_subst_map.resize(sz, 0);
+    m_subst_map.resize(sz, nullptr);
 
     for(unsigned i = 0; i < m_order.size(); i++) {
         expr_ref cur(m_map[m_order[i]], m_manager);

src/ast/rewriter/distribute_forall.h

@@ -71,7 +71,7 @@ protected:
     void reduce1_app(app * a);
 
     expr * get_cached(expr * n) const;
-    bool is_cached(expr * n) const {  return get_cached(n) != 0; }
+    bool is_cached(expr * n) const {  return get_cached(n) != nullptr; }
     void cache_result(expr * n, expr * r);
     void reset_cache() { m_cache.reset(); }
     void flush_cache() { m_cache.cleanup(); }

src/ast/rewriter/dl_rewriter.cpp

@@ -22,7 +22,7 @@ Revision History:
     br_status dl_rewriter::mk_app_core(
         func_decl * f, unsigned num_args, expr* const* args, expr_ref& result) {
         ast_manager& m = result.get_manager();
-        uint64 v1, v2;
+        uint64_t v1, v2;
         switch(f->get_decl_kind()) {
             case datalog::OP_DL_LT:
                 if (m_util.is_numeral_ext(args[0], v1) &&

src/ast/rewriter/elim_bounds.cpp

@@ -44,15 +44,15 @@ elim_bounds_cfg::elim_bounds_cfg(ast_manager & m):
    It also detects >=, and the atom can be negated.
 */
 bool elim_bounds_cfg::is_bound(expr * n, var * & lower, var * & upper) {
-    upper    = 0;
-    lower    = 0;
+    upper    = nullptr;
+    lower    = nullptr;
     bool neg = false;
     if (m.is_not(n)) {
         n   = to_app(n)->get_arg(0);
         neg = true;
     }
 
-    expr* l = 0, *r = 0;
+    expr* l = nullptr, *r = nullptr;
     bool le  = false;
     if (m_util.is_le(n, l, r) && m_util.is_numeral(r)) {
         n  = l;
@@ -139,14 +139,14 @@ bool elim_bounds_cfg::reduce_quantifier(quantifier * q,
     ptr_buffer<var>    candidates;
 #define ADD_CANDIDATE(V) if (!lowers.contains(V) && !uppers.contains(V)) { candidate_set.insert(V); candidates.push_back(V); }
     for (expr * a : atoms) {
-        var * lower = 0;
-        var * upper = 0;
+        var * lower = nullptr;
+        var * upper = nullptr;
         if (is_bound(a, lower, upper)) {
-            if (lower != 0 && !used_vars.contains(lower->get_idx()) && lower->get_idx() < num_vars) {
+            if (lower != nullptr && !used_vars.contains(lower->get_idx()) && lower->get_idx() < num_vars) {
                 ADD_CANDIDATE(lower);
                 lowers.insert(lower);
             }
-            if (upper != 0 && !used_vars.contains(upper->get_idx()) && upper->get_idx() < num_vars) {
+            if (upper != nullptr && !used_vars.contains(upper->get_idx()) && upper->get_idx() < num_vars) {
                 ADD_CANDIDATE(upper);
                 uppers.insert(upper);
             }
@@ -167,9 +167,9 @@ bool elim_bounds_cfg::reduce_quantifier(quantifier * q,
     unsigned j = 0;
     for (unsigned i = 0; i < atoms.size(); ++i) {
         expr * a = atoms[i];
-        var * lower = 0;
-        var * upper = 0;
-        if (is_bound(a, lower, upper) && ((lower != 0 && candidate_set.contains(lower)) || (upper != 0 && candidate_set.contains(upper))))
+        var * lower = nullptr;
+        var * upper = nullptr;
+        if (is_bound(a, lower, upper) && ((lower != nullptr && candidate_set.contains(lower)) || (upper != nullptr && candidate_set.contains(upper))))
             continue;
         atoms[j] = a;
         j++;
@@ -178,7 +178,7 @@ bool elim_bounds_cfg::reduce_quantifier(quantifier * q,
         return false;
     }
     atoms.resize(j);
-    expr * new_body = 0;
+    expr * new_body = nullptr;
     switch (atoms.size()) {
     case 0:
         result = m.mk_false();

src/ast/rewriter/elim_bounds.h

@@ -70,7 +70,7 @@ public:
         m_cfg(m)
     {} 
 
-    virtual ~elim_bounds_rw() {}
+    ~elim_bounds_rw() override {}
 };
 
 #endif /* ELIM_BOUNDS2_H_ */

src/ast/rewriter/enum2bv_rewriter.cpp

@@ -194,7 +194,7 @@ struct enum2bv_rewriter::imp {
                                      q->get_weight(), q->get_qid(), q->get_skid(), 
                                      q->get_num_patterns(), new_patterns,
                                      q->get_num_no_patterns(), new_no_patterns);
-            result_pr = 0;
+            result_pr = nullptr;
             return true;
         }
 
@@ -226,7 +226,7 @@ struct enum2bv_rewriter::imp {
         m_enum_bvs(m),
         m_enum_defs(m),
         m_num_translated(0), 
-        m_sort_pred(0), 
+        m_sort_pred(nullptr),
         m_rw(*this, m, p) {
     }
 

src/ast/rewriter/expr_replacer.cpp

@@ -34,7 +34,7 @@ void expr_replacer::operator()(expr * t, expr_ref & result) {
 struct expr_replacer::scoped_set_subst {
     expr_replacer & m_r;
     scoped_set_subst(expr_replacer & r, expr_substitution & s):m_r(r) { m_r.set_substitution(&s); }
-    ~scoped_set_subst() { m_r.set_substitution(0); }
+    ~scoped_set_subst() { m_r.set_substitution(nullptr); }
 };
 
 void expr_replacer::apply_substitution(expr * s, expr * def, proof * def_pr, expr_ref & t) { 
@@ -58,14 +58,14 @@ struct default_expr_replacer_cfg : public default_rewriter_cfg  {
 
     default_expr_replacer_cfg(ast_manager & _m):
         m(_m),
-        m_subst(0),
+        m_subst(nullptr),
         m_used_dependencies(_m) {
     }
 
     bool get_subst(expr * s, expr * & t, proof * & pr) { 
-        if (m_subst == 0)
+        if (m_subst == nullptr)
             return false;
-        expr_dependency * d = 0;
+        expr_dependency * d = nullptr;
         if (m_subst->find(s, t, pr, d)) {
             m_used_dependencies = m.mk_join(m_used_dependencies, d);
             return true;
@@ -90,29 +90,29 @@ public:
         m_replacer(m, m.proofs_enabled(), m_cfg) {
     }
     
-    virtual ast_manager & m() const { return m_replacer.m(); }
+    ast_manager & m() const override { return m_replacer.m(); }
 
-    virtual void set_substitution(expr_substitution * s) { 
+    void set_substitution(expr_substitution * s) override {
         m_replacer.cleanup();
         m_replacer.cfg().m_subst = s;
     }
     
-    virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) {
-        result_dep = 0;
+    void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) override {
+        result_dep = nullptr;
         m_replacer.operator()(t, result, result_pr);
         if (m_cfg.m_used_dependencies != 0) {
             result_dep = m_cfg.m_used_dependencies;
             m_replacer.reset(); // reset cache
-            m_cfg.m_used_dependencies = 0;
+            m_cfg.m_used_dependencies = nullptr;
         }
     }
 
 
-    virtual unsigned get_num_steps() const {
+    unsigned get_num_steps() const override {
         return m_replacer.get_num_steps();
     }
 
-    virtual void reset() {
+    void reset() override {
         m_replacer.reset();
     }
 };
@@ -131,23 +131,23 @@ public:
         m_r(m, p) {
     }
 
-    virtual ~th_rewriter2expr_replacer() {}
+    ~th_rewriter2expr_replacer() override {}
 
-    virtual ast_manager & m() const { return m_r.m(); }
+    ast_manager & m() const override { return m_r.m(); }
 
-    virtual void set_substitution(expr_substitution * s) { m_r.set_substitution(s); }
+    void set_substitution(expr_substitution * s) override { m_r.set_substitution(s); }
 
-    virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) {
+    void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) override {
         m_r(t, result, result_pr);
         result_dep = m_r.get_used_dependencies();
         m_r.reset_used_dependencies();
     }
 
-    virtual unsigned get_num_steps() const { 
+    unsigned get_num_steps() const override {
         return m_r.get_num_steps();
     }
 
-    virtual void reset() {
+    void reset() override {
         m_r.reset();
     }
 

src/ast/rewriter/expr_safe_replace.cpp

@@ -61,7 +61,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
             m_args.reset();
             bool arg_differs = false;
             for (unsigned i = 0; i < n; ++i) {
-                expr* d = 0, *arg = c->get_arg(i);
+                expr* d = nullptr, *arg = c->get_arg(i);
                 if (m_cache.find(arg, d)) {
                     m_args.push_back(d);
                     arg_differs |= arg != d;

src/ast/rewriter/factor_equivs.cpp

@@ -0,0 +1,145 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    factor_equivs.cpp
+
+Abstract:
+  Factor equivalence classes out of an expression.
+
+  "Equivalence class structure" for objs. Uses a union_find structure internally.
+  Operations are :
+  -Declare a new equivalence class with a single element
+  -Merge two equivalence classes
+  -Retrieve whether two elements are in the same equivalence class
+  -Iterate on all the elements of the equivalence class of a given element
+  -Iterate on all equivalence classes (and then within them)
+
+Author:
+
+    Julien Braine
+    Arie Gurfinkel
+
+Revision History:
+
+*/
+
+#include "ast/arith_decl_plugin.h"
+#include "ast/for_each_expr.h"
+#include "ast/ast_pp.h"
+#include "ast/rewriter/expr_safe_replace.h"
+#include "ast/rewriter/factor_equivs.h"
+
+/**
+   Factors input vector v into equivalence classes and the rest
+ */
+void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
+    ast_manager &m = v.get_manager();
+    arith_util arith(m);
+    expr *e1 = nullptr, *e2 = nullptr;
+
+    flatten_and(v);
+    unsigned j = 0;
+    for (unsigned i = 0; i < v.size(); ++i) {
+        if (m.is_eq(v.get(i), e1, e2)) {
+            if (arith.is_zero(e1)) {
+                std::swap(e1, e2);
+            }
+
+            // y + -1*x == 0
+            expr* a0 = nullptr, *a1 = nullptr, *x = nullptr;
+            if (arith.is_zero(e2) && arith.is_add(e1, a0, a1)) {
+                if (arith.is_times_minus_one(a1, x)) {
+                    e1 = a0;
+                    e2 = x;
+                }
+                else if (arith.is_times_minus_one(a0, x)) {
+                    e1 = a1;
+                    e2 = x;
+                }
+            }
+            equiv.merge(e1, e2);
+        }
+        else {
+            if (j < i) {
+                v[j] = v.get(i);
+            }
+            j++;
+        }
+    }
+    v.shrink(j);
+}
+
+/**
+ * Chooses a representative of an equivalence class
+ */
+expr *choose_rep(expr_equiv_class::eq_class &clazz, ast_manager &m) {
+    expr *rep = nullptr;
+    unsigned rep_sz, elem_sz;
+    for (expr *elem : clazz) {
+        if (!m.is_value(elem)) {
+            elem_sz = get_num_exprs(elem);
+            if (!rep || (rep && rep_sz > elem_sz)) {
+                rep = elem;
+                rep_sz = elem_sz;
+            }
+        }
+    }
+    TRACE("equiv",
+          tout << "Rep: " << mk_pp(rep, m) << "\n";
+          for (expr *el : clazz)
+              tout << mk_pp(el, m) << "\n";
+          tout << "RepEnd\n";);
+
+    return rep;
+}
+
+void rewrite_eqs (expr_ref_vector &v, expr_equiv_class &equiv) {
+    ast_manager &m = v.m();
+    expr_safe_replace sub(m);
+    for (auto eq_class : equiv) {
+        expr *rep = choose_rep(eq_class, m);
+        for (expr *el : eq_class) {
+            if (el != rep) {
+                sub.insert (el, rep);
+            }
+        }
+    }
+    sub(v);
+}
+
+
+/**
+ * converts equivalence classes to equalities
+ */
+void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out) {
+    ast_manager &m = out.get_manager();
+    for (auto eq_class : equiv) {
+        expr *rep = choose_rep(eq_class, m);
+        SASSERT(rep);
+        for (expr *elem : eq_class) {
+            if (rep != elem) {
+                out.push_back (m.mk_eq (rep, elem));
+            }
+        }
+    }
+}
+
+/**
+ * expands equivalence classes to all derivable equalities
+ */
+bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out) {
+    ast_manager &m = out.get_manager();
+    bool dirty = false;
+    for (auto eq_class : equiv) {
+        for (auto a = eq_class.begin(), end = eq_class.end(); a != end; ++a) {
+            expr_equiv_class::iterator b(a);
+            for (++b; b != end; ++b) {
+                out.push_back(m.mk_eq(*a, *b));
+                dirty = true;
+            }
+        }
+    }
+    return dirty;
+}

src/ast/rewriter/factor_equivs.h

@@ -0,0 +1,190 @@
+/*++
+Copyright (c) 2017 Arie Gurfinkel
+
+Module Name:
+
+    factor_equivs.h
+
+Abstract:
+  Factor equivalence classes out of an expression.
+
+  "Equivalence class structure" for objs. Uses a union_find structure internally.
+  Operations are :
+  -Declare a new equivalence class with a single element
+  -Merge two equivalence classes
+  -Retrieve whether two elements are in the same equivalence class
+  -Iterate on all the elements of the equivalence class of a given element
+  -Iterate on all equivalence classes (and then within them)
+
+Author:
+
+    Julien Braine
+    Arie Gurfinkel
+
+Revision History:
+
+*/
+
+#ifndef FACTOR_EQUIVS_H_
+#define FACTOR_EQUIVS_H_
+
+#include "util/union_find.h"
+#include "ast/ast_util.h"
+
+///All functions naturally add their parameters to the union_find class
+template<typename OBJ, typename Manager>
+class obj_equiv_class {
+    basic_union_find m_uf;
+    obj_map<OBJ, unsigned> m_to_int;
+    ref_vector<OBJ, Manager> m_to_obj;
+
+    unsigned add_elem_impl(OBJ*o) {
+        unsigned id = m_to_obj.size();
+        m_to_int.insert(o, id);
+        m_to_obj.push_back(o);
+        return id;
+    }
+    unsigned add_if_not_there(OBJ*o) {
+        unsigned id;
+        if(!m_to_int.find(o, id)) {
+            id = add_elem_impl(o);
+        }
+        return id;
+    }
+
+public:
+    class iterator;
+    class equiv_iterator;
+    friend class iterator;
+    friend class equiv_iterator;
+
+    obj_equiv_class(Manager& m) : m_to_obj(m) {}
+
+    Manager &m() const {return m_to_obj.m();}
+
+    void add_elem(OBJ*o) {
+        SASSERT(!m_to_int.find(o));
+        add_elem_impl(o);
+    }
+
+    //Invalidates all iterators
+    void merge(OBJ* a, OBJ* b) {
+        unsigned v1 = add_if_not_there(a);
+        unsigned v2 = add_if_not_there(b);
+        unsigned tmp1 = m_uf.find(v1);
+        unsigned tmp2 = m_uf.find(v2);
+        m_uf.merge(tmp1, tmp2);
+    }
+
+    void reset() {
+        m_uf.reset();
+        m_to_int.reset();
+        m_to_obj.reset();
+    }
+
+    bool are_equiv(OBJ*a, OBJ*b) {
+        unsigned id1 = add_if_not_there(a);
+        unsigned id2 = add_if_not_there(b);
+        return m_uf.find(id1) == m_uf.find(id2);
+    }
+
+    class iterator {
+        friend class obj_equiv_class;
+    private :
+        const obj_equiv_class& m_ouf;
+        unsigned m_curr_id;
+        bool m_first;
+        iterator(const obj_equiv_class& uf, unsigned id, bool f) :
+            m_ouf(uf), m_curr_id(id), m_first(f) {}
+    public :
+        OBJ*operator*() {return m_ouf.m_to_obj[m_curr_id];}
+
+        iterator& operator++() {
+            m_curr_id = m_ouf.m_uf.next(m_curr_id);
+            m_first = false;
+            return *this;
+        }
+        bool operator==(const iterator& o) {
+            SASSERT(&m_ouf == &o.m_ouf);
+            return  m_first == o.m_first && m_curr_id == o.m_curr_id;
+        }
+        bool operator!=(const iterator& o) {return !(*this == o);}
+    };
+
+    iterator begin(OBJ*o) {
+        unsigned id = add_if_not_there(o);
+        return iterator(*this, id, true);
+    }
+    iterator end(OBJ*o) {
+        unsigned id = add_if_not_there(o);
+        return iterator(*this, id, false);
+    }
+
+    class eq_class {
+    private :
+        iterator m_begin;
+        iterator m_end;
+    public :
+        eq_class(const iterator& a, const iterator& b) : m_begin(a), m_end(b) {}
+        iterator begin() {return m_begin;}
+        iterator end() {return m_end;}
+    };
+
+    class equiv_iterator {
+        friend class obj_equiv_class;
+    private :
+        const obj_equiv_class& m_ouf;
+        unsigned m_rootnb;
+        equiv_iterator(const obj_equiv_class& uf, unsigned nb) :
+            m_ouf(uf), m_rootnb(nb) {
+            while(m_rootnb != m_ouf.m_to_obj.size() &&
+                  m_ouf.m_uf.is_root(m_rootnb) != true)
+            { m_rootnb++; }
+        }
+    public :
+        eq_class operator*() {
+            return eq_class(iterator(m_ouf, m_rootnb, true),
+                            iterator(m_ouf, m_rootnb, false));
+        }
+        equiv_iterator& operator++() {
+            do {
+                m_rootnb++;
+            } while(m_rootnb != m_ouf.m_to_obj.size() &&
+                    m_ouf.m_uf.is_root(m_rootnb) != true);
+            return *this;
+        }
+        bool operator==(const equiv_iterator& o) {
+            SASSERT(&m_ouf == &o.m_ouf);
+            return m_rootnb == o.m_rootnb;
+        }
+        bool operator!=(const equiv_iterator& o) {return !(*this == o);}
+    };
+
+    equiv_iterator begin() {return equiv_iterator(*this, 0);}
+    equiv_iterator end() {return equiv_iterator(*this, m_to_obj.size());}
+};
+
+typedef obj_equiv_class<expr, ast_manager> expr_equiv_class;
+
+
+/**
+ *  Factors input vector v into equivalence classes and the rest
+ */
+void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv);
+/**
+ * Rewrite expressions in v by choosing a representative from the
+ * equivalence class.
+ */
+void rewrite_eqs(expr_ref_vector &v, expr_equiv_class &equiv);
+/**
+ * converts equivalence classes to equalities
+ */
+void equiv_to_expr(expr_equiv_class &equiv, expr_ref_vector &out);
+
+/**
+ * expands equivalence classes to all derivable equalities
+ */
+bool equiv_to_expr_full(expr_equiv_class &equiv, expr_ref_vector &out);
+
+
+#endif

src/ast/rewriter/factor_rewriter.h

@@ -61,7 +61,7 @@ struct factor_rewriter_cfg : public default_rewriter_cfg {
     bool rewrite_patterns() const { return false; }
     bool flat_assoc(func_decl * f) const { return false; }
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-        result_pr = 0;
+        result_pr = nullptr;
         return m_r.mk_app_core(f, num, args, result);
     }
     factor_rewriter_cfg(ast_manager & m):m_r(m) {}

src/ast/rewriter/fpa_rewriter.cpp

@@ -48,17 +48,17 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_FPA_RM_TOWARD_POSITIVE:
     case OP_FPA_RM_TOWARD_NEGATIVE:
     case OP_FPA_RM_TOWARD_ZERO:
-        SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)0); st = BR_DONE; break;
+        SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)nullptr); st = BR_DONE; break;
 
     case OP_FPA_PLUS_INF:
     case OP_FPA_MINUS_INF:
     case OP_FPA_NAN:
     case OP_FPA_PLUS_ZERO:
     case OP_FPA_MINUS_ZERO:
-        SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)0); st = BR_DONE; break;
+        SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)nullptr); st = BR_DONE; break;
 
     case OP_FPA_NUM:
-        SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)0); st = BR_DONE; break;
+        SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)nullptr); st = BR_DONE; break;
 
     case OP_FPA_ADD:       SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break;
     case OP_FPA_SUB:       SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break;
@@ -773,7 +773,7 @@ br_status fpa_rewriter::mk_to_ieee_bv(func_decl * f, expr * arg, expr_ref & resu
         if (m_fm.is_nan(v)) {
             if (m_hi_fp_unspecified) {
                 expr * args[4] = { bu.mk_numeral(0, 1),
-                                   bu.mk_numeral(-1, x.get_ebits()),
+                                   bu.mk_bv_neg(bu.mk_numeral(1, x.get_ebits())),
                                    bu.mk_numeral(0, x.get_sbits() - 2),
                                    bu.mk_numeral(1, 1) };
                 result = bu.mk_concat(4, args);

src/ast/rewriter/inj_axiom.cpp

@@ -29,9 +29,9 @@ Revision History:
 */
 bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
     expr * n = q->get_expr();
-    expr* arg1 = 0, * arg2 = 0, *narg = 0;
-    expr* app1 = 0, * app2 = 0;
-    expr* var1 = 0, * var2 = 0;
+    expr* arg1 = nullptr, * arg2 = nullptr, *narg = nullptr;
+    expr* app1 = nullptr, * app2 = nullptr;
+    expr* var1 = nullptr, * var2 = nullptr;
     if (q->is_forall() && m.is_or(n, arg1, arg2)) {
         if (m.is_not(arg2)) 
             std::swap(arg1, arg2);
@@ -84,7 +84,7 @@ bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
                     ptr_buffer<sort> decls;
                     buffer<symbol>   names;
                     
-                    expr * var            = 0;
+                    expr * var            = nullptr;
                     for (unsigned i = 0; i < num; i++) {
                         expr * c = f1->get_arg(i);
                         if (is_var(c)) {

src/ast/rewriter/maximize_ac_sharing.cpp

@@ -35,7 +35,7 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
     if (std::find(m_kinds.begin(), m_kinds.end(), k) == m_kinds.end())
         return BR_FAILED;
     ptr_buffer<expr, 128> _args;
-    expr * numeral = 0;
+    expr * numeral = nullptr;
     if (is_numeral(args[0])) {
         numeral = args[0];
         for (unsigned i = 1; i < num_args; i++) 
@@ -86,7 +86,7 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
         }
         num_args = j;
         if (num_args == 1) {
-            if (numeral == 0) { 
+            if (numeral == nullptr) {
                 result = _args[0];
             }
             else {

src/ast/rewriter/maximize_ac_sharing.h

@@ -45,7 +45,7 @@ class maximize_ac_sharing : public default_rewriter_cfg {
         expr *      m_arg1;
         expr *      m_arg2;
 
-        entry(func_decl * d = 0, expr * arg1 = 0, expr * arg2 = 0):m_decl(d), m_arg1(arg1), m_arg2(arg2) {
+        entry(func_decl * d = nullptr, expr * arg1 = nullptr, expr * arg2 = nullptr):m_decl(d), m_arg1(arg1), m_arg2(arg2) {
             SASSERT((d == 0 && arg1 == 0 && arg2 == 0) || (d != 0 && arg1 != 0 && arg2 != 0));
             if (arg1->get_id() > arg2->get_id())
                 std::swap(m_arg1, m_arg2);
@@ -103,8 +103,8 @@ public:
 class maximize_bv_sharing : public maximize_ac_sharing {
     bv_util m_util;
 protected:
-    virtual void init_core();
-    virtual bool is_numeral(expr * n) const;
+    void init_core() override;
+    bool is_numeral(expr * n) const override;
 public:
     maximize_bv_sharing(ast_manager & m);
 };

src/ast/rewriter/mk_extract_proc.cpp

@@ -19,8 +19,8 @@ mk_extract_proc::mk_extract_proc(bv_util & u):
     m_util(u),
     m_high(0),
     m_low(UINT_MAX),
-    m_domain(0),
-    m_f_cached(0) {
+    m_domain(nullptr),
+    m_f_cached(nullptr) {
 }
 
 mk_extract_proc::~mk_extract_proc() {

src/ast/rewriter/mk_simplified_app.cpp

@@ -98,7 +98,7 @@ br_status mk_simplified_app::mk_core(func_decl * decl, unsigned num, expr * cons
 }
 
 void mk_simplified_app::operator()(func_decl * decl, unsigned num, expr * const * args, expr_ref & result) {
-    result = 0;
+    result = nullptr;
     mk_core(decl, num, args, result);
     if (!result) 
         result = m_imp->m.mk_app(decl, num, args);

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -25,6 +25,10 @@ Notes:
 #include "ast/ast_util.h"
 #include "ast/ast_pp.h"
 #include "util/lbool.h"
+#include "util/uint_set.h"
+#include "util/gparams.h"
+
+const unsigned g_primes[7] = { 2, 3, 5, 7, 11, 13, 17};
 
 
 struct pb2bv_rewriter::imp {
@@ -35,10 +39,12 @@ struct pb2bv_rewriter::imp {
     func_decl_ref_vector      m_fresh;       // all fresh variables
     unsigned_vector           m_fresh_lim;
     unsigned                  m_num_translated;
+    unsigned                  m_compile_bv;
+    unsigned                  m_compile_card;
 
     struct card2bv_rewriter {               
-        typedef expr* literal;
-        typedef ptr_vector<expr> literal_vector;
+        typedef expr* pliteral;
+        typedef ptr_vector<expr> pliteral_vector;
         psort_nw<card2bv_rewriter> m_sort;
         ast_manager& m;
         imp&         m_imp;
@@ -49,6 +55,9 @@ struct pb2bv_rewriter::imp {
         expr_ref_vector m_args;
         rational     m_k;
         vector<rational> m_coeffs;
+        bool m_keep_cardinality_constraints;
+        symbol m_pb_solver;
+        unsigned m_min_arity;
 
         template<lbool is_le>
         expr_ref mk_le_ge(expr_ref_vector& fmls, expr* a, expr* b, expr* bound) {
@@ -68,7 +77,28 @@ struct pb2bv_rewriter::imp {
                 fmls.push_back(bv.mk_ule(bound, result));
             }
             return result;
+        }
 
+        typedef std::pair<rational, expr_ref> ca;
+
+        struct compare_coeffs {
+            bool operator()(ca const& x, ca const& y) const {
+                return x.first > y.first;
+            }
+        };
+
+        void sort_args() {
+            vector<ca> cas;
+            for (unsigned i = 0; i < m_args.size(); ++i) {
+                cas.push_back(std::make_pair(m_coeffs[i], expr_ref(m_args[i].get(), m)));
+            }
+            std::sort(cas.begin(), cas.end(), compare_coeffs());
+            m_coeffs.reset();
+            m_args.reset();
+            for (ca const& ca : cas) {
+                m_coeffs.push_back(ca.first);
+                m_args.push_back(ca.second);
+            }
         }
 
         // 
@@ -84,21 +114,25 @@ struct pb2bv_rewriter::imp {
         // is_le = l_false -  >= 
         //
         template<lbool is_le>
-        expr_ref mk_le_ge(unsigned sz, expr * const* args, rational const & k) {
+        expr_ref mk_le_ge(rational const & k) {
+            //sort_args();
+            unsigned sz = m_args.size();
+            expr * const* args = m_args.c_ptr();
             TRACE("pb", 
                   for (unsigned i = 0; i < sz; ++i) {
                       tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " ";
                       if (i + 1 < sz && !m_coeffs[i+1].is_neg()) tout << "+ ";
                   }
                   switch (is_le) {
-                  case l_true: tout << "<= "; break;
+                  case l_true:  tout << "<= "; break;
                   case l_undef: tout << "= "; break;
                   case l_false: tout << ">= "; break;
                   }
-                  tout << m_k << "\n";);
+                  tout << k << "\n";);
+
             if (k.is_zero()) {
                 if (is_le != l_false) {
-                    return expr_ref(m.mk_not(mk_or(m, sz, args)), m);
+                    return expr_ref(m.mk_not(::mk_or(m_args)), m);
                 }
                 else {
                     return expr_ref(m.mk_true(), m);
@@ -107,6 +141,35 @@ struct pb2bv_rewriter::imp {
             if (k.is_neg()) {
                 return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
             }
+
+            if (m_pb_solver == "totalizer") {
+                expr_ref result(m);
+                switch (is_le) {
+                case l_true:  if (mk_le_tot(sz, args, k, result)) return result; else break;
+                case l_false: if (mk_ge_tot(sz, args, k, result)) return result; else break;
+                case l_undef: break;
+                }
+            }
+            
+            if (m_pb_solver == "sorting") {
+                expr_ref result(m);
+                switch (is_le) {
+                case l_true:  if (mk_le(sz, args, k, result)) return result; else break;
+                case l_false: if (mk_ge(sz, args, k, result)) return result; else break;
+                case l_undef: if (mk_eq(sz, args, k, result)) return result; else break;
+                }
+            }
+
+            if (m_pb_solver == "segmented") {
+                expr_ref result(m);
+                switch (is_le) {
+                case l_true:  return mk_seg_le(k);
+                case l_false: return mk_seg_ge(k);
+                case l_undef: break;
+                }
+            }
+
+            // fall back to divide and conquer encoding.
             SASSERT(k.is_pos());
             expr_ref zero(m), bound(m);
             expr_ref_vector es(m), fmls(m);
@@ -138,12 +201,12 @@ struct pb2bv_rewriter::imp {
             }
             switch (is_le) {
             case l_true: 
-                return mk_and(fmls);
+                return ::mk_and(fmls);
             case l_false:
                 if (!es.empty()) {
                     fmls.push_back(bv.mk_ule(bound, es.back()));
                 }
-                return mk_or(fmls);
+                return ::mk_or(fmls);
             case l_undef:
                 if (es.empty()) {
                     fmls.push_back(m.mk_bool_val(k.is_zero()));
@@ -151,35 +214,415 @@ struct pb2bv_rewriter::imp {
                 else {
                     fmls.push_back(m.mk_eq(bound, es.back()));
                 }
-                return mk_and(fmls);
+                return ::mk_and(fmls);
             default:
                 UNREACHABLE();
                 return expr_ref(m.mk_true(), m);
             }
         }
 
+        /**
+           \brief Totalizer encoding. Based on a version by Miguel.
+         */
+
+        bool mk_le_tot(unsigned sz, expr * const * args, rational const& _k, expr_ref& result) {
+            SASSERT(sz == m_coeffs.size());
+            if (!_k.is_unsigned() || sz == 0) return false;
+            unsigned k = _k.get_unsigned();
+            expr_ref_vector args1(m);
+            rational bound;
+            flip(sz, args, args1, _k, bound);
+            if (bound.get_unsigned() < k) {
+                return mk_ge_tot(sz, args1.c_ptr(), bound, result);
+            }
+            if (k > 20) {
+                return false;
+            }
+            result = m.mk_not(bounded_addition(sz, args, k + 1));
+            TRACE("pb", tout << result << "\n";);
+            return true;
+        }
+
+        bool mk_ge_tot(unsigned sz, expr * const * args, rational const& _k, expr_ref& result) {
+            SASSERT(sz == m_coeffs.size());
+            if (!_k.is_unsigned() || sz == 0) return false;
+            unsigned k = _k.get_unsigned();
+            expr_ref_vector args1(m);
+            rational bound;
+            flip(sz, args, args1, _k, bound);
+            if (bound.get_unsigned() < k) {
+                return mk_le_tot(sz, args1.c_ptr(), bound, result);
+            }
+            if (k > 20) {
+                return false;
+            }
+            result = bounded_addition(sz, args, k);
+            TRACE("pb", tout << result << "\n";);
+            return true;
+        }
+
+        void flip(unsigned sz, expr* const* args, expr_ref_vector& args1, rational const& k, rational& bound) {
+            bound = -k;
+            for (unsigned i = 0; i < sz; ++i) {
+                args1.push_back(mk_not(args[i]));
+                bound += m_coeffs[i];
+            }
+        }
+
+        expr_ref bounded_addition(unsigned sz, expr * const * args, unsigned k) {
+            SASSERT(sz > 0);
+            expr_ref result(m);
+            vector<expr_ref_vector> es;
+            vector<unsigned_vector> coeffs;
+            for (unsigned i = 0; i < m_coeffs.size(); ++i) {
+                unsigned_vector v;
+                expr_ref_vector e(m);
+                unsigned c = m_coeffs[i].get_unsigned();
+                v.push_back(c >= k ? k : c);
+                e.push_back(args[i]);   
+                es.push_back(e);
+                coeffs.push_back(v);
+            }
+            while (es.size() > 1) {
+                for (unsigned i = 0; i + 1 < es.size(); i += 2) {
+                    expr_ref_vector o(m);
+                    unsigned_vector oc;
+                    tot_adder(es[i], coeffs[i], es[i + 1], coeffs[i + 1], k, o, oc);
+                    es[i / 2].set(o);
+                    coeffs[i / 2] = oc;
+                }
+                if ((es.size() % 2) == 1) {
+                    es[es.size() / 2].set(es.back());
+                    coeffs[es.size() / 2] = coeffs.back();
+                }
+                es.shrink((1 + es.size())/2);
+                coeffs.shrink((1 + coeffs.size())/2);
+            }
+            SASSERT(coeffs.size() == 1);
+            SASSERT(coeffs[0].back() <= k);
+            if (coeffs[0].back() == k) {
+                result = es[0].back();
+            }
+            else {
+                result = m.mk_false();
+            }
+            return result;
+        }
+
+        void tot_adder(expr_ref_vector const& l, unsigned_vector const& lc,
+                       expr_ref_vector const& r, unsigned_vector const& rc,
+                       unsigned k,
+                       expr_ref_vector& o, unsigned_vector & oc) {
+            SASSERT(l.size() == lc.size());
+            SASSERT(r.size() == rc.size());
+            uint_set sums;
+            vector<expr_ref_vector> trail;
+            u_map<unsigned> sum2def;
+            for (unsigned i = 0; i <= l.size(); ++i) {
+                for (unsigned j = (i == 0) ? 1 : 0; j <= r.size(); ++j) {
+                    unsigned sum = std::min(k, ((i == 0) ? 0 : lc[i - 1]) + ((j == 0) ? 0 : rc[j - 1]));
+                    sums.insert(sum);                        
+                }
+            }
+            for (unsigned u : sums) {
+                oc.push_back(u);
+            }            
+            std::sort(oc.begin(), oc.end());
+            DEBUG_CODE(                
+                for (unsigned i = 0; i + 1 < oc.size(); ++i) {
+                    SASSERT(oc[i] < oc[i+1]);
+                });
+            for (unsigned i = 0; i < oc.size(); ++i) {
+                sum2def.insert(oc[i], i);
+                trail.push_back(expr_ref_vector(m));
+            }
+            for (unsigned i = 0; i <= l.size(); ++i) {
+                for (unsigned j = (i == 0) ? 1 : 0; j <= r.size(); ++j) {
+                    if (i != 0 && j != 0 && (lc[i - 1] >= k || rc[j - 1] >= k)) continue;
+                    unsigned sum = std::min(k, ((i == 0) ? 0 : lc[i - 1]) + ((j == 0) ? 0 : rc[j - 1]));
+                    expr_ref_vector ands(m);
+                    if (i != 0) {
+                        ands.push_back(l[i - 1]);
+                    }
+                    if (j != 0) {
+                        ands.push_back(r[j - 1]);
+                    }
+                    trail[sum2def.find(sum)].push_back(::mk_and(ands));
+                }
+            }
+            for (unsigned i = 0; i < oc.size(); ++i) {
+                o.push_back(::mk_or(trail[sum2def.find(oc[i])]));
+            }
+        }
+
+        /**
+           \brief MiniSat+ based encoding of PB constraints. 
+           Translating Pseudo-Boolean Constraints into SAT,
+           Niklas Een, Niklas Soerensson, JSAT 2006.
+         */
+
+
+        vector<rational> m_min_base;
+        rational         m_min_cost;
+        vector<rational> m_base;
+
+        void create_basis(vector<rational> const& seq, rational carry_in, rational cost) {
+            if (cost >= m_min_cost) {
+                return;
+            }
+            rational delta_cost(0);
+            for (unsigned i = 0; i < seq.size(); ++i) {
+                delta_cost += seq[i];
+            }
+            if (cost + delta_cost < m_min_cost) {
+                m_min_cost = cost + delta_cost;
+                m_min_base = m_base;             
+                m_min_base.push_back(delta_cost + rational::one());
+            }
+            
+            for (unsigned i = 0; i < sizeof(g_primes)/sizeof(*g_primes); ++i) {
+                vector<rational> seq1;
+                rational p(g_primes[i]);
+                rational rest = carry_in;
+                // create seq1
+                for (unsigned j = 0; j < seq.size(); ++j) {
+                    rest += seq[j] % p;
+                    if (seq[j] >= p) {
+                        seq1.push_back(div(seq[j],  p));
+                    }
+                }
+                
+                m_base.push_back(p);
+                create_basis(seq1, div(rest, p), cost + rest);
+                m_base.pop_back();
+            }
+        }
+
+        bool create_basis() {
+            m_base.reset();
+            m_min_cost = rational(INT_MAX);
+            m_min_base.reset();
+            rational cost(0);
+            create_basis(m_coeffs, rational::zero(), cost);
+            m_base = m_min_base;
+            TRACE("pb",
+                  tout << "Base: ";
+                  for (unsigned i = 0; i < m_base.size(); ++i) {
+                      tout << m_base[i] << " ";
+                  }
+                  tout << "\n";);
+            return 
+                !m_base.empty() && 
+                m_base.back().is_unsigned() &&
+                m_base.back().get_unsigned() <= 20*m_base.size();
+        }
+
+        /**
+           \brief Check if 'out mod n >= lim'. 
+         */
+        expr_ref mod_ge(ptr_vector<expr> const& out, unsigned n, unsigned lim) {
+            TRACE("pb", for (unsigned i = 0; i < out.size(); ++i) tout << mk_pp(out[i], m) << " "; tout << "\n";
+                  tout << "n:" << n << " lim: " << lim << "\n";);
+            if (lim == n) {
+                return expr_ref(m.mk_false(), m);
+            }
+            if (lim == 0) {
+                return expr_ref(m.mk_true(), m);
+            }
+            SASSERT(0 < lim && lim < n);
+            expr_ref_vector ors(m);
+            for (unsigned j = 0; j + lim - 1 < out.size(); j += n) {
+                expr_ref tmp(m);
+                tmp = out[j + lim - 1];
+                if (j + n - 1 < out.size()) {
+                    tmp = m.mk_and(tmp, m.mk_not(out[j + n - 1]));
+                }
+                ors.push_back(tmp);
+            }
+            return ::mk_or(ors);
+        }
+
+        // x0 + 5x1 + 3x2 >= k
+        // x0 x1 x1 -> s0 s1 s2
+        // s2 x1 x2 -> s3 s4 s5
+        // k = 7: s5 or (s4 & not s2 & s0)
+        // k = 6: s4
+        // k = 5: s4 or (s3 & not s2 & s1)
+        // k = 4: s4 or (s3 & not s2 & s0)
+        // k = 3: s3
+        // 
+        bool mk_ge(unsigned sz, expr * const* args, rational bound, expr_ref& result) {
+            if (!create_basis()) return false;
+            if (!bound.is_unsigned()) return false;
+            vector<rational> coeffs(m_coeffs);
+            result = m.mk_true();
+            expr_ref_vector carry(m), new_carry(m);
+            m_base.push_back(bound + rational::one());
+            for (rational b_i : m_base) {
+                unsigned B   = b_i.get_unsigned();
+                unsigned d_i = (bound % b_i).get_unsigned();
+                bound = div(bound, b_i);                
+                for (unsigned j = 0; j < coeffs.size(); ++j) {
+                    rational c = coeffs[j] % b_i;                    
+                    SASSERT(c.is_unsigned());
+                    for (unsigned k = 0; k < c.get_unsigned(); ++k) {
+                        carry.push_back(args[j]);
+                    }
+                    coeffs[j] = div(coeffs[j], b_i);
+                }
+                TRACE("pb", tout << "Carry: " << carry << "\n";
+                      for (auto c : coeffs) tout << c << " ";
+                      tout << "\n";
+                      );
+                ptr_vector<expr> out;
+                m_sort.sorting(carry.size(), carry.c_ptr(), out);
+                
+                expr_ref gt = mod_ge(out, B, d_i + 1);
+                expr_ref ge = mod_ge(out, B, d_i);
+                result = mk_and(ge, result);
+                result = mk_or(gt, result);                
+                TRACE("pb", tout << "b: " << b_i << " d: " << d_i << " gt: " << gt << " ge: " << ge << " " << result << "\n";);
+
+                new_carry.reset();
+                for (unsigned j = B - 1; j < out.size(); j += B) {
+                    new_carry.push_back(out[j]);
+                }
+                carry.reset();
+                carry.append(new_carry);
+            }
+            TRACE("pb", tout << "bound: " << bound << " Carry: " << carry << " result: " << result << "\n";);
+            return true;
+        }
+
+        /**
+           \brief Segment based encoding.
+           The PB terms are partitoned into segments, such that each segment contains arguments with the same cofficient.
+           The segments are sorted, such that the segment with highest coefficient is first.
+           Then for each segment create circuits based on sorting networks the arguments of the segment.           
+        */
+
+        expr_ref mk_seg_ge(rational const& k) {
+            rational bound(-k);
+            for (unsigned i = 0; i < m_args.size(); ++i) {
+                m_args[i] = mk_not(m_args[i].get());
+                bound += m_coeffs[i];
+            }
+            return mk_seg_le(bound);
+        }
+        
+        expr_ref mk_seg_le(rational const& k) {
+            sort_args();
+            unsigned sz = m_args.size();            
+            expr* const* args = m_args.c_ptr();
+
+            // Create sorted entries.
+            vector<ptr_vector<expr>> outs;
+            vector<rational> coeffs;
+            for (unsigned i = 0, seg_size = 0; i < sz; i += seg_size) {
+                seg_size = segment_size(i);
+                ptr_vector<expr> out;
+                m_sort.sorting(seg_size, args + i, out);
+                out.push_back(m.mk_false());
+                outs.push_back(out);
+                coeffs.push_back(m_coeffs[i]);
+            }
+            return mk_seg_le_rec(outs, coeffs, 0, k);
+        }
+
+        expr_ref mk_seg_le_rec(vector<ptr_vector<expr>> const& outs, vector<rational> const& coeffs, unsigned i, rational const& k) {
+            rational const& c = coeffs[i];
+            ptr_vector<expr> const& out = outs[i];     
+            if (k.is_neg()) {
+                return expr_ref(m.mk_false(), m);
+            }
+            if (i == outs.size()) {
+                return expr_ref(m.mk_true(), m);
+            }
+            if (i + 1 == outs.size() && k >= rational(out.size()-1)*c) {
+                return expr_ref(m.mk_true(), m);
+            }
+            expr_ref_vector fmls(m);
+            fmls.push_back(m.mk_implies(m.mk_not(out[0]), mk_seg_le_rec(outs, coeffs, i + 1, k)));
+            rational k1;
+            for (unsigned j = 0; j + 1 < out.size(); ++j) {
+                k1 = k - rational(j+1)*c;
+                if (k1.is_neg()) {
+                    fmls.push_back(m.mk_not(out[j]));
+                    break;
+                }
+                fmls.push_back(m.mk_implies(m.mk_and(out[j], m.mk_not(out[j+1])), mk_seg_le_rec(outs, coeffs, i + 1, k1)));
+            }
+            return ::mk_and(fmls);
+        }
+
+        // The number of arguments with the same coefficient.
+        unsigned segment_size(unsigned start) const {
+            unsigned i = start;
+            while (i < m_args.size() && m_coeffs[i] == m_coeffs[start]) ++i;
+            return i - start;
+        }
+
+        expr_ref mk_and(expr_ref& a, expr_ref& b) {
+            if (m.is_true(a)) return b;
+            if (m.is_true(b)) return a;
+            if (m.is_false(a)) return a;
+            if (m.is_false(b)) return b;
+            return expr_ref(m.mk_and(a, b), m);
+        }
+        
+        expr_ref mk_or(expr_ref& a, expr_ref& b) {
+            if (m.is_true(a)) return a;
+            if (m.is_true(b)) return b;
+            if (m.is_false(a)) return b;
+            if (m.is_false(b)) return a;
+            return expr_ref(m.mk_or(a, b), m);
+        }
+
+        bool mk_le(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
+            expr_ref_vector args1(m);
+            rational bound(-k);            
+            for (unsigned i = 0; i < sz; ++i) {
+                args1.push_back(mk_not(args[i]));
+                bound += m_coeffs[i];
+            }
+            return mk_ge(sz, args1.c_ptr(), bound, result);
+        }
+
+        bool mk_eq(unsigned sz, expr * const* args, rational const& k, expr_ref& result) {
+            expr_ref r1(m), r2(m);
+            if (mk_ge(sz, args, k, r1) && mk_le(sz, args, k, r2)) {
+                result = m.mk_and(r1, r2);
+                return true;
+            }
+            else {
+                return false;
+            }
+        }
+
         expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) {
+            ++m_imp.m_compile_bv;
             decl_kind kind = f->get_decl_kind();
             rational k = pb.get_k(f);
             m_coeffs.reset();
+            m_args.reset();
             for (unsigned i = 0; i < sz; ++i) {
                 m_coeffs.push_back(pb.get_coeff(f, i));
+                m_args.push_back(args[i]);
             }
+            CTRACE("pb", k.is_neg(), tout << expr_ref(m.mk_app(f, sz, args), m) << "\n";);
             SASSERT(!k.is_neg());
             switch (kind) {
             case OP_PB_GE:
             case OP_AT_LEAST_K: {
-                expr_ref_vector nargs(m);
-                nargs.append(sz, args);
-                dualize(f, nargs, k);
+                dualize(f, m_args, k);
                 SASSERT(!k.is_neg());
-                return mk_le_ge<l_true>(sz, nargs.c_ptr(), k);
+                return mk_le_ge<l_true>(k);
             }
             case OP_PB_LE:
             case OP_AT_MOST_K:
-                return mk_le_ge<l_true>(sz, args, k);
+                return mk_le_ge<l_true>(k);
             case OP_PB_EQ:
-                return mk_le_ge<l_undef>(sz, args, k);
+                return mk_le_ge<l_undef>(k);
             default:
                 UNREACHABLE();
                 return expr_ref(m.mk_true(), m);
@@ -230,7 +673,7 @@ struct pb2bv_rewriter::imp {
 
     public:
 
-        card2bv_rewriter(imp& i, ast_manager& m):
+        card2bv_rewriter(imp& i, ast_manager& m):            
             m_sort(*this),
             m(m),
             m_imp(i),
@@ -238,29 +681,34 @@ struct pb2bv_rewriter::imp {
             pb(m),
             bv(m),
             m_trail(m),
-            m_args(m)
+            m_args(m),
+            m_keep_cardinality_constraints(false),
+            m_pb_solver(symbol("solver")),
+            m_min_arity(9)
         {}
 
+        void set_pb_solver(symbol const& s) { m_pb_solver = s; }
+
         bool mk_app(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
-            if (f->get_family_id() == pb.get_family_id()) {
-                mk_pb(full, f, sz, args, result);
+            if (f->get_family_id() == pb.get_family_id() && mk_pb(full, f, sz, args, result)) {
+                // skip
             }
             else if (au.is_le(f) && is_pb(args[0], args[1])) {
-                result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
+                result = mk_le_ge<l_true>(m_k);
             }
             else if (au.is_lt(f) && is_pb(args[0], args[1])) {
                 ++m_k;
-                result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
+                result = mk_le_ge<l_true>(m_k);
             }
             else if (au.is_ge(f) && is_pb(args[1], args[0])) {
-                result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
+                result = mk_le_ge<l_true>(m_k);
             }
             else if (au.is_gt(f) && is_pb(args[1], args[0])) {
                 ++m_k;
-                result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
+                result = mk_le_ge<l_true>(m_k);
             }
             else if (m.is_eq(f) && is_pb(args[0], args[1])) {
-                result = mk_le_ge<l_undef>(m_args.size(), m_args.c_ptr(), m_k);
+                result = mk_le_ge<l_undef>(m_k);
             }
             else {
                 return false;
@@ -278,6 +726,11 @@ struct pb2bv_rewriter::imp {
             }
         }
 
+        bool mk_app(bool full, expr* e, expr_ref& r) {
+            app* a;
+            return (is_app(e) && (a = to_app(e), mk_app(full, a->get_decl(), a->get_num_args(), a->get_args(), r)));
+        }
+
         bool is_pb(expr* x, expr* y) {
             m_args.reset();
             m_coeffs.reset();
@@ -349,53 +802,95 @@ struct pb2bv_rewriter::imp {
             return false;
         }
 
-        void mk_pb(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+        bool mk_pb(bool full, func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
             SASSERT(f->get_family_id() == pb.get_family_id());
             if (is_or(f)) {
                 result = m.mk_or(sz, args);
             }
             else if (pb.is_at_most_k(f) && pb.get_k(f).is_unsigned()) {
+                if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
                 result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
+                ++m_imp.m_compile_card;
             }
             else if (pb.is_at_least_k(f) && pb.get_k(f).is_unsigned()) {
+                if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
                 result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
+                ++m_imp.m_compile_card;
             }
             else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+                if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
                 result = m_sort.eq(full, pb.get_k(f).get_unsigned(), sz, args);
+                ++m_imp.m_compile_card;
             }
             else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+                if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
                 result = m_sort.le(full, pb.get_k(f).get_unsigned(), sz, args);
+                ++m_imp.m_compile_card;
             }
             else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && pb.has_unit_coefficients(f)) {
+                if (m_keep_cardinality_constraints && f->get_arity() >= m_min_arity) return false;
                 result = m_sort.ge(full, pb.get_k(f).get_unsigned(), sz, args);
+                ++m_imp.m_compile_card;
+            }
+            else if (pb.is_eq(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
+                return false;
+            }
+            else if (pb.is_le(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
+                return false;
+            }
+            else if (pb.is_ge(f) && pb.get_k(f).is_unsigned() && has_small_coefficients(f) && m_pb_solver == "solver") {
+                return false;
             }
             else {
                 result = mk_bv(f, sz, args);
             }
+            TRACE("pb", tout << "full: " << full << " " << expr_ref(m.mk_app(f, sz, args), m) << " " << result << "\n";
+                  );
+            return true;
+        }
+
+        bool has_small_coefficients(func_decl* f) {
+            unsigned sz = f->get_arity();
+            unsigned sum = 0;
+            for (unsigned i = 0; i < sz; ++i) {
+                rational c = pb.get_coeff(f, i);
+                if (!c.is_unsigned()) return false;
+                unsigned sum1 = sum + c.get_unsigned();
+                if (sum1 < sum) return false;
+                sum = sum1;
+            }
+            return true;
         }
    
         // definitions used for sorting network
-        literal mk_false() { return m.mk_false(); }
-        literal mk_true() { return m.mk_true(); }
-        literal mk_max(literal a, literal b) { return trail(m.mk_or(a, b)); }
-        literal mk_min(literal a, literal b) { return trail(m.mk_and(a, b)); }
-        literal mk_not(literal a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); }
+        pliteral mk_false() { return m.mk_false(); }
+        pliteral mk_true() { return m.mk_true(); }
+        pliteral mk_max(pliteral a, pliteral b) { return trail(m.mk_or(a, b)); }
+        pliteral mk_min(pliteral a, pliteral b) { return trail(m.mk_and(a, b)); }
+        pliteral mk_not(pliteral a) { if (m.is_not(a,a)) return a; return trail(m.mk_not(a)); }
 
-        std::ostream& pp(std::ostream& out, literal lit) {  return out << mk_ismt2_pp(lit, m);  }
+        std::ostream& pp(std::ostream& out, pliteral lit) {  return out << mk_ismt2_pp(lit, m);  }
         
-        literal trail(literal l) {
+        pliteral trail(pliteral l) {
             m_trail.push_back(l);
             return l;
         }
-        literal fresh() {
-            expr_ref fr(m.mk_fresh_const("sn", m.mk_bool_sort()), m);
+        pliteral fresh(char const* n) {                      
+            expr_ref fr(m.mk_fresh_const(n, m.mk_bool_sort()), m);
             m_imp.m_fresh.push_back(to_app(fr)->get_decl());
             return trail(fr);
         }
         
-        void mk_clause(unsigned n, literal const* lits) {
-            m_imp.m_lemmas.push_back(mk_or(m, n, lits));
+        void mk_clause(unsigned n, pliteral const* lits) {
+            m_imp.m_lemmas.push_back(::mk_or(m, n, lits));
         }        
+
+        void keep_cardinality_constraints(bool f) {
+            m_keep_cardinality_constraints = f;
+        }
+
+        void set_at_most1(sorting_network_encoding enc) { m_sort.cfg().m_encoding = enc; }
+
     };
 
     struct card2bv_rewriter_cfg : public default_rewriter_cfg {
@@ -403,10 +898,14 @@ struct pb2bv_rewriter::imp {
         bool rewrite_patterns() const { return false; }
         bool flat_assoc(func_decl * f) const { return false; }
         br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-            result_pr = 0;
+            result_pr = nullptr;
             return m_r.mk_app_core(f, num, args, result);
         }
         card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
+        void keep_cardinality_constraints(bool f) { m_r.keep_cardinality_constraints(f); }
+        void set_pb_solver(symbol const& s) { m_r.set_pb_solver(s); }
+        void set_at_most1(sorting_network_encoding enc) { m_r.set_at_most1(enc); }
+
     };
     
     class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
@@ -415,22 +914,77 @@ struct pb2bv_rewriter::imp {
         card_pb_rewriter(imp& i, ast_manager & m):
             rewriter_tpl<card2bv_rewriter_cfg>(m, false, m_cfg),
             m_cfg(i, m) {}
+        void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); }
+        void set_pb_solver(symbol const& s) { m_cfg.set_pb_solver(s); }
+        void set_at_most1(sorting_network_encoding e) { m_cfg.set_at_most1(e); }
+        void rewrite(bool full, expr* e, expr_ref& r, proof_ref& p) {
+            expr_ref ee(e, m());
+            if (m_cfg.m_r.mk_app(full, e, r)) {
+                ee = r;
+                // mp proof?
+            }
+            (*this)(ee, r, p);
+        }
     };
 
     card_pb_rewriter m_rw;
     
+    bool keep_cardinality() const {
+        params_ref const& p = m_params;
+        return 
+            p.get_bool("keep_cardinality_constraints", false) ||
+            p.get_bool("sat.cardinality.solver", false) ||
+            p.get_bool("cardinality.solver", false) || 
+            gparams::get_module("sat").get_bool("cardinality.solver", false);
+    }
+
+    symbol pb_solver() const {
+        params_ref const& p = m_params;
+        symbol s = p.get_sym("sat.pb.solver", symbol());
+        if (s != symbol()) return s;
+        s = p.get_sym("pb.solver", symbol());
+        if (s != symbol()) return s;
+        return gparams::get_module("sat").get_sym("pb.solver", symbol("solver"));
+    }
+
+    sorting_network_encoding atmost1_encoding() const {
+        symbol enc = m_params.get_sym("atmost1_encoding", symbol());
+        if (enc == symbol()) {
+            enc = gparams::get_module("sat").get_sym("atmost1_encoding", symbol());
+        }
+        if (enc == symbol("grouped")) return sorting_network_encoding::grouped_at_most_1;
+        if (enc == symbol("bimander")) return sorting_network_encoding::bimander_at_most_1;
+        if (enc == symbol("ordered")) return sorting_network_encoding::ordered_at_most_1;
+        return grouped_at_most_1;
+    }
+    
+
     imp(ast_manager& m, params_ref const& p): 
         m(m), m_params(p), m_lemmas(m),
         m_fresh(m),
         m_num_translated(0), 
         m_rw(*this, m) {
+        updt_params(p);
+        m_compile_bv = 0;
+        m_compile_card = 0;
+    }
+
+    void updt_params(params_ref const & p) {
+        m_params.append(p);
+        m_rw.keep_cardinality_constraints(keep_cardinality());
+        m_rw.set_pb_solver(pb_solver());
+        m_rw.set_at_most1(atmost1_encoding());
+    }
+    void collect_param_descrs(param_descrs& r) const {
+        r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver");
+        r.insert("pb.solver", CPK_SYMBOL, "(default: solver) retain pb constraints (don't bit-blast them) and use built-in pb solver");
     }
 
-    void updt_params(params_ref const & p) {}
     unsigned get_num_steps() const { return m_rw.get_num_steps(); }
     void cleanup() { m_rw.cleanup(); }
-    void operator()(expr * e, expr_ref & result, proof_ref & result_proof) {
-        m_rw(e, result, result_proof);
+    void operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof) {
+        // m_rw(e, result, result_proof);
+        m_rw.rewrite(full, e, result, result_proof);
     }
     void push() {
         m_fresh_lim.push_back(m_fresh.size());
@@ -453,6 +1007,8 @@ struct pb2bv_rewriter::imp {
     }
 
     void collect_statistics(statistics & st) const {
+        st.update("pb-compile-bv", m_compile_bv);
+        st.update("pb-compile-card", m_compile_card);
         st.update("pb-aux-variables", m_fresh.size());
         st.update("pb-aux-clauses", m_rw.m_cfg.m_r.m_sort.m_stats.m_num_compiled_clauses);
     }
@@ -463,11 +1019,13 @@ struct pb2bv_rewriter::imp {
 pb2bv_rewriter::pb2bv_rewriter(ast_manager & m, params_ref const& p) {  m_imp = alloc(imp, m, p); }
 pb2bv_rewriter::~pb2bv_rewriter() { dealloc(m_imp); }
 void pb2bv_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); }
+void pb2bv_rewriter::collect_param_descrs(param_descrs& r) const { m_imp->collect_param_descrs(r); }
+
 ast_manager & pb2bv_rewriter::m() const { return m_imp->m; }
 unsigned pb2bv_rewriter::get_num_steps() const { return m_imp->get_num_steps(); }
 void pb2bv_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p);  }
 func_decl_ref_vector const& pb2bv_rewriter::fresh_constants() const { return m_imp->m_fresh; }
-void pb2bv_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); }
+void pb2bv_rewriter::operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(full, e, result, result_proof); }
 void pb2bv_rewriter::push() { m_imp->push(); }
 void pb2bv_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); }
 void pb2bv_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } 

src/ast/rewriter/pb2bv_rewriter.h

@@ -31,11 +31,12 @@ public:
     ~pb2bv_rewriter();
 
     void updt_params(params_ref const & p);
+    void collect_param_descrs(param_descrs& r) const;
     ast_manager & m() const;
     unsigned get_num_steps() const;
     void cleanup();
     func_decl_ref_vector const& fresh_constants() const;
-    void operator()(expr * e, expr_ref & result, proof_ref & result_proof);
+    void operator()(bool full, expr * e, expr_ref & result, proof_ref & result_proof);
     void push();
     void pop(unsigned num_scopes);
     void flush_side_constraints(expr_ref_vector& side_constraints);

src/ast/rewriter/pb_rewriter.cpp

@@ -115,14 +115,15 @@ expr_ref pb_rewriter::translate_pb2lia(obj_map<expr,expr*>& vars, expr* fml) {
         else {
             tmp = a.mk_add(es.size(), es.c_ptr());
         }
+        rational k = util.get_k(fml);
         if (util.is_le(fml)) {
-            result = a.mk_le(tmp, a.mk_numeral(util.get_k(fml), false));
+            result = a.mk_le(tmp, a.mk_numeral(k, false));
         }
         else if (util.is_ge(fml)) {
-            result = a.mk_ge(tmp, a.mk_numeral(util.get_k(fml), false));
+            result = a.mk_ge(tmp, a.mk_numeral(k, false));
         }
         else {
-            result = m().mk_eq(tmp, a.mk_numeral(util.get_k(fml), false));
+            result = m().mk_eq(tmp, a.mk_numeral(k, false));
         }
     }
     else {
@@ -233,6 +234,7 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
     }    
 
     bool is_eq = f->get_decl_kind() == OP_PB_EQ;
+    br_status st = BR_DONE;
     
     pb_ast_rewriter_util pbu(m);
     pb_rewriter_util<pb_ast_rewriter_util> util(pbu);
@@ -250,29 +252,73 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
     default: {
         bool all_unit = true;
         unsigned sz = vec.size();
+        rational slack(0);
         m_args.reset();
         m_coeffs.reset();
-        for (unsigned i = 0; i < sz; ++i) {
-            m_args.push_back(vec[i].first);
-            m_coeffs.push_back(vec[i].second);
+        for (auto const& kv : vec) {
+            m_args.push_back(kv.first);
+            m_coeffs.push_back(kv.second);
+            SASSERT(kv.second.is_pos());
+            slack += kv.second;
             all_unit &= m_coeffs.back().is_one();
         }
         if (is_eq) {
             if (sz == 0) {
                 result = k.is_zero()?m.mk_true():m.mk_false();
             }
+            else if (k.is_zero()) {
+                result = mk_not(m, mk_or(m, sz, m_args.c_ptr()));
+            }
+            else if (k.is_one() && all_unit && m_args.size() == 1) {
+                result = m_args.back();
+            }
+            else if (slack == k) {
+                result = mk_and(m, sz, m_args.c_ptr());
+            }
             else {
                 result = m_util.mk_eq(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
             }
         }
-        else if (all_unit && k.is_one()) {
+        else if (all_unit && k.is_one() && sz < 10) {
             result = mk_or(m, sz, m_args.c_ptr());
         }
         else if (all_unit && k == rational(sz)) {
             result = mk_and(m, sz, m_args.c_ptr());
         }
         else {
-            result = m_util.mk_ge(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k);
+            expr_ref_vector conj(m), disj(m);
+            unsigned j = 0; 
+            sz = m_args.size();
+            for (unsigned i = 0; i < sz; ++i) {
+                rational& c = m_coeffs[i];
+                if (slack < c + k) {
+                    conj.push_back(m_args[i]);
+                    slack -= c;
+                    k -= c;
+                }
+                else if (c >= k && k.is_pos()) {
+                    disj.push_back(m_args[i]);
+                }
+                else {
+                    m_args[j] = m_args[i];
+                    m_coeffs[j] = m_coeffs[i];
+                    ++j;
+                }
+            }
+            m_args.shrink(j);
+            m_coeffs.shrink(j);
+            sz = j;
+            if (sz > 0) {
+                disj.push_back(m_util.mk_ge(sz, m_coeffs.c_ptr(), m_args.c_ptr(), k));
+            }
+            if (!disj.empty()) {
+                conj.push_back(mk_or(disj));
+            }
+            result = mk_and(conj);
+
+            if (disj.size() > 1 || conj.size() > 1) {               
+                st = BR_REWRITE3;
+            }            
         }
         break;
     }
@@ -283,11 +329,11 @@ br_status pb_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons
           tout << tmp << "\n";
           tout << result << "\n";
           );
-
+    
     TRACE("pb_validate",
           validate_rewrite(f, num_args, args, result););
           
-    return BR_DONE;
+    return st;
 }
 
 

src/ast/rewriter/pb_rewriter_def.h

@@ -45,25 +45,25 @@ void pb_rewriter_util<PBU>::unique(typename PBU::args_t& args, typename PBU::num
         }
     }
     // remove constants
-    for (unsigned i = 0; i < args.size(); ++i) {
+    unsigned j = 0, sz = args.size();
+    for (unsigned i = 0; i < sz; ++i) {
         if (m_util.is_true(args[i].first)) {
             k -= args[i].second;
-            std::swap(args[i], args[args.size()-1]);
-            args.pop_back();
-            --i;
         }
         else if (m_util.is_false(args[i].first)) {
-            std::swap(args[i], args[args.size()-1]);
-            args.pop_back();                
-            --i;
+            // no-op
+        }
+        else {
+            args[j++] = args[i];
         }
     }
+    args.shrink(j);
     // sort and coalesce arguments:
     typename PBU::compare cmp;
     std::sort(args.begin(), args.end(), cmp);
 
     // coallesce
-    unsigned i, j;
+    unsigned i;
     for (i = 0, j = 1; j < args.size(); ++j) {
         if (args[i].first == args[j].first) {
             args[i].second += args[j].second;

src/ast/rewriter/poly_rewriter.h

@@ -96,7 +96,7 @@ protected:
 public:
     poly_rewriter(ast_manager & m, params_ref const & p = params_ref()):
         Config(m),
-        m_curr_sort(0),
+        m_curr_sort(nullptr),
         m_sort_sums(false) {
         updt_params(p);
         SASSERT(!m_som || m_flat); // som of monomials form requires flattening to be enabled.

src/ast/rewriter/poly_rewriter_def.h

@@ -206,7 +206,7 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
     numeral c(1);
     unsigned num_coeffs = 0;
     unsigned num_add    = 0;
-    expr *  var         = 0;
+    expr *  var         = nullptr;
     for (unsigned i = 0; i < num_args; i++) {
         expr * arg = args[i];
         if (is_numeral(arg, a)) {
@@ -290,13 +290,13 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
 
     if (!m_som || num_add == 0) {
         ptr_buffer<expr> new_args;
-        expr * prev = 0;
+        expr * prev = nullptr;
         bool ordered = true;
         for (unsigned i = 0; i < num_args; i++) {
             expr * curr = args[i];
             if (is_numeral(curr))
                 continue;
-            if (prev != 0 && lt(curr, prev))
+            if (prev != nullptr && lt(curr, prev))
                 ordered = false;
             new_args.push_back(curr);
             prev = curr;
@@ -431,7 +431,8 @@ struct poly_rewriter<Config>::hoist_cmul_lt {
     hoist_cmul_lt(poly_rewriter<Config> & r):m_r(r) {}
 
     bool operator()(expr * t1, expr * t2) const {
-        expr * pp1, * pp2;
+        expr * pp1 = nullptr;
+        expr * pp2 = nullptr;
         numeral c1, c2;
         bool is_mul1 = m_r.is_mul(t1, c1, pp1);
         bool is_mul2 = m_r.is_mul(t2, c2, pp2);
@@ -532,7 +533,7 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
     expr_fast_mark1 visited;  // visited.is_marked(power_product) if the power_product occurs in args
     expr_fast_mark2 multiple; // multiple.is_marked(power_product) if power_product occurs more than once
     bool     has_multiple = false;
-    expr *   prev = 0;
+    expr *   prev = nullptr;
     bool     ordered  = true;
     for (unsigned i = 0; i < num_args; i++) {
         expr * arg = args[i];
@@ -543,7 +544,7 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
             ordered = !m_sort_sums || i == 0;
         }
         else if (m_sort_sums && ordered) {
-            if (prev != 0 && lt(arg, prev)) 
+            if (prev != nullptr && lt(arg, prev))
                 ordered = false;
             prev = arg;        
         }
@@ -874,8 +875,8 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
     const bool insert_c_rhs =  c_at_rhs && (new_rhs_monomials.size() == 1 || !c.is_zero());
     const unsigned lhs_offset = insert_c_lhs ? 0 : 1;
     const unsigned rhs_offset = insert_c_rhs ? 0 : 1;
-    new_rhs_monomials[0] = insert_c_rhs ? mk_numeral(c) : NULL;
-    new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : NULL;
+    new_rhs_monomials[0] = insert_c_rhs ? mk_numeral(c) : nullptr;
+    new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : nullptr;
     lhs_result = mk_add_app(new_lhs_monomials.size() - lhs_offset, new_lhs_monomials.c_ptr() + lhs_offset);
     rhs_result = mk_add_app(new_rhs_monomials.size() - rhs_offset, new_rhs_monomials.c_ptr() + rhs_offset);
     TRACE("mk_le_bug", tout << lhs_result << " " << rhs_result << "\n";);
@@ -994,7 +995,7 @@ bool poly_rewriter<Config>::is_var_plus_ground(expr * n, bool & inv, var * & v,
         return false;
     
     ptr_buffer<expr> args;
-    v = 0;
+    v = nullptr;
     expr * curr = to_app(n);
     bool stop = false;
     inv = false;
@@ -1013,12 +1014,12 @@ bool poly_rewriter<Config>::is_var_plus_ground(expr * n, bool & inv, var * & v,
             args.push_back(arg);
         }
         else if (is_var(arg)) {
-            if (v != 0)
+            if (v != nullptr)
                 return false; // already found variable
             v = to_var(arg);
         }
         else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) {
-            if (v != 0)
+            if (v != nullptr)
                 return false; // already found variable
             v = to_var(neg_arg);
             inv = true;
@@ -1027,7 +1028,7 @@ bool poly_rewriter<Config>::is_var_plus_ground(expr * n, bool & inv, var * & v,
             return false; // non ground term.
         }
     }
-    if (v == 0)
+    if (v == nullptr)
         return false; // did not find variable
     SASSERT(!args.empty());
     mk_add(args.size(), args.c_ptr(), t);

src/ast/rewriter/pull_ite_tree.cpp

@@ -1,221 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    pull_ite_tree.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-06-22.
-
-Revision History:
-
---*/
-#include "ast/rewriter/pull_ite_tree.h"
-#include "ast/recurse_expr_def.h"
-#include "ast/for_each_expr.h"
-#include "ast/ast_pp.h"
-
-pull_ite_tree::pull_ite_tree(ast_manager & m):
-    m_manager(m),
-    m_rewriter(m),
-    m_cache(m) {
-}
-
-void pull_ite_tree::cache_result(expr * n, expr * r, proof * pr) { 
-    m_cache.insert(n, r, pr); 
-}
-
-void pull_ite_tree::visit(expr * n, bool & visited) {
-    if (!is_cached(n)) {
-        m_todo.push_back(n);
-        visited = false;
-    }
-}
-
-bool pull_ite_tree::visit_children(expr * n) {
-    if (m_manager.is_ite(n)) {
-        bool visited = true;
-        visit(to_app(n)->get_arg(1), visited);
-        visit(to_app(n)->get_arg(2), visited);
-        return visited;
-    }
-    else {
-        return true;
-    }
-}
-
-void pull_ite_tree::reduce(expr * n) {
-    // Remark: invoking the simplifier to build the new expression saves a lot of memory.
-    if (m_manager.is_ite(n)) {
-        expr * c = to_app(n)->get_arg(0);
-        expr * t_old = to_app(n)->get_arg(1);
-        expr * e_old = to_app(n)->get_arg(2);
-        expr * t     = 0;
-        proof * t_pr = 0;
-        expr * e     = 0;
-        proof * e_pr = 0;
-        get_cached(t_old, t, t_pr);
-        get_cached(e_old, e, e_pr);
-        expr_ref r(m_manager);
-        expr * args[3] = {c, t, e};
-        r = m_rewriter.mk_app(to_app(n)->get_decl(), 3, args);
-        if (!m_manager.proofs_enabled()) {
-            // expr * r = m_manager.mk_ite(c, t, e);
-            cache_result(n, r, 0);
-        }
-        else {
-            // t_pr is a proof for (m_p ... t_old ...) == t
-            // e_pr is a proof for (m_p ... e_old ...) == e
-            expr_ref old(m_manager);
-            expr_ref p_t_old(m_manager);
-            expr_ref p_e_old(m_manager);
-            old     = mk_p_arg(n); // (m_p ... n ...) where n is (ite c t_old e_old)
-            p_t_old = mk_p_arg(t_old); // (m_p ... t_old ...)
-            p_e_old = mk_p_arg(e_old); // (m_p ... e_old ...)
-            expr_ref tmp1(m_manager);
-            tmp1 = m_manager.mk_ite(c, p_t_old, p_e_old); // (ite c (m_p ... t_old ...) (m_p ... e_old ...))
-            proof * pr1 = m_manager.mk_rewrite(old, tmp1);  // proof for (m_p ... (ite c t_old e_old) ...) = (ite c (m_p ... t_old ...) (m_p ... e_old ...))
-            expr_ref tmp2(m_manager);
-            tmp2 = m_manager.mk_ite(c, t, e); // (ite c t e)
-            proof * pr2 = 0; // it will contain a proof for (ite c (m_p ... t_old ...) (m_p ... e_old ...)) = (ite c t e)
-            proof * pr3 = 0; // it will contain a proof for (m_p ... (ite c t_old e_old) ...)               = (ite c t e)
-            proof * proofs[2];
-            unsigned num_proofs = 0;
-            if (t_pr != 0) {
-                proofs[num_proofs] = t_pr;
-                num_proofs++;
-            }
-            if (e_pr != 0) {
-                proofs[num_proofs] = e_pr;
-                num_proofs++;
-            }
-            if (num_proofs > 0) {
-                pr2 = m_manager.mk_congruence(to_app(tmp1), to_app(tmp2), num_proofs, proofs);
-                pr3 = m_manager.mk_transitivity(pr1, pr2);
-            }
-            else {
-                pr3 = pr1;
-            }
-            proof * pr4 = 0; // it will contain a proof for (ite c t e) = r
-            proof * pr5 = 0; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = r
-            if (tmp2 != r) {
-                pr4 = m_manager.mk_rewrite(tmp2, r);
-                pr5 = m_manager.mk_transitivity(pr3, pr4);
-            }
-            else {
-                pr5 = pr3;
-            }
-            cache_result(n, r, pr5);
-        }
-    }
-    else {
-        expr_ref r(m_manager);
-        m_args[m_arg_idx] = n;
-        r = m_rewriter.mk_app(m_p, m_args.size(), m_args.c_ptr());
-        if (!m_manager.proofs_enabled()) {
-            // expr * r = m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
-            cache_result(n, r, 0);
-        }
-        else {
-            expr_ref old(m_manager);
-            proof * p;
-            old = mk_p_arg(n);
-            if (old == r)
-                p = 0;
-            else
-                p = m_manager.mk_rewrite(old, r);
-            cache_result(n, r, p);
-        }
-    }
-}
-
-void pull_ite_tree::operator()(app * n, app_ref & r, proof_ref & pr) {
-    unsigned num_args = n->get_num_args();
-    m_args.resize(num_args);
-    m_p = n->get_decl();
-    expr * ite = 0;
-    for (unsigned i = 0; i < num_args; i++) {
-        expr * arg = n->get_arg(i);
-        if (ite) {
-            m_args[i] = arg;
-        }
-        else if (m_manager.is_ite(arg)) {
-            m_arg_idx = i;
-            m_args[i] = 0;
-            ite       = arg;
-        }
-        else {
-            m_args[i] = arg;
-        }
-    }
-    if (!ite) {
-        r = n;
-        pr = 0;
-        return;
-    }
-    m_todo.push_back(ite);
-    while (!m_todo.empty()) {
-        expr * n = m_todo.back();
-        if (is_cached(n))
-            m_todo.pop_back();
-        else if (visit_children(n)) {
-            m_todo.pop_back();
-            reduce(n);
-        }
-    }
-    SASSERT(is_cached(ite));
-    expr *   _r = 0;
-    proof * _pr = 0;
-    get_cached(ite, _r, _pr);
-    r  = to_app(_r);
-    pr = _pr;
-    m_cache.reset();
-    m_todo.reset();
-}
-
-
-
-pull_ite_tree_cfg::pull_ite_tree_cfg(ast_manager & m):
-    m(m),
-    m_trail(m),
-    m_proc(m) {
-}
-
-bool pull_ite_tree_cfg::get_subst(expr * n, expr* & r, proof* & p) {
-    if (is_app(n) && is_target(to_app(n))) {
-        app_ref tmp(m);
-        proof_ref pr(m);
-        m_proc(to_app(n), tmp, pr);
-        if (tmp != n) {
-            r = tmp;
-            p = pr;
-            m_trail.push_back(r);
-            m_trail.push_back(p);
-            return true;
-        }
-    }
-    return false;
-}
-
-bool pull_cheap_ite_tree_cfg::is_target(app * n) const {
-    bool r = 
-        n->get_num_args() == 2 &&
-        n->get_family_id() != null_family_id &&
-        m.is_bool(n) &&
-        (m.is_value(n->get_arg(0)) || m.is_value(n->get_arg(1))) &&
-        (m.is_term_ite(n->get_arg(0)) || m.is_term_ite(n->get_arg(1)));
-    TRACE("pull_ite_target", tout << mk_pp(n, m) << "\nresult: " << r << "\n";);
-    return r;
-}
-
-
-
-
-
-

src/ast/rewriter/pull_ite_tree.h

@@ -1,113 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    pull_ite_tree.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-06-22.
-
-Revision History:
-
---*/
-#ifndef PULL_ITE_TREE_H_
-#define PULL_ITE_TREE_H_
-
-#include "ast/ast.h"
-#include "ast/rewriter/rewriter.h"
-#include "ast/rewriter/th_rewriter.h"
-#include "ast/expr_map.h"
-#include "ast/recurse_expr.h"
-#include "util/obj_hashtable.h"
-
-/**
-   \brief Functor for applying the following transformation
-   F[(p (ite c t1 t2) args)] = F'[(ite c t1 t2), p, args]
-
-   F'[(ite c t1 t2), p, args] = (ite c F'[t1, p, args] F'[t2, p, args])
-   F'[t, p, args] = (p t args)
-*/
-class pull_ite_tree {
-    ast_manager &         m_manager;
-    th_rewriter           m_rewriter;
-    func_decl *           m_p;
-    ptr_vector<expr>      m_args;
-    unsigned              m_arg_idx; //!< position of the ite argument
-    expr_map              m_cache;
-    ptr_vector<expr>      m_todo;
-
-    bool is_cached(expr * n) const { return m_cache.contains(n); }
-    void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); }
-    void cache_result(expr * n, expr * r, proof * pr);
-    void visit(expr * n, bool & visited);
-    bool visit_children(expr * n);
-    void reduce(expr * n);
-    /**
-       \brief Creante an application (m_p ... n ...) where n is the argument m_arg_idx and the other arguments
-       are in m_args.
-    */
-    expr * mk_p_arg(expr * n) {
-        m_args[m_arg_idx] = n;
-        return m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
-    }
-public:
-    pull_ite_tree(ast_manager & m);
-    /**
-       \brief Apply the transformation above if n contains an ite-expression.
-       Store the result in r. If n does not contain an ite-expression, then
-       store n in r.
-
-       When proof generation is enabled, pr is a proof for n = r.
-    */
-    void operator()(app * n, app_ref & r, proof_ref & pr);
-};
-
-/**
-   \brief Functor for applying the pull_ite_tree on subexpressions n that
-   satisfy the is_target virtual predicate.
-*/
-class pull_ite_tree_cfg : public default_rewriter_cfg {
-protected:
-    ast_manager& m;
-    expr_ref_vector m_trail;
-    pull_ite_tree m_proc;
-public:
-    pull_ite_tree_cfg(ast_manager & m);
-    virtual ~pull_ite_tree_cfg() {}
-    virtual bool is_target(app * n) const = 0;
-    bool get_subst(expr * n, expr* & r, proof* & p);
-};
-
-/**
-   \brief Apply pull_ite_tree on predicates of the form
-   (p ite v) and (p v ite)
-
-   where:
-   - p is an interpreted predicate
-   - ite is an ite-term expression
-   - v is a value
-*/
-class pull_cheap_ite_tree_cfg : public pull_ite_tree_cfg {
-public:
-    pull_cheap_ite_tree_cfg(ast_manager & m):pull_ite_tree_cfg(m) {}
-    virtual ~pull_cheap_ite_tree_cfg() {}
-    virtual bool is_target(app * n) const;
-};
-
-class pull_cheap_ite_tree_rw  : public rewriter_tpl<pull_cheap_ite_tree_cfg> {
-    pull_cheap_ite_tree_cfg m_cfg;
-public:
-    pull_cheap_ite_tree_rw(ast_manager& m):
-        rewriter_tpl<pull_cheap_ite_tree_cfg>(m, m.proofs_enabled(), m_cfg),
-        m_cfg(m)
-    {}
-};
-
-#endif /* PULL_ITE_TREE_H_ */
-

src/ast/rewriter/push_app_ite.cpp

@@ -63,7 +63,7 @@ br_status push_app_ite_cfg::reduce_app(func_decl * f, unsigned num, expr * const
         return BR_FAILED;
     }
     app * ite               = to_app(args[ite_arg_idx]);
-    expr * c = 0, * t = 0, * e = 0;
+    expr * c = nullptr, * t = nullptr, * e = nullptr;
     VERIFY(m.is_ite(ite, c, t, e));
     expr ** args_prime      = const_cast<expr**>(args);
     expr * old              = args_prime[ite_arg_idx];

src/ast/rewriter/push_app_ite.h

@@ -45,7 +45,7 @@ struct push_app_ite_cfg : public default_rewriter_cfg {
 */
 class ng_push_app_ite_cfg : public push_app_ite_cfg {
 protected:
-    virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args);
+    bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override;
 public:
     ng_push_app_ite_cfg(ast_manager& m, bool conservative = true): push_app_ite_cfg(m, conservative) {}
     virtual ~ng_push_app_ite_cfg() {}

src/ast/rewriter/quant_hoist.cpp

@@ -259,7 +259,7 @@ private:
                     result = m.mk_ite(t1, tt2, tt3);
                 }
             }
-            else if ((m.is_eq(fml, t1, t2) && m.is_bool(t1)) || m.is_iff(fml, t1, t2)) {
+            else if (m.is_eq(fml, t1, t2) && m.is_bool(t1)) {
                 expr_ref tt1(m), tt2(m), ntt1(m), ntt2(m), nt1(m), nt2(m);
                 pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok);
                 pull_quantifier(t2, qt, vars, tt2, use_fresh, rewrite_ok);

src/ast/rewriter/rewriter.cpp

@@ -34,11 +34,11 @@ void rewriter_core::init_cache_stack() {
 void rewriter_core::del_cache_stack() {
     std::for_each(m_cache_stack.begin(), m_cache_stack.end(), delete_proc<cache>());
     m_cache_stack.finalize();
-    m_cache = 0;
+    m_cache = nullptr;
     if (m_proof_gen) {
         std::for_each(m_cache_pr_stack.begin(), m_cache_pr_stack.end(), delete_proc<cache>());
         m_cache_pr_stack.finalize();
-        m_cache_pr = 0;
+        m_cache_pr = nullptr;
     }
 }
 
@@ -161,7 +161,7 @@ void rewriter_core::elim_reflex_prs(unsigned spos) {
     unsigned j = spos;
     for (unsigned i = spos; i < sz; i++) {
         proof * pr = m_result_pr_stack.get(i);
-        if (pr != 0) {
+        if (pr != nullptr) {
             if (i != j)
                 m_result_pr_stack.set(j, pr);
             j++;
@@ -192,7 +192,7 @@ void rewriter_core::reset() {
     m_result_stack.reset();
     if (m_proof_gen)
         m_result_pr_stack.reset();
-    m_root = 0;
+    m_root = nullptr;
     m_num_qvars = 0;
     m_scopes.reset();
 }
@@ -201,7 +201,7 @@ void rewriter_core::reset() {
 void rewriter_core::cleanup() {
     free_memory();
     init_cache_stack();
-    m_root       = 0;
+    m_root       = nullptr;
     m_num_qvars  = 0;
 }
 

src/ast/rewriter/rewriter.h

@@ -150,7 +150,7 @@ class var_shifter : public var_shifter_core {
     unsigned  m_bound;
     unsigned  m_shift1;
     unsigned  m_shift2;
-    virtual void process_var(var * v);
+    void process_var(var * v) override;
 public:
     var_shifter(ast_manager & m):var_shifter_core(m) {}
     void operator()(expr * t, unsigned bound, unsigned shift1, unsigned shift2, expr_ref & r);
@@ -183,7 +183,7 @@ public:
 class inv_var_shifter : public var_shifter_core {
 protected:
     unsigned m_shift;
-    virtual void process_var(var * v);
+    void process_var(var * v) override;
 public:
     inv_var_shifter(ast_manager & m):var_shifter_core(m) {}
     void operator()(expr * t, unsigned shift, expr_ref & r);
@@ -339,13 +339,15 @@ public:
     Config & cfg() { return m_cfg; }
     Config const & cfg() const { return m_cfg; }
 
-    ~rewriter_tpl();
+    ~rewriter_tpl() override;
     
     void reset();
     void cleanup();
     
     void set_bindings(unsigned num_bindings, expr * const * bindings);
     void set_inv_bindings(unsigned num_bindings, expr * const * bindings);
+    void update_binding_at(unsigned i, expr* binding);
+    void update_inv_binding_at(unsigned i, expr* binding);
     void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
     void operator()(expr * t, expr_ref & result) { operator()(t, result, m_pr); }
     void operator()(expr * n, unsigned num_bindings, expr * const * bindings, expr_ref & result) {

src/ast/rewriter/rewriter_def.h

@@ -28,11 +28,11 @@ void rewriter_tpl<Config>::process_var(var * v) {
         SASSERT(v->get_sort() == m().get_sort(m_r));
         if (ProofGen) {
             result_pr_stack().push_back(m_pr);
-            m_pr = 0;
+            m_pr = nullptr;
         }
         set_new_child_flag(v);
         TRACE("rewriter", tout << mk_ismt2_pp(v, m()) << " -> " << m_r << "\n";);
-        m_r = 0;
+        m_r = nullptr;
         return;
     }
     if (!ProofGen) {
@@ -41,7 +41,7 @@ void rewriter_tpl<Config>::process_var(var * v) {
         if (idx < m_bindings.size()) {
             unsigned index = m_bindings.size() - idx - 1;
             var * r = (var*)(m_bindings[index]);
-            if (r != 0) {
+            if (r != nullptr) {
                 CTRACE("rewriter", v->get_sort() != m().get_sort(r),
                        tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m());
                        tout << "index " << index << " bindings " << m_bindings.size() << "\n";
@@ -67,14 +67,14 @@ void rewriter_tpl<Config>::process_var(var * v) {
     }
     result_stack().push_back(v);
     if (ProofGen)
-        result_pr_stack().push_back(0); // implicit reflexivity
+        result_pr_stack().push_back(nullptr); // implicit reflexivity
 }
 
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::process_const(app * t) {
     SASSERT(t->get_num_args() == 0);
-    br_status st = m_cfg.reduce_app(t->get_decl(), 0, 0, m_r, m_pr);
+    br_status st = m_cfg.reduce_app(t->get_decl(), 0, nullptr, m_r, m_pr);
     SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
     SASSERT(st == BR_FAILED || st == BR_DONE);
     if (st == BR_DONE) {
@@ -84,15 +84,15 @@ void rewriter_tpl<Config>::process_const(app * t) {
                 result_pr_stack().push_back(m_pr);
             else
                 result_pr_stack().push_back(m().mk_rewrite(t, m_r));
-            m_pr = 0;
+            m_pr = nullptr;
         }
-        m_r = 0;
+        m_r = nullptr;
         set_new_child_flag(t);
     }
     else {
         result_stack().push_back(t);
         if (ProofGen)
-            result_pr_stack().push_back(0); // implicit reflexivity
+            result_pr_stack().push_back(nullptr); // implicit reflexivity
     }
 }
 
@@ -108,8 +108,8 @@ template<typename Config>
 template<bool ProofGen>
 bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
     TRACE("rewriter_visit", tout << "visiting\n" << mk_ismt2_pp(t, m()) << "\n";);
-    expr *  new_t = 0;
-    proof * new_t_pr = 0;
+    expr *  new_t = nullptr;
+    proof * new_t_pr = nullptr;
     if (m_cfg.get_subst(t, new_t, new_t_pr)) {
         TRACE("rewriter_subst", tout << "subst\n" << mk_ismt2_pp(t, m()) << "\n---->\n" << mk_ismt2_pp(new_t, m()) << "\n";);
         SASSERT(m().get_sort(t) == m().get_sort(new_t));
@@ -122,7 +122,7 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
     if (max_depth == 0) {
         result_stack().push_back(t);
         if (ProofGen)
-            result_pr_stack().push_back(0); // implicit reflexivity
+            result_pr_stack().push_back(nullptr); // implicit reflexivity
         return true; // t is not going to be processed
     }
     SASSERT(max_depth > 0);
@@ -150,7 +150,7 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
     if (!pre_visit(t)) {
         result_stack().push_back(t);
         if (ProofGen)
-            result_pr_stack().push_back(0); // implicit reflexivity
+            result_pr_stack().push_back(nullptr); // implicit reflexivity
         return true; // t is not going to be processed
     }
     switch (t->get_kind()) {
@@ -183,7 +183,7 @@ template<typename Config>
 bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
     if (fr.m_i == 1 && m().is_ite(t)) {
         expr * cond = result_stack()[fr.m_spos].get();
-        expr* arg = 0;
+        expr* arg = nullptr;
         if (m().is_true(cond)) {
             arg = t->get_arg(1);
         }
@@ -194,16 +194,18 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
             result_stack().shrink(fr.m_spos);
             result_stack().push_back(arg);
             fr.m_state = REWRITE_BUILTIN;
+            TRACE("rewriter_step", tout << "step\n" << mk_ismt2_pp(t, m()) << "\n";);
             if (visit<false>(arg, fr.m_max_depth)) {
                 m_r = result_stack().back();
                 result_stack().pop_back();
                 result_stack().pop_back();
                 result_stack().push_back(m_r);
                 cache_result<false>(t, m_r, m_pr, fr.m_cache_result);
+                TRACE("rewriter_step", tout << "step 1\n" << mk_ismt2_pp(m_r, m()) << "\n";);
                 frame_stack().pop_back();
                 set_new_child_flag(t);
             }
-            m_r = 0;
+            m_r = nullptr;
             return true;
         }
     }
@@ -255,7 +257,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
             unsigned num_prs    = result_pr_stack().size() - fr.m_spos;
             if (num_prs == 0) {
                 new_t = t;
-                m_pr  = 0;
+                m_pr  = nullptr;
             }
             else {
                 new_t = m().mk_app(f, new_num_args, new_args);
@@ -278,16 +280,16 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                 if (!m_pr2)
                     m_pr2 = m().mk_rewrite(new_t, m_r);
                 m_pr  = m().mk_transitivity(m_pr, m_pr2);
-                m_pr2 = 0;
+                m_pr2 = nullptr;
                 result_pr_stack().push_back(m_pr);
             }
             if (st == BR_DONE) {
                 cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
                 frame_stack().pop_back();
                 set_new_child_flag(t);
-                m_r = 0;
+                m_r = nullptr;
                 if (ProofGen)
-                    m_pr = 0;
+                    m_pr = nullptr;
                 return;
             }
             else {
@@ -318,25 +320,25 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                     cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
                     frame_stack().pop_back();
                     set_new_child_flag(t);
-                    m_r = 0;
+                    m_r = nullptr;
                     if (ProofGen)
-                        m_pr = 0;
+                        m_pr = nullptr;
                     return;
                 }
                 else {
                     // frame was created for processing m_r
-                    m_r = 0;
+                    m_r = nullptr;
                     if (ProofGen)
-                        m_pr = 0;
+                        m_pr = nullptr;
                     return;
                 }
             }
             UNREACHABLE();
         }
         // TODO: add rewrite rules support
-        expr * def;
-        proof * def_pr;
-        quantifier * def_q;
+        expr * def = nullptr;
+        proof * def_pr = nullptr;
+        quantifier * def_q = nullptr;
         // When get_macro succeeds, then
         // we know that:
         // forall X. f(X) = def[X]
@@ -358,7 +360,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                 if (ProofGen) {
                     NOT_IMPLEMENTED_YET();
                     // We do not support the use of bindings in proof generation mode.
-                    // Thus we have to apply the subsitution here, and
+                    // Thus we have to apply the substitution here, and
                     // beta_reducer subst(m());
                     // subst.set_bindings(new_num_args, new_args);
                     // expr_ref r2(m());
@@ -407,11 +409,11 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
         if (ProofGen) {
             result_pr_stack().shrink(fr.m_spos);
             result_pr_stack().push_back(m_pr);
-            m_pr = 0;
+            m_pr = nullptr;
         }
         frame_stack().pop_back();
         set_new_child_flag(t, m_r);
-        m_r = 0;
+        m_r = nullptr;
         return;
     }
     case REWRITE_BUILTIN:
@@ -497,23 +499,27 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
     SASSERT(fr.m_spos + num_children == result_stack().size());
     expr * const * it = result_stack().c_ptr() + fr.m_spos;
     expr * new_body   = *it;
-    expr * const * new_pats;
-    expr * const * new_no_pats;
+    unsigned num_pats = q->get_num_patterns();
+    unsigned num_no_pats = q->get_num_no_patterns();
+    expr_ref_vector new_pats(m_manager, num_pats, q->get_patterns());
+    expr_ref_vector new_no_pats(m_manager, num_no_pats, q->get_no_patterns());
     if (rewrite_patterns()) {
         TRACE("reduce_quantifier_bug", tout << "rewrite patterns\n";);
-        new_pats    = it + 1;
-        new_no_pats = new_pats + q->get_num_patterns();
-    }
-    else {
-        new_pats    = q->get_patterns();
-        new_no_pats = q->get_no_patterns();
+        expr * const * np  = it + 1;
+        expr * const * nnp = np + num_pats;
+        for (unsigned i = 0; i < num_pats; i++)
+            if (m_manager.is_pattern(np[i]))
+                new_pats[i] = np[i];
+        for (unsigned i = 0; i < num_no_pats; i++)
+            if (m_manager.is_pattern(nnp[i]))
+                new_no_pats[i] = nnp[i];
     }
     if (ProofGen) {
-        quantifier_ref new_q(m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body), m());
-        m_pr = q == new_q ? 0 : m().mk_quant_intro(q, new_q, result_pr_stack().get(fr.m_spos));
+        quantifier_ref new_q(m().update_quantifier(q, num_pats, new_pats.c_ptr(), num_no_pats, new_no_pats.c_ptr(), new_body), m());
+        m_pr = q == new_q ? nullptr : m().mk_quant_intro(q, new_q, result_pr_stack().get(fr.m_spos));
         m_r = new_q;
         proof_ref pr2(m());
-        if (m_cfg.reduce_quantifier(new_q, new_body, new_pats, new_no_pats, m_r, pr2)) {
+        if (m_cfg.reduce_quantifier(new_q, new_body, new_pats.c_ptr(), new_no_pats.c_ptr(), m_r, pr2)) {
             m_pr = m().mk_transitivity(m_pr, pr2);
         }
         TRACE("reduce_quantifier_bug", tout << "m_pr is_null: " << (m_pr.get() == 0) << "\n";
@@ -524,9 +530,9 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
     else {
         expr_ref tmp(m());
         TRACE("reduce_quantifier_bug", tout << mk_ismt2_pp(q, m()) << " " << mk_ismt2_pp(new_body, m()) << "\n";);
-        if (!m_cfg.reduce_quantifier(q, new_body, new_pats, new_no_pats, m_r, m_pr)) {
+        if (!m_cfg.reduce_quantifier(q, new_body, new_pats.c_ptr(), new_no_pats.c_ptr(), m_r, m_pr)) {
             if (fr.m_new_child) {
-                m_r = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body);
+                m_r = m().update_quantifier(q, num_pats, new_pats.c_ptr(), num_no_pats, new_no_pats.c_ptr(), new_body);
             }
             else {
                 TRACE("rewriter_reuse", tout << "reusing:\n" << mk_ismt2_pp(q, m()) << "\n";);
@@ -546,9 +552,9 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
     }
     else {
         cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
-        m_pr = 0;
+        m_pr = nullptr;
     }
-    m_r = 0;
+    m_r = nullptr;
     frame_stack().pop_back();
     set_new_child_flag(q, m_r);
 }
@@ -633,6 +639,17 @@ void rewriter_tpl<Config>::set_inv_bindings(unsigned num_bindings, expr * const
     TRACE("rewriter", display_bindings(tout););
 }
 
+template<typename Config>
+void rewriter_tpl<Config>::update_inv_binding_at(unsigned i, expr* binding) {
+    m_bindings[i] = binding;
+}
+
+template<typename Config>
+void rewriter_tpl<Config>::update_binding_at(unsigned i, expr* binding) {
+    m_bindings[m_bindings.size() - i - 1] = binding;
+}
+
+
 template<typename Config>
 template<bool ProofGen>
 void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
@@ -652,7 +669,7 @@ void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & re
         if (ProofGen) {
             result_pr = result_pr_stack().back();
             result_pr_stack().pop_back();
-            if (result_pr.get() == 0)
+            if (result_pr.get() == nullptr)
                 result_pr = m().mk_reflexivity(t);
             SASSERT(result_pr_stack().empty());
         }
@@ -717,7 +734,7 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
     if (ProofGen) {
         result_pr = result_pr_stack().back();
         result_pr_stack().pop_back();
-        if (result_pr.get() == 0)
+        if (result_pr.get() == nullptr)
             result_pr = m().mk_reflexivity(m_root);
         SASSERT(result_pr_stack().empty());
     }

src/ast/rewriter/seq_rewriter.cpp

@@ -85,15 +85,15 @@ public:
     sym_expr_boolean_algebra(ast_manager& m, expr_solver& s): 
         m(m), m_solver(s) {}
 
-    virtual T mk_false() {
+    T mk_false() override {
         expr_ref fml(m.mk_false(), m);
         return sym_expr::mk_pred(fml, m.mk_bool_sort()); // use of Bool sort for bound variable is arbitrary
     }
-    virtual T mk_true() {
+    T mk_true() override {
         expr_ref fml(m.mk_true(), m);
         return sym_expr::mk_pred(fml, m.mk_bool_sort());
     }
-    virtual T mk_and(T x, T y) {
+    T mk_and(T x, T y) override {
         if (x->is_char() && y->is_char()) {
             if (x->get_char() == y->get_char()) {
                 return x;
@@ -118,7 +118,7 @@ public:
         br.mk_and(fml1, fml2, fml);
         return sym_expr::mk_pred(fml, x->get_sort());
     }
-    virtual T mk_or(T x, T y) {
+    T mk_or(T x, T y) override {
         if (x->is_char() && y->is_char() &&
             x->get_char() == y->get_char()) {
             return x;
@@ -135,7 +135,7 @@ public:
         return sym_expr::mk_pred(fml, x->get_sort());
     }
 
-    virtual T mk_and(unsigned sz, T const* ts) {
+    T mk_and(unsigned sz, T const* ts) override {
         switch (sz) {
         case 0: return mk_true();
         case 1: return ts[0];
@@ -148,7 +148,7 @@ public:
         }
         }
     }
-    virtual T mk_or(unsigned sz, T const* ts) {
+    T mk_or(unsigned sz, T const* ts) override {
         switch (sz) {
         case 0: return mk_false();
         case 1: return ts[0];
@@ -161,7 +161,7 @@ public:
         }
         }
     }
-    virtual lbool is_sat(T x) {
+    lbool is_sat(T x) override {
         if (x->is_char()) {
             return l_true;
         }
@@ -178,7 +178,7 @@ public:
         }
         return m_solver.check_sat(fml);
     }
-    virtual T mk_not(T x) {
+    T mk_not(T x) override {
         var_ref v(m.mk_var(0, x->get_sort()), m);
         expr_ref fml(m.mk_not(x->accept(v)), m);
         return sym_expr::mk_pred(fml, x->get_sort());
@@ -190,7 +190,7 @@ public:
     }*/
 };
 
-re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}
+re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(nullptr), m_sa(nullptr) {}
 
 re2automaton::~re2automaton() {}
 
@@ -200,6 +200,9 @@ void re2automaton::set_solver(expr_solver* solver) {
     m_sa = alloc(symbolic_automata_t, sm, *m_ba.get());
 }
 
+eautomaton* re2automaton::mk_product(eautomaton* a1, eautomaton* a2) {
+    return m_sa->mk_product(*a1, *a2);
+}
 
 eautomaton* re2automaton::operator()(expr* e) { 
     eautomaton* r = re2aut(e); 
@@ -286,19 +289,28 @@ eautomaton* re2automaton::re2aut(expr* e) {
     else if (u.re.is_empty(e)) {
         return alloc(eautomaton, sm);
     }
-    else if (u.re.is_full(e)) {
+    else if (u.re.is_full_seq(e)) {
         expr_ref tt(m.mk_true(), m);
-        sort *seq_s = 0, *char_s = 0;
+        sort *seq_s = nullptr, *char_s = nullptr;
         VERIFY (u.is_re(m.get_sort(e), seq_s));
         VERIFY (u.is_seq(seq_s, char_s));
         sym_expr* _true = sym_expr::mk_pred(tt, char_s);
         return eautomaton::mk_loop(sm, _true);
     }
+    else if (u.re.is_full_char(e)) {
+        expr_ref tt(m.mk_true(), m);
+        sort *seq_s = nullptr, *char_s = nullptr;
+        VERIFY (u.is_re(m.get_sort(e), seq_s));
+        VERIFY (u.is_seq(seq_s, char_s));
+        sym_expr* _true = sym_expr::mk_pred(tt, char_s);
+        a = alloc(eautomaton, sm, _true);
+        return a.detach();
+    }
     else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
         return m_sa->mk_product(*a, *b);
     }
     
-    return 0;
+    return nullptr;
 }
 
 eautomaton* re2automaton::seq2aut(expr* e) {
@@ -326,7 +338,7 @@ eautomaton* re2automaton::seq2aut(expr* e) {
         }
         return alloc(eautomaton, sm, init, final, mvs);
     }
-    return 0;
+    return nullptr;
 }
 
 br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@@ -355,6 +367,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         return mk_re_concat(args[0], args[1], result);
     case OP_RE_UNION:
+        if (num_args == 1) {
+            result = args[0]; return BR_DONE;
+        }
         SASSERT(num_args == 2);
         return mk_re_union(args[0], args[1], result);
     case OP_RE_RANGE:
@@ -370,7 +385,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         return mk_re_loop(num_args, args, result);
     case OP_RE_EMPTY_SET:
         return BR_FAILED;    
-    case OP_RE_FULL_SET:
+    case OP_RE_FULL_SEQ_SET:
+        return BR_FAILED;    
+    case OP_RE_FULL_CHAR_SET:
         return BR_FAILED;    
     case OP_RE_OF_PRED:
         return BR_FAILED;    
@@ -839,7 +856,7 @@ br_status seq_rewriter::mk_seq_replace(expr* a, expr* b, expr* c, expr_ref& resu
         return BR_DONE;
     }
     if (m_util.str.is_string(b, s2) && s2.length() == 0) {
-        result = m_util.str.mk_concat(a, c);
+        result = m_util.str.mk_concat(c, a);
         return BR_REWRITE1;
     }
     if (m_util.str.is_string(a, s1) && s1.length() == 0) {
@@ -982,14 +999,14 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
 
     bool isc1 = false;
     bool isc2 = false;
-    expr *a1 = 0, *a2 = 0, *b1 = 0, *b2 = 0;
+    expr *a1 = nullptr, *a2 = nullptr, *b1 = nullptr, *b2 = nullptr;
     if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
         isc1 = true;
     }
     else if (m_util.str.is_string(a, s1)) {
         isc1 = true;
         a2 = a;
-        a1 = 0;
+        a1 = nullptr;
     }
 
     if (m_util.str.is_concat(b, b1, b2) && m_util.str.is_string(b2, s2)) {
@@ -998,7 +1015,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
     else if (m_util.str.is_string(b, s2)) {
         isc2 = true;
         b2 = b;
-        b1 = 0;
+        b1 = nullptr;
     }
     if (isc1 && isc2) {
         if (s1.length() == s2.length()) {
@@ -1008,7 +1025,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
         }
         else if (s1.length() < s2.length()) {
             bool suffix = s1.suffixof(s2);
-            if (suffix && a1 == 0) {
+            if (suffix && a1 == nullptr) {
                 result = m().mk_true();
                 return BR_DONE;
             }
@@ -1025,7 +1042,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
         }
         else {
             SASSERT(s1.length() > s2.length());
-            if (b1 == 0) {
+            if (b1 == nullptr) {
                 result = m().mk_false();
                 return BR_DONE;
             }
@@ -1189,8 +1206,7 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
         e = todo.back();
         todo.pop_back();
         if (m_util.str.is_string(e, s)) {
-            for (unsigned i = s.length(); i > 0; ) {
-                --i;
+            for (unsigned i = 0; i < s.length(); ++i) {
                 seq.push_back(m_util.str.mk_char(s, i));
             }
         }
@@ -1201,14 +1217,13 @@ bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
             seq.push_back(e1);
         }
         else if (m_util.str.is_concat(e, e1, e2)) {
-            todo.push_back(e1);
             todo.push_back(e2);
+            todo.push_back(e1);
         }
         else {
             return false;
         }
     }
-    seq.reverse();
     return true;
 }
 
@@ -1217,7 +1232,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         result = m().mk_false();
         return BR_DONE;
     }
-    if (m_util.re.is_full(b)) {
+    if (m_util.re.is_full_seq(b)) {
         result = m().mk_true();
         return BR_DONE;
     }
@@ -1312,7 +1327,7 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
-    if (m_util.re.is_full(a) && m_util.re.is_full(b)) {
+    if (m_util.re.is_full_seq(a) && m_util.re.is_full_seq(b)) {
         result = a;
         return BR_DONE;
     }
@@ -1352,11 +1367,11 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
         result = a;
         return BR_DONE;
     }
-    if (m_util.re.is_full(a)) {
+    if (m_util.re.is_full_seq(a)) {
         result = a;
         return BR_DONE;
     }
-    if (m_util.re.is_full(b)) {
+    if (m_util.re.is_full_seq(b)) {
         result = b;
         return BR_DONE;
     }
@@ -1382,10 +1397,10 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
         return BR_REWRITE2;
     }
     if (m_util.re.is_empty(a)) {
-        result = m_util.re.mk_full(m().get_sort(a));
+        result = m_util.re.mk_full_seq(m().get_sort(a));
         return BR_DONE;
     }
-    if (m_util.re.is_full(a)) {
+    if (m_util.re.is_full_seq(a)) {
         result = m_util.re.mk_empty(m().get_sort(a));
         return BR_DONE;
     }
@@ -1412,11 +1427,11 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) {
         result = b;
         return BR_DONE;
     }
-    if (m_util.re.is_full(a)) {
+    if (m_util.re.is_full_seq(a)) {
         result = b;
         return BR_DONE;
     }
-    if (m_util.re.is_full(b)) {
+    if (m_util.re.is_full_seq(b)) {
         result = a;
         return BR_DONE;
     }
@@ -1459,12 +1474,16 @@ br_status seq_rewriter::mk_re_loop(unsigned num_args, expr* const* args, expr_re
 */
 br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
     expr* b, *c, *b1, *c1;
-    if (m_util.re.is_star(a) || m_util.re.is_full(a)) {
+    if (m_util.re.is_star(a) || m_util.re.is_full_seq(a)) {
         result = a;
         return BR_DONE;
     }
+    if (m_util.re.is_full_char(a)) {
+        result = m_util.re.mk_full_seq(m().get_sort(a));
+        return BR_DONE;
+    }
     if (m_util.re.is_empty(a)) {
-        sort* seq_sort = 0;
+        sort* seq_sort = nullptr;
         VERIFY(m_util.is_re(a, seq_sort));
         result = m_util.re.mk_to_re(m_util.str.mk_empty(seq_sort));
         return BR_DONE;
@@ -1519,7 +1538,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
         result = a;
         return BR_DONE;
     }
-    if (m_util.re.is_full(a)) {
+    if (m_util.re.is_full_seq(a)) {
         result = a;
         return BR_DONE;
     }
@@ -1542,7 +1561,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
 }
 
 br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
-    sort* s = 0;
+    sort* s = nullptr;
     VERIFY(m_util.is_re(a, s));
     result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(s)), a);
     return BR_REWRITE1;
@@ -1866,7 +1885,7 @@ expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
 
 bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs) {
     zstring s;
-    expr* emp = 0;
+    expr* emp = nullptr;
     for (unsigned i = 0; i < sz; ++i) {
         if (m_util.str.is_unit(es[i])) {
             if (all) return false;

src/ast/rewriter/seq_rewriter.h

@@ -53,7 +53,9 @@ public:
     bool is_range() const { return m_ty == t_range; }
     sort* get_sort() const { return m_sort; }
     expr* get_char() const { SASSERT(is_char()); return m_t; }
-
+    expr* get_pred() const { SASSERT(is_pred()); return m_t; }
+    expr* get_lo() const { SASSERT(is_range()); return m_t; }
+    expr* get_hi() const { SASSERT(is_range()); return m_s; }
 };
 
 class sym_expr_manager {
@@ -87,6 +89,8 @@ public:
     ~re2automaton();
     eautomaton* operator()(expr* e);
     void set_solver(expr_solver* solver);
+    bool has_solver() const { return m_solver; }
+    eautomaton* mk_product(eautomaton *a1, eautomaton *a2);
 };
 
 /**

src/ast/rewriter/th_rewriter.cpp

@@ -187,7 +187,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 if (st != BR_FAILED)
                     return st;
             }
-            if (k == OP_EQ || k == OP_IFF) {
+            if (k == OP_EQ) {
                 SASSERT(num == 2);
                 st = apply_tamagotchi(args[0], args[1], result);
                 if (st != BR_FAILED)
@@ -440,8 +440,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         }
         if (num1 != num2 && num1 != num2 + 1 && num1 != num2 - 1)
             return false;
-        new_t1 = 0;
-        new_t2 = 0;
+        new_t1 = nullptr;
+        new_t2 = nullptr;
         expr_fast_mark1 visited1;
         expr_fast_mark2 visited2;
         for (unsigned i = 0; i < num1; i++) {
@@ -533,7 +533,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         expr * c = args[0];
         expr * t = args[1];
         expr * e = args[2];
-        func_decl * f_prime = 0;
+        func_decl * f_prime = nullptr;
         expr_ref new_t(m()), new_e(m()), common(m());
         bool first;
         TRACE("push_ite", tout << "unifying:\n" << mk_ismt2_pp(t, m()) << "\n" << mk_ismt2_pp(e, m()) << "\n";);
@@ -559,7 +559,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     }
 
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
-        result_pr = 0;
+        result_pr = nullptr;
         br_status st = reduce_app_core(f, num, args, result);
         if (st != BR_DONE && st != BR_FAILED) {
             CTRACE("th_rewriter_step", st != BR_FAILED,
@@ -604,7 +604,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                            expr_ref & result,
                            proof_ref & result_pr) {
         quantifier_ref q1(m());
-        proof * p1 = 0;
+        proof * p1 = nullptr;
         if (is_quantifier(new_body) &&
             to_quantifier(new_body)->is_forall() == old_q->is_forall() &&
             !old_q->has_patterns() &&
@@ -627,7 +627,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                                    std::min(old_q->get_weight(), nested_q->get_weight()),
                                    old_q->get_qid(),
                                    old_q->get_skid(),
-                                   0, 0, 0, 0);
+                                   0, nullptr, 0, nullptr);
 
             SASSERT(is_well_sorted(m(), q1));
 
@@ -657,9 +657,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
 
         TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << mk_ismt2_pp(result, m()) << "\n";);
 
-        result_pr = 0;
+        result_pr = nullptr;
         if (m().proofs_enabled()) {
-            proof * p2 = 0;
+            proof * p2 = nullptr;
             if (q1.get() != result.get())
                 p2 = m().mk_elim_unused_vars(q1, result);
             result_pr = m().mk_transitivity(p1, p2);
@@ -680,7 +680,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_a_util(m),
         m_bv_util(m),
         m_used_dependencies(m),
-        m_subst(0) {
+        m_subst(nullptr) {
         updt_local_params(p);
     }
 
@@ -690,13 +690,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     }
 
     void reset() {
-        m_subst = 0;
+        m_subst = nullptr;
     }
 
     bool get_subst(expr * s, expr * & t, proof * & pr) {
-        if (m_subst == 0)
+        if (m_subst == nullptr)
             return false;
-        expr_dependency * d = 0;
+        expr_dependency * d = nullptr;
         if (m_subst->find(s, t, pr, d)) {
             m_used_dependencies = m().mk_join(m_used_dependencies, d);
             return true;
@@ -798,9 +798,9 @@ expr_dependency * th_rewriter::get_used_dependencies() {
 }
 
 void th_rewriter::reset_used_dependencies() {
-    if (get_used_dependencies() != 0) {
+    if (get_used_dependencies() != nullptr) {
         set_substitution(m_imp->cfg().m_subst); // reset cache preserving subst
-        m_imp->cfg().m_used_dependencies = 0;
+        m_imp->cfg().m_used_dependencies = nullptr;
     }
 }
 

src/ast/rewriter/var_subst.cpp

@@ -24,6 +24,10 @@ Notes:
 #include "ast/for_each_expr.h"
 
 void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, expr_ref & result) {
+    if (is_ground(n)) {
+        result = n;
+        return;
+    }
     SASSERT(is_well_sorted(result.m(), n));
     m_reducer.reset();
     if (m_std_order)
@@ -94,7 +98,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
         }
         else {
             num_removed++;
-            var_mapping.push_back(0);
+            var_mapping.push_back(nullptr);
         }
     }
     // (VAR 0) is in the first position of var_mapping.
@@ -104,7 +108,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
         if (s)
             var_mapping.push_back(m.mk_var(i - num_removed, s));
         else
-            var_mapping.push_back(0);
+            var_mapping.push_back(nullptr);
     }