checkpoint

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

src/tactic/converter.h

@@ -0,0 +1,142 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    converter.h
+
+Abstract:
+
+    Abstract class and templates for proof and model converters.
+
+Author:
+
+    Leonardo (leonardo) 2011-11-14
+
+Notes:
+
+--*/
+#ifndef _CONVERTER_H_
+#define _CONVERTER_H_
+
+#include"vector.h"
+#include"ref.h"
+#include"ast_translation.h"
+
+class converter {
+    unsigned m_ref_count;
+public:
+    converter():m_ref_count(0) {}
+    virtual ~converter() {}
+
+    void inc_ref() { ++m_ref_count; }
+    void dec_ref() { 
+        --m_ref_count;
+        if (m_ref_count == 0)
+            dealloc(this);
+    }
+
+    virtual void cancel() {}
+    
+    // for debugging purposes
+    virtual void display(std::ostream & out) {}
+};
+
+template<typename T>
+class concat_converter : public T {
+protected:
+    ref<T> m_c1;
+    ref<T> m_c2;
+
+    template<typename T2>
+    T * translate_core(ast_translation & translator) {
+        T * t1 = m_c1->translate(translator);
+        T * t2 = m_c2->translate(translator);
+        return alloc(T2, t1, t2);
+    }
+
+public:
+    concat_converter(T * c1, T * c2):m_c1(c1), m_c2(c2) {}
+    
+    virtual ~concat_converter() {}
+
+    virtual void cancel() {
+        m_c2->cancel();
+        m_c1->cancel();
+    }
+
+    virtual char const * get_name() const = 0;
+    
+    virtual void display(std::ostream & out) {
+        out << "(" << get_name() << "\n";
+        m_c1->display(out);
+        m_c2->display(out);
+        out << ")\n";
+    }
+};
+
+template<typename T>
+class concat_star_converter : public T {
+protected:
+    ref<T>          m_c1;
+    ptr_vector<T>   m_c2s;
+    unsigned_vector m_szs;
+
+    template<typename T2>
+    T * translate_core(ast_translation & translator) {
+        T * t1 = m_c1 ? m_c1->translate(translator) : 0;
+        ptr_buffer<T> t2s;
+        unsigned num = m_c2s.size();
+        for (unsigned i = 0; i < num; i++)
+            t2s.push_back(m_c2s[i] ? m_c2s[i]->translate(translator) : 0);
+        return alloc(T2, t1, num, t2s.c_ptr(), m_szs.c_ptr());
+    }
+
+public:
+    concat_star_converter(T * c1, unsigned num, T * const * c2s, unsigned * szs):
+        m_c1(c1) {
+        for (unsigned i = 0; i < num; i++) {
+            T * c2 = c2s[i];
+            if (c2)
+                c2->inc_ref();
+            m_c2s.push_back(c2);
+            m_szs.push_back(szs[i]);
+        }
+    }
+
+    virtual ~concat_star_converter() {
+        unsigned sz = m_c2s.size();
+        for (unsigned i = 0; i < sz; i++) {
+            T * c2 = m_c2s[i];
+            if (c2)
+                c2->dec_ref();
+        }
+    }
+
+    virtual void cancel() {
+        if (m_c1)
+            m_c1->cancel();
+        unsigned num = m_c2s.size();
+        for (unsigned i = 0; i < num; i++) {
+            if (m_c2s[i])
+                m_c2s[i]->cancel();
+        }
+    }
+
+    virtual char const * get_name() const = 0;
+    
+    virtual void display(std::ostream & out) {
+        out << "(" << get_name() << "\n";
+        if (m_c1)
+            m_c1->display(out);
+        out << "(\n";
+        unsigned num = m_c2s.size();
+        for (unsigned i = 0; i < num; i++)
+            if (m_c2s[i])
+                m_c2s[i]->display(out);
+        out << "))\n";
+    }
+};
+
+#endif
+

src/tactic/extension_model_converter.cpp

@@ -0,0 +1,121 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    extension_model_converter.cpp
+
+Abstract:
+
+    Model converter that introduces eliminated variables in a model.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-21
+
+Notes:
+
+--*/
+#include"extension_model_converter.h"
+#include"model_evaluator.h"
+#include"ast_smt2_pp.h"
+#include"model_v2_pp.h"
+#include"ast_pp.h"
+
+extension_model_converter::~extension_model_converter() {
+}
+
+struct extension_model_converter::set_eval {
+    extension_model_converter * m_owner;
+    model_evaluator *          m_old;
+    set_eval(extension_model_converter * owner, model_evaluator * ev) {
+        m_owner = owner;
+        m_old   = owner->m_eval;
+        #pragma omp critical (extension_model_converter) 
+        {
+            owner->m_eval = ev;
+        }
+    }
+    ~set_eval() {
+        #pragma omp critical (extension_model_converter)
+        {
+            m_owner->m_eval = m_old;
+        }
+    }
+    
+};
+
+static void display_decls_info(std::ostream & out, model_ref & md) {
+    ast_manager & m = md->get_manager();
+    unsigned sz = md->get_num_decls();
+    for (unsigned i = 0; i < sz; i++) {
+        func_decl * d = md->get_decl(i);
+        out << d->get_name();
+        out << " (";
+        for (unsigned j = 0; j < d->get_arity(); j++)
+            out << mk_pp(d->get_domain(j), m);
+        out << mk_pp(d->get_range(), m);
+        out << ") ";
+        if (d->get_info())
+            out << *(d->get_info());
+        out << " :id " << d->get_id() << "\n";
+    }
+}
+
+void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) {
+    SASSERT(goal_idx == 0);
+    TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
+    model_evaluator ev(*(md.get()));
+    ev.set_model_completion(true);
+    expr_ref val(m());
+    {
+        set_eval setter(this, &ev);
+        unsigned i = m_vars.size();
+        while (i > 0) {
+            --i;
+            expr * def = m_defs.get(i);
+            ev(def, val);
+            TRACE("extension_mc", tout << m_vars.get(i)->get_name() << " ->\n" << mk_ismt2_pp(def, m()) << "\n==>\n" << mk_ismt2_pp(val, m()) << "\n";);
+            func_decl * f  = m_vars.get(i);
+            unsigned arity = f->get_arity();
+            if (arity == 0) {
+                md->register_decl(f, val);
+            }
+            else {
+                func_interp * new_fi = alloc(func_interp, m(), arity);
+                new_fi->set_else(val);
+                md->register_decl(f, new_fi);
+            }
+        }
+    }
+    TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md););
+}
+
+void extension_model_converter::cancel() {
+    #pragma omp critical (extension_model_converter) 
+    {
+        if (m_eval)
+            m_eval->cancel();
+    }
+}
+
+void extension_model_converter::display(std::ostream & out) {
+    ast_manager & m = m_vars.get_manager();
+    out << "(extension-model-converter";
+    for (unsigned i = 0; i < m_vars.size(); i++) {
+        out << "\n  (" << m_vars.get(i)->get_name() << " ";
+        unsigned indent = m_vars.get(i)->get_name().size() + 4;
+        out << mk_ismt2_pp(m_defs.get(i), m, indent) << ")";
+    }
+    out << ")" << std::endl;
+}
+
+model_converter * extension_model_converter::translate(ast_translation & translator) {
+    extension_model_converter * res = alloc(extension_model_converter, translator.to());    
+    for (unsigned i = 0; i < m_vars.size(); i++)
+        res->m_vars.push_back(translator(m_vars[i].get()));
+    for (unsigned i = 0; i < m_defs.size(); i++)
+        res->m_defs.push_back(translator(m_defs[i].get()));    
+    // m_eval is a transient object. So, it doesn't need to be translated.
+    return res;
+}

src/tactic/extension_model_converter.h

@@ -0,0 +1,57 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    extension_model_converter.h
+
+Abstract:
+
+    Model converter that introduces new interpretations into a model.
+    It used to be called elim_var_model_converter
+
+Author:
+
+    Leonardo (leonardo) 2011-10-21
+
+Notes:
+
+--*/
+#ifndef _EXTENSION_MODEL_CONVERTER_H_
+#define _EXTENSION_MODEL_CONVERTER_H_
+
+#include"ast.h"
+#include"model_converter.h"
+
+class model_evaluator;
+
+class extension_model_converter : public model_converter {
+    func_decl_ref_vector  m_vars;
+    expr_ref_vector       m_defs;
+    model_evaluator *     m_eval;
+    struct set_eval;
+public:    
+    extension_model_converter(ast_manager & m):m_vars(m), m_defs(m), m_eval(0) {
+    }
+    
+    virtual ~extension_model_converter();
+    
+    ast_manager & m() const { return m_vars.get_manager(); }
+    
+    virtual void operator()(model_ref & md, unsigned goal_idx);
+
+    virtual void cancel();
+
+    virtual void display(std::ostream & out);
+
+    // register a variable that was eliminated
+    void insert(func_decl * v, expr * def) {
+        m_vars.push_back(v);
+        m_defs.push_back(def);
+    }
+
+    virtual model_converter * translate(ast_translation & translator);
+};
+
+
+#endif

src/tactic/filter_model_converter.cpp

@@ -0,0 +1,66 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    filter_model_converter.cpp
+
+Abstract:
+
+    Filter decls from a model
+
+Author:
+
+    Leonardo (leonardo) 2011-05-06
+
+Notes:
+
+--*/
+#include"filter_model_converter.h"
+#include"model_v2_pp.h"
+
+filter_model_converter::~filter_model_converter() {
+}
+
+void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx) {
+    TRACE("filter_mc", tout << "before filter_model_converter\n"; model_v2_pp(tout, *old_model); display(tout););
+    ast_fast_mark1 fs;
+    unsigned num = m_decls.size();
+    for (unsigned i = 0; i < num; i++) 
+        fs.mark(m_decls.get(i));
+    model * new_model = alloc(model, m());
+    num = old_model->get_num_constants();
+    for (unsigned i = 0; i < num; i++) {
+        func_decl * f = old_model->get_constant(i);
+        if (fs.is_marked(f))
+            continue;
+        expr * fi     = old_model->get_const_interp(f);
+        new_model->register_decl(f, fi);
+    }
+    num = old_model->get_num_functions();
+    for (unsigned i = 0; i < num; i++) {
+        func_decl * f = old_model->get_function(i);
+        if (fs.is_marked(f))
+            continue;
+        func_interp * fi = old_model->get_func_interp(f);
+        new_model->register_decl(f, fi->copy());
+    }
+    new_model->copy_usort_interps(*old_model);
+    old_model = new_model;
+    TRACE("filter_mc", tout << "after filter_model_converter\n"; model_v2_pp(tout, *old_model););
+}
+
+void filter_model_converter::display(std::ostream & out) {
+    out << "(filter-model-converter";
+    for (unsigned i = 0; i < m_decls.size(); i++) {
+        out << " " << m_decls.get(i)->get_name();
+    }
+    out << ")" << std::endl;
+}
+
+model_converter * filter_model_converter::translate(ast_translation & translator) {
+    filter_model_converter * res = alloc(filter_model_converter, translator.to());
+    for (unsigned i = 0; i < m_decls.size(); i++)
+        res->m_decls.push_back(translator(m_decls[i].get()));
+    return res;
+}

