Reorganizing code base

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/rewriter/arith_rewriter.h

@@ -0,0 +1,183 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    arith_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for arithmetic
+
+Author:
+
+    Leonardo (leonardo) 2011-04-10
+
+Notes:
+
+--*/
+#ifndef _ARITH_REWRITER_H_
+#define _ARITH_REWRITER_H_
+
+#include"poly_rewriter.h"
+#include"arith_decl_plugin.h"
+
+class arith_rewriter_core {
+protected:
+    typedef rational numeral;
+    arith_util  m_util;
+    bool        m_expand_power;
+    bool        m_mul2power;
+    bool        m_expand_tan;
+    
+    ast_manager & m() const { return m_util.get_manager(); }
+    family_id get_fid() const { return m_util.get_family_id(); }
+    
+    bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
+    bool is_numeral(expr * n, numeral & r) const { return m_util.is_numeral(n, r); }
+    bool is_zero(expr * n) const { return m_util.is_zero(n); }
+    bool is_minus_one(expr * n) const { return m_util.is_minus_one(n); }
+    void normalize(numeral & c, sort * s) {}
+    app * mk_numeral(numeral const & r, sort * s) { return m_util.mk_numeral(r, s); }
+    decl_kind add_decl_kind() const { return OP_ADD; }
+    decl_kind mul_decl_kind() const { return OP_MUL; }
+    bool use_power() const { return m_mul2power && !m_expand_power; }
+    decl_kind power_decl_kind() const { return OP_POWER; }
+public:
+    arith_rewriter_core(ast_manager & m):m_util(m) {}
+};
+
+class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
+    bool m_arith_lhs;
+    bool m_gcd_rounding;
+    bool m_eq2ineq;
+    bool m_elim_to_real;
+    bool m_push_to_real;
+    bool m_anum_simp;
+    bool m_elim_rem;
+    unsigned m_max_degree;
+
+    void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts);
+    enum const_treatment { CT_FLOOR, CT_CEIL, CT_FALSE };
+    bool div_polynomial(expr * t, numeral const & g, const_treatment ct, expr_ref & result);
+    enum op_kind { LE, GE, EQ };
+    static op_kind inv(op_kind k) { return k == LE ? GE : (k == GE ? LE : EQ); }
+    bool is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
+    br_status mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
+
+    bool elim_to_real_var(expr * var, expr_ref & new_var);
+    bool elim_to_real_mon(expr * monomial, expr_ref & new_monomial);
+    bool elim_to_real_pol(expr * p, expr_ref & new_p);
+    bool elim_to_real(expr * arg1, expr * arg2, expr_ref & new_arg1, expr_ref & new_arg2);
+
+    void updt_local_params(params_ref const & p);
+
+    bool is_anum_simp_target(unsigned num_args, expr * const * args);
+
+    br_status mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result);
+    
+    bool is_reduce_power_target(expr * arg, bool is_eq);
+    expr * reduce_power(expr * arg, bool is_eq);
+    br_status reduce_power(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
+
+    bool is_pi_multiple(expr * t, rational & k);
+    bool is_pi_offset(expr * t, rational & k, expr * & m);
+    bool is_2_pi_integer(expr * t);
+    bool is_2_pi_integer_offset(expr * t, expr * & m);
+    bool is_pi_integer(expr * t);
+    bool is_pi_integer_offset(expr * t, expr * & m);
+    expr * mk_sin_value(rational const & k);
+    app * mk_sqrt(rational const & k);
+
+public:
+    arith_rewriter(ast_manager & m, params_ref const & p = params_ref()):
+        poly_rewriter<arith_rewriter_core>(m, p) {
+        updt_local_params(p);
+    }
+
+    void updt_params(params_ref const & p);
+
+    static void get_param_descrs(param_descrs & r);
+
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+        if (mk_app_core(f, num_args, args, result) == BR_FAILED)
+            result = m().mk_app(f, num_args, args);
+    }
+
+    br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_le_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_lt_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_ge_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_gt_core(expr * arg1, expr * arg2, expr_ref & result);
+
+    br_status mk_add_core(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result);
+
+    void mk_eq(expr * arg1, expr * arg2, expr_ref & result) {
+        if (mk_eq_core(arg1, arg2, result) == BR_FAILED)
+            result = m_util.mk_le(arg1, arg2);
+    }
+    void mk_le(expr * arg1, expr * arg2, expr_ref & result) {
+        if (mk_le_core(arg1, arg2, result) == BR_FAILED)
+            result = m_util.mk_le(arg1, arg2);
+    }
+    void mk_lt(expr * arg1, expr * arg2, expr_ref & result) { mk_lt_core(arg1, arg2, result); }
+    void mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
+        if (mk_ge_core(arg1, arg2, result) == BR_FAILED)
+            result = m_util.mk_ge(arg1, arg2);
+    }
+    void mk_gt(expr * arg1, expr * arg2, expr_ref & result) { mk_gt_core(arg1, arg2, result); }
+
+    br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_rem_core(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result);
+    void mk_div(expr * arg1, expr * arg2, expr_ref & result) {
+        if (mk_div_core(arg1, arg2, result) == BR_FAILED)
+            result = m().mk_app(get_fid(), OP_DIV, arg1, arg2);
+    }
+    void mk_idiv(expr * arg1, expr * arg2, expr_ref & result) {
+        if (mk_idiv_core(arg1, arg2, result) == BR_FAILED)
+            result = m().mk_app(get_fid(), OP_IDIV, arg1, arg2);
+    }
+    void mk_mod(expr * arg1, expr * arg2, expr_ref & result) {
+        if (mk_mod_core(arg1, arg2, result) == BR_FAILED)
+            result = m().mk_app(get_fid(), OP_MOD, arg1, arg2);
+    }
+    void mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
+        if (mk_rem_core(arg1, arg2, result) == BR_FAILED)
+            result = m().mk_app(get_fid(), OP_REM, arg1, arg2);
+    }
+    
+    br_status mk_to_int_core(expr * arg, expr_ref & result);
+    br_status mk_to_real_core(expr * arg, expr_ref & result);
+    void mk_to_int(expr * arg, expr_ref & result) { 
+        if (mk_to_int_core(arg, result) == BR_FAILED)
+            result = m().mk_app(get_fid(), OP_TO_INT, 1, &arg); 
+    }
+    void mk_to_real(expr * arg, expr_ref & result) { 
+        if (mk_to_real_core(arg, result) == BR_FAILED)  
+            result = m().mk_app(get_fid(), OP_TO_REAL, 1, &arg); 
+    }
+    br_status mk_is_int(expr * arg, expr_ref & result);
+
+    void set_cancel(bool f);
+
+    br_status mk_sin_core(expr * arg, expr_ref & result);
+    br_status mk_cos_core(expr * arg, expr_ref & result);
+    br_status mk_tan_core(expr * arg, expr_ref & result);
+
+    br_status mk_asin_core(expr * arg, expr_ref & result);
+    br_status mk_acos_core(expr * arg, expr_ref & result);
+    br_status mk_atan_core(expr * arg, expr_ref & result);
+
+    br_status mk_sinh_core(expr * arg, expr_ref & result);
+    br_status mk_cosh_core(expr * arg, expr_ref & result);
+    br_status mk_tanh_core(expr * arg, expr_ref & result);
+};
+
+#endif

src/rewriter/array_rewriter.cpp

@@ -0,0 +1,359 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    array_rewriter.cpp
+
+Abstract:
+
+    Basic rewriting rules for Arrays.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-06
+
+Notes:
+
+--*/
+#include"array_rewriter.h"
+#include"ast_lt.h"
+#include"ast_pp.h"
+
+void array_rewriter::updt_params(params_ref const & p) {
+    m_sort_store = p.get_bool(":sort-store", false);
+    m_expand_select_store = p.get_bool(":expand-select-store", false);
+}
+
+void array_rewriter::get_param_descrs(param_descrs & r) {
+    r.insert(":expand-select-store", CPK_BOOL, "(default: false) replace a (select (store ...) ...) term by an if-then-else term.");
+    r.insert(":sort-store", CPK_BOOL, "(default: false) sort nested stores when the indices are known to be different.");
+}
+
+br_status array_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(f->get_family_id() == get_fid());
+    TRACE("array_rewriter", tout << mk_pp(f, m()) << "\n";
+          for (unsigned i = 0; i < num_args; ++i) {
+              tout << mk_pp(args[i], m()) << "\n";
+          });
+    switch (f->get_decl_kind()) {
+    case OP_SELECT:
+        return mk_select_core(num_args, args, result);
+    case OP_STORE:
+        return mk_store_core(num_args, args, result);
+    case OP_ARRAY_MAP:
+        SASSERT(f->get_num_parameters() == 1);
+        SASSERT(f->get_parameter(0).is_ast());
+        SASSERT(is_func_decl(f->get_parameter(0).get_ast()));
+        return mk_map_core(to_func_decl(f->get_parameter(0).get_ast()), num_args, args, result);
+    case OP_SET_UNION:
+        return mk_set_union(num_args, args, result);
+    case OP_SET_INTERSECT:
+        return mk_set_intersect(num_args, args, result);
+    case OP_SET_SUBSET: 
+        SASSERT(num_args == 2);
+        return mk_set_subset(args[0], args[1], result);
+    case OP_SET_COMPLEMENT:
+        SASSERT(num_args == 1);
+        return mk_set_complement(args[0], result);
+    case OP_SET_DIFFERENCE:
+        SASSERT(num_args == 2);
+        return mk_set_difference(args[0], args[1], result);
+    default:
+        return BR_FAILED;
+    }
+}
+
+// l_true  -- all equal
+// l_false -- at least one disequal
+// l_undef -- don't know
+template<bool CHECK_DISEQ>
+lbool array_rewriter::compare_args(unsigned num_args, expr * const * args1, expr * const * args2) {
+    for (unsigned i = 0; i < num_args; i++) {
+        if (args1[i] == args2[i])
+            continue;
+        if (CHECK_DISEQ && m().are_distinct(args1[i], args2[i]))
+            return l_false;
+        return l_undef;
+    }
+    return l_true;
+}
+
+br_status array_rewriter::mk_store_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args >= 3);
+
+    if (m_util.is_store(args[0])) {
+        lbool r = m_sort_store ? 
+            compare_args<true>(num_args - 2, args + 1, to_app(args[0])->get_args() + 1) :
+            compare_args<false>(num_args - 2, args + 1, to_app(args[0])->get_args() + 1);
+        switch (r) {
+        case l_true: {
+            //
+            // store(store(a,i,v),i,w) --> store(a,i,w)
+            // 
+            ptr_buffer<expr> new_args;
+            new_args.push_back(to_app(args[0])->get_arg(0));
+            new_args.append(num_args-1, args+1);
+            SASSERT(new_args.size() == num_args);
+            result = m().mk_app(get_fid(), OP_STORE, num_args, new_args.c_ptr());
+            return BR_DONE;
+        }
+        case l_false:
+            SASSERT(m_sort_store);
+            // 
+            // store(store(a,i,v),j,w) -> store(store(a,j,w),i,v)
+            // if i, j are different, lt(i,j)
+            // 
+            if (lex_lt(num_args-2, args+1, to_app(args[0])->get_args() + 1)) {
+                ptr_buffer<expr> new_args;
+                new_args.push_back(to_app(args[0])->get_arg(0));
+                new_args.append(num_args-1, args+1);
+                expr * nested_store = m().mk_app(get_fid(), OP_STORE, num_args, new_args.c_ptr());
+                new_args.reset();
+                new_args.push_back(nested_store);
+                new_args.append(num_args - 1, to_app(args[0])->get_args() + 1);
+                result = m().mk_app(get_fid(), OP_STORE, num_args, new_args.c_ptr());
+                return BR_REWRITE2;
+            }
+            break;
+        case l_undef:
+            break;
+        }
+    }
+        
+    //
+    // store(const(v),i,v) --> const(v)
+    //
+    if (m_util.is_const(args[0]) &&
+        to_app(args[0])->get_arg(0) == args[num_args-1]) {
+        result = args[0];
+        return BR_DONE;
+    }
+
+    expr * v = args[num_args-1];
+
+    // 
+    // store(a, i, select(a, i)) --> a
+    //
+    if (m_util.is_select(v) && 
+        compare_args<false>(num_args-1, args, to_app(v)->get_args())) {
+        result = args[0];
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+        
+br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args >= 2);
+    if (m_util.is_store(args[0])) {
+        SASSERT(to_app(args[0])->get_num_args() == num_args+1);
+        switch (compare_args<true>(num_args - 1, args+1, to_app(args[0])->get_args()+1)) {
+        case l_true:
+            // select(store(a, I, v), I) --> v
+            result = to_app(args[0])->get_arg(num_args);
+            return BR_DONE;
+        case l_false: {
+            // select(store(a, I, v), J) --> select(a, J) if I != J
+            ptr_buffer<expr> new_args;
+            new_args.push_back(to_app(args[0])->get_arg(0));
+            new_args.append(num_args-1, args+1);
+            result = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.c_ptr());
+            return BR_REWRITE1;
+        }
+        default:
+            if (m_expand_select_store) {
+                // select(store(a, I, v), J) --> ite(I=J, v, select(a, J))
+                ptr_buffer<expr> new_args;
+                new_args.push_back(to_app(args[0])->get_arg(0));
+                new_args.append(num_args-1, args+1);
+                expr * sel_a_j = m().mk_app(get_fid(), OP_SELECT, num_args, new_args.c_ptr());
+                expr * v       = to_app(args[0])->get_arg(num_args);
+                ptr_buffer<expr> eqs;
+                unsigned num_indices = num_args-1;
+                for (unsigned i = 0; i < num_indices; i++) {
+                    eqs.push_back(m().mk_eq(to_app(args[0])->get_arg(i+1), args[i+1]));
+                }
+                if (num_indices == 1) {
+                    result = m().mk_ite(eqs[0], v, sel_a_j);
+                    return BR_REWRITE2;
+                }
+                else {
+                    result = m().mk_ite(m().mk_and(eqs.size(), eqs.c_ptr()), v, sel_a_j);
+                    return BR_REWRITE3;
+                }
+            }
+            return BR_FAILED;
+        }
+    }
+
+    if (m_util.is_const(args[0])) {
+        // select(const(v), I) --> v
+        result = to_app(args[0])->get_arg(0);
+        return BR_DONE;
+    }
+
+    if (m_util.is_as_array(args[0])) {
+        // select(as-array[f], I) --> f(I)
+        func_decl * f = m_util.get_as_array_func_decl(to_app(args[0]));
+        result = m().mk_app(f, num_args - 1, args + 1);
+        return BR_REWRITE1;
+    }
+    
+    return BR_FAILED;
+}
+
+br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args >= 0);
+    bool is_store0 = m_util.is_store(args[0]);
+    bool is_const0 = m_util.is_const(args[0]);
+    if (num_args == 1) {
+        //
+        // map_f (store a j v) = (store (map_f a) j (f v)) 
+        //
+        if (is_store0) {
+            app * store_expr = to_app(args[0]);
+            unsigned num_args = store_expr->get_num_args();
+            SASSERT(num_args >= 3);
+            expr * a = store_expr->get_arg(0);
+            expr * v = store_expr->get_arg(num_args-1);
+            
+            ptr_buffer<expr> new_args;
+            
+            new_args.push_back(m_util.mk_map(f, 1, &a)); // (map_f a)
+            new_args.append(num_args - 2, store_expr->get_args() + 1); // j
+            new_args.push_back(m().mk_app(f, v));   // (f v)
+            
+            result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr());
+            return BR_REWRITE2;
+        }
+        
+        //
+        // map_f (const v) = (const (f v))
+        //
+        if (is_const0) {
+            expr * fv = m().mk_app(f, to_app(args[0])->get_arg(0));
+            result = m_util.mk_const_array(m().get_sort(args[0]), fv);
+            return BR_REWRITE2;
+        }
+        return BR_FAILED;
+    }
+
+    SASSERT(num_args > 1);
+    
+    if (is_store0) {
+        unsigned num_indices = to_app(args[0])->get_num_args() - 2;
+        unsigned i;
+        for (i = 1; i < num_args; i++) {
+            if (!m_util.is_store(args[i]))
+                break;
+            unsigned j;
+            for (j = 1; j < num_indices+1; j++) {
+                if (to_app(args[0])->get_arg(j) != to_app(args[i])->get_arg(j))
+                    break;
+            }
+            if (j < num_indices+1)
+                break;
+        }
+        //
+        // map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n))
+        //
+        if (i == num_args) {
+            ptr_buffer<expr> arrays;
+            ptr_buffer<expr> values;
+            for (unsigned i = 0; i < num_args; i++) {
+                arrays.push_back(to_app(args[i])->get_arg(0));
+                values.push_back(to_app(args[i])->get_arg(num_indices+1));
+            }
+            ptr_buffer<expr> new_args;
+            new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr()));
+            new_args.append(num_indices, to_app(args[0])->get_args() + 1);
+            new_args.push_back(m().mk_app(f, values.size(), values.c_ptr()));
+            result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr());
+            return BR_REWRITE2;
+        }
+        return BR_FAILED;
+    }
+
+    if (is_const0) {
+        unsigned i;
+        for (i = 1; i < num_args; i++) {
+            if (!m_util.is_const(args[i]))
+                break;
+        }
+        if (i == num_args) {
+            //
+            // map_f (const v_1) ... (const v_n) = (const (f v_1 ... v_n))
+            //
+            ptr_buffer<expr> values;
+            for (unsigned i = 0; i < num_args; i++) {
+                values.push_back(to_app(args[i])->get_arg(0));
+            }
+            
+            expr * fv = m().mk_app(f, values.size(), values.c_ptr());
+            parameter p(m().get_sort(args[0]));
+            result = m().mk_app(get_fid(), OP_CONST_ARRAY, 1, &p, 1, &fv);
+            return BR_REWRITE2;
+        }
+        return BR_FAILED;
+    }
+
+    return BR_FAILED;
+}
+
+void array_rewriter::mk_store(unsigned num_args, expr * const * args, expr_ref & result) {
+    if (mk_store_core(num_args, args, result) == BR_FAILED)
+        result = m().mk_app(get_fid(), OP_STORE, num_args, args);
+}
+        
+void array_rewriter::mk_select(unsigned num_args, expr * const * args, expr_ref & result) {
+    if (mk_select_core(num_args, args, result) == BR_FAILED)
+        result = m().mk_app(get_fid(), OP_SELECT, num_args, args);
+}
+
+void array_rewriter::mk_map(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    if (mk_map_core(f, num_args, args, result) == BR_FAILED)
+        result = m_util.mk_map(f, num_args, args);
+}
+
+br_status array_rewriter::mk_set_union(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args > 0);
+    if (num_args == 1) {
+        result = args[0];
+        return BR_DONE;
+    }
+    SASSERT(num_args >= 2);
+    br_status r = unsigned2br_status(num_args - 2);
+    result = m_util.mk_map(m().mk_or_decl(), num_args, args);
+    return r;
+}
+
+br_status array_rewriter::mk_set_intersect(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args > 0);
+    if (num_args == 1) {
+        result = args[0];
+        return BR_DONE;
+    }
+    SASSERT(num_args >= 2);
+    br_status r = unsigned2br_status(num_args - 2);
+    result = m_util.mk_map(m().mk_and_decl(), num_args, args);
+    return r;
+}
+
+
+br_status array_rewriter::mk_set_complement(expr * arg, expr_ref & result) {
+    return mk_map_core(m().mk_not_decl(), 1, &arg, result);
+}
+
+br_status array_rewriter::mk_set_difference(expr * arg1, expr * arg2, expr_ref & result) {
+    expr * args[2] = { arg1, m_util.mk_map(m().mk_not_decl(), 1, &arg2) };
+    result = m_util.mk_map(m().mk_and_decl(), 2, args);
+    return BR_REWRITE2;
+}
+
+br_status array_rewriter::mk_set_subset(expr * arg1, expr * arg2, expr_ref & result) {
+    mk_set_difference(arg1, arg2, result);
+    result = m().mk_eq(result.get(), m_util.mk_empty_set(m().get_sort(arg1)));
+    return BR_REWRITE3;
+}
+

src/rewriter/array_rewriter.h

