old_params ==> front_end_params. Isolated abstract solver interface

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

src/solver/check_sat_result.cpp

@@ -0,0 +1,54 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    check_sat_result.cpp
+
+Abstract:
+    Abstract interface for storing the result produced by 
+    a check_sat like command
+
+Author:
+
+    Leonardo (leonardo) 2012-11-01
+
+Notes:
+
+--*/
+#include"check_sat_result.h"
+
+simple_check_sat_result::simple_check_sat_result(ast_manager & m):
+    m_core(m),
+    m_proof(m) {
+    }
+
+simple_check_sat_result::~simple_check_sat_result() {
+}
+
+void simple_check_sat_result::collect_statistics(statistics & st) const { 
+    st.copy(m_stats); 
+}
+
+void simple_check_sat_result::get_unsat_core(ptr_vector<expr> & r) { 
+    if (m_status == l_false) 
+        r.append(m_core.size(), m_core.c_ptr()); 
+}
+ 
+void simple_check_sat_result::get_model(model_ref & m) { 
+    if (m_status != l_false) 
+        m = m_model; 
+    else 
+        m = 0; 
+}
+
+proof * simple_check_sat_result::get_proof() { 
+    return m_status == l_false ? m_proof.get() : 0; 
+}
+
+std::string simple_check_sat_result::reason_unknown() const { 
+    return m_unknown; 
+}
+
+void simple_check_sat_result::get_labels(svector<symbol> & r) {
+}

src/solver/check_sat_result.h

@@ -0,0 +1,77 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    check_sat_result.h
+
+Abstract:
+    Abstract interface for storing the result produced by 
+    a check_sat like command
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#ifndef _CHECK_SAT_RESULT_H_
+#define _CHECK_SAT_RESULT_H_
+
+#include"model.h"
+#include"lbool.h"
+#include"statistics.h"
+
+/**
+   \brief Abstract interface for the result of a (check-sat) like command.
+   It encapsulates information such as:
+      - the actual result: l_true (satisfiable), l_false (unsatisfiable), l_undef (unknown)
+      - statistics
+      - model (if the result is satisfiable)
+      - proof (if the result is unsatisfiable)
+      - unsat-core (if the result is unsatisfiable)
+      - reason-unknown (if the result is unknown, i.e., the solver failed to solve the problem)
+      - label (if the result is satisfiable) this is legacy for Boogie
+      
+*/
+class check_sat_result {
+protected:
+    unsigned    m_ref_count;
+    lbool       m_status; 
+public:
+    check_sat_result():m_ref_count(0), m_status(l_undef) {}
+    virtual ~check_sat_result() {}
+    void inc_ref() { m_ref_count++; }
+    void dec_ref() { SASSERT(m_ref_count > 0); m_ref_count--; if (m_ref_count == 0) dealloc(this); }
+    void set_status(lbool r) { m_status = r; }
+    lbool status() const { return m_status; }
+    virtual void collect_statistics(statistics & st) const = 0;
+    virtual void get_unsat_core(ptr_vector<expr> & r) = 0;
+    virtual void get_model(model_ref & m) = 0;
+    virtual proof * get_proof() = 0;
+    virtual std::string reason_unknown() const = 0;
+    virtual void get_labels(svector<symbol> & r) = 0;
+};
+
+/**
+   \brief Very simple implementation of the check_sat_result object.
+*/
+struct simple_check_sat_result : public check_sat_result {
+    statistics      m_stats;
+    model_ref       m_model;
+    expr_ref_vector m_core;
+    proof_ref       m_proof;
+    std::string     m_unknown;
+
+    simple_check_sat_result(ast_manager & m);
+    virtual ~simple_check_sat_result();
+    virtual void collect_statistics(statistics & st) const;
+    virtual void get_unsat_core(ptr_vector<expr> & r);
+    virtual void get_model(model_ref & m);
+    virtual proof * get_proof();
+    virtual std::string reason_unknown() const;
+    virtual void get_labels(svector<symbol> & r);
+};
+
+#endif

src/solver/progress_callback.h

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2008 Microsoft Corporation
+
+Module Name:
+
+    progress_callback.h
+
+Abstract:
+
+    Virtual callback for reporting progress.
+
+Author:
+
+    Michal Moskal (micmo) 2009-02-17.
+
+Revision History:
+
+--*/
+#ifndef _PROGRESS_CALLBACK_H_
+#define _PROGRESS_CALLBACK_H_
+
+class progress_callback {
+public:
+    virtual ~progress_callback() {}
+    
+    // Called on every check for resource limit exceeded (much more frequent).
+    virtual void fast_progress_sample() {}
+
+    // Less frequent invoked.
+    virtual void slow_progress_sample() {}
+};
+
+#endif

src/solver/solver.cpp

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    solver.h
+
+Abstract:
+
+    abstract solver interface
+
+Author:
+
+    Leonardo (leonardo) 2011-03-19
+
+Notes:
+
+--*/
+#include"solver.h"
+
+unsigned solver::get_num_assertions() const {
+    NOT_IMPLEMENTED_YET();
+    return 0;
+}
+
+expr * solver::get_assertion(unsigned idx) const {
+    NOT_IMPLEMENTED_YET();
+    return 0;
+}
+
+void solver::display(std::ostream & out) const {
+    out << "(solver)";
+}
+

src/solver/solver.h

@@ -0,0 +1,153 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    solver.h
+
+Abstract:
+
+    abstract solver interface
+
+Author:
+
+    Leonardo (leonardo) 2011-03-19
+
+Notes:
+
+--*/
+#ifndef _SOLVER_H_
+#define _SOLVER_H_
+
+#include"check_sat_result.h"
+#include"progress_callback.h"
+#include"params.h"
+
+struct front_end_params;
+
+/**
+   \brief Abstract interface for making solvers available in the Z3
+   API and front-ends such as SMT 2.0 and (legacy) SMT 1.0.
+
+   It provides the basic functionality for incremental solvers.
+     - assertions
+     - push/pop
+     - parameter setting (updt_params)
+     - statistics
+     - results based on check_sat_result API
+     - interruption (set_cancel)
+     - resets 
+*/
+class solver : public check_sat_result {
+public:
+    virtual ~solver() {}
+    
+    /**
+       \brief This method is invoked to allow the solver to access the front_end_params (environment parameters).
+       
+       \warning This method is used for backward compatibility. The first solver implemented in Z3 used
+       front_end_params to store its configuration parameters. 
+    */
+    virtual void set_front_end_params(front_end_params & p) {} 
+
+    /**
+       \brief Update the solver internal settings. 
+    */
+    virtual void updt_params(params_ref const & p) {}
+
+    /**
+       \brief Store in \c r a description of the configuration
+       parameters available in this solver.
+    */
+    virtual void collect_param_descrs(param_descrs & r) {}
+    
+    /**
+       \brief Enable/Disable proof production for this solver object.
+    
+       It is invoked before init(m, logic).
+    */
+    virtual void set_produce_proofs(bool f) {}
+    /**
+       \brief Enable/Disable model generation for this solver object.
+
+       It is invoked before init(m, logic).
+    */
+    virtual void set_produce_models(bool f) {}
+    /**
+       \brief Enable/Disable unsat core generation for this solver object.
+
+       It is invoked before init(m, logic).
+    */
+    virtual void set_produce_unsat_cores(bool f) {}
+    
+    /**
+       \brief Initialize the solver object with the given ast_manager and logic.
+    */
+    virtual void init(ast_manager & m, symbol const & logic) = 0;
+    
+    /**
+       \brief Reset the solver internal state. All assertions should be removed.
+    */
+    virtual void reset() = 0;
+
+    /**
+       \brief Add a new formula to the assertion stack.
+    */
+    virtual void assert_expr(expr * t) = 0;
+
+    /**
+       \brief Create a backtracking point.
+    */
+    virtual void push() = 0;
+
+    /**
+       \brief Remove \c n backtracking points. All assertions between the pop and matching push are removed. 
+    */
+    virtual void pop(unsigned n) = 0;
+
+    /**
+       \brief Return the number of backtracking points.
+    */
+    virtual unsigned get_scope_level() const = 0;
+
+    /**
+       \brief Check if the set of assertions in the assertion stack is satisfiable modulo the given assumptions.
+       
+       If it is unsatisfiable, and unsat-core generation is enabled. Then, the unsat-core is a subset of these assumptions.
+    */
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) = 0;
+
+    virtual void set_cancel(bool f) {}
+    /**
+       \brief Interrupt this solver.
+    */
+    void cancel() { set_cancel(true); }
+    /**
+       \brief Reset the interruption.
+    */
+    void reset_cancel() { set_cancel(false); }
+
+    /**
+       \brief Set a progress callback procedure that is invoked by this solver during check_sat.
+       
+       This is essentially for backward compatibility and integration with VCC tools.
+    */
+    virtual void set_progress_callback(progress_callback * callback) = 0;
+    
+    /**
+       \brief Return the number of assertions in the assertion stack.
+    */
+    virtual unsigned get_num_assertions() const;
+
+    /**
+       \brief Return the assertion at position idx in the assertion stack.
+    */
+    virtual expr * get_assertion(unsigned idx) const;
+
+    /**
+       \brief Display the content of this solver.
+    */
+    virtual void display(std::ostream & out) const;
+};
+
+#endif

src/solver/strategic_solver.cpp

