re-factoring

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);
+        tactic_report report("ackermannize", *g);
-		fail_if_unsat_core_generation("ackermannize", g);
+        fail_if_unsat_core_generation("ackermannize", g);
-		fail_if_proof_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<double>(my_params.div0ackermann());
+    const double ackermannize_limit = static_cast<double>(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);
+}

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

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")
                           ))
 

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);

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

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<double>(my_params.div0ackermann());
-    const double ackermannize_limit = static_cast<double>(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)
             );
 }
 

src/tactic/smtlogics/qfbv_tactic_params.pyg

@@ -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")
-                  ))