src/tactic/filter_model_converter.h

@@ -0,0 +1,48 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    filter_model_converter.h
+
+Abstract:
+
+    Filter decls from a model
+
+Author:
+
+    Leonardo (leonardo) 2011-05-06
+
+Notes:
+
+--*/
+#ifndef _FILTER_MODEL_CONVERTER_H_
+#define _FILTER_MODEL_CONVERTER_H_
+
+#include"model_converter.h"
+
+class filter_model_converter : public model_converter {
+    func_decl_ref_vector  m_decls;
+public:
+    filter_model_converter(ast_manager & m):m_decls(m) {}
+    
+    virtual ~filter_model_converter();
+    
+    ast_manager & m() const { return m_decls.get_manager(); }
+    
+    virtual void operator()(model_ref & md, unsigned goal_idx);
+
+    virtual void operator()(model_ref & md) { operator()(md, 0); } // TODO: delete
+
+    virtual void cancel() {}
+
+    virtual void display(std::ostream & out);
+
+    void insert(func_decl * d) {
+        m_decls.push_back(d);
+    }
+
+    virtual model_converter * translate(ast_translation & translator);
+};
+
+#endif

src/tactic/goal.cpp

@@ -0,0 +1,603 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    goal.cpp
+
+Abstract:
+
+    Proof / Model finding Goals
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-10-12
+
+Revision History:
+
+--*/
+#include"goal.h"
+#include"ast_ll_pp.h"
+#include"ast_smt2_pp.h"
+#include"for_each_expr.h"
+#include"well_sorted.h"
+
+std::ostream & operator<<(std::ostream & out, goal::precision p) {
+    switch (p) {
+    case goal::PRECISE: out << "precise"; break;
+    case goal::UNDER:   out << "under"; break;
+    case goal::OVER:    out << "over"; break;
+    case goal::UNDER_OVER: out << "under-over"; break;
+    }
+    return out;
+}
+
+void goal::copy_to(goal & target) const {
+    SASSERT(&m_manager == &(target.m_manager));
+    if (this == &target)
+        return;
+
+    m().copy(m_forms, target.m_forms);
+    m().copy(m_proofs, target.m_proofs);
+    m().copy(m_dependencies, target.m_dependencies);
+
+    target.m_depth                = std::max(m_depth, target.m_depth);
+    SASSERT(target.m_proofs_enabled == m_proofs_enabled);
+    SASSERT(target.m_core_enabled   == m_core_enabled);
+    target.m_inconsistent         = m_inconsistent;
+    target.m_precision            = mk_union(prec(), target.prec());
+}
+
+void goal::push_back(expr * f, proof * pr, expr_dependency * d) {
+    if (m().is_true(f))
+        return;
+    if (m().is_false(f)) {
+        m().del(m_forms);
+        m().del(m_proofs);
+        m().del(m_dependencies);
+        m_inconsistent = true;
+    }
+    else {
+        SASSERT(!m_inconsistent);
+    }
+    m().push_back(m_forms, f);
+    if (proofs_enabled())
+        m().push_back(m_proofs, pr);
+    if (unsat_core_enabled())
+        m().push_back(m_dependencies, d);
+}
+
+void goal::quick_process(bool save_first, expr * & f, expr_dependency * d) {
+    if (!m().is_and(f) && !(m().is_not(f) && m().is_or(to_app(f)->get_arg(0)))) {
+        if (!save_first) {
+            push_back(f, 0, d);
+        }
+        return; 
+    }
+    typedef std::pair<expr *, bool> expr_pol;
+    sbuffer<expr_pol, 64> todo;
+    todo.push_back(expr_pol(f, true));
+    while (!todo.empty()) {
+        if (m_inconsistent)
+            return;
+        expr_pol p  = todo.back();
+        expr * curr = p.first;
+        bool   pol  = p.second;
+        todo.pop_back();
+        if (pol && m().is_and(curr)) {
+            app * t = to_app(curr);
+            unsigned i = t->get_num_args();
+            while (i > 0) {
+                --i;
+                todo.push_back(expr_pol(t->get_arg(i), true));
+            }
+        }
+        else if (!pol && m().is_or(curr)) {
+            app * t = to_app(curr);
+            unsigned i = t->get_num_args();
+            while (i > 0) {
+                --i;
+                todo.push_back(expr_pol(t->get_arg(i), false));
+            }
+        }
+        else if (m().is_not(curr)) {
+            todo.push_back(expr_pol(to_app(curr)->get_arg(0), !pol));
+        }
+        else {
+            if (!pol) 
+                curr = m().mk_not(curr);
+            if (save_first) {
+                f  = curr;
+                save_first = false;
+            }
+            else {
+                push_back(curr, 0, d);
+            }
+        }
+    }
+}
+
+void goal::process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    unsigned num = f->get_num_args();
+    for (unsigned i = 0; i < num; i++) {
+        if (m_inconsistent)
+            return;
+        slow_process(save_first && i == 0, f->get_arg(i), m().mk_and_elim(pr, i), d, out_f, out_pr);
+    }
+}
+
+void goal::process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    unsigned num = f->get_num_args();
+    for (unsigned i = 0; i < num; i++) {
+        if (m_inconsistent)
+            return;
+        expr * child = f->get_arg(i);
+        if (m().is_not(child)) {
+            expr * not_child = to_app(child)->get_arg(0);
+            slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
+        }
+        else {
+            expr_ref not_child(m());
+            not_child = m().mk_not(child);
+            slow_process(save_first && i == 0, not_child, m().mk_not_or_elim(pr, i), d, out_f, out_pr);
+        }
+    }
+}
+
+void goal::slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr) {
+    if (m().is_and(f)) 
+        process_and(save_first, to_app(f), pr, d, out_f, out_pr);
+    else if (m().is_not(f) && m().is_or(to_app(f)->get_arg(0))) 
+        process_not_or(save_first, to_app(to_app(f)->get_arg(0)), pr, d, out_f, out_pr);
+    else if (save_first) {
+        out_f  = f;
+        out_pr = pr;
+    }
+    else {
+        push_back(f, pr, d);
+    }
+}
+
+void goal::slow_process(expr * f, proof * pr, expr_dependency * d) {
+    expr_ref out_f(m());
+    proof_ref out_pr(m());
+    slow_process(false, f, pr, d, out_f, out_pr);
+}
+
+void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) {
+    SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
+    if (m_inconsistent)
+        return;
+    if (proofs_enabled())
+        slow_process(f, pr, d);
+    else
+        quick_process(false, f, d);
+}
+
+void goal::get_formulas(ptr_vector<expr> & result) {
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        result.push_back(form(i));
+    }
+}
+
+void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
+    SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
+    if (m_inconsistent)
+        return;
+    if (proofs_enabled()) {
+        expr_ref out_f(m());
+        proof_ref out_pr(m());
+        slow_process(true, f, pr, d, out_f, out_pr);
+        if (!m_inconsistent) {
+            if (m().is_false(out_f)) {
+                push_back(out_f, out_pr, d);
+            }
+            else {
+                m().set(m_forms, i, out_f);
+                m().set(m_proofs, i, out_pr);
+                if (unsat_core_enabled()) 
+                    m().set(m_dependencies, i, d);
+            }
+        }
+    }
+    else {
+        quick_process(true, f, d);
+        if (!m_inconsistent) {
+            if (m().is_false(f)) {
+                push_back(f, 0, d);
+            }
+            else {
+                m().set(m_forms, i, f);
+                if (unsat_core_enabled()) 
+                    m().set(m_dependencies, i, d);
+            }
+        }
+    }
+}
+
+void goal::reset_core() {
+    m().del(m_forms);
+    m().del(m_proofs);
+    m().del(m_dependencies);
+}
+
+void goal::reset_all() {
+    reset_core();
+    m_depth = 0;
+    m_inconsistent = false;
+    m_precision = PRECISE;
+}
+
+void goal::reset() { 
+    reset_core(); 
+    m_inconsistent = false; 
+}
+
+void goal::display(ast_printer & prn, std::ostream & out) const {
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  ";
+        prn.display(out, form(i), 2);
+    }
+    out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+}
+
+void goal::display_with_dependencies(ast_printer & prn, std::ostream & out) const {
+    ptr_vector<expr> deps;
+    obj_hashtable<expr> to_pp;
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  |-";
+        deps.reset();
+        m().linearize(dep(i), deps);
+        ptr_vector<expr>::iterator it  = deps.begin();
+        ptr_vector<expr>::iterator end = deps.end();
+        for (; it != end; ++it) {
+            expr * d = *it;
+            if (is_uninterp_const(d)) {
+                out << " " << mk_ismt2_pp(d, m());
+            }
+            else {
+                out << " #" << d->get_id();
+                to_pp.insert(d);
+            }
+        }
+        out << "\n  ";
+        prn.display(out, form(i), 2);
+    }
+    if (!to_pp.empty()) {
+        out << "\n  :dependencies-definitions (";
+        obj_hashtable<expr>::iterator it  = to_pp.begin();
+        obj_hashtable<expr>::iterator end = to_pp.end();
+        for (; it != end; ++it) {
+            expr * d = *it;
+            out << "\n  (#" << d->get_id() << "\n  ";
+            prn.display(out, d, 2);
+            out << ")";
+        }
+        out << ")";
+    }
+    out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+}
+
+void goal::display_with_dependencies(std::ostream & out) const {
+    ptr_vector<expr> deps;
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  |-";
+        deps.reset();
+        m().linearize(dep(i), deps);
+        ptr_vector<expr>::iterator it  = deps.begin();
+        ptr_vector<expr>::iterator end = deps.end();
+        for (; it != end; ++it) {
+            expr * d = *it;
+            if (is_uninterp_const(d)) {
+                out << " " << mk_ismt2_pp(d, m());
+            }
+            else {
+                out << " #" << d->get_id();
+            }
+        }
+        out << "\n  " << mk_ismt2_pp(form(i), m(), 2);
+    }
+    out << "\n  :precision " << prec() << " :depth " << depth() << ")" << std::endl;
+}
+
+void goal::display(ast_printer_context & ctx) const {
+    display(ctx, ctx.regular_stream());
+}
+
+void goal::display_with_dependencies(ast_printer_context & ctx) const {
+    display_with_dependencies(ctx, ctx.regular_stream());
+}
+
+void goal::display(std::ostream & out) const {
+    out << "(goal";
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << "\n  ";
+        out << mk_ismt2_pp(form(i), m(), 2);
+    }
+    out << ")" << std::endl;
+}
+
+void goal::display_as_and(std::ostream & out) const {
+    ptr_buffer<expr> args;
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++)
+        args.push_back(form(i));
+    expr_ref tmp(m());
+    tmp = m().mk_and(args.size(), args.c_ptr());
+    out << mk_ismt2_pp(tmp, m()) << "\n";
+}
+
+void goal::display_ll(std::ostream & out) const {
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        out << mk_ll_pp(form(i), m()) << "\n";
+    }
+}
+
+/**
+   \brief Assumes that the formula is already in CNF.
+*/
+void goal::display_dimacs(std::ostream & out) const {
+    obj_map<expr, unsigned> expr2var;
+    unsigned num_vars = 0;
+    unsigned num_cls  = size();
+    for (unsigned i = 0; i < num_cls; i++) {
+        expr * f = form(i);
+        unsigned num_lits;
+        expr * const * lits;
+        if (m().is_or(f)) {
+            num_lits = to_app(f)->get_num_args();
+            lits     = to_app(f)->get_args();
+        }
+        else {
+            num_lits = 1;
+            lits     = &f;
+        }
+        for (unsigned j = 0; j < num_lits; j++) {
+            expr * l = lits[j];
+            if (m().is_not(l))
+                l = to_app(l)->get_arg(0);
+            if (expr2var.contains(l))
+                continue;
+            num_vars++;
+            expr2var.insert(l, num_vars);
+        }
+    }
+    out << "p cnf " << num_vars << " " << num_cls << "\n";
+    for (unsigned i = 0; i < num_cls; i++) {
+        expr * f = form(i);
+        unsigned num_lits;
+        expr * const * lits;
+        if (m().is_or(f)) {
+            num_lits = to_app(f)->get_num_args();
+            lits     = to_app(f)->get_args();
+        }
+        else {
+            num_lits = 1;
+            lits     = &f;
+        }
+        for (unsigned j = 0; j < num_lits; j++) {
+            expr * l = lits[j];
+            if (m().is_not(l)) {
+                out << "-";
+                l = to_app(l)->get_arg(0);
+            }
+            unsigned id = UINT_MAX;
+            expr2var.find(l, id);
+            SASSERT(id != UINT_MAX);
+            out << id << " ";
+        }
+        out << "0\n";
+    }
+}
+
+unsigned goal::num_exprs() const {
+    expr_fast_mark1 visited;
+    unsigned sz = size();
+    unsigned r  = 0;
+    for (unsigned i = 0; i < sz; i++) {
+        r += get_num_exprs(form(i), visited);
+    }
+    return r;
+}
+
+void goal::shrink(unsigned j) {
+    SASSERT(j <= size());
+    unsigned sz = size();
+    for (unsigned i = j; i < sz; i++)
+        m().pop_back(m_forms);
+    if (proofs_enabled()) {
+        for (unsigned i = j; i < sz; i++)
+            m().pop_back(m_proofs);
+    }
+    if (unsat_core_enabled()) {
+        for (unsigned i = j; i < sz; i++)
+            m().pop_back(m_dependencies);
+    }
+}
+
+/**
+   \brief Eliminate true formulas.
+*/
+void goal::elim_true() {
+    unsigned sz = size();
+    unsigned j = 0;
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f = form(i);
+        if (m().is_true(f))
+            continue;
+        if (i == j) {
+            j++;
+            continue;
+        }
+        m().set(m_forms, j, f);
+        if (proofs_enabled())
+            m().set(m_proofs, j, m().get(m_proofs, i));
+        if (unsat_core_enabled())
+            m().set(m_dependencies, j, m().get(m_dependencies, i));
+        j++;
+    }
+    shrink(j);
+}
+
+/**
+   \brief Return the position of formula f in the goal.
+   Return UINT_MAX if f is not in the goal
+*/
+unsigned goal::get_idx(expr * f) const {
+    unsigned sz = size();
+    for (unsigned j = 0; j < sz; j++) {
+        if (form(j) == f)
+            return j;
+    }
+    return UINT_MAX;
+}
+
+/**
+   \brief Return the position of formula (not f) in the goal.
+   Return UINT_MAX if (not f) is not in the goal
+*/
+unsigned goal::get_not_idx(expr * f) const {
+    expr * atom;
+    unsigned sz = size();
+    for (unsigned j = 0; j < sz; j++) {
+        if (m().is_not(form(j), atom) && atom == f)
+            return j;
+    }
+    return UINT_MAX;
+}
+
+void goal::elim_redundancies() {
+    if (inconsistent())
+        return;
+    expr_ref_fast_mark1 neg_lits(m());
+    expr_ref_fast_mark2 pos_lits(m());
+    unsigned sz = size();
+    unsigned j  = 0;
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f = form(i);
+        if (m().is_true(f))
+            continue;
+        if (m().is_not(f)) {
+            expr * atom = to_app(f)->get_arg(0);
+            if (neg_lits.is_marked(atom))
+                continue;
+            if (pos_lits.is_marked(atom)) {
+                proof * p = 0;
+                if (proofs_enabled()) {
+                    proof * prs[2] = { pr(get_idx(atom)), pr(i) };
+                    p = m().mk_unit_resolution(2, prs);
+                }
+                expr_dependency_ref d(m());
+                if (unsat_core_enabled())
+                    d = m().mk_join(dep(get_idx(atom)), dep(i));
+                push_back(m().mk_false(), p, d);                    
+                return;
+            }
+            neg_lits.mark(atom);
+        }
+        else {
+            if (pos_lits.is_marked(f))
+                continue;
+            if (neg_lits.is_marked(f)) {
+                proof * p = 0;
+                if (proofs_enabled()) {
+                    proof * prs[2] = { pr(get_not_idx(f)), pr(i) };
+                    p = m().mk_unit_resolution(2, prs);
+                }
+                expr_dependency_ref d(m());
+                if (unsat_core_enabled())
+                    d = m().mk_join(dep(get_not_idx(f)), dep(i));
+                push_back(m().mk_false(), p, d);
+                return;
+            }
+            pos_lits.mark(f);
+        }
+        if (i == j) {
+            j++;
+            continue;
+        }
+        m().set(m_forms, j, f);
+        if (proofs_enabled())
+            m().set(m_proofs, j, pr(i));
+        if (unsat_core_enabled())
+            m().set(m_dependencies, j, dep(i));
+        j++;
+    }
+    shrink(j);
+}
+
+bool goal::is_well_sorted() const {
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        expr * t = form(i);
+        if (!::is_well_sorted(m(), t))
+            return false;
+    }
+    return true;
+}
+
+/**
+   \brief Translate the assertion set to a new one that uses a different ast_manager.
+*/
+goal * goal::translate(ast_translation & translator) const {
+    expr_dependency_translation dep_translator(translator);
+
+    ast_manager & m_to = translator.to();
+    goal * res = alloc(goal, m_to, m_to.proofs_enabled() && proofs_enabled(), models_enabled(), unsat_core_enabled());
+    
+    unsigned sz = m().size(m_forms);
+    for (unsigned i = 0; i < sz; i++) {
+        res->m().push_back(res->m_forms, translator(m().get(m_forms, i)));        
+        if (res->proofs_enabled())
+            res->m().push_back(res->m_proofs, translator(m().get(m_proofs, i)));
+        if (res->unsat_core_enabled())
+            res->m().push_back(res->m_dependencies, dep_translator(m().get(m_dependencies, i)));
+    }
+
+    res->m_inconsistent = m_inconsistent;
+    res->m_depth        = m_depth;
+    res->m_precision    = m_precision;
+
+    return res;
+}
+
+bool is_equal(goal const & s1, goal const & s2) {
+    if (s1.size() != s2.size())
+        return false;
+    unsigned num1 = 0; // num unique ASTs in s1
+    unsigned num2 = 0; // num unique ASTs in s2
+    expr_fast_mark1 visited1;
+    expr_fast_mark2 visited2;
+    unsigned sz = s1.size();
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f1 = s1.form(i);
+        if (visited1.is_marked(f1))
+            continue;
+        num1++;
+        visited1.mark(f1);
+    }
+    SASSERT(num1 <= sz);
+    SASSERT(0 <= num1);
+    for (unsigned i = 0; i < sz; i++) {
+        expr * f2 = s2.form(i);
+        if (visited2.is_marked(f2))
+            continue;
+        num2++;
+        visited2.mark(f2);
+        if (!visited1.is_marked(f2))
+            return false;
+    }
+    SASSERT(num2 <= sz);
+    SASSERT(0 <= num2);
+    SASSERT(num1 >= num2);
+    return num1 == num2;
+}

