using a consistent naming convention for naming tactic subfolders

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

src/tactic/core/cofactor_elim_term_ite.cpp

@@ -0,0 +1,712 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    cofactor_elim_term_ite.cpp
+
+Abstract:
+
+    Eliminate term if-then-else's using cofactors.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-06-05.
+
+Revision History:
+
+--*/
+#include"cofactor_elim_term_ite.h"
+#include"mk_simplified_app.h"
+#include"rewriter_def.h"
+#include"cooperate.h"
+#include"for_each_expr.h"
+#include"ast_smt2_pp.h"
+#include"ast_ll_pp.h"
+#include"tactic.h"
+
+struct cofactor_elim_term_ite::imp {
+    ast_manager &      m;
+    params_ref         m_params;
+    unsigned long long m_max_memory;
+    volatile bool m_cancel;
+
+    void checkpoint() { 
+        cooperate("cofactor ite");
+        if (memory::get_allocation_size() > m_max_memory)
+            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+        if (m_cancel)
+            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+    }
+
+    // Collect atoms that contain term if-then-else
+    struct analyzer {
+        struct frame {
+            expr *   m_t;
+            unsigned m_first:1;
+            unsigned m_form_ctx:1;
+            frame(expr * t, bool form_ctx):m_t(t), m_first(true), m_form_ctx(form_ctx) {}
+        };
+        
+        ast_manager &       m;
+        imp &               m_owner;
+        obj_hashtable<expr> m_candidates;
+        expr_fast_mark1     m_processed;
+        expr_fast_mark2     m_has_term_ite;
+        svector<frame>      m_frame_stack;
+
+        analyzer(ast_manager & _m, imp & owner):m(_m), m_owner(owner) {}
+        
+        void push_frame(expr * t, bool form_ctx) {
+            m_frame_stack.push_back(frame(t, form_ctx && m.is_bool(t)));
+        }
+        
+        void visit(expr * t, bool form_ctx, bool & visited) {
+            if (!m_processed.is_marked(t)) {
+                visited = false;
+                push_frame(t, form_ctx);
+            }
+        }
+        
+        void save_candidate(expr * t, bool form_ctx) {
+            if (!form_ctx)
+                return;
+            if (!m.is_bool(t))
+                return;
+            if (!m_has_term_ite.is_marked(t))
+                return;
+            if (!is_app(t))
+                return;
+            if (to_app(t)->get_family_id() == m.get_basic_family_id()) {
+                switch (to_app(t)->get_decl_kind()) {
+                case OP_OR:
+                case OP_AND:
+                case OP_NOT:
+                case OP_XOR:
+                case OP_IMPLIES:
+                case OP_TRUE:
+                case OP_FALSE:
+                case OP_ITE:
+                case OP_IFF:
+                    return;
+                case OP_EQ:
+                case OP_DISTINCT:
+                    if (m.is_bool(to_app(t)->get_arg(0)))
+                        return;
+                    break;
+                default:
+                    break;
+                }
+            }
+            // it is an atom in a formula context (i.e., it is not nested inside a term),
+            // and it contains a term if-then-else.
+            m_candidates.insert(t);
+        }
+        
+        void operator()(expr * t) {
+            SASSERT(m.is_bool(t));
+            push_frame(t, true);
+            SASSERT(!m_frame_stack.empty());
+            while (!m_frame_stack.empty()) {
+                frame & fr    = m_frame_stack.back();
+                expr * t      = fr.m_t;
+                bool form_ctx = fr.m_form_ctx;
+                TRACE("cofactor_ite_analyzer", tout << "processing, form_ctx: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
+
+                m_owner.checkpoint();
+                
+                if (m_processed.is_marked(t)) {
+                    save_candidate(t, form_ctx);
+                    m_frame_stack.pop_back();
+                    continue;
+                }
+
+                if (m.is_term_ite(t)) {
+                    m_has_term_ite.mark(t);
+                    m_processed.mark(t);
+                    m_frame_stack.pop_back();
+                    continue;
+                }
+                
+                if (fr.m_first) {
+                    fr.m_first   = false;
+                    bool visited = true;
+                    if (is_app(t)) {
+                        unsigned num_args = to_app(t)->get_num_args();
+                        for (unsigned i = 0; i < num_args; i++)
+                            visit(to_app(t)->get_arg(i), form_ctx, visited);
+                    }
+                    // ignoring quantifiers
+                    if (!visited)
+                        continue;
+                }
+                
+                if (is_app(t)) {
+                    unsigned num_args = to_app(t)->get_num_args();
+                    unsigned i;
+                    for (i = 0; i < num_args; i++) {
+                        if (m_has_term_ite.is_marked(to_app(t)->get_arg(i)))
+                            break;
+                    }
+                    if (i < num_args) {
+                        m_has_term_ite.mark(t);
+                        TRACE("cofactor_ite_analyzer", tout << "saving candidate: " << form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
+                        save_candidate(t, form_ctx);
+                    }
+                }
+                else {
+                    SASSERT(is_quantifier(t) || is_var(t));
+                    // ignoring quantifiers... they are treated as black boxes.
+                }
+                m_processed.mark(t);
+                m_frame_stack.pop_back();
+            }
+            m_processed.reset();
+            m_has_term_ite.reset();
+        }
+    };
+
+    expr * get_first(expr * t) { 
+        typedef std::pair<expr *, unsigned> frame;
+        expr_fast_mark1         visited;            
+        sbuffer<frame>          stack;    
+        stack.push_back(frame(t, 0));
+        while (!stack.empty()) {
+        start:
+            checkpoint();
+            frame & fr  = stack.back();
+            expr * curr = fr.first;
+            if (m.is_term_ite(curr)) 
+                return to_app(curr)->get_arg(0);
+            switch (curr->get_kind()) {
+            case AST_VAR:
+            case AST_QUANTIFIER:
+                // ignore quantifiers
+                stack.pop_back();
+                break;
+            case AST_APP: {
+                unsigned num_args = to_app(curr)->get_num_args();
+                while (fr.second < num_args) {
+                    expr * arg = to_app(curr)->get_arg(fr.second);
+                    fr.second++;
+                    if (arg->get_ref_count() > 1) {
+                        if (visited.is_marked(arg))
+                            continue;
+                        visited.mark(arg);
+                    }
+                    switch (arg->get_kind()) {
+                    case AST_VAR:
+                    case AST_QUANTIFIER:
+                        // ingore quantifiers
+                        break;
+                    case AST_APP:
+                        if (to_app(arg)->get_num_args() > 0) {
+                            stack.push_back(frame(arg, 0));
+                            goto start;
+                        }
+                        break;
+                    default:
+                        UNREACHABLE();
+                        break;
+                    }
+                }
+                stack.pop_back();
+                break;
+            }
+            default:
+                UNREACHABLE();
+                break;
+            }
+        }
+        return 0;
+    }
+
+    /**
+       \brief Fuctor for selecting the term if-then-else condition with the most number of occurrences.
+    */
+    expr * get_best(expr * t) {
+        typedef std::pair<expr *, unsigned> frame;
+        obj_map<expr, unsigned> occs;
+        expr_fast_mark1         visited;            
+        sbuffer<frame>          stack;    
+        
+        stack.push_back(frame(t, 0));
+        while (!stack.empty()) {
+        start:
+            checkpoint();
+            frame & fr  = stack.back();
+            expr * curr = fr.first;
+            switch (curr->get_kind()) {
+            case AST_VAR:
+            case AST_QUANTIFIER:
+                // ignore quantifiers
+                stack.pop_back();
+                break;
+            case AST_APP: {
+                unsigned num_args = to_app(curr)->get_num_args();
+                bool is_term_ite = m.is_term_ite(curr);
+                while (fr.second < num_args) {
+                    expr * arg = to_app(curr)->get_arg(fr.second);
+                    if (fr.second == 0 && is_term_ite) {
+                        unsigned num = 0;
+                        if (occs.find(arg, num))
+                            occs.insert(arg, num+1);
+                        else
+                            occs.insert(arg, 1);
+                    }
+                    fr.second++;
+                    if (arg->get_ref_count() > 1) {
+                        if (visited.is_marked(arg))
+                            continue;
+                        visited.mark(arg);
+                    }
+                    switch (arg->get_kind()) {
+                    case AST_VAR:
+                    case AST_QUANTIFIER:
+                        // ingore quantifiers
+                        break;
+                    case AST_APP:
+                        if (to_app(arg)->get_num_args() > 0) {
+                            stack.push_back(frame(arg, 0));
+                            goto start;
+                        }
+                        break;
+                    default:
+                        UNREACHABLE();
+                        break;
+                    }
+                }
+                stack.pop_back();
+                break;
+            }
+            default:
+                UNREACHABLE();
+                break;
+            }
+        }
+        expr * best = 0;
+        unsigned best_occs = 0;
+        obj_map<expr, unsigned>::iterator it  = occs.begin();
+        obj_map<expr, unsigned>::iterator end = occs.end();
+        for (; it != end; ++it) {
+            if ((!best) ||
+                (get_depth(it->m_key) < get_depth(best))  ||
+                (get_depth(it->m_key) == get_depth(best) && it->m_value > best_occs) ||
+                // break ties by giving preference to equalities
+                (get_depth(it->m_key) == get_depth(best) && it->m_value == best_occs && m.is_eq(it->m_key) && !m.is_eq(best))) {
+                best = it->m_key;
+                best_occs = it->m_value;
+            }
+        }
+        visited.reset();
+        CTRACE("cofactor_ite_get_best", best != 0, tout << "best num-occs: " << best_occs << "\n" << mk_ismt2_pp(best, m) << "\n";);
+        return best;
+    }
+
+    void updt_params(params_ref const & p) {
+        m_max_memory     = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+    }
+
+    void set_cancel(bool f) {
+        m_cancel = f;
+    }
+
+    struct cofactor_rw_cfg : public default_rewriter_cfg {
+        ast_manager &         m;
+        imp &                 m_owner;
+        obj_hashtable<expr> * m_has_term_ite;
+        mk_simplified_app     m_mk_app;
+        expr *                m_atom;
+        bool                  m_sign;
+        expr *                m_term;
+        app *                 m_value;
+        bool                  m_strict_lower;
+        app *                 m_lower;
+        bool                  m_strict_upper;
+        app *                 m_upper;
+
+        cofactor_rw_cfg(ast_manager & _m, imp & owner, obj_hashtable<expr> * has_term_ite = 0):
+            m(_m),
+            m_owner(owner),
+            m_has_term_ite(has_term_ite),
+            m_mk_app(m, owner.m_params) {
+        }
+
+        bool max_steps_exceeded(unsigned num_steps) const { 
+            m_owner.checkpoint();
+            return false;
+        }
+        
+        bool pre_visit(expr * t) {
+            return true;
+        }
+
+        void set_cofactor_atom(expr * t) {
+            if (m.is_not(t)) {
+                m_atom = to_app(t)->get_arg(0);
+                m_sign = true;
+                m_term = 0;
+                // TODO: bounds
+            }
+            else {
+                m_atom = t;
+                m_sign = false;
+                m_term = 0;
+                expr * lhs;
+                expr * rhs;
+                if (m.is_eq(t, lhs, rhs)) {
+                    if (m.is_value(lhs)) {
+                        m_term  = rhs;
+                        m_value = to_app(lhs); 
+                        TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
+                    }
+                    else if (m.is_value(rhs)) {
+                        m_term  = lhs;
+                        m_value = to_app(rhs);
+                        TRACE("set_cofactor_atom", tout << "term:\n" << mk_ismt2_pp(m_term, m) << "\nvalue: " << mk_ismt2_pp(m_value, m) << "\n";);
+                    }
+                }
+                // TODO: bounds
+            }
+        }
+        
+        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;
+            return m_mk_app.mk_core(f, num, args, result);
+        }
+
+        bool get_subst(expr * s, expr * & t, proof * & pr) {
+            pr = 0;
+            
+            if (s == m_atom) {
+                t = m_sign ? m.mk_false() : m.mk_true();
+                return true;
+            }
+            
+            if (s == m_term && m_value != 0) {
+                t = m_value;
+                return true;
+            }
+            
+            // TODO: handle simple bounds
+            // Example: s is of the form (<= s 10) and m_term == s, and m_upper is 9
+            // then rewrite to true.
+            
+            return false;
+        }
+    
+    };
+
+    struct cofactor_rw : rewriter_tpl<cofactor_rw_cfg> {
+        cofactor_rw_cfg m_cfg;
+    public:
+        cofactor_rw(ast_manager & m, imp & owner, obj_hashtable<expr> * has_term_ite = 0):
+            rewriter_tpl<cofactor_rw_cfg>(m, false, m_cfg),
+            m_cfg(m, owner, has_term_ite) {
+        }
+
+        void set_cofactor_atom(expr * t) {
+            m_cfg.set_cofactor_atom(t);
+            reset();
+        }
+    };
+    
+    struct main_rw_cfg : public default_rewriter_cfg {
+        ast_manager &               m;
+        imp &                       m_owner;
+        cofactor_rw                 m_cofactor;
+        obj_hashtable<expr> const & m_candidates;
+        obj_map<expr, expr*>        m_cache;
+        expr_ref_vector             m_cache_domain;
+
+        main_rw_cfg(ast_manager & _m, imp & owner, obj_hashtable<expr> & candidates):
+            m(_m),
+            m_owner(owner),
+            m_cofactor(m, m_owner),
+            m_candidates(candidates),
+            m_cache_domain(_m) {
+        }
+
+        bool max_steps_exceeded(unsigned num_steps) const { 
+            m_owner.checkpoint();
+            return false;
+        }
+        
+        bool pre_visit(expr * t) { 
+            return m.is_bool(t) && !is_quantifier(t);
+        }
+        
+        bool get_subst(expr * s, expr * & t, proof * & t_pr) { 
+            if (m_candidates.contains(s)) {
+                t_pr = 0;
+
+                if (m_cache.find(s, t))
+                    return true;
+                unsigned step = 0;
+                TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(s, m) << "\n";);
+                expr_ref curr(m);
+                curr = s;
+                while (true) {
+                    // expr * c = m_owner.get_best(curr);
+                    expr * c = m_owner.get_first(curr);
+                    if (c == 0) {
+                        m_cache.insert(s, curr);
+                        m_cache_domain.push_back(curr);
+                        t = curr.get();
+                        return true;
+                    }
+                    step++;
+                    expr_ref pos_cofactor(m);
+                    expr_ref neg_cofactor(m);
+                    m_cofactor.set_cofactor_atom(c);
+                    m_cofactor(curr, pos_cofactor);
+                    expr_ref neg_c(m);
+                    neg_c = m.is_not(c) ? to_app(c)->get_arg(0) : m.mk_not(c);                    
+                    m_cofactor.set_cofactor_atom(neg_c);
+                    m_cofactor(curr, neg_cofactor);
+                    curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
+                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
+                }
+            }
+            return false;
+        }
+    };
+
+    struct main_rw : rewriter_tpl<main_rw_cfg> {
+        main_rw_cfg m_cfg;
+    public:
+        main_rw(ast_manager & m, imp & owner, obj_hashtable<expr> & candidates):
+            rewriter_tpl<main_rw_cfg>(m, false, m_cfg),
+            m_cfg(m, owner, candidates) {
+        }
+    };
+
+    struct bottom_up_elim {
+        typedef std::pair<expr*, bool> frame;
+        ast_manager &        m;
+        imp &                m_owner;
+        obj_map<expr, expr*> m_cache;
+        expr_ref_vector      m_cache_domain;
+        obj_hashtable<expr>  m_has_term_ite;
+        svector<frame>       m_frames;
+        cofactor_rw          m_cofactor;
+        
+        bottom_up_elim(ast_manager & _m, imp & owner):
+            m(_m),
+            m_owner(owner),
+            m_cache_domain(m),
+            m_cofactor(m, owner, &m_has_term_ite) {
+        }
+
+        bool is_atom(expr * t) const {
+            if (!m.is_bool(t))
+                return false;
+            if (!is_app(t))
+                return false;
+            if (to_app(t)->get_family_id() == m.get_basic_family_id()) {
+                switch (to_app(t)->get_decl_kind()) {
+                case OP_EQ:
+                case OP_DISTINCT:
+                    if (m.is_bool(to_app(t)->get_arg(0)))
+                        return false;
+                    else 
+                        return true;
+                default:
+                    return false;
+                }
+            }
+            return true;
+        }
+        
+        void cofactor(expr * t, expr_ref & r) {
+            unsigned step = 0;
+            TRACE("cofactor_ite", tout << "cofactor target:\n" << mk_ismt2_pp(t, m) << "\n";);
+            expr_ref curr(m);
+            curr = t;
+            while (true) {
+                expr * c = m_owner.get_best(curr);
+                // expr * c = m_owner.get_first(curr);
+                if (c == 0) {
+                    r = curr.get();
+                    return;
+                }
+                step++;
+                expr_ref pos_cofactor(m);
+                expr_ref neg_cofactor(m);
+                m_cofactor.set_cofactor_atom(c);
+                m_cofactor(curr, pos_cofactor);
+                expr_ref neg_c(m);
+                neg_c = m.is_not(c) ? to_app(c)->get_arg(0) : m.mk_not(c);                    
+                m_cofactor.set_cofactor_atom(neg_c);
+                m_cofactor(curr, neg_cofactor);
+                if (pos_cofactor == neg_cofactor) {
+                    curr = pos_cofactor;
+                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
+                    continue;
+                }
+                if (m.is_true(pos_cofactor) && m.is_false(neg_cofactor)) {
+                    curr = c;
+                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
+                    continue;
+                }
+                if (m.is_false(pos_cofactor) && m.is_true(neg_cofactor)) {
+                    curr = neg_c;
+                    TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
+                    continue;
+                }
+                curr = m.mk_ite(c, pos_cofactor, neg_cofactor);
+                TRACE("cofactor_ite", tout << "cofactor_ite step: " << step << "\n" << mk_ismt2_pp(curr, m) << "\n";);
+            }
+        }
+
+        void visit(expr * t, bool & visited) {
+            if (!m_cache.contains(t)) {
+                m_frames.push_back(frame(t, true));
+                visited = false;
+            }
+        }
+        
+        void operator()(expr * t, expr_ref & r) {
+            ptr_vector<expr> new_args;
+            m_frames.push_back(frame(t, true));
+            while (!m_frames.empty()) {
+                m_owner.checkpoint();
+                frame & fr = m_frames.back();
+                expr * t   = fr.first;
+                TRACE("cofactor_bug", tout << "processing: " << t->get_id() << " :first " << fr.second << "\n";);
+                if (!is_app(t)) {
+                    m_cache.insert(t, t);
+                    m_frames.pop_back();
+                    continue;
+                }
+                if (m_cache.contains(t)) {
+                    m_frames.pop_back();
+                    continue;
+                }
+                if (fr.second) {
+                    fr.second    = false;
+                    bool visited = true;
+                    unsigned i = to_app(t)->get_num_args();
+                    while (i > 0) {
+                        --i;
+                        expr * arg = to_app(t)->get_arg(i);
+                        visit(arg, visited);
+                    }
+                    if (!visited)
+                        continue;
+                }
+                new_args.reset();
+                bool has_new_args = false;
+                bool has_term_ite = false;
+                unsigned num = to_app(t)->get_num_args();
+                for (unsigned i = 0; i < num; i++) {
+                    expr * arg = to_app(t)->get_arg(i);
+                    expr * new_arg = 0;
+                    TRACE("cofactor_bug", tout << "collecting child: " << arg->get_id() << "\n";);
+                    m_cache.find(arg, new_arg);
+                    SASSERT(new_arg != 0);
+                    if (new_arg != arg)
+                        has_new_args = true;
+                    if (m_has_term_ite.contains(new_arg))
+                        has_term_ite = true;
+                    new_args.push_back(new_arg);
+                }
+                if (m.is_term_ite(t))
+                    has_term_ite = true;
+                expr_ref new_t(m);
+                if (has_new_args)
+                    new_t = m.mk_app(to_app(t)->get_decl(), num, new_args.c_ptr());
+                else
+                    new_t = t;
+                if (has_term_ite && is_atom(new_t)) {
+                    // update new_t
+                    expr_ref new_new_t(m);
+                    m_has_term_ite.insert(new_t);
+                    cofactor(new_t, new_new_t);
+                    m_has_term_ite.erase(new_t);
+                    new_t = new_new_t;
+                    has_term_ite = false;
+                }
+                if (has_term_ite)
+                    m_has_term_ite.insert(new_t);
+                SASSERT(new_t.get() != 0);
+                TRACE("cofactor_bug", tout << "caching: " << t->get_id() << "\n";);
+#if 0
+                counter ++;
+                verbose_stream() << counter << "\n";
+#endif
+                m_cache.insert(t, new_t);
+                m_cache_domain.push_back(new_t);
+                m_frames.pop_back();
+            }
+            expr * result = 0;
+            m_cache.find(t, result);
+            r = result;
+        }
+    };
+
+    imp(ast_manager & _m, params_ref const & p):
+        m(_m),
+        m_params(p) {
+        m_cancel = false;
+        updt_params(p);
+    }
+
+    void operator()(expr * t, expr_ref & r) {
+#if 0
+        analyzer proc(m, *this);
+        proc(t); 
+        main_rw rw(m, *this, proc.m_candidates);
+        rw(t, r);
+#else
+        bottom_up_elim proc(m, *this);
+        proc(t, r);
+#endif
+    }
+};
+
+
+cofactor_elim_term_ite::cofactor_elim_term_ite(ast_manager & m, params_ref const & p):
+    m_imp(alloc(imp, m, p)),
+    m_params(p) {
+}
+
+cofactor_elim_term_ite::~cofactor_elim_term_ite() {
+    imp * d = m_imp;
+    #pragma omp critical (cofactor_elim_term_ite)
+    {
+        m_imp = 0;
+    }
+    dealloc(d);
+}
+
+void cofactor_elim_term_ite::updt_params(params_ref const & p) {
+    m_imp->updt_params(p);
+}
+
+void cofactor_elim_term_ite::get_param_descrs(param_descrs & r) {
+}
+
+void cofactor_elim_term_ite::operator()(expr * t, expr_ref & r) {
+    m_imp->operator()(t, r);
+}
+    
+void cofactor_elim_term_ite::set_cancel(bool f) {
+    #pragma omp critical (cofactor_elim_term_ite)
+    {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+}
+
+void cofactor_elim_term_ite::cleanup() {
+    ast_manager & m = m_imp->m;
+    #pragma omp critical (cofactor_elim_term_ite) 
+    {
+        dealloc(m_imp);
+        m_imp = alloc(imp, m, m_params);
+    }
+}
+

src/tactic/core/cofactor_elim_term_ite.h

@@ -0,0 +1,44 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    cofactor_elim_term_ite.h
+
+Abstract:
+
+    Eliminate (ground) term if-then-else's using cofactors.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-06-05.
+
+Revision History:
+
+--*/
+#ifndef _COFACTOR_ELIM_TERM_ITE_H_
+#define _COFACTOR_ELIM_TERM_ITE_H_
+
+#include"ast.h"
+#include"params.h"
+
+class cofactor_elim_term_ite {
+    struct     imp;
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    cofactor_elim_term_ite(ast_manager & m, params_ref const & p = params_ref());
+    virtual ~cofactor_elim_term_ite();
+
+    void updt_params(params_ref const & p);
+    static void get_param_descrs(param_descrs & r);
+
+    void operator()(expr * t, expr_ref & r);
+    
+    void cancel() { set_cancel(true); }
+    void reset_cancel() { set_cancel(false); }
+    void set_cancel(bool f);
+    void cleanup();
+};
+
+#endif

src/tactic/core/cofactor_term_ite_tactic.cpp

@@ -0,0 +1,82 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    cofactor_term_ite_tactic.cpp
+
+Abstract:
+
+    Wrap cofactor_elim_term_ite as a tactic.
+    Eliminate (ground) term if-then-else's using cofactors.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-02-20.
+
+Revision History:
+
+--*/
+#include"tactical.h"
+#include"cofactor_elim_term_ite.h"
+
+/**
+   \brief Wrapper for applying cofactor_elim_term_ite in an assertion set.
+ */
+class cofactor_term_ite_tactic : public tactic {
+    params_ref             m_params;
+    cofactor_elim_term_ite m_elim_ite;
+
+    void process(goal & g) {
+        ast_manager & m = g.m();
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++) {
+            if (g.inconsistent())
+                break;
+            expr * f = g.form(i);
+            expr_ref new_f(m);
+            m_elim_ite(f, new_f);
+            g.update(i, new_f);
+        }
+    }
+
+public:
+    cofactor_term_ite_tactic(ast_manager & m, params_ref const & p):
+        m_params(p),
+        m_elim_ite(m, p) {
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(cofactor_term_ite_tactic, m, m_params);
+    }
+
+    virtual ~cofactor_term_ite_tactic() {}
+    virtual void updt_params(params_ref const & p) { m_params = p; m_elim_ite.updt_params(p); }
+    static  void get_param_descrs(param_descrs & r) { cofactor_elim_term_ite::get_param_descrs(r); }
+    virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
+    
+    virtual void operator()(goal_ref const & g, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        SASSERT(g->is_well_sorted());
+        fail_if_proof_generation("cofactor-term-ite", g);
+        fail_if_unsat_core_generation("cofactor-term-ite", g);
+        tactic_report report("cofactor-term-ite", *g);
+        mc = 0; pc = 0; core = 0;
+        process(*(g.get()));
+        g->inc_depth();
+        result.push_back(g.get());
+        TRACE("cofactor-term-ite", g->display(tout););
+        SASSERT(g->is_well_sorted());
+    }
+    
+    virtual void cleanup() { return m_elim_ite.cleanup(); }
+
+    virtual void set_cancel(bool f) { m_elim_ite.set_cancel(f); }
+};
+
+tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(cofactor_term_ite_tactic, m, p));
+}