@@ -0,0 +1,65 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    array_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for Arrays.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-06
+
+Notes:
+
+--*/
+#ifndef _ARRAY_REWRITER_H_
+#define _ARRAY_REWRITER_H_
+
+#include"array_decl_plugin.h"
+#include"rewriter_types.h"
+#include"lbool.h"
+#include"params.h"
+
+/**
+   \brief Cheap rewrite rules for Arrays
+*/
+class array_rewriter {
+    array_util    m_util;
+    bool          m_sort_store;
+    bool          m_expand_select_store;
+    template<bool CHECK_DISEQ>
+    lbool compare_args(unsigned num_args, expr * const * args1, expr * const * args2);
+public:    
+    array_rewriter(ast_manager & m, params_ref const & p = params_ref()):
+        m_util(m) {
+        updt_params(p);
+    }
+    ast_manager & m() const { return m_util.get_manager(); }
+    family_id get_fid() const { return m_util.get_family_id(); }
+
+    void updt_params(params_ref const & p);
+    static void get_param_descrs(param_descrs & r);
+
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+
+    br_status mk_store_core(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_select_core(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+
+    void mk_store(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_select(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_map(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+
+    // The following methods never return BR_FAILED
+    br_status mk_set_union(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_set_intersect(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_set_complement(expr * arg, expr_ref & result);
+    br_status mk_set_difference(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_set_subset(expr * arg1, expr * arg2, expr_ref & result);
+};
+
+#endif

src/rewriter/bool_rewriter.cpp

@@ -0,0 +1,989 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    bool_rewriter.h
+
+Abstract:
+
+    Basic rewrites for Boolean operators.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-04
+
+Notes:
+
+--*/
+#include"bool_rewriter.h"
+#include"rewriter_def.h"
+
+void bool_rewriter::updt_params(params_ref const & p) {
+    m_flat                 = p.get_bool(":flat", true);
+    m_elim_and             = p.get_bool(":elim-and", false);
+    m_local_ctx            = p.get_bool(":local-ctx", false);
+    m_local_ctx_limit      = p.get_uint(":local-ctx-limit", UINT_MAX);
+    m_blast_distinct       = p.get_bool(":blast-distinct", false); 
+    m_ite_extra_rules      = p.get_bool(":ite-extra-rules", false);
+}
+
+void bool_rewriter::get_param_descrs(param_descrs & r) {
+    r.insert(":ite-extra-rules", CPK_BOOL, "(default: false) extra ite simplifications, these additional simplifications may reduce size locally but increase globally.");
+    r.insert(":flat", CPK_BOOL, "(default: true) create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor.");
+    r.insert(":elim-and", CPK_BOOL, "(default: false) conjunctions are rewritten using negation and disjunctions.");
+    r.insert(":local-ctx", CPK_BOOL, "(default: false) perform local (i.e., cheap) context simplifications.");
+    r.insert(":local-ctx-limit", CPK_UINT, "(default: inf) limit for applying local context simplifier.");
+    r.insert(":blast-distinct", CPK_BOOL, "(default: false) expand a distinct predicate into a quadratic number of disequalities."); 
+}
+
+br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    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:
+        return mk_distinct_core(num_args, args, result);
+    case OP_AND:
+        return mk_and_core(num_args, args, result);
+    case OP_OR:
+        return mk_or_core(num_args, args, result);
+    case OP_NOT:
+        SASSERT(num_args == 1);
+        return mk_not_core(args[0], result);
+    case OP_ITE:
+        SASSERT(num_args == 3);
+        return mk_ite_core(args[0], args[1], args[2], result);
+    case OP_IMPLIES:
+        SASSERT(num_args == 2);
+        mk_implies(args[0], args[1], result);
+        return BR_DONE;
+    case OP_XOR:
+        SASSERT(num_args == 2);
+        mk_xor(args[0], args[1], result);
+        return BR_DONE;
+    default:
+        return BR_FAILED;
+    }
+}
+
+void bool_rewriter::mk_and_as_or(unsigned num_args, expr * const * args, expr_ref & result) {
+    expr_ref_buffer new_args(m());
+    for (unsigned i = 0; i < num_args; i++) {
+        expr_ref tmp(m());
+        mk_not(args[i], tmp);
+        new_args.push_back(tmp);
+    }
+    expr_ref tmp(m());
+    mk_or(new_args.size(), new_args.c_ptr(), tmp);
+    mk_not(tmp, result);
+}
+
+br_status bool_rewriter::mk_nflat_and_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    bool s = false;
+    ptr_buffer<expr> buffer;
+    expr_fast_mark1 neg_lits;
+    expr_fast_mark2 pos_lits;
+    
+    for (unsigned i = 0; i < num_args; i++) {
+        expr * arg  = args[i];
+        if (m().is_true(arg)) {
+            s = true;
+            continue;
+        }
+        if (m().is_false(arg)) {
+            result = m().mk_false();
+            return BR_DONE;
+        }
+        if (m().is_not(arg)) {
+            expr * atom = to_app(arg)->get_arg(0);
+            if (neg_lits.is_marked(atom)) {
+                s = true;
+                continue;
+            }
+            if (pos_lits.is_marked(atom)) {
+                result = m().mk_false();
+                return BR_DONE;
+            }
+            neg_lits.mark(atom);
+        }
+        else {
+            if (pos_lits.is_marked(arg)) {
+                s = true;
+                continue;
+            }
+            if (neg_lits.is_marked(arg)) {
+                result = m().mk_false();
+                return BR_DONE;
+            }
+            pos_lits.mark(arg);
+        }
+        buffer.push_back(arg);
+    }
+    
+    unsigned sz = buffer.size();
+    
+    switch(sz) {
+    case 0:
+        result = m().mk_true();
+        return BR_DONE;
+    case 1:
+        result = buffer.back();
+        return BR_DONE;
+    default:
+        if (s) {
+            result = m().mk_and(sz, buffer.c_ptr());
+            return BR_DONE;
+        }
+        return BR_FAILED;
+    }
+}
+
+br_status bool_rewriter::mk_flat_and_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    unsigned i;
+    for (i = 0; i < num_args; i++) {
+        if (m().is_and(args[i]))
+            break;
+    }
+    if (i < num_args) {
+        // has nested ANDs
+        ptr_buffer<expr> flat_args;
+        flat_args.append(i, args);
+        for (; i < num_args; i++) {
+            expr * arg = args[i];
+            // Remark: all rewrites are depth 1.
+            if (m().is_and(arg)) {
+                unsigned num = to_app(arg)->get_num_args();
+                for (unsigned j = 0; j < num; j++)
+                    flat_args.push_back(to_app(arg)->get_arg(j));
+            }
+            else {
+                flat_args.push_back(arg);
+            }
+        }
+        if (mk_nflat_and_core(flat_args.size(), flat_args.c_ptr(), result) == BR_FAILED)
+            result = m().mk_and(flat_args.size(), flat_args.c_ptr());
+        return BR_DONE;
+    }
+    return mk_nflat_and_core(num_args, args, result);
+}
+
+br_status bool_rewriter::mk_nflat_or_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    bool s = false;
+    ptr_buffer<expr> buffer;
+    expr_fast_mark1 neg_lits;
+    expr_fast_mark2 pos_lits;
+    for (unsigned i = 0; i < num_args; i++) {
+        expr * arg  = args[i];
+        if (m().is_true(arg)) {
+            result = m().mk_true();
+            return BR_DONE;
+        }
+        if (m().is_false(arg)) {
+            s = true;
+            continue;
+        }
+        if (m().is_not(arg)) {
+            expr * atom = to_app(arg)->get_arg(0);
+            if (neg_lits.is_marked(atom)) {
+                s = true;
+                continue;
+            }
+            if (pos_lits.is_marked(atom)) {
+                result = m().mk_true();
+                return BR_DONE;
+            }
+            neg_lits.mark(atom);
+        }
+        else {
+            if (pos_lits.is_marked(arg)) {
+                s = true;
+                continue;
+            }
+            if (neg_lits.is_marked(arg)) {
+                result = m().mk_true();
+                return BR_DONE;
+            }
+            pos_lits.mark(arg);
+        }
+        buffer.push_back(arg);
+    }
+    
+    unsigned sz = buffer.size();
+    
+    switch(sz) {
+    case 0:
+        result = m().mk_false();
+        return BR_DONE;
+    case 1:
+        result = buffer.back();
+        return BR_DONE;
+    default:
+        if (m_local_ctx && m_local_ctx_cost <= m_local_ctx_limit) {
+            neg_lits.reset();
+            pos_lits.reset();
+            if (local_ctx_simp(sz, buffer.c_ptr(), result)) 
+                return BR_DONE;
+        }
+        if (s) {
+            result = m().mk_or(sz, buffer.c_ptr());
+            return BR_DONE;
+        }
+        return BR_FAILED;
+    }
+}
+
+
+br_status bool_rewriter::mk_flat_or_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    unsigned i;
+    for (i = 0; i < num_args; i++) {
+        if (m().is_or(args[i]))
+            break;
+    }
+    if (i < num_args) {
+        // has nested ORs
+        ptr_buffer<expr> flat_args;
+        flat_args.append(i, args);
+        for (; i < num_args; i++) {
+            expr * arg = args[i];
+            // Remark: all rewrites are depth 1.
+            if (m().is_or(arg)) {
+                unsigned num = to_app(arg)->get_num_args();
+                for (unsigned j = 0; j < num; j++)
+                    flat_args.push_back(to_app(arg)->get_arg(j));
+            }
+            else {
+                flat_args.push_back(arg);
+            }
+        }
+        if (mk_nflat_or_core(flat_args.size(), flat_args.c_ptr(), result) == BR_FAILED)
+            result = m().mk_or(flat_args.size(), flat_args.c_ptr());
+        return BR_DONE;
+    }
+    return mk_nflat_or_core(num_args, args, result);
+}
+
+expr * bool_rewriter::mk_or_app(unsigned num_args, expr * const * args) {
+    switch(num_args) {
+    case 0: return m().mk_false();
+    case 1: return args[0];
+    default: return m().mk_or(num_args, args);
+    }
+}
+
+/**
+   \brief Auxiliary method for local_ctx_simp.
+   
+   Replace args[i] by true if marked in neg_lits.
+   Replace args[i] by false if marked in pos_lits.
+*/
+bool bool_rewriter::simp_nested_not_or(unsigned num_args, expr * const * args, 
+                                       expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result) {
+    ptr_buffer<expr> new_args;
+    bool simp = false;
+    m_local_ctx_cost += num_args;
+    for (unsigned i = 0; i < num_args; i++) {
+        expr * arg = args[i];
+        if (neg_lits.is_marked(arg)) {
+            result = m().mk_false();
+            return true;
+        }
+        if (pos_lits.is_marked(arg)) {
+            simp = true;
+            continue;
+        }
+        if (m().is_not(arg)) {
+            expr * atom = to_app(arg)->get_arg(0);
+            if (neg_lits.is_marked(atom)) {
+                simp = true;
+                continue;
+            }
+            if (pos_lits.is_marked(atom)) {
+                result = m().mk_false();
+                return true;
+            }
+        }
+        new_args.push_back(arg);
+    }
+    if (simp) {
+        switch(new_args.size()) {
+        case 0: 
+            result = m().mk_true(); 
+            return true;
+        case 1: 
+            mk_not(new_args[0], result); 
+            return true;
+        default: 
+            result = m().mk_not(m().mk_or(new_args.size(), new_args.c_ptr()));
+            return true;
+        }
+    }
+    return false;
+}
+
+
+expr * bool_rewriter::simp_arg(expr * arg, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, bool & modified) {
+    if (m().is_not(arg)) {
+        expr * atom = to_app(arg)->get_arg(0);
+        if (neg_lits.is_marked(atom)) {
+            modified = true;
+            return m().mk_false();
+        }
+        if (pos_lits.is_marked(atom)) {
+            modified = true;
+            return m().mk_true();
+        }
+        return arg;
+    }
+    else {
+        if (neg_lits.is_marked(arg)) {
+            modified = true;
+            return m().mk_true();
+        }
+        if (pos_lits.is_marked(arg)) {
+            modified = true;
+            return m().mk_false();
+        }
+        return arg;
+    }
+}
+
+/**
+   \brief Simpler version of mk_ite, that will not invoke mk_or/mk_and.
+   It is used byt local_ctx_simp to prevent a recursive call to local_ctx_simp.
+   See comment at simp_nested_eq_ite.
+*/
+void bool_rewriter::mk_nested_ite(expr * c, expr * t, expr * e, expr_ref & result) {
+    if (m().is_true(c)) {
+        result = t;
+        return;
+    }
+    
+    if (m().is_false(c)) {
+        result = e;
+        return;
+    }
+
+    if (t == e) {
+        result = t;
+        return;
+    }
+    
+    if (m().is_bool(t)) {
+        if (m().is_true(t)) {
+            if (m().is_false(e)) {
+                result = c;
+                return;
+            }
+            result = m().mk_or(c, e);
+            return;
+        }
+        if (m().is_false(t)) {
+            if (m().is_true(e)) {
+                mk_not(c, result);
+                return;
+            }
+            expr_ref tmp(m());
+            mk_not(e, tmp); 
+            result = m().mk_not(m().mk_or(c, tmp));
+            return;
+        }
+        if (m().is_true(e)) {
+            expr_ref tmp(m());
+            mk_not(c, tmp); 
+            result = m().mk_or(tmp, t);
+            return;
+        }
+        if (m().is_false(e) || c == e) {
+            expr_ref tmp1(m());
+            expr_ref tmp2(m());
+            mk_not(c, tmp1);
+            mk_not(t, tmp2);
+            result = m().mk_not(m().mk_or(tmp1, tmp2));
+            return;
+        }
+        if (c == t) {
+            result = m().mk_or(c, e);
+            return;
+        }
+        if (m().is_complement_core(t, e)) { // t = not(e) 
+            mk_eq(c, t, result);
+            return;
+        }
+        if (m().is_complement_core(e, t)) { // e = not(t)
+            mk_eq(c, t, result);
+            return;
+        }
+    }
+    result = m().mk_ite(c, t, e);
+}
+
+bool bool_rewriter::simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result) {
+    bool neg = false;
+    m_local_ctx_cost += 3;
+    if (m().is_not(t)) {
+        neg = true;
+        t = to_app(t)->get_arg(0);
+    }
+    if (m().is_iff(t) || 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);
+        if (!modified)
+            return false;
+        mk_eq(new_lhs, new_rhs, result);
+        if (neg)
+            mk_not(result, result);
+        return true;
+    }
+    if (m().is_ite(t)) {
+        bool modified = false;
+        expr * new_c = simp_arg(to_app(t)->get_arg(0), neg_lits, pos_lits, modified);
+        expr * new_t = simp_arg(to_app(t)->get_arg(1), neg_lits, pos_lits, modified);
+        expr * new_e = simp_arg(to_app(t)->get_arg(2), neg_lits, pos_lits, modified);
+        if (!modified)
+            return false;
+        // It is not safe to invoke mk_ite here, since it can recursively call 
+        // local_ctx_simp by 
+        //     - transforming the ITE into an OR
+        //     - and invoked mk_or, that will invoke local_ctx_simp
+        // mk_ite(new_c, new_t, new_e, result);
+        mk_nested_ite(new_c, new_t, new_e, result);
+        if (neg)
+            mk_not(result, result);
+        return true;
+    }
+    return false;
+}
+
+/**
+   \brief Apply local context simplification at (OR args[0] ... args[num_args-1])
+   Basic idea:
+   - Replace args[i] by false in the other arguments
+   - If args[i] is of the form (not t), then replace t by true in the other arguments.
+   To make sure the simplification is efficient we bound the depth.
+*/
+bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_ref & result) {
+    expr_ref_vector old_args(m());
+    expr_ref_vector new_args(m());
+    expr_ref        new_arg(m());
+    expr_fast_mark1 neg_lits;
+    expr_fast_mark2 pos_lits;
+    bool simp     = false;
+    bool modified = false;
+    bool forward  = true;
+    unsigned rounds = 0;
+
+    while (true) {
+        rounds++;
+#if 0
+        if (rounds > 10)
+            verbose_stream() << "rounds: " << rounds << "\n";
+#endif
+
+#define PUSH_NEW_ARG(ARG) {                     \
+    new_args.push_back(ARG);                    \
+    if (m().is_not(ARG))                        \
+        neg_lits.mark(to_app(ARG)->get_arg(0)); \
+    else                                        \
+        pos_lits.mark(ARG);                     \
+}
+
+#define PROCESS_ARG()                                                                           \
+        {                                                                                       \
+            expr * arg = args[i];                                                               \
+            if (m().is_not(arg) && m().is_or(to_app(arg)->get_arg(0)) &&                        \
+                simp_nested_not_or(to_app(to_app(arg)->get_arg(0))->get_num_args(),             \
+                                   to_app(to_app(arg)->get_arg(0))->get_args(),                 \
+                                   neg_lits,                                                    \
+                                   pos_lits,                                                    \
+                                   new_arg)) {                                                  \
+                modified = true; simp = true;                                                   \
+                arg = new_arg;                                                                  \
+            }                                                                                   \
+            if (simp_nested_eq_ite(arg, neg_lits, pos_lits, new_arg)) {                         \
+                modified = true; simp = true;                                                   \
+                 arg = new_arg;                                                                 \
+            }                                                                                   \
+            if (m().is_false(arg))                                                              \
+                continue;                                                                       \
+            if (m().is_true(arg)) {                                                             \
+                result = arg;                                                                   \
+                return true;                                                                    \
+            }                                                                                   \
+            if (m_flat && m().is_or(arg)) {                                                     \
+                unsigned sz = to_app(arg)->get_num_args();                                      \
+                for (unsigned j = 0; j < sz; j++) {                                             \
+                    expr * arg_arg = to_app(arg)->get_arg(j);                                   \
+                    PUSH_NEW_ARG(arg_arg);                                                      \
+                }                                                                               \
+            }                                                                                   \
+            else {                                                                              \
+                PUSH_NEW_ARG(arg);                                                              \
+            }                                                                                   \
+        }
+        
+        m_local_ctx_cost += 2*num_args;
+#if 0
+        static unsigned counter = 0;
+        counter++;
+        if (counter % 10000 == 0)
+            verbose_stream() << "local-ctx-cost: " << m_local_ctx_cost << "\n";
+#endif
+
+        if (forward) {
+            for (unsigned i = 0; i < num_args; i++) {
+                PROCESS_ARG();
+            }
+            forward = false;
+        }
+        else {
+            unsigned i = num_args;
+            while (i > 0) {
+                --i;
+                PROCESS_ARG();
+            }
+            if (!modified) {
+                if (simp) {
+                    result = mk_or_app(num_args, args);
+                    return true;
+                }
+                return false; // didn't simplify
+            }
+            // preserve the original order...
+            std::reverse(new_args.c_ptr(), new_args.c_ptr() + new_args.size());
+            modified = false;
+            forward  = true;
+        }
+        pos_lits.reset();
+        neg_lits.reset();
+        old_args.reset();
+        old_args.swap(new_args);
+        SASSERT(new_args.empty());
+        args     = old_args.c_ptr();
+        num_args = old_args.size();
+    }
+}
+
+/**
+   \brief Apply simplification if ite is an if-then-else tree where every leaf is a value.
+   
+   This is an efficient way to 
+   
+*/
+br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) {
+    SASSERT(m().is_ite(ite));
+    SASSERT(m().is_value(val));
+
+    expr * t = ite->get_arg(1);
+    expr * e = ite->get_arg(2);
+    if (!m().is_value(t) || !m().is_value(e))
+        return BR_FAILED;
+
+    if (t != val && e != val) {
+        TRACE("try_ite_value", tout << mk_ismt2_pp(t, m()) << " " << mk_ismt2_pp(e, m()) << " " << mk_ismt2_pp(val, m()) << "\n";
+              tout << t << " " << e << " " << val << "\n";);
+        result = m().mk_false();
+        return BR_DONE;
+    } 
+
+    if (t == val && e == val) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+
+    if (t == val) {
+        result = ite->get_arg(0);
+        return BR_DONE;
+    }
+
+    SASSERT(e == val);
+    
+    mk_not(ite->get_arg(0), result);
+    return BR_DONE;
+}
+
+#if 0
+// Return true if ite is an if-then-else tree where the leaves are values,
+// and they are all different from val
+static bool is_ite_value_tree_neq_value(ast_manager & m, app * ite, app * val) {
+    SASSERT(m.is_ite(ite));
+    SASSERT(m.is_value(val));
+
+    expr_fast_mark1 visited;
+    ptr_buffer<app> todo;
+    todo.push_back(ite);
+
+#define VISIT(ARG) {                                            \
+        if (m.is_value(ARG)) {                                  \
+            if (ARG == val)                                     \
+                return false;                                   \
+        }                                                       \
+        else if (m.is_ite(ARG)) {                               \
+            if (!visited.is_marked(ARG)) {                      \
+                visited.mark(ARG);                              \
+                todo.push_back(to_app(ARG));                    \
+            }                                                   \
+        }                                                       \
+        else {                                                  \
+            return false;                                       \
+        }                                                       \
+    }
+
+    while (!todo.empty()) {
+        app * ite = todo.back();
+        todo.pop_back();
+        SASSERT(m.is_ite(ite));
+        expr * t = ite->get_arg(1);
+        expr * e = ite->get_arg(2);
+        VISIT(t);
+        VISIT(e);
+    }
+
+    return true;
+}
+#endif 
+
+br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
+    if (lhs == rhs) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    
+    if (m().are_distinct(lhs, rhs)) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+
+    br_status r = BR_FAILED;
+    if (m().is_ite(lhs) && m().is_value(rhs)) {
+        // if (is_ite_value_tree_neq_value(m(), to_app(lhs), to_app(rhs))) {
+        //    result = m().mk_false();
+        //    return BR_DONE;
+        // }
+        r = try_ite_value(to_app(lhs), to_app(rhs), result);
+        CTRACE("try_ite_value", r != BR_FAILED, 
+               tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";);
+    }
+    else if (m().is_ite(rhs) && m().is_value(lhs)) {
+        // if (is_ite_value_tree_neq_value(m(), to_app(rhs), to_app(lhs))) {
+        //    result = m().mk_false();
+        //    return BR_DONE;
+        // }
+        r = try_ite_value(to_app(rhs), to_app(lhs), result);
+        CTRACE("try_ite_value", r != BR_FAILED, 
+               tout << mk_ismt2_pp(lhs, m()) << "\n" << mk_ismt2_pp(rhs, m()) << "\n--->\n" << mk_ismt2_pp(result, m()) << "\n";);
+    }
+    if (r != BR_FAILED)
+        return r;
+
+    if (m().is_bool(lhs)) {
+        bool unfolded = false;
+        if (m().is_not(lhs) && m().is_not(rhs)) {
+            lhs = to_app(lhs)->get_arg(0);
+            rhs = to_app(rhs)->get_arg(0);
+            unfolded = true;
+        }
+        if (m().is_true(lhs)) {
+            result = rhs;
+            return BR_DONE;
+        }
+        if (m().is_false(lhs)) {
+            mk_not(rhs, result);
+            return BR_DONE;
+        }
+        if (m().is_true(rhs)) {
+            result = lhs;
+            return BR_DONE;
+        }
+        if (m().is_false(rhs)) {
+            mk_not(lhs, result);
+            return BR_DONE;
+        }
+        if (m().is_complement(lhs, rhs)) {
+            result = m().mk_false();
+            return BR_DONE;
+        }
+        if (unfolded) {
+            result = m().mk_eq(lhs, rhs);
+            return BR_DONE;
+        }
+    }
+    return BR_FAILED;
+}
+
+br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    if (num_args <= 1) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+
+    if (num_args == 2) {
+        expr_ref tmp(m());
+        result = m().mk_not(m().mk_eq(args[0], args[1]));
+        return BR_REWRITE2; // mk_eq may be dispatched to other rewriters.
+    }
+
+    expr_fast_mark1 visited;
+    bool all_value = true;
+    for (unsigned i = 0; i < num_args; i++) {
+        expr * arg = args[i];
+        if (visited.is_marked(arg)) {
+            result = m().mk_false();
+            return BR_DONE;
+        }
+        visited.mark(arg);
+        if (!m().is_value(arg))
+            all_value = false;
+    }
+    if (all_value) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+
+    SASSERT(num_args > 2);
+    if (m().is_bool(args[0])) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+
+    if (m_blast_distinct) {
+        ptr_buffer<expr> new_diseqs;
+        for (unsigned i = 0; i < num_args; i++) {
+            for (unsigned j = i + 1; j < num_args; j++)
+                new_diseqs.push_back(m().mk_not(m().mk_eq(args[i], args[j])));
+        }
+        result = m().mk_and(new_diseqs.size(), new_diseqs.c_ptr());
+        return BR_REWRITE3;
+    }
+    
+    return BR_FAILED;
+}
+
+br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result) {
+    bool s = false;
+    
+    // (ite (not c) a b) ==> (ite c b a)
+    if (m().is_not(c)) {
+        c = to_app(c)->get_arg(0);
+        std::swap(t, e);
+        s = true;
+    }
+
+    // (ite c (ite c t1 t2) t3)       ==> (ite c t1 t3)
+    if (m().is_ite(t) && to_app(t)->get_arg(0) == c) {
+        // Remark: (ite c (ite (not c) t1 t2) t3) ==> (ite c t2 t3) does not happen if applying rewrites bottom up
+        t = to_app(t)->get_arg(1);
+        s = true;
+    }
+
+    // (ite c t1 (ite c t2 t3))       ==> (ite c t1 t3)
+    if (m().is_ite(e) && to_app(e)->get_arg(0) == c) {
+        // Remark: (ite c t1 (ite (not c) t2 t3)) ==> (ite c t1 t2) does not happen if applying rewrites bottom up
+        e = to_app(e)->get_arg(2);
+        s = true;
+    }
+
+    if (m().is_true(c)) {
+        result = t;
+        return BR_DONE;
+    }
+    
+    if (m().is_false(c)) {
+        result = e;
+        return BR_DONE;
+    }
+
+    if (t == e) {
+        result = t;
+        return BR_DONE;
+    }
+
+    if (m().is_bool(t)) {
+        if (m().is_true(t)) {
+            if (m().is_false(e)) {
+                result = c;
+                return BR_DONE;
+            }
+            mk_or(c, e, result);
+            return BR_DONE;
+        }
+        if (m().is_false(t)) {
+            if (m().is_true(e)) {
+                mk_not(c, result);
+                return BR_DONE;
+            }
+            expr_ref tmp(m());
+            mk_not(c, tmp); 
+            mk_and(tmp, e, result);
+            return BR_DONE;
+        }
+        if (m().is_true(e)) {
+            expr_ref tmp(m());
+            mk_not(c, tmp); 
+            mk_or(tmp, t, result);
+            return BR_DONE;
+        }
+        if (m().is_false(e)) {
+            mk_and(c, t, result); 
+            return BR_DONE;
+        }
+        if (c == e) {
+            mk_and(c, t, result);
+            return BR_DONE;
+        }
+        if (c == t) {
+            mk_or(c, e, result); 
+            return BR_DONE;
+        }
+        if (m().is_complement_core(t, e)) { // t = not(e) 
+            mk_eq(c, t, result);
+            return BR_DONE;
+        }
+        if (m().is_complement_core(e, t)) { // e = not(t)
+            mk_eq(c, t, result);
+            return BR_DONE;
+        }
+    }
+
+    if (m().is_ite(t) && m_ite_extra_rules) {
+        // (ite c1 (ite c2 t1 t2) t1) ==> (ite (and c1 (not c2)) t2 t1)
+        if (e == to_app(t)->get_arg(1)) {
+            expr_ref not_c2(m());
+            mk_not(to_app(t)->get_arg(0), not_c2);
+            expr_ref new_c(m());
+            mk_and(c, not_c2, new_c);
+            result = m().mk_ite(new_c, to_app(t)->get_arg(2), e);
+            return BR_REWRITE1;
+        }
+        // (ite c1 (ite c2 t1 t2) t2) ==> (ite (and c1 c2) t1 t2)
+        if (e == to_app(t)->get_arg(2)) {
+            expr_ref new_c(m());
+            mk_and(c, to_app(t)->get_arg(0), new_c);
+            result = m().mk_ite(new_c, to_app(t)->get_arg(1), e);
+            return BR_REWRITE1;
+        }
+        
+        if (m().is_ite(e)) {
+            // (ite c1 (ite c2 t1 t2) (ite c3 t1 t2)) ==> (ite (or (and c1 c2) (and (not c1) c3)) t1 t2)
+            if (to_app(t)->get_arg(1) == to_app(e)->get_arg(1) && 
+                to_app(t)->get_arg(2) == to_app(e)->get_arg(2)) {
+                expr_ref and1(m());
+                expr_ref and2(m());
+                expr_ref notc(m());
+                mk_and(c, to_app(t)->get_arg(0), and1);
+                mk_not(c, notc);
+                mk_and(notc, to_app(e)->get_arg(0), and2);
+                expr_ref new_c(m());
+                mk_or(and1, and2, new_c);
+                result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2));
+                return BR_REWRITE1;
+            }
+            
+            // (ite c1 (ite c2 t1 t2) (ite c3 t2 t1)) ==> (ite (or (and c1 c2) (and (not c1) (not c3))) t1 t2)
+            if (to_app(t)->get_arg(1) == to_app(e)->get_arg(2) && 
+                to_app(t)->get_arg(2) == to_app(e)->get_arg(1)) {
+                expr_ref and1(m());
+                expr_ref and2(m());
+                expr_ref notc(m());
+                mk_and(c, to_app(t)->get_arg(0), and1);
+                mk_not(c, notc);
+                expr_ref notc3(m());
+                mk_not(to_app(e)->get_arg(0), notc3);
+                mk_and(notc, notc3, and2);
+                expr_ref new_c(m());
+                mk_or(and1, and2, new_c);
+                result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2));
+                return BR_REWRITE1;
+            }
+        }
+    }
+
+    if (m().is_ite(e) && m_ite_extra_rules) {
+        // (ite c1 t1 (ite c2 t1 t2)) ==> (ite (or c1 c2)        t1 t2)
+        if (t == to_app(e)->get_arg(1)) {
+            expr_ref new_c(m());
+            mk_or(c, to_app(e)->get_arg(0), new_c);
+            result = m().mk_ite(new_c, t, to_app(e)->get_arg(2));
+            return BR_REWRITE1;
+        }
+        // (ite c1 t1 (ite c2 t2 t1)) ==> (ite (or c1 (not c2))  t1 t2)
+        if (t == to_app(e)->get_arg(2)) {
+            expr_ref not_c2(m());
+            mk_not(to_app(e)->get_arg(0), not_c2);
+            expr_ref new_c(m());
+            mk_or(c, not_c2, new_c);
+            result = m().mk_ite(new_c, t, to_app(e)->get_arg(1));
+            return BR_REWRITE1;
+        }
+    }
+
+    if (s) {
+        result = m().mk_ite(c, t, e);
+        return BR_DONE;
+    }
+    
+    return BR_FAILED;
+}
+ 
+br_status bool_rewriter::mk_not_core(expr * t, expr_ref & result) {
+    if (m().is_not(t)) {
+        result = to_app(t)->get_arg(0);
+        return BR_DONE;
+    }
+    if (m().is_true(t)) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    if (m().is_false(t)) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    if (is_eq(t) && m().is_bool(to_app(t)->get_arg(0))) {
+        expr_ref tmp(m());
+        mk_not(to_app(t)->get_arg(0), tmp);
+        mk_eq(tmp, to_app(t)->get_arg(1), result);
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
+void bool_rewriter::mk_xor(expr * lhs, expr * rhs, expr_ref & result) {
+    expr_ref tmp(m());
+    mk_not(lhs, tmp);
+    mk_eq(tmp, rhs, result);
+}
+
+void bool_rewriter::mk_implies(expr * lhs, expr * rhs, expr_ref & result) {
+    expr_ref tmp(m());
+    mk_not(lhs, tmp);
+    mk_or(tmp, rhs, result);
+}
+
+void bool_rewriter::mk_nand(unsigned num_args, expr * const * args, expr_ref & result) {
+    expr_ref tmp(m_manager);
+    mk_and(num_args, args, tmp);
+    mk_not(tmp, result);
+}
+
+void bool_rewriter::mk_nor(unsigned num_args, expr * const * args, expr_ref & result) {
+    expr_ref tmp(m_manager);
+    mk_or(num_args, args, tmp);
+    mk_not(tmp, result);
+}
+
+void bool_rewriter::mk_nand(expr * arg1, expr * arg2, expr_ref & result) {
+    expr_ref tmp(m_manager);
+    mk_and(arg1, arg2, tmp);
+    mk_not(tmp, result);
+}
+
+void bool_rewriter::mk_nor(expr * arg1, expr * arg2, expr_ref & result) {
+    expr_ref tmp(m_manager);
+    mk_or(arg1, arg2, tmp);
+    mk_not(tmp, result);
+}
+
+template class rewriter_tpl<bool_rewriter_cfg>;

src/rewriter/bool_rewriter.h

@@ -0,0 +1,199 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    bool_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for Boolean operators.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-04
+
+Notes:
+
+--*/
+#ifndef _BOOL_REWRITER_H_
+#define _BOOL_REWRITER_H_
+
+#include"ast.h"
+#include"rewriter.h"
+#include"params.h"
+
+/**
+   \brief Apply basic Boolean rewriting operations.
+
+   Only depth 1 simplifications are performed.
+
+   Note: there are no recursive calls. 
+
+   Note: arguments of AC operators are not sorted.
+   Note: arguments of = and xor are also not sorted.
+   
+   Note: By default, (AND A B) is not rewritten as (NOT (OR (NOT A) (NOT B)))
+
+   Note: AND OR operators are flattened only if mk_flat_app, mk_flat_or, mk_flat_and are used.
+   
+   The following operators are expanded:
+   - => (implies)
+   - xor
+   - nand
+   - nor
+   - iff    
+   
+   All methods run in time almost linear on the number of arguments.
+   Actually, this is not true when flattening is enabled.
+   A better approximation is O(Sum_{t \in args} size1(t)).
+   Where size1(t) = max{t->get_num_args(), 1}.
+*/
+class bool_rewriter {
+    ast_manager &  m_manager;
+    bool           m_flat;
+    bool           m_local_ctx;
+    bool           m_elim_and;
+    bool           m_blast_distinct;
+    bool           m_ite_extra_rules;
+    unsigned       m_local_ctx_limit;
+    unsigned       m_local_ctx_cost;
+
+    br_status mk_flat_and_core(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_flat_or_core(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_nflat_and_core(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_nflat_or_core(unsigned num_args, expr * const * args, expr_ref & result);
+
+    void mk_and_as_or(unsigned num_args, expr * const * args, expr_ref & result);
+
+    expr * mk_or_app(unsigned num_args, expr * const * args);
+    bool simp_nested_not_or(unsigned num_args, expr * const * args, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result);
+    expr * simp_arg(expr * arg, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, bool & modified);
+    void mk_nested_ite(expr * new_c, expr * new_t, expr * new_e, expr_ref & result);
+    bool simp_nested_eq_ite(expr * t, expr_fast_mark1 & neg_lits, expr_fast_mark2 & pos_lits, expr_ref & result);
+    bool local_ctx_simp(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status try_ite_value(app * ite, app * val, expr_ref & result);
+
+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 flat() const { return m_flat; }
+    void set_flat(bool f) { m_flat = f; }
+    bool elim_and() const { return m_elim_and; }
+    void set_elim_and(bool f) { m_elim_and = f; }
+    void reset_local_ctx_cost() { m_local_ctx_cost = 0; }
+    
+    void updt_params(params_ref const & p);
+
+    static void get_param_descrs(param_descrs & r);
+
+    // The core methods return true if a rewrite-step/simplification was applied
+    // to the arguments, and the result is stored in 'result'. Otherwise, they return false
+    // and result.get == 0.
+    
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+        if (mk_app_core(f, num_args, args, result) == BR_FAILED)
+            result = m().mk_app(f, num_args, args);
+    }
+    
+    br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+    br_status mk_distinct_core(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_iff_core(expr * lhs, expr * rhs, expr_ref & result) { return mk_eq_core(lhs, rhs, result); }
+    br_status mk_and_core(unsigned num_args, expr * const * args, expr_ref & result) {
+        if (m_elim_and) {
+            mk_and_as_or(num_args, args, result);
+            return BR_DONE;
+        }
+        else if (m_flat) {
+            return mk_flat_and_core(num_args, args, result);
+        }
+        else {
+            return mk_nflat_and_core(num_args, args, result);
+        }
+    }
+    br_status mk_or_core(unsigned num_args, expr * const * args, expr_ref & result) {
+        return m_flat ?
+            mk_flat_or_core(num_args, args, result) :
+            mk_nflat_or_core(num_args, args, result);
+    }
+    br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result);
+    br_status mk_not_core(expr * t, expr_ref & result);
+
+    void mk_eq(expr * lhs, expr * rhs, expr_ref & result) {
+        if (mk_eq_core(lhs, rhs, result) == BR_FAILED)
+            result = m().mk_eq(lhs, rhs);
+    }
+    void mk_iff(expr * lhs, expr * rhs, expr_ref & result) { mk_eq(lhs, rhs, result); }
+    void mk_xor(expr * lhs, expr * rhs, expr_ref & result);
+    void mk_and(unsigned num_args, expr * const * args, expr_ref & result) {
+        if (mk_and_core(num_args, args, result) == BR_FAILED) {
+            SASSERT(!m_elim_and);
+            result = m().mk_and(num_args, args);
+        }
+    }
+    void mk_or(unsigned num_args, expr * const * args, expr_ref & result) {
+        if (mk_or_core(num_args, args, result) == BR_FAILED)
+            result = m().mk_or(num_args, args);
+    }
+    void mk_and(expr * arg1, expr * arg2, expr_ref & result) {
+        expr * args[2] = {arg1, arg2};
+        mk_and(2, args, result);
+    }
+    void mk_or(expr * arg1, expr * arg2, expr_ref & result) {
+        expr * args[2] = {arg1, arg2};
+        mk_or(2, args, result);
+    }
+    void mk_and(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
+        expr * args[3] = {arg1, arg2, arg3};
+        mk_and(3, args, result);
+    }
+    void mk_or(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
+        expr * args[3] = {arg1, arg2, arg3};
+        mk_or(3, args, result);
+    }
+    void mk_implies(expr * lhs, expr * rhs, expr_ref & result);
+    void mk_ite(expr * c, expr * t, expr * e, expr_ref & result) {
+        if (mk_ite_core(c, t, e, result) == BR_FAILED)
+            result = m().mk_ite(c, t, e);
+    }
+    void mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
+        if (mk_distinct_core(num_args, args, result) == BR_FAILED)
+            result = m().mk_distinct(num_args, args);
+    }
+    void mk_not(expr * t, expr_ref & result) {
+        if (mk_not_core(t, result) == BR_FAILED)
+            result = m().mk_not(t);
+    }
+
+    void mk_nand(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_nor(unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_nand(expr * arg1, expr * arg2, expr_ref & result);
+    void mk_nor(expr * arg1, expr * arg2, expr_ref & result);
+};
+
+struct bool_rewriter_cfg : public default_rewriter_cfg {
+    bool_rewriter m_r;
+    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;
+        if (f->get_family_id() != m_r.get_fid())
+            return BR_FAILED;
+        return m_r.mk_app_core(f, num, args, result);
+    }
+    bool_rewriter_cfg(ast_manager & m, params_ref const & p):m_r(m, p) {}
+};
+
+class bool_rewriter_star : public rewriter_tpl<bool_rewriter_cfg> {
+    bool_rewriter_cfg m_cfg;
+public:
+    bool_rewriter_star(ast_manager & m, params_ref const & p):
+        rewriter_tpl<bool_rewriter_cfg>(m, false, m_cfg),
+        m_cfg(m, p) {}
+};
+
+#endif

src/rewriter/bv_rewriter.h

@@ -0,0 +1,171 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    bv_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for bit-vectors
+
+Author:
+
+    Leonardo (leonardo) 2011-04-14
+
+Notes:
+
+--*/
+#ifndef _BV_REWRITER_H_
+#define _BV_REWRITER_H_
+
+#include"poly_rewriter.h"
+#include"bv_decl_plugin.h"
+#include"arith_decl_plugin.h"
+
+class mk_extract_proc {
+    bv_util &     m_util;
+    unsigned      m_high;
+    unsigned      m_low;
+    sort *        m_domain;
+    func_decl *   m_f_cached;
+public:
+    mk_extract_proc(bv_util & u);
+    ~mk_extract_proc();
+    app * operator()(unsigned high, unsigned low, expr * arg);
+};
+
+class bv_rewriter_core {
+protected:
+    typedef rational numeral;
+    bv_util         m_util;
+    ast_manager & m() const { return m_util.get_manager(); }
+    family_id get_fid() const { return m_util.get_family_id(); }
+
+    bool is_numeral(expr * n) const { return m_util.is_numeral(n); }
+    bool is_numeral(expr * n, numeral & r) const { unsigned sz; return m_util.is_numeral(n, r, sz); }
+    bool is_zero(expr * n) const { return m_util.is_zero(n); }
+    bool is_minus_one(expr * n) const { return m_util.is_allone(n); }
+    void normalize(numeral & c, sort * s) { unsigned bv_size = m_util.get_bv_size(s); c = m_util.norm(c, bv_size); }
+    app * mk_numeral(numeral const & r, sort * s) { return m_util.mk_numeral(r, s); }
+    decl_kind add_decl_kind() const { return OP_BADD; }
+    decl_kind mul_decl_kind() const { return OP_BMUL; }
+    bool use_power() const { return false; }
+    decl_kind power_decl_kind() const { UNREACHABLE(); return static_cast<decl_kind>(UINT_MAX); }
+public:
+    bv_rewriter_core(ast_manager & m):m_util(m) {}
+};
+
+class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
+    mk_extract_proc m_mk_extract;
+    arith_util m_autil;
+    bool       m_hi_div0;
+    bool       m_elim_sign_ext;
+    bool       m_mul2concat;
+    bool       m_bit2bool;
+    bool       m_blast_eq_value;
+    bool       m_mkbv2num;
+    bool       m_split_concat_eq;
+    bool       m_udiv2mul;
+
+    bool is_zero_bit(expr * x, unsigned idx);
+
+    br_status mk_ule(expr * a, expr * b, expr_ref & result);
+    br_status mk_uge(expr * a, expr * b, expr_ref & result);
+    br_status mk_ult(expr * a, expr * b, expr_ref & result);
+    br_status mk_sle(expr * a, expr * b, expr_ref & result);
+    br_status mk_sge(expr * a, expr * b, expr_ref & result);
+    br_status mk_slt(expr * a, expr * b, expr_ref & result);
+    br_status mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref & result);
+
+    br_status mk_concat(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_extract(unsigned high, unsigned low, expr * arg, expr_ref & result);
+    br_status mk_repeat(unsigned n, expr * arg, expr_ref & result);
+    br_status mk_zero_extend(unsigned n, expr * arg, expr_ref & result);
+    br_status mk_sign_extend(unsigned n, expr * arg, expr_ref & result);
+    br_status mk_bv_not(expr * arg, expr_ref & result);
+    br_status mk_bv_or(unsigned num, expr * const * args, expr_ref & result);
+    br_status mk_bv_xor(unsigned num, expr * const * args, expr_ref & result);
+    br_status mk_bv_and(unsigned num, expr * const * args, expr_ref & result);
+    br_status mk_bv_nand(unsigned num, expr * const * args, expr_ref & result);
+    br_status mk_bv_nor(unsigned num, expr * const * args, expr_ref & result);
+    br_status mk_bv_xnor(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_bv_rotate_left(unsigned n, expr * arg, expr_ref & result);
+    br_status mk_bv_rotate_right(unsigned n, expr * arg, expr_ref & result);
+    br_status mk_bv_ext_rotate_left(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_bv_add(expr * arg1, expr * arg2, expr_ref & result) {
+        expr * args[2] = { arg1, arg2 };
+        return mk_bv_add(2, args, result);
+    }
+    br_status mk_bv_mul(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_bv_lshr(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result);
+    bool is_minus_one_core(expr * arg) const;
+    bool is_x_minus_one(expr * arg, expr * & x);
+    br_status mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);
+    br_status mk_bv_udiv_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);
+    br_status mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);
+    br_status mk_bv_urem_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);
+    br_status mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, expr_ref & result);
+    br_status mk_bv_sdiv(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_sdiv_core(arg1, arg2, m_hi_div0, result); }
+    br_status mk_bv_udiv(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_udiv_core(arg1, arg2, m_hi_div0, result); }
+    br_status mk_bv_srem(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_srem_core(arg1, arg2, m_hi_div0, result); }
+    br_status mk_bv_urem(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_urem_core(arg1, arg2, m_hi_div0, result); }
+    br_status mk_bv_smod(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_smod_core(arg1, arg2, m_hi_div0, result); }
+    br_status mk_bv_sdiv_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_sdiv_core(arg1, arg2, true, result); }
+    br_status mk_bv_udiv_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_udiv_core(arg1, arg2, true, result); }
+    br_status mk_bv_srem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_srem_core(arg1, arg2, true, result); }
+    br_status mk_bv_urem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_urem_core(arg1, arg2, true, result); }
+    br_status mk_bv_smod_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_smod_core(arg1, arg2, true, result); }
+    br_status mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result);
+    br_status mk_bv2int(expr * arg, expr_ref & result);
+    br_status mk_bv_redor(expr * arg, expr_ref & result);
+    br_status mk_bv_redand(expr * arg, expr_ref & result);
+    br_status mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result);
+    br_status mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & result);
+    br_status mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result);
+    br_status mk_mkbv(unsigned num, expr * const * args, expr_ref & result);
+    bool is_minus_one_times_t(expr * arg);
+    void mk_t1_add_t2_eq_c(expr * t1, expr * t2, expr * c, expr_ref & result);
+
+    bool is_concat_split_target(expr * t) const;
+
+    br_status mk_mul_eq(expr * lhs, expr * rhs, expr_ref & result);
+
+    void updt_local_params(params_ref const & p);
+
+public:
+    bv_rewriter(ast_manager & m, params_ref const & p = params_ref()):
+        poly_rewriter<bv_rewriter_core>(m, p),
+        m_mk_extract(m_util),
+        m_autil(m) {
+        updt_local_params(p);
+    }
+
+    void updt_params(params_ref const & p);
+
+    static void get_param_descrs(param_descrs & r);
+    
+    void set_mkbv2num(bool f) { m_mkbv2num = f; }
+
+    unsigned get_bv_size(expr * t) const {return m_util.get_bv_size(t); }
+    bool is_numeral(expr * t) const { return m_util.is_numeral(t); }
+    bool is_numeral(expr * t, numeral & r, unsigned & sz) const { return m_util.is_numeral(t, r, sz); }
+    bool is_bv(expr * t) const { return m_util.is_bv(t); }
+    expr * mk_numeral(numeral const & v, unsigned sz) { return m_util.mk_numeral(v, sz); }
+    expr * mk_numeral(unsigned v, unsigned sz) { return m_util.mk_numeral(numeral(v), sz); }
+    
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    void mk_app(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+        if (mk_app_core(f, num_args, args, result) == BR_FAILED)
+            result = m().mk_app(f, num_args, args);
+    }
+
+    br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+};
+
+#endif