src/tactic/goal.h

@@ -0,0 +1,252 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    goal.h
+
+Abstract:
+
+    A goal is essentially a set of formulas. Tactics are used to build 
+    proof and model finding procedures for these sets.
+    
+    Remark: In a previous version of Z3, goals were called assertion_sets.
+    Here is a summary of the main changes:
+       - Goals track whether they are the result of applying over/under approximation steps.
+         This prevent users from creating unsound strategies (e.g., user uses nia2sat, but does not check the sat_preserving flag).
+       - Goals track dependencies (aka light proofs) for unsat core extraction, and building multi-tier solvers.
+         This kind of dependency tracking is more powerful than the one used in the current Z3, since
+         it does not prevent the use of preprocessing steps such as "Gaussian Elimination".
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2011-10-12
+
+Revision History:
+
+--*/
+#ifndef _GOAL_H_
+#define _GOAL_H_
+
+#include"ast.h"
+#include"ast_translation.h"
+#include"ast_printer.h"
+#include"for_each_expr.h"
+#include"ref.h"
+#include"ref_vector.h"
+#include"ref_buffer.h"
+
+class goal {
+public:
+    enum precision {
+        PRECISE,      
+        UNDER,   // goal is the product of an under-approximation 
+        OVER,    // goal is the product of an over-approximation
+        UNDER_OVER // goal is garbage: the produce of combined under and over approximation steps.
+    };
+
+    static precision mk_union(precision p1, precision p2) { 
+        if (p1 == PRECISE) return p2;
+        if (p2 == PRECISE) return p1;
+        if (p1 != p2) return UNDER_OVER;
+        return p1;
+    }
+    
+protected:
+    ast_manager &         m_manager;
+    unsigned              m_ref_count;
+    expr_array            m_forms;
+    expr_array            m_proofs;
+    expr_dependency_array m_dependencies;
+    // attributes
+    unsigned              m_depth:26;          // depth of the goal in the goal tree.
+    unsigned              m_models_enabled:1;  // model generation is enabled.
+    unsigned              m_proofs_enabled:1;  // proof production is enabled. m_manager.proofs_enabled() must be true if m_proofs_enabled == true
+    unsigned              m_core_enabled:1;    // unsat core extraction is enabled.
+    unsigned              m_inconsistent:1;    // true if the goal is known to be inconsistent. 
+    unsigned              m_precision:2;       // PRECISE, UNDER, OVER.
+
+    void push_back(expr * f, proof * pr, expr_dependency * d);
+    void quick_process(bool save_first, expr * & f, expr_dependency * d);
+    void process_and(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
+    void process_not_or(bool save_first, app * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
+    void slow_process(bool save_first, expr * f, proof * pr, expr_dependency * d, expr_ref & out_f, proof_ref & out_pr);
+    void slow_process(expr * f, proof * pr, expr_dependency * d);
+    unsigned get_idx(expr * f) const;
+    unsigned get_not_idx(expr * f) const;
+    void shrink(unsigned j);
+    void reset_core();
+    
+public:
+    goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false):
+        m_manager(m), 
+        m_ref_count(0),
+        m_depth(0), 
+        m_models_enabled(models_enabled),
+        m_proofs_enabled(m.proofs_enabled()), 
+        m_core_enabled(core_enabled), 
+        m_inconsistent(false), 
+        m_precision(PRECISE) {
+    }
+    
+    goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled):
+        m_manager(m), 
+        m_ref_count(0),
+        m_depth(0), 
+        m_models_enabled(models_enabled),
+        m_proofs_enabled(proofs_enabled), 
+        m_core_enabled(core_enabled), 
+        m_inconsistent(false), 
+        m_precision(PRECISE) {
+        SASSERT(!proofs_enabled || m.proofs_enabled());
+    }
+
+    goal(goal const & src):
+        m_manager(src.m()),
+        m_ref_count(0),
+        m_depth(0), 
+        m_models_enabled(src.models_enabled()),
+        m_proofs_enabled(src.proofs_enabled()), 
+        m_core_enabled(src.unsat_core_enabled()), 
+        m_inconsistent(false), 
+        m_precision(PRECISE) {
+        copy_from(src);
+    }
+
+    // Copy configuration: depth, models/proofs/cores flags, and precision from src.
+    // The assertions are not copied
+    goal(goal const & src, bool):
+        m_manager(src.m()),
+        m_ref_count(0),
+        m_depth(src.m_depth), 
+        m_models_enabled(src.models_enabled()),
+        m_proofs_enabled(src.proofs_enabled()), 
+        m_core_enabled(src.unsat_core_enabled()), 
+        m_inconsistent(false), 
+        m_precision(src.m_precision) {
+    }
+    
+    ~goal() { reset_core(); }
+
+    void inc_ref() { ++m_ref_count; }
+    void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); }
+
+    ast_manager & m() const { return m_manager; }
+
+    unsigned depth() const { return m_depth; }
+    bool models_enabled() const { return m_models_enabled; }
+    bool proofs_enabled() const { return m_proofs_enabled; }
+    bool unsat_core_enabled() const { return m_core_enabled; }
+    bool inconsistent() const { return m_inconsistent; }
+    precision prec() const { return static_cast<precision>(m_precision); }
+    
+    void set_depth(unsigned d) { m_depth = d; }
+    void inc_depth() { m_depth++; }
+    void set_prec(precision d) { m_precision = d; }
+    void updt_prec(precision d) { m_precision = mk_union(prec(), d); }
+
+    void reset_all(); // reset goal and precision and depth attributes.
+    void reset(); // reset goal but preserve precision and depth attributes.
+
+    void copy_to(goal & target) const;
+    void copy_from(goal const & src) { src.copy_to(*this); }
+    
+    void assert_expr(expr * f, proof * pr, expr_dependency * d);
+    void assert_expr(expr * f) {
+        assert_expr(f, proofs_enabled() ? m().mk_asserted(f) : 0, 0);
+    }
+    
+    unsigned size() const { return m().size(m_forms); }
+
+    unsigned num_exprs() const;
+  
+    expr * form(unsigned i) const { return m().get(m_forms, i); }
+    proof * pr(unsigned i) const { return proofs_enabled() ? static_cast<proof*>(m().get(m_proofs, i)) : 0; }
+    expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m().get(m_dependencies, i) : 0; }
+
+    void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0);
+
+    void get_formulas(ptr_vector<expr> & result);
+    
+    void elim_true();
+    void elim_redundancies();
+
+    void display(ast_printer & prn, std::ostream & out) const;
+    void display(ast_printer_context & ctx) const;
+    void display(std::ostream & out) const;
+    void display_ll(std::ostream & out) const;
+    void display_as_and(std::ostream & out) const;
+    void display_dimacs(std::ostream & out) const;
+    void display_with_dependencies(ast_printer & prn, std::ostream & out) const;
+    void display_with_dependencies(ast_printer_context & ctx) const;
+    void display_with_dependencies(std::ostream & out) const;
+
+    bool sat_preserved() const { 
+        return prec() == PRECISE || prec() == UNDER; 
+    }
+
+    bool unsat_preserved() const {
+        return prec() == PRECISE || prec() == OVER;
+    }
+
+    bool is_decided_sat() const { 
+        return size() == 0 && sat_preserved();
+    }
+
+    bool is_decided_unsat() const {
+        return inconsistent() && unsat_preserved();
+    }
+
+    bool is_decided() const { 
+        return is_decided_sat() || is_decided_unsat();
+    }
+
+    bool is_well_sorted() const;
+
+    goal * translate(ast_translation & translator) const;
+};
+
+std::ostream & operator<<(std::ostream & out, goal::precision p);
+
+typedef ref<goal> goal_ref;
+typedef sref_vector<goal> goal_ref_vector;
+typedef sref_buffer<goal> goal_ref_buffer;
+
+template<typename GoalCollection>
+inline bool is_decided(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided(); }
+template<typename GoalCollection>
+inline bool is_decided_sat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_sat(); }
+template<typename GoalCollection>
+inline bool is_decided_unsat(GoalCollection const & c) { return c.size() == 1 && c[0]->is_decided_unsat(); }
+
+template<typename ForEachProc>
+void for_each_expr_at(ForEachProc& proc, goal const & s) {
+    expr_mark visited;
+    for (unsigned i = 0; i < s.size(); ++i) {
+        for_each_expr(proc, visited, s.form(i));
+    }
+}
+
+bool is_equal(goal const & g1, goal const & g2);
+
+template<typename Predicate>
+bool test(goal const & g, Predicate & proc) {
+    expr_fast_mark1 visited;
+    try {
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++)
+            quick_for_each_expr(proc, visited, g.form(i));
+    }
+    catch (typename Predicate::found) {
+        return true;
+    }
+    return false;
+}
+
+template<typename Predicate>
+bool test(goal const & g) {
+    Predicate proc(g.m());
+    return test(g, proc);
+}
+
+#endif

