From 4f6b34bc7b00351a376fda28f6856dc34896e984 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 24 Oct 2012 14:04:33 -0700
Subject: [PATCH] removing last refs to assertion_set
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
scripts/mk_make.py | 2 +-
src/muz_qe/arith_bounds_tactic.cpp | 1 -
src/muz_qe/dl_mk_coi_filter.cpp | 4 +-
src/smt/smt_solver_strategy.cpp | 182 -------------------------
src/smt/smt_solver_strategy.h | 31 -----
src/tactic/ufbv_tactic/ufbv_tactic.cpp | 6 +-
6 files changed, 6 insertions(+), 220 deletions(-)
delete mode 100644 src/smt/smt_solver_strategy.cpp
delete mode 100644 src/smt/smt_solver_strategy.h
diff --git a/scripts/mk_make.py b/scripts/mk_make.py
index e29c11772..13a3696a7 100644
--- a/scripts/mk_make.py
+++ b/scripts/mk_make.py
@@ -53,7 +53,7 @@ add_lib('grobner', ['ast'], 'math/grobner')
add_lib('euclid', ['util'], 'math/euclid')
add_lib('proof_checker', ['rewriter', 'spc'], 'ast/proof_checker')
add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'tactic'], 'tactic/bit_blaster')
-add_lib('smt', ['assertion_set', 'bit_blaster', 'macros', 'normal_forms', 'cmd_context',
+add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context',
'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util'])
add_lib('user_plugin', ['smt'], 'smt/user_plugin')
add_lib('core_tactics', ['tactic', 'normal_forms'], 'tactic/core_tactics')
diff --git a/src/muz_qe/arith_bounds_tactic.cpp b/src/muz_qe/arith_bounds_tactic.cpp
index afafbb4b5..0de507183 100644
--- a/src/muz_qe/arith_bounds_tactic.cpp
+++ b/src/muz_qe/arith_bounds_tactic.cpp
@@ -1,7 +1,6 @@
#include"arith_bounds_tactic.h"
-#include"assertion_set_util.h"
#include"arith_decl_plugin.h"
struct arith_bounds_tactic : public tactic {
diff --git a/src/muz_qe/dl_mk_coi_filter.cpp b/src/muz_qe/dl_mk_coi_filter.cpp
index bd05e5cf7..04d654120 100644
--- a/src/muz_qe/dl_mk_coi_filter.cpp
+++ b/src/muz_qe/dl_mk_coi_filter.cpp
@@ -22,7 +22,7 @@ Revision History:
#include <sstream>
#include"ast_pp.h"
#include"dl_mk_coi_filter.h"
-#include"elim_var_model_converter.h"
+#include"extension_model_converter.h"
namespace datalog {
@@ -93,7 +93,7 @@ namespace datalog {
if (res && mc) {
decl_set::iterator end = pruned_preds.end();
decl_set::iterator it = pruned_preds.begin();
- elim_var_model_converter* mc0 = alloc(elim_var_model_converter, m);
+ extension_model_converter* mc0 = alloc(extension_model_converter, m);
for (; it != end; ++it) {
mc0->insert(*it, m.mk_true());
}
diff --git a/src/smt/smt_solver_strategy.cpp b/src/smt/smt_solver_strategy.cpp
deleted file mode 100644
index a7cd8a6b8..000000000
--- a/src/smt/smt_solver_strategy.cpp
+++ /dev/null
@@ -1,182 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
- smt_solver_strategy.cpp
-
-Abstract:
-
- Wraps a solver as an assertion_set strategy.
- **Temporary code**
- It should be deleted when we finish porting the assertion_set code to the tactic framework.
-
-Author:
-
- Leonardo (leonardo) 2012-10-20
-
-Notes:
-
---*/
-#include"smt_solver_strategy.h"
-#include"smt_solver.h"
-#include"front_end_params.h"
-#include"params2front_end_params.h"
-
-class as_st_solver : public assertion_set_strategy {
- scoped_ptr<front_end_params> m_params;
- params_ref m_params_ref;
- statistics m_stats;
- std::string m_failure;
- smt::solver * m_ctx;
- bool m_candidate_models;
- symbol m_logic;
- progress_callback * m_callback;
-public:
- as_st_solver(bool candidate_models):m_ctx(0), m_candidate_models(candidate_models), m_callback(0) {}
-
- front_end_params & fparams() {
- if (!m_params)
- m_params = alloc(front_end_params);
- return *m_params;
- }
-
- struct scoped_init_ctx {
- as_st_solver & m_owner;
-
- scoped_init_ctx(as_st_solver & o, ast_manager & m):m_owner(o) {
- smt::solver * new_ctx = alloc(smt::solver, m, o.fparams());
- TRACE("as_solver", tout << "logic: " << o.m_logic << "\n";);
- new_ctx->set_logic(o.m_logic);
- if (o.m_callback) {
- new_ctx->set_progress_callback(o.m_callback);
- }
- #pragma omp critical (as_st_solver)
- {
- o.m_ctx = new_ctx;
- }
- }
-
- ~scoped_init_ctx() {
- smt::solver * d = m_owner.m_ctx;
- #pragma omp critical (as_st_cancel)
- {
- m_owner.m_ctx = 0;
- }
- if (d)
- dealloc(d);
- }
- };
-
- virtual ~as_st_solver() {
- SASSERT(m_ctx == 0);
- }
-
- virtual void updt_params(params_ref const & p) {
- TRACE("as_solver", tout << "updt_params: " << p << "\n";);
- m_params_ref = p;
- params2front_end_params(m_params_ref, fparams());
- }
-
- virtual void collect_param_descrs(param_descrs & r) {
- }
-
- virtual void set_cancel(bool f) {
- if (m_ctx)
- m_ctx->set_cancel(f);
- }
-
- virtual void operator()(assertion_set & s, model_converter_ref & mc) {
- SASSERT(is_well_sorted(s));
- IF_VERBOSE(ST_VERBOSITY_LVL, verbose_stream() << "(smt-solver)" << std::endl;);
- TRACE("as_solver", tout << "AUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
- << " PREPROCESS: " << fparams().m_preprocess << ", SOLVER:" << fparams().m_solver << "\n";);
- TRACE("as_solver_detail", s.display(tout););
- ast_manager & m = s.m();
- TRACE("as_solver_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";);
- // verbose_stream() << "wasted_size: " << m.get_allocator().get_wasted_size() << ", free_objs: " << m.get_allocator().get_num_free_objs() << "\n";
- // m.get_allocator().consolidate();
- scoped_init_ctx init(*this, m);
- SASSERT(m_ctx != 0);
- unsigned sz = s.size();
- for (unsigned i = 0; i < sz; i++) {
- expr * f = s.form(i);
- m_ctx->assert_expr(f);
- }
- lbool r = m_ctx->setup_and_check();
- m_ctx->collect_statistics(m_stats);
- switch (r) {
- case l_true: {
- // the empty assertion set is trivially satifiable.
- s.reset();
- // store the model in a do nothin model converter.
- model_ref md;
- m_ctx->get_model(md);
- mc = model2model_converter(md.get());
- return;
- }
- case l_false:
- // formula is unsat, reset the assertion set, and store false there.
- s.reset();
- s.assert_expr(m.mk_false(), m_ctx->get_proof());
- return;
- case l_undef:
- if (m_candidate_models) {
- switch (m_ctx->last_failure()) {
- case smt::NUM_CONFLICTS:
- case smt::THEORY:
- case smt::QUANTIFIERS: {
- model_ref md;
- m_ctx->get_model(md);
- mc = model2model_converter(md.get());
- return;
- }
- default:
- break;
- }
- }
- m_failure = m_ctx->last_failure_as_string();
- throw strategy_exception(m_failure.c_str());
- }
- }
-
- virtual void collect_statistics(statistics & st) const {
- if (m_ctx)
- m_ctx->collect_statistics(st); // ctx is still running...
- else
- st.copy(m_stats);
- }
-
- virtual void cleanup() {
- }
-
- virtual void reset_statistics() {
- m_stats.reset();
- }
-
- // for backward compatibility
- virtual void set_front_end_params(front_end_params & p) {
- m_params = alloc(front_end_params, p);
- // must propagate the params_ref to fparams
- params2front_end_params(m_params_ref, fparams());
- }
-
- virtual void set_logic(symbol const & l) {
- m_logic = l;
- }
-
- virtual void set_progress_callback(progress_callback * callback) {
- m_callback = callback;
- }
-};
-
-as_st * mk_smt_solver_core(bool candidate_models) {
- return alloc(as_st_solver, candidate_models);
-}
-
-as_st * mk_smt_solver(bool auto_config, bool candidate_models) {
- as_st * solver = mk_smt_solver_core(candidate_models);
- params_ref solver_p;
- solver_p.set_bool(":auto-config", auto_config);
- return using_params(solver, solver_p);
-};
diff --git a/src/smt/smt_solver_strategy.h b/src/smt/smt_solver_strategy.h
deleted file mode 100644
index eb74dc530..000000000
--- a/src/smt/smt_solver_strategy.h
+++ /dev/null
@@ -1,31 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
- smt_solver_strategy.h
-
-Abstract:
-
- Wraps a solver as an assertion_set strategy.
- **Temporary code**
- It should be deleted when we finish porting the assertion_set code to the tactic framework.
-
-Author:
-
- Leonardo (leonardo) 2012-10-20
-
-Notes:
-
---*/
-#ifndef _SMT_SOLVER_STRATEGY_H_
-#define _SMT_SOLVER_STRATEGY_H_
-
-#include"assertion_set_strategy.h"
-
-as_st * mk_smt_solver_core(bool candidate_models = false);
-as_st * mk_smt_solver(bool auto_config = true, bool candidate_models = false);
-
-MK_SIMPLE_ST_FACTORY(smt_solver_stf, mk_smt_solver());
-
-#endif
diff --git a/src/tactic/ufbv_tactic/ufbv_tactic.cpp b/src/tactic/ufbv_tactic/ufbv_tactic.cpp
index 3091d6e53..fa280c482 100644
--- a/src/tactic/ufbv_tactic/ufbv_tactic.cpp
+++ b/src/tactic/ufbv_tactic/ufbv_tactic.cpp
@@ -28,8 +28,8 @@ Notes:
#include"macro_manager.h"
#include"macro_finder.h"
#include"quasi_macros.h"
-#include"elim_var_model_converter.h"
#include"ufbv_rewriter.h"
+#include"extension_model_converter.h"
#include"distribute_forall_tactic.h"
#include"der_tactic.h"
#include"reduce_args_tactic.h"
@@ -97,7 +97,7 @@ class macro_finder_tactic : public tactic {
for (; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), new_proofs.get(i), 0);
- elim_var_model_converter * evmc = alloc(elim_var_model_converter, mm.get_manager());
+ extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
unsigned num = mm.get_num_macros();
for (unsigned i = 0; i < num; i++) {
expr_ref f_interp(mm.get_manager());
@@ -377,7 +377,7 @@ class quasi_macros_tactic : public tactic {
for (; i < new_forms.size(); i++)
g->assert_expr(new_forms.get(i), new_proofs.get(i), 0);
- elim_var_model_converter * evmc = alloc(elim_var_model_converter, mm.get_manager());
+ extension_model_converter * evmc = alloc(extension_model_converter, mm.get_manager());
unsigned num = mm.get_num_macros();
for (unsigned i = 0; i < num; i++) {
expr_ref f_interp(mm.get_manager());