src/tactic/core/cofactor_term_ite_tactic.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    cofactor_term_ite_tactic.h
+
+Abstract:
+
+    Wrap cofactor_elim_term_ite as a tactic.
+    Eliminate (ground) term if-then-else's using cofactors.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-02-20.
+
+Revision History:
+
+--*/
+#ifndef _COFACTOR_TERM_ITE_TACTIC_H_
+#define _COFACTOR_TERM_ITE_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif

src/tactic/core/ctx_simplify_tactic.cpp

@@ -0,0 +1,555 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    ctx_simplify_tactic.cpp
+
+Abstract:
+
+    Simple context simplifier for propagating constants.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-26
+
+Notes:
+
+--*/
+#include"ctx_simplify_tactic.h"
+#include"mk_simplified_app.h"
+#include"num_occurs_goal.h"
+#include"cooperate.h"
+#include"ast_ll_pp.h"
+#include"ast_smt2_pp.h"
+
+struct ctx_simplify_tactic::imp {
+    struct cached_result {
+        expr *          m_to;
+        unsigned        m_lvl;
+        cached_result * m_next;
+        cached_result(expr * t, unsigned lvl, cached_result * next):
+            m_to(t), 
+            m_lvl(lvl),
+            m_next(next) {
+        }
+    };
+
+    struct cache_cell {
+        expr *          m_from;
+        cached_result * m_result;
+        cache_cell():m_from(0), m_result(0) {}
+    };
+
+    ast_manager &               m;
+    small_object_allocator      m_allocator;
+    obj_map<expr, expr*>        m_assertions;
+    ptr_vector<expr>            m_trail;
+    svector<unsigned>           m_scopes;
+    svector<cache_cell>         m_cache;
+    vector<ptr_vector<expr> >   m_cache_undo;
+    unsigned                    m_scope_lvl;
+    unsigned                    m_depth;                  
+    unsigned                    m_num_steps;
+    num_occurs_goal             m_occs;
+    mk_simplified_app           m_mk_app;
+    unsigned long long          m_max_memory;
+    unsigned                    m_max_depth;
+    unsigned                    m_max_steps;
+    bool                        m_bail_on_blowup;
+    volatile bool               m_cancel;
+
+    imp(ast_manager & _m, params_ref const & p):
+        m(_m),
+        m_allocator("context-simplifier"),
+        m_occs(true, true),
+        m_mk_app(m, p) {
+        m_cancel = false;
+        m_scope_lvl = 0;
+        updt_params(p);
+    }
+
+    void set_cancel(bool f) {
+        m_cancel = f;
+    }
+
+    ~imp() {
+        pop(m_scope_lvl);
+        SASSERT(m_scope_lvl == 0);
+        restore_cache(0);
+        DEBUG_CODE({
+            for (unsigned i = 0; i < m_cache.size(); i++) {
+                CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from, 
+                       tout << "i: " << i << "\n" << mk_ismt2_pp(m_cache[i].m_from, m) << "\n";
+                       tout << "m_result: " << m_cache[i].m_result << "\n";
+                       if (m_cache[i].m_result) tout << "lvl: " << m_cache[i].m_result->m_lvl << "\n";);
+                SASSERT(m_cache[i].m_from == 0);
+                SASSERT(m_cache[i].m_result == 0);
+            }
+        });
+    }
+
+    void updt_params(params_ref const & p) {
+        m_max_memory   = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+        m_max_steps    = p.get_uint(":max-steps", UINT_MAX);
+        m_max_depth    = p.get_uint(":max-depth", 1024);
+        m_bail_on_blowup = p.get_bool(":bail-on-blowup", false);
+    }
+
+    void checkpoint() {
+        cooperate("ctx_simplify_tactic");
+        if (memory::get_allocation_size() > m_max_memory)
+            throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+        if (m_cancel)
+            throw tactic_exception(TACTIC_CANCELED_MSG);
+    }
+
+    bool shared(expr * t) const { 
+        return t->get_ref_count() > 1 && m_occs.get_num_occs(t) > 1;
+    }
+
+    bool check_cache() {
+        for (unsigned i = 0; i < m_cache.size(); i++) {
+            cache_cell & cell = m_cache[i];
+            if (cell.m_from != 0) {
+                SASSERT(cell.m_result != 0);
+                cached_result * curr = cell.m_result;
+                while (curr) {
+                    SASSERT(curr->m_lvl <= scope_level());
+                    curr = curr->m_next;
+                }
+            }
+        }
+        return true;
+    }
+
+    void cache_core(expr * from, expr * to) {
+        TRACE("ctx_simplify_tactic_cache", tout << "caching\n" << mk_ismt2_pp(from, m) << "\n--->\n" << mk_ismt2_pp(to, m) << "\n";);
+        unsigned id = from->get_id();
+        m_cache.reserve(id+1);
+        cache_cell & cell = m_cache[id]; 
+        void * mem = m_allocator.allocate(sizeof(cached_result));
+        if (cell.m_from == 0) {
+            // new_entry
+            cell.m_from   = from;
+            cell.m_result = new (mem) cached_result(to, m_scope_lvl, 0);
+            m.inc_ref(from);
+            m.inc_ref(to);
+        }
+        else {
+            // update 
+            cell.m_result = new (mem) cached_result(to, m_scope_lvl, cell.m_result);
+            m.inc_ref(to);
+        }
+        m_cache_undo.reserve(m_scope_lvl+1);
+        m_cache_undo[m_scope_lvl].push_back(from);
+    }
+
+    void cache(expr * from, expr * to) {
+        if (shared(from))
+            cache_core(from, to);
+    }
+    
+    unsigned scope_level() const {
+        return m_scope_lvl;
+    }
+
+    void push() { 
+        m_scope_lvl++;
+        m_scopes.push_back(m_trail.size());
+    }
+
+    void restore_cache(unsigned lvl) {
+        if (lvl >= m_cache_undo.size())
+            return;
+        ptr_vector<expr> & keys = m_cache_undo[lvl];
+        ptr_vector<expr>::iterator it    = keys.end();
+        ptr_vector<expr>::iterator begin = keys.begin();
+        while (it != begin) {
+            --it;
+            expr * key        = *it;
+            unsigned key_id   = key->get_id();
+            cache_cell & cell = m_cache[key_id];
+            SASSERT(cell.m_from == key);
+            SASSERT(cell.m_result != 0);
+            m.dec_ref(cell.m_result->m_to);
+            cached_result * to_delete = cell.m_result;
+            SASSERT(to_delete->m_lvl == lvl);
+            TRACE("ctx_simplify_tactic_cache", tout << "uncaching: " << to_delete->m_lvl << "\n" << 
+                  mk_ismt2_pp(key, m) << "\n--->\n" << mk_ismt2_pp(to_delete->m_to, m) << "\nrestoring:\n";
+                  if (to_delete->m_next) tout << mk_ismt2_pp(to_delete->m_next->m_to, m); else tout << "<null>";
+                  tout << "\n";);
+            cell.m_result = to_delete->m_next;
+            if (cell.m_result == 0) {
+                m.dec_ref(cell.m_from);
+                cell.m_from = 0;
+            }
+            m_allocator.deallocate(sizeof(cached_result), to_delete);
+        }
+        keys.reset();    
+    }
+
+    void pop(unsigned num_scopes) {
+        if (num_scopes == 0)
+            return;
+        SASSERT(num_scopes <= m_scope_lvl);
+        SASSERT(m_scope_lvl == m_scopes.size());
+        
+        // undo assertions
+        unsigned old_trail_size = m_scopes[m_scope_lvl - num_scopes];
+        unsigned i = m_trail.size();
+        while (i > old_trail_size) {
+            --i;
+            expr * key = m_trail.back();
+            m_assertions.erase(key);
+            m_trail.pop_back();
+        }
+        SASSERT(m_trail.size() == old_trail_size);
+        m_scopes.shrink(m_scope_lvl - num_scopes);
+
+        // restore cache
+        for (unsigned i = 0; i < num_scopes; i++) {
+            restore_cache(m_scope_lvl);
+            m_scope_lvl--;
+        }
+        CASSERT("ctx_simplify_tactic", check_cache());
+    }
+
+    void assert_eq_core(expr * t, app * val) {
+        if (m_assertions.contains(t)) {
+            // This branch can only happen when m_max_depth was reached.
+            // It can happen when m_assertions contains an entry t->val',
+            //  but (= t val) was not simplified to (= val' val)
+            //  because the simplifier stopped at depth m_max_depth
+            return;
+        }
+        
+        CTRACE("assert_eq_bug", m_assertions.contains(t), tout << "m_depth: " << m_depth << " m_max_depth: " << m_max_depth << "\n" 
+               << "t:\n" << mk_ismt2_pp(t, m) << "\nval:\n" << mk_ismt2_pp(val, m) << "\n";
+               expr * old_val = 0;
+               m_assertions.find(t, old_val);
+               tout << "old_val:\n" << mk_ismt2_pp(old_val, m) << "\n";);
+        m_assertions.insert(t, val);
+        m_trail.push_back(t);
+    }
+
+    void assert_eq_val(expr * t, app * val, bool mk_scope) {
+        if (shared(t)) {
+            if (mk_scope)
+                push();
+            assert_eq_core(t, val);
+        }
+    }
+
+    void assert_expr(expr * t, bool sign) {
+        if (m.is_not(t)) {
+            t    = to_app(t)->get_arg(0);
+            sign = !sign;
+        }
+        bool mk_scope = true;
+        if (shared(t)) {
+            push();
+            mk_scope  = false;
+            assert_eq_core(t, sign ? m.mk_false() : m.mk_true());
+        }
+        expr * lhs, * rhs;
+        if (!sign && m.is_eq(t, lhs, rhs)) {
+            if (m.is_value(rhs))
+                assert_eq_val(lhs, to_app(rhs), mk_scope);
+            else if (m.is_value(lhs))
+                assert_eq_val(rhs, to_app(lhs), mk_scope);
+        }
+    }
+
+    bool is_cached(expr * t, expr_ref & r) {
+        unsigned id = t->get_id();
+        if (id >= m_cache.size())
+            return false;
+        cache_cell & cell = m_cache[id];
+        SASSERT(cell.m_result == 0 || cell.m_result->m_lvl <= scope_level());
+        if (cell.m_result != 0 && cell.m_result->m_lvl == scope_level()) {
+            SASSERT(cell.m_from == t);
+            SASSERT(cell.m_result->m_to != 0);
+            r = cell.m_result->m_to;
+            return true;
+        }
+        return false;
+    }
+
+    void simplify(expr * t, expr_ref & r) {
+        r = 0;
+        if (m_depth >= m_max_depth || m_num_steps >= m_max_steps || !is_app(t)) {
+            r = t;
+            return;
+        }
+        checkpoint();
+        TRACE("ctx_simplify_tactic_detail", tout << "processing: " << mk_bounded_pp(t, m) << "\n";);
+        expr * _r;
+        if (m_assertions.find(t, _r)) {
+            r = _r;
+            SASSERT(r.get() != 0);
+            return;
+        }
+        if (is_cached(t, r)) {
+            SASSERT(r.get() != 0);
+            return;
+        }
+        m_num_steps++;
+        m_depth++;
+        if (m.is_or(t)) 
+            simplify_or_and<true>(to_app(t), r);
+        else if (m.is_and(t))
+            simplify_or_and<false>(to_app(t), r);
+        else if (m.is_ite(t))
+            simplify_ite(to_app(t), r);
+        else
+            simplify_app(to_app(t), r);
+        m_depth--;
+        SASSERT(r.get() != 0);
+        TRACE("ctx_simplify_tactic_detail", tout << "result:\n" << mk_bounded_pp(t, m) << "\n---->\n" << mk_bounded_pp(r, m) << "\n";);
+    }
+    
+    template<bool OR>
+    void simplify_or_and(app * t, expr_ref & r) {
+        // go forwards
+        expr_ref_buffer new_args(m);
+        unsigned old_lvl = scope_level();
+        bool modified = false;
+        unsigned num_args = t->get_num_args();
+        for (unsigned i = 0; i < num_args; i++) {
+            expr * arg = t->get_arg(i);
+            expr_ref new_arg(m);
+            simplify(arg, new_arg);
+            if (new_arg != arg)
+                modified = true;
+            if ((OR && m.is_false(new_arg)) ||
+                (!OR && m.is_true(new_arg))) {
+                modified = true;
+                continue;
+            }
+            if ((OR && m.is_true(new_arg)) ||
+                (!OR && m.is_false(new_arg))) { 
+                r = new_arg;
+                pop(scope_level() - old_lvl);
+                cache(t, r);
+                return;
+            }
+            new_args.push_back(new_arg);
+            if (i < num_args - 1)
+                assert_expr(new_arg, OR);
+        }
+        pop(scope_level() - old_lvl);
+
+        // go backwards
+        expr_ref_buffer new_new_args(m);
+        unsigned i = new_args.size();
+        while (i > 0) {
+            --i;
+            expr * arg = new_args[i];
+            expr_ref new_arg(m);
+            simplify(arg, new_arg);
+            if (new_arg != arg)
+                modified = true;
+            if ((OR && m.is_false(new_arg)) ||
+                (!OR && m.is_true(new_arg))) {
+                modified = true;
+                continue;
+            }
+            if ((OR && m.is_true(new_arg)) ||
+                (!OR && m.is_false(new_arg))) { 
+                r = new_arg;
+                pop(scope_level() - old_lvl);
+                cache(t, r);
+                return;
+            }
+            new_new_args.push_back(new_arg);
+            if (i > 0)
+                assert_expr(new_arg, OR);
+        }
+        pop(scope_level() - old_lvl);
+
+        if (!modified) {
+            r = t;
+        }
+        else {
+            std::reverse(new_new_args.c_ptr(), new_new_args.c_ptr() + new_new_args.size());
+            m_mk_app(t->get_decl(), new_new_args.size(), new_new_args.c_ptr(), r);
+        }
+        cache(t, r);
+    }
+    
+    void simplify_ite(app * ite, expr_ref & r) {
+        expr * c = ite->get_arg(0);
+        expr * t = ite->get_arg(1);
+        expr * e = ite->get_arg(2);
+        expr_ref new_c(m);
+        unsigned old_lvl = scope_level();
+        simplify(c, new_c);
+        if (m.is_true(new_c)) {
+            simplify(t, r);
+        }
+        else if (m.is_false(new_c)) {
+            simplify(e, r);
+        }
+        else {
+            expr_ref new_t(m);
+            expr_ref new_e(m);
+            assert_expr(new_c, false);
+            simplify(t, new_t);
+            pop(scope_level() - old_lvl);
+            assert_expr(new_c, true);
+            simplify(e, new_e);
+            pop(scope_level() - old_lvl);
+            if (c == new_c && t == new_t && e == new_e) {
+                r     = ite;
+            }
+            else {
+                expr * args[3] = { new_c.get(), new_t.get(), new_e.get() };
+                TRACE("ctx_simplify_tactic_ite_bug", 
+                      tout << "mk_ite\n" << mk_ismt2_pp(new_c.get(), m) << "\n" << mk_ismt2_pp(new_t.get(), m) 
+                      << "\n" << mk_ismt2_pp(new_e.get(), m) << "\n";);
+                m_mk_app(ite->get_decl(), 3, args, r);
+            }
+        }
+        cache(ite, r);
+    }
+
+    void simplify_app(app * t, expr_ref & r) {
+        if (t->get_num_args() == 0) {
+            r = t;
+            return;
+        }
+        expr_ref_buffer new_args(m);
+        bool modified = false;
+        unsigned num_args = t->get_num_args();
+        for (unsigned i = 0; i < num_args; i++) {
+            expr * arg = t->get_arg(i);
+            expr_ref new_arg(m);
+            simplify(arg, new_arg);
+            CTRACE("ctx_simplify_tactic_bug", new_arg.get() == 0, tout << mk_ismt2_pp(arg, m) << "\n";);
+            SASSERT(new_arg);
+            if (new_arg != arg)
+                modified = true;
+            new_args.push_back(new_arg);
+        }
+        if (!modified) {
+            r     = t;
+        }
+        else {
+            m_mk_app(t->get_decl(), new_args.size(), new_args.c_ptr(), r);
+        }
+    }
+
+    unsigned expr_size(expr* s) {
+        ast_mark visit;
+        unsigned sz = 0;
+        ptr_vector<expr> todo;
+        todo.push_back(s);
+        while (!todo.empty()) {
+            s = todo.back();
+            todo.pop_back();
+            if (visit.is_marked(s)) {
+                continue;
+            }
+			visit.mark(s, true);
+            ++sz;
+            for (unsigned i = 0; is_app(s) && i < to_app(s)->get_num_args(); ++i) {
+                todo.push_back(to_app(s)->get_arg(i));
+            }
+        }
+        return sz;
+    }
+
+    void process(expr * s, expr_ref & r) {
+        TRACE("ctx_simplify_tactic", tout << "simplifying:\n" << mk_ismt2_pp(s, m) << "\n";);
+        SASSERT(m_scope_lvl == 0);
+        m_depth = 0;
+        simplify(s, r);
+        SASSERT(m_scope_lvl == 0);
+        SASSERT(m_depth == 0);
+        SASSERT(r.get() != 0);
+        TRACE("ctx_simplify_tactic", tout << "result\n" << mk_ismt2_pp(r, m) << " :num-steps " << m_num_steps << "\n";
+              tout << "old size: " << expr_size(s) << " new size: " << expr_size(r) << "\n";);
+        if (m_bail_on_blowup && expr_size(s) < expr_size(r)) {
+            r = s;
+        }
+    }
+
+    void operator()(goal & g) {
+        SASSERT(g.is_well_sorted());
+        bool proofs_enabled = g.proofs_enabled();
+        m_occs.reset();
+        m_occs(g);
+        m_num_steps = 0;
+        expr_ref r(m);
+        proof * new_pr = 0;
+        tactic_report report("ctx-simplify", g);
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++) {
+            if (g.inconsistent())
+                return;
+            expr * t = g.form(i);
+            process(t, r);
+            if (proofs_enabled) {
+                proof * pr = g.pr(i);
+                new_pr     = m.mk_modus_ponens(pr, m.mk_rewrite_star(t, r, 0, 0)); // TODO :-)
+            }
+            g.update(i, r, new_pr, g.dep(i));
+        }
+        IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-simplify :num-steps " << m_num_steps << ")\n";);
+        SASSERT(g.is_well_sorted());
+    }
+    
+};
+
+ctx_simplify_tactic::ctx_simplify_tactic(ast_manager & m, params_ref const & p):
+    m_imp(alloc(imp, m, p)),
+    m_params(p) {
+}
+
+ctx_simplify_tactic::~ctx_simplify_tactic() {
+    dealloc(m_imp);
+}
+
+void ctx_simplify_tactic::updt_params(params_ref const & p) {
+    m_params = p;
+    m_imp->updt_params(p);
+}
+
+void ctx_simplify_tactic::get_param_descrs(param_descrs & r) {
+    insert_max_memory(r);
+    insert_max_steps(r);
+    r.insert(":max-depth", CPK_UINT, "(default: 1024) maximum term depth.");
+}
+
+void ctx_simplify_tactic::operator()(goal_ref const & in, 
+                                     goal_ref_buffer & result, 
+                                     model_converter_ref & mc, 
+                                     proof_converter_ref & pc,
+                                     expr_dependency_ref & core) {
+    mc = 0; pc = 0; core = 0;
+    (*m_imp)(*(in.get()));
+    in->inc_depth();
+    result.push_back(in.get());
+}
+    
+void ctx_simplify_tactic::set_cancel(bool f) {
+    if (m_imp)
+        m_imp->set_cancel(f);
+}
+
+void ctx_simplify_tactic::cleanup() {
+    ast_manager & m   = m_imp->m;
+    imp * d = m_imp;
+    #pragma omp critical (tactic_cancel)
+    {
+        m_imp = 0;
+    }
+    dealloc(d);
+    d = alloc(imp, m, m_params);
+    #pragma omp critical (tactic_cancel)
+    {
+        m_imp = d;
+    }
+}
+

src/tactic/core/ctx_simplify_tactic.h

@@ -0,0 +1,56 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    ctx_simplify_tactic.h
+
+Abstract:
+
+    Simple context simplifier for propagating constants.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-26
+
+Notes:
+
+--*/
+#ifndef _CTX_SIMPLIFY_TACTIC_H_
+#define _CTX_SIMPLIFY_TACTIC_H_
+
+#include"tactical.h"
+
+class ctx_simplify_tactic : public tactic {
+    struct     imp;
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    ctx_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(ctx_simplify_tactic, m, m_params);
+    }
+
+    virtual ~ctx_simplify_tactic();
+
+    virtual void updt_params(params_ref const & p);
+    static  void get_param_descrs(param_descrs & r);
+    virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core);
+
+    virtual void cleanup();
+protected:
+    virtual void set_cancel(bool f);
+};
+
+inline tactic * mk_ctx_simplify_tactic(ast_manager & m, params_ref const & p = params_ref()) {
+    return clean(alloc(ctx_simplify_tactic, m, p));
+}
+
+#endif

src/tactic/core/der_tactic.cpp