src/tactic/goal_shared_occs.cpp

@@ -0,0 +1,29 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    goal_shared_occs.cpp
+
+Abstract:
+
+    Functor for computing the set of shared occurrences in a goal.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-28
+
+Revision History:
+
+--*/
+#include"goal_shared_occs.h"
+
+void goal_shared_occs::operator()(goal const & g) {
+    m_occs.reset();
+    shared_occs_mark visited;
+    unsigned sz = g.size();
+    for (unsigned i = 0; i < sz; i++) {
+        expr * t = g.form(i);
+        m_occs(t, visited);
+    }
+}

src/tactic/goal_shared_occs.h

@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    goal_shared_occs.h
+
+Abstract:
+
+    Functor for computing the set of shared occurrences in a goal.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-12-28
+
+Revision History:
+
+--*/
+#ifndef _GOAL_SHARED_OCCS_H_
+#define _GOAL_SHARED_OCCS_H_
+
+#include"goal.h"
+#include"shared_occs.h"
+
+/**
+   \brief Functor for computing the set of shared occurrences in a goal.
+   
+   It is essentially a wrapper for shared_occs functor.
+*/
+class goal_shared_occs {
+    shared_occs m_occs;
+public:
+    goal_shared_occs(ast_manager & m, bool track_atomic = false, bool visit_quantifiers = true, bool visit_patterns = false):
+        m_occs(m, track_atomic, visit_quantifiers, visit_patterns) {
+    }
+    void operator()(goal const & s);
+    bool is_shared(expr * t) { return m_occs.is_shared(t); }
+    unsigned num_shared() const { return m_occs.num_shared(); }
+    void reset() { return m_occs.reset(); }
+    void cleanup() { return m_occs.cleanup(); }
+    void display(std::ostream & out, ast_manager & m) const { m_occs.display(out, m); }
+};
+
+
+#endif

src/tactic/goal_util.cpp

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    goal_util.cpp
+
+Abstract:
+
+    goal goodies.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-01-03.
+
+Revision History:
+
+--*/
+#include"goal_util.h"
+#include"goal.h"
+
+struct has_term_ite_functor {
+    struct found {};
+    ast_manager & m;
+    has_term_ite_functor(ast_manager & _m):m(_m) {}
+    void operator()(var *) {}
+    void operator()(quantifier *) {}
+    void operator()(app * n) { if (m.is_term_ite(n)) throw found(); }
+};
+
+bool has_term_ite(goal const & g) {
+    return test<has_term_ite_functor>(g);
+}

src/tactic/goal_util.h

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    goal_util.h
+
+Abstract:
+
+    goal goodies.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-01-03.
+
+Revision History:
+
+--*/
+#ifndef _GOAL_UTIL_H_
+#define _GOAL_UTIL_H_
+
+class goal;
+bool has_term_ite(goal const & g);
+
+#endif

src/tactic/model_converter.cpp

@@ -0,0 +1,150 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_converter.h
+
+Abstract:
+
+    Abstract interface for converting models.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-21
+
+Notes:
+
+--*/
+#include"model_converter.h"
+#include"model_v2_pp.h"
+
+class concat_model_converter : public concat_converter<model_converter> {
+public:
+    concat_model_converter(model_converter * mc1, model_converter * mc2):concat_converter<model_converter>(mc1, mc2) {}
+
+    virtual void operator()(model_ref & m) {
+        this->m_c2->operator()(m);
+        this->m_c1->operator()(m);
+    }
+
+    virtual void operator()(model_ref & m, unsigned goal_idx) {
+        this->m_c2->operator()(m, goal_idx);
+        this->m_c1->operator()(m, 0);
+    }
+
+    virtual char const * get_name() const { return "concat-model-converter"; }
+
+    virtual model_converter * translate(ast_translation & translator) {
+        return this->translate_core<concat_model_converter>(translator);
+    }
+};
+
+model_converter * concat(model_converter * mc1, model_converter * mc2) {
+    if (mc1 == 0)
+        return mc2;
+    if (mc2 == 0)
+        return mc1;
+    return alloc(concat_model_converter, mc1, mc2);
+}
+
+class concat_star_model_converter : public concat_star_converter<model_converter> {
+public:
+    concat_star_model_converter(model_converter * mc1, unsigned num, model_converter * const * mc2s, unsigned * szs):
+        concat_star_converter<model_converter>(mc1, num, mc2s, szs) {
+    }
+
+    virtual void operator()(model_ref & m) {
+        // TODO: delete method after conversion is complete
+        UNREACHABLE();
+    }
+
+    virtual void operator()(model_ref & m, unsigned goal_idx) {
+        unsigned num = this->m_c2s.size();
+        for (unsigned i = 0; i < num; i++) {
+            if (goal_idx < this->m_szs[i]) {
+                // found the model converter that should be used
+                model_converter * c2 = this->m_c2s[i];
+                if (c2)
+                    c2->operator()(m, goal_idx);
+                if (m_c1)
+                    this->m_c1->operator()(m, i);
+                return;
+            }
+            // invalid goal
+            goal_idx -= this->m_szs[i];
+        }
+        UNREACHABLE();
+    }
+    
+    virtual char const * get_name() const { return "concat-star-model-converter"; }
+
+    virtual model_converter * translate(ast_translation & translator) {
+        return this->translate_core<concat_star_model_converter>(translator);
+    }
+};
+
+model_converter * concat(model_converter * mc1, unsigned num, model_converter * const * mc2s, unsigned * szs) {
+    SASSERT(num > 0);
+    if (num == 1)
+        return concat(mc1, mc2s[0]);
+    unsigned i;
+    for (i = 0; i < num; i++) {
+        if (mc2s[i] != 0)
+            break;
+    }
+    if (i == num) {
+        // all mc2s are 0
+        return mc1;
+    }
+    return alloc(concat_star_model_converter, mc1, num, mc2s, szs);
+}
+
+class model2mc : public model_converter {
+    model_ref m_model;
+public:
+    model2mc(model * m):m_model(m) {}
+    virtual ~model2mc() {}
+
+    virtual void operator()(model_ref & m) {
+        m = m_model;
+    }
+
+    virtual void operator()(model_ref & m, unsigned goal_idx) {
+        m = m_model;
+    }
+
+    virtual void cancel() {
+    }
+    
+    virtual void display(std::ostream & out) {
+        out << "(model->model-converter-wrapper\n";
+        model_v2_pp(out, *m_model);
+        out << ")\n";
+    }    
+    
+    virtual model_converter * translate(ast_translation & translator) {
+        model * m = m_model->translate(translator);
+        return alloc(model2mc, m);
+    }
+};
+
+model_converter * model2model_converter(model * m) {
+    if (m == 0)
+        return 0;
+    return alloc(model2mc, m);
+}
+
+void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m) {
+    if (mc) {
+        m = alloc(model, mng);
+        (*mc)(m, 0);
+    }
+}
+
+void apply(model_converter_ref & mc, model_ref & m, unsigned gidx) {
+    if (mc) {
+        (*mc)(m, gidx);
+    }
+}
+

src/tactic/model_converter.h

@@ -0,0 +1,59 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    model_converter.h
+
+Abstract:
+
+    Abstract interface for converting models.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-21
+
+Notes:
+
+--*/
+#ifndef _MODEL_CONVERTER_H_
+#define _MODEL_CONVERTER_H_
+
+#include"model.h"
+#include"converter.h"
+#include"ref.h"
+
+class model_converter : public converter {
+public:
+    virtual void operator()(model_ref & m) {}  // TODO: delete
+
+    virtual void operator()(model_ref & m, unsigned goal_idx) {
+        // TODO: make it virtual after the transition to goal/tactic/tactical is complete
+        SASSERT(goal_idx == 0);
+        operator()(m);
+    }
+    
+    virtual model_converter * translate(ast_translation & translator) = 0;
+};
+
+typedef ref<model_converter> model_converter_ref;
+
+model_converter * concat(model_converter * mc1, model_converter * mc2);
+
+/**
+   \brief \c mc1 is the model converter for a sequence of subgoals of size \c num.
+   Given an i in [0, num), mc2s[i] is the model converter for subgoal i,
+   and num_subgoals[i] is the number of subgoals of subgoals[i].
+*/
+model_converter * concat(model_converter * mc1, unsigned num, model_converter * const * mc2s, unsigned * num_subgoals);
+
+model_converter * model2model_converter(model * m);
+
+void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m);
+
+void apply(model_converter_ref & mc, model_ref & m, unsigned gidx);
+
+typedef sref_vector<model_converter> model_converter_ref_vector;
+typedef sref_buffer<model_converter> model_converter_ref_buffer;
+
+#endif

src/tactic/num_occurs_goal.cpp

@@ -0,0 +1,27 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    num_occurs_goal.cpp
+
+Abstract:
+
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-20.
+
+Revision History:
+
+--*/
+#include"num_occurs_goal.h"
+#include"goal.h"
+
+void num_occurs_goal::operator()(goal const & g) {
+    expr_fast_mark1   visited;
+    unsigned sz = g.size();
+    for (unsigned i = 0; i < sz; i++) {
+        process(g.form(i), visited);
+    }
+}

src/tactic/num_occurs_goal.h

@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    num_occurs_goal.h
+
+Abstract:
+
+
+Author:
+
+    Leonardo de Moura (leonardo) 2012-10-20.
+
+Revision History:
+
+--*/
+#ifndef _NUM_OCCURS_GOAL_H_
+#define _NUM_OCCURS_GOAL_H_
+
+#include"num_occurs.h"
+
+class goal;
+
+class num_occurs_goal : public num_occurs { 
+public:
+    num_occurs_goal(bool ignore_ref_count1 = false, bool ignore_quantifiers = false):
+        num_occurs(ignore_ref_count1, ignore_quantifiers) {
+    }
+
+    void operator()(goal const & s);
+};
+
+
+#endif

src/tactic/probe.cpp

@@ -0,0 +1,449 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    probe.cpp
+
+Abstract:
+
+    Evaluates/Probes a goal.
+    
+    A probe is used to build tactics (aka strategies) that
+    makes decisions based on the structure of a goal.
+    
+Author:
+
+    Leonardo de Moura (leonardo) 2011-10-13.
+
+Revision History:
+
+--*/
+#include"probe.h"
+#include"arith_decl_plugin.h"
+#include"bv_decl_plugin.h"
+#include"goal_util.h"
+
+class memory_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return result(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024));
+    }
+};
+
+probe * mk_memory_probe() {
+    return alloc(memory_probe);
+}
+
+class depth_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return result(g.depth());
+    }
+};
+
+class size_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return result(g.size());
+    }
+};
+
+class num_exprs_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return result(g.num_exprs());
+    }
+};
+
+probe * mk_depth_probe() {
+    return alloc(depth_probe);
+}
+
+probe * mk_size_probe() {
+    return alloc(size_probe);
+}
+
+probe * mk_num_exprs_probe() {
+    return alloc(num_exprs_probe);
+}
+
+class unary_probe : public probe {
+protected:
+    probe * m_p;
+public:
+    unary_probe(probe * p):
+        m_p(p) {
+        SASSERT(p); 
+        p->inc_ref(); 
+    }
+    
+    ~unary_probe() { 
+        m_p->dec_ref(); 
+    }
+
+};
+
+class bin_probe : public probe {
+protected:
+    probe * m_p1;
+    probe * m_p2;
+public:
+    bin_probe(probe * p1, probe * p2):
+        m_p1(p1), 
+        m_p2(p2) { 
+        SASSERT(p1); 
+        SASSERT(p2);
+        p1->inc_ref(); 
+        p2->inc_ref(); 
+    }
+    
+    ~bin_probe() { 
+        m_p1->dec_ref(); 
+        m_p2->dec_ref(); 
+    }
+};
+
+class not_probe : public unary_probe {
+public:
+    not_probe(probe * p):unary_probe(p) {}
+    virtual result operator()(goal const & g) {
+        return result(!m_p->operator()(g).is_true());
+    }    
+};
+
+class and_probe : public bin_probe {
+public:
+    and_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).is_true() && m_p2->operator()(g).is_true());
+    }
+};
+
+class or_probe : public bin_probe {
+public:
+    or_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).is_true() || m_p2->operator()(g).is_true());
+    }
+};
+
+class eq_probe : public bin_probe {
+public:
+    eq_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() == m_p2->operator()(g).get_value());
+    }
+};
+
+class le_probe : public bin_probe {
+public:
+    le_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() <= m_p2->operator()(g).get_value());
+    }
+};
+
+class add_probe : public bin_probe {
+public:
+    add_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() + m_p2->operator()(g).get_value());
+    }
+};
+
+class sub_probe : public bin_probe {
+public:
+    sub_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() - m_p2->operator()(g).get_value());
+    }
+};
+
+class mul_probe : public bin_probe {
+public:
+    mul_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() * m_p2->operator()(g).get_value());
+    }
+};
+
+class div_probe : public bin_probe {
+public:
+    div_probe(probe * p1, probe * p2):bin_probe(p1, p2) {}
+    virtual result operator()(goal const & g) {
+        return result(m_p1->operator()(g).get_value() / m_p2->operator()(g).get_value());
+    }
+};
+
+class const_probe : public probe {
+    double m_val;
+public:
+    const_probe(double v):m_val(v) {}
+    
+    virtual result operator()(goal const & g) {
+        return result(m_val); 
+    }
+};
+
+probe * mk_const_probe(double v) {
+    return alloc(const_probe, v);
+}
+
+probe * mk_not(probe * p) {
+    return alloc(not_probe, p);
+}
+
+probe * mk_and(probe * p1, probe * p2) {
+    return alloc(and_probe, p1, p2);
+}
+
+probe * mk_or(probe * p1, probe * p2) {
+    return alloc(or_probe, p1, p2);
+}
+
+probe * mk_implies(probe * p1, probe * p2) {
+    return mk_or(mk_not(p1), p2);
+}
+
+probe * mk_eq(probe * p1, probe * p2) {
+    return alloc(eq_probe, p1, p2);
+}
+
+probe * mk_neq(probe * p1, probe * p2) {
+    return mk_not(mk_eq(p1, p2));
+}
+
+probe * mk_le(probe * p1, probe * p2) {
+    return alloc(le_probe, p1, p2);
+}
+
+probe * mk_ge(probe * p1, probe * p2) {
+    return mk_le(p2, p1);
+}
+
+probe * mk_lt(probe * p1, probe * p2) {
+    return mk_not(mk_ge(p1, p2));
+}
+
+probe * mk_gt(probe * p1, probe * p2) {
+    return mk_lt(p2, p1);
+}
+
+probe * mk_add(probe * p1, probe * p2) {
+    return alloc(add_probe, p1, p2);
+}
+
+probe * mk_mul(probe * p1, probe * p2) {
+    return alloc(mul_probe, p1, p2);
+}
+
+probe * mk_sub(probe * p1, probe * p2) {
+    return alloc(sub_probe, p1, p2);
+}
+
+probe * mk_div(probe * p1, probe * p2) {
+    return alloc(div_probe, p1, p2);
+}
+
+struct is_non_propositional_predicate {
+    struct found {};
+    ast_manager & m;
+
+    is_non_propositional_predicate(ast_manager & _m):m(_m) {}
+    void operator()(var *) { throw found();  }
+    void operator()(quantifier *) { throw found(); }
+    void operator()(app * n) {
+        if (!m.is_bool(n))
+            throw found();
+        
+        family_id fid = n->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return; 
+        
+        if (is_uninterp_const(n))
+            return;
+
+        throw found();
+    }
+};
+
+struct is_non_qfbv_predicate {
+    struct found {};
+    ast_manager & m;
+    bv_util       u;
+
+    is_non_qfbv_predicate(ast_manager & _m):m(_m), u(m) {}
+
+    void operator()(var *) { throw found();  }
+    
+    void operator()(quantifier *) { throw found(); }
+    
+    void operator()(app * n) {
+        if (!m.is_bool(n) && !u.is_bv(n))
+            throw found();
+        family_id fid = n->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return; 
+        if (fid == u.get_family_id())
+            return;
+        if (is_uninterp_const(n))
+            return;
+
+        throw found();
+    }
+};
+
+class is_propositional_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_propositional_predicate>(g);
+    }
+};
+
+class is_qfbv_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_qfbv_predicate>(g);
+    }
+};
+
+probe * mk_is_propositional_probe() {
+    return alloc(is_propositional_probe);
+}
+
+probe * mk_is_qfbv_probe() {
+    return alloc(is_qfbv_probe); 
+}
+
+class num_consts_probe : public probe {
+    bool         m_bool;   // If true, track only boolean constants. Otherwise, track only non boolean constants.
+    char const * m_family; // (Ignored if m_bool == true), if != 0 and m_bool == true, then track only constants of the given family.
+    struct proc {
+        ast_manager & m;
+        bool          m_bool;
+        family_id     m_fid;
+        unsigned      m_counter;
+        proc(ast_manager & _m, bool b, char const * family):m(_m), m_bool(b), m_counter(0) {
+            if (family != 0)
+                m_fid = m.get_family_id(family);
+            else
+                m_fid = null_family_id;
+        }
+        void operator()(quantifier *) {}
+        void operator()(var *) {}
+        void operator()(app * n) { 
+            if (n->get_num_args() == 0 && !m.is_value(n)) {
+                if (m_bool) {
+                    if (m.is_bool(n))
+                        m_counter++;
+                }
+                else {
+                    if (m_fid == null_family_id) {
+                        if (!m.is_bool(n))
+                            m_counter++;
+                    }
+                    else {
+                        if (m.get_sort(n)->get_family_id() == m_fid)
+                            m_counter++;
+                    }
+                }
+            }
+        }
+    };
+
+public:
+    num_consts_probe(bool b, char const * f):
+        m_bool(b), m_family(f) {
+    }
+    virtual result operator()(goal const & g) {
+        proc p(g.m(), m_bool, m_family);
+        unsigned sz = g.size();
+        expr_fast_mark1 visited;
+        for (unsigned i = 0; i < sz; i++) {
+            for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));        
+        }
+        return result(p.m_counter);
+    }
+};
+
+probe * mk_num_consts_probe() {
+    return alloc(num_consts_probe, false, 0);
+}
+
+probe * mk_num_bool_consts_probe() {
+    return alloc(num_consts_probe, true, 0);
+}
+
+probe * mk_num_arith_consts_probe() {
+    return alloc(num_consts_probe, false, "arith");
+}
+
+probe * mk_num_bv_consts_probe() {
+    return alloc(num_consts_probe, false, "bv");
+}
+
+class produce_proofs_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return g.proofs_enabled();
+    }
+};
+
+class produce_models_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return g.models_enabled();
+    }
+};
+
+class produce_unsat_cores_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return g.unsat_core_enabled();
+    }
+};
+
+probe * mk_produce_proofs_probe() {
+    return alloc(produce_proofs_probe);
+}
+
+probe * mk_produce_models_probe() {
+    return alloc(produce_models_probe);
+}
+
+probe * mk_produce_unsat_cores_probe() {
+    return alloc(produce_unsat_cores_probe);
+}
+
+struct has_pattern_probe : public probe {
+    struct found {};
+
+    struct proc {
+        void operator()(var * n) {}
+        void operator()(app * n) {}
+        void operator()(quantifier * n) { 
+            if (n->get_num_patterns() > 0 || n->get_num_no_patterns() > 0)
+                throw found();
+        }
+    };
+public:
+    virtual result operator()(goal const & g) {
+        try {
+            expr_fast_mark1 visited;
+            proc p;
+            unsigned sz = g.size();
+            for (unsigned i = 0; i < sz; i++) {
+                quick_for_each_expr(p, visited, g.form(i));
+            }
+            return false;
+        }
+        catch (found) {
+            return true;
+        }
+    }
+};
+
+probe * mk_has_pattern_probe() {
+    return alloc(has_pattern_probe);
+}

src/tactic/probe.h

@@ -0,0 +1,91 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    probe.h
+
+Abstract:
+
+    Evaluates/Probes a goal.
+    
+    A probe is used to build tactics (aka strategies) that
+    makes decisions based on the structure of a goal.
+
+    The current implementation is very simple.
+
+Author:
+
+    Leonardo de Moura (leonardo) 2011-10-13.
+
+Revision History:
+
+--*/
+#ifndef _PROBE_H_
+#define _PROBE_H_
+
+#include"goal.h"
+
+class probe {
+public:
+    class result {
+        double m_value;
+    public:
+        result(double v = 0.0):m_value(v) {}
+        result(unsigned v):m_value(static_cast<double>(v)) {}
+        result(int v):m_value(static_cast<double>(v)) {}
+        result(bool b):m_value(b ? 1.0 : 0.0) {}
+
+        bool is_true() const { return m_value != 0.0; }
+        double get_value() const { return m_value; }
+    };
+
+private:
+    unsigned m_ref_count;
+
+public:
+    probe():m_ref_count(0) {}
+    virtual ~probe() {}
+
+    void inc_ref() { ++m_ref_count; }
+    void dec_ref() { SASSERT(m_ref_count > 0); --m_ref_count; if (m_ref_count == 0) dealloc(this); }
+    
+    virtual result operator()(goal const & g) = 0;
+};
+
+typedef ref<probe> probe_ref;
+
+probe * mk_memory_probe();
+probe * mk_depth_probe();
+probe * mk_size_probe();
+probe * mk_num_exprs_probe();
+probe * mk_const_probe(double val);
+probe * mk_num_consts_probe();
+probe * mk_num_bool_consts_probe();
+probe * mk_num_arith_consts_probe();
+probe * mk_num_bv_consts_probe();
+probe * mk_produce_proofs_probe();
+probe * mk_produce_models_probe();
+probe * mk_produce_unsat_cores_probe();
+probe * mk_has_pattern_probe();
+
+// Some basic combinators for probes
+probe * mk_not(probe * p1);
+probe * mk_and(probe * p1, probe * p2);
+probe * mk_or(probe * p1, probe * p2);
+probe * mk_implies(probe * p1, probe * p2);
+probe * mk_eq(probe * p1, probe * p2);
+probe * mk_neq(probe * p1, probe * p2);
+probe * mk_le(probe * p1, probe * p2);
+probe * mk_lt(probe * p1, probe * p2);
+probe * mk_ge(probe * p1, probe * p2);
+probe * mk_gt(probe * p1, probe * p2);
+probe * mk_add(probe * p1, probe * p2);
+probe * mk_sub(probe * p1, probe * p2);
+probe * mk_mul(probe * p1, probe * p2);
+probe * mk_div(probe * p1, probe * p2);
+
+probe * mk_is_propositional_probe();
+probe * mk_is_qfbv_probe();
+
+#endif

src/tactic/proof_converter.cpp

@@ -0,0 +1,162 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    proof_converter.cpp
+
+Abstract:
+
+    Abstract interface for converting proofs, and basic combinators
+
+Author:
+
+    Leonardo (leonardo) 2011-11-14
+
+Notes:
+
+--*/
+#include"proof_converter.h"
+#include"ast_smt2_pp.h"
+
+class concat_proof_converter : public concat_converter<proof_converter> {
+public:
+    concat_proof_converter(proof_converter * pc1, proof_converter * pc2):concat_converter<proof_converter>(pc1, pc2) {}
+
+    virtual char const * get_name() const { return "concat-proof-converter"; }
+
+    virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
+        proof_ref tmp(m);
+        this->m_c2->operator()(m, num_source, source, tmp);
+        proof * new_source = tmp.get();
+        this->m_c1->operator()(m, 1, &new_source, result);
+    }
+
+    virtual proof_converter * translate(ast_translation & translator) {
+        return this->translate_core<concat_proof_converter>(translator);
+    }
+};
+
+proof_converter * concat(proof_converter * pc1, proof_converter * pc2) {
+    if (pc1 == 0)
+        return pc2;
+    if (pc2 == 0)
+        return pc1;
+    return alloc(concat_proof_converter, pc1, pc2);
+}
+
+class concat_star_proof_converter : public concat_star_converter<proof_converter> {
+public:
+    concat_star_proof_converter(proof_converter * pc1, unsigned num, proof_converter * const * pc2s, unsigned * szs):
+        concat_star_converter<proof_converter>(pc1, num, pc2s, szs) {
+    }
+
+    virtual char const * get_name() const { return "concat-star-proof-converter"; }
+
+    virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
+        unsigned num = this->m_szs.size();
+#ifdef Z3DEBUG
+        unsigned sum = 0;
+        for (unsigned i = 0; i < num; i++) {
+            sum += this->m_szs[i];
+        }
+        SASSERT(sum == num_source);
+#endif
+        proof_ref_buffer tmp_prs(m);
+        for (unsigned i = 0; i < num; i++) {
+            unsigned sz = m_szs[i];
+            proof_converter * c2 = m_c2s[i];
+            proof_ref pr(m);
+            if (c2) {
+                (*c2)(m, sz, source, pr);
+            }
+            else {
+                SASSERT(sz == 1);
+                pr = *source;
+            }
+            source += sz;
+            tmp_prs.push_back(pr.get());
+        }
+        if (m_c1) {
+            (*m_c1)(m, tmp_prs.size(), tmp_prs.c_ptr(), result);
+        }
+        else {
+            SASSERT(tmp_prs.size() == 1);
+            result = tmp_prs[0];
+        }
+    }
+
+    virtual proof_converter * translate(ast_translation & translator) {
+        return this->translate_core<concat_star_proof_converter>(translator);
+    }
+};
+
+proof_converter * concat(proof_converter * pc1, unsigned num, proof_converter * const * pc2s, unsigned * szs) {
+    SASSERT(num > 0);
+    if (num == 1)
+        return concat(pc1, pc2s[0]);
+    unsigned i;
+    for (i = 0; i < num; i++) {
+        if (pc2s[i] != 0)
+            break;
+    }
+    if (i == num) {
+        // all pc2s are 0
+        return pc1;
+    }
+    return alloc(concat_star_proof_converter, pc1, num, pc2s, szs);
+}
+
+class proof2pc : public proof_converter {
+    proof_ref m_pr;
+public:
+    proof2pc(ast_manager & m, proof * pr):m_pr(pr, m) {}
+    virtual ~proof2pc() {}
+
+    virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) {
+        SASSERT(num_source == 0);
+        result = m_pr;
+    }
+
+    virtual proof_converter * translate(ast_translation & translator) {
+        return alloc(proof2pc, translator.to(), translator(m_pr.get()));
+    }
+
+    virtual void display(std::ostream & out) {
+        out << "(proof->proof-converter-wrapper\n" << mk_ismt2_pp(m_pr.get(), m_pr.get_manager()) << ")\n";
+    }    
+};
+
+proof_converter * proof2proof_converter(ast_manager & m, proof * pr) {
+    if (pr == 0)
+        return 0;
+    return alloc(proof2pc, m, pr);
+}
+
+void apply(ast_manager & m, proof_converter * pc, proof_ref & pr) {
+    if (pc) {
+        proof * _pr = pr.get();
+        (*pc)(m, 1, &_pr, pr);
+    }
+}
+
+/**
+   Let pc2s be a buffer of proof converters that are wrappers for proofs.
+   That is, they are functors of the form: unit -> Proof
+   Then, this function applies pc1 to the proofs produced by pc2s's and store
+   the resultant proof in result.
+   
+   pc1 and pc2s must be different from 0.
+*/
+void apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_buffer & pc2s, proof_ref & result) {
+    SASSERT(pc1);
+    proof_ref_buffer prs(m);
+    unsigned sz = pc2s.size();
+    for (unsigned i = 0; i < sz; i++) {
+        proof_ref pr(m);
+        SASSERT(pc2s[i]); // proof production is enabled
+        pc2s[i]->operator()(m, 0, 0, pr);
+        prs.push_back(pr);
+    }
+    (*pc1)(m, sz, prs.c_ptr(), result);
+}

src/tactic/proof_converter.h

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    proof_converter.h
+
+Abstract:
+
+    Abstract interface for converting proofs, and basic combinators.
+
+Author:
+
+    Leonardo (leonardo) 2011-04-26
+
+Notes:
+
+--*/
+#ifndef _PROOF_CONVERTER_H_
+#define _PROOF_CONVERTER_H_
+
+#include"ast.h"
+#include"converter.h"
+#include"ref.h"
+
+class proof_converter : public converter {
+public:
+    virtual ~proof_converter() { }
+    virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) = 0;
+    virtual proof_converter * translate(ast_translation & translator) = 0;
+};
+
+typedef ref<proof_converter> proof_converter_ref;
+
+proof_converter * concat(proof_converter * pc1, proof_converter * pc2);
+
+/**
+   \brief \c pc1 is the proof converter for a sequence of subgoals of size \c num.
+   Given an i in [0, num), pc2s[i] is the proof converter for subgoal i,
+   and num_subgoals[i] is the number of subgoals of subgoals[i].
+*/
+proof_converter * concat(proof_converter * pc1, unsigned num, proof_converter * const * pc2s, unsigned * num_subgoals);
+
+proof_converter * proof2proof_converter(ast_manager & m, proof * pr);
+
+typedef sref_vector<proof_converter> proof_converter_ref_vector;
+typedef sref_buffer<proof_converter> proof_converter_ref_buffer;
+
+void apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_buffer & pc2s, proof_ref & result);
+void apply(ast_manager & m, proof_converter * pc, proof_ref & pr);
+
+#endif

src/tactic/tactic.cpp

@@ -0,0 +1,259 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tactic.h
+
+Abstract:
+
+    Abstract tactic object.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-13
+
+Notes:
+
+--*/
+#include<iomanip>
+#include"tactic.h"
+#include"probe.h"
+#include"stopwatch.h"
+#include"model_v2_pp.h"
+
+void tactic::cancel() {
+    #pragma omp critical (tactic_cancel)
+    {
+        set_cancel(true);
+    }
+}
+
+void tactic::reset_cancel() {
+    #pragma omp critical (tactic_cancel)
+    {
+        set_cancel(false);
+    }
+}
+
+struct tactic_report::imp {
+    char const *    m_id;
+    goal const &    m_goal;
+    stopwatch       m_watch;
+    double          m_start_memory;
+
+    imp(char const * id, goal const & g):
+        m_id(id),
+        m_goal(g),
+        m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)) {
+        m_watch.start();
+    }
+        
+    ~imp() {
+        m_watch.stop();
+        double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
+        verbose_stream() << "(" << m_id
+                         << " :num-exprs " << m_goal.num_exprs()
+                         << " :num-asts " << m_goal.m().get_num_asts()
+                         << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
+                         << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
+                         << " :after-memory " << std::fixed << std::setprecision(2) << end_memory
+                         << ")" << std::endl;
+    }
+};
+
+tactic_report::tactic_report(char const * id, goal const & g) {
+    if (get_verbosity_level() >= TACTIC_VERBOSITY_LVL)
+        m_imp = alloc(imp, id, g);
+    else
+        m_imp = 0;
+}
+
+tactic_report::~tactic_report() {
+    if (m_imp)
+        dealloc(m_imp);
+}
+
+void report_tactic_progress(char const * id, unsigned val) {
+    if (val > 0) {
+        IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(" << id << " " << val << ")" << std::endl;);
+    }
+}
+
+void skip_tactic::operator()(goal_ref const & in, 
+                             goal_ref_buffer & result, 
+                             model_converter_ref & mc, 
+                             proof_converter_ref & pc,
+                             expr_dependency_ref & core) {
+    result.reset();
+    result.push_back(in.get());
+    mc = 0;
+    pc = 0;
+    core = 0;
+}
+
+tactic * mk_skip_tactic() {
+    return alloc(skip_tactic);
+}
+
+class fail_tactic : public tactic {
+public:
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        throw tactic_exception("fail tactic");
+    }
+
+    virtual void cleanup() {}
+
+    virtual tactic * translate(ast_manager & m) { return this; }
+};
+
+tactic * mk_fail_tactic() {
+    return alloc(fail_tactic);
+}
+
+class report_verbose_tactic : public skip_tactic {
+    char const * m_msg;
+    unsigned     m_lvl;
+public:
+    report_verbose_tactic(char const * msg, unsigned lvl) : m_msg(msg), m_lvl(lvl) {}
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        IF_VERBOSE(m_lvl, verbose_stream() << m_msg << "\n";);
+        skip_tactic::operator()(in, result, mc, pc, core);
+    }
+};
+
+tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl) {
+    return alloc(report_verbose_tactic, msg, lvl);
+}
+
+class trace_tactic : public skip_tactic {
+    char const * m_tag;
+public:
+    trace_tactic(char const * tag):m_tag(tag) {}
+    
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        TRACE(m_tag, in->display(tout););
+        skip_tactic::operator()(in, result, mc, pc, core);
+    }
+};
+
+tactic * mk_trace_tactic(char const * tag) {
+    return alloc(trace_tactic, tag);
+}
+
+class fail_if_undecided_tactic : public skip_tactic {
+public:
+    fail_if_undecided_tactic() {}
+
+    virtual void operator()(goal_ref const & in, 
+                            goal_ref_buffer & result, 
+                            model_converter_ref & mc, 
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        if (!in->is_decided()) 
+            throw tactic_exception("undecided");
+        skip_tactic::operator()(in, result, mc, pc, core);
+    }
+};
+
+tactic * mk_fail_if_undecided_tactic() {
+    return alloc(fail_if_undecided_tactic);
+}
+
+void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) {
+    t.reset_statistics();
+    t.reset_cancel();
+    try {
+        t(in, result, mc, pc, core);
+        t.cleanup();
+    }
+    catch (tactic_exception & ex) {
+        IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(tactic-exception \"" << escaped(ex.msg()) << "\")" << std::endl;);
+        t.cleanup();
+        throw ex;
+    }
+}
+
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
+    bool models_enabled = g->models_enabled();
+    bool proofs_enabled = g->proofs_enabled();
+    bool cores_enabled  = g->unsat_core_enabled();
+    md   = 0;
+    pr   = 0;
+    core = 0;
+    ast_manager & m = g->m();
+    goal_ref_buffer r;
+    model_converter_ref mc;
+    proof_converter_ref pc;
+    try {
+        exec(t, g, r, mc, pc, core);
+    }
+    catch (tactic_exception & ex) {
+        reason_unknown = ex.msg();
+        return l_undef;
+    }
+    TRACE("tactic_mc", mc->display(tout););
+    TRACE("tactic_check_sat",
+          tout << "r.size(): " << r.size() << "\n";
+          for (unsigned i = 0; i < r.size(); i++) r[0]->display(tout););
+
+    if (is_decided_sat(r)) {
+        if (models_enabled) {
+            model_converter2model(m, mc.get(), md);
+            if (!md) {
+                // create empty model.
+                md = alloc(model, m);
+            }
+        }
+        return l_true;
+    }
+    else if (is_decided_unsat(r)) {
+        goal * final = r[0];
+        SASSERT(m.is_false(final->form(0)));
+        if (proofs_enabled) pr   = final->pr(0);
+        if (cores_enabled)  core = final->dep(0);
+        return l_false;
+    }
+    else {
+        if (models_enabled) model_converter2model(m, mc.get(), md);
+        reason_unknown = "incomplete";
+        return l_undef;
+    }
+}
+
+void fail_if_proof_generation(char const * tactic_name, goal_ref const & in) {
+    if (in->proofs_enabled()) {
+        std::string msg = tactic_name;
+        msg += " does not support proof production";
+        throw tactic_exception(msg.c_str());
+    }
+}
+
+void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in) {
+    if (in->unsat_core_enabled()) {
+        std::string msg = tactic_name;
+        msg += " does not support unsat core production";
+        throw tactic_exception(msg.c_str());
+    }
+}
+
+void fail_if_model_generation(char const * tactic_name, goal_ref const & in) {
+    if (in->models_enabled()) {
+        std::string msg = tactic_name;
+        msg += " does not generate models";
+        throw tactic_exception(msg.c_str());
+    }
+}

src/tactic/tactic.h

@@ -0,0 +1,157 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tactic.h
+
+Abstract:
+
+    Abstract tactic object.
+    It used to be called assertion_set_strategy.
+    The main improvement is the support for multiple subgoals.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-13
+
+Notes:
+
+--*/
+#ifndef _TACTIC_H_
+#define _TACTIC_H_
+
+#include"goal.h"
+#include"params.h"
+#include"statistics.h"
+#include"model_converter.h"
+#include"proof_converter.h"
+#include"tactic_exception.h"
+#include"lbool.h"
+
+struct front_end_params;
+class progress_callback;
+
+typedef ptr_buffer<goal> goal_buffer;
+
+class tactic {
+    unsigned m_ref_count;
+public:
+    tactic():m_ref_count(0) {}
+    virtual ~tactic() {}
+
+    void inc_ref() { m_ref_count++; }
+    void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
+
+    virtual void updt_params(params_ref const & p) {}
+    virtual void collect_param_descrs(param_descrs & r) {}
+
+    void cancel();
+    void reset_cancel();
+    virtual void set_cancel(bool f) {}
+    
+    /**
+       \brief Apply tactic to goal \c in.
+       
+       The list of resultant subgoals is stored in \c result.
+       The content of \c in may be destroyed during the operation.
+       
+       The resultant model converter \c mc can be used to convert a model for one of the returned subgoals
+       into a model for \in. If mc == 0, then model construction is disabled or any model for a subgoal
+       of \c in is also a model for \c in.
+       If \c result is decided_sat (i.e., it contains a single empty subgoal), then
+       the model converter is just wrapping the model.
+
+       The resultant proof converter \c pc can be used to convert proofs for each subgoal in \c result
+       into a proof for \c in. If pc == 0, then one of the following conditions should hold:
+         1- proof construction is disabled, 
+         2- result contains a single subgoal, and any proof of unsatisfiability for this subgoal is a proof for \c in.
+         3- result is an decided_unsat (i.e., it contains a single unsat subgoal). The actual proof can be extracted from this goal.
+         
+       The output parameter \c core is used to accumulate the unsat core of closed subgoals.
+       It must be 0 if dependency tracking is disabled, or the result is decided unsat, or 
+       no tagged assertions were used to close any subgoal.
+       
+       Note that, this signature is not compatible with the one described in the paper:
+       "The Strategy Challenge in SMT Solving".
+       The approach in the paper is conceptually simpler, but (for historical reasons) it would
+       require a lot of re-engineering in the Z3 code. In Z3, we keep a proof/justification for every formula
+       in a goal.
+       
+       Therefore, in most cases, pc == 0 and core == 0 for non-branching tactics.
+    */
+    virtual void operator()(/* in */  goal_ref const & in, 
+                            /* out */ goal_ref_buffer & result, 
+                            /* out */ model_converter_ref & mc, 
+                            /* out */ proof_converter_ref & pc,
+                            /* out */ expr_dependency_ref & core) = 0;
+
+    virtual void collect_statistics(statistics & st) const {}
+    virtual void reset_statistics() {}
+    virtual void cleanup() = 0;
+    virtual void reset() { cleanup(); }
+
+    // for backward compatibility
+    virtual void set_front_end_params(front_end_params & p) {}
+    virtual void set_logic(symbol const & l) {}
+    virtual void set_progress_callback(progress_callback * callback) {}
+
+    // translate tactic to the given manager
+    virtual tactic * translate(ast_manager & m) = 0;
+};
+
+typedef ref<tactic>         tactic_ref;
+typedef sref_vector<tactic> tactic_ref_vector;
+typedef sref_buffer<tactic> tactic_ref_buffer;
+
+// minimum verbosity level for tactics
+#define TACTIC_VERBOSITY_LVL 10
+
+class tactic_report {
+    struct imp;
+    imp *  m_imp;
+public:
+    tactic_report(char const * id, goal const & g);
+    ~tactic_report();
+};
+
+void report_tactic_progress(char const * id, unsigned val);
+
+class skip_tactic : public tactic {
+public:
+    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() {}
+    virtual tactic * translate(ast_manager & m) { return this; }
+};
+
+tactic * mk_skip_tactic();
+tactic * mk_fail_tactic();
+tactic * mk_fail_if_undecided_tactic();
+
+tactic * mk_report_verbose_tactic(char const * msg, unsigned lvl);
+tactic * mk_trace_tactic(char const * tag);
+
+class tactic_factory {
+public:
+    virtual ~tactic_factory() {}
+    virtual tactic * operator()(ast_manager & m, params_ref const & p) = 0;
+};
+
+#define MK_TACTIC_FACTORY(NAME, CODE)                                           \
+class NAME : public tactic_factory {                                            \
+public:                                                                         \
+    virtual ~NAME() {}                                                          \
+    virtual tactic * operator()(ast_manager & m, params_ref const & p) { CODE } \
+};
+
+#define MK_SIMPLE_TACTIC_FACTORY(NAME, ST)  MK_TACTIC_FACTORY(NAME, return ST;)
+
+void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
+
+// Throws an exception if goal \c in requires proof generation.
+void fail_if_proof_generation(char const * tactic_name, goal_ref const & in);
+void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in);
+void fail_if_model_generation(char const * tactic_name, goal_ref const & in);
+
+#endif

src/tactic/tactical.h

@@ -0,0 +1,83 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    tactical.h
+
+Abstract:
+
+    Basic combinators
+
+Author:
+
+    Leonardo (leonardo) 2011-10-13
+
+Notes:
+
+--*/
+#ifndef _TACTICAL_H_
+#define _TACTICAL_H_
+
+#include"tactic.h"
+#include"probe.h"
+
+tactic * and_then(unsigned num, tactic * const * ts);
+tactic * and_then(tactic * t1, tactic * t2);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9);
+tactic * and_then(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9, tactic * t10);
+
+tactic * or_else(unsigned num, tactic * const * ts);
+tactic * or_else(tactic * t1, tactic * t2);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9);
+tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5, tactic * t6, tactic * t7, tactic * t8, tactic * t9, tactic * t10);
+
+tactic * repeat(tactic * t, unsigned max = UINT_MAX); 
+/**
+   \brief Fails if \c t produeces more than \c threshold subgoals.
+   Otherwise, it behabes like \c t.
+*/
+tactic * fail_if_branching(tactic * t, unsigned threshold = 1);
+
+tactic * par(unsigned num, tactic * const * ts);
+tactic * par(tactic * t1, tactic * t2);
+tactic * par(tactic * t1, tactic * t2, tactic * t3);
+tactic * par(tactic * t1, tactic * t2, tactic * t3, tactic * t4);
+
+tactic * par_and_then(unsigned num, tactic * const * ts);
+tactic * par_and_then(tactic * t1, tactic * t2);
+
+tactic * try_for(tactic * t, unsigned msecs);
+tactic * clean(tactic * t);
+tactic * using_params(tactic * t, params_ref const & p);
+
+// Create a tactic that fails if the result returned by probe p is true.
+tactic * fail_if(probe * p);
+tactic * fail_if_not(probe * p);
+// Execute t1 if p returns true, and t2 otherwise
+tactic * cond(probe * p, tactic * t1, tactic * t2);
+// Alias for cond(p, t, mk_skip_tactic())
+tactic * when(probe * p, tactic * t);
+
+// alias for (or-else t skip)
+tactic * skip_if_failed(tactic * t);
+
+// Execute the given tactic only if proof production is not enabled.
+// If proof production is enabled it is a skip
+tactic * if_no_proofs(tactic * t);
+tactic * if_no_unsat_cores(tactic * t);
+tactic * if_no_models(tactic * t);
+
+#endif