src/rewriter/datatype_rewriter.cpp

@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    datatype_rewriter.cpp
+
+Abstract:
+
+    Basic rewriting rules for Datatypes.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-06
+
+Notes:
+
+--*/
+#include"datatype_rewriter.h"
+
+br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(f->get_family_id() == get_fid());
+    switch(f->get_decl_kind()) {
+    case OP_DT_CONSTRUCTOR: return BR_FAILED;
+    case OP_DT_RECOGNISER:
+        //
+        // simplify is_cons(cons(x,y)) -> true
+        // simplify is_cons(nil) -> false
+        //
+        SASSERT(num_args == 1);
+        if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
+            return BR_FAILED;
+        if (to_app(args[0])->get_decl() == m_util.get_recognizer_constructor(f))
+            result = m().mk_true();
+        else
+            result = m().mk_false();
+        return BR_DONE;
+    case OP_DT_ACCESSOR: {
+        // 
+        // simplify head(cons(x,y)) -> x
+        // 
+        SASSERT(num_args == 1);
+        if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
+            return BR_FAILED;
+        
+        app * a = to_app(args[0]);
+        func_decl * c_decl = a->get_decl();
+        if (c_decl != m_util.get_accessor_constructor(f))
+            return BR_FAILED;
+        ptr_vector<func_decl> const * acc = m_util.get_constructor_accessors(c_decl);
+        SASSERT(acc && acc->size() == a->get_num_args());
+        unsigned num = acc->size();
+        for (unsigned i = 0; i < num; ++i) {
+            if (f == (*acc)[i]) {
+                // found it.
+                result = a->get_arg(i);
+                return BR_DONE;
+            }
+        }
+        UNREACHABLE();
+        break;
+    }
+    default:
+        UNREACHABLE();
+    }
+    
+    return BR_FAILED;
+}
+
+br_status datatype_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
+    if (!is_app(lhs) || !is_app(rhs) || !m_util.is_constructor(to_app(lhs)) || !m_util.is_constructor(to_app(rhs)))
+        return BR_FAILED;
+    if (to_app(lhs)->get_decl() != to_app(rhs)->get_decl()) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+
+    // Remark: In datatype_simplifier_plugin, we used
+    // m_basic_simplifier to create '=' and 'and' applications in the
+    // following code. This trick not guarantee that the final expression
+    // will be fully simplified. 
+    //
+    // Example:
+    // The assertion  
+    // (assert (= (cons a1 (cons a2 (cons a3 (cons (+ a4 1) (cons (+ a5 c5) (cons a6 nil))))))
+    //         (cons b1 (cons b2 (cons b3 (cons b4 (cons b5 (cons b6 nil))))))))
+    // 
+    // After applying asserted_formulas::reduce(), the following formula was generated.
+    //
+    //   (= a1 b1)
+    //   (= a2 b2)
+    //   (= a3 b3)
+    //   (= (+ a4 (* (- 1) b4)) (- 1))
+    //   (= (+ c5 a5) b5)                    <<< NOT SIMPLIFIED WITH RESPECT TO ARITHMETIC
+    //   (= (cons a6 nil) (cons b6 nil)))    <<< NOT SIMPLIFIED WITH RESPECT TO DATATYPE theory
+    //
+    // Note that asserted_formulas::reduce() applied the simplier many times.
+    // After the first simplification step we had:
+    //  (= a1 b1)
+    //  (= (cons a2 (cons a3 (cons (+ a4 1) (cons (+ a5 c5) (cons a6 nil))))))
+    //     (cons b2 (cons b3 (cons b4 (cons b5 (cons b6 nil))))))
+
+    ptr_buffer<expr> eqs;
+    unsigned num = to_app(lhs)->get_num_args();
+    SASSERT(num == to_app(rhs)->get_num_args());
+    for (unsigned i = 0; i < num; ++i) {            
+        eqs.push_back(m().mk_eq(to_app(lhs)->get_arg(i), to_app(rhs)->get_arg(i)));
+    }
+    result = m().mk_and(eqs.size(), eqs.c_ptr());
+    return BR_REWRITE2;
+}

src/rewriter/datatype_rewriter.h

@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    datatype_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for Datatypes.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-06
+
+Notes:
+
+--*/
+#ifndef _DATATYPE_REWRITER_H_
+#define _DATATYPE_REWRITER_H_
+
+#include"datatype_decl_plugin.h"
+#include"rewriter_types.h"
+
+class datatype_rewriter {
+    datatype_util    m_util;
+public:    
+    datatype_rewriter(ast_manager & m):m_util(m) {}
+    ast_manager & m() const { return m_util.get_manager(); }
+    family_id get_fid() const { return m_util.get_family_id(); }
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result);
+};
+
+#endif

src/rewriter/dl_rewriter.cpp

@@ -0,0 +1,57 @@
+/*++
+Copyright (c) 2010 Microsoft Corporation
+
+Module Name:
+
+    dl_rewriter.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2010-08-10
+
+Revision History:
+
+--*/
+
+#include"dl_rewriter.h"
+    
+    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;
+        switch(f->get_decl_kind()) {
+		case datalog::OP_DL_LT:
+            if (m_util.is_numeral_ext(args[0], v1) &&
+                m_util.is_numeral_ext(args[1], v2)) {
+                result = (v1 < v2)?m.mk_true():m.mk_false();
+                return BR_DONE;
+            }
+            // x < x <=> false
+            if (args[0] == args[1]) {
+                result = m.mk_false();
+                return BR_DONE;
+            }
+            // x < 0 <=> false
+            if (m_util.is_numeral_ext(args[1], v2) && v2 == 0) {
+                result = m.mk_false();
+                return BR_DONE;
+            }
+            // 0 < x <=> 0 != x
+            if (m_util.is_numeral_ext(args[1], v1) && v1 == 0) {
+                result = m.mk_not(m.mk_eq(args[0], args[1]));
+                return BR_DONE;
+            }
+            break;
+
+        default:
+            break;
+        }
+        return BR_FAILED;
+    }
+    
+
+

src/rewriter/dl_rewriter.h

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    dl_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for atalog finite domains.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2012-03-09
+
+Notes:
+
+--*/
+#ifndef _DL_REWRITER_H_
+#define _DL_REWRITER_H_
+
+#include"dl_decl_plugin.h"
+#include"rewriter_types.h"
+
+class dl_rewriter {
+    datalog::dl_decl_util    m_util;
+public:    
+    dl_rewriter(ast_manager & m):m_util(m) {}
+    family_id get_fid() const { return m_util.get_family_id(); }
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+};
+
+#endif

src/rewriter/float_rewriter.cpp