@@ -0,0 +1,114 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    der_tactic.cpp
+
+Abstract:
+
+    DER tactic
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-20
+
+--*/
+#include"der.h"
+#include"tactical.h"
+
+class der_tactic : public tactic {
+    struct imp {
+        ast_manager &   m_manager;
+        der_rewriter    m_r;
+        
+        imp(ast_manager & m):
+            m_manager(m),
+            m_r(m) {
+        }
+        
+        ast_manager & m() const { return m_manager; }
+        
+        void set_cancel(bool f) {
+            m_r.set_cancel(f);
+        }
+        
+        void reset() {
+            m_r.reset();
+        }
+        
+        void operator()(goal & g) {
+            SASSERT(g.is_well_sorted());
+            bool proofs_enabled = g.proofs_enabled();
+            tactic_report report("der", g);
+            TRACE("before_der", g.display(tout););
+            expr_ref   new_curr(m());
+            proof_ref  new_pr(m());
+            unsigned size = g.size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                if (g.inconsistent())
+                    break;
+                expr * curr = g.form(idx);
+                m_r(curr, new_curr, new_pr);
+                if (proofs_enabled) {
+                    proof * pr = g.pr(idx);
+                    new_pr     = m().mk_modus_ponens(pr, new_pr);
+                }
+                g.update(idx, new_curr, new_pr, g.dep(idx));
+            }
+            g.elim_redundancies();
+            TRACE("after_der", g.display(tout););
+            SASSERT(g.is_well_sorted());
+        }
+    };
+
+    imp *      m_imp;
+
+public:
+    der_tactic(ast_manager & m) {
+        m_imp = alloc(imp, m);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(der_tactic, m);
+    }
+
+    virtual ~der_tactic() {
+        dealloc(m_imp);
+    }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        mc = 0; pc = 0; core = 0;
+        (*m_imp)(*(in.get()));
+        in->inc_depth();
+        result.push_back(in.get());
+    }
+
+    virtual void cleanup() {
+        ast_manager & m = m_imp->m();
+        imp * d = m_imp;
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = 0;
+        }
+        dealloc(d);
+        d = alloc(imp, m);
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = d;
+        }
+    }
+    
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+};
+
+tactic * mk_der_tactic(ast_manager & m) {
+    return alloc(der_tactic, m);
+}

src/tactic/core/der_tactic.h

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    der_tactic.h
+
+Abstract:
+
+    DER tactic
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-20
+
+--*/
+#ifndef _DER_TACTIC_H_
+#define _DER_TACTIC_H_
+
+class ast_manager;
+class tactic;
+
+tactic * mk_der_tactic(ast_manager & m);
+
+#endif /* _DER_TACTIC_H_ */

src/tactic/core/distribute_forall_tactic.cpp

@@ -0,0 +1,149 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    distribute_forall_tactic.cpp
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-02-18.
+
+--*/
+#include"tactical.h"
+#include"rewriter_def.h"
+#include"var_subst.h"
+
+class distribute_forall_tactic : public tactic {
+
+    struct rw_cfg : public default_rewriter_cfg {
+        ast_manager & m;
+
+        rw_cfg(ast_manager & _m):m(_m) {}
+        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) {
+            
+            if (m.is_not(new_body) && m.is_or(to_app(new_body)->get_arg(0))) {
+                // (forall X (not (or F1 ... Fn)))
+                // -->
+                // (and (forall X (not F1))
+                //      ...
+                //      (forall X (not Fn)))
+                app * or_e        = to_app(to_app(new_body)->get_arg(0));
+                unsigned num_args = or_e->get_num_args();
+                expr_ref_buffer new_args(m);
+                for (unsigned i = 0; i < num_args; i++) {
+                    expr * arg     = or_e->get_arg(i);
+                    expr * not_arg = m.mk_not(arg);
+                    quantifier_ref tmp_q(m);
+                    tmp_q = m.update_quantifier(old_q, not_arg);
+                    expr_ref new_q(m);
+                    elim_unused_vars(m, tmp_q, new_q);
+                    new_args.push_back(new_q);
+                }
+                result = m.mk_and(new_args.size(), new_args.c_ptr());
+                return true;
+            }
+            
+            if (m.is_and(new_body)) {
+                // (forall X (and F1 ... Fn))
+                // -->
+                // (and (forall X F1)
+                //      ...
+                //      (forall X Fn)
+                unsigned num_args = to_app(new_body)->get_num_args();
+                expr_ref_buffer new_args(m);
+                for (unsigned i = 0; i < num_args; i++) {
+                    expr * arg     = to_app(new_body)->get_arg(i);
+                    quantifier_ref tmp_q(m);
+                    tmp_q = m.update_quantifier(old_q, arg);
+                    expr_ref new_q(m);
+                    elim_unused_vars(m, tmp_q, new_q);
+                    new_args.push_back(new_q);
+                }
+                result = m.mk_and(new_args.size(), new_args.c_ptr());
+                return true;
+            }
+            
+            return false;
+        }
+    };
+
+    struct rw : public rewriter_tpl<rw_cfg> {
+        rw_cfg m_cfg;
+        
+        rw(ast_manager & m, bool proofs_enabled):
+            rewriter_tpl<rw_cfg>(m, proofs_enabled, m_cfg),
+            m_cfg(m) {
+        }
+    };
+
+    rw * m_rw;
+
+public:
+    distribute_forall_tactic():m_rw(0) {}
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(distribute_forall_tactic);
+    }
+
+    virtual void operator()(goal_ref const & g, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        SASSERT(g->is_well_sorted());
+        ast_manager & m = g->m();
+        bool produce_proofs = g->proofs_enabled();
+        rw r(m, produce_proofs);
+        #pragma omp critical (tactic_cancel)
+        {
+            m_rw = &r;
+        }
+        mc = 0; pc = 0; core = 0; result.reset();
+        tactic_report report("distribute-forall", *g);
+        
+        expr_ref   new_curr(m);
+        proof_ref  new_pr(m);
+        unsigned size = g->size();
+        for (unsigned idx = 0; idx < size; idx++) {
+            if (g->inconsistent())
+                break;
+            expr * curr = g->form(idx);
+            r(curr, new_curr, new_pr);
+            if (g->proofs_enabled()) {
+                proof * pr = g->pr(idx);
+                new_pr     = m.mk_modus_ponens(pr, new_pr);
+            }
+            g->update(idx, new_curr, new_pr, g->dep(idx));
+        }
+        
+        g->inc_depth();
+        result.push_back(g.get());
+        TRACE("distribute-forall", g->display(tout););
+        SASSERT(g->is_well_sorted());
+        #pragma omp critical (tactic_cancel)
+        {
+            m_rw = 0;
+        }
+    }
+
+    virtual void set_cancel(bool f) {
+        if (m_rw)
+            m_rw->set_cancel(f);
+    }
+
+    virtual void cleanup() {}
+};
+
+tactic * mk_distribute_forall_tactic(ast_manager & m, params_ref const & p) {
+    return alloc(distribute_forall_tactic);
+}

src/tactic/core/distribute_forall_tactic.h

@@ -0,0 +1,26 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    distribute_forall_tactic.h
+
+Abstract:
+
+    <abstract>
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-02-18.
+
+--*/
+#ifndef _DISTRIBUTE_FORALL_TACTIC_H_
+#define _DISTRIBUTE_FORALL_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_distribute_forall_tactic(ast_manager & m, params_ref const & p);
+
+#endif

src/tactic/core/elim_term_ite_tactic.cpp

@@ -0,0 +1,198 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    elim_term_ite_tactic.cpp
+
+Abstract:
+
+    Eliminate term if-then-else by adding 
+    new fresh auxiliary variables.
+
+Author:
+
+    Leonardo (leonardo) 2011-12-29
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"defined_names.h"
+#include"rewriter_def.h"
+#include"filter_model_converter.h"
+#include"cooperate.h"
+
+class elim_term_ite_tactic : public tactic {
+
+    struct rw_cfg : public default_rewriter_cfg {
+        ast_manager &               m;
+        defined_names               m_defined_names;
+        ref<filter_model_converter> m_mc;
+        goal *                      m_goal;
+        unsigned long long          m_max_memory; // in bytes
+        bool                        m_produce_models;
+        unsigned                    m_num_fresh;
+
+        bool max_steps_exceeded(unsigned num_steps) const { 
+            cooperate("elim term ite");
+            if (memory::get_allocation_size() > m_max_memory)
+                throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+            return false;
+        }
+
+        br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+            if (!m.is_term_ite(f))
+                return BR_FAILED;
+            expr_ref new_ite(m);
+            new_ite = m.mk_app(f, num, args);
+            
+            expr_ref new_def(m);
+            proof_ref new_def_pr(m);
+            app_ref _result(m);
+            if (m_defined_names.mk_name(new_ite, new_def, new_def_pr, _result, result_pr)) {
+                m_goal->assert_expr(new_def, new_def_pr, 0);
+                m_num_fresh++;
+                if (m_produce_models) {
+                    if (!m_mc)
+                        m_mc = alloc(filter_model_converter, m);
+                    m_mc->insert(_result->get_decl());
+                }
+            }
+            result = _result.get();
+            return BR_DONE;
+        }
+        
+        rw_cfg(ast_manager & _m, params_ref const & p):
+            m(_m),
+            m_defined_names(m, 0 /* don't use prefix */) {
+            updt_params(p);
+            m_goal      = 0;
+            m_num_fresh = 0;
+        }
+
+        void updt_params(params_ref const & p) {
+            m_max_memory     = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+        }
+    };
+    
+    struct rw : public rewriter_tpl<rw_cfg> {
+        rw_cfg m_cfg;
+        
+        rw(ast_manager & m, params_ref const & p):
+            rewriter_tpl<rw_cfg>(m, m.proofs_enabled(), m_cfg),
+            m_cfg(m, p) {
+        }
+    };
+
+    struct imp {
+        ast_manager & m;
+        rw            m_rw;
+        
+        imp(ast_manager & _m, params_ref const & p):
+            m(_m),
+            m_rw(m, p) {
+        }
+        
+        void set_cancel(bool f) {
+            m_rw.set_cancel(f);
+        }
+        
+        void updt_params(params_ref const & p) {
+            m_rw.cfg().updt_params(p);
+        }
+        
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
+            SASSERT(g->is_well_sorted());
+            mc = 0; pc = 0; core = 0;
+            tactic_report report("elim-term-ite", *g);
+            bool produce_proofs = g->proofs_enabled();
+            m_rw.cfg().m_produce_models = g->models_enabled();
+
+            m_rw.m_cfg.m_num_fresh = 0;
+            m_rw.m_cfg.m_goal = g.get();
+            expr_ref   new_curr(m);
+            proof_ref  new_pr(m);
+            unsigned   size = g->size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                expr * curr = g->form(idx);
+                m_rw(curr, new_curr, new_pr);
+                if (produce_proofs) {
+                    proof * pr = g->pr(idx);
+                    new_pr     = m.mk_modus_ponens(pr, new_pr);
+                }
+                g->update(idx, new_curr, new_pr, g->dep(idx));
+            }
+            mc = m_rw.m_cfg.m_mc.get();
+            report_tactic_progress(":elim-term-ite-consts", m_rw.m_cfg.m_num_fresh);
+            g->inc_depth();
+            result.push_back(g.get());
+            TRACE("elim_term_ite", g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+    };
+    
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    elim_term_ite_tactic(ast_manager & m, params_ref const & p):
+        m_params(p) {
+        m_imp = alloc(imp, m, p);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(elim_term_ite_tactic, m, m_params);
+    }
+        
+    virtual ~elim_term_ite_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_imp->m_rw.cfg().updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        insert_max_memory(r);
+        insert_max_steps(r);
+        r.insert(":max-args", CPK_UINT, 
+                 "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.");
+    }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+    }
+    
+    virtual void cleanup() {
+        ast_manager & m = m_imp->m;
+        imp * d = m_imp;
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = 0;
+        }
+        dealloc(d);
+        d = alloc(imp, m, m_params);
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = d;
+        }
+    }
+
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+};
+
+tactic * mk_elim_term_ite_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(elim_term_ite_tactic, m, p));
+}

src/tactic/core/elim_term_ite_tactic.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    elim_term_ite_tactic.h
+
+Abstract:
+
+    Eliminate term if-then-else by adding 
+    new fresh auxiliary variables.
+
+Author:
+
+    Leonardo (leonardo) 2011-12-29
+
+Notes:
+
+--*/
+#ifndef _ELIM_TERM_ITE_TACTIC_H_
+#define _ELIM_TERM_ITE_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_elim_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif

src/tactic/core/elim_uncnstr_tactic.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    elim_uncnstr_tactic.h
+
+Abstract:
+
+    Eliminated applications containing unconstrained variables.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-22
+
+Notes:
+
+--*/
+#ifndef _ELIM_UNCNSTR_TACTIC_H_
+#define _ELIM_UNCNSTR_TACTIC_H_
+
+#include"params.h"
+
+class tactic;
+class ast_manager;
+
+tactic * mk_elim_uncnstr_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif
+

src/tactic/core/nnf_tactic.cpp

@@ -0,0 +1,126 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    nnf_tactic.cpp
+
+Abstract:
+
+    NNF tactic
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-28.
+
+Revision History:
+
+--*/
+#include"nnf.h"
+#include"tactical.h"
+
+class nnf_tactic : public tactic {
+    params_ref    m_params;
+    nnf *         m_nnf;
+
+    struct set_nnf {
+        nnf_tactic & m_owner;
+        
+        set_nnf(nnf_tactic & owner, nnf & n):
+            m_owner(owner) {
+            #pragma omp critical (nnf_tactic)
+            {
+                m_owner.m_nnf = &n;
+            }
+        }
+        
+        ~set_nnf() {
+            #pragma omp critical (nnf_tactic)
+            {
+                m_owner.m_nnf = 0;
+            }
+        }
+    };
+public:
+    nnf_tactic(params_ref const & p):
+        m_params(p),
+        m_nnf(0) {
+        TRACE("nnf", tout << "nnf_tactic constructor: " << p << "\n";);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(nnf_tactic, m_params);
+    }
+
+    virtual ~nnf_tactic() {}
+
+    virtual void updt_params(params_ref const & p) { m_params = p; }
+
+    virtual void collect_param_descrs(param_descrs & r) { nnf::get_param_descrs(r); }
+
+    virtual void operator()(goal_ref const & g, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        TRACE("nnf", tout << "params: " << m_params << "\n"; g->display(tout););
+        SASSERT(g->is_well_sorted());
+        mc = 0; pc = 0; core = 0;
+        tactic_report report("nnf", *g);
+        bool produce_proofs = g->proofs_enabled();
+
+        ast_manager & m = g->m();
+        defined_names dnames(m);
+        nnf local_nnf(m, dnames, m_params);
+        set_nnf setter(*this, local_nnf);
+        
+        expr_ref_vector defs(m);
+        proof_ref_vector def_prs(m);
+        
+        expr_ref   new_curr(m);
+        proof_ref  new_pr(m);
+        
+        unsigned sz = g->size();
+        for (unsigned i = 0; i < sz; i++) {
+            expr * curr = g->form(i);
+            local_nnf(curr, defs, def_prs, new_curr, new_pr);
+            if (produce_proofs) {
+                proof * pr = g->pr(i);
+                new_pr     = m.mk_modus_ponens(pr, new_pr);
+            }
+            g->update(i, new_curr, new_pr, g->dep(i));
+        }
+        
+        sz = defs.size();
+        for (unsigned i = 0; i < sz; i++) {
+            if (produce_proofs)
+                g->assert_expr(defs.get(i), def_prs.get(i), 0);
+            else
+                g->assert_expr(defs.get(i), 0, 0);
+        }
+        g->inc_depth();
+        result.push_back(g.get());
+        TRACE("nnf", g->display(tout););
+        SASSERT(g->is_well_sorted());
+    }
+    
+    virtual void cleanup() {}
+    virtual void set_cancel(bool f) {
+        #pragma omp critical (nnf_tactic)
+        {
+            if (m_nnf)
+                m_nnf->set_cancel(f);
+        }
+    }
+};
+
+tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) {
+    return alloc(nnf_tactic, p);
+}
+
+tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p) {
+    params_ref new_p(p);
+    new_p.set_sym(":nnf-mode", symbol("full"));
+    TRACE("nnf", tout << "mk_nnf: " << new_p << "\n";);
+    return using_params(mk_snf_tactic(m, p), new_p);
+}

src/tactic/core/nnf_tactic.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    nnf_tactic.h
+
+Abstract:
+
+    NNF tactic
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-28.
+
+Revision History:
+
+--*/
+#ifndef _NNF_TACTIC_H_
+#define _NNF_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref());
+tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif
+

src/tactic/core/occf_tactic.cpp

@@ -0,0 +1,252 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    occf_tactic.cpp
+
+Abstract:
+
+    Put clauses in the assertion set in
+    OOC (one constraint per clause) form.
+    Constraints occuring in formulas that
+    are not clauses are ignored.
+    The formula can be put into CNF by
+    using mk_sat_preprocessor strategy.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-28.
+
+Revision History:
+
+--*/
+#include"tactical.h"
+#include"occf_tactic.h"
+#include"filter_model_converter.h"
+#include"cooperate.h"
+
+class occf_tactic : public tactic {
+    struct     imp {
+        ast_manager &            m;
+        volatile bool            m_cancel;
+        filter_model_converter * m_mc;
+        
+        imp(ast_manager & _m):
+            m(_m) {
+            m_cancel = false;
+        }
+
+        void set_cancel(bool f) {
+            m_cancel = f;
+        }
+
+        void checkpoint() {
+            if (m_cancel)
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+            cooperate("occf");
+        }
+
+        bool is_literal(expr * t) const {
+            expr * atom;
+            return is_uninterp_const(t) || (m.is_not(t, atom) && is_uninterp_const(atom));
+        }
+        
+        bool is_constraint(expr * t) const {
+            return !is_literal(t);
+        }
+        
+        bool is_target(app * cls) {
+            SASSERT(m.is_or(cls));
+            bool found = false;
+            unsigned num = cls->get_num_args();
+            for (unsigned i = 0; i < num; i++) {
+                if (is_constraint(cls->get_arg(i))) {
+                    if (found)
+                        return true;
+                    found = true;
+                }
+            }
+            return false;
+        }
+        
+        struct bvar_info {
+            expr *   m_bvar;
+            unsigned m_gen_pos:1;
+            unsigned m_gen_neg:1;
+            bvar_info():m_bvar(0), m_gen_pos(false), m_gen_neg(false) {}
+            bvar_info(expr * var, bool sign):
+                m_bvar(var),
+                                            m_gen_pos(!sign),
+                m_gen_neg(sign) {
+            }
+        };
+        
+        typedef obj_map<expr, bvar_info> cnstr2bvar;
+        
+        expr * get_aux_lit(cnstr2bvar & c2b, expr * cnstr, goal_ref const & g) {
+            bool sign = false;
+            while (m.is_not(cnstr)) {
+                cnstr = to_app(cnstr)->get_arg(0);
+                sign  = !sign;
+            }
+            
+            cnstr2bvar::obj_map_entry * entry = c2b.find_core(cnstr);
+            if (entry == 0)
+                return 0;
+            bvar_info & info = entry->get_data().m_value;
+            if (sign) {
+                if (!info.m_gen_neg) {
+                    info.m_gen_neg = true;
+                    g->assert_expr(m.mk_or(info.m_bvar, m.mk_not(cnstr)), 0, 0);
+                }
+                return m.mk_not(info.m_bvar);
+            }
+            else {
+                if (!info.m_gen_pos) {
+                    info.m_gen_pos = true;
+                    g->assert_expr(m.mk_or(m.mk_not(info.m_bvar), cnstr), 0, 0);
+                }
+                return info.m_bvar;
+            }
+        }
+
+        expr * mk_aux_lit(cnstr2bvar & c2b, expr * cnstr, bool produce_models, goal_ref const & g) {
+            bool sign = false;
+            while (m.is_not(cnstr)) {
+                cnstr = to_app(cnstr)->get_arg(0);
+                sign  = !sign;
+            }
+            
+            SASSERT(!c2b.contains(cnstr));
+            expr * bvar = m.mk_fresh_const(0, m.mk_bool_sort());
+            if (produce_models)
+                m_mc->insert(to_app(bvar)->get_decl());
+            c2b.insert(cnstr, bvar_info(bvar, sign));
+            if (sign) {
+                g->assert_expr(m.mk_or(bvar, m.mk_not(cnstr)), 0, 0);
+                return m.mk_not(bvar);
+            }
+            else {
+                g->assert_expr(m.mk_or(m.mk_not(bvar), cnstr), 0, 0);
+                return bvar;
+            }
+        }
+        
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
+            SASSERT(g->is_well_sorted());
+            mc = 0; pc = 0; core = 0;
+
+            fail_if_proof_generation("occf", g);
+
+            bool produce_models = g->models_enabled();
+            tactic_report report("occf", *g);
+            
+            m_mc = 0;
+            
+            ptr_vector<expr> new_lits;
+            
+            cnstr2bvar c2b;
+            
+            unsigned sz = g->size();
+            for (unsigned i = 0; i < sz; i++) {
+                checkpoint();
+                expr * f = g->form(i);
+                expr_dependency * d = g->dep(i);
+                if (!m.is_or(f))
+                    continue;
+                app * cls = to_app(f);
+                if (!is_target(cls))
+                    continue;
+                if (produce_models && !m_mc) {
+                    m_mc = alloc(filter_model_converter, m);
+                    mc = m_mc;
+                }
+                expr * keep = 0;
+                new_lits.reset();
+                unsigned num = cls->get_num_args();
+                for (unsigned j = 0; j < num; j++) {
+                    expr * l = cls->get_arg(j);
+                    if (is_constraint(l)) {
+                        expr * new_l = get_aux_lit(c2b, l, g);
+                        if (new_l != 0) {
+                            new_lits.push_back(new_l);
+                        }
+                        else if (keep == 0) {
+                            keep = l;
+                        }
+                        else {
+                            new_l = mk_aux_lit(c2b, l, produce_models, g);
+                            new_lits.push_back(new_l);
+                        }
+                    }
+                    else {
+                        new_lits.push_back(l);
+                    }
+                }
+                if (keep != 0)
+                    new_lits.push_back(keep);
+                g->update(i, m.mk_or(new_lits.size(), new_lits.c_ptr()), 0, d);
+            }
+            g->inc_depth();
+            result.push_back(g.get());
+            TRACE("occf", g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+    };
+    
+    imp *      m_imp;
+public:
+    occf_tactic(ast_manager & m) {
+        m_imp = alloc(imp, m);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(occf_tactic, m);
+    }
+        
+    virtual ~occf_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {}
+    virtual void collect_param_descrs(param_descrs & r) {}
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+    }
+    
+    virtual void cleanup() {
+        ast_manager & m = m_imp->m;
+        imp * d = m_imp;
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = 0;
+        }
+        dealloc(d);
+        d = alloc(imp, m);
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = d;
+        }
+    }
+    
+protected:
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+};
+
+tactic * mk_occf_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(occf_tactic, m));
+}
+

src/tactic/core/occf_tactic.h

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    occf_tactic.h
+
+Abstract:
+
+    Put clauses in the assertion set in
+    OOC (one constraint per clause) form.
+    Constraints occuring in formulas that
+    are not clauses are ignored.
+    The formula can be put into CNF by
+    using mk_sat_preprocessor strategy.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-28.
+
+Revision History:
+
+--*/
+#ifndef _OCCF_TACTIC_H_
+#define _OCCF_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_occf_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif
+

src/tactic/core/propagate_values_tactic.cpp

