refactoring

src/tactic/ackr/ackermannize_bv_model_converter.cpp

@@ -0,0 +1,22 @@
+/*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  ackermannize_bv_model_converter.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+--*/
+#include"ackr_model_converter.h"
+#include"ackermannize_bv_model_converter.h"
+
+model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info) {
+ return mk_ackr_model_converter(m, info);
+}

src/tactic/ackr/ackermannize_bv_model_converter.h

@@ -0,0 +1,25 @@
+ /*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  ackermannize_bv_model_converter.h
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+ --*/
+#ifndef ACKERMANNIZE_BV_MODEL_CONVERTER_H_
+#define ACKERMANNIZE_BV_MODEL_CONVERTER_H_
+
+#include"model_converter.h"
+#include"ackr_info.h"
+
+model_converter * mk_ackermannize_bv_model_converter(ast_manager & m, const ackr_info_ref& info);
+
+#endif /* ACKERMANNIZE_BV_MODEL_CONVERTER_H_ */

src/tactic/ackr/ackermannize_bv_tactic.cpp

@@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation
 
 Module Name:
 
-ackermannize_tactic.cpp
+ackermannize_bv_tactic.cpp
 
 Abstract:
 
@@ -13,22 +13,24 @@ Mikolas Janota
 
 Revision History:
 --*/
+#include"ackermannize_bv_tactic.h"
 #include"tactical.h"
 #include"lackr.h"
 #include"ackr_params.hpp"
-#include"ackr_model_converter.h"
 #include"model_smt2_pp.h"
 #include"ackr_bound_probe.h"
-#include"ackr_tactics_params.hpp"
+#include"ackermannize_bv_tactic_params.hpp"
+#include"ackermannize_bv_model_converter.h"
 
-class ackermannize_tactic : public tactic {
+
+class ackermannize_bv_tactic : public tactic {
 public:
-    ackermannize_tactic(ast_manager& m, params_ref const& p)
+    ackermannize_bv_tactic(ast_manager& m, params_ref const& p)
         : m_m(m)
         , m_p(p)
     {}
 
-    virtual ~ackermannize_tactic() { }
+    virtual ~ackermannize_bv_tactic() { }
 
     virtual void operator()(goal_ref const & g,
         goal_ref_buffer & result,
@@ -48,11 +50,19 @@ public:
         flas.reset();
         // mk result
         goal_ref resg(alloc(goal, *g, true));
-        imp->mk_ackermann(resg);
+        const bool success = imp->mk_ackermann(resg, m_lemma_limit);
+        if (!success) { // Just pass on the input unchanged
+            result.reset();
+            result.push_back(g.get());
+            mc = 0;
+            pc = 0;
+            core = 0;
+            return;
+        }
         result.push_back(resg.get());
         // report model
         if (g->models_enabled()) {
-            mc = mk_ackr_model_converter(m, imp->get_info());
+            mc = mk_ackermannize_bv_model_converter(m, imp->get_info());
         }
 
 		resg->inc_depth();
@@ -60,6 +70,12 @@ public:
 		SASSERT(resg->is_well_sorted());
     }
 
+
+    void updt_params(params_ref const & _p) {
+        ackermannize_bv_tactic_params p(_p);
+        m_lemma_limit = p.div0_ackermann_limit();
+    }
+
     virtual void collect_statistics(statistics & st) const {
         st.update("ackr-constraints", m_st.m_ackrs_sz);
     }
@@ -69,26 +85,15 @@ public:
     virtual void cleanup() { }
 
     virtual tactic* translate(ast_manager& m) {
-        return alloc(ackermannize_tactic, m, m_p);
+        return alloc(ackermannize_bv_tactic, m, m_p);
     }
 private:
     ast_manager&                         m_m;
     params_ref                           m_p;
     lackr_stats                          m_st;
+    double                               m_lemma_limit;
 };
 
-tactic * mk_ackermannize_tactic(ast_manager & m, params_ref const & p) {
-    return alloc(ackermannize_tactic, m, p);
+tactic * mk_ackermannize_bv_tactic(ast_manager & m, params_ref const & p) {
+    return alloc(ackermannize_bv_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_bv_tactic.h

@@ -0,0 +1,28 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ackermannize_bv_tactic.h
+
+Abstract:
+
+Author:
+
+Mikolas Janota
+
+Revision History:
+--*/
+
+#ifndef _ACKERMANNIZE_TACTIC_H_
+#define _ACKERMANNIZE_TACTIC_H_
+#include"tactical.h"
+
+tactic * mk_ackermannize_bv_tactic(ast_manager & m, params_ref const & p);
+
+/*
+  ADD_TACTIC("ackermannize_bv", "A tactic for performing full Ackermannization on bv instances.", "mk_ackermannize_bv_tactic(m, p)")
+*/
+
+#endif
+

src/tactic/ackr/ackermannize_bv_tactic_params.pyg

@@ -0,0 +1,8 @@
+def_module_params(module_name='rewriter',
+                  class_name='ackermannize_bv_tactic_params',
+                  export=True,
+                  params=(
+                          ("div0_ackermann_limit", UINT, 1000, "a bound for number of congruence Ackermann lemmas for div0 modelling"),
+                          )
+                  )
+

src/tactic/ackr/ackermannize_tactic.h

@@ -1,30 +0,0 @@
-/*++
-Copyright (c) 2016 Microsoft Corporation
-
-Module Name:
-
-ackermannize_tactic.h
-
-Abstract:
-
-Author:
-
-Mikolas Janota
-
-Revision History:
---*/
-
-#ifndef _ACKERMANNIZE_TACTIC_H_
-#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_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/ackr_bound_probe.cpp

@@ -18,18 +18,18 @@
 #include"ackr_bound_probe.h"
 #include"ast_smt2_pp.h"
 
-/** \brief
- * For each function f, calculate the number of its occurrences o_f and compute "o_f choose 2".
- * The probe then sums up these for all functions.
- * This upper bound might be crude because some congruence lemmas trivially simplify to true.
- */
+/*
+  For each function f, calculate the number of its occurrences o_f and compute "o_f choose 2".
+  The probe then sums up these for all functions.
+  This upper bound might be crude because some congruence lemmas trivially simplify to true.
+*/
 class ackr_bound_probe : public probe {
     struct proc {
-        typedef obj_hashtable<app>           app_set;
-        typedef obj_map<func_decl, app_set*> fun2terms_map;
-        ast_manager &            m_m;
-        fun2terms_map            m_fun2terms; // a map from functions to occurrences
-        ackr_helper              m_ackr_helper;
+        typedef ackr_helper::fun2terms_map fun2terms_map;
+        typedef ackr_helper::app_set       app_set;
+        ast_manager&                 m_m;
+        fun2terms_map                m_fun2terms; // a map from functions to occurrences
+        ackr_helper                  m_ackr_helper;
 
         proc(ast_manager & m) : m_m(m), m_ackr_helper(m) { }
 
@@ -64,15 +64,7 @@ public:
         for (unsigned i = 0; i < sz; i++) {
             for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));
         }
-        proc::fun2terms_map::iterator it = p.m_fun2terms.begin();
-        proc::fun2terms_map::iterator end = p.m_fun2terms.end();
-        unsigned total = 0;
-        for (; it != end; ++it) {
-            const unsigned fsz = it->m_value->size();
-            const unsigned n2 = n_choose_2(fsz);
-            TRACE("ackr_bound_probe", tout << mk_ismt2_pp(it->m_key, g.m(), 0) << " #" << fsz << " n_choose_2=" << n2 << std::endl;);
-            total += n2;
-        }
+        const double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms);
         TRACE("ackr_bound_probe", tout << "total=" << total << std::endl;);
         return result(total);
     }

src/tactic/ackr/ackr_bound_probe.h

@@ -15,12 +15,15 @@
 
  Revision History:
  --*/
-#ifndef ACKR_BOUND_PROBE_H_15037
-#define ACKR_BOUND_PROBE_H_15037
+#ifndef ACKR_BOUND_PROBE_H_
+#define ACKR_BOUND_PROBE_H_
+
 #include"probe.h"
+
 probe * mk_ackr_bound_probe();
 
 /*
-ADD_PROBE("ackr-bound-probe", "A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.", "mk_ackr_bound_probe()")
+  ADD_PROBE("ackr-bound-probe", "A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.", "mk_ackr_bound_probe()")
 */
-#endif /* ACKR_BOUND_PROBE_H_15037 */
+
+#endif /* ACKR_BOUND_PROBE_H_ */

src/tactic/ackr/ackr_helper.cpp

@@ -0,0 +1,30 @@
+/*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  ackr_helper.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota (MikolasJanota)
+
+ Revision History:
+--*/
+#include"ackr_helper.h"
+
+
+double ackr_helper::calculate_lemma_bound(ackr_helper::fun2terms_map& occurrences) {
+    fun2terms_map::iterator it = occurrences.begin();
+    const fun2terms_map::iterator end = occurrences.end();
+    double total = 0;
+    for (; it != end; ++it) {
+        const unsigned fsz = it->m_value->size();
+        const double n2 = n_choose_2_chk(fsz);
+        total += n2;
+    }
+    return total;
+}

src/tactic/ackr/ackr_helper.h

@@ -14,12 +14,24 @@
 
  Revision History:
  --*/
-#ifndef ACKR_HELPER_H_6475
-#define ACKR_HELPER_H_6475
+#ifndef ACKR_HELPER_H_
+#define ACKR_HELPER_H_
+
 #include"bv_decl_plugin.h"
+
 class ackr_helper {
     public:
+        typedef obj_hashtable<app>           app_set;
+        typedef obj_map<func_decl, app_set*> fun2terms_map;
+
         ackr_helper(ast_manager& m) : m_bvutil(m) {}
+
+        /**
+        \brief  Determines if a given function should be Ackermannized.
+
+         This includes all uninterpreted functions but also "special" functions, e.g. OP_BSMOD0,
+         which are not marked as uninterpreted but effectively are.
+        */
         inline bool should_ackermannize(app const * a) const {
             if (a->get_family_id() == m_bvutil.get_family_id()) {
                 switch (a->get_decl_kind()) {
@@ -36,7 +48,20 @@ class ackr_helper {
             return (is_uninterp(a));
         }
 
-        bv_util& bvutil() { return m_bvutil; }
+        inline bv_util& bvutil() { return m_bvutil; }
+
+        /**
+        \brief Calculates an upper bound for congruence lemmas given a map of function of occurrences.
+        */
+        static double calculate_lemma_bound(fun2terms_map& occurrences);
+
+        /** \brief Calculate n choose 2. **/
+        inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); }
+
+        inline static double n_choose_2_chk(unsigned n) {
+            SASSERT(std::numeric_limits<unsigned>().max() & 32);
+            return n & (1 << 16) ? n_choose_2(n) : std::numeric_limits<double>().infinity();;
+        }
     private:
         bv_util                              m_bvutil;
 };

src/tactic/ackr/ackr_info.h

@@ -13,8 +13,9 @@ Mikolas Janota
 
 Revision History:
 --*/
-#ifndef ACKR_INFO_H_12278
-#define ACKR_INFO_H_12278
+#ifndef ACKR_INFO_H_
+#define ACKR_INFO_H_
+
 #include"obj_hashtable.h"
 #include"ast.h"
 #include"ref.h"
@@ -104,4 +105,5 @@ class ackr_info {
 };
 
 typedef ref<ackr_info> ackr_info_ref;
-#endif /* ACKR_INFO_H_12278 */
+
+#endif /* ACKR_INFO_H_ */

src/tactic/ackr/ackr_model_converter.h

@@ -13,11 +13,12 @@ Mikolas Janota
 
 Revision History:
 --*/
-#ifndef ACKR_MODEL_CONVERTER_H_5814
-#define ACKR_MODEL_CONVERTER_H_5814
+#ifndef ACKR_MODEL_CONVERTER_H_
+#define ACKR_MODEL_CONVERTER_H_
+
 #include"model_converter.h"
 #include"ackr_info.h"
 
 model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);
 model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info);
-#endif /* LACKR_MODEL_CONVERTER_H_5814 */
+#endif /* LACKR_MODEL_CONVERTER_H_ */

src/tactic/ackr/lackr.cpp

@@ -14,16 +14,15 @@
 
  Revision History:
 --*/
-///////////////
+
 #include"lackr.h"
 #include"ackr_params.hpp"
 #include"tactic.h"
 #include"lackr_model_constructor.h"
 #include"ackr_info.h"
 #include"for_each_expr.h"
-///////////////
 #include"model_smt2_pp.h"
-///////////////
+
 lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas,
     solver * uffree_solver)
     : m_m(m)
@@ -57,11 +56,17 @@ lbool lackr::operator() () {
     return rv;
 }
 
-void lackr::mk_ackermann(/*out*/goal_ref& g) {
+bool lackr::mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound) {
+    if (lemmas_upper_bound <= 0) return false;
     init();
+    if (lemmas_upper_bound != std::numeric_limits<double>::infinity()) {
+        const double lemmas_bound = ackr_helper::calculate_lemma_bound(m_fun2terms);
+        if (lemmas_bound > lemmas_upper_bound) return false;
+    }
     eager_enc();
     for (unsigned i = 0; i < m_abstr.size(); ++i) g->assert_expr(m_abstr.get(i));
     for (unsigned i = 0; i < m_ackrs.size(); ++i) g->assert_expr(m_ackrs.get(i));
+    return true;
 }
 
 void lackr::init() {

src/tactic/ackr/lackr.h

@@ -14,9 +14,9 @@
 
  Revision History:
  --*/
-#ifndef LACKR_H_15079
-#define LACKR_H_15079
-///////////////
+#ifndef LACKR_H_
+#define LACKR_H_
+
 #include"ackr_info.h"
 #include"ackr_helper.h"
 #include"ackr_params.hpp"
@@ -58,11 +58,13 @@ class lackr {
 
 
         /** \brief
-        * Converts function occurrences to constants and encodes all congruence ackermann lemmas.
-        * This guarantees a equisatisfiability with the input formula. It has a worst-case quadratic blowup.
-        **/
-        void mk_ackermann(/*out*/goal_ref& g);
+          Converts function occurrences to constants and encodes all congruence ackermann lemmas.
 
+          This procedure guarantees a equisatisfiability with the input formula and it has a worst-case quadratic blowup.
+          Before ackermannization an upper bound on congruence lemmas is computed and tested against \p lemmas_upper_bound.
+          If this bound is exceeded, the function returns false, it returns true otherwise.
+        **/
+        bool mk_ackermann(/*out*/goal_ref& g, double lemmas_upper_bound);
 
         //
         // getters
@@ -80,8 +82,8 @@ class lackr {
             cooperate("lackr");
         }
     private:
-        typedef obj_hashtable<app>           app_set;
-        typedef obj_map<func_decl, app_set*> fun2terms_map;
+        typedef ackr_helper::fun2terms_map fun2terms_map;
+        typedef ackr_helper::app_set       app_set;
         ast_manager&                         m_m;
         params_ref                           m_p;
         expr_ref_vector                      m_formulas;
@@ -122,4 +124,4 @@ class lackr {
         //
         void collect_terms();
 };
-#endif /* LACKR_H_15079 */
+#endif /* LACKR_H_ */

src/tactic/ackr/lackr_model_constructor.h

@@ -15,8 +15,9 @@
 
  Revision History:
  --*/
-#ifndef LACKR_MODEL_CONSTRUCTOR_H_626
-#define LACKR_MODEL_CONSTRUCTOR_H_626
+#ifndef LACKR_MODEL_CONSTRUCTOR_H_
+#define LACKR_MODEL_CONSTRUCTOR_H_
+
 #include"ast.h"
 #include"ackr_info.h"
 #include"ackr_helper.h"
@@ -57,4 +58,4 @@ class lackr_model_constructor {
 };
 
 typedef ref<lackr_model_constructor> lackr_model_constructor_ref;
-#endif /* MODEL_CONSTRUCTOR_H_626 */
+#endif /* MODEL_CONSTRUCTOR_H_ */

src/tactic/ackr/lackr_model_converter_lazy.h

@@ -14,10 +14,12 @@
 
  Revision History:
  --*/
-#ifndef LACKR_MODEL_CONVERTER_LAZY_H_14201
-#define LACKR_MODEL_CONVERTER_LAZY_H_14201
+#ifndef LACKR_MODEL_CONVERTER_LAZY_H_
+#define LACKR_MODEL_CONVERTER_LAZY_H_
+
 #include"model_converter.h"
 #include"ackr_info.h"
 
 model_converter * mk_lackr_model_converter_lazy(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model);
-#endif /* LACKR_MODEL_CONVERTER_LAZY_H_14201 */
+
+#endif /* LACKR_MODEL_CONVERTER_LAZY_H_ */

src/tactic/ackr_tactics/ackr_tactics.pyg

@@ -3,7 +3,5 @@ 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/smtlogics/qfbv_tactic.cpp

@@ -28,7 +28,7 @@ Notes:
 #include"bv_size_reduction_tactic.h"
 #include"aig_tactic.h"
 #include"sat_tactic.h"
-#include"ackermannize_tactic.h"
+#include"ackermannize_bv_tactic.h"
 
 #define MEMLIMIT 300
 
@@ -67,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),
-            mk_ackermannize_bounded_tactic(m,p)
+            mk_ackermannize_bv_tactic(m,p)
             );
 }