@@ -0,0 +1,441 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    float_rewriter.cpp
+
+Abstract:
+
+    Basic rewriting rules for floating point numbers.
+
+Author:
+
+    Leonardo (leonardo) 2012-02-02
+
+Notes:
+
+--*/
+#include"float_rewriter.h"
+
+float_rewriter::float_rewriter(ast_manager & m, params_ref const & p):
+    m_util(m) {
+    updt_params(p);
+}
+
+float_rewriter::~float_rewriter() {
+}
+
+void float_rewriter::updt_params(params_ref const & p) {
+}
+ 
+void float_rewriter::get_param_descrs(param_descrs & r) {
+}
+
+br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    br_status st = BR_FAILED;
+    SASSERT(f->get_family_id() == get_fid());
+    switch (f->get_decl_kind()) {
+    case OP_TO_FLOAT:        st = mk_to_float(f, num_args, args, result); break;
+    case OP_FLOAT_ADD:       SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break;
+    case OP_FLOAT_SUB:       SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break;
+    case OP_FLOAT_UMINUS:    SASSERT(num_args == 1); st = mk_uminus(args[0], result); break;
+    case OP_FLOAT_MUL:       SASSERT(num_args == 3); st = mk_mul(args[0], args[1], args[2], result); break;
+    case OP_FLOAT_DIV:       SASSERT(num_args == 3); st = mk_div(args[0], args[1], args[2], result); break;
+    case OP_FLOAT_REM:       SASSERT(num_args == 2); st = mk_rem(args[0], args[1], result); break;
+    case OP_FLOAT_ABS:       SASSERT(num_args == 1); st = mk_abs(args[0], result); break;
+    case OP_FLOAT_MIN:       SASSERT(num_args == 2); st = mk_min(args[0], args[1], result); break;
+    case OP_FLOAT_MAX:       SASSERT(num_args == 2); st = mk_max(args[0], args[1], result); break;
+    case OP_FLOAT_FUSED_MA:  SASSERT(num_args == 4); st = mk_fused_ma(args[0], args[1], args[2], args[3], result); break;
+    case OP_FLOAT_SQRT:      SASSERT(num_args == 2); st = mk_sqrt(args[0], args[1], result); break;
+    case OP_FLOAT_ROUND_TO_INTEGRAL: SASSERT(num_args == 2); st = mk_round(args[0], args[1], result); break;
+
+    case OP_FLOAT_EQ:        SASSERT(num_args == 2); st = mk_float_eq(args[0], args[1], result); break; 
+    case OP_FLOAT_LT:        SASSERT(num_args == 2); st = mk_lt(args[0], args[1], result); break;
+    case OP_FLOAT_GT:        SASSERT(num_args == 2); st = mk_gt(args[0], args[1], result); break;
+    case OP_FLOAT_LE:        SASSERT(num_args == 2); st = mk_le(args[0], args[1], result); break;
+    case OP_FLOAT_GE:        SASSERT(num_args == 2); st = mk_ge(args[0], args[1], result); break;
+    case OP_FLOAT_IS_ZERO:   SASSERT(num_args == 1); st = mk_is_zero(args[0], result); break;
+    case OP_FLOAT_IS_NZERO:  SASSERT(num_args == 1); st = mk_is_nzero(args[0], result); break;
+    case OP_FLOAT_IS_PZERO:  SASSERT(num_args == 1); st = mk_is_pzero(args[0], result); break;
+    case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break;
+    }
+    return st;
+}
+
+br_status float_rewriter::mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(f->get_num_parameters() == 2);
+    SASSERT(f->get_parameter(0).is_int());
+    SASSERT(f->get_parameter(1).is_int());
+    unsigned ebits = f->get_parameter(0).get_int();
+    unsigned sbits = f->get_parameter(1).get_int();
+
+    if (num_args == 2) {
+        mpf_rounding_mode rm;
+        if (!m_util.is_rm(args[0], rm))
+            return BR_FAILED;
+        
+        rational q;
+        if (!m_util.au().is_numeral(args[1], q))
+            return BR_FAILED;
+        
+        mpf v;
+        m_util.fm().set(v, ebits, sbits, rm, q.to_mpq());
+        result = m_util.mk_value(v);
+        m_util.fm().del(v);
+        return BR_DONE;
+    }
+    else if (num_args == 3 && 
+             m_util.is_rm(m().get_sort(args[0])) && 
+             m_util.au().is_real(args[1]) &&
+             m_util.au().is_int(args[2])) {
+
+        mpf_rounding_mode rm;
+        if (!m_util.is_rm(args[0], rm))
+            return BR_FAILED;
+
+        rational q;
+        if (!m_util.au().is_numeral(args[1], q))
+            return BR_FAILED;
+
+        rational e;
+        if (!m_util.au().is_numeral(args[2], e))
+            return BR_FAILED;
+
+        TRACE("fp_rewriter", tout << "q: " << q << ", e: " << e << "\n";);
+
+        mpf v;
+	    m_util.fm().set(v, ebits, sbits, rm, q.to_mpq(), e.to_mpq().numerator());
+        result = m_util.mk_value(v);
+        m_util.fm().del(v);
+        return BR_DONE;
+    }
+    else {
+        return BR_FAILED;
+    }
+}
+
+br_status float_rewriter::mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
+    mpf_rounding_mode rm;
+    if (m_util.is_rm(arg1, rm)) {
+        scoped_mpf v2(m_util.fm()), v3(m_util.fm());
+        if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
+            scoped_mpf t(m_util.fm());
+            m_util.fm().add(rm, v2, v3, t);
+            result = m_util.mk_value(t);
+            return BR_DONE;
+        }
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
+    // a - b = a + (-b)
+    result = m_util.mk_add(arg1, arg2, m_util.mk_uminus(arg3));
+    return BR_REWRITE2;
+}
+
+br_status float_rewriter::mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {    
+    mpf_rounding_mode rm;
+    if (m_util.is_rm(arg1, rm)) {
+        scoped_mpf v2(m_util.fm()), v3(m_util.fm());
+        if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
+            scoped_mpf t(m_util.fm());
+            m_util.fm().mul(rm, v2, v3, t);
+            result = m_util.mk_value(t);
+            return BR_DONE;
+        }
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) {
+    mpf_rounding_mode rm;
+    if (m_util.is_rm(arg1, rm)) {
+        scoped_mpf v2(m_util.fm()), v3(m_util.fm());
+        if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3)) {
+            scoped_mpf t(m_util.fm());
+            m_util.fm().div(rm, v2, v3, t);
+            result = m_util.mk_value(t);
+            return BR_DONE;
+        }
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_uminus(expr * arg1, expr_ref & result) {
+    if (m_util.is_nan(arg1)) {
+        // -nan --> nan
+        result = arg1;
+        return BR_DONE;
+    }
+    if (m_util.is_plus_inf(arg1)) {
+        // - +oo --> -oo
+        result = m_util.mk_minus_inf(m().get_sort(arg1));
+        return BR_DONE;
+    }
+    if (m_util.is_minus_inf(arg1)) {
+        // - -oo -> +oo
+        result = m_util.mk_plus_inf(m().get_sort(arg1));
+        return BR_DONE;
+    }
+    if (m_util.is_uminus(arg1)) {
+        // - - a --> a
+        result = to_app(arg1)->get_arg(0);
+        return BR_DONE;
+    }
+    
+    scoped_mpf v1(m_util.fm());
+    if (m_util.is_value(arg1, v1)) {
+        m_util.fm().neg(v1);
+        result = m_util.mk_value(v1);
+        return BR_DONE;
+    }
+
+    // TODO: more simplifications
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_rem(expr * arg1, expr * arg2, expr_ref & result) {
+    scoped_mpf v1(m_util.fm()), v2(m_util.fm());
+    if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) {
+        scoped_mpf t(m_util.fm());
+        m_util.fm().rem(v1, v2, t);
+        result = m_util.mk_value(t);
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_abs(expr * arg1, expr_ref & result) {
+    if (m_util.is_nan(arg1)) {
+        result = arg1;
+        return BR_DONE;
+    }
+    sort * s = m().get_sort(arg1);
+    result = m().mk_ite(m_util.mk_lt(arg1, m_util.mk_pzero(s)),
+                        m_util.mk_uminus(arg1),
+                        arg1);
+    return BR_REWRITE2;
+}
+
+br_status float_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) {
+    if (m_util.is_nan(arg1)) {
+        result = arg2;
+        return BR_DONE;
+    }
+    if (m_util.is_nan(arg2)) {
+        result = arg1;
+        return BR_DONE;
+    }
+    // expand as using ite's
+    result = m().mk_ite(mk_eq_nan(arg1),
+                        arg2,
+                        m().mk_ite(mk_eq_nan(arg2), 
+                                   arg1,
+                                   m().mk_ite(m_util.mk_lt(arg1, arg2),
+                                              arg1,
+                                              arg2)));
+    return BR_REWRITE_FULL;
+}
+
+br_status float_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) {
+    if (m_util.is_nan(arg1)) {
+        result = arg2;
+        return BR_DONE;
+    }
+    if (m_util.is_nan(arg2)) {
+        result = arg1;
+        return BR_DONE;
+    }
+    // expand as using ite's
+    result = m().mk_ite(mk_eq_nan(arg1), 
+                        arg2,
+                        m().mk_ite(mk_eq_nan(arg2), 
+                                   arg1,
+                                   m().mk_ite(m_util.mk_gt(arg1, arg2),
+                                              arg1,
+                                              arg2)));
+    return BR_REWRITE_FULL;
+}
+
+br_status float_rewriter::mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result) {
+    mpf_rounding_mode rm;
+    if (m_util.is_rm(arg1, rm)) {
+        scoped_mpf v2(m_util.fm()), v3(m_util.fm()), v4(m_util.fm());
+        if (m_util.is_value(arg2, v2) && m_util.is_value(arg3, v3) && m_util.is_value(arg4, v4)) {
+            scoped_mpf t(m_util.fm());
+            m_util.fm().fused_mul_add(rm, v2, v3, v4, t);
+            result = m_util.mk_value(t);
+            return BR_DONE;
+        }
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_sqrt(expr * arg1, expr * arg2, expr_ref & result) {
+    mpf_rounding_mode rm;
+    if (m_util.is_rm(arg1, rm)) {
+        scoped_mpf v2(m_util.fm());
+        if (m_util.is_value(arg2, v2)) {
+            scoped_mpf t(m_util.fm());
+            m_util.fm().sqrt(rm, v2, t);
+            result = m_util.mk_value(t);
+            return BR_DONE;
+        }
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_round(expr * arg1, expr * arg2, expr_ref & result) {
+    mpf_rounding_mode rm;
+    if (m_util.is_rm(arg1, rm)) {
+        scoped_mpf v2(m_util.fm());
+        if (m_util.is_value(arg2, v2)) {
+            scoped_mpf t(m_util.fm());
+            m_util.fm().round_to_integral(rm, v2, t);
+            result = m_util.mk_value(t);
+            return BR_DONE;
+        }
+    }
+
+    return BR_FAILED;
+}
+
+// This the floating point theory ==
+br_status float_rewriter::mk_float_eq(expr * arg1, expr * arg2, expr_ref & result) {
+    scoped_mpf v1(m_util.fm()), v2(m_util.fm());
+    if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) {
+        result = (m_util.fm().eq(v1, v2)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+// Return (= arg NaN)
+app * float_rewriter::mk_eq_nan(expr * arg) {
+    return m().mk_eq(arg, m_util.mk_nan(m().get_sort(arg)));
+}
+
+// Return (not (= arg NaN))
+app * float_rewriter::mk_neq_nan(expr * arg) {
+    return m().mk_not(mk_eq_nan(arg));
+}
+
+br_status float_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) {
+    if (m_util.is_nan(arg1) || m_util.is_nan(arg2)) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    if (m_util.is_minus_inf(arg1)) {
+        // -oo < arg2 -->  not(arg2 = -oo) and not(arg2 = NaN)
+        result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2));
+        return BR_REWRITE2;
+    }
+    if (m_util.is_minus_inf(arg2)) {
+        // arg1 < -oo  --> false
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    if (m_util.is_plus_inf(arg1)) {
+        // +oo < arg2 --> false
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    if (m_util.is_plus_inf(arg2)) {
+        // arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN)
+        result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1));
+        return BR_REWRITE2;
+    }
+
+    scoped_mpf v1(m_util.fm()), v2(m_util.fm());
+    if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) {
+        result = (m_util.fm().lt(v1, v2)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    // TODO: more simplifications
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_gt(expr * arg1, expr * arg2, expr_ref & result) {
+    result = m_util.mk_lt(arg2, arg1);
+    return BR_REWRITE1;
+}
+
+br_status float_rewriter::mk_le(expr * arg1, expr * arg2, expr_ref & result) {
+    if (m_util.is_nan(arg1) || m_util.is_nan(arg2)) {
+        result = m().mk_false();
+        return BR_DONE;
+    }
+    scoped_mpf v1(m_util.fm()), v2(m_util.fm());
+    if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) {
+        result = (m_util.fm().le(v1, v2)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_ge(expr * arg1, expr * arg2, expr_ref & result) {
+    result = m_util.mk_le(arg2, arg1);
+    return BR_REWRITE1;
+}
+
+br_status float_rewriter::mk_is_zero(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_zero(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_is_nzero(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_nzero(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_is_pzero(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_pzero(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+br_status float_rewriter::mk_is_sign_minus(expr * arg1, expr_ref & result) {
+    scoped_mpf v(m_util.fm());
+    if (m_util.is_value(arg1, v)) {
+        result = (m_util.fm().is_neg(v)) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}
+
+// This the SMT =
+br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
+    scoped_mpf v1(m_util.fm()), v2(m_util.fm());
+    if (m_util.is_value(arg1, v1) && m_util.is_value(arg2, v2)) {
+        result = (v1 == v2) ? m().mk_true() : m().mk_false();
+        return BR_DONE;
+    }
+
+    return BR_FAILED;
+}

src/rewriter/float_rewriter.h

@@ -0,0 +1,72 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    float_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for floating point numbers.
+
+Author:
+
+    Leonardo (leonardo) 2012-02-02
+
+Notes:
+
+--*/
+#ifndef _FLOAT_REWRITER_H_
+#define _FLOAT_REWRITER_H_
+
+#include"ast.h"
+#include"rewriter.h"
+#include"params.h"
+#include"float_decl_plugin.h"
+#include"mpf.h"
+
+class float_rewriter {
+    float_util    m_util;
+    mpf_manager   m_fm;
+
+    app * mk_eq_nan(expr * arg);
+    app * mk_neq_nan(expr * arg);
+
+public:
+    float_rewriter(ast_manager & m, params_ref const & p = params_ref());
+    ~float_rewriter();
+
+    ast_manager & m() const { return m_util.m(); }
+    family_id get_fid() const { return m_util.get_fid(); }
+    
+    void updt_params(params_ref const & p);
+    static void get_param_descrs(param_descrs & r);
+
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_eq_core(expr * arg1, expr * arg2, expr_ref & result);
+
+    br_status mk_to_float(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_add(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
+    br_status mk_sub(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
+    br_status mk_mul(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
+    br_status mk_div(expr * arg1, expr * arg2, expr * arg3, expr_ref & result);
+    br_status mk_uminus(expr * arg1, expr_ref & result);
+    br_status mk_rem(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_abs(expr * arg1, expr_ref & result);
+    br_status mk_min(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_max(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_fused_ma(expr * arg1, expr * arg2, expr * arg3, expr * arg4, expr_ref & result);
+    br_status mk_sqrt(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_round(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_float_eq(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_lt(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_gt(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_le(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_ge(expr * arg1, expr * arg2, expr_ref & result);
+    br_status mk_is_zero(expr * arg1, expr_ref & result);
+    br_status mk_is_nzero(expr * arg1, expr_ref & result);
+    br_status mk_is_pzero(expr * arg1, expr_ref & result);
+    br_status mk_is_sign_minus(expr * arg1, expr_ref & result);
+};
+
+#endif

src/rewriter/poly_rewriter.h

@@ -0,0 +1,167 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    poly_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for Polynomials.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-08
+
+Notes:
+
+--*/
+#ifndef _POLY_REWRITER_H_
+#define _POLY_REWRITER_H_
+
+#include"ast.h"
+#include"obj_hashtable.h"
+#include"rewriter_types.h"
+#include"params.h"
+
+template<typename Config>
+class poly_rewriter : public Config {
+public:
+    static char const * g_ste_blowup_msg;
+protected:
+    typedef typename Config::numeral numeral; 
+    sort *   m_curr_sort;
+    obj_map<expr, unsigned> m_expr2pos;
+    bool                    m_flat;
+    bool                    m_som;
+    unsigned                m_som_blowup;
+    bool                    m_sort_sums;
+    bool                    m_hoist_mul;
+    bool                    m_hoist_cmul;
+    
+    bool is_numeral(expr * n) const { return Config::is_numeral(n); }
+    bool is_numeral(expr * n, numeral & r) const { return Config::is_numeral(n, r); }
+    bool is_zero(expr * n) const { return Config::is_zero(n); }
+    bool is_minus_one(expr * n) const { return Config::is_minus_one(n); }
+    void normalize(numeral & c) { Config::normalize(c, m_curr_sort); }
+    app * mk_numeral(numeral const & r) { return Config::mk_numeral(r, m_curr_sort); }
+    decl_kind add_decl_kind() const { return Config::add_decl_kind(); }
+    decl_kind mul_decl_kind() const { return Config::mul_decl_kind(); }
+    bool use_power() const { return Config::use_power(); }
+    decl_kind power_decl_kind() const { return Config::power_decl_kind(); }
+    bool is_power(expr * t) const { return is_app_of(t, get_fid(), power_decl_kind()); }
+    expr * get_power_body(expr * t, rational & k);
+    struct mon_pw_lt; // functor used to sort monomial elements when use_power() == true
+
+    expr * mk_mul_app(unsigned num_args, expr * const * args);
+    expr * mk_mul_app(numeral const & c, expr * arg);
+    expr * mk_add_app(unsigned num_args, expr * const * args);
+
+    br_status mk_flat_mul_core(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_nflat_mul_core(unsigned num_args, expr * const * args, expr_ref & result);
+
+    expr * get_power_product(expr * t);
+    expr * get_power_product(expr * t, numeral & a);
+
+    br_status mk_flat_add_core(unsigned num_args, expr * const * args, expr_ref & result);
+    br_status mk_nflat_add_core(unsigned num_args, expr * const * args, expr_ref & result);
+
+    void set_curr_sort(sort * s) { m_curr_sort = s; }
+
+    expr * const * get_monomials(expr * & t, unsigned & sz) {
+        if (is_add(t)) {
+            sz = to_app(t)->get_num_args();
+            return to_app(t)->get_args();
+        }
+        else {
+            sz = 1;
+            return &t;
+        }
+    }
+
+    br_status cancel_monomials(expr * lhs, expr * rhs, bool move, expr_ref & lhs_result, expr_ref & rhs_result);
+
+    bool hoist_multiplication(expr_ref& som);
+    expr* merge_muls(expr* x, expr* y);
+
+    struct hoist_cmul_lt;
+    bool is_mul(expr * t, numeral & c, expr * & pp);
+    void hoist_cmul(expr_ref_buffer & args);
+    
+public:
+    poly_rewriter(ast_manager & m, params_ref const & p = params_ref()):
+        Config(m), 
+        m_curr_sort(0),
+        m_sort_sums(false) {
+        updt_params(p);
+        SASSERT(!m_som || m_flat); // som of monomials form requires flattening to be enabled.
+        SASSERT(!m_som || !m_hoist_mul); // som is mutually exclusive with hoisting multiplication.
+        updt_params(p);
+    }
+
+    ast_manager & m() const { return Config::m(); }
+    family_id get_fid() const { return Config::get_fid(); }
+
+    void updt_params(params_ref const & p);
+    static void get_param_descrs(param_descrs & r);
+
+    void set_flat(bool f) { m_flat = f; }
+
+    void set_sort_sums(bool f) { m_sort_sums = f; }
+
+    bool is_add(expr * n) const { return is_app_of(n, get_fid(), add_decl_kind()); }
+    bool is_mul(expr * n) const { return is_app_of(n, get_fid(), mul_decl_kind()); }
+    bool is_add(func_decl * f) const { return is_decl_of(f, get_fid(), add_decl_kind()); }
+    bool is_mul(func_decl * f) const { return is_decl_of(f, get_fid(), mul_decl_kind()); }
+
+    br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
+        SASSERT(num_args > 0);
+        if (num_args == 1) {
+            result = args[0];
+            return BR_DONE;
+        }
+        set_curr_sort(m().get_sort(args[0]));
+        return m_flat ?
+            mk_flat_mul_core(num_args, args, result) :
+            mk_nflat_mul_core(num_args, args, result);
+    }
+    br_status mk_add_core(unsigned num_args, expr * const * args, expr_ref & result) {
+        SASSERT(num_args > 0);
+        if (num_args == 1) {
+            result = args[0];
+            return BR_DONE;
+        }
+        set_curr_sort(m().get_sort(args[0]));
+        return m_flat ?
+            mk_flat_add_core(num_args, args, result) :
+            mk_nflat_add_core(num_args, args, result);
+    }
+    void mk_add(unsigned num_args, expr * const * args, expr_ref & result) {
+        if (mk_add_core(num_args, args, result) == BR_FAILED)
+            result = mk_add_app(num_args, args);
+    }
+    void mk_add(expr* a1, expr* a2, expr_ref& result) {
+        expr* args[2] = { a1, a2 };
+        mk_add(2, args, result);
+    }
+
+    void mk_mul(unsigned num_args, expr * const * args, expr_ref & result) {
+        if (mk_mul_core(num_args, args, result) == BR_FAILED)
+            result = mk_mul_app(num_args, args);
+    }
+    void mk_mul(expr* a1, expr* a2, expr_ref& result) {
+        expr* args[2] = { a1, a2 };
+        mk_mul(2, args, result);
+    }
+    // The result of the following functions is never BR_FAILED
+    br_status mk_uminus(expr * arg, expr_ref & result);
+    br_status mk_sub(unsigned num_args, expr * const * args, expr_ref & result);
+    
+    void mk_sub(expr* a1, expr* a2, expr_ref& result) {
+        expr* args[2] = { a1, a2 };
+        mk_sub(2, args, result);
+    }
+};
+
+
+#endif

src/rewriter/poly_rewriter_def.h

@@ -0,0 +1,933 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    poly_rewriter_def.h
+
+Abstract:
+
+    Basic rewriting rules for Polynomials.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-08
+
+Notes:
+
+--*/
+#include"poly_rewriter.h"
+#include"ast_lt.h"
+#include"ast_ll_pp.h"
+#include"ast_smt2_pp.h"
+
+template<typename Config>
+char const * poly_rewriter<Config>::g_ste_blowup_msg = "sum of monomials blowup";
+
+
+template<typename Config>
+void poly_rewriter<Config>::updt_params(params_ref const & p) {
+    m_flat = p.get_bool(":flat", true);
+    m_som  = p.get_bool(":som", false);
+    m_hoist_mul = p.get_bool(":hoist-mul", false);
+    m_hoist_cmul = p.get_bool(":hoist-cmul", false);
+    m_som_blowup = p.get_uint(":som-blowup", UINT_MAX);
+}
+
+template<typename Config>
+void poly_rewriter<Config>::get_param_descrs(param_descrs & r) {
+    r.insert(":som", CPK_BOOL, "(default: false) put polynomials in som-of-monomials form.");
+    r.insert(":som-blowup", CPK_UINT, "(default: infty) maximum number of monomials generated when putting a polynomial in sum-of-monomials normal form");
+    r.insert(":hoist-mul", CPK_BOOL, "(default: false) hoist multiplication over summation to minimize number of multiplications");
+    r.insert(":hoist-cmul", CPK_BOOL, "(default: false) hoist constant multiplication over summation to minimize number of multiplications");
+}
+
+template<typename Config>
+expr * poly_rewriter<Config>::mk_add_app(unsigned num_args, expr * const * args) { 
+    switch (num_args) {
+    case 0: return mk_numeral(numeral(0));
+    case 1: return args[0];
+    default: return m().mk_app(get_fid(), add_decl_kind(), num_args, args);
+    }
+}
+
+// t = (^ x y)  --> return x, and set k = y  if k is an integer >= 1
+// Otherwise return t and set k = 1
+template<typename Config>
+expr * poly_rewriter<Config>::get_power_body(expr * t, rational & k) {
+    if (!is_power(t)) {
+        k = rational(1);
+        return t;
+    }
+    if (is_numeral(to_app(t)->get_arg(1), k) && k.is_int() && k > rational(1)) {
+        return to_app(t)->get_arg(0);
+    }
+    k = rational(1);
+    return t;
+}
+
+template<typename Config>
+expr * poly_rewriter<Config>::mk_mul_app(unsigned num_args, expr * const * args) { 
+    switch (num_args) {
+    case 0: 
+        return mk_numeral(numeral(1));
+    case 1: 
+        return args[0];
+    default: 
+        if (use_power()) {
+            rational k_prev;
+            expr * prev = get_power_body(args[0], k_prev);
+            rational k;
+            ptr_buffer<expr> new_args;
+#define PUSH_POWER() {                                                                          \
+                if (k_prev.is_one()) {                                                          \
+                    new_args.push_back(prev);                                                   \
+                }                                                                               \
+                else {                                                                          \
+                    expr * pargs[2] = { prev, mk_numeral(k_prev) };                             \
+                    new_args.push_back(m().mk_app(get_fid(), power_decl_kind(), 2, pargs));     \
+                }                                                                               \
+            }
+ 
+            for (unsigned i = 1; i < num_args; i++) {
+                expr * arg = get_power_body(args[i], k);
+                if (arg == prev) {
+                    k_prev += k;
+                }
+                else {
+                    PUSH_POWER();
+                    prev   = arg;
+                    k_prev = k;
+                }
+            }
+            PUSH_POWER();
+            SASSERT(new_args.size() > 0);
+            if (new_args.size() == 1) {
+                return new_args[0];
+            }
+            else {
+                return m().mk_app(get_fid(), mul_decl_kind(), new_args.size(), new_args.c_ptr());
+            }
+        }
+        else {
+            return m().mk_app(get_fid(), mul_decl_kind(), num_args, args);
+        }
+    }
+}
+
+template<typename Config>
+expr * poly_rewriter<Config>::mk_mul_app(numeral const & c, expr * arg) {
+    if (c.is_one()) {
+        return arg;
+    }
+    else {
+        expr * new_args[2] = { mk_numeral(c), arg };
+        return mk_mul_app(2, new_args); 
+    }
+}
+
+template<typename Config>
+br_status poly_rewriter<Config>::mk_flat_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args >= 2);
+    // only try to apply flattening if it is not already in one of the flat monomial forms
+    // - (* c x)
+    // - (* c (* x_1 ... x_n))
+    if (num_args != 2 || !is_numeral(args[0]) || (is_mul(args[1]) && is_numeral(to_app(args[1])->get_arg(0)))) {
+        unsigned i;
+        for (i = 0; i < num_args; i++) {
+            if (is_mul(args[i]))
+                break;
+        }
+        if (i < num_args) {
+            // input has nested monomials. 
+            ptr_buffer<expr> flat_args;
+            // we need the todo buffer to handle: (* (* c (* x_1 ... x_n)) (* d (* y_1 ... y_n)))
+            ptr_buffer<expr> todo;
+            flat_args.append(i, args);
+            for (unsigned j = i; j < num_args; j++) {
+                if (is_mul(args[j])) {
+                    todo.push_back(args[j]);
+                    while (!todo.empty()) {
+                        expr * curr = todo.back();
+                        todo.pop_back();
+                        if (is_mul(curr)) {
+                            unsigned k = to_app(curr)->get_num_args();
+                            while (k > 0) {
+                                --k;
+                                todo.push_back(to_app(curr)->get_arg(k));
+                            }
+                        }
+                        else {
+                            flat_args.push_back(curr);
+                        }
+                    }
+                }
+                else {
+                    flat_args.push_back(args[j]);
+                }
+            }
+            TRACE("poly_rewriter",
+                  tout << "flat mul:\n";
+                  for (unsigned i = 0; i < num_args; i++) tout << mk_bounded_pp(args[i], m()) << "\n";
+                  tout << "---->\n";
+                  for (unsigned i = 0; i < flat_args.size(); i++) tout << mk_bounded_pp(flat_args[i], m()) << "\n";);
+            br_status st = mk_nflat_mul_core(flat_args.size(), flat_args.c_ptr(), result);
+            if (st == BR_FAILED) {
+                result = mk_mul_app(flat_args.size(), flat_args.c_ptr());
+                return BR_DONE;
+            }
+            return st;
+        }
+    }
+    return mk_nflat_mul_core(num_args, args, result);    
+}
+
+
+template<typename Config>
+struct poly_rewriter<Config>::mon_pw_lt {
+    poly_rewriter<Config> & m_owner;
+    mon_pw_lt(poly_rewriter<Config> & o):m_owner(o) {}
+    
+    bool operator()(expr * n1, expr * n2) const { 
+        rational k;
+        return lt(m_owner.get_power_body(n1, k), 
+                  m_owner.get_power_body(n2, k));
+    }
+};
+
+
+template<typename Config>
+br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args >= 2);
+    // cheap case
+    numeral a;
+    if (num_args == 2 && is_numeral(args[0], a) && !a.is_one() && !a.is_zero() && 
+        (is_var(args[1]) || to_app(args[1])->get_decl()->get_family_id() != get_fid())) 
+        return BR_FAILED;
+    numeral c(1);
+    unsigned num_coeffs = 0;
+    unsigned num_add    = 0;
+    expr *  var         = 0;
+    for (unsigned i = 0; i < num_args; i++) {
+        expr * arg = args[i];
+        if (is_numeral(arg, a)) {
+            num_coeffs++;
+            c *= a;
+        }
+        else {
+            var = arg;
+            if (is_add(arg))
+                num_add++;
+        }
+    }
+    
+    normalize(c);
+    // (* c_1 ... c_n) --> c_1*...*c_n
+    if (num_coeffs == num_args) {
+        result = mk_numeral(c);
+        return BR_DONE;
+    }
+
+    // (* s ... 0 ... r) --> 0
+    if (c.is_zero()) {
+        result = mk_numeral(c);
+        return BR_DONE;
+    }
+
+    if (num_coeffs == num_args - 1) {
+        SASSERT(var != 0);
+        // (* c_1 ... c_n x) --> x  if c_1*...*c_n == 1
+        if (c.is_one()) {
+            result = var;
+            return BR_DONE;
+        }
+
+        numeral c_prime;
+        if (is_mul(var)) {
+            // apply basic simplification even when flattening is not enabled.
+            // (* c1 (* c2 x)) --> (* c1*c2 x)
+            if (to_app(var)->get_num_args() == 2 && is_numeral(to_app(var)->get_arg(0), c_prime)) {
+                c *= c_prime;
+                normalize(c);
+                result = mk_mul_app(c, to_app(var)->get_arg(1));
+                return BR_REWRITE1;
+            }
+            else {
+                // var is a power-product
+                return BR_FAILED;
+            }
+        }
+        
+        if (num_add == 0 || m_hoist_cmul) {
+            SASSERT(!is_add(var) || m_hoist_cmul);
+            if (num_args == 2 && args[1] == var) {
+                DEBUG_CODE({ 
+                    numeral c_prime;
+                    SASSERT(is_numeral(args[0], c_prime) && c == c_prime);
+                });
+                // it is already simplified
+                return BR_FAILED;
+            }
+            
+            // (* c_1 ... c_n x) --> (* c_1*...*c_n x)
+            result = mk_mul_app(c, var);
+            return BR_DONE;
+        }
+        else {
+            SASSERT(is_add(var));
+            // (* c_1 ... c_n (+ t_1 ... t_m)) --> (+ (* c_1*...*c_n t_1) ... (* c_1*...*c_n t_m))
+            ptr_buffer<expr> new_add_args;
+            unsigned num = to_app(var)->get_num_args();
+            for (unsigned i = 0; i < num; i++) {
+                new_add_args.push_back(mk_mul_app(c, to_app(var)->get_arg(i)));
+            }
+            result = mk_add_app(new_add_args.size(), new_add_args.c_ptr());
+            TRACE("mul_bug", tout << "result: " << mk_bounded_pp(result, m(),5) << "\n";);
+            return BR_REWRITE2;
+        }
+    }
+
+    SASSERT(num_coeffs <= num_args - 2);
+
+    if (!m_som || num_add == 0) {
+        ptr_buffer<expr> new_args;
+        expr * prev = 0;
+        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))
+                ordered = false;
+            new_args.push_back(curr);
+            prev = curr;
+        }
+        TRACE("poly_rewriter", 
+              for (unsigned i = 0; i < new_args.size(); i++) {
+                  if (i > 0)
+                      tout << (lt(new_args[i-1], new_args[i]) ? " < " : " !< ");
+                  tout << mk_ismt2_pp(new_args[i], m());
+              }
+              tout << "\nordered: " << ordered << "\n";);
+        if (ordered && num_coeffs == 0 && !use_power())
+            return BR_FAILED;
+        if (!ordered) {
+            if (use_power())
+                std::sort(new_args.begin(), new_args.end(), mon_pw_lt(*this));
+            else
+                std::sort(new_args.begin(), new_args.end(), ast_to_lt());
+            TRACE("poly_rewriter",
+                  tout << "after sorting:\n";
+                  for (unsigned i = 0; i < new_args.size(); i++) {
+                      if (i > 0)
+                          tout << (lt(new_args[i-1], new_args[i]) ? " < " : " !< ");
+                      tout << mk_ismt2_pp(new_args[i], m());
+                  }
+                  tout << "\n";);
+        }
+        SASSERT(new_args.size() >= 2);
+        result = mk_mul_app(new_args.size(), new_args.c_ptr());
+        result = mk_mul_app(c, result);
+        TRACE("poly_rewriter", tout << "mk_nflat_mul_core result:\n" << mk_ismt2_pp(result, m()) << "\n";);
+        return BR_DONE;
+    }
+
+    SASSERT(m_som && num_add > 0);
+
+    sbuffer<unsigned> szs;
+    sbuffer<unsigned> it;
+    sbuffer<expr **> sums;
+    for (unsigned i = 0; i < num_args; i ++) {
+        it.push_back(0);
+        expr * arg  = args[i];
+        if (is_add(arg)) {
+            sums.push_back(const_cast<expr**>(to_app(arg)->get_args()));
+            szs.push_back(to_app(arg)->get_num_args());
+        }
+        else {
+            sums.push_back(const_cast<expr**>(args + i));
+            szs.push_back(1);
+            SASSERT(sums.back()[0] == arg);
+        }
+    }
+    expr_ref_buffer sum(m()); // must be ref_buffer because we may throw an exception
+    ptr_buffer<expr> m_args;
+    TRACE("som", tout << "starting som...\n";);
+    do {
+        TRACE("som", for (unsigned i = 0; i < it.size(); i++) tout << it[i] << " ";
+              tout << "\n";);
+        if (sum.size() > m_som_blowup)
+            throw rewriter_exception(g_ste_blowup_msg);
+        m_args.reset();
+        for (unsigned i = 0; i < num_args; i++) {
+            expr * const * v = sums[i];
+            expr * arg       = v[it[i]];
+            m_args.push_back(arg);
+        }
+        sum.push_back(mk_mul_app(m_args.size(), m_args.c_ptr()));
+    }
+    while (product_iterator_next(szs.size(), szs.c_ptr(), it.c_ptr()));
+    result = mk_add_app(sum.size(), sum.c_ptr());
+    return BR_REWRITE2;
+}
+
+template<typename Config>
+br_status poly_rewriter<Config>::mk_flat_add_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    unsigned i;
+    for (i = 0; i < num_args; i++) {
+        if (is_add(args[i]))
+            break;
+    }
+    if (i < num_args) {
+        // has nested ADDs
+        ptr_buffer<expr> flat_args;
+        flat_args.append(i, args);
+        for (; i < num_args; i++) {
+            expr * arg = args[i];
+            // Remark: all rewrites are depth 1.
+            if (is_add(arg)) {
+                unsigned num = to_app(arg)->get_num_args();
+                for (unsigned j = 0; j < num; j++)
+                    flat_args.push_back(to_app(arg)->get_arg(j));
+            }
+            else {
+                flat_args.push_back(arg);
+            }
+        }
+        br_status st = mk_nflat_add_core(flat_args.size(), flat_args.c_ptr(), result);
+        if (st == BR_FAILED) {
+            result = mk_add_app(flat_args.size(), flat_args.c_ptr());
+            return BR_DONE;
+        }
+        return st;
+    }
+    return mk_nflat_add_core(num_args, args, result);
+}
+
+template<typename Config>
+inline expr * poly_rewriter<Config>::get_power_product(expr * t) {
+    if (is_mul(t) && to_app(t)->get_num_args() == 2 && is_numeral(to_app(t)->get_arg(0)))
+        return to_app(t)->get_arg(1);
+    return t;
+}
+
+template<typename Config>
+inline expr * poly_rewriter<Config>::get_power_product(expr * t, numeral & a) {
+    if (is_mul(t) && to_app(t)->get_num_args() == 2 && is_numeral(to_app(t)->get_arg(0), a))
+        return to_app(t)->get_arg(1);
+    a = numeral(1);
+    return t;
+}
+
+template<typename Config>
+bool poly_rewriter<Config>::is_mul(expr * t, numeral & c, expr * & pp) {
+    if (!is_mul(t) || to_app(t)->get_num_args() != 2)
+        return false;
+    if (!is_numeral(to_app(t)->get_arg(0), c))
+        return false;
+    pp = to_app(t)->get_arg(1);
+    return true;
+}
+
+template<typename Config>
+struct poly_rewriter<Config>::hoist_cmul_lt {
+    poly_rewriter<Config> & m_r;
+    hoist_cmul_lt(poly_rewriter<Config> & r):m_r(r) {}
+
+    bool operator()(expr * t1, expr * t2) const {
+        expr * pp1, * pp2;
+        numeral c1, c2;
+        bool is_mul1 = m_r.is_mul(t1, c1, pp1);
+        bool is_mul2 = m_r.is_mul(t2, c2, pp2);
+        if (!is_mul1 && is_mul2)
+            return true;
+        if (is_mul1 && !is_mul2)
+            return false;
+        if (!is_mul1 && !is_mul2)
+            return t1->get_id() < t2->get_id();
+        if (c1 < c2)
+            return true;
+        if (c1 > c2)
+            return false;
+        return pp1->get_id() < pp2->get_id();
+    }
+};
+
+template<typename Config>
+void poly_rewriter<Config>::hoist_cmul(expr_ref_buffer & args) {
+    unsigned sz = args.size();
+    std::sort(args.c_ptr(), args.c_ptr() + sz, hoist_cmul_lt(*this));
+    numeral c, c_prime;
+    ptr_buffer<expr> pps;
+    expr * pp, * pp_prime;
+    unsigned j = 0;
+    unsigned i = 0;
+    while (i < sz) {
+        expr * mon = args[i];
+        if (is_mul(mon, c, pp) && i < sz - 1) {
+            expr * mon_prime = args[i+1];
+            if (is_mul(mon_prime, c_prime, pp_prime) && c == c_prime) {
+                // found target
+                pps.reset();
+                pps.push_back(pp);
+                pps.push_back(pp_prime);
+                i += 2;
+                while (i < sz && is_mul(args[i], c_prime, pp_prime) && c == c_prime) {
+                    pps.push_back(pp_prime);
+                    i++;
+                }
+                SASSERT(is_numeral(to_app(mon)->get_arg(0), c_prime) && c == c_prime);
+                expr * mul_args[2] = { to_app(mon)->get_arg(0), mk_add_app(pps.size(), pps.c_ptr()) };
+                args.set(j, mk_mul_app(2, mul_args));
+                j++;
+                continue;
+            }
+        }
+        args.set(j, mon);
+        j++;
+        i++;
+    }
+    args.resize(j);
+}
+
+template<typename Config>
+br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args >= 2);
+    numeral c;
+    unsigned num_coeffs = 0;
+    numeral a;
+    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;
+    bool     ordered      = true;
+    for (unsigned i = 0; i < num_args; i++) {
+        expr * arg = args[i];
+        if (is_numeral(arg, a)) {
+            num_coeffs++;
+            c += a;
+        }
+        else {
+            // arg is not a numeral
+            if (m_sort_sums && ordered) {
+                if (prev != 0 && lt(arg, prev))
+                    ordered = false;
+                prev = arg;
+            }
+        }
+
+        arg = get_power_product(arg);
+        if (visited.is_marked(arg)) {
+            multiple.mark(arg);
+            has_multiple = true;
+        }
+        else {
+            visited.mark(arg);
+        }
+    }
+    normalize(c);
+    SASSERT(m_sort_sums || ordered);
+    TRACE("sort_sums", 
+          tout << "ordered: " << ordered << "\n";
+          for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";);
+
+    if (has_multiple) {
+        // expensive case
+        buffer<numeral>  coeffs;
+        m_expr2pos.reset();
+        // compute the coefficient of power products that occur multiple times.
+        for (unsigned i = 0; i < num_args; i++) {
+            expr * arg = args[i];
+            if (is_numeral(arg))
+                continue;
+            expr * pp = get_power_product(arg, a);
+            if (!multiple.is_marked(pp))
+                continue;
+            unsigned pos;
+            if (m_expr2pos.find(pp, pos)) {
+                coeffs[pos] += a;
+            }
+            else {
+                m_expr2pos.insert(pp, coeffs.size());
+                coeffs.push_back(a);
+            }
+        }
+        expr_ref_buffer new_args(m());
+        if (!c.is_zero()) {
+            new_args.push_back(mk_numeral(c));
+        }
+        // copy power products with non zero coefficients to new_args
+        visited.reset();
+        for (unsigned i = 0; i < num_args; i++) {
+            expr * arg = args[i];
+            if (is_numeral(arg))
+                continue;
+            expr * pp = get_power_product(arg);
+            if (!multiple.is_marked(pp)) {
+                new_args.push_back(arg);
+            }
+            else if (!visited.is_marked(pp)) {
+                visited.mark(pp);
+                unsigned pos = UINT_MAX;
+                m_expr2pos.find(pp, pos);
+                SASSERT(pos != UINT_MAX);
+                a = coeffs[pos];
+                normalize(a);
+                if (!a.is_zero()) 
+                    new_args.push_back(mk_mul_app(a, pp));
+            }
+        }
+        if (m_hoist_cmul) {
+            hoist_cmul(new_args);
+        }
+        else if (m_sort_sums) {
+            TRACE("sort_sums_bug", tout << "new_args.size(): " << new_args.size() << "\n";);
+            if (c.is_zero())
+                std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt());
+            else
+                std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt());
+        }
+        result = mk_add_app(new_args.size(), new_args.c_ptr());
+        if (hoist_multiplication(result)) {
+            return BR_REWRITE_FULL;
+        }
+        return BR_DONE;
+    }
+    else {
+        SASSERT(!has_multiple);
+        if (ordered && !m_hoist_mul && !m_hoist_cmul) {
+            if (num_coeffs == 0)
+                return BR_FAILED; 
+            if (num_coeffs == 1 && is_numeral(args[0], a) && !a.is_zero())
+                return BR_FAILED;
+        }
+        expr_ref_buffer new_args(m());
+        if (!c.is_zero())
+            new_args.push_back(mk_numeral(c));
+        for (unsigned i = 0; i < num_args; i++) {
+            expr * arg = args[i];
+            if (is_numeral(arg))
+                continue;
+            new_args.push_back(arg);
+        }
+        if (m_hoist_cmul) {
+            hoist_cmul(new_args);
+        }
+        else if (!ordered) {
+            if (c.is_zero())
+                std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt());
+            else 
+                std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt());
+        }
+        result = mk_add_app(new_args.size(), new_args.c_ptr());        
+        if (hoist_multiplication(result)) {
+            return BR_REWRITE_FULL;
+        }
+        return BR_DONE;
+    }
+}
+
+
+template<typename Config>
+br_status poly_rewriter<Config>::mk_uminus(expr * arg, expr_ref & result) {
+    numeral a;
+    set_curr_sort(m().get_sort(arg));
+    if (is_numeral(arg, a)) {
+        a.neg();
+        normalize(a);
+        result = mk_numeral(a);
+        return BR_DONE;
+    }
+    else {
+        result = mk_mul_app(numeral(-1), arg);
+        return BR_REWRITE1;
+    }
+}
+
+template<typename Config>
+br_status poly_rewriter<Config>::mk_sub(unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(num_args > 0);
+    if (num_args == 1) {
+        result = args[0];
+        return BR_DONE;
+    }
+    set_curr_sort(m().get_sort(args[0]));
+    expr * minus_one = mk_numeral(numeral(-1));
+    ptr_buffer<expr> new_args;
+    new_args.push_back(args[0]);
+    for (unsigned i = 1; i < num_args; i++) {
+        expr * aux_args[2] = { minus_one, args[i] };
+        new_args.push_back(mk_mul_app(2, aux_args));
+    }
+    result = mk_add_app(new_args.size(), new_args.c_ptr());
+    return BR_REWRITE2;
+}
+
+/**
+   \brief Cancel/Combine monomials that occur is the left and right hand sides.
+   
+   \remark If move = true, then all non-constant monomials are moved to the left-hand-side.
+*/
+template<typename Config>
+br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool move, expr_ref & lhs_result, expr_ref & rhs_result) {
+    set_curr_sort(m().get_sort(lhs));
+    unsigned lhs_sz;
+    expr * const * lhs_monomials = get_monomials(lhs, lhs_sz);
+    unsigned rhs_sz;
+    expr * const * rhs_monomials = get_monomials(rhs, rhs_sz);
+
+    expr_fast_mark1 visited;  // visited.is_marked(power_product) if the power_product occurs in lhs or rhs
+    expr_fast_mark2 multiple; // multiple.is_marked(power_product) if power_product occurs more than once
+    bool     has_multiple = false;
+
+    numeral c(0);
+    numeral a;
+    unsigned num_coeffs = 0;
+
+    for (unsigned i = 0; i < lhs_sz; i++) {
+        expr * arg = lhs_monomials[i];
+        if (is_numeral(arg, a)) {
+            c += a;
+            num_coeffs++;
+        }
+        else {
+            visited.mark(get_power_product(arg));
+        }
+    }
+
+    if (move && num_coeffs == 0 && is_numeral(rhs))
+        return BR_FAILED;
+
+    for (unsigned i = 0; i < rhs_sz; i++) {
+        expr * arg = rhs_monomials[i];
+        if (is_numeral(arg, a)) {
+            c -= a;
+            num_coeffs++;
+        }
+        else {
+            expr * pp = get_power_product(arg);
+            if (visited.is_marked(pp)) {
+                multiple.mark(pp);
+                has_multiple = true;
+            }
+        }
+    }
+
+    normalize(c);
+    
+    if (!has_multiple && num_coeffs <= 1) {
+        if (move) {
+            if (is_numeral(rhs))
+                return BR_FAILED;
+        }
+        else {
+            if (num_coeffs == 0 || is_numeral(rhs))
+                return BR_FAILED;
+        }
+    }
+    
+    buffer<numeral>  coeffs;
+    m_expr2pos.reset();
+    for (unsigned i = 0; i < lhs_sz; i++) {
+        expr * arg = lhs_monomials[i];
+        if (is_numeral(arg))
+            continue;
+        expr * pp = get_power_product(arg, a);
+        if (!multiple.is_marked(pp))
+            continue;
+        unsigned pos;
+        if (m_expr2pos.find(pp, pos)) {
+            coeffs[pos] += a;
+        }
+        else {
+            m_expr2pos.insert(pp, coeffs.size());
+            coeffs.push_back(a);
+        }
+    }
+
+    for (unsigned i = 0; i < rhs_sz; i++) {
+        expr * arg = rhs_monomials[i];
+        if (is_numeral(arg))
+            continue;
+        expr * pp = get_power_product(arg, a);
+        if (!multiple.is_marked(pp))
+            continue;
+        unsigned pos = UINT_MAX;
+        m_expr2pos.find(pp, pos);
+        SASSERT(pos != UINT_MAX);
+        coeffs[pos] -= a;
+    }
+
+
+    ptr_buffer<expr> new_lhs_monomials;
+    new_lhs_monomials.push_back(0); // save space for coefficient if needed
+    // copy power products with non zero coefficients to new_lhs_monomials
+    visited.reset();
+    for (unsigned i = 0; i < lhs_sz; i++) {
+        expr * arg = lhs_monomials[i];
+        if (is_numeral(arg))
+            continue;
+        expr * pp = get_power_product(arg);
+        if (!multiple.is_marked(pp)) {
+            new_lhs_monomials.push_back(arg);
+        }
+        else if (!visited.is_marked(pp)) {
+            visited.mark(pp);
+            unsigned pos = UINT_MAX;
+            m_expr2pos.find(pp, pos);
+            SASSERT(pos != UINT_MAX);
+            a = coeffs[pos];
+            if (!a.is_zero())
+                new_lhs_monomials.push_back(mk_mul_app(a, pp));
+        }
+    }
+    
+    ptr_buffer<expr> new_rhs_monomials;
+    new_rhs_monomials.push_back(0); // save space for coefficient if needed
+    for (unsigned i = 0; i < rhs_sz; i++) {
+        expr * arg = rhs_monomials[i];
+        if (is_numeral(arg))
+            continue;
+        expr * pp = get_power_product(arg, a);
+        if (!multiple.is_marked(pp)) {
+            if (move) {
+                if (!a.is_zero()) {
+                    if (a.is_minus_one()) {
+                        new_lhs_monomials.push_back(pp);
+                    }
+                    else {
+                        a.neg();
+                        SASSERT(!a.is_one());
+                        expr * args[2] = { mk_numeral(a), pp };
+                        new_lhs_monomials.push_back(mk_mul_app(2, args));
+                    }
+                }
+            }
+            else {
+                new_rhs_monomials.push_back(arg);
+            }
+        }
+    }
+
+    bool c_at_rhs = false;
+    if (move) {
+        if (m_sort_sums) { 
+            // + 1 to skip coefficient
+            std::sort(new_lhs_monomials.begin() + 1, new_lhs_monomials.end(), ast_to_lt());
+        }
+        c_at_rhs = true;
+    }
+    else if (new_rhs_monomials.size() == 1) { // rhs is empty
+        c_at_rhs = true;
+    }
+    else if (new_lhs_monomials.size() > 1) {
+        c_at_rhs = true;
+    }
+
+    if (c_at_rhs) {
+        c.neg();
+        normalize(c);
+        new_rhs_monomials[0] = mk_numeral(c);
+        lhs_result = mk_add_app(new_lhs_monomials.size() - 1, new_lhs_monomials.c_ptr() + 1);
+        rhs_result = mk_add_app(new_rhs_monomials.size(), new_rhs_monomials.c_ptr());
+    }
+    else {
+        new_lhs_monomials[0] = mk_numeral(c);
+        lhs_result = mk_add_app(new_lhs_monomials.size(), new_lhs_monomials.c_ptr());
+        rhs_result = mk_add_app(new_rhs_monomials.size() - 1, new_rhs_monomials.c_ptr() + 1);
+    }
+    return BR_DONE;
+}
+
+#define TO_BUFFER(_tester_, _buffer_, _e_)                       \
+    _buffer_.push_back(_e_);                                     \
+    for (unsigned _i = 0; _i < _buffer_.size(); ) {                \
+        expr* _e = _buffer_[_i];                                  \
+        if (_tester_(_e)) {                                      \
+            app* a = to_app(_e);                                 \
+            _buffer_[_i] = a->get_arg(0);                        \
+            for (unsigned _j = 1; _j < a->get_num_args(); ++_j) {       \
+                _buffer_.push_back(a->get_arg(_j));                    \
+            }                                                   \
+        }                                                       \
+        else {                                                  \
+            ++_i;                                                \
+        }                                                       \
+    }                                                           \
+
+template<typename Config>
+bool poly_rewriter<Config>::hoist_multiplication(expr_ref& som) {
+    if (!m_hoist_mul) {
+        return false;
+    }
+    ptr_buffer<expr> adds, muls;
+    TO_BUFFER(is_add, adds, som);
+    buffer<bool> valid(adds.size(), true);
+    obj_map<expr, unsigned> mul_map;
+    unsigned j;
+    bool change = false;
+    for (unsigned k = 0; k < adds.size(); ++k) {
+        expr* e = adds[k];
+        muls.reset();
+        TO_BUFFER(is_mul, muls, e);
+        for (unsigned i = 0; i < muls.size(); ++i) {
+            e = muls[i];
+            if (is_numeral(e)) {
+                continue;
+            }
+            if (mul_map.find(e, j) && valid[j] && j != k) {
+                m_curr_sort = m().get_sort(adds[k]);
+                adds[j]  = merge_muls(adds[j], adds[k]);
+                adds[k]  = mk_numeral(rational(0)); 
+                valid[j] = false;
+                valid[k] = false;
+                change = true;
+                break;
+            }
+            else {
+                mul_map.insert(e, k);
+            }
+        }
+    }
+    if (!change) {
+        return false;
+    }
+    
+    som = mk_add_app(adds.size(), adds.c_ptr());
+    
+       
+    return true;
+}
+
+template<typename Config>
+expr* poly_rewriter<Config>::merge_muls(expr* x, expr* y) {
+    ptr_buffer<expr> m1, m2;
+    TO_BUFFER(is_mul, m1, x);
+    TO_BUFFER(is_mul, m2, y);
+    unsigned k = 0;
+    for (unsigned i = 0; i < m1.size(); ++i) {
+        x = m1[i];
+        bool found = false;
+        unsigned j;
+        for (j = k; j < m2.size(); ++j) {
+            found = m2[j] == x;
+            if (found) break;
+        }
+        if (found) {
+            std::swap(m1[i],m1[k]);
+            std::swap(m2[j],m2[k]);
+            ++k;
+        }
+    }
+    m_curr_sort = m().get_sort(x);
+    SASSERT(k > 0);
+    SASSERT(m1.size() >= k); 
+    SASSERT(m2.size() >= k);
+    expr* args[2] = { mk_mul_app(m1.size()-k, m1.c_ptr()+k), 
+                      mk_mul_app(m2.size()-k, m2.c_ptr()+k) };
+    if (k == m1.size()) {
+        m1.push_back(0);
+    }
+    m1[k] = mk_add_app(2, args);
+    return mk_mul_app(k+1, m1.c_ptr());
+}

src/rewriter/rewriter.cpp

@@ -0,0 +1,402 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    rewriter.cpp
+
+Abstract:
+
+    Lean and mean rewriter
+
+Author:
+
+    Leonardo (leonardo) 2011-03-31
+
+Notes:
+
+--*/
+#include"rewriter_def.h"
+#include"ast_ll_pp.h"
+#include"ast_smt2_pp.h"
+
+void rewriter_core::init_cache_stack() {
+    SASSERT(m_cache_stack.empty());
+    m_cache = alloc(cache, m());
+    m_cache_stack.push_back(m_cache);
+    if (m_proof_gen) {
+        SASSERT(m_cache_pr_stack.empty());
+        m_cache_pr = alloc(cache, m());
+        m_cache_pr_stack.push_back(m_cache_pr);
+    }
+}
+
+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;
+    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;
+    }
+}
+
+void rewriter_core::cache_result(expr * k, expr * v) {
+#if 0
+    // trace for tracking cache usage
+    verbose_stream() << "1 " << k->get_id() << std::endl;
+#endif
+    SASSERT(!m_proof_gen);
+    
+    TRACE("rewriter_cache_result", tout << mk_ismt2_pp(k, m()) << "\n--->\n" << mk_ismt2_pp(v, m()) << "\n";);
+
+    m_cache->insert(k, v);
+#if 0
+    static unsigned num_cached = 0;
+    num_cached ++;
+    if (num_cached % 100000 == 0)
+        verbose_stream() << "[rewriter] :num-cached " << num_cached << " :capacity " << m_cache->capacity() << " :size " << m_cache->size() 
+                  << " :frame-stack-size " << m_frame_stack.size() << std::endl;
+#endif
+}
+
+void rewriter_core::cache_result(expr * k, expr * v, proof * pr) {
+    m_cache->insert(k, v);
+    SASSERT(m_proof_gen);
+    m_cache_pr->insert(k, pr);
+}
+
+unsigned rewriter_core::get_cache_size() const {
+    return m_cache->size();
+}
+
+void rewriter_core::reset_cache() {
+    m_cache = m_cache_stack[0];
+    m_cache->reset();
+    if (m_proof_gen) {
+        m_cache_pr = m_cache_pr_stack[0];
+        m_cache_pr->reset();
+    }
+}
+
+// free memory allocated by the rewriter
+void rewriter_core::free_memory() {
+    del_cache_stack();
+    m_frame_stack.finalize();
+    m_result_stack.finalize();
+    m_scopes.finalize();
+}
+
+void rewriter_core::begin_scope() {
+    m_scopes.push_back(scope(m_root, m_num_qvars));
+    unsigned lvl = m_scopes.size();
+    SASSERT(lvl <= m_cache_stack.size());
+    SASSERT(!m_proof_gen || m_cache_pr_stack.size() == m_cache_stack.size());
+    if (lvl == m_cache_stack.size()) {
+        m_cache_stack.push_back(alloc(cache, m()));
+        if (m_proof_gen)
+            m_cache_pr_stack.push_back(alloc(cache, m()));
+    }
+    m_cache = m_cache_stack[lvl];
+    m_cache->reset();
+    SASSERT(m_cache->empty());
+    if (m_proof_gen) {
+        m_cache_pr = m_cache_pr_stack[lvl];
+        m_cache_pr->reset();
+        SASSERT(m_cache_pr->empty());
+    }
+}
+
+void rewriter_core::end_scope() {
+    m_cache->reset();
+    if (m_proof_gen)
+        m_cache_pr->reset();
+    scope & s        = m_scopes.back();
+    m_root           = s.m_old_root;
+    m_num_qvars      = s.m_old_num_qvars;
+    m_scopes.pop_back();
+    unsigned new_lvl = m_scopes.size();
+    m_cache          = m_cache_stack[new_lvl];
+    if (m_proof_gen)
+        m_cache_pr   = m_cache_pr_stack[new_lvl];
+}
+
+bool rewriter_core::is_child_of_top_frame(expr * t) const {
+    if (m_frame_stack.empty())
+        return true;
+    frame const & fr = m_frame_stack.back();
+    expr * parent = fr.m_curr;
+    unsigned num;
+    switch (parent->get_kind()) {
+    case AST_APP:
+        num = to_app(parent)->get_num_args();
+        for (unsigned i = 0; i < num; i++) {
+            if (to_app(parent)->get_arg(i) == t)
+                return true;
+        }
+        return false;
+    case AST_QUANTIFIER:
+        num = to_quantifier(parent)->get_num_children();
+        for (unsigned i = 0; i < num; i++) {
+            if (to_quantifier(parent)->get_child(i) == t)
+                return true;
+        }
+        return false;
+    default:
+        return false;
+    }
+}
+
+/**
+   \brief Eliminate (implicit) reflexivity proofs from m_result_pr_stack starting at position spos.
+   The implicit reflexivity proof is 0.
+*/
+void rewriter_core::elim_reflex_prs(unsigned spos) {
+    SASSERT(m_proof_gen);
+    unsigned sz = m_result_pr_stack.size();
+    SASSERT(spos <= sz);
+    unsigned j = spos;
+    for (unsigned i = spos; i < sz; i++) {
+        proof * pr = m_result_pr_stack.get(i);
+        if (pr != 0) {
+            if (i != j)
+                m_result_pr_stack.set(j, pr);
+            j++;
+        }
+    }
+    m_result_pr_stack.shrink(j);
+}
+
+rewriter_core::rewriter_core(ast_manager & m, bool proof_gen):
+    m_manager(m),
+    m_proof_gen(proof_gen),
+    m_result_stack(m),
+    m_result_pr_stack(m),
+    m_num_qvars(0) {
+    init_cache_stack();
+}
+
+rewriter_core::~rewriter_core() {
+    del_cache_stack();
+}
+
+// reset rewriter (macro definitions are not erased)
+void rewriter_core::reset() {
+    SASSERT(!m_cache_stack.empty());
+    reset_cache();
+    m_frame_stack.reset();
+    m_result_stack.reset();
+    if (m_proof_gen)
+        m_result_pr_stack.reset();
+    m_root = 0;
+    m_num_qvars = 0;
+    m_scopes.reset();
+}
+
+// free memory & reset (macro definitions are not erased)
+void rewriter_core::cleanup() {
+    free_memory();
+    init_cache_stack();
+    m_root       = 0;
+    m_num_qvars  = 0;
+}
+
+
+#ifdef _TRACE
+void rewriter_core::display_stack(std::ostream & out, unsigned pp_depth) {
+    svector<frame>::iterator it  = m_frame_stack.begin();
+    svector<frame>::iterator end = m_frame_stack.end();
+    for (; it != end; ++it) {
+        out << mk_bounded_pp(it->m_curr, m(), pp_depth) << "\n";
+        out << "state: " << it->m_state << "\n";
+        out << "cache: " << it->m_cache_result << ", new_child: " << it->m_new_child << ", max-depth: " << it->m_max_depth << ", i: " << it->m_i << "\n";
+        out << "------------------\n";
+    }
+}
+#endif
+
+bool var_shifter_core::visit(expr * t) {
+    if (is_ground(t)) {
+        m_result_stack.push_back(t);
+        return true;
+    }
+    bool c = must_cache(t);
+    if (c) {
+        expr * r = get_cached(t);
+        if (r) {
+            m_result_stack.push_back(r);
+            set_new_child_flag(t, r);
+            return true;
+        }
+    }
+    switch (t->get_kind()) {
+    case AST_APP:
+        SASSERT(to_app(t)->get_num_args() > 0);
+        push_frame(t, c);
+        return false;
+    case AST_VAR:
+        process_var(to_var(t));
+        return true;
+    case AST_QUANTIFIER:
+        push_frame(t, c);
+        return false;
+    default:
+        UNREACHABLE();
+        return true;
+    }
+}
+
+void var_shifter_core::process_app(app * t, frame & fr) {
+    unsigned num_args = t->get_num_args();
+    while (fr.m_i < num_args) {
+        expr * arg = t->get_arg(fr.m_i);
+        fr.m_i++;
+        if (!visit(arg))
+            return;
+    }
+    SASSERT(fr.m_spos + num_args == m_result_stack.size());
+    expr * new_t;
+    if (fr.m_new_child) {
+        expr * const * new_args = m_result_stack.c_ptr() + fr.m_spos;
+        new_t = m().mk_app(t->get_decl(), num_args, new_args);
+    }
+    else {
+        new_t = t;
+    }
+    m_result_stack.shrink(fr.m_spos);
+    m_result_stack.push_back(new_t);
+    m_frame_stack.pop_back();
+    set_new_child_flag(t, new_t);
+    if (fr.m_cache_result)
+        cache_result(t, new_t);
+}
+
+void var_shifter_core::process_quantifier(quantifier * q, frame & fr) {
+    if (fr.m_i == 0) {
+        begin_scope();
+        m_num_qvars += q->get_num_decls();
+        m_root       = q->get_expr();
+    }
+    unsigned num_children = q->get_num_children();
+    while (fr.m_i < num_children) {
+        expr * child = q->get_child(fr.m_i);
+        fr.m_i++;
+        if (!visit(child))
+            return;
+    }
+    SASSERT(fr.m_spos + num_children == m_result_stack.size());
+    expr * new_q;
+    if (fr.m_new_child) {
+        expr * const * it = m_result_stack.c_ptr() + fr.m_spos;
+        expr * new_expr = *it;
+        ++it;
+        expr * const * new_pats    = it;
+        expr * const * new_no_pats = new_pats + q->get_num_patterns();
+        new_q = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_expr);
+    }
+    else {
+        new_q = q;
+    }
+    m_result_stack.shrink(fr.m_spos);
+    m_result_stack.push_back(new_q);
+    m_frame_stack.pop_back();
+    set_new_child_flag(q, new_q);
+    end_scope();
+    if (fr.m_cache_result)
+        cache_result(q, new_q);
+}
+
+void var_shifter_core::main_loop(expr * t, expr_ref & r) {
+    SASSERT(m_cache == m_cache_stack[0]);
+    SASSERT(m_frame_stack.empty());
+    SASSERT(m_result_stack.empty());
+    m_root      = t;
+
+    if (visit(t)) {
+        r = m_result_stack.back();
+        m_result_stack.pop_back();
+        SASSERT(m_result_stack.empty());
+        return;
+    }
+    SASSERT(!m_frame_stack.empty());
+    while (!m_frame_stack.empty()) {
+        frame & fr = m_frame_stack.back();
+        expr * t   = fr.m_curr;
+        if (fr.m_i == 0 && fr.m_cache_result) {
+            expr * r = get_cached(t);
+            if (r) {
+                m_result_stack.push_back(r);
+                m_frame_stack.pop_back();
+                set_new_child_flag(t, r);
+                continue;
+            }
+        }
+        switch (t->get_kind()) {
+        case AST_APP:
+            process_app(to_app(t), fr);
+            break;
+        case AST_QUANTIFIER:
+            process_quantifier(to_quantifier(t), fr);
+            break;
+        default:
+            UNREACHABLE();
+        }
+    }
+    r = m_result_stack.back();
+    m_result_stack.pop_back();
+    SASSERT(m_result_stack.empty());
+}
+
+void var_shifter::operator()(expr * t, unsigned bound, unsigned shift1, unsigned shift2, expr_ref & r) {
+    if (is_ground(t)) {
+        r = t;
+        return;
+    }
+    reset_cache();
+    m_bound     = bound;
+    m_shift1    = shift1;
+    m_shift2    = shift2;
+    main_loop(t, r);
+}
+
+void var_shifter::process_var(var * v) {
+    unsigned vidx = v->get_idx();
+    if (vidx < m_num_qvars) {
+        m_result_stack.push_back(v);
+    }
+    else {
+        unsigned nvidx = vidx - m_num_qvars;
+        if (nvidx >= m_bound)
+            vidx += m_shift1;
+        else
+            vidx += m_shift2;
+        m_result_stack.push_back(m().mk_var(vidx, v->get_sort()));
+        set_new_child_flag(v);
+    }
+}
+
+void inv_var_shifter::operator()(expr * t, unsigned shift, expr_ref & r) {
+    if (is_ground(t)) {
+        r = t;
+        return;
+    }
+    reset_cache();
+    m_shift     = shift;
+    main_loop(t, r);
+}
+
+void inv_var_shifter::process_var(var * v) {
+    unsigned vidx = v->get_idx();
+    if (vidx < m_num_qvars) {
+        m_result_stack.push_back(v);
+    }
+    else {
+        SASSERT(vidx >= m_num_qvars + m_shift); 
+        vidx -= m_shift;
+        m_result_stack.push_back(m().mk_var(vidx, v->get_sort()));
+        set_new_child_flag(v);
+    }
+}
+    
+template class rewriter_tpl<beta_reducer_cfg>;

src/rewriter/rewriter.h

@@ -0,0 +1,399 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    rewriter.h
+
+Abstract:
+
+    Lean and mean rewriter
+
+Author:
+
+    Leonardo (leonardo) 2011-03-31
+
+Notes:
+
+--*/
+#ifndef _REWRITER_H_
+#define _REWRITER_H_
+
+#include"ast.h"
+#include"rewriter_types.h"
+#include"act_cache.h"
+
+/**
+   \brief Common infrastructure for AST rewriters.
+*/
+class rewriter_core {
+protected:
+    struct frame {
+        expr *   m_curr;
+        unsigned m_cache_result:1; // true if the result of rewriting m_expr must be cached.
+        unsigned m_new_child:1;
+        unsigned m_state:2;
+        unsigned m_max_depth:2;     // bounded rewrite... if m_max_depth == 0, then children are not rewritten.
+        unsigned m_i:26;
+        unsigned m_spos;           // top of the result stack, when the frame was created.
+        frame(expr * n, bool cache_res, unsigned st, unsigned max_depth, unsigned spos):
+            m_curr(n), 
+            m_cache_result(cache_res),
+            m_new_child(false),
+            m_state(st),
+            m_max_depth(max_depth),
+            m_i(0),
+            m_spos(spos) {
+        }
+    };
+    ast_manager &              m_manager;
+    bool                       m_proof_gen; 
+    typedef act_cache          cache;
+    ptr_vector<cache>          m_cache_stack;
+    cache *                    m_cache; // current cache.
+    svector<frame>             m_frame_stack;
+    expr_ref_vector            m_result_stack;
+
+    // proof generation goodness ----
+    ptr_vector<cache>          m_cache_pr_stack; 
+    cache *                    m_cache_pr;
+    proof_ref_vector           m_result_pr_stack;
+    // --------------------------
+
+    expr *                     m_root;
+    unsigned                   m_num_qvars;
+    struct scope {
+        expr *   m_old_root;
+        unsigned m_old_num_qvars;
+        scope(expr * r, unsigned n):m_old_root(r), m_old_num_qvars(n) {}
+    };
+    svector<scope>             m_scopes;
+
+    // Return true if the rewriting result of the given expression must be cached.
+    bool must_cache(expr * t) const {
+        return 
+            t->get_ref_count() > 1 &&  // t must be a shared expression
+            t != m_root && // t must not be the root expression
+            ((is_app(t) && to_app(t)->get_num_args() > 0) || is_quantifier(t)); // t is a (non-constant) application or a quantifier.
+    }
+
+    void push_frame_core(expr * t, bool cache_res, unsigned st = 0, unsigned max_depth = RW_UNBOUNDED_DEPTH) {
+        SASSERT(!m_proof_gen || m_result_stack.size() == m_result_pr_stack.size());
+        m_frame_stack.push_back(frame(t, cache_res, st, max_depth, m_result_stack.size()));
+    }
+
+    void push_frame(expr * t, unsigned st = 0) {
+        push_frame_core(t, must_cache(t), st);
+    } 
+
+    void init_cache_stack();
+    void del_cache_stack();
+    void reset_cache();
+    void cache_result(expr * k, expr * v);
+    expr * get_cached(expr * k) const { return m_cache->find(k); } 
+
+    void cache_result(expr * k, expr * v, proof * pr);
+    proof * get_cached_pr(expr * k) const { return static_cast<proof*>(m_cache_pr->find(k)); } 
+
+    void free_memory();
+    void begin_scope();
+    void end_scope();
+    bool is_child_of_top_frame(expr * t) const;
+    void set_new_child_flag(expr * old_t) {
+        CTRACE("rewriter_bug", !is_child_of_top_frame(old_t), display_stack(tout, 3););
+        SASSERT(is_child_of_top_frame(old_t));
+        if (!m_frame_stack.empty())
+            m_frame_stack.back().m_new_child = true;
+    }
+    void set_new_child_flag(expr * old_t, expr * new_t) { if (old_t != new_t) set_new_child_flag(old_t); }
+    
+    void elim_reflex_prs(unsigned spos);
+public:
+    rewriter_core(ast_manager & m, bool proof_gen);
+    ~rewriter_core();
+    ast_manager & m() const { return m_manager; }
+    void reset();
+    void cleanup();
+#ifdef _TRACE
+    void display_stack(std::ostream & out, unsigned pp_depth);
+#endif
+    unsigned get_cache_size() const;
+};
+
+class var_shifter_core : public rewriter_core {
+protected:
+    bool visit(expr * t);
+    void process_app(app * t, frame & fr);
+    virtual void process_var(var * v) = 0;
+    void process_quantifier(quantifier * q, frame & fr);
+    void main_loop(expr * t, expr_ref & r);
+public:
+    var_shifter_core(ast_manager & m):rewriter_core(m, false) {}
+};
+
+/**
+   \brief Functor used to shift the free variables of an AST by a given amount.
+   This functor is used by the var_subst functor.
+
+   This functor implements the following functions:
+   1) shift(n, s) will return a new AST where all free variables (VAR i) in n,
+   are replaced by (VAR (+ i s)).
+
+   2) shift(n, b, s1, s2) is a variant of the previous function such that 
+   for a each free variable (VAR i) is shifted to:
+       - (VAR i + s1) if i >= b
+       - (VAR i + s2) if i < b 
+*/
+class var_shifter : public var_shifter_core {
+    unsigned  m_bound;
+    unsigned  m_shift1;
+    unsigned  m_shift2;
+    virtual void process_var(var * v);
+public:
+    var_shifter(ast_manager & m):var_shifter_core(m) {}
+    void operator()(expr * t, unsigned bound, unsigned shift1, unsigned shift2, expr_ref & r);
+    void operator()(expr * t, unsigned s, expr_ref & r) {
+        operator()(t, 0, s, 0, r);
+    }
+};
+
+/**
+   \brief Functor used to shift the free variables of an AST by a negative amount.
+
+   Abstract implementation:
+
+   inv_shift(f(c_1, ..., c_n), d, s) =
+     f(inv_shift(c_1, d, s), ..., inv_shift(c_n, d, s))
+   inv_shift(var(i), d, s) =
+     if (i < d) 
+       var(i)
+     else
+       assert(i - s >= d)
+       var(i-s)
+  inv_shift((forall (x) P), d, s) =
+    (forall (x) inv_shift(P, d+1, s))
+   
+  This functor assumes that if we are shifting an expression F by N, then F
+  does not contain free variables #0, ... #N-1 
+
+  See assertion above.
+*/
+class inv_var_shifter : public var_shifter_core {
+protected:
+    unsigned m_shift;
+    virtual void process_var(var * v);
+public:
+    inv_var_shifter(ast_manager & m):var_shifter_core(m) {}
+    void operator()(expr * t, unsigned shift, expr_ref & r);
+};
+
+template<typename Config> 
+class rewriter_tpl : public rewriter_core {
+protected:
+    // Rewriter maintains a stack of frames.
+    // Each frame represents an expression that is being rewritten.
+    // The resultant expressions are store on the Result stack.
+    // Each frame is in a particular state.
+    // Let f(t_0,...,t_n) be the expression is the frame Fr. Then Fr can be is one of the 
+    // following states:
+    //    PROCESS_CHILDREN(i) the children t_0, ..., t_{i-1} have already been rewritten, and the result is on the Result stack.
+    //    REWRITE_BUILTIN All t_0, ..., t_n have been rewritten to t_0',...,t_n', and the builtin rewriter (or plugin) produced a new term t
+    //                    that can be further rewritten.
+    //    EXPAND_DEF      All t_0, ..., t_n have been rewritten to t_0',...,t_n'.
+    //                    The function symbol f is a macro, and the body of the macro needs to be rewritten using the t_0',...,t_n' as bindings.
+    //    REWRITE_RULE    All t_0, ..., t_n have been rewritten to t_0',...,t_n'.
+    //                    There is rewrite rule lhs -> rhs s.t. f(t_0', ..., t_n') matches lhs with substitution delta.
+    //                    rhs is then rewritten using delta.
+    enum state {
+        PROCESS_CHILDREN,
+        REWRITE_BUILTIN,
+        EXPAND_DEF,
+        REWRITE_RULE
+    };
+    Config &                   m_cfg;
+    unsigned                   m_num_steps;
+    volatile bool              m_cancel;
+    ptr_vector<expr>           m_bindings;
+    var_shifter                m_shifter;
+    expr_ref                   m_r;
+    proof_ref                  m_pr;
+    proof_ref                  m_pr2;
+    
+    svector<frame> & frame_stack() { return this->m_frame_stack; }
+    svector<frame> const & frame_stack() const { return this->m_frame_stack; }
+    expr_ref_vector & result_stack() { return this->m_result_stack; }
+    expr_ref_vector const & result_stack() const { return this->m_result_stack; }
+    proof_ref_vector & result_pr_stack() { return this->m_result_pr_stack; }
+    proof_ref_vector const & result_pr_stack() const { return this->m_result_pr_stack; }
+
+    void set_new_child_flag(expr * old_t) {
+        SASSERT(frame_stack().empty() || frame_stack().back().m_state != PROCESS_CHILDREN || this->is_child_of_top_frame(old_t));
+        if (!frame_stack().empty())
+            frame_stack().back().m_new_child = true;
+    }
+    void set_new_child_flag(expr * old_t, expr * new_t) { if (old_t != new_t) set_new_child_flag(old_t); }
+
+
+    // cache the result of shared non atomic expressions.
+    bool cache_results() const { return m_cfg.cache_results(); }
+    // cache all results share and non shared expressions non atomic expressions.
+    bool cache_all_results() const { return m_cfg.cache_all_results(); }
+    // flat non shared AC terms
+    bool flat_assoc(func_decl * f) const { return m_cfg.flat_assoc(f); }
+    // rewrite patterns
+    bool rewrite_patterns() const { return m_cfg.rewrite_patterns(); }
+   
+    // check maximum number of scopes
+    void check_max_scopes() const { 
+        if (m_cfg.max_scopes_exceeded(this->m_scopes.size()))
+            throw rewriter_exception(TACTIC_MAX_SCOPES_MSG);
+    }
+    // check maximum size of the frame stack
+    void check_max_frames() const { 
+        if (m_cfg.max_frames_exceeded(frame_stack().size()))
+            throw rewriter_exception(TACTIC_MAX_FRAMES_MSG);
+    }
+    // check maximum number of rewriting steps
+    void check_max_steps() const { 
+        if (m_cfg.max_steps_exceeded(m_num_steps))
+            throw rewriter_exception(TACTIC_MAX_STEPS_MSG);
+    }
+
+    // If pre_visit returns false, then t children are not visited/rewritten.
+    // This should be used with care, since it may produce incorrect results
+    // when the rewriter is used to apply variable substitution.
+    bool pre_visit(expr * t) {
+        return m_cfg.pre_visit(t);
+    }
+
+    // Return true if the rewriting result of the given expression must be cached.
+    bool must_cache(expr * t) const {
+        if (cache_all_results())
+            return t != this->m_root && ((is_app(t) && to_app(t)->get_num_args() > 0) || is_quantifier(t));
+        if (cache_results())
+            return rewriter_core::must_cache(t); 
+        return false;
+    }
+
+    bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) {
+        return m_cfg.get_macro(f, def, q, def_pr);
+    }
+
+    void push_frame(expr * t, bool mcache, unsigned max_depth) {
+        check_max_frames();
+        push_frame_core(t, mcache, PROCESS_CHILDREN, max_depth);
+    }
+
+    void begin_scope() {
+        check_max_scopes();
+        rewriter_core::begin_scope();
+    }
+    
+    template<bool ProofGen>
+    void process_var(var * v);
+
+    template<bool ProofGen>
+    void process_const(app * t);
+
+    template<bool ProofGen>
+    bool visit(expr * t, unsigned max_depth);
+
+    template<bool ProofGen>
+    void cache_result(expr * t, expr * new_t, proof * pr, bool c) {
+        if (c) {
+            if (!ProofGen)
+                rewriter_core::cache_result(t, new_t);
+            else
+                rewriter_core::cache_result(t, new_t, pr);
+        }
+    }
+
+    template<bool ProofGen>
+    void process_app(app * t, frame & fr);
+
+    template<bool ProofGen>
+    void process_quantifier(quantifier * q, frame & fr);
+
+    bool first_visit(frame & fr) const {
+        return fr.m_state == PROCESS_CHILDREN && fr.m_i == 0;
+    }
+
+    bool not_rewriting() const;
+
+    template<bool ProofGen>
+    void main_loop(expr * t, expr_ref & result, proof_ref & result_pr);
+
+    template<bool ProofGen>
+    void resume_core(expr_ref & result, proof_ref & result_pr);
+
+public:
+    rewriter_tpl(ast_manager & m, bool proof_gen, Config & cfg);
+
+    ast_manager & m() const { return this->m_manager; }
+    Config & cfg() { return m_cfg; }
+    Config const & cfg() const { return m_cfg; }
+
+    void set_cancel(bool f) { m_cancel = f; }
+    void cancel() { set_cancel(true); }
+    void reset_cancel() { set_cancel(false); }
+
+    ~rewriter_tpl();
+    
+    void reset();
+    void cleanup();
+    
+    void set_bindings(unsigned num_bindings, expr * const * bindings);
+    void set_inv_bindings(unsigned num_bindings, expr * const * bindings);
+    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) {
+        SASSERT(!m_proof_gen);
+        reset();
+        set_inv_bindings(num_bindings, bindings);
+        operator()(n, result);
+    }
+
+    void resume(expr_ref & result, proof_ref & result_pr);
+    void resume(expr_ref & result) { resume(result, m_pr); }
+
+    // Return the number of steps performed by the rewriter in the last call to operator().
+    unsigned get_num_steps() const { return m_num_steps; }
+};
+
+struct default_rewriter_cfg {
+    bool cache_all_results() const { return false; }
+    bool cache_results() const { return true; }
+    bool flat_assoc(func_decl * f) const { return false; }
+    bool rewrite_patterns() const { return true; }
+    bool max_scopes_exceeded(unsigned num_scopes) const { return false; }
+    bool max_frames_exceeded(unsigned num_frames) const { return false; }
+    bool max_steps_exceeded(unsigned num_steps) const { return false; }
+    bool pre_visit(expr * t) { return true; }
+    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { return BR_FAILED; }
+    bool reduce_quantifier(quantifier * old_q, 
+                           expr * new_body, 
+                           expr * const * new_patterns, 
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr) {
+        return false;
+    }
+    bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { return false; }
+    bool get_macro(func_decl * d, expr * & def, quantifier * & q, proof * & def_pr) { return false; }
+    bool get_subst(expr * s, expr * & t, proof * & t_pr) { return false; }
+    void reset() {}
+    void cleanup() {}
+};
+
+struct beta_reducer_cfg : public default_rewriter_cfg {
+    bool pre_visit(expr * t) { return !is_ground(t); }
+};
+
+class beta_reducer : public rewriter_tpl<beta_reducer_cfg>  {
+    beta_reducer_cfg m_cfg;
+public:
+    beta_reducer(ast_manager & m):
+        rewriter_tpl<beta_reducer_cfg>(m, false, m_cfg) {}
+};
+
+#endif

src/rewriter/rewriter_def.h

@@ -0,0 +1,642 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    rewriter_def.h
+
+Abstract:
+
+    Lean and mean rewriter
+
+Author:
+
+    Leonardo (leonardo) 2011-03-31
+
+Notes:
+
+--*/
+#include"rewriter.h"
+#include"ast_smt2_pp.h"
+
+template<typename Config>
+template<bool ProofGen>
+void rewriter_tpl<Config>::process_var(var * v) {
+    if (m_cfg.reduce_var(v, m_r, m_pr)) {
+        result_stack().push_back(m_r);
+        if (ProofGen) {
+            result_pr_stack().push_back(m_pr);
+            m_pr = 0; 
+        }
+        set_new_child_flag(v);
+        m_r = 0;
+        return;
+    }
+    if (!ProofGen) {
+        // bindings are only used when Proof Generation is not enabled.
+        unsigned idx = v->get_idx();
+        if (idx < m_bindings.size()) {
+            expr * r = m_bindings[m_bindings.size() - idx - 1];
+            TRACE("process_var", if (r) tout << "idx: " << idx << " --> " << mk_ismt2_pp(r, m()) << "\n";
+                  tout << "bindings:\n";
+                  for (unsigned i = 0; i < m_bindings.size(); i++) if (m_bindings[i]) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
+            if (r != 0) {
+                if (m_num_qvars == 0 || is_ground(r)) {
+                    result_stack().push_back(r);
+                }
+                else {
+                    expr_ref new_term(m());
+                    m_shifter(r, m_num_qvars, new_term);
+                    result_stack().push_back(new_term);
+                }
+                set_new_child_flag(v);
+                return;
+            }
+        }
+    }
+    result_stack().push_back(v);
+    if (ProofGen)
+        result_pr_stack().push_back(0); // 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);
+    SASSERT(st == BR_FAILED || st == BR_DONE);
+    if (st == BR_DONE) {
+        result_stack().push_back(m_r.get());
+        if (ProofGen) {
+            if (m_pr)
+                result_pr_stack().push_back(m_pr);
+            else
+                result_pr_stack().push_back(m().mk_rewrite(t, m_r));
+            m_pr = 0;
+        }
+        m_r = 0;
+        set_new_child_flag(t);
+    }
+    else {
+        result_stack().push_back(t);
+        if (ProofGen)
+            result_pr_stack().push_back(0); // implicit reflexivity
+    }
+}
+
+/**
+   \brief visit expression t. Return true if t was rewritten and the result is on the top m_result_stack.
+   We may skip t if:
+      - pre_visit(t) returns false
+      - max_depth == 0
+      - t is already in the cache
+   Otherwise, return false and add a new frame stack for t with the updated max_depth.
+*/
+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;
+    proof * new_t_pr;
+    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";);
+        result_stack().push_back(new_t);
+        set_new_child_flag(t, new_t);
+        if (ProofGen)
+            result_pr_stack().push_back(new_t_pr);
+        return true;
+    }
+    if (max_depth == 0) {
+        result_stack().push_back(t);
+        if (ProofGen)
+            result_pr_stack().push_back(0); // implicit reflexivity
+        return true; // t is not going to be processed
+    }
+    SASSERT(max_depth > 0);
+    SASSERT(max_depth <= RW_UNBOUNDED_DEPTH);
+    bool c = must_cache(t);
+    if (c) {
+#if 0
+        static unsigned checked_cache = 0;
+        checked_cache ++;
+        if (checked_cache % 100000 == 0)
+            std::cerr << "[rewriter] num-cache-checks: " << checked_cache << std::endl;
+#endif
+        expr * r = get_cached(t);
+        if (r) {
+            result_stack().push_back(r);
+            set_new_child_flag(t, r);
+            if (ProofGen) {
+                proof * pr = get_cached_pr(t);
+                result_pr_stack().push_back(pr);
+            }
+            return true;
+        }
+    }
+    if (!pre_visit(t)) {
+        result_stack().push_back(t);
+        if (ProofGen)
+            result_pr_stack().push_back(0); // implicit reflexivity
+        return true; // t is not going to be processed
+    }
+    switch (t->get_kind()) {
+    case AST_APP:
+        if (to_app(t)->get_num_args() == 0) {
+            process_const<ProofGen>(to_app(t));
+            return true;
+        }
+        else {
+            if (max_depth != RW_UNBOUNDED_DEPTH)
+                max_depth--;
+            push_frame(t, c, max_depth);
+            return false;
+        }
+    case AST_VAR:
+        process_var<ProofGen>(to_var(t));
+        return true;
+    case AST_QUANTIFIER:
+        if (max_depth != RW_UNBOUNDED_DEPTH)
+            max_depth--;
+        push_frame(t, c, max_depth);
+        return false;
+    default:
+        UNREACHABLE();
+        return true;
+    }
+}
+
+template<typename Config>
+template<bool ProofGen>
+void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
+    SASSERT(t->get_num_args() > 0);
+    SASSERT(!frame_stack().empty());
+    switch (fr.m_state) {
+    case PROCESS_CHILDREN: {
+        unsigned num_args = t->get_num_args();
+        while (fr.m_i < num_args) {
+            expr * arg = t->get_arg(fr.m_i);
+            fr.m_i++;
+            if (!visit<ProofGen>(arg, fr.m_max_depth))
+                return;
+        }
+        func_decl * f = t->get_decl();
+
+        // If AC flattening is enabled, f is associative, t is not shared, and there is a previous frame on the stack.
+        if (!ProofGen) {
+            // this optimization is only used when Proof generation is disabled.
+            if (f->is_associative() && t->get_ref_count() <= 1 && frame_stack().size() > 1) {
+                frame & prev_fr = frame_stack()[frame_stack().size() - 2];
+                if (is_app(prev_fr.m_curr) && 
+                    to_app(prev_fr.m_curr)->get_decl() == f && 
+                    prev_fr.m_state == PROCESS_CHILDREN && 
+                    flat_assoc(f)) {
+                    frame_stack().pop_back();
+                    set_new_child_flag(t);
+                    return;
+                }
+            }
+        }
+
+        unsigned new_num_args   = result_stack().size() - fr.m_spos;
+        expr * const * new_args = result_stack().c_ptr() + fr.m_spos;
+        app * new_t;
+        if (ProofGen) {
+            elim_reflex_prs(fr.m_spos);
+            unsigned num_prs    = result_pr_stack().size() - fr.m_spos;
+            if (num_prs == 0) {
+                new_t = t;
+                m_pr  = 0;
+            }
+            else {
+                new_t = m().mk_app(f, new_num_args, new_args);
+                m_pr  = m().mk_congruence(t, new_t, num_prs, result_pr_stack().c_ptr() + fr.m_spos);
+            }
+        }
+        br_status st = m_cfg.reduce_app(f, new_num_args, new_args, m_r, m_pr2);
+        TRACE("reduce_app", 
+              tout << mk_ismt2_pp(t, m()) << "\n";
+              tout << "st: " << st;
+              if (m_r) tout << " --->\n" << mk_ismt2_pp(m_r, m());
+              tout << "\n";);
+        if (st != BR_FAILED) {
+            result_stack().shrink(fr.m_spos);
+            result_stack().push_back(m_r);
+            if (ProofGen) {
+                result_pr_stack().shrink(fr.m_spos);
+                if (!m_pr2)
+                    m_pr2 = m().mk_rewrite(new_t, m_r);
+                m_pr  = m().mk_transitivity(m_pr, m_pr2);
+                m_pr2 = 0;
+                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;
+                if (ProofGen)
+                    m_pr = 0;
+                return;
+            }
+            else {
+                fr.m_state = REWRITE_BUILTIN;
+                SASSERT(st == BR_REWRITE1 || st == BR_REWRITE2 || st == BR_REWRITE3 || st == BR_REWRITE_FULL);
+                unsigned max_depth = static_cast<unsigned>(st);
+                SASSERT(0 <= max_depth && max_depth <= RW_UNBOUNDED_DEPTH);
+                SASSERT((st == BR_REWRITE1) == (max_depth == 0));
+                SASSERT((st == BR_REWRITE2) == (max_depth == 1));
+                SASSERT((st == BR_REWRITE3) == (max_depth == 2));
+                SASSERT((st == BR_REWRITE_FULL) == (max_depth == RW_UNBOUNDED_DEPTH));
+                if (max_depth != RW_UNBOUNDED_DEPTH)
+                    max_depth++;
+                if (visit<ProofGen>(m_r, max_depth)) {
+                    if (ProofGen) {
+                        proof_ref pr2(m()), pr1(m());
+                        pr2 = result_pr_stack().back();
+                        result_pr_stack().pop_back();
+                        pr1 = result_pr_stack().back();
+                        result_pr_stack().pop_back();
+                        m_pr = m().mk_transitivity(pr1, pr2);
+                        result_pr_stack().push_back(m_pr);
+                    }
+                    m_r = result_stack().back();
+                    result_stack().pop_back();
+                    result_stack().pop_back();
+                    result_stack().push_back(m_r);
+                    cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
+                    frame_stack().pop_back();
+                    set_new_child_flag(t);
+                    m_r = 0;
+                    if (ProofGen)
+                        m_pr = 0;
+                    return;
+                }
+                else {
+                    // frame was created for processing m_r
+                    m_r = 0;
+                    if (ProofGen)
+                        m_pr = 0;
+                    return;
+                }
+            }
+            UNREACHABLE();
+        }
+        // TODO: add rewrite rules support
+        expr * def;
+        proof * def_pr;
+        quantifier * def_q;
+        // When get_macro succeeds, then 
+        // we know that:
+        // forall X. f(X) = def[X]
+        // and def_pr is a proof for this quantifier.
+        // 
+        // Remark: def_q is only used for proof generation.
+        // It is the quantifier forall X. f(X) = def[X]
+        if (get_macro(f, def, def_q, def_pr)) {
+            SASSERT(!f->is_associative() || !flat_assoc(f));
+            SASSERT(new_num_args == t->get_num_args());
+            if (is_ground(def)) {
+                m_r = def;
+                if (ProofGen) {
+                    SASSERT(def_pr);
+                    m_pr = m().mk_transitivity(m_pr, def_pr);
+                }
+            }
+            else {
+                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 
+                    // beta_reducer subst(m());
+                    // subst.set_bindings(new_num_args, new_args);
+                    // expr_ref r2(m());
+                    // subst(def, r2);
+                }
+                else {
+                    fr.m_state = EXPAND_DEF;
+                    TRACE("get_macro", tout << "f: " << f->get_name() << ", def: \n" << mk_ismt2_pp(def, m()) << "\n";
+                          tout << "Args num: " << num_args << "\n";
+                          for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(new_args[i], m()) << "\n";);
+                    unsigned i = num_args;
+                    while (i > 0) {
+                        --i;
+                        m_bindings.push_back(new_args[i]);
+                    }
+                    result_stack().push_back(def);
+                    TRACE("get_macro", tout << "bindings:\n";
+                          for (unsigned i = 0; i < m_bindings.size(); i++) tout << i << ": " << mk_ismt2_pp(m_bindings[i], m()) << "\n";);
+                    begin_scope();
+                    m_num_qvars = 0;
+                    m_root      = def;
+                    push_frame(def, false, RW_UNBOUNDED_DEPTH);
+                    return;
+                }
+            }
+        }
+        else {
+            if (ProofGen) {
+                m_r = new_t;
+            }
+            else {
+                if (fr.m_new_child) {
+                    m_r = m().mk_app(f, new_num_args, new_args);
+                }
+                else {
+                    TRACE("rewriter_reuse", tout << "reusing:\n" << mk_ismt2_pp(t, m()) << "\n";);
+                    m_r = t;
+                }
+            }
+        }
+        result_stack().shrink(fr.m_spos);
+        result_stack().push_back(m_r);
+        cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
+        if (ProofGen) {
+            result_pr_stack().shrink(fr.m_spos);
+            result_pr_stack().push_back(m_pr);
+            m_pr = 0;
+        }
+        frame_stack().pop_back();
+        set_new_child_flag(t, m_r);
+        m_r = 0;
+        return;
+    }
+    case REWRITE_BUILTIN:
+        SASSERT(fr.m_spos + 2 == result_stack().size());
+        if (ProofGen) {
+            proof_ref pr2(m()), pr1(m());
+            pr2 = result_pr_stack().back();
+            result_pr_stack().pop_back();
+            pr1 = result_pr_stack().back();
+            result_pr_stack().pop_back();
+            m_pr = m().mk_transitivity(pr1, pr2);
+            result_pr_stack().push_back(m_pr);
+        }
+        m_r = result_stack().back();
+        result_stack().pop_back();
+        result_stack().pop_back();
+        result_stack().push_back(m_r);
+        cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
+        frame_stack().pop_back();
+        set_new_child_flag(t);
+        return;
+    case EXPAND_DEF:
+        SASSERT(fr.m_spos + t->get_num_args() + 2 == result_stack().size());
+        SASSERT(t->get_num_args() <= m_bindings.size());
+        if (!ProofGen) {
+            m_bindings.shrink(m_bindings.size() - t->get_num_args());
+            end_scope();
+            m_r = result_stack().back();
+            result_stack().shrink(fr.m_spos);
+            result_stack().push_back(m_r);
+            cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
+            frame_stack().pop_back();
+            set_new_child_flag(t);
+        }
+        else {
+            // TODO
+            NOT_IMPLEMENTED_YET();
+        }
+        return;
+    case REWRITE_RULE:
+        // support for rewriting rules was not implemented yet.
+        NOT_IMPLEMENTED_YET();
+        break;
+    default:
+        UNREACHABLE();
+        break;
+    }
+}
+
+template<typename Config>
+template<bool ProofGen>
+void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
+    SASSERT(fr.m_state == PROCESS_CHILDREN);
+    if (fr.m_i == 0) {
+        if (!ProofGen) {
+            begin_scope();
+            m_root       = q->get_expr();
+        }
+        m_num_qvars += q->get_num_decls();
+        if (!ProofGen) {
+            for (unsigned i = 0; i < q->get_num_decls(); i++) 
+                m_bindings.push_back(0);
+        }
+    }
+    unsigned num_children = rewrite_patterns() ? q->get_num_children() : 1;
+    while (fr.m_i < num_children) {
+        expr * child = q->get_child(fr.m_i);
+        fr.m_i++;
+        if (!visit<ProofGen>(child, fr.m_max_depth))
+            return;
+    }
+    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;
+    if (rewrite_patterns()) {
+        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(); 
+    }
+    if (ProofGen) {
+        quantifier * new_q = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body);
+        m_pr = q == new_q ? 0 : 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)) {
+            m_pr = m().mk_transitivity(m_pr, pr2);
+        }
+        TRACE("reduce_quantifier_bug", tout << "m_pr is_null: " << (m_pr.get() == 0) << "\n";
+              if (m_pr) tout << mk_ismt2_pp(m_pr, m()) << "\n";);
+        result_pr_stack().shrink(fr.m_spos);
+        result_pr_stack().push_back(m_pr);
+    }
+    else {
+        if (!m_cfg.reduce_quantifier(q, new_body, new_pats, new_no_pats, 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);
+            }
+            else {
+                TRACE("rewriter_reuse", tout << "reusing:\n" << mk_ismt2_pp(q, m()) << "\n";);
+                m_r = q;
+            }
+        }
+    }
+    result_stack().shrink(fr.m_spos);
+    result_stack().push_back(m_r.get());
+    if (!ProofGen) {
+        SASSERT(q->get_num_decls() <= m_bindings.size());
+        m_bindings.shrink(m_bindings.size() - q->get_num_decls());
+        end_scope();
+        cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
+    }
+    else {
+        cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
+        m_pr = 0;
+    }
+    m_r = 0;
+    frame_stack().pop_back();
+    set_new_child_flag(q, m_r);
+}
+
+template<typename Config>
+bool rewriter_tpl<Config>::not_rewriting() const {
+    SASSERT(frame_stack().empty());
+    SASSERT(m_cache == m_cache_stack[0]);
+    return true;
+}
+
+template<typename Config>
+rewriter_tpl<Config>::rewriter_tpl(ast_manager & m, bool proof_gen, Config & cfg):
+    rewriter_core(m, proof_gen),
+    m_cfg(cfg),
+    m_num_steps(0),
+    m_cancel(false),
+    m_shifter(m),
+    m_r(m),
+    m_pr(m),
+    m_pr2(m) {
+}
+
+template<typename Config>
+rewriter_tpl<Config>::~rewriter_tpl() {
+}
+
+template<typename Config>
+void rewriter_tpl<Config>::reset() {
+    m_cfg.reset();
+    rewriter_core::reset();
+    m_bindings.reset();
+    m_shifter.reset();
+}
+
+template<typename Config>
+void rewriter_tpl<Config>::cleanup() {
+    m_cfg.cleanup();
+    rewriter_core::cleanup();
+    m_bindings.finalize();
+    m_shifter.cleanup();
+}
+
+template<typename Config>
+void rewriter_tpl<Config>::set_bindings(unsigned num_bindings, expr * const * bindings) {
+    SASSERT(!m_proof_gen);
+    SASSERT(not_rewriting());
+    m_bindings.reset();
+    unsigned i = num_bindings;
+    while (i > 0) {
+        --i;
+        m_bindings.push_back(bindings[i]);
+    }
+}
+
+template<typename Config>
+void rewriter_tpl<Config>::set_inv_bindings(unsigned num_bindings, expr * const * bindings) {
+    SASSERT(!m_proof_gen);
+    SASSERT(not_rewriting());
+    m_bindings.reset();
+    for (unsigned i = 0; i < num_bindings; i++) {
+        m_bindings.push_back(bindings[i]);
+    }
+}
+
+template<typename Config>
+template<bool ProofGen>
+void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & result_pr) {
+    SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
+    SASSERT(not_rewriting());
+    m_root      = t;
+    m_num_qvars = 0;
+    m_num_steps = 0;
+    if (visit<ProofGen>(t, RW_UNBOUNDED_DEPTH)) {
+        result = result_stack().back();
+        result_stack().pop_back();
+        SASSERT(result_stack().empty());
+        if (ProofGen) {
+            result_pr = result_pr_stack().back();
+            result_pr_stack().pop_back();
+            if (result_pr.get() == 0)
+                result_pr = m().mk_reflexivity(t);
+            SASSERT(result_pr_stack().empty());
+        }
+        return;
+    }
+    resume_core<ProofGen>(result, result_pr);
+}
+
+/**
+   \brief Resume the execution when it was interrupted by cancel() or check_max_steps().
+*/
+template<typename Config>
+template<bool ProofGen>
+void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr) {
+    SASSERT(!frame_stack().empty());
+    while (!frame_stack().empty()) {
+        if (m_cancel)
+            throw rewriter_exception(TACTIC_CANCELED_MSG);
+        SASSERT(!ProofGen || result_stack().size() == result_pr_stack().size());
+        frame & fr = frame_stack().back();
+        expr * t   = fr.m_curr;
+        TRACE("rewriter_step", tout << "step\n" << mk_ismt2_pp(t, m()) << "\n";);
+        m_num_steps++;
+        check_max_steps();
+        if (first_visit(fr) && fr.m_cache_result) {
+            expr * r = get_cached(t);
+            if (r) {
+                result_stack().push_back(r);
+                if (ProofGen) {
+                    proof * pr = get_cached_pr(t);
+                    result_pr_stack().push_back(pr);
+                }
+                frame_stack().pop_back();
+                set_new_child_flag(t, r);
+                continue;
+            }
+        }
+        switch (t->get_kind()) {
+        case AST_APP:
+            process_app<ProofGen>(to_app(t), fr);
+            break;
+        case AST_QUANTIFIER:
+            process_quantifier<ProofGen>(to_quantifier(t), fr);
+            break;
+        case AST_VAR:
+            frame_stack().pop_back();
+            process_var<ProofGen>(to_var(t));
+            break;
+        default:
+            UNREACHABLE();
+            break;
+        }
+    }
+    result = result_stack().back();
+    result_stack().pop_back();
+    SASSERT(result_stack().empty());
+    if (ProofGen) {
+        result_pr = result_pr_stack().back();
+        result_pr_stack().pop_back();
+        if (result_pr.get() == 0)
+            result_pr = m().mk_reflexivity(m_root);
+        SASSERT(result_pr_stack().empty());
+    }
+}
+
+template<typename Config>
+void rewriter_tpl<Config>::operator()(expr * t, expr_ref & result, proof_ref & result_pr) {
+    if (m_proof_gen)
+        main_loop<true>(t, result, result_pr);
+    else
+        main_loop<false>(t, result, result_pr);
+}
+
+template<typename Config>
+void rewriter_tpl<Config>::resume(expr_ref & result, proof_ref & result_pr) {
+    if (m_proof_gen)
+        resume_core<true>(result, result_pr);
+    else
+        resume_core<false>(result, result_pr);
+}