@@ -0,0 +1,275 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    propagate_values_tactic.cpp
+
+Abstract:
+
+    Propagate values using equalities of the form (= t v) where v is a value,
+    and atoms t and (not t)
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-28.
+
+Revision History:
+
+--*/
+#include"tactical.h"
+#include"propagate_values_tactic.h"
+#include"th_rewriter.h"
+#include"ast_smt2_pp.h"
+#include"expr_substitution.h"
+#include"goal_shared_occs.h"
+
+class propagate_values_tactic : public tactic {
+    struct     imp {
+        ast_manager &                 m_manager;
+        th_rewriter                   m_r;
+        scoped_ptr<expr_substitution> m_subst;
+        goal *                        m_goal;
+        goal_shared_occs              m_occs;
+        unsigned                      m_idx;
+        unsigned                      m_max_rounds;
+        bool                          m_modified;
+        
+        imp(ast_manager & m, params_ref const & p):
+            m_manager(m),
+            m_r(m, p),
+            m_goal(0),
+            m_occs(m, true /* track atoms */) {
+            updt_params_core(p);
+        }
+
+        void updt_params_core(params_ref const & p) {
+            m_max_rounds = p.get_uint(":max-rounds", 4);
+        }
+        
+        void updt_params(params_ref const & p) {
+            m_r.updt_params(p);
+            updt_params_core(p);
+        }
+
+        ast_manager & m() const { return m_manager; }
+        
+        void set_cancel(bool f) {
+            m_r.set_cancel(f);
+        }
+        
+        bool is_shared(expr * t) {
+            return m_occs.is_shared(t);
+        }
+        
+        bool is_shared_neg(expr * t, expr * & atom) {
+            if (!m().is_not(t))
+                return false;
+            atom = to_app(t)->get_arg(0);
+            return is_shared(atom);
+        }
+
+        bool is_shared_eq(expr * t, expr * & lhs, expr * & value) {
+            if (!m().is_eq(t))
+                return false;
+            expr * arg1 = to_app(t)->get_arg(0);
+            expr * arg2 = to_app(t)->get_arg(1);
+            if (m().is_value(arg1) && is_shared(arg2)) {
+                lhs   = arg2;
+                value = arg1;
+                return true;
+            }
+            if (m().is_value(arg2) && is_shared(arg1)) {
+                lhs   = arg1;
+                value = arg2;
+                return true;
+            }
+            return false;
+        }
+        
+        void push_result(expr * new_curr, proof * new_pr) {
+            if (m_goal->proofs_enabled()) {
+                proof * pr = m_goal->pr(m_idx);
+                new_pr     = m().mk_modus_ponens(pr, new_pr);
+            }
+            
+            expr_dependency_ref new_d(m());
+            if (m_goal->unsat_core_enabled()) {
+                new_d = m_goal->dep(m_idx);
+                expr_dependency * used_d = m_r.get_used_dependencies();
+                if (used_d != 0) {
+                    new_d = m().mk_join(new_d, used_d);
+                    m_r.reset_used_dependencies();
+                }
+            }
+            
+            m_goal->update(m_idx, new_curr, new_pr, new_d);
+        
+            if (is_shared(new_curr)) {
+                m_subst->insert(new_curr, m().mk_true(), m().mk_iff_true(new_pr), new_d);
+            }
+            expr * atom;
+            if (is_shared_neg(new_curr, atom)) {
+                m_subst->insert(atom, m().mk_false(), m().mk_iff_false(new_pr), new_d);
+            }
+            expr * lhs, * value;
+            if (is_shared_eq(new_curr, lhs, value)) {
+                TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m()) << "\n";);
+                m_subst->insert(lhs, value, new_pr, new_d);
+            }
+        }
+        
+        void process_current() {
+            expr * curr = m_goal->form(m_idx);
+            expr_ref   new_curr(m());
+            proof_ref  new_pr(m());
+            
+            if (!m_subst->empty()) {
+                m_r(curr, new_curr, new_pr);
+            }
+            else {
+                new_curr = curr;
+                if (m().proofs_enabled())
+                    new_pr   = m().mk_reflexivity(curr);
+            }
+
+            TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m()) << "\n---->\n" << mk_ismt2_pp(new_curr, m()) << "\n";);
+            push_result(new_curr, new_pr);
+            if (new_curr != curr)
+                m_modified = true;
+        }
+
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
+            SASSERT(g->is_well_sorted());
+            mc = 0; pc = 0; core = 0;
+            tactic_report report("propagate-values", *g);
+            m_goal = g.get();
+
+            bool forward   = true;
+            expr_ref   new_curr(m());
+            proof_ref  new_pr(m());
+            unsigned size  = m_goal->size();
+            m_idx          = 0;
+            m_modified     = false;
+            unsigned round = 0;
+
+            if (m_goal->inconsistent())
+                goto end;
+
+            m_subst = alloc(expr_substitution, m(), g->unsat_core_enabled(), g->proofs_enabled());
+            m_r.set_substitution(m_subst.get());
+            m_occs(*m_goal);
+
+            while (true) {
+                TRACE("propagate_values", m_goal->display(tout););
+                if (forward) {
+                    for (; m_idx < size; m_idx++) {
+                        process_current();
+                        if (m_goal->inconsistent()) 
+                            goto end;
+                    }
+                    if (m_subst->empty() && !m_modified)
+                        goto end;
+                    m_occs(*m_goal);
+                    m_idx        = m_goal->size();
+                    forward      = false;
+                    m_subst->reset();
+                    m_r.set_substitution(m_subst.get()); // reset, but keep substitution
+                }
+                else {
+                    while (m_idx > 0) {
+                        m_idx--;
+                        process_current();
+                        if (m_goal->inconsistent()) 
+                            goto end;
+                    }
+                    if (!m_modified)
+                        goto end;
+                    m_subst->reset();
+                    m_r.set_substitution(m_subst.get()); // reset, but keep substitution
+                    m_modified   = false;
+                    m_occs(*m_goal);
+                    m_idx        = 0;
+                    size         = m_goal->size();
+                    forward      = true;
+                }
+                round++;
+                if (round >= m_max_rounds)
+                    break;
+                IF_VERBOSE(100, verbose_stream() << "starting new round, goal size: " << m_goal->num_exprs() << std::endl;);
+                TRACE("propgate_values", tout << "round finished\n"; m_goal->display(tout); tout << "\n";);
+            }
+        end:
+            m_goal->elim_redundancies();
+            m_goal->inc_depth();
+            result.push_back(m_goal);
+            SASSERT(m_goal->is_well_sorted());
+            TRACE("propagate_values", m_goal->display(tout););
+            m_goal = 0;
+        }
+    };
+    
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    propagate_values_tactic(ast_manager & m, params_ref const & p):
+        m_params(p) {
+        m_imp = alloc(imp, m, p);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(propagate_values_tactic, m, m_params);
+    }
+    
+    virtual ~propagate_values_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_imp->updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        th_rewriter::get_param_descrs(r);
+        r.insert(":max-rounds", CPK_UINT, "(default: 2) maximum number of rounds.");
+    }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+    }
+    
+    virtual void cleanup() {
+        ast_manager & m = m_imp->m();
+        imp * d = m_imp;
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = 0;
+        }
+        dealloc(d);
+        d = alloc(imp, m, m_params);
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = d;
+        }
+    }
+    
+protected:
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+};
+
+tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(propagate_values_tactic, m, p));
+}
+

src/tactic/core/propagate_values_tactic.h

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    propagate_values_tactic.h
+
+Abstract:
+
+    Propagate values using equalities of the form (= t v) where v is a value,
+    and atoms t and (not t)
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-28.
+
+Revision History:
+
+--*/
+#ifndef _PROPAGATE_VALUES_TACTIC_H_
+#define _PROPAGATE_VALUES_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif

src/tactic/core/reduce_args_tactic.cpp

@@ -0,0 +1,557 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    reduce_args_tactic.cpp
+
+Abstract:
+
+    Reduce the number of arguments in function applications.
+
+Author:
+
+    Leonardo (leonardo) 2012-02-19
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"cooperate.h"
+#include"ast_smt2_pp.h"
+#include"map.h"
+#include"rewriter_def.h"
+#include"extension_model_converter.h"
+#include"filter_model_converter.h"
+
+/**
+   \brief Reduce the number of arguments in function applications.
+
+   Example, suppose we have a function f with 2 arguments. 
+   There are 1000 applications of this function, but the first argument is always "a", "b" or "c".
+   Thus, we replace the f(t1, t2)
+   with 
+      f_a(t2)   if   t1 = a
+      f_b(t2)   if   t2 = b
+      f_c(t2)   if   t2 = c
+
+   Since f_a, f_b, f_c are new symbols, satisfiability is preserved.
+   
+   This transformation is very similar in spirit to the Ackermman's reduction. 
+
+   This transformation should work in the following way:
+
+   1- Create a mapping decl2arg_map from declarations to tuples of booleans, an entry [f -> (true, false, true)]
+       means that f is a declaration with 3 arguments where the first and third arguments are always values.
+   2- Traverse the formula and populate the mapping. 
+        For each function application f(t1, ..., tn) do
+          a) Create a boolean tuple (is_value(t1), ..., is_value(tn)) and do
+             the logical-and with the tuple that is already in the mapping. If there is no such tuple
+             in the mapping, we just add a new entry.
+
+   If all entries are false-tuples, then there is nothing to be done. The transformation is not applicable.
+
+   Now, we create a mapping decl2new_decl from (decl, val_1, ..., val_n) to decls. Note that, n may be different for each entry,
+   but it is the same for the same declaration.
+   For example, suppose we have [f -> (true, false, true)] in decl2arg_map, and applications f(1, a, 2), f(1, b, 2), f(1, b, 3), f(2, b, 3), f(2, c, 3) in the formula.
+   Then, decl2arg_map would contain
+        (f, 1, 2) -> f_1_2
+        (f, 1, 3) -> f_1_3
+        (f, 2, 3) -> f_2_3
+   where f_1_2, f_1_3 and f_2_3 are new function symbols.
+   Using the new map, we can replace the occurrences of f.
+*/
+class reduce_args_tactic : public tactic {
+    struct     imp;
+    imp *      m_imp;
+public:
+    reduce_args_tactic(ast_manager & m);
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(reduce_args_tactic, m);
+    }
+
+    virtual ~reduce_args_tactic();
+    
+    virtual void operator()(goal_ref const & g, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
+    virtual void cleanup();
+    virtual void set_cancel(bool f);
+};
+
+tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(reduce_args_tactic, m));
+}
+
+struct reduce_args_tactic::imp {
+    ast_manager &            m_manager;
+    bool                     m_produce_models;
+    volatile bool            m_cancel;
+
+    ast_manager & m() const { return m_manager; }
+    
+    imp(ast_manager & m):
+        m_manager(m) {
+        m_cancel = false;
+    }
+
+    void set_cancel(bool f) {
+        m_cancel = f;
+    }
+
+    void checkpoint() { 
+        if (m_cancel)
+            throw tactic_exception(TACTIC_CANCELED_MSG);
+        cooperate("reduce-args");
+    }
+    
+    struct find_non_candidates_proc {
+        ast_manager &              m_manager;
+        obj_hashtable<func_decl> & m_non_cadidates;
+        
+        find_non_candidates_proc(ast_manager & m, obj_hashtable<func_decl> & non_cadidates):
+            m_manager(m),
+            m_non_cadidates(non_cadidates) {
+        }
+        
+        void operator()(var * n) {}
+        
+        void operator()(quantifier * n) {}
+        
+        void operator()(app * n) {
+            if (n->get_num_args() == 0)
+                return; // ignore constants
+            func_decl * d = n->get_decl();
+            if (d->get_family_id() != null_family_id)
+                return; // ignore interpreted symbols
+            if (m_non_cadidates.contains(d))
+                return; // it is already in the set.
+            unsigned j    = n->get_num_args();        
+            while (j > 0) {
+                --j;
+                if (m_manager.is_value(n->get_arg(j)))
+                    return;
+            }  
+            m_non_cadidates.insert(d);
+        }
+    };
+
+    /**
+       \brief Populate the table non_cadidates with function declarations \c f
+       such that there is a function application (f t1 ... tn) where t1 ... tn are not values.
+    */
+    void find_non_candidates(goal const & g, obj_hashtable<func_decl> & non_candidates) {
+        non_candidates.reset();
+        find_non_candidates_proc proc(m_manager, non_candidates);
+        expr_fast_mark1 visited;
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++) {
+            checkpoint();
+            quick_for_each_expr(proc, visited, g.form(i));
+        }
+        
+        TRACE("reduce_args", tout << "non_candidates:\n";
+              obj_hashtable<func_decl>::iterator it  = non_candidates.begin();
+              obj_hashtable<func_decl>::iterator end = non_candidates.end();
+              for (; it != end; ++it) {
+                  func_decl * d = *it;
+                  tout << d->get_name() << "\n";
+              });
+    }
+
+    struct populate_decl2args_proc {
+        ast_manager &                     m_manager;
+        obj_hashtable<func_decl> &        m_non_cadidates;
+        obj_map<func_decl, bit_vector> &  m_decl2args;    
+        
+        populate_decl2args_proc(ast_manager & m, obj_hashtable<func_decl> & nc, obj_map<func_decl, bit_vector> & d):
+            m_manager(m), m_non_cadidates(nc), m_decl2args(d) {}
+        
+        void operator()(var * n) {}
+        void operator()(quantifier * n) {}
+        void operator()(app * n) {
+            if (n->get_num_args() == 0)
+                return; // ignore constants
+            func_decl * d = n->get_decl();
+            if (d->get_family_id() != null_family_id)
+                return; // ignore interpreted symbols
+            if (m_non_cadidates.contains(d))
+                return; // declaration is not a candidate
+            unsigned j = n->get_num_args();
+            obj_map<func_decl, bit_vector>::iterator it = m_decl2args.find_iterator(d);
+            if (it == m_decl2args.end()) {
+                m_decl2args.insert(d, bit_vector());
+                it = m_decl2args.find_iterator(d);
+                SASSERT(it != m_decl2args.end());
+                it->m_value.reserve(j);
+                while (j > 0) {
+                    --j;
+                    it->m_value.set(j, m_manager.is_value(n->get_arg(j)));
+                }
+            } else {
+                SASSERT(j == it->m_value.size());                        
+                while (j > 0) {
+                    --j;
+                    it->m_value.set(j, it->m_value.get(j) && m_manager.is_value(n->get_arg(j)));
+                }
+            }
+        }
+    };
+
+    void populate_decl2args(goal const & g, 
+                            obj_hashtable<func_decl> & non_candidates, 
+                            obj_map<func_decl, bit_vector> & decl2args) {
+        expr_fast_mark1 visited;
+        decl2args.reset();
+        populate_decl2args_proc proc(m_manager, non_candidates, decl2args);
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++) {
+            checkpoint();
+            quick_for_each_expr(proc, visited, g.form(i));
+        }
+        
+        // Remove all cases where the simplification is not applicable.
+        ptr_buffer<func_decl> bad_decls;
+        obj_map<func_decl, bit_vector>::iterator it  = decl2args.begin();
+        obj_map<func_decl, bit_vector>::iterator end = decl2args.end();
+        for (; it != end; it++) {
+            bool is_zero = true;
+            for (unsigned i = 0; i < it->m_value.size() && is_zero ; i++) {
+                if (it->m_value.get(i)) 
+                    is_zero = false;
+            }
+            if (is_zero) 
+                bad_decls.push_back(it->m_key);
+        }
+    
+        ptr_buffer<func_decl>::iterator it2  = bad_decls.begin();
+        ptr_buffer<func_decl>::iterator end2 = bad_decls.end();
+        for (; it2 != end2; ++it2)
+            decl2args.erase(*it2);
+
+        TRACE("reduce_args", tout << "decl2args:" << std::endl;
+              for (obj_map<func_decl, bit_vector>::iterator it = decl2args.begin() ; it != decl2args.end() ; it++) {
+                  tout << it->m_key->get_name() << ": ";
+                  for (unsigned i = 0 ; i < it->m_value.size() ; i++)
+                      tout << (it->m_value.get(i) ? "1" : "0");                            
+                  tout << std::endl;
+              });
+    }
+
+    struct arg2func_hash_proc {
+        bit_vector const & m_bv;
+        
+        arg2func_hash_proc(bit_vector const & bv):m_bv(bv) {}
+        unsigned operator()(app const * n) const {
+            // compute the hash-code using only the arguments where m_bv is true.
+            unsigned a = 0x9e3779b9;
+            unsigned num_args = n->get_num_args();
+            for (unsigned i = 0; i < num_args; i++) {
+                if (!m_bv.get(i)) 
+                    continue; // ignore argument
+                a = hash_u_u(a, n->get_arg(i)->get_id());
+            }
+            return a;
+        }
+    };
+     
+    struct arg2func_eq_proc {
+        bit_vector const & m_bv;
+     
+        arg2func_eq_proc(bit_vector const & bv):m_bv(bv) {}
+        bool operator()(app const * n1, app const * n2) const {
+            // compare only the arguments where m_bv is true
+            SASSERT(n1->get_num_args() == n2->get_num_args());
+            unsigned num_args = n1->get_num_args();
+            for (unsigned i = 0; i < num_args; i++) {
+                if (!m_bv.get(i)) 
+                    continue; // ignore argument
+                if (n1->get_arg(i) != n2->get_arg(i))
+                    return false;
+            }
+            return true;
+        }
+    };
+
+    typedef map<app *, func_decl *, arg2func_hash_proc, arg2func_eq_proc> arg2func;
+    typedef obj_map<func_decl, arg2func *> decl2arg2func_map;
+
+    struct reduce_args_ctx { 
+        ast_manager &           m_manager;
+        decl2arg2func_map       m_decl2arg2funcs;
+
+        reduce_args_ctx(ast_manager & m): m_manager(m) {
+        }
+        
+        ~reduce_args_ctx() {
+            obj_map<func_decl, arg2func *>::iterator it  = m_decl2arg2funcs.begin();
+            obj_map<func_decl, arg2func *>::iterator end = m_decl2arg2funcs.end();
+            for (; it != end; ++it) {
+                arg2func * map = it->m_value;
+                arg2func::iterator it2  = map->begin();
+                arg2func::iterator end2 = map->end();
+                for (; it2 != end2; ++it2) {
+                    m_manager.dec_ref(it2->m_key);
+                    m_manager.dec_ref(it2->m_value);
+                }
+                dealloc(map);
+            }
+        }
+    };
+
+    struct populate_decl2arg_set_proc {
+        ast_manager &                          m_manager;
+        obj_map<func_decl, bit_vector> &       m_decl2args;
+        decl2arg2func_map &                    m_decl2arg2funcs;
+    
+        populate_decl2arg_set_proc(ast_manager & m, 
+                                   obj_map<func_decl, bit_vector> & d,
+                                   decl2arg2func_map & ds):
+            m_manager(m), m_decl2args(d), m_decl2arg2funcs(ds) {}
+
+        void operator()(var * n) {}
+        void operator()(quantifier * n) {}
+
+        void operator()(app * n) {
+            if (n->get_num_args() == 0)
+                return; // ignore constants
+            func_decl * d = n->get_decl();
+            if (d->get_family_id() != null_family_id)
+                return; // ignore interpreted symbols
+            obj_map<func_decl, bit_vector>::iterator it = m_decl2args.find_iterator(d);
+            if (it == m_decl2args.end())
+                return; // not reducing the arguments of this declaration
+            bit_vector & bv = it->m_value;
+            arg2func * map = 0;
+            decl2arg2func_map::iterator it2 = m_decl2arg2funcs.find_iterator(d);
+            if (it2 == m_decl2arg2funcs.end()) {
+                map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv));
+                m_decl2arg2funcs.insert(d, map);
+            }
+            else {
+                map = it2->m_value;
+            }
+            if (!map->contains(n)) {
+                // create fresh symbol...
+                ptr_buffer<sort> domain;
+                unsigned arity = d->get_arity();
+                for (unsigned i = 0; i < arity; i++) {
+                    if (!bv.get(i))
+                        domain.push_back(d->get_domain(i));
+                }
+                func_decl * new_d = m_manager.mk_fresh_func_decl(d->get_name(), symbol::null, domain.size(), domain.c_ptr(), d->get_range());
+                map->insert(n, new_d);
+                m_manager.inc_ref(n);
+                m_manager.inc_ref(new_d);
+            }
+        }    
+    };
+    
+    void populate_decl2arg_set(goal const & g, 
+                               obj_map<func_decl, bit_vector> & decl2args,
+                               decl2arg2func_map & decl2arg2funcs) {
+        expr_fast_mark1 visited;
+    
+        populate_decl2arg_set_proc proc(m_manager, decl2args, decl2arg2funcs);
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++) {
+            checkpoint();
+            quick_for_each_expr(proc, visited, g.form(i));
+        }
+    }
+    
+    struct reduce_args_rw_cfg : public default_rewriter_cfg {
+        ast_manager &                    m;
+        imp &                            m_owner;
+        obj_map<func_decl, bit_vector> & m_decl2args;
+        decl2arg2func_map &              m_decl2arg2funcs;
+        
+        reduce_args_rw_cfg(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
+            m(owner.m_manager),
+            m_owner(owner),
+            m_decl2args(decl2args),
+            m_decl2arg2funcs(decl2arg2funcs) {
+        }
+
+        bool max_steps_exceeded(unsigned num_steps) const { 
+            m_owner.checkpoint();
+            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_arity() == 0)
+                return BR_FAILED; // ignore constants
+            if (f->get_family_id() != null_family_id)
+                return BR_FAILED; // ignore interpreted symbols
+            decl2arg2func_map::iterator it  = m_decl2arg2funcs.find_iterator(f);
+            if (it == m_decl2arg2funcs.end())
+                return BR_FAILED;
+            SASSERT(m_decl2args.contains(f));
+            bit_vector & bv = m_decl2args.find(f);
+            arg2func * map  = it->m_value;
+            app_ref tmp(m);
+            tmp = m.mk_app(f, num, args);
+            CTRACE("reduce_args", !map->contains(tmp),
+                   tout << "map does not contain tmp f: " << f->get_name() << "\n";
+                   tout << mk_ismt2_pp(tmp, m) << "\n";
+                   arg2func::iterator it  = map->begin();
+                   arg2func::iterator end = map->end();
+                   for (; it != end; ++it) {
+                       tout << mk_ismt2_pp(it->m_key, m) << "\n---> " << it->m_value->get_name() << "\n";
+                   });
+            SASSERT(map->contains(tmp));
+            func_decl * new_f = map->find(tmp);
+            ptr_buffer<expr> new_args;
+            for (unsigned i = 0; i < num; i++) {
+                if (!bv.get(i))
+                    new_args.push_back(args[i]);
+            }
+            result = m.mk_app(new_f, new_args.size(), new_args.c_ptr());
+            return BR_DONE;
+        }
+    };
+
+    struct reduce_args_rw : rewriter_tpl<reduce_args_rw_cfg> {
+        reduce_args_rw_cfg m_cfg;
+    public:
+        reduce_args_rw(imp & owner, obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs):
+            rewriter_tpl<reduce_args_rw_cfg>(owner.m_manager, false, m_cfg),
+            m_cfg(owner, decl2args, decl2arg2funcs) {
+        }
+    };
+
+    model_converter * mk_mc(obj_map<func_decl, bit_vector> & decl2args, decl2arg2func_map & decl2arg2funcs) {
+        ptr_buffer<expr> new_args;
+        var_ref_vector   new_vars(m_manager);
+        ptr_buffer<expr> new_eqs;
+        extension_model_converter * e_mc = alloc(extension_model_converter, m_manager);
+        filter_model_converter * f_mc    = alloc(filter_model_converter, m_manager);
+        decl2arg2func_map::iterator it   = decl2arg2funcs.begin();
+        decl2arg2func_map::iterator end  = decl2arg2funcs.end();
+        for (; it != end; ++it) {
+            func_decl * f  = it->m_key;
+            arg2func * map = it->m_value;
+            expr * def     = 0;
+            SASSERT(decl2args.contains(f));
+            bit_vector & bv = decl2args.find(f);
+            new_vars.reset();
+            new_args.reset();
+            for (unsigned i = 0; i < f->get_arity(); i++) {
+                new_vars.push_back(m_manager.mk_var(i, f->get_domain(i)));
+                if (!bv.get(i))
+                    new_args.push_back(new_vars.back());
+            }
+            arg2func::iterator it2  = map->begin();
+            arg2func::iterator end2 = map->end();
+            for (; it2 != end2; ++it2) {
+                app * t = it2->m_key;
+                func_decl * new_def = it2->m_value;
+                f_mc->insert(new_def);
+                SASSERT(new_def->get_arity() == new_args.size());
+                app * new_t = m_manager.mk_app(new_def, new_args.size(), new_args.c_ptr());
+                if (def == 0) {
+                    def = new_t;
+                }
+                else {
+                    new_eqs.reset();
+                    for (unsigned i = 0; i < f->get_arity(); i++) {
+                        if (bv.get(i))
+                            new_eqs.push_back(m_manager.mk_eq(new_vars.get(i), t->get_arg(i)));
+                    }
+                    SASSERT(new_eqs.size() > 0);
+                    expr * cond;
+                    if (new_eqs.size() == 1)
+                        cond = new_eqs[0];
+                    else
+                        cond = m_manager.mk_and(new_eqs.size(), new_eqs.c_ptr());
+                    def = m_manager.mk_ite(cond, new_t, def);
+                }
+            }
+            SASSERT(def);
+            e_mc->insert(f, def);
+        }
+        return concat(f_mc, e_mc);
+    }
+
+    void operator()(goal & g, model_converter_ref & mc) {
+        if (g.inconsistent())
+            return;
+        m_produce_models = g.models_enabled();
+        TRACE("reduce_args", g.display(tout););
+        tactic_report report("reduce-args", g);
+        obj_hashtable<func_decl> non_candidates;
+        obj_map<func_decl, bit_vector> decl2args;
+        find_non_candidates(g, non_candidates);
+        populate_decl2args(g, non_candidates, decl2args);
+        
+        if (decl2args.empty())
+            return;
+        
+        ptr_vector<arg2func> arg2funcs;
+        reduce_args_ctx ctx(m_manager);
+        populate_decl2arg_set(g, decl2args, ctx.m_decl2arg2funcs);
+    
+        reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs);
+        
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++) {
+            if (g.inconsistent())
+                break;
+            expr * f = g.form(i);
+            expr_ref new_f(m_manager);
+            rw(f, new_f);
+            g.update(i, new_f);
+        }
+
+        report_tactic_progress(":reduced-funcs", decl2args.size());
+
+        if (m_produce_models)
+            mc = mk_mc(decl2args, ctx.m_decl2arg2funcs);
+
+        TRACE("reduce_args", g.display(tout); if (mc) mc->display(tout););
+    }
+};
+
+reduce_args_tactic::reduce_args_tactic(ast_manager & m) {
+    m_imp = alloc(imp, m);
+}
+
+reduce_args_tactic::~reduce_args_tactic() {
+    dealloc(m_imp);
+}
+
+void reduce_args_tactic::operator()(goal_ref const & g, 
+                                    goal_ref_buffer & result, 
+                                    model_converter_ref & mc, 
+                                    proof_converter_ref & pc,
+                                    expr_dependency_ref & core) {
+    SASSERT(g->is_well_sorted());
+    fail_if_proof_generation("reduce-args", g);
+    fail_if_unsat_core_generation("reduce-args", g);
+    mc = 0; pc = 0; core = 0; result.reset();
+    m_imp->operator()(*(g.get()), mc);
+    g->inc_depth();
+    result.push_back(g.get());
+    SASSERT(g->is_well_sorted());
+}
+
+void reduce_args_tactic::set_cancel(bool f) {
+    if (m_imp)
+        m_imp->set_cancel(f);
+}
+
+void reduce_args_tactic::cleanup() {
+    ast_manager & m   = m_imp->m();
+    imp * d = m_imp;
+    #pragma omp critical (tactic_cancel)
+    {
+        m_imp = 0;
+    }
+    dealloc(d);
+    d = alloc(imp, m);
+    #pragma omp critical (tactic_cancel)
+    {
+        m_imp = d;
+    }
+}
+

