diff --git a/scripts/mk_make.py b/scripts/mk_make.py index 2e21d45e5..51ea58836 100644 --- a/scripts/mk_make.py +++ b/scripts/mk_make.py @@ -43,7 +43,7 @@ add_lib('cmd_context', ['tactic', 'rewriter', 'model', 'old_params', 'simplifier # code to the new tactic framework. add_lib('assertion_set', ['cmd_context']) add_lib('substitution', ['ast'], 'ast/substitution') -add_lib('normal_forms', ['tactic', 'assertion_set']) +add_lib('normal_forms', ['tactic', 'old_params']) add_lib('pattern', ['normal_forms'], 'ast/pattern') add_lib('spc', ['simplifier', 'substitution', 'old_params', 'pattern']) add_lib('parser_util', ['ast']) @@ -52,7 +52,7 @@ add_lib('macros', ['simplifier', 'old_params'], 'ast/macros') 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', 'assertion_set'], 'tactic/bit_blaster') +add_lib('bit_blaster', ['rewriter', 'simplifier', 'old_params', 'tactic'], 'tactic/bit_blaster') add_lib('smt', ['assertion_set', 'bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util']) add_lib('user_plugin', ['smt'], 'smt/user_plugin') diff --git a/src/normal_forms/nnf.cpp b/src/normal_forms/nnf.cpp index 10ae1cb01..566eac8d7 100644 --- a/src/normal_forms/nnf.cpp +++ b/src/normal_forms/nnf.cpp @@ -29,10 +29,6 @@ Notes: #include"ast_smt2_pp.h" -// Old strategy framework -#include"assertion_set_strategy.h" - -// New framework #include"tactical.h" class skolemizer { @@ -365,9 +361,9 @@ struct nnf::imp { void checkpoint() { cooperate("nnf"); if (memory::get_allocation_size() > m_max_memory) - throw nnf_exception(STE_MAX_MEMORY_MSG); + throw nnf_exception(TACTIC_MAX_MEMORY_MSG); if (m_cancel) - throw nnf_exception(STE_CANCELED_MSG); + throw nnf_exception(TACTIC_CANCELED_MSG); } void set_new_child_flag() { @@ -931,100 +927,3 @@ void nnf::reset_cache() { m_imp->reset_cache(); } -// TODO: delete after conversion to new tactic framework is done. -class nnf_strategy : public assertion_set_strategy { - params_ref m_params; - nnf * m_nnf; - - struct set_nnf { - nnf_strategy & m_owner; - - set_nnf(nnf_strategy & owner, nnf & n): - m_owner(owner) { - #pragma omp critical (nnf_strategy) - { - m_owner.m_nnf = &n; - } - } - - ~set_nnf() { - #pragma omp critical (nnf_strategy) - { - m_owner.m_nnf = 0; - } - } - }; -public: - nnf_strategy(params_ref const & p): - m_params(p), - m_nnf(0) { - TRACE("nnf", tout << "nnf_strategy constructor: " << p << "\n";); - } - - virtual ~nnf_strategy() {} - - virtual void updt_params(params_ref const & p) { m_params = p; } - static void get_param_descrs(param_descrs & r) { nnf::get_param_descrs(r); } - virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } - - virtual void operator()(assertion_set & s, model_converter_ref & mc) { - TRACE("nnf", tout << "params: " << m_params << "\n"; s.display(tout);); - SASSERT(is_well_sorted(s)); - as_st_report report("nnf", s); - mc = 0; - if (s.inconsistent()) - return; - ast_manager & m = s.m(); - defined_names dnames(m); - nnf local_nnf(m, dnames, m_params); - set_nnf setter(*this, local_nnf); - - expr_ref_vector defs(m); - proof_ref_vector def_prs(m); - - expr_ref new_curr(m); - proof_ref new_pr(m); - - unsigned sz = s.size(); - for (unsigned i = 0; i < sz; i++) { - expr * curr = s.form(i); - local_nnf(curr, defs, def_prs, new_curr, new_pr); - if (m.proofs_enabled()) { - proof * pr = s.pr(i); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - s.update(i, new_curr, new_pr); - } - - sz = defs.size(); - for (unsigned i = 0; i < sz; i++) { - if (m.proofs_enabled()) - s.assert_expr(defs.get(i), def_prs.get(i)); - else - s.assert_expr(defs.get(i), 0); - } - TRACE("nnf", s.display(tout);); - SASSERT(is_well_sorted(s)); - } - - virtual void cleanup() {} - virtual void set_cancel(bool f) { - #pragma omp critical (nnf_strategy) - { - if (m_nnf) - m_nnf->set_cancel(f); - } - } -}; - -as_st * mk_snf(params_ref const & p) { - return alloc(nnf_strategy, p); -} - -as_st * mk_nnf(params_ref const & p) { - params_ref new_p(p); - new_p.set_sym(":nnf-mode", symbol("full")); - TRACE("nnf", tout << "mk_nnf: " << new_p << "\n";); - return using_params(mk_snf(), new_p); -} - diff --git a/src/normal_forms/nnf.h b/src/normal_forms/nnf.h index 10f6ba128..5674bd635 100644 --- a/src/normal_forms/nnf.h +++ b/src/normal_forms/nnf.h @@ -51,14 +51,6 @@ public: void reset_cache(); }; -// Old strategy framework -class assertion_set_strategy; -// Skolem Normal Form -assertion_set_strategy * mk_snf(params_ref const & p = params_ref()); -// Negation Normal Form -assertion_set_strategy * mk_nnf(params_ref const & p = params_ref()); - -// New strategy framework class tactic; // Skolem Normal Form tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref()); diff --git a/src/tactic/bit_blaster/bit_blaster_tpl.h b/src/tactic/bit_blaster/bit_blaster_tpl.h index 7901a3187..ca60d0f5c 100644 --- a/src/tactic/bit_blaster/bit_blaster_tpl.h +++ b/src/tactic/bit_blaster/bit_blaster_tpl.h @@ -20,7 +20,6 @@ Revision History: #define _BIT_BLASTER_TPL_H_ #include"rational.h" -#include"strategy_exception.h" template class bit_blaster_tpl : public Cfg { diff --git a/src/tactic/bit_blaster/bit_blaster_tpl_def.h b/src/tactic/bit_blaster/bit_blaster_tpl_def.h index f00c17322..4c8ef7662 100644 --- a/src/tactic/bit_blaster/bit_blaster_tpl_def.h +++ b/src/tactic/bit_blaster/bit_blaster_tpl_def.h @@ -20,13 +20,14 @@ Revision History: #include"rational.h" #include"ast_pp.h" #include"cooperate.h" +#include"tactic_exception.h" template void bit_blaster_tpl::checkpoint() { if (memory::get_allocation_size() > m_max_memory) - throw strategy_exception(STE_MAX_MEMORY_MSG); + throw tactic_exception(TACTIC_MAX_MEMORY_MSG); if (m_cancel) - throw strategy_exception(STE_CANCELED_MSG); + throw tactic_exception(TACTIC_CANCELED_MSG); cooperate("bit-blaster"); } diff --git a/src/tactic/core_tactics/reduce_args_tactic.cpp b/src/tactic/core_tactics/reduce_args_tactic.cpp index 417fd3bf2..686c5128d 100644 --- a/src/tactic/core_tactics/reduce_args_tactic.cpp +++ b/src/tactic/core_tactics/reduce_args_tactic.cpp @@ -17,7 +17,6 @@ Notes: --*/ #include"tactical.h" -#include"reduce_args.h" #include"cooperate.h" #include"ast_smt2_pp.h" #include"map.h" diff --git a/src/tactic/sls_tactic/sls_tactic.cpp b/src/tactic/sls_tactic/sls_tactic.cpp index 1e2bdff6a..93e61f3b3 100644 --- a/src/tactic/sls_tactic/sls_tactic.cpp +++ b/src/tactic/sls_tactic/sls_tactic.cpp @@ -26,8 +26,6 @@ Notes: #include"model_pp.h" #include"model_evaluator.h" #include"solve_eqs_tactic.h" -#include"assertion_set_rewriter.h" -#include"shallow_context_simplifier.h" #include"elim_uncnstr_tactic.h" #include"bv_size_reduction_tactic.h" #include"max_bv_sharing_tactic.h"