src/rewriter/rewriter_types.h

@@ -0,0 +1,51 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    rewriter_types.h
+
+Abstract:
+
+    Lean and mean rewriter
+
+Author:
+
+    Leonardo (leonardo) 2011-04-10
+
+Notes:
+
+--*/
+#ifndef _REWRITER_TYPES_H_
+#define _REWRITER_TYPES_H_
+
+#include"tactic_exception.h"
+
+/**
+   \brief Builtin rewrite result status
+*/
+enum br_status {
+    BR_REWRITE1,               // rewrite the result (bounded by depth 1)
+    BR_REWRITE2,               // rewrite the result (bounded by depth 2)
+    BR_REWRITE3,               // rewrite the result (bounded by depth 3)
+    BR_REWRITE_FULL,           // rewrite the result unbounded
+    BR_DONE,                   // done, the result is simplified
+    BR_FAILED                  // no builtin rewrite is available
+};
+
+#define RW_UNBOUNDED_DEPTH 3
+inline br_status unsigned2br_status(unsigned u) {
+    br_status r = u >= RW_UNBOUNDED_DEPTH ? BR_REWRITE_FULL : static_cast<br_status>(u);
+    SASSERT((u == 0) == (r == BR_REWRITE1));
+    SASSERT((u == 1) == (r == BR_REWRITE2));
+    SASSERT((u == 2) == (r == BR_REWRITE3));
+    SASSERT((u >= 3) == (r == BR_REWRITE_FULL));
+    return r;
+}
+
+class rewriter_exception : public tactic_exception {
+public:                                                
+    rewriter_exception(char const * msg):tactic_exception(msg) {}
+};
+
+#endif