src/tactic/core/reduce_args_tactic.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    reduce_args_tactic.h
+
+Abstract:
+
+    Reduce the number of arguments in function applications.
+
+Author:
+
+    Leonardo (leonardo) 2012-02-19
+
+Notes:
+
+--*/
+#ifndef _REDUCE_ARGS_TACTIC_H_
+#define _REDUCE_ARGS_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif

src/tactic/core/simplify_tactic.cpp

@@ -0,0 +1,139 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    simplify_tactic.cpp
+
+Abstract:
+
+    Apply simplification and rewriting rules.
+
+Author:
+
+    Leonardo (leonardo) 2011-11-20
+
+Notes:
+
+--*/
+#include"simplify_tactic.h"
+#include"th_rewriter.h"
+#include"ast_smt2_pp.h"
+
+struct simplify_tactic::imp {
+    ast_manager &   m_manager;
+    th_rewriter     m_r;
+    unsigned        m_num_steps;
+
+    imp(ast_manager & m, params_ref const & p):
+        m_manager(m),
+        m_r(m, p),
+        m_num_steps(0) {
+    }
+
+    ast_manager & m() const { return m_manager; }
+
+    void set_cancel(bool f) {
+        m_r.set_cancel(f);
+    }
+
+    void reset() {
+        m_r.reset();
+        m_num_steps = 0;
+    }
+
+    void operator()(goal & g) {
+        SASSERT(g.is_well_sorted());
+        tactic_report report("simplifier", g);
+        TRACE("before_simplifier", g.display(tout););
+        m_num_steps = 0;
+        if (g.inconsistent())
+            return;
+        expr_ref   new_curr(m());
+        proof_ref  new_pr(m());
+        unsigned size = g.size();
+        for (unsigned idx = 0; idx < size; idx++) {
+            if (g.inconsistent())
+                break;
+            expr * curr = g.form(idx);
+            m_r(curr, new_curr, new_pr);
+            m_num_steps += m_r.get_num_steps();
+            if (g.proofs_enabled()) {
+                proof * pr = g.pr(idx);
+                new_pr     = m().mk_modus_ponens(pr, new_pr);
+            }
+            g.update(idx, new_curr, new_pr, g.dep(idx));
+        }
+        TRACE("after_simplifier_bug", g.display(tout););
+        g.elim_redundancies();
+        TRACE("after_simplifier", g.display(tout););
+        TRACE("after_simplifier_detail", g.display_with_dependencies(tout););
+        SASSERT(g.is_well_sorted());
+    }
+
+    unsigned get_num_steps() const { return m_num_steps; }
+};
+
+simplify_tactic::simplify_tactic(ast_manager & m, params_ref const & p):
+    m_params(p) {
+    m_imp = alloc(imp, m, p);
+}
+
+simplify_tactic::~simplify_tactic() {
+    dealloc(m_imp);
+}
+
+void simplify_tactic::updt_params(params_ref const & p) {
+    m_params = p;
+    m_imp->m_r.updt_params(p);
+}
+
+void simplify_tactic::get_param_descrs(param_descrs & r) {
+    th_rewriter::get_param_descrs(r);
+}
+
+void simplify_tactic::operator()(goal_ref const & in, 
+                                 goal_ref_buffer & result, 
+                                 model_converter_ref & mc, 
+                                 proof_converter_ref & pc,
+                                 expr_dependency_ref & core) {
+    (*m_imp)(*(in.get()));
+    in->inc_depth();
+    result.push_back(in.get());
+    mc = 0; pc = 0; core = 0;
+}
+
+void simplify_tactic::set_cancel(bool f) {
+    if (m_imp)
+        m_imp->set_cancel(f);
+}
+
+void simplify_tactic::cleanup() {
+    ast_manager & m = m_imp->m();
+    imp * d = m_imp;
+    #pragma omp critical (tactic_cancel)
+    {
+        m_imp = 0;
+    }
+    dealloc(d);
+    d = alloc(imp, m, m_params);
+    #pragma omp critical (tactic_cancel)
+    {
+        m_imp = d;
+    }
+}
+
+unsigned simplify_tactic::get_num_steps() const {
+    return m_imp->get_num_steps();
+}
+
+tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(simplify_tactic, m, p));
+}
+
+tactic * mk_elim_and_tactic(ast_manager & m, params_ref const & p) {
+    params_ref xp = p;
+    xp.set_bool(":elim-and", true);
+    return using_params(mk_simplify_tactic(m, xp), xp);
+}
+

src/tactic/core/simplify_tactic.h

@@ -0,0 +1,54 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    simplify_tactic.h
+
+Abstract:
+
+    Apply simplification and rewriting rules.
+
+Author:
+
+    Leonardo (leonardo) 2011-11-20
+
+Notes:
+
+--*/
+#ifndef _SIMPLIFY_TACTIC_H_
+#define _SIMPLIFY_TACTIC_H_
+
+#include"tactic.h"
+#include"tactical.h"
+
+class simplify_tactic : public tactic {
+    struct     imp;
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    simplify_tactic(ast_manager & m, params_ref const & ref = params_ref());
+    virtual ~simplify_tactic();
+
+    virtual void updt_params(params_ref const & p);
+    static void get_param_descrs(param_descrs & r);
+    virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core);
+    
+    virtual void cleanup();
+
+    unsigned get_num_steps() const;
+    virtual void set_cancel(bool f);
+
+    virtual tactic * translate(ast_manager & m) { return alloc(simplify_tactic, m, m_params); }
+};
+
+tactic * mk_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
+tactic * mk_elim_and_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif

src/tactic/core/solve_eqs_tactic.cpp

@@ -0,0 +1,791 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    solve_eqs_tactic.cpp
+
+Abstract:
+
+    Tactic for solving equations and performing gaussian elimination.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-29.
+
+Revision History:
+
+--*/
+#include"tactical.h"
+#include"expr_replacer.h"
+#include"extension_model_converter.h"
+#include"occurs.h"
+#include"cooperate.h"
+#include"goal_shared_occs.h"
+#include"ast_smt2_pp.h"
+
+class solve_eqs_tactic : public tactic {
+    struct imp {
+        typedef extension_model_converter gmc;
+        
+        ast_manager &                 m_manager;
+        expr_replacer *               m_r;
+        bool                          m_r_owner;
+        arith_util                    m_a_util;
+        obj_map<expr, unsigned>       m_num_occs;
+        unsigned                      m_num_steps;
+        unsigned                      m_num_eliminated_vars;
+        bool                          m_theory_solver;
+        bool                          m_ite_solver;
+        unsigned                      m_max_occs;
+        scoped_ptr<expr_substitution> m_subst;
+        scoped_ptr<expr_substitution> m_norm_subst;
+        expr_sparse_mark              m_candidate_vars;
+        expr_sparse_mark              m_candidate_set;
+        ptr_vector<expr>              m_candidates;
+        ptr_vector<app>               m_vars;
+        ptr_vector<app>               m_ordered_vars;
+        bool                          m_produce_proofs;
+        bool                          m_produce_unsat_cores;
+        bool                          m_produce_models;
+        volatile bool                 m_cancel;
+        
+        imp(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner):
+            m_manager(m),
+            m_r(r),
+            m_r_owner(r == 0 || owner),
+            m_a_util(m),
+            m_num_steps(0),
+            m_num_eliminated_vars(0),
+            m_cancel(false) {
+            updt_params(p);
+            if (m_r == 0)
+                m_r       = mk_default_expr_replacer(m);
+        }
+        
+        ~imp() {
+            if (m_r_owner)
+                dealloc(m_r);
+        }
+        
+        ast_manager & m() const { return m_manager; }
+        
+        void updt_params(params_ref const & p) {
+            m_ite_solver     = p.get_bool(":ite-solver", true);
+            m_theory_solver  = p.get_bool(":theory-solver", true);
+            m_max_occs       = p.get_uint(":solve-eqs-max-occs", UINT_MAX);
+        }
+        
+        void set_cancel(bool f) {
+            m_cancel = f;
+            m_r->set_cancel(f);
+        }
+        
+        void checkpoint() {
+            if (m_cancel)
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+            cooperate("solve-eqs");
+        }
+        
+        // Check if the number of occurrences of t is below the specified threshold :solve-eqs-max-occs
+        bool check_occs(expr * t) const {
+            if (m_max_occs == UINT_MAX)
+                return true;
+            unsigned num = 0;
+            m_num_occs.find(t, num);
+            TRACE("solve_eqs_check_occs", tout << mk_ismt2_pp(t, m_manager) << " num_occs: " << num << " max: " << m_max_occs << "\n";);
+            return num <= m_max_occs;
+        }
+        
+        // Use: (= x def) and (= def x)
+        bool trivial_solve(expr * lhs, expr * rhs, app_ref & var, expr_ref & def, proof_ref & pr) {
+            if (is_uninterp_const(lhs) && !m_candidate_vars.is_marked(lhs) && !occurs(lhs, rhs) && check_occs(lhs)) {
+                var = to_app(lhs); 
+                def = rhs;
+                pr  = 0;
+                return true;
+            }
+            else if (is_uninterp_const(rhs) && !m_candidate_vars.is_marked(rhs) && !occurs(rhs, lhs) && check_occs(rhs)) {
+                var = to_app(rhs);
+                def = lhs;
+                if (m_produce_proofs)
+                    pr = m().mk_commutativity(m().mk_eq(lhs, rhs));
+                return true;
+            }
+            return false;
+        }
+        
+        // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2))
+        bool solve_ite_core(app * ite, expr * lhs1, expr * rhs1, expr * lhs2, expr * rhs2, app_ref & var, expr_ref & def, proof_ref & pr) {
+            if (lhs1 != lhs2)
+                return false;
+            if (!is_uninterp_const(lhs1) || m_candidate_vars.is_marked(lhs1))
+                return false;
+            if (occurs(lhs1, ite->get_arg(0)) || occurs(lhs1, rhs1) || occurs(lhs1, rhs2))
+                return false;
+            if (!check_occs(lhs1))
+                return false;
+            var = to_app(lhs1);
+            def = m().mk_ite(ite->get_arg(0), rhs1, rhs2);
+            
+            if (m_produce_proofs)
+                pr = m().mk_rewrite(ite, m().mk_eq(var, def));
+            return true;
+        }
+        
+        // (ite c (= x t1) (= x t2)) --> (= x (ite c t1 t2))
+        bool solve_ite(app * ite, app_ref & var, expr_ref & def, proof_ref & pr) {
+            expr * t = ite->get_arg(1);
+            expr * e = ite->get_arg(2);
+            
+            if (!m().is_eq(t) || !m().is_eq(e))
+                return false;
+            
+            expr * lhs1 = to_app(t)->get_arg(0);
+            expr * rhs1 = to_app(t)->get_arg(1);
+            expr * lhs2 = to_app(e)->get_arg(0);
+            expr * rhs2 = to_app(e)->get_arg(1);
+            
+            return 
+                solve_ite_core(ite, lhs1, rhs1, lhs2, rhs2, var, def, pr) ||
+                solve_ite_core(ite, rhs1, lhs1, lhs2, rhs2, var, def, pr) ||
+                solve_ite_core(ite, lhs1, rhs1, rhs2, lhs2, var, def, pr) ||
+                solve_ite_core(ite, rhs1, lhs1, rhs2, lhs2, var, def, pr);
+        }
+        
+        bool is_pos_literal(expr * n) {
+            return is_app(n) && to_app(n)->get_num_args() == 0 && to_app(n)->get_family_id() == null_family_id;
+        }
+        
+        bool is_neg_literal(expr * n) {
+            if (m_manager.is_not(n))
+                return is_pos_literal(to_app(n)->get_arg(0));
+            return false;
+        }
+        
+#if 0
+        bool not_bool_eq(expr * f, app_ref & var, expr_ref & def, proof_ref & pr) {
+            if (!m().is_not(f))
+                return false;
+            expr * eq = to_app(f)->get_arg(0);
+            if (!m().is_eq(f))
+                return false;
+            
+        }
+#endif
+        
+        /**
+           \brief Given t of the form (f s_0 ... s_n), 
+           return true if x occurs in some s_j for j != i 
+        */
+        bool occurs_except(expr * x, app * t, unsigned i) {
+            unsigned num = t->get_num_args();
+            for (unsigned j = 0; j < num; j++) {
+                if (i != j && occurs(x, t->get_arg(j)))
+                    return true;
+            }
+            return false;
+        }
+        
+        bool solve_arith_core(app * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
+            SASSERT(m_a_util.is_add(lhs));
+            bool is_int  = m_a_util.is_int(lhs);
+            expr * a; 
+            expr * v;
+            rational a_val;
+            unsigned num = lhs->get_num_args();
+            unsigned i;
+            for (i = 0; i < num; i++) {
+                expr * arg = lhs->get_arg(i);
+                if (is_uninterp_const(arg) && !m_candidate_vars.is_marked(arg) && check_occs(arg) && !occurs(arg, rhs) && !occurs_except(arg, lhs, i)) {
+                    a_val = rational(1); 
+                    v     = arg;
+                    break;
+                }
+                else if (m_a_util.is_mul(arg, a, v) && 
+                         is_uninterp_const(v) && !m_candidate_vars.is_marked(v) &&
+                         m_a_util.is_numeral(a, a_val) &&
+                         !a_val.is_zero() &&
+                         (!is_int || a_val.is_minus_one()) &&
+                         check_occs(v) &&
+                         !occurs(v, rhs) && 
+                         !occurs_except(v, lhs, i)) {
+                    break;
+                }
+            }
+            if (i == num)
+                return false;
+            var = to_app(v);
+            expr_ref inv_a(m());
+            if (!a_val.is_one()) {
+                inv_a = m_a_util.mk_numeral(rational(1)/a_val, is_int);
+                rhs   = m_a_util.mk_mul(inv_a, rhs);
+            }
+            
+            ptr_buffer<expr> other_args;
+            for (unsigned j = 0; j < num; j++) {
+                if (i != j) {
+                    if (inv_a)
+                        other_args.push_back(m_a_util.mk_mul(inv_a, lhs->get_arg(j)));
+                    else
+                        other_args.push_back(lhs->get_arg(j));
+                }
+            }
+            switch (other_args.size()) {
+            case 0:
+                def = rhs;
+                break;
+            case 1:
+                def = m_a_util.mk_sub(rhs, other_args[0]);
+                break;
+            default:
+                def = m_a_util.mk_sub(rhs, m_a_util.mk_add(other_args.size(), other_args.c_ptr()));
+                break;
+            }
+            if (m_produce_proofs)
+                pr = m().mk_rewrite(eq, m().mk_eq(var, def));
+            return true;
+        }
+        
+        bool solve_arith(expr * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
+            return 
+                (m_a_util.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, var, def, pr)) ||
+                (m_a_util.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, def, pr));
+        }
+        
+        bool solve(expr * f, app_ref & var, expr_ref & def, proof_ref & pr) {
+            if (m().is_eq(f)) {
+                if (trivial_solve(to_app(f)->get_arg(0), to_app(f)->get_arg(1), var, def, pr))
+                    return true;
+                if (m_theory_solver) {
+                    expr * lhs = to_app(f)->get_arg(0);
+                    expr * rhs = to_app(f)->get_arg(1);
+                    if (solve_arith(lhs, rhs, f, var, def, pr))
+                        return true;
+                }
+                return false;
+            }
+            
+            if (m().is_iff(f))
+                return trivial_solve(to_app(f)->get_arg(0), to_app(f)->get_arg(1), var, def, pr);
+            
+#if 0
+            if (not_bool_eq(f, var, def, pr))
+                return true;
+#endif
+            
+            if (m_ite_solver && m().is_ite(f))
+                return solve_ite(to_app(f), var, def, pr);
+            
+            if (is_pos_literal(f)) {
+                if (m_candidate_vars.is_marked(f))
+                    return false;
+                var = to_app(f);
+                def = m().mk_true();
+                if (m_produce_proofs) {
+                    // [rewrite]: (iff (iff l true) l)
+                    // [symmetry T1]: (iff l (iff l true))
+                    pr = m().mk_rewrite(m().mk_eq(var, def), var);
+                    pr = m().mk_symmetry(pr);
+                }
+                TRACE("solve_eqs_bug2", tout << "eliminating: " << mk_ismt2_pp(f, m()) << "\n";);
+                return true;
+            }
+            
+            if (is_neg_literal(f)) {
+                var = to_app(to_app(f)->get_arg(0));
+                if (m_candidate_vars.is_marked(var))
+                    return false;
+                def = m().mk_false();
+                if (m_produce_proofs) {
+                    // [rewrite]: (iff (iff l false) ~l)
+                    // [symmetry T1]: (iff ~l (iff l false))
+                    pr = m().mk_rewrite(m().mk_eq(var, def), f);
+                    pr = m().mk_symmetry(pr);
+                }
+                return true;
+            }
+            
+            return false;
+        }
+        
+        /**
+           \brief Start collecting candidates
+        */
+        void collect(goal const & g) {
+            m_subst->reset();
+            m_norm_subst->reset();
+            m_r->set_substitution(0);
+            m_candidate_vars.reset();
+            m_candidate_set.reset();
+            m_candidates.reset();
+            m_vars.reset();
+            
+            app_ref  var(m());
+            expr_ref  def(m());
+            proof_ref pr(m());
+            unsigned size = g.size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                checkpoint();
+                expr * f = g.form(idx);
+                if (solve(f, var, def, pr)) {
+                    m_vars.push_back(var);
+                    m_candidates.push_back(f);
+                    m_candidate_set.mark(f);
+                    m_candidate_vars.mark(var);
+                    if (m_produce_proofs) {
+                        if (pr == 0)
+                            pr = g.pr(idx);
+                        else
+                            pr = m().mk_modus_ponens(g.pr(idx), pr);
+                    }
+                    m_subst->insert(var, def, pr, g.dep(idx));
+                }
+                m_num_steps++;
+            }
+            
+            TRACE("solve_eqs", 
+                  tout << "candidate vars:\n";
+                  ptr_vector<app>::iterator it = m_vars.begin();
+                  ptr_vector<app>::iterator end = m_vars.end();
+                  for (; it != end; ++it) {
+                      tout << mk_ismt2_pp(*it, m()) << " ";
+                  }
+                  tout << "\n";);
+        }
+        
+        void sort_vars() {
+            SASSERT(m_candidates.size() == m_vars.size());
+            TRACE("solve_eqs_bug", tout << "sorting vars...\n";);
+            m_ordered_vars.reset();
+            
+
+            // The variables (and its definitions) in m_subst must remain alive until the end of this procedure.
+            // Reason: they are scheduled for unmarking in visiting/done. 
+            // They should remain alive while they are on the stack.
+            // To make sure this is the case, whenever a variable (and its definition) is removed from m_subst,
+            // I add them to the saved vector. 
+            
+            expr_ref_vector saved(m());
+            
+            expr_fast_mark1 visiting;
+            expr_fast_mark2 done;
+            
+            typedef std::pair<expr *, unsigned> frame;
+            svector<frame> todo;
+            ptr_vector<app>::const_iterator it  = m_vars.begin();
+            ptr_vector<app>::const_iterator end = m_vars.end();
+            unsigned num;
+            for (; it != end; ++it) {
+                checkpoint();
+                app * v = *it;
+                if (!m_candidate_vars.is_marked(v))
+                    continue;
+                todo.push_back(frame(v, 0));
+                while (!todo.empty()) {
+                start:
+                    frame & fr = todo.back();
+                    expr * t   = fr.first;
+                    m_num_steps++;
+                    TRACE("solve_eqs_bug", tout << "processing:\n" << mk_ismt2_pp(t, m()) << "\n";);
+                    if (t->get_ref_count() > 1 && done.is_marked(t)) {
+                        todo.pop_back();
+                        continue;
+                    }
+                    switch (t->get_kind()) {
+                    case AST_VAR:
+                        todo.pop_back();
+                        break;
+                    case AST_QUANTIFIER:
+                        num = to_quantifier(t)->get_num_children();
+                        while (fr.second < num) {
+                            expr * c = to_quantifier(t)->get_child(fr.second);
+                            fr.second++;
+                            if (c->get_ref_count() > 1 && done.is_marked(c))
+                                continue;
+                            todo.push_back(frame(c, 0));
+                            goto start;
+                        }
+                        if (t->get_ref_count() > 1)
+                            done.mark(t);
+                        todo.pop_back();
+                        break;
+                    case AST_APP:
+                        num = to_app(t)->get_num_args();
+                        if (num == 0) {
+                            if (fr.second == 0) {
+                                if (m_candidate_vars.is_marked(t)) {
+                                    if (visiting.is_marked(t)) {
+                                        // cycle detected: remove t
+                                        visiting.reset_mark(t);
+                                        m_candidate_vars.mark(t, false);
+                                        SASSERT(!m_candidate_vars.is_marked(t));
+                                        
+                                        // Must save t and its definition.
+                                        // See comment in the beginning of the function
+                                        expr * def = 0;
+                                        proof * pr;
+                                        expr_dependency * dep;
+                                        m_subst->find(to_app(t), def, pr, dep);
+                                        SASSERT(def != 0);
+                                        saved.push_back(t); 
+                                        saved.push_back(def);
+                                        // 
+                                        
+                                        m_subst->erase(t);
+                                    }
+                                    else {
+                                        visiting.mark(t);
+                                        fr.second = 1;
+                                        expr * def = 0;
+                                        proof * pr;
+                                        expr_dependency * dep;
+                                        m_subst->find(to_app(t), def, pr, dep);
+                                        SASSERT(def != 0);
+                                        todo.push_back(frame(def, 0));
+                                        goto start;
+                                    }
+                                }
+                            }
+                            else {
+                                SASSERT(fr.second == 1);
+                                if (m_candidate_vars.is_marked(t)) {
+                                    visiting.reset_mark(t);
+                                    m_ordered_vars.push_back(to_app(t));
+                                }
+                                else {
+                                    // var was removed from the list of candidate vars to elim cycle
+                                    // do nothing
+                                }
+                            }
+                        }
+                        else {
+                            while (fr.second < num) {
+                                expr * arg = to_app(t)->get_arg(fr.second);
+                                fr.second++;
+                                if (arg->get_ref_count() > 1 && done.is_marked(arg))
+                                    continue;
+                                todo.push_back(frame(arg, 0));
+                                goto start;
+                            }
+                        }
+                        if (t->get_ref_count() > 1)
+                            done.mark(t);
+                        todo.pop_back();
+                        break;
+                    default:
+                        UNREACHABLE();
+                        todo.pop_back();
+                        break;
+                    }
+                }
+            }
+            
+            // cleanup
+            it  = m_vars.begin();
+            for (unsigned idx = 0; it != end; ++it, ++idx) {
+                if (!m_candidate_vars.is_marked(*it)) {
+                    m_candidate_set.mark(m_candidates[idx], false);
+                }
+            }
+            
+            TRACE("solve_eqs", 
+                  tout << "ordered vars:\n";
+                  ptr_vector<app>::iterator it = m_ordered_vars.begin();
+                  ptr_vector<app>::iterator end = m_ordered_vars.end();
+                  for (; it != end; ++it) {
+                      SASSERT(m_candidate_vars.is_marked(*it));
+                      tout << mk_ismt2_pp(*it, m()) << " ";
+                  }
+                  tout << "\n";);
+            m_candidate_vars.reset();
+        }
+        
+        void normalize() {
+            m_norm_subst->reset();
+            m_r->set_substitution(m_norm_subst.get());
+            
+            expr_ref new_def(m());
+            proof_ref new_pr(m());
+            expr_dependency_ref new_dep(m());
+            unsigned size = m_ordered_vars.size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                checkpoint();
+                expr * v   = m_ordered_vars[idx];
+                expr * def = 0;
+                proof * pr = 0;
+                expr_dependency * dep = 0;
+                m_subst->find(v, def, pr, dep);
+                SASSERT(def != 0);
+                m_r->operator()(def, new_def, new_pr, new_dep);
+                m_num_steps += m_r->get_num_steps() + 1;
+                if (m_produce_proofs)
+                    new_pr = m().mk_transitivity(pr, new_pr);
+                if (m_produce_unsat_cores)
+                    new_dep = m().mk_join(dep, new_dep);
+                m_norm_subst->insert(v, new_def, new_pr, new_dep);
+                // we updated the substituting, but we don't need to reset m_r
+                // because all cached values there do not depend on v.
+            }
+            m_subst->reset();
+            TRACE("solve_eqs", 
+                  tout << "after normalizing variables\n";
+                  for (unsigned i = 0; i < m_ordered_vars.size(); i++) {
+                      expr * v = m_ordered_vars[i];
+                      expr * def = 0;
+                      proof * pr = 0;
+                      expr_dependency * dep = 0;
+                      m_norm_subst->find(v, def, pr, dep);
+                      tout << mk_ismt2_pp(v, m()) << "\n----->\n" << mk_ismt2_pp(def, m()) << "\n\n";
+                  });
+#if 0
+            DEBUG_CODE({
+                for (unsigned i = 0; i < m_ordered_vars.size(); i++) {
+                    expr * v = m_ordered_vars[i];
+                    expr * def = 0;
+                    proof * pr = 0;
+                    expr_dependency * dep = 0;
+                    m_norm_subst->find(v, def, pr, dep);
+                    SASSERT(def != 0);
+                    CASSERT("solve_eqs_bug", !occurs(v, def));
+                }
+            });
+#endif
+        }
+
+        void substitute(goal & g) {
+            // force the cache of m_r to be reset.
+            m_r->set_substitution(m_norm_subst.get());
+            
+            expr_ref new_f(m());
+            proof_ref new_pr(m());
+            expr_dependency_ref new_dep(m());
+            unsigned size = g.size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                checkpoint();
+                expr * f = g.form(idx);
+                TRACE("gaussian_leak", tout << "processing:\n" << mk_ismt2_pp(f, m()) << "\n";);
+                if (m_candidate_set.is_marked(f)) {
+                    // f may be deleted after the following update.
+                    // so, we must remove remove the mark before doing the update
+                    m_candidate_set.mark(f, false);
+                    SASSERT(!m_candidate_set.is_marked(f));
+                    g.update(idx, m().mk_true(), m().mk_true_proof(), 0);
+                    m_num_steps ++;
+                    continue;
+                }
+
+                m_r->operator()(f, new_f, new_pr, new_dep);
+                TRACE("solve_eqs_subst", tout << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n";);
+                m_num_steps += m_r->get_num_steps() + 1;
+                if (m_produce_proofs)
+                    new_pr = m().mk_modus_ponens(g.pr(idx), new_pr);
+                if (m_produce_unsat_cores)
+                    new_dep = m().mk_join(g.dep(idx), new_dep);
+                
+                g.update(idx, new_f, new_pr, new_dep);
+                if (g.inconsistent())
+                    return;
+            }
+            g.elim_true();
+            TRACE("solve_eqs", 
+                  tout << "after applying substitution\n";
+                  g.display(tout););
+#if 0
+            DEBUG_CODE({
+                for (unsigned i = 0; i < m_ordered_vars.size(); i++) {
+                    expr * v = m_ordered_vars[i];
+                    for (unsigned j = 0; j < g.size(); j++) {
+                        CASSERT("solve_eqs_bug", !occurs(v, g.form(j)));
+                    }
+                }});
+#endif
+        }
+
+        void save_elim_vars(model_converter_ref & mc) {
+            IF_VERBOSE(100, if (!m_ordered_vars.empty()) verbose_stream() << "num. eliminated vars: " << m_ordered_vars.size() << "\n";);
+            m_num_eliminated_vars += m_ordered_vars.size();
+            if (m_produce_models) {
+                if (mc.get() == 0)
+                    mc = alloc(gmc, m());
+                ptr_vector<app>::iterator it  = m_ordered_vars.begin();
+                ptr_vector<app>::iterator end = m_ordered_vars.end();
+                for (; it != end; ++it) {
+                    app * v    = *it;
+                    expr * def = 0;
+                    proof * pr;
+                    expr_dependency * dep;
+                    m_norm_subst->find(v, def, pr, dep);
+                    SASSERT(def != 0);
+                    static_cast<gmc*>(mc.get())->insert(v->get_decl(), def);
+                }
+            }
+        }
+        
+        void collect_num_occs(expr * t, expr_fast_mark1 & visited) {
+            ptr_buffer<expr, 128> stack;
+            
+#define VISIT(ARG) {                                                                                            \
+            if (is_uninterp_const(ARG)) {                                                                       \
+                obj_map<expr, unsigned>::obj_map_entry * entry = m_num_occs.insert_if_not_there2(ARG, 0);       \
+                entry->get_data().m_value++;                                                                    \
+            }                                                                                                   \
+            if (!visited.is_marked(ARG)) {                                                                      \
+                visited.mark(ARG, true);                                                                        \
+                stack.push_back(ARG);                                                                           \
+            }                                                                                                   \
+        }
+            
+            VISIT(t);
+            
+            while (!stack.empty()) {
+                expr * t = stack.back();
+                stack.pop_back();
+                if (!is_app(t))
+                    continue;
+                unsigned j = to_app(t)->get_num_args();
+                while (j > 0) {
+                    --j;
+                    expr * arg = to_app(t)->get_arg(j);
+                    VISIT(arg);
+                }
+            }
+        }
+        
+        void collect_num_occs(goal const & g) {
+            if (m_max_occs == UINT_MAX)
+                return; // no need to compute num occs
+            m_num_occs.reset();
+            expr_fast_mark1 visited;
+            unsigned sz = g.size();
+            for (unsigned i = 0; i < sz; i++)
+                collect_num_occs(g.form(i), visited);
+        }
+        
+        unsigned get_num_steps() const {
+            return m_num_steps;
+        }
+        
+        unsigned get_num_eliminated_vars() const {
+            return m_num_eliminated_vars;
+        }
+        
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
+            SASSERT(g->is_well_sorted());
+            mc = 0; pc = 0; core = 0;
+            tactic_report report("solve_eqs", *g);
+            m_produce_models = g->models_enabled();
+            m_produce_proofs = g->proofs_enabled();
+            m_produce_unsat_cores = g->unsat_core_enabled();
+
+            if (!g->inconsistent()) {
+                m_subst      = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
+                m_norm_subst = alloc(expr_substitution, m(), m_produce_unsat_cores, m_produce_proofs);
+                while (true) {
+                    collect_num_occs(*g);
+                    collect(*g);
+                    if (m_subst->empty()) 
+                        break;
+                    sort_vars();
+                    if (m_ordered_vars.empty())
+                        break;
+                    normalize();
+                    substitute(*(g.get()));
+                    if (g->inconsistent()) {
+                        mc   = 0;
+                        break;
+                    }
+                    save_elim_vars(mc);
+                    TRACE("solve_eqs_round", g->display(tout); if (mc) mc->display(tout););
+                }
+            }
+            g->inc_depth();
+            result.push_back(g.get());
+            TRACE("solve_eqs", g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+    };
+    
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r, bool owner):
+        m_params(p) {
+        m_imp = alloc(imp, m, p, r, owner);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(solve_eqs_tactic, m, m_params, mk_expr_simp_replacer(m, m_params), true);
+    }
+        
+    virtual ~solve_eqs_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_imp->updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        r.insert(":solve-eqs-max-occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.");
+        r.insert(":theory-solver", CPK_BOOL, "(default: true) use theory solvers.");
+        r.insert(":ite-solver", CPK_BOOL, "(default: true) use if-then-else solver.");
+    }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+        report_tactic_progress(":num-elim-vars", m_imp->get_num_eliminated_vars());
+    }
+    
+    virtual void cleanup() {
+        unsigned num_elim_vars = m_imp->m_num_eliminated_vars;
+        ast_manager & m = m_imp->m();
+        imp * d = m_imp;
+        expr_replacer * r = m_imp->m_r;
+        if (r)
+            r->set_substitution(0);
+        bool owner = m_imp->m_r_owner;
+        m_imp->m_r_owner  = false; // stole replacer
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = 0;
+        }
+        dealloc(d);
+        d = alloc(imp, m, m_params, r, owner);
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = d;
+        }
+        m_imp->m_num_eliminated_vars = num_elim_vars;
+    }
+
+    virtual void collect_statistics(statistics & st) const {
+        st.update("eliminated vars", m_imp->get_num_eliminated_vars());
+    }
+
+    virtual void reset_statistics() {
+        m_imp->m_num_eliminated_vars = 0;
+    }
+    
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+};
+
+tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p, expr_replacer * r) {
+    if (r == 0)
+        return clean(alloc(solve_eqs_tactic, m, p, mk_expr_simp_replacer(m, p), true));
+    else
+        return clean(alloc(solve_eqs_tactic, m, p, r, false));
+}
+

