diff --git a/lib/asserted_formulas.cpp b/lib/asserted_formulas.cpp index 6f7d8827e..4fb476500 100644 --- a/lib/asserted_formulas.cpp +++ b/lib/asserted_formulas.cpp @@ -44,7 +44,7 @@ Revision History: #include"bit2int.h" #include"qe.h" #include"distribute_forall.h" -#include"demodulator.h" +#include"ufbv_rewriter.h" #include"quasi_macros.h" asserted_formulas::asserted_formulas(ast_manager & m, front_end_params & p): @@ -955,7 +955,7 @@ void asserted_formulas::apply_demodulators() { expr_ref_vector new_exprs(m_manager); proof_ref_vector new_prs(m_manager); unsigned sz = m_asserted_formulas.size(); - demodulator proc(m_manager, *m_bsimp); + ufbv_rewriter proc(m_manager, *m_bsimp); proc(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, m_asserted_formula_prs.c_ptr() + m_asserted_qhead, diff --git a/lib/lib.vcxproj b/lib/lib.vcxproj index 92193faba..42318e413 100644 --- a/lib/lib.vcxproj +++ b/lib/lib.vcxproj @@ -1,4 +1,4 @@ - + @@ -528,7 +528,6 @@ - @@ -919,7 +918,9 @@ + + diff --git a/lib/demodulator.cpp b/lib/ufbv_rewriter.cpp similarity index 94% rename from lib/demodulator.cpp rename to lib/ufbv_rewriter.cpp index 560af99ee..e4ed2ec01 100644 --- a/lib/demodulator.cpp +++ b/lib/ufbv_rewriter.cpp @@ -15,17 +15,18 @@ Author: Revision History: - Christoph Wintersteiger 2010-04-21: Implementation + Christoph M. Wintersteiger (cwinter) 2010-04-21: Implementation + Christoph M. Wintersteiger (cwinter) 2012-10-24: Moved from demodulator.h to ufbv_rewriter.h --*/ #include"ast_pp.h" -#include"demodulator.h" +#include"ufbv_rewriter.h" #include"for_each_expr.h" #include"var_subst.h" #include"uint_set.h" -demodulator::demodulator(ast_manager & m, basic_simplifier_plugin & p): +ufbv_rewriter::ufbv_rewriter(ast_manager & m, basic_simplifier_plugin & p): m_manager(m), m_match_subst(m), m_bsimp(p), @@ -35,7 +36,7 @@ demodulator::demodulator(ast_manager & m, basic_simplifier_plugin & p): m_new_exprs(m) { } -demodulator::~demodulator() { +ufbv_rewriter::~ufbv_rewriter() { reset_dealloc_values(m_fwd_idx); reset_dealloc_values(m_back_idx); for (demodulator2lhs_rhs::iterator it = m_demodulator2lhs_rhs.begin(); it != m_demodulator2lhs_rhs.end(); it++) { @@ -45,7 +46,7 @@ demodulator::~demodulator() { } } -bool demodulator::is_demodulator(expr * e, expr_ref & large, expr_ref & small) const { +bool ufbv_rewriter::is_demodulator(expr * e, expr_ref & large, expr_ref & small) const { if (e->get_kind() == AST_QUANTIFIER) { quantifier * q = to_quantifier(e); if (q->is_forall()) { @@ -121,7 +122,7 @@ public: void operator()(app * n) {} }; -int demodulator::is_subset(expr * e1, expr * e2) const { +int ufbv_rewriter::is_subset(expr * e1, expr * e2) const { uint_set ev1, ev2; if (m_manager.is_value(e1)) @@ -138,7 +139,7 @@ int demodulator::is_subset(expr * e1, expr * e2) const { 0 ; } -int demodulator::is_smaller(expr * e1, expr * e2) const { +int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const { unsigned sz1 = 0, sz2 = 0; // values are always smaller! @@ -202,14 +203,14 @@ public: unsigned get_max(void) { return m_max_var_id; } }; -unsigned demodulator::max_var_id(expr * e) +unsigned ufbv_rewriter::max_var_id(expr * e) { max_var_id_proc proc; for_each_expr(proc, e); return proc.get_max(); } -void demodulator::insert_fwd_idx(expr * large, expr * small, quantifier * demodulator) { +void ufbv_rewriter::insert_fwd_idx(expr * large, expr * small, quantifier * demodulator) { SASSERT(large->get_kind() == AST_APP); SASSERT(demodulator); SASSERT(large && small); @@ -233,7 +234,7 @@ void demodulator::insert_fwd_idx(expr * large, expr * small, quantifier * demodu m_demodulator2lhs_rhs.insert(demodulator, expr_pair(large, small)); } -void demodulator::remove_fwd_idx(func_decl * f, quantifier * demodulator) { +void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) { TRACE("demodulator_fwd", tout << "REMOVE: " << std::hex << (size_t)demodulator << std::endl; ); fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f); @@ -249,7 +250,7 @@ void demodulator::remove_fwd_idx(func_decl * f, quantifier * demodulator) { } } -bool demodulator::check_fwd_idx_consistency(void) { +bool ufbv_rewriter::check_fwd_idx_consistency(void) { for (fwd_idx_map::iterator it = m_fwd_idx.begin(); it != m_fwd_idx.end() ; it++ ) { quantifier_set * set = it->m_value; SASSERT(set); @@ -262,7 +263,7 @@ bool demodulator::check_fwd_idx_consistency(void) { return true; } -void demodulator::show_fwd_idx(std::ostream & out) { +void ufbv_rewriter::show_fwd_idx(std::ostream & out) { for (fwd_idx_map::iterator it = m_fwd_idx.begin(); it != m_fwd_idx.end() ; it++ ) { quantifier_set * set = it->m_value; SASSERT(!set); @@ -280,7 +281,7 @@ void demodulator::show_fwd_idx(std::ostream & out) { } } -bool demodulator::rewrite1(func_decl * f, ptr_vector & m_new_args, expr_ref & np) { +bool ufbv_rewriter::rewrite1(func_decl * f, ptr_vector & m_new_args, expr_ref & np) { fwd_idx_map::iterator it = m_fwd_idx.find_iterator(f); if (it != m_fwd_idx.end()) { TRACE("demodulator_bug", tout << "trying to rewrite: " << f->get_name() << " args:\n"; @@ -312,7 +313,7 @@ bool demodulator::rewrite1(func_decl * f, ptr_vector & m_new_args, expr_re return false; } -bool demodulator::rewrite_visit_children(app * a) { +bool ufbv_rewriter::rewrite_visit_children(app * a) { bool res=true; unsigned j = a->get_num_args(); while (j > 0) { @@ -325,11 +326,11 @@ bool demodulator::rewrite_visit_children(app * a) { return res; } -void demodulator::rewrite_cache(expr * e, expr * new_e, bool done) { +void ufbv_rewriter::rewrite_cache(expr * e, expr * new_e, bool done) { m_rewrite_cache.insert(e, expr_bool_pair(new_e, done)); } -expr * demodulator::rewrite(expr * n) { +expr * ufbv_rewriter::rewrite(expr * n) { if (m_fwd_idx.empty()) return n; @@ -440,7 +441,7 @@ expr * demodulator::rewrite(expr * n) { return r; } -class demodulator::add_back_idx_proc { +class ufbv_rewriter::add_back_idx_proc { ast_manager & m_manager; back_idx_map & m_back_idx; expr * m_expr; @@ -467,7 +468,7 @@ public: } }; -class demodulator::remove_back_idx_proc { +class ufbv_rewriter::remove_back_idx_proc { ast_manager & m_manager; back_idx_map & m_back_idx; expr * m_expr; @@ -489,7 +490,7 @@ public: } }; -void demodulator::reschedule_processed(func_decl * f) { +void ufbv_rewriter::reschedule_processed(func_decl * f) { //use m_back_idx to find all formulas p in m_processed that contains f { back_idx_map::iterator it = m_back_idx.find_iterator(f); if (it != m_back_idx.end()) { @@ -518,7 +519,7 @@ void demodulator::reschedule_processed(func_decl * f) { } } -bool demodulator::can_rewrite(expr * n, expr * lhs) { +bool ufbv_rewriter::can_rewrite(expr * n, expr * lhs) { // this is a quick check, we just traverse d and check if there is an expression in d that is an instance of lhs of n'. // we cannot use the trick used for m_processed, since the main loop would not terminate. @@ -575,7 +576,7 @@ bool demodulator::can_rewrite(expr * n, expr * lhs) { return false; } -void demodulator::reschedule_demodulators(func_decl * f, expr * lhs) { +void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) { // use m_back_idx to find all demodulators d in m_fwd_idx that contains f { //ptr_vector to_remove; @@ -634,7 +635,7 @@ void demodulator::reschedule_demodulators(func_decl * f, expr * lhs) { //} } -void demodulator::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { +void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs) { if (m_manager.proofs_enabled()) { // Let us not waste time with proof production warning_msg("PRE_DEMODULATOR=true is not supported when proofs are enabled."); @@ -734,7 +735,7 @@ void demodulator::operator()(unsigned n, expr * const * exprs, proof * const * p } -demodulator::match_subst::match_subst(ast_manager & m): +ufbv_rewriter::match_subst::match_subst(ast_manager & m): m_manager(m), m_subst(m) { } @@ -764,7 +765,7 @@ struct match_args_aux_proc { void operator()(app * n) {} }; -bool demodulator::match_subst::match_args(app * lhs, expr * const * args) { +bool ufbv_rewriter::match_subst::match_args(app * lhs, expr * const * args) { m_cache.reset(); m_todo.reset(); @@ -880,7 +881,7 @@ bool demodulator::match_subst::match_args(app * lhs, expr * const * args) { } -bool demodulator::match_subst::operator()(app * lhs, expr * rhs, expr * const * args, expr_ref & new_rhs) { +bool ufbv_rewriter::match_subst::operator()(app * lhs, expr * rhs, expr * const * args, expr_ref & new_rhs) { if (match_args(lhs, args)) { if (m_all_args_eq) { // quick success... @@ -894,7 +895,7 @@ bool demodulator::match_subst::operator()(app * lhs, expr * rhs, expr * const * return false; } -bool demodulator::match_subst::operator()(expr * t, expr * i) { +bool ufbv_rewriter::match_subst::operator()(expr * t, expr * i) { m_cache.reset(); m_todo.reset(); if (is_var(t)) diff --git a/lib/demodulator.h b/lib/ufbv_rewriter.h similarity index 97% rename from lib/demodulator.h rename to lib/ufbv_rewriter.h index 1925368e5..036af1793 100644 --- a/lib/demodulator.h +++ b/lib/ufbv_rewriter.h @@ -15,9 +15,11 @@ Author: Revision History: + Christoph M. Wintersteiger (cwinter) 2012-10-24: Moved from demodulator.h to ufbv_rewriter.h + --*/ -#ifndef _DEMODULATOR_H_ -#define _DEMODULATOR_H_ +#ifndef _UFBV_REWRITER_H_ +#define _UFBV_REWRITER_H_ #include"ast.h" #include"substitution.h" @@ -90,7 +92,7 @@ The code in spc_rewriter.* does something like that. We cannot reuse this code d for the superposion engine in Z3, but we can adapt it for our needs in the preprocessor. */ -class demodulator { +class ufbv_rewriter { class rewrite_proc; class add_back_idx_proc; class remove_back_idx_proc; @@ -192,8 +194,8 @@ protected: virtual int is_subset(expr * e1, expr * e2) const; public: - demodulator(ast_manager & m, basic_simplifier_plugin & p); - virtual ~demodulator(); + ufbv_rewriter(ast_manager & m, basic_simplifier_plugin & p); + virtual ~ufbv_rewriter(); void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs); @@ -261,5 +263,5 @@ public: */ }; -#endif /* _DEMODULATOR_H_ */ +#endif /* _UFBV_REWRITER_H_ */ diff --git a/lib/ufbv_strategy.cpp b/lib/ufbv_strategy.cpp index 9b6b41704..70eba8ab9 100644 --- a/lib/ufbv_strategy.cpp +++ b/lib/ufbv_strategy.cpp @@ -23,7 +23,7 @@ Notes: #include"macro_finder.h" #include"arith_simplifier_plugin.h" #include"bv_simplifier_plugin.h" -#include"demodulator.h" +#include"ufbv_rewriter.h" #include"quasi_macros.h" #include"reduce_args.h" #include"ufbv_strategy.h" @@ -206,17 +206,17 @@ as_st * mk_macro_finder(ast_manager & m, params_ref const & p, bool elim_and=fal } -// --- DEMODULATOR STRATEGY +// --- UFBV-Rewriter (demodulator) STRATEGY -class demodulator_st : public assertion_set_strategy { +class ufbv_rewriter_st : public assertion_set_strategy { ast_manager & m; params_ref m_params; bool m_produce_models; bool m_cancel; public: - demodulator_st(ast_manager & m, params_ref const & p = params_ref()) : m(m),m_params(p),m_produce_models(false),m_cancel(false) { } - virtual ~demodulator_st() {} + ufbv_rewriter_st(ast_manager & m, params_ref const & p = params_ref()) : m(m),m_params(p),m_produce_models(false),m_cancel(false) { } + virtual ~ufbv_rewriter_st() {} virtual void updt_params(params_ref const & p) { m_produce_models = p.get_bool(":produce-models", false); @@ -229,10 +229,10 @@ public: virtual void collect_param_descrs(param_descrs & r) { get_param_descrs(r); } virtual void operator()(assertion_set & s, model_converter_ref & mc) { - as_st_report report("demodulator", s); + as_st_report report("ufbv-rewriter", s); basic_simplifier_plugin bsimp(m); bsimp.set_eliminate_and(true); - demodulator dem(m, bsimp); + ufbv_rewriter dem(m, bsimp); expr_ref_vector forms(m), new_forms(m); proof_ref_vector proofs(m), new_proofs(m); @@ -257,8 +257,8 @@ protected: virtual void set_cancel(bool f) { m_cancel = f; } }; -as_st * mk_demodulator(ast_manager & m, params_ref const & p) { - return alloc(demodulator_st, m, p); +as_st * mk_ufbv_rewriter(ast_manager & m, params_ref const & p) { + return alloc(ufbv_rewriter_st, m, p); } @@ -465,7 +465,7 @@ as_st * mk_preprocessor(ast_manager & m, params_ref const & p) { ), and_then( and_then(mk_reduce_args(m, p), mk_simplifier(m, p)), and_then(mk_macro_finder(m, p, true), mk_simplifier(m, p)), - and_then(mk_demodulator(m, p), mk_simplifier(m, p)), + and_then(mk_ufbv_rewriter(m, p), mk_simplifier(m, p)), and_then(mk_quasi_macros(m, p), mk_simplifier(m, p)), and_then(mk_der_fp(m, p), mk_simplifier(m, p)), mk_simplifier(m, p)), diff --git a/lib/ufbv_tactic.cpp b/lib/ufbv_tactic.cpp new file mode 100644 index 000000000..178a5c5d2 --- /dev/null +++ b/lib/ufbv_tactic.cpp @@ -0,0 +1,345 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + ufbv_tactic.cpp + +Abstract: + + General purpose tactic for UFBV benchmarks. + +Author: + + Christoph (cwinter) 2012-10-24 + +Notes: + +--*/ +#include"tactical.h" +#include"simplify_tactic.h" +#include"propagate_values_tactic.h" +#include"nnf.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"elim_var_model_converter.h" +#include"ufbv_rewriter.h" +#include"distribute_forall_tactic.h" +#include"der.h" +#include"smt_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, g->dep(i)); + + 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()); + 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(ast_manager & m, params_ref const & p) { + return repeat(and_then(mk_der_tactic(m), mk_simplify_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); + + return and_then( + 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), + mk_solve_eqs_tactic(m, p), + and_then(mk_der_fp(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(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(m, p), mk_simplify_tactic(m, p)), + and_then(mk_der_fp(m, p), mk_simplify_tactic(m, p)), + mk_simplify_tactic(m, p))); +} + +tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) { + params_ref main_p(p); + main_p.set_bool(":mbqi", true); + main_p.set_uint(":mbqi-max-iterations", -1); + main_p.set_bool(":elim-and", true); + main_p.set_bool(":solver", true); + + params_ref smt_p(p); + smt_p.set_bool(":auto-config", false); + + tactic * t = and_then(repeat(mk_ufbv_preprocessor_tactic(m, main_p), 2), + using_params(mk_smt_tactic(smt_p), main_p)); + + t->updt_params(p); + + return t; +} \ No newline at end of file diff --git a/lib/ufbv_tactic.h b/lib/ufbv_tactic.h new file mode 100644 index 000000000..00499c8a1 --- /dev/null +++ b/lib/ufbv_tactic.h @@ -0,0 +1,30 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + ufbv_tactic.h + +Abstract: + + General purpose tactic for UFBV benchmarks. + +Author: + + Christoph (cwinter) 2012-10-24 + +Notes: + +--*/ +#ifndef _UFBV_TACTIC_H_ +#define _UFBV_TACTIC_H_ + +#include"params.h" +class ast_manager; +class tactic; + +tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p); + +tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p); + +#endif