src/rewriter/th_rewriter.cpp

@@ -0,0 +1,770 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    th_rewriter.h
+
+Abstract:
+
+    Rewriter for applying all builtin (cheap) theory rewrite rules.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-07
+
+Notes:
+
+--*/
+#include"th_rewriter.h"
+#include"bool_rewriter.h"
+#include"arith_rewriter.h"
+#include"bv_rewriter.h"
+#include"datatype_rewriter.h"
+#include"array_rewriter.h"
+#include"float_rewriter.h"
+#include"dl_rewriter.h"
+#include"rewriter_def.h"
+#include"expr_substitution.h"
+#include"ast_smt2_pp.h"
+#include"cooperate.h"
+#include"var_subst.h"
+#include"ast_util.h"
+#include"well_sorted.h"
+
+struct th_rewriter_cfg : public default_rewriter_cfg {
+    bool_rewriter       m_b_rw;
+    arith_rewriter      m_a_rw;
+    bv_rewriter         m_bv_rw;
+    array_rewriter      m_ar_rw;
+    datatype_rewriter   m_dt_rw;
+    float_rewriter      m_f_rw;
+    dl_rewriter         m_dl_rw;
+    arith_util          m_a_util;
+    bv_util             m_bv_util;
+    unsigned long long  m_max_memory; // in bytes
+    unsigned            m_max_steps;
+    bool                m_pull_cheap_ite;
+    bool                m_flat;
+    bool                m_cache_all;
+    bool                m_push_ite_arith;
+    bool                m_push_ite_bv;
+
+    // substitution support
+    expr_dependency_ref m_used_dependencies; // set of dependencies of used substitutions
+    expr_substitution * m_subst;
+
+    ast_manager & m() const { return m_b_rw.m(); }
+
+    void updt_local_params(params_ref const & p) {
+        m_flat           = p.get_bool(":flat", true);
+        m_max_memory     = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+        m_max_steps      = p.get_uint(":max-steps", UINT_MAX);
+        m_pull_cheap_ite = p.get_bool(":pull-cheap-ite", false);
+        m_cache_all      = p.get_bool(":cache-all", false);
+        m_push_ite_arith = p.get_bool(":push-ite-arith", false);
+        m_push_ite_bv    = p.get_bool(":push-ite-bv", false);
+    }
+        
+    void updt_params(params_ref const & p) {
+        m_b_rw.updt_params(p);
+        m_a_rw.updt_params(p);
+        m_bv_rw.updt_params(p);
+        m_ar_rw.updt_params(p);
+        updt_local_params(p);
+    }
+
+    bool flat_assoc(func_decl * f) const { 
+        if (!m_flat) return false;
+        family_id fid = f->get_family_id();
+        if (fid == null_family_id)
+            return false;
+        decl_kind k   = f->get_decl_kind();
+        if (fid == m_b_rw.get_fid())
+            return k == OP_AND || k == OP_OR;
+        if (fid == m_a_rw.get_fid())
+            return k == OP_ADD;
+        if (fid == m_bv_rw.get_fid())
+            return k == OP_BADD || k == OP_BOR || k == OP_BAND || k == OP_BXOR;
+        return false;
+    }
+
+    bool rewrite_patterns() const { return false; }
+    
+    bool cache_all_results() const { return m_cache_all; }
+
+    bool max_steps_exceeded(unsigned num_steps) const { 
+        cooperate("simplifier");
+        if (memory::get_allocation_size() > m_max_memory)
+            throw rewriter_exception(TACTIC_MAX_MEMORY_MSG);
+        return num_steps > m_max_steps;
+    }
+
+    // Return true if t is of the form
+    //    (= t #b0)
+    //    (= t #b1)
+    //    (= #b0 t)
+    //    (= #b1 t)
+    bool is_eq_bit(expr * t, expr * & x, unsigned & val) {
+        if (!m().is_eq(t))
+            return false;
+        expr * lhs = to_app(t)->get_arg(0);
+        if (!m_bv_rw.is_bv(lhs))
+            return false;
+        if (m_bv_rw.get_bv_size(lhs) != 1)
+            return false;
+        expr * rhs = to_app(t)->get_arg(1);
+        rational v;
+        unsigned sz;
+        if (m_bv_rw.is_numeral(lhs, v, sz)) {
+            x    = rhs;
+            val  = v.get_unsigned();
+            SASSERT(val == 0 || val == 1);
+            return true;
+        }
+        if (m_bv_rw.is_numeral(rhs, v, sz)) {
+            x   = lhs;
+            val  = v.get_unsigned();
+            SASSERT(val == 0 || val == 1);
+            return true;
+        }
+        return false;
+    }
+
+    // (iff (= x bit1) A)
+    // --->
+    // (= x (ite A bit1 bit0))
+    br_status apply_tamagotchi(expr * lhs, expr * rhs, expr_ref & result) {
+        expr * x;
+        unsigned val;
+        if (is_eq_bit(lhs, x, val)) {
+            result = m().mk_eq(x, m().mk_ite(rhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1)));
+            return BR_REWRITE2;
+        }
+        if (is_eq_bit(rhs, x, val)) {
+            result = m().mk_eq(x, m().mk_ite(lhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1)));
+            return BR_REWRITE2;
+        }
+        return BR_FAILED;
+    }
+
+    br_status reduce_app_core(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+        family_id fid = f->get_family_id();
+        if (fid == null_family_id)
+            return BR_FAILED;
+        br_status st = BR_FAILED;
+        if (fid == m_b_rw.get_fid()) {
+            decl_kind k = f->get_decl_kind();
+            if (k == OP_EQ) {
+                // theory dispatch for =
+                SASSERT(num == 2);
+                family_id s_fid = m().get_sort(args[0])->get_family_id();
+                if (s_fid == m_a_rw.get_fid())
+                    st = m_a_rw.mk_eq_core(args[0], args[1], result);
+                else if (s_fid == m_bv_rw.get_fid())
+                    st = m_bv_rw.mk_eq_core(args[0], args[1], result);
+                else if (s_fid == m_dt_rw.get_fid())
+                    st = m_dt_rw.mk_eq_core(args[0], args[1], result);
+                else if (s_fid == m_f_rw.get_fid())
+                    st = m_f_rw.mk_eq_core(args[0], args[1], result);
+
+                if (st != BR_FAILED)
+                    return st;
+            }
+            if (k == OP_EQ || k == OP_IFF) {
+                SASSERT(num == 2);
+                st = apply_tamagotchi(args[0], args[1], result);            
+                if (st != BR_FAILED)
+                    return st;
+            }
+            return m_b_rw.mk_app_core(f, num, args, result);
+        }
+        if (fid == m_a_rw.get_fid())
+            return m_a_rw.mk_app_core(f, num, args, result);
+        if (fid == m_bv_rw.get_fid())
+            return m_bv_rw.mk_app_core(f, num, args, result);
+        if (fid == m_ar_rw.get_fid())
+            return m_ar_rw.mk_app_core(f, num, args, result);
+        if (fid == m_dt_rw.get_fid())
+            return m_dt_rw.mk_app_core(f, num, args, result);
+        if (fid == m_f_rw.get_fid())
+            return m_f_rw.mk_app_core(f, num, args, result);
+        if (fid == m_dl_rw.get_fid())
+            return m_dl_rw.mk_app_core(f, num, args, result);
+        return BR_FAILED;
+    }
+
+    // auxiliary function for pull_ite_core
+    expr * mk_eq_value(expr * lhs, expr * value) {
+        SASSERT(m().is_value(value));
+        if (m().is_value(lhs)) {
+            return lhs == value ? m().mk_true() : m().mk_false();
+        }
+        return m().mk_eq(lhs, value);
+    }
+
+    template<bool SWAP>
+    br_status pull_ite_core(func_decl * p, app * ite, app * value, expr_ref & result) {
+        if (m().is_eq(p)) {
+            result = m().mk_ite(ite->get_arg(0),
+                                mk_eq_value(ite->get_arg(1), value),
+                                mk_eq_value(ite->get_arg(2), value));
+            return BR_REWRITE2;
+        }
+        else {
+            if (SWAP) {
+                result = m().mk_ite(ite->get_arg(0), 
+                                    m().mk_app(p, value, ite->get_arg(1)),
+                                    m().mk_app(p, value, ite->get_arg(2)));
+                return BR_REWRITE2;
+            }
+            else {
+                result = m().mk_ite(ite->get_arg(0), 
+                                    m().mk_app(p, ite->get_arg(1), value),
+                                    m().mk_app(p, ite->get_arg(2), value));
+                return BR_REWRITE2;
+            }
+        }
+    }
+
+    // Return true if t is an ite-value-tree form defined as:
+    //    ite-value-tree := (ite c <subtree> <subtree>)
+    //    subtree        := value
+    //                   |  (ite c <subtree> <subtree>)
+    //    
+    bool is_ite_value_tree(expr * t) {
+        if (!m().is_ite(t))
+            return false;
+        ptr_buffer<app> todo;
+        todo.push_back(to_app(t));
+        while (!todo.empty()) {
+            app * ite = todo.back();
+            todo.pop_back();
+            expr * arg1 = ite->get_arg(1);
+            expr * arg2 = ite->get_arg(2);
+
+            if (m().is_ite(arg1) && arg1->get_ref_count() == 1) // do not apply on shared terms, since it may blowup
+                todo.push_back(to_app(arg1));
+            else if (!m().is_value(arg1))
+                return false;
+
+            if (m().is_ite(arg2) && arg2->get_ref_count() == 1) // do not apply on shared terms, since it may blowup
+                todo.push_back(to_app(arg2));
+            else if (!m().is_value(arg2))
+                return false;
+        }
+        return true;
+    }
+    
+    br_status pull_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+        if (num == 2 && m().is_bool(f->get_range()) && !m().is_bool(args[0])) {
+            if (m().is_ite(args[0])) {
+                if (m().is_value(args[1]))
+                    return pull_ite_core<false>(f, to_app(args[0]), to_app(args[1]), result);
+                if (m().is_ite(args[1]) && to_app(args[0])->get_arg(0) == to_app(args[1])->get_arg(0)) {
+                    // (p (ite C A1 B1) (ite C A2 B2)) --> (ite (p A1 A2) (p B1 B2))
+                    result = m().mk_ite(to_app(args[0])->get_arg(0),
+                                        m().mk_app(f, to_app(args[0])->get_arg(1), to_app(args[1])->get_arg(1)),
+                                        m().mk_app(f, to_app(args[0])->get_arg(2), to_app(args[1])->get_arg(2)));
+                    return BR_REWRITE2;
+                }
+            }
+            if (m().is_ite(args[1]) && m().is_value(args[0]))
+                return pull_ite_core<true>(f, to_app(args[1]), to_app(args[0]), result);
+        }
+        family_id fid = f->get_family_id();
+        if (num == 2 && (fid == m().get_basic_family_id() || fid == m_a_rw.get_fid() || fid == m_bv_rw.get_fid())) {
+            // (f v3 (ite c v1 v2)) --> (ite v (f v3 v1) (f v3 v2))
+            if (m().is_value(args[0]) && is_ite_value_tree(args[1]))
+                return pull_ite_core<true>(f, to_app(args[1]), to_app(args[0]), result);
+
+            // (f (ite c v1 v2) v3) --> (ite v (f v1 v3) (f v2 v3))
+            if (m().is_value(args[1]) && is_ite_value_tree(args[0]))
+                return pull_ite_core<false>(f, to_app(args[0]), to_app(args[1]), result);
+        }
+        return BR_FAILED;
+    }
+
+    br_status pull_ite(expr_ref & result) {
+        expr * t = result.get();
+        if (is_app(t)) {
+            br_status st = pull_ite(to_app(t)->get_decl(), to_app(t)->get_num_args(), to_app(t)->get_args(), result);
+            if (st != BR_FAILED)
+                return st;
+        }
+        return BR_DONE;
+    }
+
+    bool is_arith_bv_app(expr * t) const {
+        if (!is_app(t))
+            return false;
+        family_id fid = to_app(t)->get_family_id();
+        return ((fid == m_a_rw.get_fid() && m_push_ite_arith) || 
+                (fid == m_bv_rw.get_fid() && m_push_ite_bv));
+    }
+
+    bool get_neutral_elem(app * t, expr_ref & n) {
+        family_id fid = t->get_family_id();
+        if (fid == m_a_rw.get_fid()) {
+            switch (t->get_decl_kind()) {
+            case OP_ADD: n = m_a_util.mk_numeral(rational(0), m().get_sort(t)); return true;
+            case OP_MUL: n = m_a_util.mk_numeral(rational(1), m().get_sort(t)); return true;
+            default:
+                return false;
+            }
+        }
+        if (fid == m_bv_rw.get_fid()) {
+            switch (t->get_decl_kind()) {
+            case OP_BADD: n = m_bv_util.mk_numeral(rational(0), m().get_sort(t)); return true;
+            case OP_BMUL: n = m_bv_util.mk_numeral(rational(1), m().get_sort(t)); return true;
+            default:
+                return false;
+            }
+        }
+        return false;
+    }
+    
+    /**
+       \brief Try to "unify" t1 and t2
+       Examples
+         (+ 2 a) (+ 3 a) -->  2, 3, a
+         (+ 2 a) a       -->  2, 0, a
+         ...
+    */
+    bool unify_core(app * t1, expr * t2, expr_ref & new_t1, expr_ref & new_t2, expr_ref & c, bool & first) {
+        if (t1->get_num_args() != 2)
+            return false;
+        expr * a1 = t1->get_arg(0);
+        expr * b1 = t1->get_arg(1);
+        if (t2 == b1) {
+            if (get_neutral_elem(t1, new_t2)) {
+                new_t1 = a1;
+                c      = b1;
+                first  = false;
+                return true;
+            }
+        }
+        else if (t2 == a1) {
+            if (get_neutral_elem(t1, new_t2)) {
+                new_t1 = b1;
+                c      = a1;
+                first  = true;
+                return true;
+            }
+        }
+        else if (is_app_of(t2, t1->get_decl()) && to_app(t2)->get_num_args() == 2) {
+            expr * a2 = to_app(t2)->get_arg(0);
+            expr * b2 = to_app(t2)->get_arg(1);
+            if (b1 == b2) {
+                new_t1 = a1;
+                new_t2 = a2;
+                c      = b2;
+                first  = false;
+                return true;
+            }
+            if (a1 == a2) {
+                new_t1 = b1;
+                new_t2 = b2;
+                c      = a1;
+                first  = true;
+                return true;
+            }
+            if (t1->get_decl()->is_commutative()) {
+                if (a1 == b2) {
+                    new_t1 = b1;
+                    new_t2 = a2;
+                    c      = a1;
+                    first  = true; // doesn't really matter for commutative ops.
+                    return true;
+                }
+                if (b1 == a2) {
+                    new_t1 = a1;
+                    new_t2 = b2;
+                    c      = b1;
+                    first  = false; // doesn't really matter for commutative ops.
+                    return true;
+                }
+            }
+        }
+        return false;
+    }
+
+    // Return true if t1 and t2 are of the form:
+    //   t + a1*x1 + ... + an*xn
+    //   t' + a1*x1 + ... + an*xn
+    // Store t in new_t1, t' in new_t2 and (a1*x1 + ... + an*xn) in c.
+    bool unify_add(app * t1, expr * t2, expr_ref & new_t1, expr_ref & new_t2, expr_ref & c) {
+        unsigned num1 = t1->get_num_args();
+        expr * const * ms1 = t1->get_args();
+        if (num1 < 2)
+            return false;
+        unsigned num2;
+        expr * const * ms2;
+        if (m_a_util.is_add(t2)) {
+            num2 = to_app(t2)->get_num_args();
+            ms2  = to_app(t2)->get_args();
+        }
+        else {
+            num2 = 1;
+            ms2  = &t2;
+        }
+        if (num1 != num2 && num1 != num2 + 1 && num1 != num2 - 1)
+            return false;
+        new_t1 = 0;
+        new_t2 = 0;
+        expr_fast_mark1 visited1;
+        expr_fast_mark2 visited2;
+        for (unsigned i = 0; i < num1; i++) {
+            expr * arg = ms1[i];
+            visited1.mark(arg);
+        }
+        for (unsigned i = 0; i < num2; i++) {
+            expr * arg = ms2[i];
+            visited2.mark(arg);
+            if (visited1.is_marked(arg))
+                continue;
+            if (new_t2)
+                return false; // more than one missing term
+            new_t2 = arg;
+        }
+        for (unsigned i = 0; i < num1; i++) {
+            expr * arg = ms1[i];
+            if (visited2.is_marked(arg))
+                continue;
+            if (new_t1)
+                return false; // more than one missing term
+            new_t1 = arg;
+        }
+        // terms matched...
+        bool is_int = m_a_util.is_int(t1);
+        if (!new_t1) 
+            new_t1 = m_a_util.mk_numeral(rational(0), is_int);
+        if (!new_t2)
+            new_t2 = m_a_util.mk_numeral(rational(0), is_int);
+        // mk common part
+        ptr_buffer<expr> args;
+        for (unsigned i = 0; i < num1; i++) {
+            expr * arg = ms1[i];
+            if (arg == new_t1.get())
+                continue;
+            args.push_back(arg);
+        }
+        SASSERT(!args.empty());
+        if (args.size() == 1) 
+            c = args[0];
+        else
+            c = m_a_util.mk_add(args.size(), args.c_ptr());
+        return true;
+    }
+
+    bool unify(expr * t1, expr * t2, func_decl * & f, expr_ref & new_t1, expr_ref & new_t2, expr_ref & c, bool & first) {
+#if 0
+        // Did not work for ring benchmarks
+
+        // Hack for handling more complex cases of + apps
+        // such as (+ 2 t1 t2 t3) and (+ 3 t3 t2 t1)
+        if (m_a_util.is_add(t1)) {
+            first = true; // doesn't matter for AC ops
+            f     = to_app(t1)->get_decl();
+            if (unify_add(to_app(t1), t2, new_t1, new_t2, c))
+                return true;
+        }
+        if (m_a_util.is_add(t2)) {
+            first = true; // doesn't matter for AC ops
+            f     = to_app(t2)->get_decl();
+            if (unify_add(to_app(t2), t1, new_t2, new_t1, c))
+                return true;
+        }
+#endif
+
+        if (is_arith_bv_app(t1)) {
+            f = to_app(t1)->get_decl();
+            return unify_core(to_app(t1), t2, new_t1, new_t2, c, first);
+        }
+        else {
+            f = to_app(t2)->get_decl();
+            return unify_core(to_app(t2), t1, new_t2, new_t1, c, first);
+        }
+    }
+
+    // Apply transformations of the form
+    //
+    // (ite c (+ k1 a) (+ k2 a)) --> (+ (ite c k1 k2) a)   
+    // (ite c (* k1 a) (* k2 a)) --> (* (ite c k1 k2) a)
+    //
+    // These transformations are useful for bit-vector problems, since
+    // they will minimize the number of adders/multipliers/etc
+    br_status push_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
+        if (!m().is_ite(f))
+            return BR_FAILED;
+        expr * c = args[0];
+        expr * t = args[1];
+        expr * e = args[2];
+        func_decl * f_prime = 0;
+        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";);
+        if (unify(t, e, f_prime, new_t, new_e, common, first)) {
+            if (first)
+                result = m().mk_app(f_prime, common, m().mk_ite(c, new_t, new_e));
+            else 
+                result = m().mk_app(f_prime, m().mk_ite(c, new_t, new_e), common);
+            return BR_DONE;
+        }
+        TRACE("push_ite", tout << "failed\n";);
+        return BR_FAILED;
+    }
+
+    br_status push_ite(expr_ref & result) {
+        expr * t = result.get();
+        if (m().is_ite(t)) {
+            br_status st = push_ite(to_app(t)->get_decl(), to_app(t)->get_num_args(), to_app(t)->get_args(), result);
+            if (st != BR_FAILED)
+                return st;
+        }
+        return BR_DONE;
+    }
+
+    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+        result_pr = 0;
+        br_status st = reduce_app_core(f, num, args, result);
+        if (st != BR_DONE && st != BR_FAILED) {
+            CTRACE("th_rewriter_step", st != BR_FAILED, 
+                   tout << f->get_name() << "\n";
+                   for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
+                   tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";);
+            return st;
+        }
+        if (m_push_ite_bv || m_push_ite_arith) {
+            if (st == BR_FAILED)
+                st = push_ite(f, num, args, result);
+            else
+                st = push_ite(result);
+        }
+        if (m_pull_cheap_ite) {
+            if (st == BR_FAILED)
+                st = pull_ite(f, num, args, result);
+            else
+                st = pull_ite(result);
+        }
+        CTRACE("th_rewriter_step", st != BR_FAILED, 
+               tout << f->get_name() << "\n";
+               for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n";
+               tout << "---------->\n" << mk_ismt2_pp(result, m()) << "\n";);
+        return st;
+    }
+
+    bool reduce_quantifier(quantifier * old_q, 
+                           expr * new_body, 
+                           expr * const * new_patterns, 
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr) {
+        quantifier_ref q1(m());
+        proof * p1 = 0;
+        if (is_quantifier(new_body) && 
+            to_quantifier(new_body)->is_forall() == old_q->is_forall() &&
+            !old_q->has_patterns() &&
+            !to_quantifier(new_body)->has_patterns()) {
+        
+            quantifier * nested_q = to_quantifier(new_body);
+            
+            ptr_buffer<sort> sorts;
+            buffer<symbol>   names;   
+            sorts.append(old_q->get_num_decls(), old_q->get_decl_sorts());
+            names.append(old_q->get_num_decls(), old_q->get_decl_names());
+            sorts.append(nested_q->get_num_decls(), nested_q->get_decl_sorts());
+            names.append(nested_q->get_num_decls(), nested_q->get_decl_names());
+            
+            q1 = m().mk_quantifier(old_q->is_forall(),
+                                   sorts.size(),
+                                   sorts.c_ptr(),
+                                   names.c_ptr(),
+                                   nested_q->get_expr(),
+                                   std::min(old_q->get_weight(), nested_q->get_weight()),
+                                   old_q->get_qid(),
+                                   old_q->get_skid(),
+                                   0, 0, 0, 0);
+            
+            SASSERT(is_well_sorted(m(), q1));
+            
+            if (m().proofs_enabled()) {
+                SASSERT(old_q->get_expr() == new_body);
+                p1 = m().mk_pull_quant(old_q, q1);
+            }
+        }
+        else {
+            ptr_buffer<expr> new_patterns_buf;
+            ptr_buffer<expr> new_no_patterns_buf;
+            
+            new_patterns_buf.append(old_q->get_num_patterns(), new_patterns);
+            new_no_patterns_buf.append(old_q->get_num_no_patterns(), new_no_patterns);
+
+            remove_duplicates(new_patterns_buf);
+            remove_duplicates(new_no_patterns_buf);
+            
+            q1 = m().update_quantifier(old_q, 
+                                       new_patterns_buf.size(), new_patterns_buf.c_ptr(), new_no_patterns_buf.size(), new_no_patterns_buf.c_ptr(),
+                                       new_body);
+            TRACE("reduce_quantifier", tout << mk_ismt2_pp(old_q, m()) << "\n----->\n" << mk_ismt2_pp(q1, m()) << "\n";);
+            SASSERT(is_well_sorted(m(), q1));
+        }
+    
+        elim_unused_vars(m(), q1, result);
+
+        TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << mk_ismt2_pp(result, m()) << "\n";);
+    
+        result_pr = 0;
+        if (m().proofs_enabled()) {
+            proof * p2 = 0;
+            if (q1.get() != result.get())
+                p2 = m().mk_elim_unused_vars(q1, result);
+            result_pr = m().mk_transitivity(p1, p2);
+        }
+        return true;
+    }
+
+    th_rewriter_cfg(ast_manager & m, params_ref const & p):
+        m_b_rw(m, p),
+        m_a_rw(m, p),
+        m_bv_rw(m, p),
+        m_ar_rw(m, p),
+        m_dt_rw(m),
+        m_f_rw(m, p),
+        m_dl_rw(m),
+        m_a_util(m),
+        m_bv_util(m),
+        m_used_dependencies(m),
+        m_subst(0) {
+        updt_local_params(p);
+    }
+
+    void set_substitution(expr_substitution * s) {
+        reset();
+        m_subst = s;
+    }
+
+    void reset() {
+        m_subst = 0;
+    }
+
+    bool get_subst(expr * s, expr * & t, proof * & pr) {
+        if (m_subst == 0)
+            return false;
+        expr_dependency * d = 0;
+        if (m_subst->find(s, t, pr, d)) {
+            m_used_dependencies = m().mk_join(m_used_dependencies, d);
+            return true;
+        }
+        return false;
+    }
+
+    void set_cancel(bool f) {
+        m_a_rw.set_cancel(f);
+    }
+};
+
+template class rewriter_tpl<th_rewriter_cfg>;
+
+struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
+    th_rewriter_cfg m_cfg;
+    imp(ast_manager & m, params_ref const & p):
+        rewriter_tpl<th_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
+        m_cfg(m, p) {
+    }
+};
+
+th_rewriter::th_rewriter(ast_manager & m, params_ref const & p):
+    m_params(p) {
+    m_imp = alloc(imp, m, p);
+}
+
+ast_manager & th_rewriter::m() const {
+    return m_imp->m();
+}
+
+void th_rewriter::updt_params(params_ref const & p) {
+    m_params = p;
+    m_imp->cfg().updt_params(p);
+}
+
+void th_rewriter::get_param_descrs(param_descrs & r) {
+    bool_rewriter::get_param_descrs(r);
+    arith_rewriter::get_param_descrs(r);
+    bv_rewriter::get_param_descrs(r);
+    array_rewriter::get_param_descrs(r);
+    insert_max_memory(r);
+    insert_max_steps(r);
+    r.insert(":push-ite-arith", CPK_BOOL, "(default: false) push if-then-else over arithmetic terms.");
+    r.insert(":push-ite-bv", CPK_BOOL, "(default: false) push if-then-else over bit-vector terms.");
+    r.insert(":pull-cheap-ite", CPK_BOOL, "(default: false) pull if-then-else terms when cheap.");
+    r.insert(":cache-all", CPK_BOOL, "(default: false) cache all intermediate results.");
+}
+
+th_rewriter::~th_rewriter() {
+    dealloc(m_imp);
+}
+
+unsigned th_rewriter::get_cache_size() const {
+    return m_imp->get_cache_size();
+}
+
+unsigned th_rewriter::get_num_steps() const {
+    return m_imp->get_num_steps();
+}
+
+void th_rewriter::set_cancel(bool f) {
+    #pragma omp critical (th_rewriter)
+    {
+        m_imp->set_cancel(f);
+        m_imp->cfg().set_cancel(f);
+    }
+}
+
+void th_rewriter::cleanup() {
+    ast_manager & m = m_imp->m();
+    #pragma omp critical (th_rewriter)
+    {
+        dealloc(m_imp);
+        m_imp = alloc(imp, m, m_params);
+    }
+}
+
+void th_rewriter::reset() {
+    m_imp->reset();
+    m_imp->cfg().reset();
+}
+
+void th_rewriter::operator()(expr_ref & term) {
+    expr_ref result(term.get_manager());
+    m_imp->operator()(term, result);
+    term = result;
+}
+
+void th_rewriter::operator()(expr * t, expr_ref & result) {
+    m_imp->operator()(t, result);
+}
+
+void th_rewriter::operator()(expr * t, expr_ref & result, proof_ref & result_pr) {
+    m_imp->operator()(t, result, result_pr);
+}
+
+void th_rewriter::operator()(expr * n, unsigned num_bindings, expr * const * bindings, expr_ref & result) {
+    m_imp->operator()(n, num_bindings, bindings, result);
+}
+
+void th_rewriter::set_substitution(expr_substitution * s) {
+    m_imp->reset(); // reset the cache
+    m_imp->cfg().set_substitution(s);
+}
+
+expr_dependency * th_rewriter::get_used_dependencies() {
+    return m_imp->cfg().m_used_dependencies;
+}
+
+void th_rewriter::reset_used_dependencies() {
+    if (get_used_dependencies() != 0) {
+        set_substitution(m_imp->cfg().m_subst); // reset cache preserving subst
+        m_imp->cfg().m_used_dependencies = 0;
+    }
+}