src/tactic/core/solve_eqs_tactic.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    solve_eqs_tactic.h
+
+Abstract:
+
+    Tactic for solving equations and performing gaussian elimination.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-29.
+
+Revision History:
+
+--*/
+#ifndef _SOLVE_EQS_TACTIC_H_
+#define _SOLVE_EQS_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+class expr_replacer;
+
+tactic * mk_solve_eqs_tactic(ast_manager & m, params_ref const & p = params_ref(), expr_replacer * r = 0);
+
+#endif
+

src/tactic/core/split_clause_tactic.cpp

@@ -0,0 +1,150 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    split_clause_tactic.cpp
+
+Abstract:
+
+    Tactic that creates a subgoal for each literal in a clause (l_1 or ... or l_n).
+    The tactic fails if the main goal does not contain any clause.
+
+Author:
+
+    Leonardo (leonardo) 2011-11-21
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"split_clause_tactic.h"
+
+class split_clause_tactic : public tactic {
+    bool          m_largest_clause;
+    
+    unsigned select_clause(ast_manager & m, goal_ref const & in) {
+        unsigned result_idx = UINT_MAX;
+        unsigned len = 0;
+        unsigned sz  = in->size();
+        for (unsigned i = 0; i < sz; i++) {
+            expr * f = in->form(i);
+            if (m.is_or(f)) {
+                unsigned curr_len = to_app(f)->get_num_args();
+                if (curr_len >= 2) {
+                    // consider only non unit clauses
+                    if (!m_largest_clause)
+                        return i;
+                    if (curr_len > len) {
+                        result_idx = i;
+                        len    = curr_len;
+                    }
+                }
+            }
+        }
+        return result_idx;
+    }
+
+    class split_pc : public proof_converter {
+        ast_manager & m_manager;
+        app *         m_clause;
+        proof *       m_clause_pr;
+    public:
+        split_pc(ast_manager & m, app * cls, proof * pr):m_manager(m), m_clause(cls), m_clause_pr(pr) {
+            m.inc_ref(cls); 
+            m.inc_ref(pr);
+        }
+
+        ~split_pc() {
+            m_manager.dec_ref(m_clause);
+            m_manager.dec_ref(m_clause_pr);
+        }
+
+        virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
+            // Let m_clause be of the form (l_0 or ... or l_{num_source - 1})
+            // Each source[i] proof is a proof for "false" using l_i as a hypothesis
+            // So, I use lemma for producing a proof for (not l_i) that does not contain the hypothesis,
+            // and unit_resolution for building a proof for the goal.
+            SASSERT(num_source == m_clause->get_num_args());
+            proof_ref_buffer prs(m);
+            prs.push_back(m_clause_pr);
+            for (unsigned i = 0; i < num_source; i++) {
+                proof * pr_i  = source[i];
+                expr * not_li = m.mk_not(m_clause->get_arg(i));
+                prs.push_back(m.mk_lemma(pr_i, not_li));
+            }
+            result = m.mk_unit_resolution(prs.size(), prs.c_ptr());
+        }
+
+        virtual proof_converter * translate(ast_translation & translator) {
+            return alloc(split_pc, translator.to(), translator(m_clause), translator(m_clause_pr));
+        }
+    };
+
+public:
+    split_clause_tactic(params_ref const & ref = params_ref()) {
+        updt_params(ref);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        split_clause_tactic * t = alloc(split_clause_tactic);
+        t->m_largest_clause = m_largest_clause;
+        return t;
+    }
+    
+    virtual ~split_clause_tactic() {
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_largest_clause = p.get_bool(":split-largest-clause", false);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) { 
+        r.insert(":split-largest-clause", CPK_BOOL, "(default: false) split the largest clause in the goal.");
+    }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        SASSERT(in->is_well_sorted());
+        tactic_report report("split-clause", *in);
+        TRACE("before_split_clause", in->display(tout););
+        pc = 0; mc = 0; core = 0; 
+        ast_manager & m = in->m();
+        unsigned cls_pos = select_clause(m, in);
+        if (cls_pos == UINT_MAX) {
+            throw tactic_exception("split-clause tactic failed, goal does not contain any clause");
+        }
+        bool produce_proofs       = in->proofs_enabled();
+        app * cls                 = to_app(in->form(cls_pos));
+        expr_dependency * cls_dep = in->dep(cls_pos);
+        if (produce_proofs)
+            pc = alloc(split_pc, m, cls, in->pr(cls_pos));
+        unsigned cls_sz = cls->get_num_args();
+        report_tactic_progress(":num-new-branches", cls_sz);
+        for (unsigned i = 0; i < cls_sz; i++) {
+            goal * subgoal_i;
+            if (i == cls_sz - 1)
+                subgoal_i = in.get();
+            else
+                subgoal_i = alloc(goal, *in);
+            expr * lit_i = cls->get_arg(i);
+            proof * pr_i = 0;
+            if (produce_proofs)
+                pr_i = m.mk_hypothesis(lit_i);
+            subgoal_i->update(cls_pos, lit_i, pr_i, cls_dep);
+            subgoal_i->inc_depth();
+            result.push_back(subgoal_i);
+        }
+    }
+    
+    virtual void cleanup() {
+        // do nothing this tactic is too simple
+    }
+};
+
+tactic * mk_split_clause_tactic(params_ref const & p) {
+    return clean(alloc(split_clause_tactic, p));
+}

src/tactic/core/split_clause_tactic.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    split_clause_tactic.h
+
+Abstract:
+
+    Tactic that creates a subgoal for each literal in a clause (l_1 or ... or l_n).
+    The tactic fails if the main goal does not contain any clause.
+
+Author:
+
+    Leonardo (leonardo) 2011-11-21
+
+Notes:
+
+--*/
+#ifndef _SPLIT_CLAUSE_TACTIC_H_
+#define _SPLIT_CLAUSE_TACTIC_H_
+
+#include"params.h"
+class tactic;
+
+tactic * mk_split_clause_tactic(params_ref const & p = params_ref());
+
+#endif

src/tactic/core/symmetry_reduce_tactic.cpp

