From bcab9a3600ba6f0a13d51f99e50d128128a4a677 Mon Sep 17 00:00:00 2001 From: mikolas Date: Tue, 2 Feb 2016 15:04:20 +0000 Subject: [PATCH] re-factoring --- src/tactic/ackr/ackermannize_tactic.cpp | 22 +++++++++++++++---- src/tactic/ackr/ackermannize_tactic.h | 4 +++- src/tactic/ackr_tactics/ackr_tactics.pyg | 2 ++ .../ackr_tactics/qfufbv_ackr_tactic.cpp | 4 ++++ src/tactic/ackr_tactics/qfufbv_ackr_tactic.h | 2 +- src/tactic/smtlogics/qfbv_tactic.cpp | 15 +------------ src/tactic/smtlogics/qfbv_tactic_params.pyg | 6 ----- 7 files changed, 29 insertions(+), 26 deletions(-) delete mode 100644 src/tactic/smtlogics/qfbv_tactic_params.pyg diff --git a/src/tactic/ackr/ackermannize_tactic.cpp b/src/tactic/ackr/ackermannize_tactic.cpp index 1345b9415..6f67ff40b 100644 --- a/src/tactic/ackr/ackermannize_tactic.cpp +++ b/src/tactic/ackr/ackermannize_tactic.cpp @@ -18,6 +18,8 @@ Revision History: #include"ackr_params.hpp" #include"ackr_model_converter.h" #include"model_smt2_pp.h" +#include"ackr_bound_probe.h" +#include"ackr_tactics_params.hpp" class ackermannize_tactic : public tactic { public: @@ -35,10 +37,10 @@ public: expr_dependency_ref & core) { mc = 0; ast_manager& m(g->m()); - tactic_report report("ackermannize", *g); - fail_if_unsat_core_generation("ackermannize", g); - fail_if_proof_generation("ackermannize", g); - + tactic_report report("ackermannize", *g); + fail_if_unsat_core_generation("ackermannize", g); + fail_if_proof_generation("ackermannize", g); + expr_ref_vector flas(m); const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); @@ -78,3 +80,15 @@ private: tactic * mk_ackermannize_tactic(ast_manager & m, params_ref const & p) { return alloc(ackermannize_tactic, m, p); } + +tactic * mk_ackermannize_bounded_tactic(ast_manager & m, params_ref const & p) { + ackr_tactics_params my_params(p); + const double should_ackermannize = static_cast(my_params.div0ackermann()); + const double ackermannize_limit = static_cast(my_params.div0_ackermann_limit()); + probe * const should_ackermann_p = mk_and( + mk_const_probe(should_ackermannize), + mk_lt(mk_ackr_bound_probe(), mk_const_probe(ackermannize_limit)) + ); + tactic * const actual_tactic = mk_ackermannize_tactic(m, p); + return when(should_ackermann_p, actual_tactic); +} \ No newline at end of file diff --git a/src/tactic/ackr/ackermannize_tactic.h b/src/tactic/ackr/ackermannize_tactic.h index 07c68d5e5..18ea20683 100644 --- a/src/tactic/ackr/ackermannize_tactic.h +++ b/src/tactic/ackr/ackermannize_tactic.h @@ -18,10 +18,12 @@ Revision History: #define _ACKERMANNIZE_TACTIC_H #include"tactical.h" +tactic * mk_ackermannize_bounded_tactic(ast_manager & m, params_ref const & p); tactic * mk_ackermannize_tactic(ast_manager & m, params_ref const & p); /* -ADD_TACTIC("ackermannize", "A tactic for performing full Ackermannization.", "mk_ackermannize_tactic(m, p)") + ADD_TACTIC("ackermannize", "A tactic for performing full Ackermannization.", "mk_ackermannize_tactic(m, p)") + ADD_TACTIC("ackermannize_bounded", "A tactic for performing full Ackermannization where Ackermannization is invoked only if bounds given by the parameters of the tactic are not exceeded.", "mk_ackermannize_bounded_tactic(m, p)") */ #endif diff --git a/src/tactic/ackr_tactics/ackr_tactics.pyg b/src/tactic/ackr_tactics/ackr_tactics.pyg index 8f391bc91..1fccd1ad4 100644 --- a/src/tactic/ackr_tactics/ackr_tactics.pyg +++ b/src/tactic/ackr_tactics/ackr_tactics.pyg @@ -3,5 +3,7 @@ def_module_params('ackr_tactics', export=True, params=( ('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'), + ('div0ackermann', BOOL, False, "if true, then try to Ackermannize div etc functions."), + ("div0_ackermann_limit", UINT, 1000, "a bound for number of congruence Ackermann lemmas") )) diff --git a/src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp index 4eb3792ff..a8a76e698 100644 --- a/src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp +++ b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp @@ -55,6 +55,10 @@ public: expr_dependency_ref & core) { mc = 0; ast_manager& m(g->m()); + tactic_report report("qfufbv_ackr", *g); + fail_if_unsat_core_generation("qfufbv_ackr", g); + fail_if_proof_generation("qfufbv_ackr", g); + TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n");); // running implementation expr_ref_vector flas(m); diff --git a/src/tactic/ackr_tactics/qfufbv_ackr_tactic.h b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.h index 699500be6..57b32bf75 100644 --- a/src/tactic/ackr_tactics/qfufbv_ackr_tactic.h +++ b/src/tactic/ackr_tactics/qfufbv_ackr_tactic.h @@ -21,7 +21,7 @@ Revision History: tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p); /* -ADD_TACTIC("qfufbv_ackr", "A tactic for solving QF_UFBV based on Ackermannization.", "mk_qfufbv_ackr_tactic(m, p)") + ADD_TACTIC("qfufbv_ackr", "A tactic for solving QF_UFBV based on Ackermannization.", "mk_qfufbv_ackr_tactic(m, p)") */ #endif diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index fa188dffd..207115455 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -29,8 +29,6 @@ Notes: #include"aig_tactic.h" #include"sat_tactic.h" #include"ackermannize_tactic.h" -#include"ackr_bound_probe.h" -#include"qfbv_tactic_params.hpp" #define MEMLIMIT 300 @@ -49,21 +47,10 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { simp2_p.set_bool("flat", true); // required by som simp2_p.set_bool("hoist_mul", false); // required by som - - qfbv_tactic_params my_params(p); - params_ref hoist_p; hoist_p.set_bool("hoist_mul", true); hoist_p.set_bool("som", false); - const double should_ackermannize = static_cast(my_params.div0ackermann()); - const double ackermannize_limit = static_cast(my_params.div0_ackermann_limit()); - probe * const should_ackermann_p = mk_and( - mk_const_probe(should_ackermannize), - mk_lt(mk_ackr_bound_probe(), mk_const_probe(ackermannize_limit)) - ); - - return and_then( mk_simplify_tactic(m), @@ -80,7 +67,7 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { // using_params(mk_simplify_tactic(m), hoist_p), mk_max_bv_sharing_tactic(m), - when(should_ackermann_p, mk_ackermannize_tactic(m,p)) + mk_ackermannize_bounded_tactic(m,p) ); } diff --git a/src/tactic/smtlogics/qfbv_tactic_params.pyg b/src/tactic/smtlogics/qfbv_tactic_params.pyg deleted file mode 100644 index 8dccfc650..000000000 --- a/src/tactic/smtlogics/qfbv_tactic_params.pyg +++ /dev/null @@ -1,6 +0,0 @@ -def_module_params(class_name='qfbv_tactic_params', - module_name="smtlogic_tactic", - export=True, - params=(('div0ackermann', BOOL, False, "if true, then try to Ackermannize div etc functions."), - ("div0_ackermann_limit", UINT, 1000, "a bound for number of congregants Ackerman lemmas") - ))