src/rewriter/th_rewriter.h

@@ -0,0 +1,65 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    th_rewriter.h
+
+Abstract:
+
+    Rewriter for applying all builtin (cheap) theory rewrite rules.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-07
+
+Notes:
+
+--*/
+#ifndef _TH_REWRITER_H_
+#define _TH_REWRITER_H_
+
+#include"ast.h"
+#include"rewriter_types.h"
+#include"params.h"
+
+class expr_substitution;
+
+class th_rewriter {
+    struct     imp;
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    th_rewriter(ast_manager & m, params_ref const & p = params_ref());
+    ~th_rewriter();
+
+    ast_manager & m () const;
+
+    void updt_params(params_ref const & p);
+    static void get_param_descrs(param_descrs & r);
+
+    unsigned get_cache_size() const;
+    unsigned get_num_steps() const;
+
+    void operator()(expr_ref& term);
+    void operator()(expr * t, expr_ref & result);
+    void operator()(expr * t, expr_ref & result, proof_ref & result_pr);
+    void operator()(expr * n, unsigned num_bindings, expr * const * bindings, expr_ref & result);
+
+    void cancel() { set_cancel(true); }
+    void reset_cancel() { set_cancel(false); }
+    void set_cancel(bool f);
+    void cleanup();
+    void reset();
+
+    void set_substitution(expr_substitution * s);
+    
+    // Dependency tracking is very coarse. 
+    // The rewriter just keeps accumulating the dependencies of the used substitutions.
+    // The following methods are used to recover and reset them.
+    // Remark: reset_used_dependecies will reset the internal cache if get_used_dependencies() != 0
+    expr_dependency * get_used_dependencies();
+    void reset_used_dependencies();
+};
+
+#endif

src/rewriter/var_subst.cpp

@@ -0,0 +1,211 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    var_subst.cpp
+
+Abstract:
+
+    Variable substitution.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-10
+
+Notes:
+
+--*/
+#include"var_subst.h"
+#include"used_vars.h"
+#include"ast_ll_pp.h"
+#include"ast_pp.h"
+#include"ast_smt2_pp.h"
+#include"well_sorted.h"
+#include"for_each_expr.h"
+
+void var_subst::operator()(expr * n, unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(is_well_sorted(result.m(), n));
+    m_reducer.reset();
+    if (m_std_order)
+	m_reducer.set_inv_bindings(num_args, args);
+    else
+        m_reducer.set_bindings(num_args, args);
+    m_reducer(n, result);
+    SASSERT(is_well_sorted(m_reducer.m(), result));
+    TRACE("var_subst_bug",
+          tout << "m_std_order: " << m_std_order << "\n" << mk_ismt2_pp(n, m_reducer.m()) << "\nusing\n";
+          for (unsigned i = 0; i < num_args; i++) tout << mk_ismt2_pp(args[i], m_reducer.m()) << "\n";
+          tout << "\n------>\n";
+          tout << mk_ismt2_pp(result, m_reducer.m()) << "\n";);
+}
+
+void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & result) {
+    SASSERT(is_well_sorted(m, q));
+    if (is_ground(q->get_expr())) {
+        // ignore patterns if the body is a ground formula.
+        result = q->get_expr();
+        return;
+    }
+    if (!q->may_have_unused_vars()) {
+        result = q;
+        return;
+    }
+    used_vars used;
+    used.process(q->get_expr());
+    unsigned num_patterns = q->get_num_patterns();
+    for (unsigned i = 0; i < num_patterns; i++)
+        used.process(q->get_pattern(i));
+    unsigned num_no_patterns = q->get_num_no_patterns();
+    for (unsigned i = 0; i < num_no_patterns; i++)
+        used.process(q->get_no_pattern(i));
+
+    unsigned num_decls = q->get_num_decls();
+    if (used.uses_all_vars(num_decls)) {
+        q->set_no_unused_vars();
+        result = q;
+        return;
+    }
+
+    ptr_buffer<sort>  used_decl_sorts; 
+    buffer<symbol>    used_decl_names;
+    for (unsigned i = 0; i < num_decls; ++i) {
+        if (used.contains(num_decls - i - 1)) {
+            used_decl_sorts.push_back(q->get_decl_sort(i));
+            used_decl_names.push_back(q->get_decl_name(i));
+        }
+    }
+    
+    unsigned         num_removed = 0;
+    expr_ref_buffer  var_mapping(m);
+    int              next_idx = 0;
+    unsigned         sz = used.get_max_found_var_idx_plus_1();
+
+    for (unsigned i = 0; i < num_decls; ++i) {
+        sort * s = used.contains(i);
+        if (s) {
+            var_mapping.push_back(m.mk_var(next_idx, s));
+            next_idx++;
+        }
+        else {
+            num_removed++;
+            var_mapping.push_back(0);
+        }
+    }
+    // (VAR 0) is in the first position of var_mapping.
+
+    for (unsigned i = num_decls; i < sz; i++) {
+        sort * s = used.contains(i);
+        if (s)
+            var_mapping.push_back(m.mk_var(i - num_removed, s));
+        else
+            var_mapping.push_back(0);
+    }
+    
+    
+    // Remark: 
+    // (VAR 0) should be in the last position of var_mapping.
+    // ...
+    // (VAR (var_mapping.size() - 1)) should be in the first position.
+    std::reverse(var_mapping.c_ptr(), var_mapping.c_ptr() + var_mapping.size());
+
+    expr_ref  new_expr(m);
+    var_subst subst(m);
+    
+    subst(q->get_expr(), var_mapping.size(), var_mapping.c_ptr(), new_expr);
+    
+    if (num_removed == num_decls) {
+        result = new_expr;
+        return;
+    }
+
+    expr_ref tmp(m);
+    expr_ref_buffer new_patterns(m);
+    expr_ref_buffer new_no_patterns(m);
+    
+    for (unsigned i = 0; i < num_patterns; i++) {
+        subst(q->get_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
+        new_patterns.push_back(tmp);
+    }
+    for (unsigned i = 0; i < num_no_patterns; i++) {
+        subst(q->get_no_pattern(i), var_mapping.size(), var_mapping.c_ptr(), tmp);
+        new_no_patterns.push_back(tmp);
+    }
+    
+    result = m.mk_quantifier(q->is_forall(),
+                             used_decl_sorts.size(),
+                             used_decl_sorts.c_ptr(),
+                             used_decl_names.c_ptr(),
+                             new_expr,
+                             q->get_weight(),
+                             q->get_qid(),
+                             q->get_skid(),
+                             num_patterns,
+                             new_patterns.c_ptr(),
+                             num_no_patterns,
+                             new_no_patterns.c_ptr());
+    to_quantifier(result)->set_no_unused_vars();
+    SASSERT(is_well_sorted(m, result));
+}
+
+void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref & result) {
+    var_subst subst(m);
+    expr_ref new_expr(m);
+    subst(q->get_expr(), q->get_num_decls(), exprs, new_expr);
+    TRACE("var_subst", tout << mk_pp(q, m) << "\n" << mk_pp(new_expr, m) << "\n";);
+    inv_var_shifter shift(m);
+    shift(new_expr, q->get_num_decls(), result);
+    SASSERT(is_well_sorted(m, result));
+    TRACE("instantiate_bug", tout << mk_ismt2_pp(q, m) << "\nusing\n";
+          for (unsigned i = 0; i < q->get_num_decls(); i++) tout << mk_ismt2_pp(exprs[i], m) << "\n";
+          tout << "\n----->\n" << mk_ismt2_pp(result, m) << "\n";);
+}
+
+static void get_free_vars_offset(expr* e, unsigned offset, ptr_vector<sort>& sorts) {
+    ast_mark mark;
+    ptr_vector<expr> todo;
+    todo.push_back(e);
+    while (!todo.empty()) {
+        e = todo.back();
+        todo.pop_back();
+        if (mark.is_marked(e)) {
+            continue;
+        }
+        mark.mark(e, true);
+        switch(e->get_kind()) {
+        case AST_QUANTIFIER: {
+            quantifier* q = to_quantifier(e);
+            get_free_vars_offset(q->get_expr(), offset+q->get_num_decls(), sorts);
+            break;
+        }
+        case AST_VAR: {
+            var* v = to_var(e);
+            if (v->get_idx() >= offset) {
+                unsigned idx = v->get_idx()-offset;
+                if (sorts.size() <= idx) {
+                    sorts.resize(idx+1);
+                }
+                if (!sorts[idx]) {
+                    sorts[idx] = v->get_sort();
+                }
+                SASSERT(sorts[idx] == v->get_sort());
+            }
+            break;
+        }
+        case AST_APP: {
+            app* a = to_app(e);
+            for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                todo.push_back(a->get_arg(i));
+            }
+            break;
+        }
+        default:
+            UNREACHABLE();
+        }
+    }
+}
+
+
+void get_free_vars(expr* e, ptr_vector<sort>& sorts) {
+    get_free_vars_offset(e, 0, sorts);
+}

src/rewriter/var_subst.h

@@ -0,0 +1,78 @@
+/*++
+Copyright (c) 2007 Microsoft Corporation
+
+Module Name:
+
+    var_subst.h
+
+Abstract:
+
+    Variable substitution.
+
+Author:
+
+    Leonardo (leonardo) 2008-01-10
+
+Notes:
+
+--*/
+#ifndef _VAR_SUBST_H_
+#define _VAR_SUBST_H_
+
+#include"rewriter.h"
+
+/**
+   \brief Alias for var_shifter class.
+*/
+typedef var_shifter shift_vars;
+
+/**
+   \brief Variable substitution functor. It substitutes variables by expressions.
+   The expressions may contain variables.
+*/
+class var_subst { 
+    beta_reducer   m_reducer;
+    bool           m_std_order;
+public:
+    var_subst(ast_manager & m, bool std_order = true):m_reducer(m), m_std_order(std_order) {}
+    bool std_order() const { return m_std_order; }
+
+    /**
+       When std_order() == true, 
+       I'm using the same standard used in quantifier instantiation.
+       (VAR 0) is stored in the last position of the array.
+       ...
+       (VAR (num_args - 1)) is stored in the first position of the array.
+
+       Otherwise, (VAR 0) is stored in the first position, (VAR 1) in the second, and so on.
+    */
+    void operator()(expr * n, unsigned num_args, expr * const * args, expr_ref & result);
+    void reset() { m_reducer.reset(); }
+};
+
+/**
+   \brief Eliminate the unused variables from \c q. Store the result in \c r.
+*/
+void elim_unused_vars(ast_manager & m, quantifier * q, expr_ref & r);
+
+/**
+   \brief Instantiate quantifier q using the given exprs.
+   The vector exprs should contain at least q->get_num_decls() expressions.
+
+   I'm using the same standard used in quantifier instantiation.
+   (VAR 0) is stored in the last position of the array.
+   ...
+   (VAR (q->get_num_decls() - 1)) is stored in the first position of the array.
+*/
+void instantiate(ast_manager & m, quantifier * q, expr * const * exprs, expr_ref & result);
+
+/**
+   \brief Enumerate set of free variables in expression.
+
+   Return the sorts of the free variables.
+*/
+void get_free_vars(expr* e, ptr_vector<sort>& sorts);
+
+#endif
+
+