Adding a probe for estimating the number of Ackermann congruence lemas.

src/tactic/ackr/ackr_bound_probe.cpp

@@ -0,0 +1,78 @@
+/*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  ackr_bound_probe.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+--*/
+#include"ackr_helper.h"
+#include"ackr_bound_probe.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.
+ */
+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;
+
+        proc(ast_manager & m) : m_m(m), m_ackr_helper(m) { }
+
+        ~proc() {
+            fun2terms_map::iterator it = m_fun2terms.begin();
+            const fun2terms_map::iterator end = m_fun2terms.end();
+            for (; it != end; ++it) dealloc(it->get_value());
+        }
+
+        void operator()(quantifier *) {}
+        void operator()(var *) {}
+        void operator()(app * a) {
+            if (a->get_num_args() == 0) return;
+            if (!m_ackr_helper.should_ackermannize(a)) return;
+            func_decl* const fd = a->get_decl();
+            app_set* ts = 0;
+            if (!m_fun2terms.find(fd, ts)) {
+                ts = alloc(app_set);
+                m_fun2terms.insert(fd, ts);
+            }
+            ts->insert(a);
+        }
+    };
+
+public:
+    ackr_bound_probe() {}
+
+    virtual result operator()(goal const & g) {
+        proc p(g.m());
+        unsigned sz = g.size();
+        expr_fast_mark1 visited;
+        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) total += n_choose_2(it->m_value->size());
+        return result(total);
+    }
+
+    inline static unsigned n_choose_2(unsigned n) { return n & 1 ? (n * (n >> 1)) : (n >> 1) * (n - 1); }
+};
+
+probe * mk_ackr_bound_probe() {
+    return alloc(ackr_bound_probe);
+}

src/tactic/ackr/ackr_bound_probe.h

@@ -0,0 +1,26 @@
+ /*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  ackr_bound_probe.h
+
+ Abstract:
+
+ A probe to give an upper bound of Ackermann congruence lemmas that a formula might generate.
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+ --*/
+#ifndef ACKR_BOUND_PROBE_H_15037
+#define ACKR_BOUND_PROBE_H_15037
+#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()")
+*/
+#endif /* ACKR_BOUND_PROBE_H_15037 */

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -29,6 +29,7 @@ Notes:
 #include"aig_tactic.h"
 #include"sat_tactic.h"
 #include"ackermannize_tactic.h"
+#include"ackr_bound_probe.h"
 
 #define MEMLIMIT 300
 
@@ -68,7 +69,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_tactic(m,p)
+            when(mk_lt(mk_ackr_bound_probe(), mk_const_probe(static_cast<double>(100))),  mk_ackermannize_tactic(m,p))
             );
 }