@@ -0,0 +1,656 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    symmetry_reduce.cpp
+
+Abstract:
+
+    Add symmetry breaking predicates to goals.
+
+Author:
+
+    Nikolaj (nbjorner) 2011-05-31
+
+Notes:
+
+    This is a straight-forward and literal
+    adaption of the algorithms proposed for veriT.
+
+--*/
+#include"tactical.h"
+#include"for_each_expr.h"
+#include"map.h"
+#include"expr_replacer.h"
+#include"rewriter_def.h"
+#include"ast_pp.h"
+
+class symmetry_reduce_tactic : public tactic {
+    class imp;
+    imp *  m_imp;
+public:
+    symmetry_reduce_tactic(ast_manager & m);
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(symmetry_reduce_tactic, m);
+    }
+    
+    virtual ~symmetry_reduce_tactic();
+    
+    virtual void operator()(goal_ref const & g, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core);
+    virtual void cleanup();
+};
+
+class ac_rewriter {
+    ast_manager& m_manager;
+public:
+    ac_rewriter(ast_manager& m): m_manager(m) {}
+
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+        if ((f->is_associative() && f->is_commutative()) ||
+            m_manager.is_distinct(f)) {
+            ptr_buffer<expr> buffer;
+            buffer.append(num_args, args);
+            std::sort(buffer.begin(), buffer.end(), ast_lt_proc());
+            bool change = false;
+            for (unsigned i = 0; !change && i < num_args; ++i) {
+                change = (args[i] != buffer[i]);
+            }
+            if (change) {
+                result = m().mk_app(f, num_args, buffer.begin());
+                return BR_DONE;
+            }
+        }
+        else if (f->is_commutative() && num_args == 2 && args[0]->get_id() > args[1]->get_id()) {
+            expr* args2[2] = { args[1], args[0] };
+            result = m().mk_app(f, num_args, args2);
+            return BR_DONE;
+        }
+        return BR_FAILED;
+    }
+
+    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);
+    }
+private:
+    ast_manager& m() const { return m_manager; }
+};
+
+
+struct ac_rewriter_cfg : public default_rewriter_cfg {
+    ac_rewriter m_r;
+    bool rewrite_patterns() const { return false; }
+    bool flat_assoc(func_decl * f) const { return false; }
+    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+        result_pr = 0;
+        return m_r.mk_app_core(f, num, args, result);
+    }
+    ac_rewriter_cfg(ast_manager & m):m_r(m) {}
+};
+
+class ac_rewriter_star : public rewriter_tpl<ac_rewriter_cfg> {
+    ac_rewriter_cfg m_cfg;
+public:
+    ac_rewriter_star(ast_manager & m):
+        rewriter_tpl<ac_rewriter_cfg>(m, false, m_cfg),
+        m_cfg(m) {}
+};
+
+template class rewriter_tpl<ac_rewriter_cfg>;
+
+class symmetry_reduce_tactic::imp {
+    typedef ptr_vector<app>     permutation;
+    typedef vector<permutation> permutations;
+    typedef ptr_vector<app>     term_set;
+    typedef obj_map<app, unsigned> app_map;
+    typedef u_map<ptr_vector<app> > inv_app_map;
+    ast_manager&                m_manager;
+    ac_rewriter_star            m_rewriter;
+    scoped_ptr<expr_replacer>   m_replace;
+    
+    ast_manager& m() const { return m_manager; }
+public:
+    imp(ast_manager& m) : m_manager(m), m_rewriter(m) {
+        m_replace = mk_default_expr_replacer(m);
+    }
+
+    ~imp() {}
+
+    void operator()(goal & g) {
+        if (g.inconsistent())
+            return;
+        tactic_report report("symmetry-reduce", g);
+        vector<ptr_vector<app> > P;    
+        expr_ref fml(m());
+        to_formula(g, fml);
+        app_map occs;
+        compute_occurrences(fml, occs);
+        find_candidate_permutations(fml, occs, P);
+        if (P.empty()) {
+            return;
+        }
+        term_set T, cts;        
+        unsigned num_sym_break_preds = 0;
+        for (unsigned i = 0; i < P.size(); ++i) {
+            term_set& consts = P[i];
+            if (invariant_by_permutations(fml, consts)) {
+                cts.reset();
+                select_terms(fml, consts, T);
+                while (!T.empty() && cts.size() < consts.size()) {
+                    app* t = select_most_promising_term(fml, T, cts, consts, occs);
+                    T.erase(t);                    
+                    compute_used_in(t, cts, consts);
+                    app* c = select_const(consts, cts);
+                    if (!c) break;
+                    cts.push_back(c);
+                    expr* mem = mk_member(t, cts);
+                    g.assert_expr(mem); 
+                    num_sym_break_preds++;
+                    TRACE("symmetry_reduce", tout << "member predicate: " << mk_pp(mem, m()) << "\n";);
+                    fml = m().mk_and(fml.get(), mem);
+                    normalize(fml);
+                }
+            }
+        }
+        report_tactic_progress(":num-symmetry-breaking ", num_sym_break_preds);
+    }
+
+private:
+    void to_formula(goal const & g, expr_ref& fml) {
+        ptr_vector<expr> conjs;
+        for (unsigned i = 0; i < g.size(); ++i) {
+            conjs.push_back(g.form(i));
+        }
+        fml = m().mk_and(conjs.size(), conjs.c_ptr());
+        normalize(fml);
+    }
+
+    // find candidate permutations
+    void find_candidate_permutations(expr* fml, app_map const& occs, permutations& P) {
+        app_map coloring;
+        app_map depth;
+        inv_app_map inv_color;
+        unsigned num_occs;
+        compute_sort_colors(fml, coloring);
+        compute_max_depth(fml, depth);
+        merge_colors(occs, coloring);        
+        merge_colors(depth, coloring);     
+        // compute_siblings(fml, coloring);
+        compute_inv_app(coloring, inv_color);
+        
+        inv_app_map::iterator it = inv_color.begin(), end = inv_color.end();
+        for (; it != end; ++it) {
+            if (it->m_value.size() < 2) {
+                continue;
+            }
+            VERIFY(occs.find(it->m_value[0], num_occs));
+            if (num_occs < 2) {
+                continue;
+            }
+            bool is_const = true;
+            for (unsigned j = 0; is_const && j < it->m_value.size(); ++j) {
+                is_const = it->m_value[j]->get_num_args() == 0;
+            }
+            if (!is_const) {
+                continue;
+            }
+            P.push_back(it->m_value);
+            TRACE("symmetry_reduce",
+                for (unsigned i = 0; i < it->m_value.size(); ++i) {
+                    tout << mk_pp(it->m_value[i], m()) << " ";
+                }
+            tout << "\n";);
+        }
+    }
+
+    //
+    // refine coloring by taking most specific generalization.
+    // a |-> c1, b |-> c2 <c1,c2> |-> c
+    // 
+    struct u_pair {
+        unsigned m_first;
+        unsigned m_second;
+        u_pair(unsigned f, unsigned s) : m_first(f), m_second(s) {}
+        u_pair(): m_first(0), m_second(0) {}
+
+        struct hash {
+            unsigned operator()(u_pair const& p) const {
+                return mk_mix(p.m_first, p.m_second, 23);
+            }
+        };
+        struct eq {
+            bool operator()(u_pair const& p, u_pair const& q) const {
+                return p.m_first == q.m_first && p.m_second == q.m_second;
+            }
+        };
+    };
+    typedef map<u_pair, unsigned, u_pair::hash, u_pair::eq> pair_map;
+    bool merge_colors(app_map const& colors1, app_map& colors2) {
+        pair_map recolor;
+        unsigned num_colors = 0, v1, v2, w, old_max = 0;
+        app_map::iterator it = colors2.begin(), end = colors2.end();
+        for (; it != end; ++it) {
+            app* a = it->m_key;
+            v1 = it->m_value;
+            VERIFY(colors1.find(a, v2));
+            if (recolor.find(u_pair(v1, v2), w)) {
+                it->m_value = w;
+            }
+            else {
+                it->m_value = num_colors;
+                recolor.insert(u_pair(v1, v2), num_colors++);
+            }
+            if (v1 > old_max) old_max = v1;
+        }
+        return num_colors > old_max + 1;
+    }
+
+    class sort_colors {
+        ast_manager& m_manager;
+        app_map& m_app2sortid;
+        obj_map<sort,unsigned>  m_sort2id;
+        unsigned m_max_id;
+
+    public:
+        sort_colors(ast_manager& m, app_map& app2sort): 
+          m_manager(m), m_app2sortid(app2sort), m_max_id(0) {}
+
+        void operator()(app* n) {
+            sort* s = m_manager.get_sort(n);
+            unsigned id;
+            if (!m_sort2id.find(s, id)) {
+                id = m_max_id++;
+                m_sort2id.insert(s, id);
+            }
+            m_app2sortid.insert(n, id);
+        }
+        void operator()(quantifier * n) {}
+        void operator()(var * n) {}
+    };
+
+    void compute_sort_colors(expr* fml, app_map& app2sortId) {
+        app2sortId.reset();
+        sort_colors sc(m(), app2sortId);
+        for_each_expr(sc, fml);
+    }
+
+    void compute_inv_app(app_map const& map, inv_app_map& inv_map) {
+        app_map::iterator it = map.begin(), end = map.end();
+        for (; it != end; ++it) {
+            app* t = it->m_key;
+            unsigned n = it->m_value;
+            if (is_uninterpreted(t)) {
+                inv_app_map::entry* e = inv_map.insert_if_not_there2(n, ptr_vector<app>());
+                e->get_data().m_value.push_back(t);
+            }
+        }
+    }
+    bool is_uninterpreted(app* t) const {
+        return t->get_family_id() == null_family_id;
+    }
+
+    // compute maximal depth of terms.
+    void compute_max_depth(expr* e, app_map& depth) {
+        ptr_vector<expr> todo;
+        unsigned_vector  depths;
+        unsigned d, d1;
+        todo.push_back(e);
+        depths.push_back(0);
+        while (!todo.empty()) {
+            e = todo.back();
+            d = depths.back();
+            todo.pop_back();
+            depths.pop_back();
+            if (is_var(e)) {
+                // nothing
+            }
+            else if (is_quantifier(e)) {
+                todo.push_back(to_quantifier(e)->get_expr());
+                depths.push_back(d+1);
+            }
+            else if (is_app(e)) {
+                app* a = to_app(e);
+                if (depth.find(a, d1) && d <= d1) {
+                    continue;
+                }
+                depth.insert(a, d);                
+                ++d;
+                for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                    todo.push_back(a->get_arg(i));
+                    depths.push_back(d);
+                }
+            }
+            else {
+                UNREACHABLE();
+            }
+
+        }
+    }
+
+    // color nodes according to the function symbols they appear in
+    typedef obj_hashtable<func_decl> fun_set;
+    typedef obj_map<app, fun_set*> app_parents;
+
+    class parents {
+        app_parents m_use_funs;        
+    public:
+        parents() {}
+
+        app_parents const& get_parents() { return m_use_funs; }
+
+        void operator()(app* n) {
+            func_decl* f;
+            unsigned sz = n->get_num_args();
+            for (unsigned i = 0; i < sz; ++i) {
+                expr* e = n->get_arg(i);
+                if (is_app(e)) {
+                    app_parents::obj_map_entry* entry = m_use_funs.insert_if_not_there2(to_app(e), 0);
+                    if (!entry->get_data().m_value) entry->get_data().m_value = alloc(fun_set);
+                    entry->get_data().m_value->insert(f); 
+                }
+            }
+        }
+        void operator()(quantifier *n) {}
+        void operator()(var* n) {}
+    };
+    void compute_parents(expr* e, app_map& parents) {
+    }
+
+    typedef hashtable<unsigned, u_hash, u_eq> uint_set;
+    typedef obj_map<app, uint_set*> app_siblings;;
+
+    class siblings {
+        app_map const& m_colors;
+        app_siblings m_sibs;
+    public:
+        siblings(app_map const& colors): m_colors(colors) {}
+
+        app_siblings const& get() { return m_sibs; }
+        void operator()(app* n) {
+            unsigned sz = n->get_num_args();
+            for (unsigned i = 0; i < sz; ++i) {
+                expr* e = n->get_arg(i);
+                if (!is_app(e)) continue;
+                app_siblings::obj_map_entry* entry = m_sibs.insert_if_not_there2(to_app(e), 0);
+                if (!entry->get_data().get_value()) entry->get_data().m_value = alloc(uint_set);
+                for (unsigned j = 0; j < sz; ++j) {
+                    expr* f = n->get_arg(j);
+                    if (is_app(f) && i != j) {
+                        unsigned c1 = 0;
+                        m_colors.find(to_app(f), c1);
+                        entry->get_data().m_value->insert(c1);
+                    }
+                }
+            }
+        }
+        void operator()(quantifier *n) {}
+        void operator()(var* n) {}        
+    };
+    // refine coloring by taking colors of siblings into account.
+    bool compute_siblings_rec(expr* e, app_map& colors) {
+        siblings sibs(colors);
+        app_map colors1;
+        for_each_expr(sibs, e);
+        app_siblings const& s = sibs.get();
+        app_siblings::iterator it = s.begin(), end = s.end();
+        for (; it != end; ++it) {
+            app* a = it->m_key;
+            uint_set* set = it->m_value;
+            uint_set::iterator it2 = set->begin(), end2 = set->end();
+            unsigned c = 0;
+            for(; it2 != end2; ++it2) {
+                c += 1 + *it2;
+            }
+            colors1.insert(a, c);
+            dealloc(set);
+        }
+        if (is_app(e)) {
+            colors1.insert(to_app(e), 0);
+        }
+        return merge_colors(colors1, colors);
+    }
+    void compute_siblings(expr* fml, app_map& colors) {
+        while(compute_siblings_rec(fml, colors));
+    }
+
+    // check if assertion set is invariant under the current permutation
+    bool invariant_by_permutations(expr* fml, permutation& p) {
+
+        SASSERT(p.size() >= 2);
+        bool result = check_swap(fml, p[0], p[1]) && check_cycle(fml, p);
+        TRACE("symmetry_reduce", 
+              if (result) {
+                  tout << "Symmetric: ";
+              }
+              else {
+                  tout << "Not symmetric: ";
+              }
+              for (unsigned i = 0; i < p.size(); ++i) {
+                  tout << mk_pp(p[i], m()) << " ";
+              }
+              tout << "\n";);
+        return result;
+    }
+
+    bool check_swap(expr* fml, app* t1, app* t2) {
+        expr_substitution sub(m());
+        sub.insert(t1, t2);
+        sub.insert(t2, t1);
+        m_replace->set_substitution(&sub);
+        return check_substitution(fml);
+    }
+
+    bool check_cycle(expr* fml, permutation& p) {
+        expr_substitution sub(m());
+        for (unsigned i = 0; i + 1 < p.size(); ++i) {
+            sub.insert(p[i], p[i+1]);
+        }
+        sub.insert(p[p.size()-1], p[0]);
+        m_replace->set_substitution(&sub);
+        return check_substitution(fml);
+    }
+
+    bool check_substitution(expr* t) {
+        expr_ref r(m());
+        (*m_replace)(t, r);
+        normalize(r);
+        return t == r.get();
+    }
+
+    void normalize(expr_ref& r) {
+        proof_ref pr(m());
+        expr_ref  result(m());
+        m_rewriter(r.get(), result, pr);
+        r = result;
+    }
+
+    // select terms that are range restricted by set p.
+    void select_terms(expr* fml, term_set const& p, term_set& T) {
+        T.reset();
+        ptr_vector<expr> todo;
+        todo.push_back(fml);
+        app* t = 0;
+        while (!todo.empty()) {
+            fml = todo.back();
+            todo.pop_back();
+            if (m().is_and(fml)) {
+                todo.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());               
+            }
+            else if (is_range_restriction(fml, p, t)) {
+                T.push_back(t);
+            }
+        }
+    }
+    bool is_range_restriction(expr* form, term_set const& C, app*& t) {
+        if (!m().is_or(form)) return false;
+        unsigned sz = to_app(form)->get_num_args();
+        t = 0;
+        for (unsigned i = 0; i < sz; ++i) {
+            expr* e = to_app(form)->get_arg(i);
+            expr* e1, *e2;
+            if (!m().is_eq(e, e1, e2)) return false;
+            if (!is_app(e1) || !is_app(e2)) return false;
+            app* a1 = to_app(e1), *a2 = to_app(e2);
+            if (C.contains(a1) && (t == 0 || t == a2)) {
+                t = a2;
+            }
+            else if (C.contains(a2) && (t == 0 || t == a1)) {
+                t = a1;
+            }
+            else {
+                return false;
+            }
+        }
+        return t != 0;
+    }
+
+
+    // select the most promising term among T.
+    // terms with the largest number of occurrences have higher weight.
+    // terms that have fewest terms among C as subterms are preferred.
+    
+    class num_occurrences {
+        app_map& m_occs;
+    public:
+        num_occurrences(app_map& occs): m_occs(occs) {}
+        void operator()(app* n) {
+            app_map::obj_map_entry* e;
+            m_occs.insert_if_not_there2(n, 0);
+            unsigned sz = n->get_num_args();
+            for (unsigned i = 0; i < sz; ++i) {
+                expr* arg = n->get_arg(i);
+                if (is_app(arg)) {
+                    e = m_occs.insert_if_not_there2(to_app(arg), 0);
+                    e->get_data().m_value++;
+                }
+            }
+        }
+        void operator()(quantifier * n) {}
+        void operator()(var * n) {}
+    };
+    void compute_occurrences(expr* fml, app_map& occs) {
+        occs.reset();
+        num_occurrences num_occ(occs);
+        for_each_expr(num_occ, fml);
+    }
+
+    app* select_most_promising_term(
+        expr* fml, term_set const& T, 
+        term_set& cts, term_set const& consts, app_map const& occs) {
+        SASSERT(!T.empty());
+        app* t = T[0];
+        unsigned weight, weight1;
+        VERIFY(occs.find(t, weight));
+        unsigned cts_delta = compute_cts_delta(t, cts, consts);
+        TRACE("symmetry_reduce", tout << mk_pp(t, m()) << " " << weight << " " << cts_delta << "\n";);
+        for (unsigned i = 1; i < T.size(); ++i) {
+            app* t1 = T[i];
+            VERIFY(occs.find(t1, weight1));
+            if (weight1 < weight && t->get_num_args() <= t1->get_num_args()) {
+                continue;
+            }
+            unsigned cts_delta1 = compute_cts_delta(t1, cts, consts);
+            TRACE("symmetry_reduce", tout << mk_pp(t1, m()) << " " << weight1 << " " << cts_delta1 << "\n";);
+            if ((t->get_num_args() == t1->get_num_args() && (weight1 > weight || cts_delta1 < cts_delta)) || 
+                t->get_num_args() > t1->get_num_args()) {
+                 cts_delta = cts_delta1;
+                 weight = weight1;
+                 t = t1;
+            }
+        }        
+        return t;
+    }
+
+    // add to cts subterms of t that are members of consts.
+    class member_of {
+        term_set const& m_S;
+        term_set&       m_r;
+    public:
+        member_of(term_set const& S, term_set& r) : m_S(S), m_r(r) {}
+        void operator()(app* n) {
+            if (m_S.contains(n) && !m_r.contains(n)) {
+                m_r.push_back(n);
+            }
+        }
+        void operator()(quantifier * n) {}
+        void operator()(var * n) {}
+    };
+    void compute_used_in(app* t, term_set& cts, term_set const& consts) {
+        member_of mem(consts, cts);
+        for_each_expr(mem, t);
+        TRACE("symmetry_reduce",
+              tout << "Term: " << mk_pp(t, m()) << "\n";
+              tout << "Support set: ";
+              for (unsigned i = 0; i < consts.size(); ++i) {
+                  tout << mk_pp(consts[i], m()) << " ";
+              }
+              tout << "\n";
+              tout << "Constants: ";
+              for (unsigned i = 0; i < cts.size(); ++i) {
+                  tout << mk_pp(cts[i], m()) << " ";
+              }
+              tout << "\n";
+              );
+    }
+
+    unsigned compute_cts_delta(app* t, term_set& cts, term_set const& consts) {
+        unsigned cts_size = cts.size();
+        if (cts_size == consts.size()) {
+            return 0;
+        }
+        compute_used_in(t, cts, consts);
+        unsigned cts_delta = cts.size() - cts_size;
+        cts.resize(cts_size);
+        return cts_delta;
+    }
+
+    // select element in A not in B
+    app* select_const(term_set const& A, term_set const& B) {
+        unsigned j;
+        for (j = 0; j < A.size() && B.contains(A[j]); ++j);
+        return (j == A.size())?0:A[j];
+    }
+
+    app* mk_member(app* t, term_set const& C) {
+        expr_ref_vector eqs(m());
+        for (unsigned i = 0; i < C.size(); ++i) {
+            eqs.push_back(m().mk_eq(t, C[i]));
+        }
+        return m().mk_or(eqs.size(), eqs.c_ptr());
+    }
+};
+
+symmetry_reduce_tactic::symmetry_reduce_tactic(ast_manager & m) {
+    m_imp = alloc(imp, m);
+}
+
+symmetry_reduce_tactic::~symmetry_reduce_tactic() {
+    dealloc(m_imp);
+}
+    
+void symmetry_reduce_tactic::operator()(goal_ref const & g, 
+                                        goal_ref_buffer & result, 
+                                        model_converter_ref & mc, 
+                                        proof_converter_ref & pc,
+                                        expr_dependency_ref & core) {
+    fail_if_proof_generation("symmetry_reduce", g);
+    fail_if_unsat_core_generation("symmetry_reduce", g);
+    mc = 0; pc = 0; core = 0; result.reset();
+    (*m_imp)(*(g.get()));
+    g->inc_depth();
+    result.push_back(g.get());
+}
+
+void symmetry_reduce_tactic::cleanup() {
+    // no-op.
+}
+
+tactic * mk_symmetry_reduce_tactic(ast_manager & m, params_ref const & p) {
+    return alloc(symmetry_reduce_tactic, m);
+}

src/tactic/core/symmetry_reduce_tactic.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    symmetry_reduce.h
+
+Abstract:
+
+    Add symmetry breaking predicates to assertion sets.
+
+Author:
+
+    Nikolaj (nbjorner) 2011-05-31
+
+Notes:
+
+--*/
+#ifndef _SYMMETRY_REDUCE_TACTIC_H_
+#define _SYMMETRY_REDUCE_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_symmetry_reduce_tactic(ast_manager & m, params_ref const & p);
+
+#endif

src/tactic/core/tseitin_cnf_tactic.cpp