@@ -0,0 +1,473 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    strategic_solver.h
+
+Abstract:
+
+    Strategies -> Solver
+
+Author:
+
+    Leonardo (leonardo) 2011-05-19
+
+Notes:
+
+--*/
+#include"strategic_solver.h"
+#include"scoped_timer.h"
+#include"front_end_params.h"
+#include"params2front_end_params.h"
+#include"ast_smt2_pp.h"
+
+// minimum verbosity level for portfolio verbose messages
+#define PS_VB_LVL 15
+
+strategic_solver_core::strategic_solver_core():
+    m_manager(0),
+    m_fparams(0),
+    m_force_tactic(false),
+    m_inc_mode(false),
+    m_check_sat_executed(false),
+    m_inc_solver(0),
+    m_inc_solver_timeout(UINT_MAX),
+    m_inc_unknown_behavior(IUB_USE_TACTIC_IF_QF),
+    m_default_fct(0),
+    m_curr_tactic(0),
+    m_proof(0),
+    m_callback(0) {
+    m_use_inc_solver_results = false;
+    DEBUG_CODE(m_num_scopes = 0;);
+    m_produce_proofs = false;
+    m_produce_models = false;
+    m_produce_unsat_cores = false;
+}
+
+strategic_solver_core::~strategic_solver_core() {
+    SASSERT(!m_curr_tactic);
+    dictionary<tactic_factory*>::iterator it  = m_logic2fct.begin();
+    dictionary<tactic_factory*>::iterator end = m_logic2fct.end();
+    for (; it != end; ++it) {
+        dealloc(it->m_value);
+    }
+    if (m_proof)
+        m().dec_ref(m_proof);
+}
+
+bool strategic_solver_core::has_quantifiers() const {
+    unsigned sz = get_num_assertions();
+    for (unsigned i = 0; i < sz; i++) {
+        if (::has_quantifiers(get_assertion(i)))
+            return true;
+    }
+    return false;
+}
+
+/**
+   \brief Return true if a tactic should be used when the incremental solver returns unknown.
+*/
+bool strategic_solver_core::use_tactic_when_undef() const {
+    switch (m_inc_unknown_behavior) {
+    case IUB_RETURN_UNDEF: return false;
+    case IUB_USE_TACTIC_IF_QF: return !has_quantifiers();
+    case IUB_USE_TACTIC: return true;
+    default:
+        UNREACHABLE();
+        return false;
+    }
+}
+
+void strategic_solver_core::set_inc_solver(solver * s) {
+    SASSERT(m_inc_solver == 0);
+    SASSERT(m_num_scopes == 0);
+    m_inc_solver = s;
+    if (m_callback)
+        m_inc_solver->set_progress_callback(m_callback);
+}
+
+void strategic_solver_core::updt_params(params_ref const & p) {
+    if (m_inc_solver)
+        m_inc_solver->updt_params(p);
+    if (m_fparams)
+        params2front_end_params(p, *m_fparams);
+}
+
+
+void strategic_solver_core::collect_param_descrs(param_descrs & r) {
+    if (m_inc_solver)
+        m_inc_solver->collect_param_descrs(r);
+}
+
+/**
+   \brief Set a timeout for each check_sat query that is processed by the inc_solver.
+   timeout == UINT_MAX means infinite
+   After the timeout a strategy is used.
+*/
+void strategic_solver_core::set_inc_solver_timeout(unsigned timeout) {
+    m_inc_solver_timeout = timeout;
+}
+
+/**
+   \brief Set the default tactic factory.
+   It is used if there is no tactic for a given logic.
+*/
+void strategic_solver_core::set_default_tactic(tactic_factory * fct) {
+    m_default_fct = fct;
+}
+
+/**
+   \brief Set a tactic factory for a given logic.
+*/
+void strategic_solver_core::set_tactic_for(symbol const & logic, tactic_factory * fct) {
+    tactic_factory * old_fct;
+    if (m_logic2fct.find(logic, old_fct)) {
+        dealloc(old_fct);
+    }
+    m_logic2fct.insert(logic, fct);
+}
+
+void strategic_solver_core::init(ast_manager & m, symbol const & logic) {
+    m_manager = &m;
+    m_logic   = logic;
+    if (m_inc_mode) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->init(m, logic);
+    }
+}
+
+// delayed inc solver initialization
+void strategic_solver_core::init_inc_solver() {
+    if (m_inc_mode) 
+        return; // solver was already initialized
+    if (!m_inc_solver)
+        return; // inc solver was not installed
+    m_inc_mode = true;
+    m_inc_solver->set_front_end_params(*m_fparams);
+    m_inc_solver->init(m(), m_logic);
+    unsigned sz = get_num_assertions();
+    for (unsigned i = 0; i < sz; i++) {
+        m_inc_solver->assert_expr(get_assertion(i));
+    }
+}
+
+void strategic_solver_core::collect_statistics(statistics & st) const {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->collect_statistics(st);
+    }
+    else {
+        if (m_curr_tactic) 
+            m_curr_tactic->collect_statistics(st); // m_curr_tactic is still being executed.
+        else
+            st.copy(m_stats);
+    }
+}
+
+void strategic_solver_core::reset() {
+    m_logic    = symbol::null;
+    m_inc_mode = false;
+    m_check_sat_executed = false;
+    if (m_inc_solver)
+        m_inc_solver->reset();
+    SASSERT(!m_curr_tactic);
+    m_use_inc_solver_results = false;
+    reset_results();
+}
+
+void strategic_solver_core::reset_results() {
+    m_use_inc_solver_results = false;
+    m_model = 0;
+    if (m_proof) {
+        m().dec_ref(m_proof);
+        m_proof = 0;
+    }
+    m_reason_unknown.clear();
+    m_stats.reset();
+}
+
+void strategic_solver_core::assert_expr(expr * t) {
+    if (m_check_sat_executed && !m_inc_mode) {
+        // a check sat was already executed --> switch to incremental mode
+        init_inc_solver();
+        SASSERT(m_inc_solver == 0 || m_inc_mode);
+    }
+    if (m_inc_mode) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->assert_expr(t);
+    }
+}
+
+void strategic_solver_core::push() {
+    DEBUG_CODE(m_num_scopes++;);
+    init_inc_solver();
+    if (m_inc_solver)
+        m_inc_solver->push();
+}
+
+void strategic_solver_core::pop(unsigned n) {
+    DEBUG_CODE({
+            SASSERT(n <= m_num_scopes);
+            m_num_scopes -= n;
+        });
+    init_inc_solver();
+    if (m_inc_solver)
+        m_inc_solver->pop(n);
+}
+
+unsigned strategic_solver_core::get_scope_level() const {
+    if (m_inc_solver)
+        return m_inc_solver->get_scope_level();
+    else
+        return 0;
+}
+
+struct aux_timeout_eh : public event_handler {
+    solver *        m_solver;
+    volatile bool   m_canceled;
+    aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
+    virtual void operator()() {
+        m_solver->cancel();
+        m_canceled = true;
+    }
+};
+
+struct strategic_solver_core::mk_tactic {
+    strategic_solver_core *  m_solver;
+
+    mk_tactic(strategic_solver_core * s, tactic_factory * f):m_solver(s) {
+        ast_manager & m = s->m();
+        params_ref p;
+        front_end_params2params(*s->m_fparams, p);
+        tactic * tct = (*f)(m, p);
+        tct->set_front_end_params(*s->m_fparams);
+        tct->set_logic(s->m_logic);
+        if (s->m_callback)
+            tct->set_progress_callback(s->m_callback);
+        #pragma omp critical (strategic_solver) 
+        {
+            s->m_curr_tactic = tct;
+        }
+    }
+
+    ~mk_tactic() {
+        #pragma omp critical (strategic_solver)
+        {
+            m_solver->m_curr_tactic = 0;
+        }
+    }
+};
+
+tactic_factory * strategic_solver_core::get_tactic_factory() const {
+    tactic_factory * f = 0;
+    if (m_logic2fct.find(m_logic, f))
+        return f;
+    return m_default_fct.get();
+}
+
+lbool strategic_solver_core::check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions) {
+    if (!m_inc_solver) {
+        IF_VERBOSE(PS_VB_LVL, verbose_stream() << "incremental solver was not installed, returning unknown...\n";);
+        m_use_inc_solver_results = false;
+        m_reason_unknown         = "incomplete";
+        return l_undef; 
+    }
+    init_inc_solver();
+    m_use_inc_solver_results = true;
+    return m_inc_solver->check_sat(num_assumptions, assumptions);
+}
+
+lbool strategic_solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) {
+    reset_results();
+    m_check_sat_executed = true;
+    if (num_assumptions > 0 || // assumptions were provided
+        (!m_fparams->m_auto_config && !m_force_tactic) // auto config and force_tactic are turned off
+        ) {
+        // must use incremental solver
+        return check_sat_with_assumptions(num_assumptions, assumptions);
+    }
+
+    tactic_factory * factory = get_tactic_factory();
+    if (factory == 0)
+        init_inc_solver(); // try to switch to incremental solver
+    
+    if (m_inc_mode) {
+        SASSERT(m_inc_solver);
+        unsigned timeout = m_inc_solver_timeout;
+        if (factory == 0)
+            timeout = UINT_MAX; // there is no tactic available
+        if (timeout == UINT_MAX) {
+            IF_VERBOSE(PS_VB_LVL, verbose_stream() << "using incremental solver (without a timeout).\n";);            
+            m_use_inc_solver_results = true;
+            lbool r = m_inc_solver->check_sat(0, 0);
+            if (r != l_undef || factory == 0 || !use_tactic_when_undef()) {
+                m_use_inc_solver_results = true;
+                return r;
+            }
+        }
+        else {
+            IF_VERBOSE(PS_VB_LVL, verbose_stream() << "using incremental solver (with timeout).\n";);            
+            SASSERT(factory != 0);
+            aux_timeout_eh eh(m_inc_solver.get());
+            lbool r;
+            {
+                scoped_timer timer(m_inc_solver_timeout, &eh);
+                r = m_inc_solver->check_sat(0, 0);
+            }
+            if ((r != l_undef || !use_tactic_when_undef()) && !eh.m_canceled) {
+                m_use_inc_solver_results = true;
+                return r;
+            }
+        }
+        IF_VERBOSE(PS_VB_LVL, verbose_stream() << "incremental solver failed, trying tactic.\n";);                        
+    }
+    
+    m_use_inc_solver_results = false;
+    
+    if (factory == 0) {
+        IF_VERBOSE(PS_VB_LVL, verbose_stream() << "there is no tactic available for the current logic.\n";);            
+        m_reason_unknown         = "incomplete";
+        return l_undef; 
+    }
+
+    goal_ref g = alloc(goal, m(), m_produce_proofs, m_produce_models, m_produce_unsat_cores);
+    unsigned sz = get_num_assertions();
+    for (unsigned i = 0; i < sz; i++) {
+        g->assert_expr(get_assertion(i));
+    }
+    expr_dependency_ref core(m());
+    
+    mk_tactic tct_maker(this, factory);
+    SASSERT(m_curr_tactic);
+
+    proof_ref pr(m());
+    lbool r = ::check_sat(*(m_curr_tactic.get()), g, m_model, pr, core, m_reason_unknown);
+    m_curr_tactic->collect_statistics(m_stats);
+    if (pr) {
+        m_proof = pr; 
+        m().inc_ref(m_proof);
+    }
+    return r;
+}
+
+void strategic_solver_core::set_cancel(bool f) {
+    if (m_inc_solver)
+        m_inc_solver->set_cancel(f);
+    #pragma omp critical (strategic_solver)
+    {
+        if (m_curr_tactic)
+            m_curr_tactic->set_cancel(f);
+    }
+}
+
+void strategic_solver_core::get_unsat_core(ptr_vector<expr> & r) {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->get_unsat_core(r); 
+    }
+}
+
+void strategic_solver_core::get_model(model_ref & m) {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->get_model(m);
+    }
+    else {
+        m = m_model;
+    }
+}
+
+proof * strategic_solver_core::get_proof() {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        return m_inc_solver->get_proof();
+    }
+    else {
+        return m_proof;
+    }
+}
+
+std::string strategic_solver_core::reason_unknown() const {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        return m_inc_solver->reason_unknown();
+    }
+    return m_reason_unknown;
+}
+
+void strategic_solver_core::get_labels(svector<symbol> & r) {
+    if (m_use_inc_solver_results) {
+        SASSERT(m_inc_solver);
+        m_inc_solver->get_labels(r);
+    }
+}
+
+void strategic_solver_core::set_progress_callback(progress_callback * callback) { 
+    m_callback = callback; 
+    if (m_inc_solver)
+        m_inc_solver->set_progress_callback(callback);
+}
+
+void strategic_solver_core::display(std::ostream & out) const {
+    if (m_manager) {
+        unsigned num = get_num_assertions();
+        out << "(solver";
+        for (unsigned i = 0; i < num; i++) {
+            out << "\n  " << mk_ismt2_pp(get_assertion(i), m(), 2);
+        }
+        out << ")";
+    }
+    else {
+        out << "(solver)";
+    }
+}
+
+
+strategic_solver::ctx::ctx(ast_manager & m):m_assertions(m) {
+}
+
+void strategic_solver::init(ast_manager & m, symbol const & logic) {
+    strategic_solver_core::init(m, logic);
+    m_ctx = alloc(ctx, m);
+}
+
+unsigned strategic_solver::get_num_assertions() const {
+    if (m_ctx == 0)
+        return 0;
+    return m_ctx->m_assertions.size();
+}
+
+expr * strategic_solver::get_assertion(unsigned idx) const {
+    SASSERT(m_ctx);
+    return m_ctx->m_assertions.get(idx);
+}
+
+void strategic_solver::assert_expr(expr * t) {
+    SASSERT(m_ctx);
+    strategic_solver_core::assert_expr(t);
+    m_ctx->m_assertions.push_back(t);
+}
+
+void strategic_solver::push() {
+    SASSERT(m_ctx);
+    strategic_solver_core::push();
+    m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
+}
+
+void strategic_solver::pop(unsigned n) {
+    SASSERT(m_ctx);
+    unsigned new_lvl = m_ctx->m_scopes.size() - n;
+    unsigned old_sz  = m_ctx->m_scopes[new_lvl];
+    m_ctx->m_assertions.shrink(old_sz);
+    m_ctx->m_scopes.shrink(new_lvl);
+    strategic_solver_core::pop(n);
+}
+
+void strategic_solver::reset() {
+    m_ctx = 0;
+    strategic_solver_core::reset();
+}
+
+
+

src/solver/strategic_solver.h

@@ -0,0 +1,169 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    strategic_solver.h
+
+Abstract:
+
+    Strategies -> Solver
+
+Author:
+
+    Leonardo (leonardo) 2011-05-19
+
+Notes:
+
+--*/
+#ifndef _STRATEGIC_SOLVER_H_
+#define _STRATEGIC_SOLVER_H_
+
+#include"solver.h"
+#include"tactic.h"
+
+class progress_callback;
+struct front_end_params;
+
+/**
+   \brief Implementation of the solver API that supports:
+       - a different tactic for each logic 
+       - a general purpose tactic
+       - a default incremental solver
+
+   The strategic solver has two modes:
+       - non-incremental
+       - incremental
+   In non-incremental mode, tactics are used.
+   In incremental model, the incremental (general purpose) solver is used.
+   
+   A timeout for the incremental solver can be specified.
+   If the timeout is reached, then the strategic_solver tries to solve the problem using tactics.
+
+   The strategic_solver switches to incremental when:
+       - push is used
+       - assertions are peformed after a check_sat
+   It goes back to non_incremental mode when:
+       - reset is invoked.
+*/
+class strategic_solver_core : public solver {
+public:
+    // Behavior when the incremental solver returns unknown.
+    enum inc_unknown_behavior {
+        IUB_RETURN_UNDEF,      // just return unknown
+        IUB_USE_TACTIC_IF_QF,  // invoke tactic if problem is quantifier free
+        IUB_USE_TACTIC         // invoke tactic
+    };
+
+private:
+    ast_manager *        m_manager;
+    front_end_params *   m_fparams;
+    symbol               m_logic;
+    bool                 m_force_tactic; // use tactics even when auto_config = false
+    bool                 m_inc_mode;
+    bool                 m_check_sat_executed;
+    scoped_ptr<solver>   m_inc_solver;
+    unsigned             m_inc_solver_timeout;
+    inc_unknown_behavior m_inc_unknown_behavior;
+    scoped_ptr<tactic_factory>  m_default_fct;
+    dictionary<tactic_factory*> m_logic2fct;
+
+    ref<tactic>          m_curr_tactic;
+    
+    bool                 m_use_inc_solver_results;
+    model_ref            m_model;
+    proof *              m_proof;
+    std::string          m_reason_unknown;
+    statistics           m_stats;
+
+#ifdef Z3DEBUG
+    unsigned             m_num_scopes;
+#endif
+
+    bool                 m_produce_proofs;
+    bool                 m_produce_models;
+    bool                 m_produce_unsat_cores;
+
+    progress_callback *  m_callback;
+
+    void reset_results();
+    void init_inc_solver();
+    tactic_factory * get_tactic_factory() const;
+    lbool check_sat_with_assumptions(unsigned num_assumptions, expr * const * assumptions);
+
+    struct mk_tactic;
+
+    bool has_quantifiers() const;
+    bool use_tactic_when_undef() const;
+
+public:
+    strategic_solver_core();
+    ~strategic_solver_core();
+
+    ast_manager & m() const { SASSERT(m_manager); return *m_manager; }
+
+    void set_inc_solver(solver * s);
+    void set_inc_solver_timeout(unsigned timeout);
+    void set_default_tactic(tactic_factory * fct);
+    void set_tactic_for(symbol const & logic, tactic_factory * fct);
+    void set_inc_unknown_behavior(inc_unknown_behavior b) { m_inc_unknown_behavior = b; }
+    void force_tactic(bool f) { m_force_tactic = f; }
+
+    virtual void set_front_end_params(front_end_params & p) { m_fparams = &p; }
+
+    virtual void updt_params(params_ref const & p);
+    virtual void collect_param_descrs(param_descrs & r);
+
+    virtual void set_produce_proofs(bool f) { m_produce_proofs = f; }
+    virtual void set_produce_models(bool f) { m_produce_models = f; }
+    virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; }
+
+    virtual unsigned get_num_assertions() const = 0;
+    virtual expr * get_assertion(unsigned idx) const = 0;
+    
+    virtual void display(std::ostream & out) const;
+    
+    virtual void init(ast_manager & m, symbol const & logic);
+    virtual void collect_statistics(statistics & st) const;
+    virtual void reset();
+    virtual void assert_expr(expr * t);
+    virtual void push();
+    virtual void pop(unsigned n);
+    virtual unsigned get_scope_level() const;
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
+    virtual void get_unsat_core(ptr_vector<expr> & r);
+    virtual void get_model(model_ref & m);
+    virtual proof * get_proof();
+    virtual std::string reason_unknown() const;
+    virtual void get_labels(svector<symbol> & r);
+    virtual void set_cancel(bool f);
+    virtual void set_progress_callback(progress_callback * callback);
+};
+
+/**
+   \brief Default implementation of strategic_solver_core
+*/
+class strategic_solver : public strategic_solver_core {
+    struct ctx {
+        expr_ref_vector              m_assertions;
+        unsigned_vector              m_scopes;
+        ctx(ast_manager & m);
+    };
+    scoped_ptr<ctx>            m_ctx;
+public:
+    strategic_solver() {}
+
+    virtual void init(ast_manager & m, symbol const & logic);
+
+    virtual void assert_expr(expr * t);
+    virtual void push();
+    virtual void pop(unsigned n);
+    virtual void reset();
+
+    virtual unsigned get_num_assertions() const;
+    virtual expr * get_assertion(unsigned idx) const;
+};
+
+
+
+#endif

src/solver/tactic2solver.cpp

@@ -0,0 +1,258 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    tactic2solver.cpp
+
+Abstract:
+
+    Wrapper for implementing the solver interface
+    using a tactic.
+
+    This is a light version of the strategic solver.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#include"tactic2solver.h"
+#include"params2front_end_params.h"
+#include"ast_smt2_pp.h"
+
+tactic2solver_core::ctx::ctx(ast_manager & m, symbol const & logic):
+    m_logic(logic),
+    m_assertions(m) {
+}
+
+tactic2solver_core::~tactic2solver_core() {
+}
+
+void tactic2solver_core::init(ast_manager & m, symbol const & logic) {
+    m_ctx = alloc(ctx, m, logic);
+}
+
+void tactic2solver_core::updt_params(params_ref const & p) {
+    m_params = p;
+}
+
+void tactic2solver_core::collect_param_descrs(param_descrs & r) {
+    if (m_ctx) {
+        if (!m_ctx->m_tactic) {
+            #pragma omp critical (tactic2solver_core)
+            {
+                m_ctx->m_tactic = get_tactic(m_ctx->m(), m_params);
+            }
+
+            if (m_ctx->m_tactic) {
+                m_ctx->m_tactic->collect_param_descrs(r);
+            }
+
+            #pragma omp critical (tactic2solver_core)
+            {
+                m_ctx->m_tactic = 0;
+            }
+        }
+        else {
+            m_ctx->m_tactic->collect_param_descrs(r);
+        }
+    }
+}
+
+void tactic2solver_core::reset() {
+    SASSERT(m_ctx);
+    m_ctx->m_assertions.reset();
+    m_ctx->m_scopes.reset();
+    m_ctx->m_result = 0;
+}
+
+void tactic2solver_core::assert_expr(expr * t) {
+    SASSERT(m_ctx);
+    m_ctx->m_assertions.push_back(t);
+    m_ctx->m_result = 0;
+}
+
+void tactic2solver_core::push() {
+    SASSERT(m_ctx);
+    m_ctx->m_scopes.push_back(m_ctx->m_assertions.size());
+    m_ctx->m_result = 0;
+}
+
+void tactic2solver_core::pop(unsigned n) {
+    SASSERT(m_ctx);
+    unsigned new_lvl = m_ctx->m_scopes.size() - n;
+    unsigned old_sz  = m_ctx->m_scopes[new_lvl];
+    m_ctx->m_assertions.shrink(old_sz);
+    m_ctx->m_scopes.shrink(new_lvl);
+    m_ctx->m_result = 0;
+}
+
+unsigned tactic2solver_core::get_scope_level() const {
+    SASSERT(m_ctx);
+    return m_ctx->m_scopes.size();
+}
+
+lbool tactic2solver_core::check_sat(unsigned num_assumptions, expr * const * assumptions) {
+    SASSERT(m_ctx);
+    ast_manager & m = m_ctx->m();
+    params_ref p = m_params;
+    if (m_fparams)
+        front_end_params2params(*m_fparams, p);
+    #pragma omp critical (tactic2solver_core)
+    {
+        m_ctx->m_tactic = get_tactic(m, p);
+        if (m_ctx->m_tactic) {
+            m_ctx->m_result = alloc(simple_check_sat_result, m);
+        }
+    }
+    if (!m_ctx->m_tactic)
+        return l_undef;
+    tactic & t                       = *(m_ctx->m_tactic);
+    simple_check_sat_result & result = *(m_ctx->m_result);
+    if (m_fparams)
+        t.set_front_end_params(*m_fparams);
+    goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores);
+    t.set_logic(m_ctx->m_logic);
+    unsigned sz = m_ctx->m_assertions.size();
+    for (unsigned i = 0; i < sz; i++) {
+        g->assert_expr(m_ctx->m_assertions.get(i));
+    }
+    for (unsigned i = 0; i < num_assumptions; i++) {
+        g->assert_expr(assumptions[i], m.mk_asserted(assumptions[i]), m.mk_leaf(assumptions[i]));
+    }
+
+    model_ref           md;
+    proof_ref           pr(m);
+    expr_dependency_ref core(m);
+    std::string         reason_unknown = "unknown";
+    try {
+        switch (::check_sat(t, g, md, pr, core, reason_unknown)) {
+        case l_true: 
+            result.set_status(l_true);
+            break;
+        case l_false: 
+            result.set_status(l_false);
+            break;
+        default: 
+            result.set_status(l_undef);
+            if (reason_unknown != "")
+                result.m_unknown = reason_unknown;
+            break;
+        }
+    }
+    catch (z3_error & ex) {
+        throw ex;
+    }
+    catch (z3_exception & ex) {
+        TRACE("tactic2solver_core", tout << "exception: " << ex.msg() << "\n";);
+        result.set_status(l_undef);
+        result.m_unknown = ex.msg();
+    }
+    t.collect_statistics(result.m_stats);
+    result.m_model = md;
+    result.m_proof = pr;
+    if (m_produce_unsat_cores) {
+        ptr_vector<expr> core_elems;
+        m.linearize(core, core_elems);
+        result.m_core.append(core_elems.size(), core_elems.c_ptr());
+    }
+    
+    #pragma omp critical (tactic2solver_core)
+    {
+        m_ctx->m_tactic = 0;
+    }
+    return result.status();
+}
+
+void tactic2solver_core::set_cancel(bool f) {
+    #pragma omp critical (tactic2solver_core)
+    {
+        if (m_ctx && m_ctx->m_tactic)
+            m_ctx->m_tactic->set_cancel(f);
+    }
+}
+
+void tactic2solver_core::collect_statistics(statistics & st) const {
+    if (m_ctx->m_result.get())
+        m_ctx->m_result->collect_statistics(st);
+}
+
+void tactic2solver_core::get_unsat_core(ptr_vector<expr> & r) {
+    if (m_ctx->m_result.get())
+        m_ctx->m_result->get_unsat_core(r);
+}
+
+void tactic2solver_core::get_model(model_ref & m) {
+    if (m_ctx->m_result.get())
+        m_ctx->m_result->get_model(m);
+}
+
+proof * tactic2solver_core::get_proof() {
+    if (m_ctx->m_result.get())
+        return m_ctx->m_result->get_proof();
+    else
+        return 0;
+}
+
+std::string tactic2solver_core::reason_unknown() const {
+    if (m_ctx->m_result.get())
+        return m_ctx->m_result->reason_unknown();
+    else
+        return std::string("unknown");
+}
+
+unsigned tactic2solver_core::get_num_assertions() const {
+    if (m_ctx) 
+        return m_ctx->m_assertions.size();
+    else
+        return 0;
+}
+
+expr * tactic2solver_core::get_assertion(unsigned idx) const {
+    SASSERT(m_ctx);
+    return m_ctx->m_assertions.get(idx);
+}
+
+void tactic2solver_core::display(std::ostream & out) const {
+    if (m_ctx) {
+        ast_manager & m = m_ctx->m_assertions.m();
+        unsigned num = m_ctx->m_assertions.size();
+        out << "(solver";
+        for (unsigned i = 0; i < num; i++) {
+            out << "\n  " << mk_ismt2_pp(m_ctx->m_assertions.get(i), m, 2);
+        }
+        out << ")";
+    }
+    else {
+        out << "(solver)";
+    }
+}
+
+tactic2solver::tactic2solver(tactic * t):
+    m_tactic(t) {
+}
+
+tactic2solver::~tactic2solver() {
+}
+
+tactic * tactic2solver::get_tactic(ast_manager & m, params_ref const & p) {
+    m_tactic->cleanup();
+    m_tactic->updt_params(p);
+    return m_tactic.get();
+}
+
+tactic_factory2solver::~tactic_factory2solver() {
+}
+
+void tactic_factory2solver::set_tactic(tactic_factory * f) {
+    m_tactic_factory = f;
+}
+
+tactic * tactic_factory2solver::get_tactic(ast_manager & m, params_ref const & p) {
+    if (m_tactic_factory == 0)
+        return 0;
+    return (*m_tactic_factory)(m, p);
+}

src/solver/tactic2solver.h

@@ -0,0 +1,112 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    tactic2solver.h
+
+Abstract:
+
+    Wrapper for implementing the external solver interface
+    using a tactic.
+
+    This is a light version of the strategic solver.
+
+Author:
+
+    Leonardo (leonardo) 2012-01-23
+
+Notes:
+
+--*/
+#ifndef _TACTIC2SOLVER_H_
+#define _TACTIC2SOLVER_H_
+
+#include"solver.h"
+#include"tactic.h"
+
+/**
+   \brief Simulates the incremental solver interface using a tactic.
+
+   Every query will be solved from scratch.  So, this is not a good
+   option for applications trying to solve many easy queries that a
+   similar to each other.
+*/
+class tactic2solver_core : public solver {
+    struct ctx {
+        symbol                       m_logic;
+        expr_ref_vector              m_assertions;
+        unsigned_vector              m_scopes;
+        ref<simple_check_sat_result> m_result;
+        tactic_ref                   m_tactic;
+        ctx(ast_manager & m, symbol const & logic);
+        ast_manager & m() const { return m_assertions.m(); }
+    };
+    scoped_ptr<ctx>            m_ctx;
+    front_end_params *         m_fparams;
+    params_ref                 m_params;
+    bool                       m_produce_models;
+    bool                       m_produce_proofs;
+    bool                       m_produce_unsat_cores;
+public:
+    tactic2solver_core():m_ctx(0), m_fparams(0), m_produce_models(false), m_produce_proofs(false), m_produce_unsat_cores(false) {}
+    virtual ~tactic2solver_core();
+
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p) = 0;
+    
+    virtual void set_front_end_params(front_end_params & p) { m_fparams = &p; } 
+
+    virtual void updt_params(params_ref const & p);
+    virtual void collect_param_descrs(param_descrs & r);
+
+    virtual void set_produce_proofs(bool f) { m_produce_proofs = f; }
+    virtual void set_produce_models(bool f) { m_produce_models = f; }
+    virtual void set_produce_unsat_cores(bool f) { m_produce_unsat_cores = f; }
+
+    virtual void init(ast_manager & m, symbol const & logic);
+    virtual void reset();
+    virtual void assert_expr(expr * t);
+    virtual void push();
+    virtual void pop(unsigned n);
+    virtual unsigned get_scope_level() const;
+    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions);
+
+    virtual void set_cancel(bool f);
+
+    virtual void collect_statistics(statistics & st) const;
+    virtual void get_unsat_core(ptr_vector<expr> & r);
+    virtual void get_model(model_ref & m);
+    virtual proof * get_proof();
+    virtual std::string reason_unknown() const;
+    virtual void get_labels(svector<symbol> & r) {}
+
+    virtual void set_progress_callback(progress_callback * callback) {}
+
+    virtual unsigned get_num_assertions() const;
+    virtual expr * get_assertion(unsigned idx) const;
+
+    virtual void display(std::ostream & out) const;
+};
+
+class tactic2solver : public tactic2solver_core {
+    tactic_ref m_tactic;
+public:
+    tactic2solver(tactic * t);
+    virtual ~tactic2solver();
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p);
+};
+
+
+class tactic_factory2solver : public tactic2solver_core {
+    scoped_ptr<tactic_factory> m_tactic_factory;
+public:
+    virtual ~tactic_factory2solver();
+    /**
+       \brief Set tactic that will be used to process the satisfiability queries.
+    */
+    void set_tactic(tactic_factory * f); 
+    virtual tactic * get_tactic(ast_manager & m, params_ref const & p);
+};
+
+
+#endif