From 6c2ef9e70cc83f2f73b539006a476e72c61e4144 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 26 Oct 2012 13:50:31 +0100 Subject: [PATCH] UFBV tactic fixed and cleanup. Signed-off-by: Christoph M. Wintersteiger --- src/tactic/ufbv/macro_finder_tactic.cpp | 169 +++++++++ src/tactic/ufbv/macro_finder_tactic.h | 28 ++ src/tactic/ufbv/quasi_macros_tactic.cpp | 179 +++++++++ src/tactic/ufbv/quasi_macros_tactic.h | 28 ++ src/tactic/ufbv/ufbv_rewriter_tactic.cpp | 147 ++++++++ src/tactic/ufbv/ufbv_rewriter_tactic.h | 28 ++ src/tactic/ufbv/ufbv_tactic.cpp | 456 +---------------------- src/tactic/ufbv/ufbv_tactic.h | 5 +- 8 files changed, 600 insertions(+), 440 deletions(-) create mode 100644 src/tactic/ufbv/macro_finder_tactic.cpp create mode 100644 src/tactic/ufbv/macro_finder_tactic.h create mode 100644 src/tactic/ufbv/quasi_macros_tactic.cpp create mode 100644 src/tactic/ufbv/quasi_macros_tactic.h create mode 100644 src/tactic/ufbv/ufbv_rewriter_tactic.cpp create mode 100644 src/tactic/ufbv/ufbv_rewriter_tactic.h diff --git a/src/tactic/ufbv/macro_finder_tactic.cpp b/src/tactic/ufbv/macro_finder_tactic.cpp new file mode 100644 index 000000000..c58c04f14 --- /dev/null +++ b/src/tactic/ufbv/macro_finder_tactic.cpp @@ -0,0 +1,169 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + macro_finder_tactic.cpp + +Abstract: + + Macro finder + +Author: + + Christoph (cwinter) 2012-10-26 + +Notes: + +--*/ +#include"tactical.h" +#include"simplifier.h" +#include"basic_simplifier_plugin.h" +#include"arith_simplifier_plugin.h" +#include"bv_simplifier_plugin.h" +#include"macro_manager.h" +#include"macro_finder.h" +#include"extension_model_converter.h" +#include"macro_finder_tactic.h" + +class macro_finder_tactic : public tactic { + + struct imp { + ast_manager & m_manager; + bool m_cancel; + bool m_elim_and; + + imp(ast_manager & m, params_ref const & p) : m_manager(m),m_elim_and(false),m_cancel(false) { + updt_params(p); + } + + ast_manager & m() const { return m_manager; } + + void set_cancel(bool f) { + m_cancel = f; + } + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(g->is_well_sorted()); + mc = 0; pc = 0; core = 0; + tactic_report report("macro-finder", *g); + fail_if_unsat_core_generation("macro-finder", g); + + bool produce_proofs = g->proofs_enabled(); + bool produce_models = g->models_enabled(); + + simplifier simp(m_manager); + basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager); + bsimp->set_eliminate_and(m_elim_and); + simp.register_plugin(bsimp); + arith_simplifier_params a_params; + arith_simplifier_plugin * asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, a_params); + simp.register_plugin(asimp); + bv_simplifier_params bv_params; + bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params); + simp.register_plugin(bvsimp); + + macro_manager mm(m_manager, simp); + macro_finder mf(m_manager, mm); + + expr_ref_vector forms(m_manager), new_forms(m_manager); + proof_ref_vector proofs(m_manager), new_proofs(m_manager); + unsigned size = g->size(); + for (unsigned idx = 0; idx < size; idx++) { + forms.push_back(g->form(idx)); + proofs.push_back(g->pr(idx)); + } + + mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); + + unsigned i = 0; + for (; i < g->size(); i++) + g->update(i, new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0); + + for (; i < new_forms.size(); i++) + g->assert_expr(new_forms.get(i), new_proofs.get(i), 0); + + 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()); + func_decl * f = mm.get_macro_interpretation(i, f_interp); + evmc->insert(f, f_interp); + } + mc = evmc; + + g->inc_depth(); + result.push_back(g.get()); + TRACE("macro-finder", g->display(tout);); + SASSERT(g->is_well_sorted()); + } + + void updt_params(params_ref const & p) { + m_elim_and = p.get_bool(":elim-and", false); + } + }; + + imp * m_imp; + params_ref m_params; +public: + macro_finder_tactic(ast_manager & m, params_ref const & p): + m_params(p) { + m_imp = alloc(imp, m, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(macro_finder_tactic, m, m_params); + } + + virtual ~macro_finder_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + insert_produce_models(r); + insert_produce_proofs(r); + r.insert(":elim-and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); + } + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + (*m_imp)(in, result, mc, pc, core); + } + + virtual void cleanup() { + ast_manager & m = m_imp->m(); + imp * d = m_imp; + #pragma omp critical (tactic_cancel) + { + m_imp = 0; + } + dealloc(d); + d = alloc(imp, m, m_params); + #pragma omp critical (tactic_cancel) + { + m_imp = d; + } + } + + virtual void set_cancel(bool f) { + if (m_imp) + m_imp->set_cancel(f); + } +}; + +tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p) { + return alloc(macro_finder_tactic, m, p); +} diff --git a/src/tactic/ufbv/macro_finder_tactic.h b/src/tactic/ufbv/macro_finder_tactic.h new file mode 100644 index 000000000..560f89b23 --- /dev/null +++ b/src/tactic/ufbv/macro_finder_tactic.h @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + macro_finder_tactic.h + +Abstract: + + Macro finder + +Author: + + Christoph (cwinter) 2012-10-26 + +Notes: + +--*/ +#ifndef _MACRO_FINDER_TACTIC_H_ +#define _MACRO_FINDER_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p = params_ref()); + +#endif diff --git a/src/tactic/ufbv/quasi_macros_tactic.cpp b/src/tactic/ufbv/quasi_macros_tactic.cpp new file mode 100644 index 000000000..6356adfbe --- /dev/null +++ b/src/tactic/ufbv/quasi_macros_tactic.cpp @@ -0,0 +1,179 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + quasi_macros_tactic.cpp + +Abstract: + + Quasi-Macros + +Author: + + Christoph (cwinter) 2012-10-26 + +Notes: + +--*/ +#include"tactical.h" +#include"simplifier.h" +#include"basic_simplifier_plugin.h" +#include"arith_simplifier_plugin.h" +#include"bv_simplifier_plugin.h" +#include"macro_manager.h" +#include"macro_finder.h" +#include"extension_model_converter.h" +#include"quasi_macros.h" +#include"quasi_macros_tactic.h" + +class quasi_macros_tactic : public tactic { + + struct imp { + ast_manager & m_manager; + bool m_cancel; + + imp(ast_manager & m, params_ref const & p) : m_manager(m),m_cancel(false) { + updt_params(p); + } + + ast_manager & m() const { return m_manager; } + + void set_cancel(bool f) { + m_cancel = f; + } + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(g->is_well_sorted()); + mc = 0; pc = 0; core = 0; + tactic_report report("quasi-macros", *g); + fail_if_unsat_core_generation("quasi-macros", g); + + bool produce_proofs = g->proofs_enabled(); + bool produce_models = g->models_enabled(); + + simplifier simp(m_manager); + basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager); + bsimp->set_eliminate_and(true); + simp.register_plugin(bsimp); + arith_simplifier_params a_params; + arith_simplifier_plugin * asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, a_params); + simp.register_plugin(asimp); + bv_simplifier_params bv_params; + bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params); + simp.register_plugin(bvsimp); + + macro_manager mm(m_manager, simp); + quasi_macros qm(m_manager, mm, *bsimp, simp); + bool more = true; + + expr_ref_vector forms(m_manager), new_forms(m_manager); + proof_ref_vector proofs(m_manager), new_proofs(m_manager); + + unsigned size = g->size(); + for (unsigned i = 0; i < size; i++) { + forms.push_back(g->form(i)); + proofs.push_back(g->pr(i)); + } + + while (more) { // CMW: use repeat(...) ? + if (m_cancel) + throw tactic_exception(TACTIC_CANCELED_MSG); + + new_forms.reset(); + new_proofs.reset(); + more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); + forms.swap(new_forms); + proofs.swap(new_proofs); + } + + unsigned i = 0; + for (; i < g->size(); i++) + g->update(i, new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0); + + for (; i < new_forms.size(); i++) + g->assert_expr(new_forms.get(i), new_proofs.get(i), 0); + + 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()); + func_decl * f = mm.get_macro_interpretation(i, f_interp); + evmc->insert(f, f_interp); + } + mc = evmc; + + g->inc_depth(); + result.push_back(g.get()); + TRACE("quasi-macros", g->display(tout);); + SASSERT(g->is_well_sorted()); + } + + void updt_params(params_ref const & p) { + } + }; + + imp * m_imp; + params_ref m_params; + +public: + quasi_macros_tactic(ast_manager & m, params_ref const & p): + m_params(p) { + m_imp = alloc(imp, m, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(quasi_macros_tactic, m, m_params); + } + + virtual ~quasi_macros_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + insert_produce_models(r); + insert_produce_proofs(r); + } + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + (*m_imp)(in, result, mc, pc, core); + } + + virtual void cleanup() { + ast_manager & m = m_imp->m(); + imp * d = m_imp; + #pragma omp critical (tactic_cancel) + { + m_imp = 0; + } + dealloc(d); + d = alloc(imp, m, m_params); + #pragma omp critical (tactic_cancel) + { + m_imp = d; + } + } + + virtual void set_cancel(bool f) { + if (m_imp) + m_imp->set_cancel(f); + } +}; + +tactic * mk_quasi_macros_tactic(ast_manager & m, params_ref const & p) { + return alloc(quasi_macros_tactic, m, p); +} diff --git a/src/tactic/ufbv/quasi_macros_tactic.h b/src/tactic/ufbv/quasi_macros_tactic.h new file mode 100644 index 000000000..c09771761 --- /dev/null +++ b/src/tactic/ufbv/quasi_macros_tactic.h @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + quasi_macros_tactic.h + +Abstract: + + Quasi-Macros + +Author: + + Christoph (cwinter) 2012-10-26 + +Notes: + +--*/ +#ifndef _QUASI_MACROS_TACTIC_H_ +#define _QUASI_MACROS_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_quasi_macros_tactic(ast_manager & m, params_ref const & p = params_ref()); + +#endif diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.cpp b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp new file mode 100644 index 000000000..b9c0b5f7c --- /dev/null +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.cpp @@ -0,0 +1,147 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + ufbv_rewriter_tactic.cpp + +Abstract: + + UFBV Rewriter (demodulator) + +Author: + + Christoph (cwinter) 2012-10-26 + +Notes: + +--*/ +#include"tactical.h" +#include"simplifier.h" +#include"basic_simplifier_plugin.h" +#include"ufbv_rewriter.h" +#include"ufbv_rewriter_tactic.h" + +class ufbv_rewriter_tactic : public tactic { + + struct imp { + ast_manager & m_manager; + bool m_cancel; + + imp(ast_manager & m, params_ref const & p) : m_manager(m),m_cancel(false) { + updt_params(p); + } + + ast_manager & m() const { return m_manager; } + + void set_cancel(bool f) { + m_cancel = f; + } + + void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + SASSERT(g->is_well_sorted()); + mc = 0; pc = 0; core = 0; + tactic_report report("ufbv-rewriter", *g); + fail_if_unsat_core_generation("ufbv-rewriter", g); + + bool produce_proofs = g->proofs_enabled(); + bool produce_models = g->models_enabled(); + + basic_simplifier_plugin bsimp(m_manager); + bsimp.set_eliminate_and(true); + ufbv_rewriter dem(m_manager, bsimp); + + expr_ref_vector forms(m_manager), new_forms(m_manager); + proof_ref_vector proofs(m_manager), new_proofs(m_manager); + + unsigned size = g->size(); + for (unsigned i = 0; i < size; i++) { + forms.push_back(g->form(i)); + proofs.push_back(g->pr(i)); + } + + dem(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); + + unsigned i = 0; + for (; i < g->size(); i++) + g->update(i, new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, g->dep(i)); + + for (; i < new_forms.size(); i++) + g->assert_expr(new_forms.get(i), new_proofs.get(i), 0); + + mc = 0; // CMW: Remark: The demodulator could potentially remove all references to a variable. + + g->inc_depth(); + result.push_back(g.get()); + TRACE("ufbv-rewriter", g->display(tout);); + SASSERT(g->is_well_sorted()); + } + + void updt_params(params_ref const & p) { + } + }; + + imp * m_imp; + params_ref m_params; + +public: + ufbv_rewriter_tactic(ast_manager & m, params_ref const & p): + m_params(p) { + m_imp = alloc(imp, m, p); + } + + virtual tactic * translate(ast_manager & m) { + return alloc(ufbv_rewriter_tactic, m, m_params); + } + + virtual ~ufbv_rewriter_tactic() { + dealloc(m_imp); + } + + virtual void updt_params(params_ref const & p) { + m_params = p; + m_imp->updt_params(p); + } + + virtual void collect_param_descrs(param_descrs & r) { + insert_max_memory(r); + insert_produce_models(r); + insert_produce_proofs(r); + } + + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, + proof_converter_ref & pc, + expr_dependency_ref & core) { + (*m_imp)(in, result, mc, pc, core); + } + + virtual void cleanup() { + ast_manager & m = m_imp->m(); + imp * d = m_imp; + #pragma omp critical (tactic_cancel) + { + m_imp = 0; + } + dealloc(d); + d = alloc(imp, m, m_params); + #pragma omp critical (tactic_cancel) + { + m_imp = d; + } + } + + virtual void set_cancel(bool f) { + if (m_imp) + m_imp->set_cancel(f); + } +}; + +tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p) { + return alloc(ufbv_rewriter_tactic, m, p); +} diff --git a/src/tactic/ufbv/ufbv_rewriter_tactic.h b/src/tactic/ufbv/ufbv_rewriter_tactic.h new file mode 100644 index 000000000..0afe42bf7 --- /dev/null +++ b/src/tactic/ufbv/ufbv_rewriter_tactic.h @@ -0,0 +1,28 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + ufbv_rewriter_tactic.cpp + +Abstract: + + UFBV Rewriter (demodulator) + +Author: + + Christoph (cwinter) 2012-10-26 + +Notes: + +--*/ +#ifndef _UFBV_REWRITER_TACTIC_H_ +#define _UFBV_REWRITER_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p = params_ref()); + +#endif diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index ac0bff8f0..de8ac875b 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -20,463 +20,43 @@ Notes: #include"simplify_tactic.h" #include"propagate_values_tactic.h" #include"solve_eqs_tactic.h" -#include"simplifier.h" -#include"basic_simplifier_plugin.h" -#include"arith_simplifier_plugin.h" -#include"bv_simplifier_plugin.h" -#include"macro_manager.h" -#include"macro_finder.h" -#include"quasi_macros.h" -#include"ufbv_rewriter.h" -#include"extension_model_converter.h" #include"distribute_forall_tactic.h" #include"der_tactic.h" #include"reduce_args_tactic.h" #include"smt_tactic.h" -#include"ufbv_tactic.h" #include"nnf_tactic.h" +#include"macro_finder_tactic.h" +#include"ufbv_rewriter_tactic.h" +#include"quasi_macros_tactic.h" +#include"ufbv_tactic.h" -class macro_finder_tactic : public tactic { - - struct imp { - ast_manager & m_manager; - bool m_cancel; - bool m_elim_and; - - imp(ast_manager & m, params_ref const & p) : m_manager(m),m_elim_and(false),m_cancel(false) { - updt_params(p); - } - - ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { - m_cancel = f; - } - - void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - SASSERT(g->is_well_sorted()); - mc = 0; pc = 0; core = 0; - tactic_report report("macro-finder", *g); - fail_if_unsat_core_generation("macro-finder", g); - - bool produce_proofs = g->proofs_enabled(); - bool produce_models = g->models_enabled(); - - simplifier simp(m_manager); - basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager); - bsimp->set_eliminate_and(m_elim_and); - simp.register_plugin(bsimp); - arith_simplifier_params a_params; - arith_simplifier_plugin * asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, a_params); - simp.register_plugin(asimp); - bv_simplifier_params bv_params; - bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params); - simp.register_plugin(bvsimp); - - macro_manager mm(m_manager, simp); - macro_finder mf(m_manager, mm); - - expr_ref_vector forms(m_manager), new_forms(m_manager); - proof_ref_vector proofs(m_manager), new_proofs(m_manager); - unsigned size = g->size(); - for (unsigned idx = 0; idx < size; idx++) { - forms.push_back(g->form(idx)); - proofs.push_back(g->pr(idx)); - } - - mf(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); - - unsigned i = 0; - for (; i < g->size(); i++) - g->update(i, new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0); - - for (; i < new_forms.size(); i++) - g->assert_expr(new_forms.get(i), new_proofs.get(i), 0); - - 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()); - func_decl * f = mm.get_macro_interpretation(i, f_interp); - evmc->insert(f, f_interp); - } - mc = evmc; - - g->inc_depth(); - result.push_back(g.get()); - TRACE("macro-finder", g->display(tout);); - SASSERT(g->is_well_sorted()); - } - - void updt_params(params_ref const & p) { - m_elim_and = p.get_bool(":elim-and", false); - } - }; - - imp * m_imp; - params_ref m_params; -public: - macro_finder_tactic(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); - } - - virtual tactic * translate(ast_manager & m) { - return alloc(macro_finder_tactic, m, m_params); - } - - virtual ~macro_finder_tactic() { - dealloc(m_imp); - } - - virtual void updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); - } - - virtual void collect_param_descrs(param_descrs & r) { - insert_max_memory(r); - insert_produce_models(r); - insert_produce_proofs(r); - r.insert(":elim-and", CPK_BOOL, "(default: false) eliminate conjunctions during (internal) calls to the simplifier."); - } - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - (*m_imp)(in, result, mc, pc, core); - } - - virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; - #pragma omp critical (tactic_cancel) - { - m_imp = 0; - } - dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } - } - - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } -}; - -tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p) { - return alloc(macro_finder_tactic, m, p); -} - -class ufbv_rewriter_tactic : public tactic { - - struct imp { - ast_manager & m_manager; - bool m_cancel; - - imp(ast_manager & m, params_ref const & p) : m_manager(m),m_cancel(false) { - updt_params(p); - } - - ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { - m_cancel = f; - } - - void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - SASSERT(g->is_well_sorted()); - mc = 0; pc = 0; core = 0; - tactic_report report("ufbv-rewriter", *g); - fail_if_unsat_core_generation("ufbv-rewriter", g); - - bool produce_proofs = g->proofs_enabled(); - bool produce_models = g->models_enabled(); - - basic_simplifier_plugin bsimp(m_manager); - bsimp.set_eliminate_and(true); - ufbv_rewriter dem(m_manager, bsimp); - - expr_ref_vector forms(m_manager), new_forms(m_manager); - proof_ref_vector proofs(m_manager), new_proofs(m_manager); - - unsigned size = g->size(); - for (unsigned i = 0; i < size; i++) { - forms.push_back(g->form(i)); - proofs.push_back(g->pr(i)); - } - - dem(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); - - unsigned i = 0; - for (; i < g->size(); i++) - g->update(i, new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, g->dep(i)); - - for (; i < new_forms.size(); i++) - g->assert_expr(new_forms.get(i), new_proofs.get(i), 0); - - mc = 0; // CMW: Remark: The demodulator could potentially remove all references to a variable. - - g->inc_depth(); - result.push_back(g.get()); - TRACE("ufbv-rewriter", g->display(tout);); - SASSERT(g->is_well_sorted()); - } - - void updt_params(params_ref const & p) { - } - }; - - imp * m_imp; - params_ref m_params; - -public: - ufbv_rewriter_tactic(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); - } - - virtual tactic * translate(ast_manager & m) { - return alloc(ufbv_rewriter_tactic, m, m_params); - } - - virtual ~ufbv_rewriter_tactic() { - dealloc(m_imp); - } - - virtual void updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); - } - - virtual void collect_param_descrs(param_descrs & r) { - insert_max_memory(r); - insert_produce_models(r); - insert_produce_proofs(r); - } - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - (*m_imp)(in, result, mc, pc, core); - } - - virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; - #pragma omp critical (tactic_cancel) - { - m_imp = 0; - } - dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } - } - - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } -}; - -tactic * mk_ufbv_rewriter_tactic(ast_manager & m, params_ref const & p) { - return alloc(ufbv_rewriter_tactic, m, p); -} tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) { return repeat(and_then(mk_der_tactic(m), mk_simplify_tactic(m, p))); } -class quasi_macros_tactic : public tactic { - - struct imp { - ast_manager & m_manager; - bool m_cancel; - - imp(ast_manager & m, params_ref const & p) : m_manager(m),m_cancel(false) { - updt_params(p); - } - - ast_manager & m() const { return m_manager; } - - void set_cancel(bool f) { - m_cancel = f; - } - - void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - SASSERT(g->is_well_sorted()); - mc = 0; pc = 0; core = 0; - tactic_report report("quasi-macros", *g); - fail_if_unsat_core_generation("quasi-macros", g); - - bool produce_proofs = g->proofs_enabled(); - bool produce_models = g->models_enabled(); - - simplifier simp(m_manager); - basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager); - bsimp->set_eliminate_and(true); - simp.register_plugin(bsimp); - arith_simplifier_params a_params; - arith_simplifier_plugin * asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, a_params); - simp.register_plugin(asimp); - bv_simplifier_params bv_params; - bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params); - simp.register_plugin(bvsimp); - - macro_manager mm(m_manager, simp); - quasi_macros qm(m_manager, mm, *bsimp, simp); - bool more = true; - - expr_ref_vector forms(m_manager), new_forms(m_manager); - proof_ref_vector proofs(m_manager), new_proofs(m_manager); - - unsigned size = g->size(); - for (unsigned i = 0; i < size; i++) { - forms.push_back(g->form(i)); - proofs.push_back(g->pr(i)); - } - - while (more) { // CMW: use repeat(...) ? - if (m_cancel) - throw tactic_exception(TACTIC_CANCELED_MSG); - - new_forms.reset(); - new_proofs.reset(); - more = qm(forms.size(), forms.c_ptr(), proofs.c_ptr(), new_forms, new_proofs); - forms.swap(new_forms); - proofs.swap(new_proofs); - } - - unsigned i = 0; - for (; i < g->size(); i++) - g->update(i, new_forms.get(i), produce_proofs ? new_proofs.get(i) : 0, 0); - - for (; i < new_forms.size(); i++) - g->assert_expr(new_forms.get(i), new_proofs.get(i), 0); - - 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()); - func_decl * f = mm.get_macro_interpretation(i, f_interp); - evmc->insert(f, f_interp); - } - mc = evmc; - - g->inc_depth(); - result.push_back(g.get()); - TRACE("quasi-macros", g->display(tout);); - SASSERT(g->is_well_sorted()); - } - - void updt_params(params_ref const & p) { - } - }; - - imp * m_imp; - params_ref m_params; - -public: - quasi_macros_tactic(ast_manager & m, params_ref const & p): - m_params(p) { - m_imp = alloc(imp, m, p); - } - - virtual tactic * translate(ast_manager & m) { - return alloc(quasi_macros_tactic, m, m_params); - } - - virtual ~quasi_macros_tactic() { - dealloc(m_imp); - } - - virtual void updt_params(params_ref const & p) { - m_params = p; - m_imp->updt_params(p); - } - - virtual void collect_param_descrs(param_descrs & r) { - insert_max_memory(r); - insert_produce_models(r); - insert_produce_proofs(r); - } - - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - (*m_imp)(in, result, mc, pc, core); - } - - virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = m_imp; - #pragma omp critical (tactic_cancel) - { - m_imp = 0; - } - dealloc(d); - d = alloc(imp, m, m_params); - #pragma omp critical (tactic_cancel) - { - m_imp = d; - } - } - - virtual void set_cancel(bool f) { - if (m_imp) - m_imp->set_cancel(f); - } -}; - -tactic * mk_quasi_macros_tactic(ast_manager & m, params_ref const & p) { - return alloc(quasi_macros_tactic, m, p); -} - tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { - params_ref elim_and_p; - elim_and_p.set_bool(":elim-and", true); + params_ref no_elim_and(p); + no_elim_and.set_bool(":elim-and", false); return and_then( + mk_trace_tactic("ufbv_pre"), and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), - and_then(mk_macro_finder_tactic(m, elim_and_p), - mk_macro_finder_tactic(m, p), mk_simplify_tactic(m, p)), - and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), - mk_simplify_tactic(m, elim_and_p), + and_then(using_params(mk_macro_finder_tactic(m, no_elim_and), no_elim_and), + mk_simplify_tactic(m, p)), + and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), + mk_elim_and_tactic(m, p), mk_solve_eqs_tactic(m, p), and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), and_then(mk_distribute_forall_tactic(m, p), mk_simplify_tactic(m, p))), - and_then( and_then(mk_reduce_args_tactic(m, p), mk_simplify_tactic(m, p)), - and_then(mk_macro_finder_tactic(m, elim_and_p), mk_simplify_tactic(m, p)), - and_then(mk_ufbv_rewriter_tactic(m, p), mk_simplify_tactic(m, p)), - and_then(mk_quasi_macros_tactic(m, p), mk_simplify_tactic(m, p)), - and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), - mk_simplify_tactic(m, p))); + and_then(and_then(mk_reduce_args_tactic(m, p), mk_simplify_tactic(m, p)), + and_then(mk_macro_finder_tactic(m, p), mk_simplify_tactic(m, p)), + and_then(mk_ufbv_rewriter_tactic(m, p), mk_simplify_tactic(m, p)), + and_then(mk_quasi_macros_tactic(m, p), mk_simplify_tactic(m, p)), + and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), + mk_simplify_tactic(m, p)), + mk_trace_tactic("ufbv_post")); } tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) { diff --git a/src/tactic/ufbv/ufbv_tactic.h b/src/tactic/ufbv/ufbv_tactic.h index 939185491..e642ecda7 100644 --- a/src/tactic/ufbv/ufbv_tactic.h +++ b/src/tactic/ufbv/ufbv_tactic.h @@ -23,9 +23,10 @@ Notes: class ast_manager; class tactic; -tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p); +tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p = params_ref()); + +tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p = params_ref()); -tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p); /* ADD_TACTIC("bv", "builtin strategy for solving BV problems (with quantifiers).", "mk_ufbv_tactic(m, p)") ADD_TACTIC("ufbv", "builtin strategy for solving UFBV problems (with quantifiers).", "mk_ufbv_tactic(m, p)")