default_solver --> smt_solver

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

src/api/api_solver.cpp

@@ -29,7 +29,7 @@ Revision History:
 #include"cancel_eh.h"
 #include"scoped_timer.h"
 #include"smt_strategic_solver.h"
-#include"default_solver.h"
+#include"smt_solver.h"
 
 extern "C" {
 
@@ -38,7 +38,7 @@ extern "C" {
         LOG_Z3_mk_simple_solver(c);
         RESET_ERROR_CODE();
         Z3_solver_ref * s = alloc(Z3_solver_ref);
-        s->m_solver       = mk_default_solver();
+        s->m_solver       = mk_smt_solver();
         s->m_solver->set_front_end_params(mk_c(c)->fparams());
         s->m_solver->init(mk_c(c)->m(), symbol::null);
         mk_c(c)->save_object(s);

src/smt/default_solver.cpp

@@ -1,181 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    default_solver.cpp
-
-Abstract:
-
-    Wrapps smt::kernel as a solver for cmd_context
-
-Author:
-
-    Leonardo (leonardo) 2012-10-21
-
-Notes:
-
---*/
-#include"solver.h"
-#include"smt_kernel.h"
-#include"reg_decl_plugins.h"
-#include"front_end_params.h"
-
-class default_solver : public solver {
-    front_end_params * m_params;
-    smt::kernel *     m_context;
-public:
-    default_solver():m_params(0), m_context(0) {}
-
-    virtual ~default_solver() {
-        if (m_context != 0)
-            dealloc(m_context);
-    }
-
-    virtual void set_front_end_params(front_end_params & p) {
-        m_params = &p;
-    }
-
-    virtual void updt_params(params_ref const & p) {
-        if (m_context == 0)
-            return;
-        m_context->updt_params(p);
-    }
-
-    virtual void collect_param_descrs(param_descrs & r) {
-        if (m_context == 0) {
-            ast_manager m;
-            reg_decl_plugins(m);
-            front_end_params p;
-            smt::kernel s(m, p);
-            s.collect_param_descrs(r);
-        }
-        else {
-            m_context->collect_param_descrs(r);
-        }
-    }
-
-    virtual void init(ast_manager & m, symbol const & logic) {
-        SASSERT(m_params);
-        reset();
-        #pragma omp critical (solver)
-        {
-            m_context = alloc(smt::kernel, m, *m_params);
-        }
-        if (logic != symbol::null)
-            m_context->set_logic(logic);
-    }
-
-    virtual void collect_statistics(statistics & st) const {
-        if (m_context == 0) {
-            return;
-        }
-        else {
-            m_context->collect_statistics(st);
-        }
-    }
-
-    virtual void reset() {
-        if (m_context != 0) {
-            #pragma omp critical (solver)
-            {
-                dealloc(m_context);
-                m_context = 0;
-            }
-        }
-    }
-
-    virtual void assert_expr(expr * t) {
-        SASSERT(m_context);
-        m_context->assert_expr(t);
-    }
-
-    virtual void push() {
-        SASSERT(m_context);
-        m_context->push();
-    }
-
-    virtual void pop(unsigned n) {
-        SASSERT(m_context);
-        m_context->pop(n);
-    }
-
-    virtual unsigned get_scope_level() const {
-        if (m_context)
-            return m_context->get_scope_level();
-        else
-            return 0;
-    }
-
-    virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
-        SASSERT(m_context);
-        return m_context->check(num_assumptions, assumptions);
-    }
-
-    virtual void get_unsat_core(ptr_vector<expr> & r) {
-        SASSERT(m_context);
-        unsigned sz = m_context->get_unsat_core_size();
-        for (unsigned i = 0; i < sz; i++)
-            r.push_back(m_context->get_unsat_core_expr(i));
-    }
-
-    virtual void get_model(model_ref & m) {
-        SASSERT(m_context);
-        m_context->get_model(m);
-    }
-
-    virtual proof * get_proof() {
-        SASSERT(m_context);
-        return m_context->get_proof();
-    }
-
-    virtual std::string reason_unknown() const {
-        SASSERT(m_context);
-        return m_context->last_failure_as_string();
-    }
-
-    virtual void get_labels(svector<symbol> & r) {
-        SASSERT(m_context);
-        buffer<symbol> tmp;
-        m_context->get_relevant_labels(0, tmp);
-        r.append(tmp.size(), tmp.c_ptr());
-    }
-
-    virtual void set_cancel(bool f) {
-        #pragma omp critical (solver)
-        {
-            if (m_context) 
-                m_context->set_cancel(f);
-        }
-    }
-
-    virtual void set_progress_callback(progress_callback * callback) {
-        SASSERT(m_context);
-        m_context->set_progress_callback(callback);
-    }
-
-    virtual unsigned get_num_assertions() const {
-        if (m_context)
-            return m_context->size();
-        else
-            return 0;
-    }
-    
-    virtual expr * get_assertion(unsigned idx) const {
-        SASSERT(m_context);
-        SASSERT(idx < get_num_assertions());
-        return m_context->get_formulas()[idx];
-    }
-
-    virtual void display(std::ostream & out) const {
-        if (m_context)
-            m_context->display(out);
-        else
-            out << "(solver)";
-    }
-   
-};
-
-solver * mk_default_solver() {
-    return alloc(default_solver);
-}

src/smt/default_solver.h

@@ -1,26 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    default_solver.h
-
-Abstract:
-
-    Wrapps smt::kernel as a solver for cmd_context and external API
-
-Author:
-
-    Leonardo (leonardo) 2012-10-21
-
-Notes:
-
---*/
-#ifndef _DEFAULT_SOLVER_H_
-#define _DEFAULT_SOLVER_H_
-
-class solver;
-
-solver * mk_default_solver();
-
-#endif

src/smt/smt_solver.cpp

@@ -0,0 +1,185 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    smt_solver.cpp
+
+Abstract:
+
+    Wraps smt::kernel as a solver for the external API and cmd_context.
+
+Author:
+
+    Leonardo (leonardo) 2012-10-21
+
+Notes:
+
+--*/
+#include"solver.h"
+#include"smt_kernel.h"
+#include"reg_decl_plugins.h"
+#include"front_end_params.h"
+
+namespace smt {
+
+    class solver : public ::solver {
+        front_end_params * m_params;
+        smt::kernel *     m_context;
+    public:
+        solver():m_params(0), m_context(0) {}
+
+        virtual ~solver() {
+            if (m_context != 0)
+                dealloc(m_context);
+        }
+
+        virtual void set_front_end_params(front_end_params & p) {
+            m_params = &p;
+        }
+
+        virtual void updt_params(params_ref const & p) {
+            if (m_context == 0)
+                return;
+            m_context->updt_params(p);
+        }
+
+        virtual void collect_param_descrs(param_descrs & r) {
+            if (m_context == 0) {
+                ast_manager m;
+                reg_decl_plugins(m);
+                front_end_params p;
+                smt::kernel s(m, p);
+                s.collect_param_descrs(r);
+            }
+            else {
+                m_context->collect_param_descrs(r);
+            }
+        }
+
+        virtual void init(ast_manager & m, symbol const & logic) {
+            SASSERT(m_params);
+            reset();
+#pragma omp critical (solver)
+            {
+                m_context = alloc(smt::kernel, m, *m_params);
+            }
+            if (logic != symbol::null)
+                m_context->set_logic(logic);
+        }
+
+        virtual void collect_statistics(statistics & st) const {
+            if (m_context == 0) {
+                return;
+            }
+            else {
+                m_context->collect_statistics(st);
+            }
+        }
+
+        virtual void reset() {
+            if (m_context != 0) {
+#pragma omp critical (solver)
+                {
+                    dealloc(m_context);
+                    m_context = 0;
+                }
+            }
+        }
+
+        virtual void assert_expr(expr * t) {
+            SASSERT(m_context);
+            m_context->assert_expr(t);
+        }
+
+        virtual void push() {
+            SASSERT(m_context);
+            m_context->push();
+        }
+
+        virtual void pop(unsigned n) {
+            SASSERT(m_context);
+            m_context->pop(n);
+        }
+
+        virtual unsigned get_scope_level() const {
+            if (m_context)
+                return m_context->get_scope_level();
+            else
+                return 0;
+        }
+
+        virtual lbool check_sat(unsigned num_assumptions, expr * const * assumptions) {
+            SASSERT(m_context);
+            return m_context->check(num_assumptions, assumptions);
+        }
+
+        virtual void get_unsat_core(ptr_vector<expr> & r) {
+            SASSERT(m_context);
+            unsigned sz = m_context->get_unsat_core_size();
+            for (unsigned i = 0; i < sz; i++)
+                r.push_back(m_context->get_unsat_core_expr(i));
+        }
+
+        virtual void get_model(model_ref & m) {
+            SASSERT(m_context);
+            m_context->get_model(m);
+        }
+
+        virtual proof * get_proof() {
+            SASSERT(m_context);
+            return m_context->get_proof();
+        }
+
+        virtual std::string reason_unknown() const {
+            SASSERT(m_context);
+            return m_context->last_failure_as_string();
+        }
+
+        virtual void get_labels(svector<symbol> & r) {
+            SASSERT(m_context);
+            buffer<symbol> tmp;
+            m_context->get_relevant_labels(0, tmp);
+            r.append(tmp.size(), tmp.c_ptr());
+        }
+
+        virtual void set_cancel(bool f) {
+#pragma omp critical (solver)
+            {
+                if (m_context) 
+                    m_context->set_cancel(f);
+            }
+        }
+
+        virtual void set_progress_callback(progress_callback * callback) {
+            SASSERT(m_context);
+            m_context->set_progress_callback(callback);
+        }
+
+        virtual unsigned get_num_assertions() const {
+            if (m_context)
+                return m_context->size();
+            else
+                return 0;
+        }
+    
+        virtual expr * get_assertion(unsigned idx) const {
+            SASSERT(m_context);
+            SASSERT(idx < get_num_assertions());
+            return m_context->get_formulas()[idx];
+        }
+
+        virtual void display(std::ostream & out) const {
+            if (m_context)
+                m_context->display(out);
+            else
+                out << "(solver)";
+        }
+   
+    };
+
+};
+
+solver * mk_smt_solver() {
+    return alloc(smt::solver);
+}

src/smt/smt_solver.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    smt_solver.h
+
+Abstract:
+
+    Wraps smt::kernel as a solver for the external API and cmd_context.
+
+Author:
+
+    Leonardo (leonardo) 2012-10-21
+
+Notes:
+   
+    This file was called default_solver.h. It was a bad name.
+
+--*/
+#ifndef _SMT_SOLVER_H_
+#define _SMT_SOLVER_H_
+
+class solver;
+
+solver * mk_smt_solver();
+
+#endif

src/tactic/portfolio/smt_strategic_solver.cpp

@@ -34,7 +34,7 @@ Notes:
 #include"default_tactic.h"
 #include"ufbv_tactic.h"
 #include"qffpa_tactic.h"
-#include"default_solver.h"
+#include"smt_solver.h"
 
 MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p));
 MK_SIMPLE_TACTIC_FACTORY(qfidl_fct, mk_qfidl_tactic(m, p));
@@ -90,7 +90,7 @@ solver * mk_smt_strategic_solver(cmd_context & ctx) {
 solver * mk_smt_strategic_solver(bool force_tactic) {
     strategic_solver * s = alloc(strategic_solver);
     s->force_tactic(force_tactic);
-    s->set_inc_solver(mk_default_solver());
+    s->set_inc_solver(mk_smt_solver());
     init(s);
     return s;
 }