@@ -0,0 +1,942 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tseitin_cnf_tactic.cpp
+
+Abstract:
+
+    Puts an assertion set in CNF.
+    Auxiliary variables are used to avoid blowup.
+
+    Features:
+    
+    - Efficient encoding is used for commonly used patterns such as:
+       (iff a (iff b c))
+       (or (not (or a b)) (not (or a c)) (not (or b c)))
+
+    - Efficient encoding is used for chains of if-then-elses 
+
+    - Distributivity is applied to non-shared nodes if the blowup is acceptable.
+    
+    - The features above can be disabled/enabled using parameters.
+
+    - The assertion-set is only modified if the resultant set of clauses
+    is "acceptable".
+
+    Notes: 
+    
+    - Term-if-then-else expressions are not handled by this strategy.
+    This kind of expression should be processed by other strategies.
+
+    - Quantifiers are treated as "theory" atoms. They are viewed
+    as propositional variables by this strategy.
+    
+    - The assertion set may contain free variables. 
+
+    - This strategy assumes the assertion_set_rewriter was
+    used before invoking it.
+    In particular, it is more effective when "and" operators
+    were eliminated.
+
+    TODO: add proof production
+
+Author:
+
+    Leonardo (leonardo) 2011-12-29
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"goal_shared_occs.h"
+#include"filter_model_converter.h"
+#include"bool_rewriter.h"
+#include"simplify_tactic.h"
+#include"cooperate.h"
+
+static void swap_if_gt(expr * & n1, expr * & n2) {
+    if (n1->get_id() > n2->get_id())
+        std::swap(n1, n2);
+}
+
+/**
+   \brief Return true if n is of the form (= a b)
+*/
+static bool is_iff(ast_manager & m, expr * n, expr * & a, expr * & b) {
+    if (m.is_iff(n, a, b))
+        return true;
+    if (m.is_eq(n, a, b) && m.is_bool(a))
+        return true;
+    return false;
+}
+
+class tseitin_cnf_tactic : public tactic {
+    struct imp {
+        struct frame {
+            app *     m_t;
+            bool      m_first;
+            frame(app * n):m_t(n), m_first(true) {}
+        };
+        
+        typedef filter_model_converter mc;
+        
+        ast_manager &              m;
+        svector<frame>             m_frame_stack;
+        obj_map<app, app*>         m_cache;
+        expr_ref_vector            m_cache_domain;
+        goal_shared_occs           m_occs;
+        expr_ref_vector            m_fresh_vars;
+        ref<mc>                    m_mc;
+        expr_ref_vector            m_clauses;
+        expr_dependency_ref_vector m_deps;
+        bool_rewriter              m_rw;
+        expr_dependency *          m_curr_dep;
+        bool                       m_produce_models;
+        bool                       m_produce_unsat_cores;
+
+        // parameters
+        bool                 m_common_patterns;
+        bool                 m_distributivity;
+        unsigned             m_distributivity_blowup;
+        bool                 m_ite_chains;
+        bool                 m_ite_extra;
+        unsigned long long   m_max_memory;
+
+        unsigned             m_num_aux_vars;
+        volatile bool        m_cancel;
+
+        imp(ast_manager & _m, params_ref const & p):
+            m(_m),
+            m_cache_domain(_m),
+            m_occs(m, false /* don't track atoms */, false /* do not visit quantifiers */),
+            m_fresh_vars(_m),
+            m_clauses(_m),
+            m_deps(_m),
+            m_rw(_m),
+            m_num_aux_vars(0),
+            m_cancel(false) {
+            updt_params(p);
+            m_rw.set_flat(false);
+        }
+        
+        void updt_params(params_ref const & p) {
+            m_common_patterns = p.get_bool(":common-patterns", true);
+            m_distributivity  = p.get_bool(":distributivity",  true);
+            m_distributivity_blowup = p.get_uint(":distributivity-blowup", 32);
+            m_ite_chains      = p.get_bool(":ite-chains", true);
+            m_ite_extra       = p.get_bool(":ite-extra", true);
+            m_max_memory      = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+        }
+        
+        void push_frame(app * n) { m_frame_stack.push_back(frame(n)); }
+        
+        void throw_op_not_handled() {
+            throw tactic_exception("operator not supported, apply simplifier before invoking this strategy");
+        }
+        
+        void inv(expr * n, expr_ref & r) {
+            if (m.is_true(n)) {
+                r = m.mk_false();
+                return;
+            }
+            if (m.is_false(n)) {
+                r = m.mk_true();
+                return; 
+            }
+            if (m.is_not(n)) {
+                r = to_app(n)->get_arg(0);
+                return;
+            }
+            r = m.mk_not(n);
+        }
+
+        void mk_lit(expr * n, bool sign, expr_ref & r) {
+            if (sign)
+                r = m.mk_not(n);
+            else
+                r = n;
+        }
+        
+        void get_lit(expr * n, bool sign, expr_ref & r) {
+        start:
+            if (!is_app(n) ||
+                to_app(n)->get_num_args() == 0) {
+                mk_lit(n, sign, r);
+                return;
+            }
+            func_decl * f = to_app(n)->get_decl();
+            if (f->get_family_id() != m.get_basic_family_id()) {
+                mk_lit(n, sign, r);
+                return;
+            }
+            app * l;
+            switch (f->get_decl_kind()) {
+            case OP_NOT:
+                n    = to_app(n)->get_arg(0);
+                sign = !sign;
+                goto start;
+            case OP_OR:
+            case OP_IFF:
+                l = 0;
+                m_cache.find(to_app(n), l);
+                SASSERT(l != 0);
+                mk_lit(l, sign, r);
+                return;
+            case OP_ITE:
+            case OP_EQ:
+                if (m.is_bool(to_app(n)->get_arg(1))) {
+                    l = 0;
+                    m_cache.find(to_app(n), l);
+                    SASSERT(l != 0);
+                    mk_lit(l, sign, r);
+                    return;
+                }
+                mk_lit(n, sign, r);
+                return;
+            default:
+                TRACE("tseitin_cnf_bug", tout << f->get_name() << "\n";);
+                UNREACHABLE();
+                return;
+            }
+        }
+        
+        void visit(expr * n, bool & visited, bool root = false) {
+        start:
+            if (!is_app(n))
+                return;
+            if (m_cache.contains(to_app(n)))
+                return;
+            if (to_app(n)->get_num_args() == 0)
+                return;
+            func_decl * f = to_app(n)->get_decl();
+            if (f->get_family_id() != m.get_basic_family_id())
+                return;
+            switch (f->get_decl_kind()) {
+            case OP_NOT:
+                if (root) {
+                    visited = false;
+                    push_frame(to_app(n));
+                    return;
+                }
+                else {
+                    n = to_app(n)->get_arg(0);
+                    goto start;
+                }
+            case OP_OR:
+            case OP_IFF:
+                visited = false;
+                push_frame(to_app(n));
+                return;
+            case OP_ITE:
+            case OP_EQ:
+                if (m.is_bool(to_app(n)->get_arg(1))) {
+                    visited = false;
+                    push_frame(to_app(n));
+                }
+                return;
+            case OP_AND:
+            case OP_XOR:
+            case OP_IMPLIES:
+            case OP_DISTINCT:
+                throw_op_not_handled();
+            default:
+                return;
+            }
+        }
+        
+        bool is_shared(expr * t) {
+            return m_occs.is_shared(t);
+        }
+        
+        /**
+           \brief Return true if n is of the form
+           
+           (or (not (or a b)) (not (or a c)) (not (or b c)))
+           
+           \remark This pattern is found in the following "circuits":
+           - carry
+           - less-than (signed and unsigned)
+        */
+        bool is_or_3and(expr * n, expr * & a, expr * & b, expr * & c) {
+            expr * a1, * a2, * b1, * b2, * c1, * c2;
+            if (!m.is_or(n, a1, b1, c1) ||
+                !m.is_not(a1, a1) || 
+                is_shared(a1) ||
+                !m.is_not(b1, b1) || 
+                is_shared(b1) ||
+                !m.is_not(c1, c1) ||
+                is_shared(c1) ||
+                !m.is_or(a1, a1, a2) ||
+                !m.is_or(b1, b1, b2) ||
+                !m.is_or(c1, c1, c2))
+                return false;
+            
+            swap_if_gt(a1, a2);
+            swap_if_gt(b1, b2);
+            swap_if_gt(c1, c2);
+            
+            if ((a1 == b1 && a2 == c1 && b2 == c2) ||
+                (a1 == b1 && a2 == c2 && b2 == c1) ||
+                (a1 == c1 && a2 == b1 && b2 == c2)) {
+                a = a1; b = a2; c = b2;
+                return true;
+            }
+            
+            if ((a1 == b2 && a2 == c2 && b1 == c1) ||
+                (a1 == c1 && a2 == b2 && b1 == c2) ||
+                (a1 == c2 && a2 == b2 && b1 == c1)) {
+                a = a1; b = a2; c = b1;
+                return true;
+            }
+            
+            return false;
+        }
+        
+        
+        /**
+           \brief Return true if n is of the form
+           (iff a (iff b c))
+        */
+        bool is_iff3(expr * n, expr * & a, expr * & b, expr * & c) {
+            expr * l1, * l2;
+            if (!is_iff(m, n, l1, l2))
+                return false;
+            if (!is_shared(l1) && is_iff(m, l1, a, b)) {
+                c = l2;
+                return true;
+            }
+            if (!is_shared(l2) && is_iff(m, l2, b, c)) {
+                a = l1;
+                return true;
+            }
+            return false;
+        }
+        
+        void mk_clause(unsigned num, expr * const * ls) {
+            expr_ref cls(m);
+            m_rw.mk_or(num, ls, cls);
+            m_clauses.push_back(cls);
+            if (m_produce_unsat_cores)
+                m_deps.push_back(m_curr_dep);
+        }
+        
+        void mk_clause(expr * l1) {
+            return mk_clause(1, &l1);
+        }
+        
+        void mk_clause(expr * l1, expr * l2) {
+            expr * ls[2] = { l1, l2 };
+            mk_clause(2, ls);
+        }
+        
+        void mk_clause(expr * l1, expr * l2, expr * l3) {
+            expr * ls[3] = { l1, l2, l3 };
+            mk_clause(3, ls);
+        }
+        
+        void mk_clause(expr * l1, expr * l2, expr * l3, expr * l4) {
+            expr * ls[4] = { l1, l2, l3, l4 };
+            mk_clause(4, ls);
+        }
+        
+        app * mk_fresh() {
+            m_num_aux_vars++;
+            app * v = m.mk_fresh_const(0, m.mk_bool_sort());
+            m_fresh_vars.push_back(v);
+            if (m_mc)
+                m_mc->insert(v->get_decl());
+            return v;
+        }
+        
+        void cache_result(app * t, app * r) {
+            m_cache.insert(t, r);
+            m_cache_domain.push_back(t);
+        }
+        
+        enum mres {
+            NO,    // did not match
+            CONT,  // matched but the children need to be processed
+            DONE   // matched 
+        };
+
+        mres match_not(app * t, bool first, bool root) {
+            expr * a;
+            if (m.is_not(t, a)) {
+                if (first) {
+                    bool visited = true;
+                    visit(a, visited);
+                    if (!visited)
+                        return CONT;
+                }
+                expr_ref nla(m);
+                get_lit(a, true, nla);
+                if (root) {
+                    mk_clause(nla);
+                }
+                // Remark: don't need to do anything if it is not a root.
+                return DONE;
+            }
+            return NO;
+        }
+        
+        mres match_or_3and(app * t, bool first, bool root) {
+            if (!m_common_patterns)
+                return NO;
+            expr * a, * b, * c;
+            if (is_or_3and(t, a, b, c)) {
+                if (first) {
+                    bool visited = true;
+                    visit(a, visited);
+                    visit(b, visited);
+                    visit(c, visited);
+                    if (!visited)
+                        return CONT;
+                }
+                expr_ref nla(m), nlb(m), nlc(m);
+                get_lit(a, true, nla);
+                get_lit(b, true, nlb);
+                get_lit(c, true, nlc);
+                if (root) {
+                    mk_clause(nla, nlb);
+                    mk_clause(nla, nlc);
+                    mk_clause(nlb, nlc);
+                }
+                else {
+                    app_ref k(m), nk(m);
+                    k  = mk_fresh();
+                    nk = m.mk_not(k);
+                    mk_clause(nk, nla, nlb);
+                    mk_clause(nk, nla, nlc);
+                    mk_clause(nk, nlb, nlc);
+                    expr_ref la(m), lb(m), lc(m);
+                    inv(nla, la);
+                    inv(nlb, lb);
+                    inv(nlc, lc);
+                    mk_clause(k,  la,  lb);
+                    mk_clause(k,  la,  lc);
+                    mk_clause(k,  lb,  lc);
+                    cache_result(t, k);
+                }
+                return DONE;
+            }
+            return NO;
+        }
+
+        mres match_iff3(app * t, bool first, bool root) {
+            if (!m_common_patterns)
+                return NO;
+            expr * a, * b, * c;
+            if (is_iff3(t, a, b, c)) {
+                if (first) {
+                    bool visited = true;
+                    visit(a, visited);
+                    visit(b, visited);
+                    visit(c, visited);
+                    if (!visited)
+                        return CONT;
+                }
+                expr_ref la(m), lb(m), lc(m);
+                expr_ref nla(m), nlb(m), nlc(m);
+                get_lit(a, false, la);
+                get_lit(b, false, lb);
+                get_lit(c, false, lc);
+                inv(la, nla);
+                inv(lb, nlb);
+                inv(lc, nlc);
+                if (root) {
+                    mk_clause(la,   lb,  lc);
+                    mk_clause(la,  nlb, nlc);
+                    mk_clause(nla,  lb, nlc);
+                    mk_clause(nla, nlb,  lc); 
+                }
+                else {
+                    app_ref k(m), nk(m);
+                    k  = mk_fresh();
+                    nk = m.mk_not(k);
+                    mk_clause(nk, la,   lb,  lc);
+                    mk_clause(nk, la,  nlb, nlc);
+                    mk_clause(nk, nla,  lb, nlc);
+                    mk_clause(nk, nla, nlb,  lc); 
+                    
+                    mk_clause(k, nla, nlb, nlc);
+                    mk_clause(k, nla,  lb,  lc);
+                    mk_clause(k,  la, nlb,  lc);
+                    mk_clause(k,  la,  lb, nlc); 
+                    cache_result(t, k);
+                }
+                return DONE;
+            }
+            return NO;
+        }
+        
+        mres match_iff(app * t, bool first, bool root) {
+            expr * a, * b;
+            if (is_iff(m, t, a, b)) {
+                if (first) {
+                    bool visited = true;
+                    visit(a, visited);
+                    visit(b, visited);
+                    if (!visited)
+                        return CONT;
+                }
+                expr_ref la(m), lb(m);
+                expr_ref nla(m), nlb(m);
+                get_lit(a, false, la);
+                get_lit(b, false, lb);
+                inv(la, nla);
+                inv(lb, nlb);
+                if (root) {
+                    mk_clause(la,  nlb);
+                    mk_clause(nla,  lb);
+                }
+                else {
+                    app_ref k(m), nk(m);
+                    k  = mk_fresh();
+                    nk = m.mk_not(k);
+                    
+                    mk_clause(nk, la,  nlb);
+                    mk_clause(nk, nla,  lb);
+                    
+                    mk_clause(k, nla, nlb);
+                    mk_clause(k,  la,  lb);
+                    cache_result(t, k);
+                }
+                return DONE;
+            }
+            return NO;
+        }
+        
+        mres match_ite(app * t, bool first, bool root) {
+            if (!m.is_ite(t))
+                return NO;
+            if (first) {
+                bool visited = true;
+                app * ite = t;
+                while (true) {
+                    visit(ite->get_arg(0), visited);
+                    if (m_ite_chains && m.is_ite(ite->get_arg(1)) && !is_shared(ite->get_arg(1))) {
+                        visit(ite->get_arg(2), visited);
+                        ite = to_app(ite->get_arg(1));
+                        continue;
+                    }
+                    if (m_ite_chains && m.is_ite(ite->get_arg(2)) && !is_shared(ite->get_arg(2))) {
+                        visit(ite->get_arg(1), visited);
+                        ite = to_app(ite->get_arg(2));
+                        continue;
+                    }
+                    visit(ite->get_arg(1), visited);
+                    visit(ite->get_arg(2), visited);
+                    break;
+                }
+                if (!visited)
+                    return CONT;
+            }
+            expr_ref_buffer ctx(m);
+            expr_ref_buffer ex_pos_ctx(m); // for extra ite clauses
+            expr_ref_buffer ex_neg_ctx(m); // for extra ite clauses
+            expr_ref la(m),   lb(m), lc(m);
+            expr_ref nla(m), nlb(m), nlc(m);
+            app_ref k(m), nk(m);
+            if (!root) {
+                k = mk_fresh();
+                nk = m.mk_not(k);
+                cache_result(t, k);
+            }
+            
+#define MK_ITE_ROOT_CLS(L1, L2) {               \
+    ctx.push_back(L1); ctx.push_back(L2);       \
+    mk_clause(ctx.size(), ctx.c_ptr());         \
+    ctx.pop_back(); ctx.pop_back();             \
+}
+            
+#define MK_ITE_CLS(L1, L2, L3) {                                \
+    ctx.push_back(L1); ctx.push_back(L2); ctx.push_back(L3);    \
+    mk_clause(ctx.size(), ctx.c_ptr());                         \
+    ctx.pop_back(); ctx.pop_back(); ctx.pop_back();             \
+}
+            
+            app * ite = t;
+            while (true) {
+                get_lit(ite->get_arg(0), false, la);
+                inv(la, nla);
+                if (m_ite_chains && m.is_ite(ite->get_arg(1)) && !is_shared(ite->get_arg(1))) {
+                    get_lit(ite->get_arg(2), false, lc);
+                    if (root) {
+                        MK_ITE_ROOT_CLS(la, lc);
+                    }
+                    else {
+                        inv(lc, nlc);
+                        MK_ITE_CLS(la, lc, nk);
+                        MK_ITE_CLS(la, nlc, k);
+                        if (m_ite_extra) {
+                            ex_neg_ctx.push_back(lc);
+                            ex_pos_ctx.push_back(nlc);
+                        }
+                    }
+                    ctx.push_back(nla);
+                    ite = to_app(ite->get_arg(1));
+                    continue;
+                }
+                if (m_ite_chains && m.is_ite(ite->get_arg(2)) && !is_shared(ite->get_arg(2))) {
+                    get_lit(ite->get_arg(1), false, lb);
+                    if (root) {
+                        MK_ITE_ROOT_CLS(nla, lb);
+                    }
+                    else {
+                        inv(lb, nlb);
+                        MK_ITE_CLS(nla, lb, nk);
+                        MK_ITE_CLS(nla, nlb, k);
+                        if (m_ite_extra) {
+                            ex_neg_ctx.push_back(lb);
+                            ex_pos_ctx.push_back(nlb);
+                        }
+                    }
+                    ctx.push_back(la);
+                    ite = to_app(ite->get_arg(2));
+                    continue;
+                }
+                get_lit(ite->get_arg(1), false, lb);
+                get_lit(ite->get_arg(2), false, lc);
+                if (root) {
+                    MK_ITE_ROOT_CLS(nla, lb);
+                    MK_ITE_ROOT_CLS(la,  lc);
+                }
+                else {
+                    inv(lb, nlb);
+                    inv(lc, nlc);
+                    MK_ITE_CLS(nla, lb, nk);
+                    MK_ITE_CLS(la,  lc, nk);
+                    MK_ITE_CLS(nla, nlb, k);
+                    MK_ITE_CLS(la,  nlc, k);
+                    if (m_ite_extra) {
+                        MK_ITE_CLS(lb,   lc, nk);
+                        MK_ITE_CLS(nlb, nlc, k);
+                        
+                        ex_neg_ctx.push_back(lb); ex_neg_ctx.push_back(lc); ex_neg_ctx.push_back(nk);
+                        mk_clause(ex_neg_ctx.size(), ex_neg_ctx.c_ptr());
+                        ex_pos_ctx.push_back(nlb); ex_pos_ctx.push_back(nlc); ex_pos_ctx.push_back(k);
+                        mk_clause(ex_pos_ctx.size(), ex_pos_ctx.c_ptr());
+                    }
+                }
+                break;
+            }
+            return DONE;
+        }
+        
+        mres match_or(app * t, bool first, bool root) {
+            if (!m.is_or(t))
+                return NO;
+            if (first) {
+                bool visited = true;
+                unsigned num = t->get_num_args();
+                unsigned blowup = 1;
+                for (unsigned i = 0; i < num; i++) {
+                    expr * a = t->get_arg(i);
+                    expr * a0;
+                    if (m_distributivity && m.is_not(a, a0) && m.is_or(a0) && !is_shared(a0)) {
+                        unsigned num2 = to_app(a0)->get_num_args();
+                        if (num2 < m_distributivity_blowup && blowup * num2 < m_distributivity_blowup && blowup < blowup * num2) { 
+                            blowup *= num2;
+                            for (unsigned j = 0; j < num2; j++)
+                                visit(to_app(a0)->get_arg(j), visited);
+                            continue;
+                        }
+                    }
+                    visit(a, visited);
+                }
+                if (!visited)
+                    return CONT;
+            }
+            
+            app_ref k(m), nk(m);
+            if (!root) {
+                k = mk_fresh();
+                nk = m.mk_not(k);
+                cache_result(t, k);
+            }
+            
+            unsigned num = t->get_num_args();
+            bool distributivity = false;
+            if (m_distributivity) {
+                // check if need to apply distributivity
+                for (unsigned i = 0; i < num; i++) {
+                    expr * a = t->get_arg(i);
+                    expr * a0;
+                    if (m.is_not(a, a0) && m.is_or(a0) && !is_shared(a0) && to_app(a0)->get_num_args() < m_distributivity_blowup) {
+                        distributivity = true;
+                        break;
+                    }
+                }
+            }
+            
+            if (!distributivity) {
+                // easy case
+                expr_ref_buffer lits(m); expr_ref l(m);
+                for (unsigned i = 0; i < num; i++) {
+                    get_lit(t->get_arg(i), false, l);
+                    lits.push_back(l);
+                }
+                if (root) {
+                    mk_clause(lits.size(), lits.c_ptr());
+                }
+                else {
+                    for (unsigned i = 0; i < num; i++) {
+                        inv(lits[i], l);
+                        mk_clause(l, k);
+                    }
+                    lits.push_back(nk);
+                    mk_clause(lits.size(), lits.c_ptr());
+                }
+            }
+            else {
+                expr_ref_buffer buffer(m); expr_ref l(m), nl(m);
+                sbuffer<unsigned> szs;
+                sbuffer<unsigned> it;
+                sbuffer<unsigned> offsets;
+                unsigned blowup = 1;
+                for (unsigned i = 0; i < num; i++) {
+                    it.push_back(0);
+                    offsets.push_back(buffer.size());
+                    expr * a = t->get_arg(i);
+                    expr * a0;
+                    if (m.is_not(a, a0) && m.is_or(a0) && !is_shared(a0)) {
+                        unsigned num2 = to_app(a0)->get_num_args();
+                        if (num2 < m_distributivity_blowup && blowup * num2 < m_distributivity_blowup && blowup < blowup * num2) { 
+                            szs.push_back(num2);
+                            blowup *= num2;
+                            expr_ref_buffer lits(m);
+                            for (unsigned j = 0; j < num2; j++) {
+                                get_lit(to_app(a0)->get_arg(j), true, nl);
+                                buffer.push_back(nl);
+                                if (!root) {
+                                    inv(nl, l);
+                                    lits.push_back(l);
+                                }
+                            }
+                            if (!root) {
+                                lits.push_back(k);
+                                mk_clause(lits.size(), lits.c_ptr());
+                            }
+                            continue;
+                        }
+                    }
+                    szs.push_back(1);
+                    get_lit(a, false, l);
+                    buffer.push_back(l);
+                    if (!root) {
+                        inv(l, nl);
+                        mk_clause(nl, k); 
+                    }
+                }
+                SASSERT(offsets.size() == num);
+                sbuffer<expr**> arg_lits;
+                ptr_buffer<expr> lits;
+                expr ** buffer_ptr = buffer.c_ptr();
+                for (unsigned i = 0; i < num; i++) {
+                    arg_lits.push_back(buffer_ptr + offsets[i]);
+                }
+                do {
+                    lits.reset();
+                    for (unsigned i = 0; i < num; i++) {
+                        lits.push_back(arg_lits[i][it[i]]);
+                    }
+                    if (!root)
+                        lits.push_back(nk);
+                    mk_clause(lits.size(), lits.c_ptr());
+                }
+                while (product_iterator_next(szs.size(), szs.c_ptr(), it.c_ptr()));
+            }
+            return DONE;
+        }
+        
+#define TRY(_MATCHER_)                                          \
+    r = _MATCHER_(t, first, t == root);                         \
+    if (r == CONT) goto loop;                                   \
+    if (r == DONE) { m_frame_stack.pop_back(); continue; }
+        
+        void set_cancel(bool f) {
+            m_cancel = f;
+        }
+        
+        void checkpoint() {
+            cooperate("tseitin cnf");
+            if (m_cancel)
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+            if (memory::get_allocation_size() > m_max_memory)
+                throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+        }
+
+        void process(expr * n, expr_dependency * dep) {
+            m_curr_dep = dep;
+            bool visited = true;
+            visit(n, visited, true);
+            if (visited) {
+                expr_ref l(m);
+                get_lit(n, false, l);
+                mk_clause(l);
+                return;
+            }
+            expr * root = n;
+            
+            app * t; bool first; mres r;
+            while (!m_frame_stack.empty()) {
+            loop:
+                checkpoint();
+                frame & fr = m_frame_stack.back();
+                t = fr.m_t;
+                first = fr.m_first;
+                fr.m_first = false;
+                TRY(match_or_3and);
+                TRY(match_or);
+                TRY(match_iff3);
+                TRY(match_iff);
+                TRY(match_ite);
+                TRY(match_not);
+                UNREACHABLE();
+            }
+        }
+
+        void reset_cache() {
+            m_cache.reset();
+            m_cache_domain.reset();
+        }
+
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
+            SASSERT(g->is_well_sorted());
+            mc = 0; pc = 0; core = 0;
+            tactic_report report("tseitin-cnf", *g);
+            fail_if_proof_generation("tseitin-cnf", g);
+            m_produce_models      = g->models_enabled();
+            m_produce_unsat_cores = g->unsat_core_enabled(); 
+
+            m_occs(*g);
+            reset_cache();
+            m_deps.reset();
+            m_fresh_vars.reset();
+            m_frame_stack.reset();
+            m_clauses.reset();
+            if (m_produce_models)
+                m_mc = alloc(filter_model_converter, m);
+            else
+                m_mc = 0;
+
+            unsigned size = g->size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                process(g->form(idx), g->dep(idx));
+                g->update(idx, m.mk_true(), 0, 0); // to save memory
+            }
+
+            SASSERT(!m_produce_unsat_cores || m_clauses.size() == m_deps.size());
+
+            g->reset();
+            unsigned sz = m_clauses.size();
+            expr_fast_mark1 added;
+            for (unsigned i = 0; i < sz; i++) {
+                expr * cls = m_clauses.get(i);
+                if (added.is_marked(cls))
+                    continue;
+                added.mark(cls);
+                if (m_produce_unsat_cores)
+                    g->assert_expr(cls, 0, m_deps.get(i));
+                else
+                    g->assert_expr(cls);
+            }
+            if (m_produce_models && !m_fresh_vars.empty()) 
+                mc = m_mc.get();
+            else
+                mc = 0;
+            g->inc_depth();
+            result.push_back(g.get());
+            TRACE("tseitin_cnf", g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+    };
+    
+    imp *      m_imp;
+    params_ref m_params;
+public:
+    tseitin_cnf_tactic(ast_manager & m, params_ref const & p):
+        m_params(p) {
+        m_imp = alloc(imp, m, p);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(tseitin_cnf_tactic, m, m_params);
+    }
+        
+    virtual ~tseitin_cnf_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_imp->updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        insert_max_memory(r);
+        r.insert(":common-patterns", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing commonly used patterns");
+        r.insert(":distributivity", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by applying distributivity over unshared subformulas");
+        r.insert(":distributivity-blowup", CPK_UINT, "(default: 32) maximum overhead for applying distributivity during CNF encoding");
+        r.insert("ite-chaing", CPK_BOOL, "(default: true) minimize the number of auxiliary variables during CNF encoding by identifing if-then-else chains");                                                       
+        r.insert(":ite-extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas");
+    }
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+        report_tactic_progress(":cnf-aux-vars", m_imp->m_num_aux_vars);
+    }
+    
+    virtual void cleanup() {
+        unsigned num_aux_vars = m_imp->m_num_aux_vars;
+        ast_manager & m = m_imp->m;
+        imp * d = m_imp;
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = 0;
+        }
+        dealloc(d);
+        d = alloc(imp, m, m_params);
+        #pragma omp critical (tactic_cancel)
+        {
+            m_imp = d;
+        }
+        m_imp->m_num_aux_vars = num_aux_vars;
+    }
+
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+
+    virtual void collect_statistics(statistics & st) const {
+        st.update("cnf encoding aux vars", m_imp->m_num_aux_vars);
+    }
+    
+    virtual void reset_statistics() {
+        m_imp->m_num_aux_vars = 0;
+    }
+};
+
+tactic * mk_tseitin_cnf_core_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(tseitin_cnf_tactic, m, p));
+}
+
+tactic * mk_tseitin_cnf_tactic(ast_manager & m, params_ref const & p) {
+    params_ref simp_p = p;
+    simp_p.set_bool(":elim-and", true);
+    simp_p.set_bool(":blast-distinct", true);
+    return or_else(mk_tseitin_cnf_core_tactic(m, p),
+                   and_then(using_params(mk_simplify_tactic(m, p), simp_p),
+                            mk_tseitin_cnf_core_tactic(m, p)));
+}

src/tactic/core/tseitin_cnf_tactic.h

@@ -0,0 +1,31 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tseitin_cnf_tactic.h
+
+Abstract:
+
+    Puts an assertion set in CNF.
+    Auxiliary variables are used to avoid blowup.
+
+Author:
+
+    Leonardo (leonardo) 2011-12-29
+
+Notes:
+
+--*/
+#ifndef _TSEITIN_CNF_TACTIC_H_
+#define _TSEITIN_CNF_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_tseitin_cnf_core_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+tactic * mk_tseitin_cnf_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif