From 230382d4c993b2447526dfa33c77d42df93ac443 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Nov 2012 21:52:27 -0700 Subject: [PATCH] default_solver --> smt_solver Signed-off-by: Leonardo de Moura --- src/api/api_solver.cpp | 4 +- src/smt/default_solver.cpp | 181 ----------------- src/smt/default_solver.h | 26 --- src/smt/smt_solver.cpp | 185 ++++++++++++++++++ src/smt/smt_solver.h | 28 +++ src/tactic/portfolio/smt_strategic_solver.cpp | 4 +- 6 files changed, 217 insertions(+), 211 deletions(-) delete mode 100644 src/smt/default_solver.cpp delete mode 100644 src/smt/default_solver.h create mode 100644 src/smt/smt_solver.cpp create mode 100644 src/smt/smt_solver.h diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 9b3619a6e..8aecc0a3a 100644 --- a/src/api/api_solver.cpp +++ b/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); diff --git a/src/smt/default_solver.cpp b/src/smt/default_solver.cpp deleted file mode 100644 index 1a895d212..000000000 --- a/src/smt/default_solver.cpp +++ /dev/null @@ -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 & 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 & r) { - SASSERT(m_context); - buffer 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); -} diff --git a/src/smt/default_solver.h b/src/smt/default_solver.h deleted file mode 100644 index adffac1c3..000000000 --- a/src/smt/default_solver.h +++ /dev/null @@ -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 diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp new file mode 100644 index 000000000..516a6321e --- /dev/null +++ b/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 & 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 & r) { + SASSERT(m_context); + buffer 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); +} diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h new file mode 100644 index 000000000..e9af9aafa --- /dev/null +++ b/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 diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 52762edc4..00c0afaa5 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/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; }