checkpoint

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

src/tactic/nlsat_tactic/goal2nlsat.cpp

@@ -0,0 +1,309 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    goal2nlsat.cpp
+
+Abstract:
+
+    "Compile" a goal into the nonlinear arithmetic engine.
+    Non-arithmetic atoms are "abstracted" into boolean variables.
+    Non-supported terms are "abstracted" into variables.
+
+    The mappings can be used to convert back the state of the 
+    engine into a goal.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-02
+
+Notes:
+
+--*/
+#include"goal2nlsat.h"
+#include"goal.h"
+#include"goal_util.h"
+#include"nlsat_solver.h"
+#include"expr2polynomial.h"
+#include"expr2var.h"
+#include"arith_decl_plugin.h"
+#include"tactic.h"
+#include"ast_smt2_pp.h"
+
+struct goal2nlsat::imp {
+    struct nlsat_expr2polynomial : public expr2polynomial {
+        nlsat::solver & m_solver;
+        nlsat_expr2polynomial(nlsat::solver & s, ast_manager & m, polynomial::manager & pm, expr2var * e2v):
+            expr2polynomial(m, pm, e2v),
+            m_solver(s) {
+        }
+
+        virtual bool is_int(polynomial::var x) const {
+            return m_solver.is_int(x);
+        }
+
+        virtual polynomial::var mk_var(bool is_int) {
+            return m_solver.mk_var(is_int);
+        }
+    };
+    
+    ast_manager &             m;
+    nlsat::solver &           m_solver;
+    polynomial::manager &     m_pm;
+    unsynch_mpq_manager &     m_qm;
+    arith_util                m_util;
+    expr2var &                m_a2b;
+    expr2var &                m_t2x;
+    nlsat_expr2polynomial     m_expr2poly;
+    polynomial::factor_params m_fparams;
+
+    unsigned long long        m_max_memory;
+    bool                      m_factor;
+
+    volatile bool             m_cancel;
+
+    imp(ast_manager & _m, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x):
+        m(_m),
+        m_solver(s),
+        m_pm(s.pm()),
+        m_qm(s.qm()),
+        m_util(m),
+        m_a2b(a2b),
+        m_t2x(t2x),
+        m_expr2poly(m_solver, m, m_solver.pm(), &m_t2x) {
+        updt_params(p);
+        m_cancel = false;
+    }
+
+    void updt_params(params_ref const & p) {
+        m_max_memory   = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+        m_factor       = p.get_bool(":factor", true);  
+        m_fparams.updt_params(p);
+    }
+
+    void set_cancel(bool f) {
+        m_cancel = f;
+        m_pm.set_cancel(f);
+    }
+
+    nlsat::atom::kind flip(nlsat::atom::kind k) {
+        switch (k) {
+        case nlsat::atom::EQ: return k;
+        case nlsat::atom::LT: return nlsat::atom::GT;
+        case nlsat::atom::GT: return nlsat::atom::LT;
+        default:
+            UNREACHABLE();
+            return k;
+        }
+    }
+
+    nlsat::bool_var factor_atom(polynomial::polynomial * p, nlsat::atom::kind k) {
+        sbuffer<bool> is_even;
+        ptr_buffer<polynomial::polynomial> ps;
+        polynomial::factors fs(m_pm);
+        m_pm.factor(p, fs, m_fparams);
+        TRACE("goal2nlsat_bug", tout << "factors:\n" << fs << "\n";); 
+        SASSERT(fs.distinct_factors() > 0);
+        for (unsigned i = 0; i < fs.distinct_factors(); i++) {
+            ps.push_back(fs[i]);
+            is_even.push_back(fs.get_degree(i) % 2 == 0);
+        }
+        if (m_qm.is_neg(fs.get_constant()))
+            k = flip(k);
+        return m_solver.mk_ineq_atom(k, ps.size(), ps.c_ptr(), is_even.c_ptr());
+    }
+
+    nlsat::literal process_atom(app * f, nlsat::atom::kind k) {
+        SASSERT(f->get_num_args() == 2);
+        expr * lhs = f->get_arg(0);
+        expr * rhs = f->get_arg(1);
+        polynomial_ref p1(m_pm);
+        polynomial_ref p2(m_pm);
+        scoped_mpz d1(m_qm);
+        scoped_mpz d2(m_qm);
+        m_expr2poly.to_polynomial(lhs, p1, d1);
+        m_expr2poly.to_polynomial(rhs, p2, d2);
+        scoped_mpz lcm(m_qm);
+        m_qm.lcm(d1, d2, lcm);
+        m_qm.div(lcm, d1, d1);
+        m_qm.div(lcm, d2, d2);
+        m_qm.neg(d2);
+        polynomial_ref p(m_pm);
+        p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2);
+        TRACE("goal2nlsat_bug", tout << "p: " << p << "\nk: " << k << "\n";);
+        if (is_const(p)) {
+            int sign;
+            if (is_zero(p))
+                sign = 0;
+            else
+                sign = m_qm.is_pos(m_pm.coeff(p, 0)) ? 1 : -1;
+            switch (k) {
+            case nlsat::atom::EQ: return sign == 0 ? nlsat::true_literal : nlsat::false_literal;
+            case nlsat::atom::LT: return sign <  0 ? nlsat::true_literal : nlsat::false_literal;
+            case nlsat::atom::GT: return sign >  0 ? nlsat::true_literal : nlsat::false_literal;
+            default:
+                UNREACHABLE();
+                return nlsat::true_literal;
+            }
+        }
+        if (m_factor) {
+            return nlsat::literal(factor_atom(p, k), false);
+        }
+        else {
+            bool is_even = false;
+            polynomial::polynomial * _p = p.get();
+            return nlsat::literal(m_solver.mk_ineq_atom(k, 1, &_p, &is_even), false);
+        }
+    }
+
+    nlsat::literal process_eq(app * f) {
+        return process_atom(f, nlsat::atom::EQ);
+    }
+
+    nlsat::literal process_le(app * f) {
+        return ~process_atom(f, nlsat::atom::GT);
+    }
+
+    nlsat::literal process_ge(app * f) {
+        return ~process_atom(f, nlsat::atom::LT);
+    }
+
+    // everything else is compiled as a boolean variable
+    nlsat::bool_var process_bvar(expr * f) {
+        if (m_a2b.is_var(f)) {
+            return static_cast<nlsat::bool_var>(m_a2b.to_var(f));
+        }
+        else {
+            nlsat::bool_var b = m_solver.mk_bool_var();
+            m_a2b.insert(f, b);
+            return b;
+        }
+    }
+
+    nlsat::literal process_atom(expr * f) {
+        if (m.is_eq(f)) {
+            if (m_util.is_int_real(to_app(f)->get_arg(0)))
+                return process_eq(to_app(f));
+            else
+                return nlsat::literal(process_bvar(f), false);                
+        }
+        else if (m_util.is_le(f)) {
+            return process_le(to_app(f));
+        }
+        else if (m_util.is_ge(f)) {
+            return process_ge(to_app(f));
+        }
+        else if (is_app(f)) {
+            if (to_app(f)->get_family_id() == m.get_basic_family_id()) {
+                switch (to_app(f)->get_decl_kind()) {
+                case OP_TRUE:
+                case OP_FALSE:
+                    TRACE("goal2nlsat", tout << "f: " << mk_ismt2_pp(f, m) << "\n";);
+                    throw tactic_exception("apply simplify before applying nlsat");
+                case OP_AND:
+                case OP_OR:
+                case OP_IFF:
+                case OP_XOR:
+                case OP_NOT:
+                case OP_IMPLIES:
+                    throw tactic_exception("convert goal into cnf before applying nlsat");
+                case OP_DISTINCT:
+                    throw tactic_exception("eliminate distinct operator (use tactic '(using-params simplify :blast-distinct true)') before applying nlsat");
+                default:
+                    UNREACHABLE();
+                    return nlsat::literal(nlsat::null_bool_var, false);
+                }
+            }
+            else if (to_app(f)->get_family_id() == m_util.get_family_id()) {
+                throw tactic_exception("apply purify-arith before applying nlsat");
+            }
+            else {
+                return nlsat::literal(process_bvar(f), false);
+            }
+        }
+        else {
+            SASSERT(is_quantifier(f));
+            return nlsat::literal(process_bvar(f), false);
+        }
+    }
+    
+    nlsat::literal process_literal(expr * f) {
+        bool neg = false;
+        while (m.is_not(f, f))
+            neg = !neg;
+        nlsat::literal l = process_atom(f);
+        if (neg)
+            l.neg();
+        return l;
+    }
+
+    void process(expr * f, expr_dependency * dep) {
+        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;
+        }
+        sbuffer<nlsat::literal> ls;
+        for (unsigned i = 0; i < num_lits; i++) {
+            ls.push_back(process_literal(lits[i]));
+        }
+        m_solver.mk_clause(ls.size(), ls.c_ptr(), dep);
+    }
+
+    void operator()(goal const & g) {
+        if (has_term_ite(g))
+            throw tactic_exception("eliminate term-ite before applying nlsat");
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++) {
+            process(g.form(i), g.dep(i));
+        }
+    }
+};
+
+struct goal2nlsat::scoped_set_imp {
+    goal2nlsat & m_owner; 
+    scoped_set_imp(goal2nlsat & o, imp & i):m_owner(o) {
+        #pragma omp critical (tactic_cancel)
+        {
+            m_owner.m_imp = &i;
+        }
+    }
+    
+    ~scoped_set_imp() {
+        #pragma omp critical (tactic_cancel)
+        {
+            m_owner.m_imp = 0;
+        }
+    }
+};
+
+goal2nlsat::goal2nlsat() {
+    m_imp = 0;
+}
+
+goal2nlsat::~goal2nlsat() {
+    SASSERT(m_imp == 0);
+}
+    
+void goal2nlsat::collect_param_descrs(param_descrs & r) {
+    insert_max_memory(r);
+    r.insert(":factor", CPK_BOOL, "(default: true) factor polynomials.");
+    polynomial::factor_params::get_param_descrs(r);
+}
+    
+void goal2nlsat::operator()(goal const & g, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x) {
+    imp local_imp(g.m(), p, s, a2b, t2x);
+    scoped_set_imp setter(*this, local_imp);
+    local_imp(g);
+}
+    
+void goal2nlsat::set_cancel(bool f) {
+    if (m_imp)
+        m_imp->set_cancel(f);
+}

src/tactic/nlsat_tactic/goal2nlsat.h

@@ -0,0 +1,75 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    goal2nlsat.h
+
+Abstract:
+
+    "Compile" a goal into the nonlinear arithmetic engine.
+    Non-arithmetic atoms are "abstracted" into boolean variables.
+    Non-supported terms are "abstracted" into variables.
+
+    The mappings can be used to convert back the state of the 
+    engine into a goal.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-02
+
+Notes:
+
+--*/
+#ifndef _GOAL2NLSAT_H_
+#define _GOAL2NLSAT_H_
+
+#include"nlsat_types.h"
+#include"model_converter.h"
+
+class goal;
+class expr2var;
+
+class goal2nlsat {
+    struct imp;
+    imp *  m_imp;
+    struct scoped_set_imp;
+public:
+    goal2nlsat();
+    ~goal2nlsat();
+    
+    static void collect_param_descrs(param_descrs & r);
+    
+    /**
+       \brief "Compile" the goal into the given nlsat engine.
+       Store a mapping from atoms to boolean variables into a2b.
+       Store a mapping from terms into arithmetic variables into t2x.
+       
+       \remark a2b and t2x m don't need to be empty. The definitions there are reused.
+
+       The input is expected to be in CNF
+    */
+    void operator()(goal const & g, params_ref const & p, nlsat::solver & s, expr2var & a2b, expr2var & t2x);
+    
+    void set_cancel(bool f);
+};
+
+class nlsat2goal {
+    struct imp;
+    imp *  m_imp;
+public:
+    nlsat2goal();
+    ~nlsat2goal();
+
+    static void collect_param_descrs(param_descrs & r);
+
+    /**
+       \brief Translate the state of the nlsat engine back into a goal.
+    */
+    void operator()(nlsat::solver const & s, expr2var const & a2b, expr2var const & t2x,
+                    params_ref const & p, goal & g, model_converter_ref & mc);
+    
+    void set_cancel(bool f);
+};
+
+#endif

src/tactic/nlsat_tactic/nlsat_tactic.cpp

@@ -0,0 +1,258 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    nlsat_tactic.cpp
+
+Abstract:
+
+    Tactic for using nonlinear procedure.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-02
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"goal2nlsat.h"
+#include"nlsat_solver.h"
+#include"model.h"
+#include"expr2var.h"
+#include"arith_decl_plugin.h"
+#include"ast_smt2_pp.h"
+#include"z3_exception.h"
+#include"algebraic_numbers.h"
+
+class nlsat_tactic : public tactic {
+    struct expr_display_var_proc : public nlsat::display_var_proc {
+        ast_manager & m;
+        expr_ref_vector m_var2expr;
+        expr_display_var_proc(ast_manager & _m):m(_m), m_var2expr(_m) {}
+        virtual void operator()(std::ostream & out, nlsat::var x) const { 
+            if (x < m_var2expr.size())
+                out << mk_ismt2_pp(m_var2expr.get(x), m); 
+            else
+                out << "x!" << x;
+        }
+    };
+
+    struct     imp {
+        ast_manager &         m;
+        params_ref            m_params;
+        expr_display_var_proc m_display_var;
+        nlsat::solver         m_solver;
+        goal2nlsat            m_g2nl;
+
+        imp(ast_manager & _m, params_ref const & p):
+            m(_m),
+            m_params(p),
+            m_display_var(_m),
+            m_solver(p) {
+        }
+        
+        void updt_params(params_ref const & p) {
+            m_params = p;
+            m_solver.updt_params(p);
+        }
+
+        void set_cancel(bool f) {
+            m_solver.set_cancel(f);
+            m_g2nl.set_cancel(f);
+        }
+        
+        bool contains_unsupported(expr_ref_vector & b2a, expr_ref_vector & x2t) {
+            for (unsigned x = 0; x < x2t.size(); x++) {
+                if (!is_uninterp_const(x2t.get(x))) {
+                    TRACE("unsupported", tout << "unsupported atom:\n" << mk_ismt2_pp(x2t.get(x), m) << "\n";);
+                    return true;
+                }
+            }
+            for (unsigned b = 0; b < b2a.size(); b++) {
+                expr * a = b2a.get(b);
+                if (a == 0)
+                    continue;
+                if (is_uninterp_const(a))
+                    continue;
+                if (m_solver.is_interpreted(b))
+                    continue; // arithmetic atom
+                TRACE("unsupported", tout << "unsupported atom:\n" << mk_ismt2_pp(a, m) << "\n";);
+                return true; // unsupported
+            }
+            return false;
+        }
+        
+        // Return false if nlsat assigned noninteger value to an integer variable.
+        bool mk_model(expr_ref_vector & b2a, expr_ref_vector & x2t, model_converter_ref & mc) {
+            bool ok = true;
+            model_ref md = alloc(model, m);
+            arith_util util(m);
+            for (unsigned x = 0; x < x2t.size(); x++) {
+                expr * t = x2t.get(x);
+                if (!is_uninterp_const(t))
+                    continue;
+                expr * v;
+                try {
+                    v = util.mk_numeral(m_solver.value(x), util.is_int(t));
+                }
+                catch (z3_error & ex) {
+                    throw ex;
+                }
+                catch (z3_exception &) {
+                    v = util.mk_to_int(util.mk_numeral(m_solver.value(x), false));
+                    ok = false;
+                }
+                md->register_decl(to_app(t)->get_decl(), v);
+            }
+            for (unsigned b = 0; b < b2a.size(); b++) {
+                expr * a = b2a.get(b);
+                if (a == 0 || !is_uninterp_const(a))
+                    continue;
+                lbool val = m_solver.bvalue(b);
+                if (val == l_undef)
+                    continue; // don't care
+                md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false());
+            }
+            mc = model2model_converter(md.get());
+            return ok;
+        }
+
+        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("nlsat", *g);
+            
+            if (g->is_decided()) {
+                result.push_back(g.get());
+                return;
+            }
+
+            fail_if_proof_generation("nlsat", g);
+
+            expr2var  a2b(m);
+            expr2var  t2x(m);
+            m_g2nl(*g, m_params, m_solver, a2b, t2x);
+
+            m_display_var.m_var2expr.reset();
+            t2x.mk_inv(m_display_var.m_var2expr);
+            m_solver.set_display_var(m_display_var);
+            
+            lbool st = m_solver.check();
+            
+            if (st == l_undef) {
+            }
+            else if (st == l_true) {
+                expr_ref_vector x2t(m);
+                expr_ref_vector b2a(m);
+                a2b.mk_inv(b2a);
+                t2x.mk_inv(x2t);
+                if (!contains_unsupported(b2a, x2t)) {
+                    // If mk_model is false it means that the model produced by nlsat 
+                    // assigns noninteger values to integer variables
+                    if (mk_model(b2a, x2t, mc)) {
+                        // result goal is trivially SAT
+                        g->reset(); 
+                    }
+                }
+            }
+            else {
+                // TODO: extract unsat core
+                g->assert_expr(m.mk_false(), 0, 0);
+            }
+            g->inc_depth();
+            result.push_back(g.get());
+            TRACE("nlsat", g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+    };
+    
+    imp *      m_imp;
+    params_ref m_params;
+    statistics m_stats;
+    
+    struct scoped_set_imp {
+        nlsat_tactic & m_owner; 
+        scoped_set_imp(nlsat_tactic & o, imp & i):m_owner(o) {
+            #pragma omp critical (tactic_cancel)
+            {
+                m_owner.m_imp = &i;
+            }
+        }
+
+        ~scoped_set_imp() {
+            m_owner.m_imp->m_solver.collect_statistics(m_owner.m_stats);
+            #pragma omp critical (tactic_cancel)
+            {
+                m_owner.m_imp = 0;
+            }
+        }
+    };
+
+public:
+    nlsat_tactic(params_ref const & p):
+        m_params(p) {
+        m_imp = 0;
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(nlsat_tactic, m_params);
+    }
+        
+    virtual ~nlsat_tactic() {
+        SASSERT(m_imp == 0);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        goal2nlsat::collect_param_descrs(r);
+        nlsat::solver::collect_param_descrs(r);
+        algebraic_numbers::manager::collect_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) {
+        try {
+            imp local_imp(in->m(), m_params);
+            scoped_set_imp setter(*this, local_imp);
+            local_imp(in, result, mc, pc, core);
+        }
+        catch (z3_error & ex) {
+            throw ex;
+        }
+        catch (z3_exception & ex) {
+            throw tactic_exception(ex.msg());
+        }
+    }
+    
+    virtual void cleanup() {}
+    
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+
+    virtual void collect_statistics(statistics & st) const {
+        st.copy(m_stats);
+    }
+
+    virtual void reset_statistics() {
+        m_stats.reset();
+    }
+};
+
+tactic * mk_nlsat_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(nlsat_tactic, p));
+}
+

src/tactic/nlsat_tactic/nlsat_tactic.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    nlsat_tactic.h
+
+Abstract:
+
+    Tactic for using nonlinear procedure.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-02
+
+Notes:
+
+--*/
+#ifndef _NLSAT_TACTIC_H_
+#define _NLSAT_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_nlsat_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif

src/tactic/nlsat_tactic/qfnra_nlsat_tactic.cpp

@@ -0,0 +1,63 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    qfnra_nlsat_tactic.h
+
+Abstract:
+
+    Tactic based on nlsat for solving QF_NRA problems
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#include"tactical.h"
+
+#include"tseitin_cnf_tactic.h"
+#include"degree_shift_tactic.h"
+#include"purify_arith_tactic.h"
+#include"nlsat_tactic.h"
+#include"factor_tactic.h"
+#include"simplify_tactic.h"
+#include"elim_uncnstr_tactic.h"
+#include"propagate_values_tactic.h"
+#include"solve_eqs_tactic.h"
+#include"elim_term_ite_tactic.h"
+
+tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
+    params_ref main_p = p;
+    main_p.set_bool(":elim-and", true);
+    main_p.set_bool(":blast-distinct", true);
+    params_ref purify_p = p;
+    purify_p.set_bool(":complete", false); // temporary hack, solver does not support uninterpreted functions for encoding (div0 x) applications. So, we replace it application of this kind with an uninterpreted function symbol.
+
+    tactic * factor;
+    if (p.get_bool(":factor", true))
+        factor = mk_factor_tactic(m, p);
+    else
+        factor = mk_skip_tactic();
+
+    return and_then(and_then(using_params(mk_simplify_tactic(m, p),
+                                          main_p),
+                             using_params(mk_purify_arith_tactic(m, p),
+                                          purify_p),
+                             mk_propagate_values_tactic(m, p),
+                             mk_solve_eqs_tactic(m, p),
+                             mk_elim_uncnstr_tactic(m, p),
+                             mk_elim_term_ite_tactic(m, p)),
+                    and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
+                             factor,
+                             mk_solve_eqs_tactic(m, p),
+                             using_params(mk_simplify_tactic(m, p),
+                                          main_p),
+                             mk_tseitin_cnf_core_tactic(m, p),
+                             using_params(mk_simplify_tactic(m, p),
+                                          main_p),
+                             mk_nlsat_tactic(m, p)));
+}
+

src/tactic/nlsat_tactic/qfnra_nlsat_tactic.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    qfnra_nlsat_tactic.h
+
+Abstract:
+
+    Tactic based on nlsat for solving QF_NRA problems
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#ifndef _QFNRA_NLSAT_TACTIC_H_
+#define _QFNRA_NLSAT_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+MK_SIMPLE_TACTIC_FACTORY(qfnra_nlsat_fct, mk_qfnra_nlsat_tactic(m, p));
+
+#endif

src/tactic/sat_tactic/atom2bool_var.cpp

@@ -0,0 +1,116 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    atom2bool_var.cpp
+
+Abstract:
+
+    The mapping between SAT boolean variables and atoms
+
+Author:
+
+    Leonardo (leonardo) 2011-10-25
+
+Notes:
+
+--*/
+#include"atom2bool_var.h"
+#include"ast_smt2_pp.h"
+#include"ref_util.h"
+#include"goal.h"
+
+void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const {
+    obj_map<expr, var>::iterator it  = m_mapping.begin();
+    obj_map<expr, var>::iterator end = m_mapping.end();
+    for (; it != end; ++it) {
+        sat::literal l(static_cast<sat::bool_var>(it->m_value), false);
+        lit2expr.set(l.index(), it->m_key);
+        l.neg();
+        lit2expr.set(l.index(), m().mk_not(it->m_key));
+    }
+}
+
+sat::bool_var atom2bool_var::to_bool_var(expr * n) const {
+    sat::bool_var v = sat::null_bool_var;
+    m_mapping.find(n, v);
+    return v;
+}
+
+struct collect_boolean_interface_proc {
+    struct visitor {
+        obj_hashtable<expr> & m_r;
+        visitor(obj_hashtable<expr> & r):m_r(r) {}
+        void operator()(var * n)  {}
+        void operator()(app * n)  { if (is_uninterp_const(n)) m_r.insert(n); }       
+        void operator()(quantifier * n) {} 
+    };
+
+    ast_manager &    m;
+    expr_fast_mark2  fvisited;
+    expr_fast_mark1  tvisited;
+    ptr_vector<expr> todo;
+    visitor          proc;
+
+    collect_boolean_interface_proc(ast_manager & _m, obj_hashtable<expr> & r):
+        m(_m),
+        proc(r) {
+    }
+
+    void process(expr * f) {
+        if (fvisited.is_marked(f))
+            return;
+        fvisited.mark(f);
+        todo.push_back(f);
+        while (!todo.empty()) {
+            expr * t = todo.back();
+            todo.pop_back();
+            if (is_uninterp_const(t))
+                continue;
+            if (is_app(t) && to_app(t)->get_family_id() == m.get_basic_family_id() && to_app(t)->get_num_args() > 0) {
+                decl_kind k = to_app(t)->get_decl_kind();
+                if (k == OP_OR || k == OP_NOT || k == OP_IFF || ((k == OP_EQ || k == OP_ITE) && m.is_bool(to_app(t)->get_arg(1)))) {
+                    unsigned num = to_app(t)->get_num_args();
+                    for (unsigned i = 0; i < num; i++) {
+                        expr * arg = to_app(t)->get_arg(i);
+                        if (fvisited.is_marked(arg))
+                            continue;
+                        fvisited.mark(arg);
+                        todo.push_back(arg);
+                    }
+                }
+            }
+            else {
+                quick_for_each_expr(proc, tvisited, t);
+            }
+        }
+    }
+    
+    template<typename T>
+    void operator()(T const & g) {
+        unsigned sz = g.size();
+        for (unsigned i = 0; i < sz; i++)
+            process(g.form(i));
+    }
+    
+    void operator()(unsigned sz, expr * const * fs) {
+        for (unsigned i = 0; i < sz; i++)
+            process(fs[i]);
+    }
+};
+
+template<typename T>
+void collect_boolean_interface_core(T const & s, obj_hashtable<expr> & r) {
+    collect_boolean_interface_proc proc(s.m(), r);
+    proc(s);
+}
+
+void collect_boolean_interface(goal const & g, obj_hashtable<expr> & r) {
+    collect_boolean_interface_core(g, r);
+}
+
+void collect_boolean_interface(ast_manager & m, unsigned num, expr * const * fs, obj_hashtable<expr> & r) {
+    collect_boolean_interface_proc proc(m, r);
+    proc(num, fs);
+}

src/tactic/sat_tactic/atom2bool_var.h

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    atom2bool_var.h
+
+Abstract:
+
+    The mapping between SAT boolean variables and atoms
+
+Author:
+
+    Leonardo (leonardo) 2011-10-25
+
+Notes:
+
+--*/
+#ifndef _ATOM2BOOL_VAR_H_
+#define _ATOM2BOOL_VAR_H_
+
+#include"expr2var.h"
+#include"sat_types.h"
+
+/**
+   \brief Mapping from atoms into SAT boolean variables.
+*/
+class atom2bool_var : public expr2var {
+public:
+    atom2bool_var(ast_manager & m):expr2var(m) {}
+    void insert(expr * n, sat::bool_var v) { expr2var::insert(n, v); }
+    sat::bool_var to_bool_var(expr * n) const;
+    void mk_inv(expr_ref_vector & lit2expr) const;
+    // return true if the mapping contains uninterpreted atoms.
+    bool interpreted_atoms() const { return expr2var::interpreted_vars(); }
+};
+
+class goal;
+
+void collect_boolean_interface(goal const & g, obj_hashtable<expr> & r);
+void collect_boolean_interface(ast_manager & m, unsigned num, expr * const * fs, obj_hashtable<expr> & r);
+
+#endif

src/tactic/sat_tactic/goal2sat.cpp

@@ -0,0 +1,711 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    goal2sat.cpp
+
+Abstract:
+
+    "Compile" a goal into the SAT engine.
+    Atoms are "abstracted" into boolean variables.
+    The mapping between boolean variables and atoms
+    can be used to convert back the state of the 
+    SAT engine into a goal.
+
+    The idea is to support scenarios such as:
+    1) simplify, blast, convert into SAT, and solve
+    2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal.
+    3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal.
+    4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-26
+
+Notes:
+
+--*/
+#include"goal2sat.h"
+#include"ast_smt2_pp.h"
+#include"ref_util.h"
+#include"cooperate.h"
+#include"filter_model_converter.h"
+#include"model_evaluator.h"
+#include"for_each_expr.h"
+#include"model_v2_pp.h"
+#include"tactic.h"
+
+struct goal2sat::imp {
+    struct frame {
+        app *    m_t;
+        unsigned m_root:1;
+        unsigned m_sign:1;
+        unsigned m_idx;
+        frame(app * t, bool r, bool s, unsigned idx):
+            m_t(t), m_root(r), m_sign(s), m_idx(idx) {}
+    };
+    ast_manager &               m;
+    svector<frame>              m_frame_stack;
+    svector<sat::literal>       m_result_stack;
+    obj_map<app, sat::literal>  m_cache;
+    obj_hashtable<expr>         m_interface_vars;
+    sat::solver &               m_solver;
+    atom2bool_var &             m_map;
+    sat::bool_var               m_true;
+    bool                        m_ite_extra;
+    unsigned long long          m_max_memory;
+    volatile bool               m_cancel;
+    
+    imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map):
+        m(_m),
+        m_solver(s),
+        m_map(map) {
+        updt_params(p);
+        m_cancel = false;
+        m_true = sat::null_bool_var;
+    }
+        
+    void updt_params(params_ref const & p) {
+        m_ite_extra       = p.get_bool(":ite-extra", true);
+        m_max_memory      = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+    }
+
+    void throw_op_not_handled() {
+        throw tactic_exception("operator not supported, apply simplifier before invoking translator");
+    }
+    
+    void mk_clause(sat::literal l) {
+        TRACE("goal2sat", tout << "mk_clause: " << l << "\n";);
+        m_solver.mk_clause(1, &l);
+    }
+
+    void mk_clause(sat::literal l1, sat::literal l2) {
+        TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";);
+        m_solver.mk_clause(l1, l2);
+    }
+
+    void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
+        TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
+        m_solver.mk_clause(l1, l2, l3);
+    }
+
+    void mk_clause(unsigned num, sat::literal * lits) {
+        TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";);
+        m_solver.mk_clause(num, lits);
+    }
+
+    sat::bool_var mk_true() {
+        // create fake variable to represent true;
+        if (m_true == sat::null_bool_var) {
+            m_true = m_solver.mk_var();
+            mk_clause(sat::literal(m_true, false)); // v is true
+        }
+        return m_true;
+    }
+    
+    void convert_atom(expr * t, bool root, bool sign) {
+        SASSERT(m.is_bool(t));
+        sat::literal  l;
+        sat::bool_var v = m_map.to_bool_var(t);
+        if (v == sat::null_bool_var) {
+            if (m.is_true(t)) {
+                l = sat::literal(mk_true(), sign);
+            }
+            else if (m.is_false(t)) {
+                l = sat::literal(mk_true(), !sign);
+            }
+            else {
+                bool ext = !is_uninterp_const(t) || m_interface_vars.contains(t);
+                sat::bool_var v = m_solver.mk_var(ext);
+                m_map.insert(t, v);
+                l = sat::literal(v, sign);
+                TRACE("goal2sat", tout << "new_var: " << v << "\n" << mk_ismt2_pp(t, m) << "\n";);
+            }
+        }
+        else {
+            SASSERT(v != sat::null_bool_var);
+            l = sat::literal(v, sign);
+        }
+        SASSERT(l != sat::null_literal);
+        if (root)
+            mk_clause(l);
+        else
+            m_result_stack.push_back(l);
+    }
+
+    bool process_cached(app * t, bool root, bool sign) {
+        sat::literal l;
+        if (m_cache.find(t, l)) {
+            if (sign)
+                l.neg();
+            if (root)
+                mk_clause(l);
+            else
+                m_result_stack.push_back(l);
+            return true;
+        }
+        return false;
+    }
+
+    bool visit(expr * t, bool root, bool sign) {
+        if (!is_app(t)) {
+            convert_atom(t, root, sign);
+            return true;
+        }
+        if (process_cached(to_app(t), root, sign))
+            return true;
+        if (to_app(t)->get_family_id() != m.get_basic_family_id()) {
+            convert_atom(t, root, sign);
+            return true;
+        }
+        switch (to_app(t)->get_decl_kind()) {
+        case OP_NOT:
+        case OP_OR:
+        case OP_IFF:
+            m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
+            return false;
+        case OP_ITE:
+        case OP_EQ:
+            if (m.is_bool(to_app(t)->get_arg(1))) {
+                m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
+                return false;
+            }
+            convert_atom(t, root, sign);
+            return true;
+        case OP_AND:
+        case OP_XOR:
+        case OP_IMPLIES:
+        case OP_DISTINCT:
+            TRACE("goal2sat_not_handled", tout << mk_ismt2_pp(t, m) << "\n";);
+            throw_op_not_handled();
+        default:
+            convert_atom(t, root, sign);
+            return true;
+        }
+    }
+
+    void convert_or(app * t, bool root, bool sign) {
+        TRACE("goal2sat", tout << "convert_or:\n" << mk_ismt2_pp(t, m) << "\n";);
+        unsigned num = t->get_num_args();
+        if (root) {
+            SASSERT(num == m_result_stack.size());
+            if (sign) {
+                // this case should not really happen.
+                for (unsigned i = 0; i < num; i++) {
+                    sat::literal l = m_result_stack[i];
+                    l.neg();
+                    mk_clause(l);
+                }
+            }
+            else {
+                mk_clause(m_result_stack.size(), m_result_stack.c_ptr());
+                m_result_stack.reset();
+            }
+        }
+        else {
+            SASSERT(num <= m_result_stack.size());
+            sat::bool_var k = m_solver.mk_var();
+            sat::literal  l(k, false);
+            m_cache.insert(t, l);
+            sat::literal * lits = m_result_stack.end() - num;
+            for (unsigned i = 0; i < num; i++) {
+                mk_clause(~lits[i], l);
+            }
+            m_result_stack.push_back(~l);
+            lits = m_result_stack.end() - num - 1;
+            // remark: mk_clause may perform destructive updated to lits.
+            // I have to execute it after the binary mk_clause above.
+            mk_clause(num+1, lits);
+            unsigned old_sz = m_result_stack.size() - num - 1;
+            m_result_stack.shrink(old_sz);
+            if (sign)
+                l.neg();
+            m_result_stack.push_back(l);
+        }
+    }
+
+    void convert_ite(app * n, bool root, bool sign) {
+        unsigned sz = m_result_stack.size();
+        SASSERT(sz >= 3);
+        sat::literal  c = m_result_stack[sz-3];
+        sat::literal  t = m_result_stack[sz-2];
+        sat::literal  e = m_result_stack[sz-1];
+        if (root) {
+            SASSERT(sz == 3);
+            if (sign) {
+                mk_clause(~c, ~t);
+                mk_clause(c,  ~e);
+            }
+            else {
+                mk_clause(~c, t);
+                mk_clause(c, e);
+            }
+            m_result_stack.reset();
+        }
+        else {
+            sat::bool_var k = m_solver.mk_var();
+            sat::literal  l(k, false);
+            m_cache.insert(n, l);
+            mk_clause(~l, ~c, t);
+            mk_clause(~l,  c, e);
+            mk_clause(l,  ~c, ~t);
+            mk_clause(l,   c, ~e);
+            if (m_ite_extra) {
+                mk_clause(~t, ~e, l);
+                mk_clause(t,  e, ~l);
+            }
+            m_result_stack.shrink(sz-3);
+            if (sign)
+                l.neg();
+            m_result_stack.push_back(l);
+        }
+    }
+
+    void convert_iff(app * t, bool root, bool sign) {
+        TRACE("goal2sat", tout << "convert_iff " << root << " " << sign << "\n" << mk_ismt2_pp(t, m) << "\n";);
+        unsigned sz = m_result_stack.size();
+        SASSERT(sz >= 2);
+        sat::literal  l1 = m_result_stack[sz-1];
+        sat::literal  l2 = m_result_stack[sz-2];
+        if (root) {
+            SASSERT(sz == 2);
+            if (sign) {
+                mk_clause(l1, l2);
+                mk_clause(~l1, ~l2);
+            }
+            else {
+                mk_clause(l1, ~l2);
+                mk_clause(~l1, l2);
+            }
+            m_result_stack.reset();
+        }
+        else {
+            sat::bool_var k = m_solver.mk_var();
+            sat::literal  l(k, false);
+            m_cache.insert(t, l);
+            mk_clause(~l, l1, ~l2);
+            mk_clause(~l, ~l1, l2);
+            mk_clause(l,  l1, l2);
+            mk_clause(l, ~l1, ~l2);
+            m_result_stack.shrink(sz-2);
+            if (sign)
+                l.neg();
+            m_result_stack.push_back(l);
+        }
+    }
+
+    void convert(app * t, bool root, bool sign) {
+        SASSERT(t->get_family_id() == m.get_basic_family_id());
+        switch (to_app(t)->get_decl_kind()) {
+        case OP_OR:
+            convert_or(t, root, sign);
+            break;
+        case OP_ITE:
+            convert_ite(t, root, sign);
+            break;
+        case OP_IFF:
+        case OP_EQ:
+            convert_iff(t, root, sign);
+            break;
+        default:
+            UNREACHABLE();
+        }
+    }
+    
+    void process(expr * n) {
+        TRACE("goal2sat", tout << "converting: " << mk_ismt2_pp(n, m) << "\n";);
+        if (visit(n, true, false)) {
+            SASSERT(m_result_stack.empty());
+            return;
+        }
+        while (!m_frame_stack.empty()) {
+        loop:
+            cooperate("goal2sat");
+            if (m_cancel)
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+            if (memory::get_allocation_size() > m_max_memory)
+                throw tactic_exception(TACTIC_MAX_MEMORY_MSG);
+            frame & fr = m_frame_stack.back();
+            app * t    = fr.m_t;
+            bool root  = fr.m_root;
+            bool sign  = fr.m_sign;
+            TRACE("goal2sat_bug", tout << "result stack\n";
+                  tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
+                  for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
+                  tout << "\n";);
+            if (fr.m_idx == 0 && process_cached(t, root, sign)) {
+                m_frame_stack.pop_back();
+                continue;
+            }
+            if (m.is_not(t)) {
+                m_frame_stack.pop_back();
+                visit(t->get_arg(0), root, !sign);
+                continue;
+            }
+            unsigned num = t->get_num_args();
+            while (fr.m_idx < num) {
+                expr * arg = t->get_arg(fr.m_idx);
+                fr.m_idx++;
+                if (!visit(arg, false, false))
+                    goto loop;
+            }
+            TRACE("goal2sat_bug", tout << "converting\n";
+                  tout << mk_ismt2_pp(t, m) << " root: " << root << " sign: " << sign << "\n";
+                  for (unsigned i = 0; i < m_result_stack.size(); i++) tout << m_result_stack[i] << " ";
+                  tout << "\n";);
+            convert(t, root, sign);
+            m_frame_stack.pop_back();
+        }
+        SASSERT(m_result_stack.empty());
+    }
+
+
+    void operator()(goal const & g) {
+        m_interface_vars.reset();
+        collect_boolean_interface(g, m_interface_vars);
+        
+        unsigned size = g.size();
+        for (unsigned idx = 0; idx < size; idx++) {
+            expr * f = g.form(idx);
+            process(f);
+        }
+    }
+
+    void operator()(unsigned sz, expr * const * fs) {
+        m_interface_vars.reset();
+        collect_boolean_interface(m, sz, fs, m_interface_vars);
+        
+        for (unsigned i = 0; i < sz; i++)
+            process(fs[i]);
+    }
+
+    void set_cancel(bool f) { m_cancel = f; }
+};
+
+struct unsupported_bool_proc {
+    struct found {};
+    ast_manager & m;
+    unsupported_bool_proc(ast_manager & _m):m(_m) {}
+    void operator()(var *) {}
+    void operator()(quantifier *) {}
+    void operator()(app * n) { 
+        if (n->get_family_id() == m.get_basic_family_id()) {
+            switch (n->get_decl_kind()) {
+            case OP_AND:
+            case OP_XOR:
+            case OP_IMPLIES:
+            case OP_DISTINCT:
+                throw found();
+            default:
+                break;
+            }
+        }
+    }
+};
+
+/**
+   \brief Return true if s contains an unsupported Boolean operator.
+   goal_rewriter (with the following configuration) can be used to
+   eliminate unsupported operators.
+      :elim-and true
+      :blast-distinct true
+*/
+bool goal2sat::has_unsupported_bool(goal const & g) {
+    return test<unsupported_bool_proc>(g);
+}
+
+goal2sat::goal2sat():m_imp(0) {
+}
+
+void goal2sat::collect_param_descrs(param_descrs & r) {
+    insert_max_memory(r);
+    r.insert(":ite-extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas");
+}
+
+struct goal2sat::scoped_set_imp {
+    goal2sat * m_owner; 
+    scoped_set_imp(goal2sat * o, goal2sat::imp * i):m_owner(o) {
+        #pragma omp critical (goal2sat)
+        {
+            m_owner->m_imp = i;
+        }
+    }
+    ~scoped_set_imp() {
+        #pragma omp critical (goal2sat)
+        {
+            m_owner->m_imp = 0;
+        }
+    }
+};
+
+void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m) {
+    imp proc(g.m(), p, t, m);
+    scoped_set_imp set(this, &proc);
+    proc(g);
+}
+
+void goal2sat::set_cancel(bool f) {
+    #pragma omp critical (goal2sat)
+    {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+}
+
+struct sat2goal::imp {
+
+    // Wrapper for sat::model_converter: converts it into an "AST level" model_converter.
+    class sat_model_converter : public model_converter {
+        sat::model_converter        m_mc;
+        // TODO: the following mapping is storing a lot of useless information, and may be a performance bottleneck.
+        // We need to save only the expressions associated with variables that occur in m_mc.
+        // This information may be stored as a vector of pairs.
+        // The mapping is only created during the model conversion.
+        expr_ref_vector             m_var2expr;
+        ref<filter_model_converter> m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion
+        
+        sat_model_converter(ast_manager & m):
+            m_var2expr(m) {
+        }
+        
+    public:
+        sat_model_converter(ast_manager & m, sat::solver const & s):m_var2expr(m) {
+            m_mc.copy(s.get_model_converter());
+            m_fmc = alloc(filter_model_converter, m);
+        }
+        
+        ast_manager & m() { return m_var2expr.get_manager(); }
+        
+        void insert(expr * atom, bool aux) {
+            m_var2expr.push_back(atom);
+            if (aux) {
+                SASSERT(is_uninterp_const(atom));
+                SASSERT(m().is_bool(atom));
+                m_fmc->insert(to_app(atom)->get_decl());
+            }
+        }
+        
+        virtual void operator()(model_ref & md, unsigned goal_idx) {
+            SASSERT(goal_idx == 0);
+            TRACE("sat_mc", tout << "before sat_mc\n"; model_v2_pp(tout, *md); display(tout););
+            // REMARK: potential problem
+            // model_evaluator can't evaluate quantifiers. Then,
+            // an eliminated variable that depends on a quantified expression can't be recovered.
+            // A similar problem also affects any model_converter that uses elim_var_model_converter.
+            //
+            // Possible solution:
+            //   model_converters reject any variable elimination that depends on a quantified expression.
+            
+            model_evaluator ev(*md);
+            ev.set_model_completion(false);
+            
+            // create a SAT model using md
+            sat::model sat_md;
+            unsigned sz = m_var2expr.size();
+            expr_ref val(m());
+            for (sat::bool_var v = 0; v < sz; v++) {
+                expr * atom = m_var2expr.get(v);
+                ev(atom, val);
+                if (m().is_true(val)) 
+                    sat_md.push_back(l_true);
+                else if (m().is_false(val))
+                    sat_md.push_back(l_false);
+                else 
+                    sat_md.push_back(l_undef);
+            }
+            
+            // apply SAT model converter
+            m_mc(sat_md);
+            
+            // register value of non-auxiliary boolean variables back into md
+            sz = m_var2expr.size();
+            for (sat::bool_var v = 0; v < sz; v++) {
+                expr * atom = m_var2expr.get(v);
+                if (is_uninterp_const(atom)) {
+                    func_decl * d = to_app(atom)->get_decl();
+                    lbool new_val = sat_md[v];
+                    if (new_val == l_true)
+                        md->register_decl(d, m().mk_true());
+                    else if (new_val == l_false)
+                        md->register_decl(d, m().mk_false());
+                }
+            }
+            
+            // apply filter model converter
+            (*m_fmc)(md);
+            TRACE("sat_mc", tout << "after sat_mc\n"; model_v2_pp(tout, *md););
+        }
+        
+        virtual model_converter * translate(ast_translation & translator) {
+            sat_model_converter * res = alloc(sat_model_converter, translator.to());
+            res->m_fmc = static_cast<filter_model_converter*>(m_fmc->translate(translator));
+            unsigned sz = m_var2expr.size();
+            for (unsigned i = 0; i < sz; i++) 
+                res->m_var2expr.push_back(translator(m_var2expr.get(i)));
+            return res;
+        }
+        
+        void display(std::ostream & out) {
+            out << "(sat-model-converter\n";
+            m_mc.display(out);
+            sat::bool_var_set vars;
+            m_mc.collect_vars(vars);
+            out << "(atoms";
+            unsigned sz = m_var2expr.size();
+            for (unsigned i = 0; i < sz; i++) {
+                if (vars.contains(i)) {
+                    out << "\n (" << i << "\n  " << mk_ismt2_pp(m_var2expr.get(i), m(), 2) << ")";
+                }
+            }
+            out << ")\n";
+            m_fmc->display(out);
+            out << ")\n";
+        }
+    };
+
+    ast_manager &           m;
+    expr_ref_vector         m_lit2expr;
+    unsigned long long      m_max_memory;
+    bool                    m_learned;
+    volatile bool           m_cancel;
+    
+    imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m), m_cancel(false) {
+        updt_params(p);
+    }
+
+    void updt_params(params_ref const & p) {
+        m_learned        = p.get_bool(":learned", false);
+        m_max_memory     = megabytes_to_bytes(p.get_uint(":max-memory", UINT_MAX));
+    }
+
+    void checkpoint() {
+        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 init_lit2expr(sat::solver const & s, atom2bool_var const & map, model_converter_ref & mc, bool produce_models) {
+        ref<sat_model_converter> _mc;
+        if (produce_models)
+            _mc = alloc(sat_model_converter, m, s);
+        unsigned num_vars = s.num_vars();
+        m_lit2expr.resize(num_vars * 2);
+        map.mk_inv(m_lit2expr);
+        sort * b = m.mk_bool_sort();
+        for (sat::bool_var v = 0; v < num_vars; v++) {
+            checkpoint();
+            sat::literal l(v, false);
+            if (m_lit2expr.get(l.index()) == 0) {
+                SASSERT(m_lit2expr.get((~l).index()) == 0);
+                app * aux = m.mk_fresh_const(0, b);
+                if (_mc)
+                    _mc->insert(aux, true);
+                m_lit2expr.set(l.index(), aux);
+                m_lit2expr.set((~l).index(), m.mk_not(aux));
+            }
+            else {
+                if (_mc)
+                    _mc->insert(m_lit2expr.get(l.index()), false);
+                SASSERT(m_lit2expr.get((~l).index()) != 0);
+            }
+        }
+        mc = _mc.get();
+    }
+
+    expr * lit2expr(sat::literal l) {
+        return m_lit2expr.get(l.index());
+    }
+
+    void assert_clauses(sat::clause * const * begin, sat::clause * const * end, goal & r) {
+        ptr_buffer<expr> lits;
+        for (sat::clause * const * it = begin; it != end; it++) {
+            checkpoint();
+            lits.reset();
+            sat::clause const & c = *(*it);
+            unsigned sz = c.size();
+            for (unsigned i = 0; i < sz; i++) {
+                lits.push_back(lit2expr(c[i]));
+            }
+            r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
+        }
+    }
+
+    void operator()(sat::solver const & s, atom2bool_var const & map, goal & r, model_converter_ref & mc) {
+        if (s.inconsistent()) {
+            r.assert_expr(m.mk_false());
+            return;
+        }
+        init_lit2expr(s, map, mc, r.models_enabled());
+        // collect units
+        unsigned num_vars = s.num_vars();
+        for (sat::bool_var v = 0; v < num_vars; v++) {
+            checkpoint();
+            switch (s.value(v)) {
+            case l_true:
+                r.assert_expr(lit2expr(sat::literal(v, false)));
+                break;
+            case l_false:
+                r.assert_expr(lit2expr(sat::literal(v, true)));
+                break;
+            case l_undef:
+                break;
+            }
+        }
+        // collect binary clauses
+        svector<sat::solver::bin_clause> bin_clauses;
+        s.collect_bin_clauses(bin_clauses, m_learned);
+        svector<sat::solver::bin_clause>::iterator it  = bin_clauses.begin();
+        svector<sat::solver::bin_clause>::iterator end = bin_clauses.end();
+        for (; it != end; ++it) {
+            checkpoint();
+            r.assert_expr(m.mk_or(lit2expr(it->first), lit2expr(it->second)));
+        }
+        // collect clauses
+        assert_clauses(s.begin_clauses(), s.end_clauses(), r);
+        if (m_learned)
+            assert_clauses(s.begin_learned(), s.end_learned(), r);
+    }
+
+    void set_cancel(bool f) { m_cancel = f; }
+};
+
+sat2goal::sat2goal():m_imp(0) {
+}
+
+void sat2goal::collect_param_descrs(param_descrs & r) {
+    insert_max_memory(r);
+    r.insert(":learned", CPK_BOOL, "(default: false) collect also learned clauses.");
+}
+
+struct sat2goal::scoped_set_imp {
+    sat2goal * m_owner; 
+    scoped_set_imp(sat2goal * o, sat2goal::imp * i):m_owner(o) {
+        #pragma omp critical (sat2goal)
+        {
+            m_owner->m_imp = i;
+        }
+    }
+    ~scoped_set_imp() {
+        #pragma omp critical (sat2goal)
+        {
+            m_owner->m_imp = 0;
+        }
+    }
+};
+
+void sat2goal::operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p, 
+                          goal & g, model_converter_ref & mc) {
+    imp proc(g.m(), p);
+    scoped_set_imp set(this, &proc);
+    proc(t, m, g, mc);
+}
+
+void sat2goal::set_cancel(bool f) {
+    #pragma omp critical (sat2goal)
+    {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+}

src/tactic/sat_tactic/goal2sat.h

@@ -0,0 +1,86 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    goal2sat.h
+
+Abstract:
+
+    "Compile" a goal into the SAT engine.
+    Atoms are "abstracted" into boolean variables.
+    The mapping between boolean variables and atoms
+    can be used to convert back the state of the 
+    SAT engine into a goal.
+
+    The idea is to support scenarios such as:
+    1) simplify, blast, convert into SAT, and solve
+    2) convert into SAT, apply SAT for a while, learn new units, and translate back into a goal.
+    3) convert into SAT, apply SAT preprocessor (failed literal propagation, resolution, etc) and translate back into a goal.
+    4) Convert boolean structure into SAT, convert atoms into another engine, combine engines using lazy combination, solve.
+
+Author:
+
+    Leonardo (leonardo) 2011-10-26
+
+Notes:
+
+--*/
+#ifndef _GOAL2SAT_H_
+#define _GOAL2SAT_H_
+
+#include"goal.h"
+#include"sat_solver.h"
+#include"model_converter.h"
+#include"atom2bool_var.h"
+
+class goal2sat {
+    struct imp;
+    imp *  m_imp;
+    struct scoped_set_imp;
+public:
+    goal2sat();
+
+    static void collect_param_descrs(param_descrs & r);
+
+    static bool has_unsupported_bool(goal const & s);
+
+    /**
+       \brief "Compile" the goal into the given sat solver.
+       Store a mapping from atoms to boolean variables into m.
+       
+       \remark m doesn't need to be empty. the definitions there are 
+       reused.
+    
+       \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
+       an unsupported operator is found, or memory consumption limit is reached (set with param :max-memory).
+    */
+    void operator()(goal const & g, params_ref const & p, sat::solver & t, atom2bool_var & m);
+
+    void set_cancel(bool f);
+};
+
+
+class sat2goal {
+    struct imp;
+    imp *  m_imp;
+    struct scoped_set_imp;
+public:
+    sat2goal();
+
+    static void collect_param_descrs(param_descrs & r);
+
+    /**
+       \brief Translate the state of the SAT engine back into a goal.
+       The SAT solver may use variables that are not in \c m. The translator
+       creates fresh boolean AST variables for them. They are stored in fvars.
+       
+       \warning conversion throws a tactic_exception, if it is interrupted (by set_cancel),
+       or memory consumption limit is reached (set with param :max-memory).
+    */
+    void operator()(sat::solver const & t, atom2bool_var const & m, params_ref const & p, goal & s, model_converter_ref & mc);
+    
+    void set_cancel(bool f);
+};
+
+#endif

src/tactic/sat_tactic/sat_tactic.cpp

@@ -0,0 +1,218 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_tactic.cpp
+
+Abstract:
+
+    Tactic for using the SAT solver and its preprocessing capabilities.
+    
+Author:
+
+    Leonardo (leonardo) 2011-10-25
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"goal2sat.h"
+#include"sat_solver.h"
+#include"filter_model_converter.h"
+#include"ast_smt2_pp.h"
+#include"model_v2_pp.h"
+
+class sat_tactic : public tactic {
+
+    struct imp {
+        ast_manager &   m;
+        goal2sat        m_goal2sat;
+        sat2goal        m_sat2goal;
+        sat::solver     m_solver;
+        params_ref      m_params;
+        
+        imp(ast_manager & _m, params_ref const & p):
+            m(_m),
+            m_solver(p, 0),
+            m_params(p) {
+            SASSERT(!m.proofs_enabled());
+        }
+        
+        void operator()(goal_ref const & g, 
+                        goal_ref_buffer & result, 
+                        model_converter_ref & mc, 
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core) {
+            mc = 0; pc = 0; core = 0;
+            fail_if_proof_generation("sat", g);
+            fail_if_unsat_core_generation("sat", g);
+            bool produce_models = g->models_enabled();
+            TRACE("before_sat_solver", g->display(tout););
+            g->elim_redundancies();
+
+            atom2bool_var map(m);
+            m_goal2sat(*g, m_params, m_solver, map);
+            TRACE("sat_solver_unknown", tout << "interpreted_atoms: " << map.interpreted_atoms() << "\n";
+                  atom2bool_var::iterator it  = map.begin();
+                  atom2bool_var::iterator end = map.end();
+                  for (; it != end; ++it) {
+                      if (!is_uninterp_const(it->m_key))
+                          tout << mk_ismt2_pp(it->m_key, m) << "\n";
+                  });
+            g->reset();
+            g->m().compact_memory();
+
+            CASSERT("sat_solver", m_solver.check_invariant());
+            IF_VERBOSE(TACTIC_VERBOSITY_LVL, m_solver.display_status(verbose_stream()););
+            TRACE("sat_dimacs", m_solver.display_dimacs(tout););
+            
+            lbool r = m_solver.check();
+            if (r == l_false) {
+                g->assert_expr(m.mk_false(), 0, 0);
+            }
+            else if (r == l_true && !map.interpreted_atoms()) {
+                // register model
+                if (produce_models) {
+                    model_ref md = alloc(model, m);
+                    sat::model const & ll_m = m_solver.get_model();
+                    TRACE("sat_tactic", for (unsigned i = 0; i < ll_m.size(); i++) tout << i << ":" << ll_m[i] << " "; tout << "\n";);
+                    atom2bool_var::iterator it  = map.begin();
+                    atom2bool_var::iterator end = map.end();
+                    for (; it != end; ++it) {
+                        expr * n   = it->m_key;
+                        sat::bool_var v = it->m_value;
+                        TRACE("sat_tactic", tout << "extracting value of " << mk_ismt2_pp(n, m) << "\nvar: " << v << "\n";);
+                        switch (sat::value_at(v, ll_m)) {
+                        case l_true: 
+                            md->register_decl(to_app(n)->get_decl(), m.mk_true()); 
+                            break;
+                        case l_false:
+                            md->register_decl(to_app(n)->get_decl(), m.mk_false());
+                            break;
+                        default:
+                            break;
+                        }
+                    }
+                    TRACE("sat_tactic", model_v2_pp(tout, *md););
+                    mc = model2model_converter(md.get());
+                }
+            }
+            else {
+                // get simplified problem.
+#if 0
+                IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "\"formula constains interpreted atoms, recovering formula from sat solver...\"\n";);
+#endif
+                m_solver.pop(m_solver.scope_lvl());
+                m_sat2goal(m_solver, map, m_params, *(g.get()), mc);
+            }
+            g->inc_depth();
+            result.push_back(g.get());
+        }
+        
+        void set_cancel(bool f) {
+            m_goal2sat.set_cancel(f);
+            m_sat2goal.set_cancel(f);
+            m_solver.set_cancel(f);
+        }
+    };
+    
+    struct scoped_set_imp {
+        sat_tactic * m_owner; 
+
+        scoped_set_imp(sat_tactic * o, imp * i):m_owner(o) {
+            #pragma omp critical (sat_tactic)
+            {
+                m_owner->m_imp = i;
+            }
+        }
+        
+        ~scoped_set_imp() {
+            #pragma omp critical (sat_tactic)
+            {
+                m_owner->m_imp = 0;
+            }
+        }
+    };
+
+    imp *      m_imp;
+    params_ref m_params;
+    statistics m_stats;
+
+public:
+    sat_tactic(ast_manager & m, params_ref const & p):
+        m_imp(0),
+        m_params(p) {
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(sat_tactic, m, m_params);
+    }
+
+    virtual ~sat_tactic() {
+        SASSERT(m_imp == 0);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        goal2sat::collect_param_descrs(r);
+        sat2goal::collect_param_descrs(r);
+        sat::solver::collect_param_descrs(r);
+    }
+    
+    void operator()(goal_ref const & g, 
+                    goal_ref_buffer & result, 
+                    model_converter_ref & mc, 
+                    proof_converter_ref & pc,
+                    expr_dependency_ref & core) {
+        imp proc(g->m(), m_params);
+        scoped_set_imp set(this, &proc);
+        try {
+            proc(g, result, mc, pc, core);
+            proc.m_solver.collect_statistics(m_stats);
+        }
+        catch (sat::solver_exception & ex) {
+            proc.m_solver.collect_statistics(m_stats);
+            throw tactic_exception(ex.msg());
+        }
+        TRACE("sat_stats", m_stats.display_smt2(tout););
+    }
+
+    virtual void cleanup() {
+        SASSERT(m_imp == 0);
+    }
+
+    virtual void collect_statistics(statistics & st) const {
+        st.copy(m_stats);
+    }
+
+    virtual void reset_statistics() {
+        m_stats.reset();
+    }
+
+protected:
+    virtual void set_cancel(bool f) {
+        #pragma omp critical (sat_tactic)
+        {
+            if (m_imp)
+                m_imp->set_cancel(f);
+        }
+    }
+
+};
+
+tactic * mk_sat_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(sat_tactic, m, p));
+}
+
+tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p) {
+    params_ref p_aux;
+    p_aux.set_uint(":max-conflicts", 0);
+    tactic * t = clean(using_params(mk_sat_tactic(m, p), p_aux));
+    t->updt_params(p);
+    return t;
+}
+

src/tactic/sat_tactic/sat_tactic.h

@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    sat_tactic.cpp
+
+Abstract:
+
+    Tactic for using the SAT solver and its preprocessing capabilities.
+    
+Author:
+
+    Leonardo (leonardo) 2011-10-26
+
+Notes:
+
+--*/
+#ifndef _SAT_TACTIC_H_
+#define _SAT_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_sat_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+tactic * mk_sat_preprocessor_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+#endif