enhance ackermannize for constant arguments

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ackermannization/ackermannize_bv_tactic.cpp

@@ -25,7 +25,9 @@ class ackermannize_bv_tactic : public tactic {
 public:
     ackermannize_bv_tactic(ast_manager& m, params_ref const& p)
         : m(m), m_p(p)
-    {}
+    {
+        updt_params(p);
+    }
 
     ~ackermannize_bv_tactic() override { }
 

src/ackermannization/ackr_bound_probe.cpp

@@ -53,29 +53,9 @@ class ackr_bound_probe : public probe {
 
         void operator()(quantifier *) {}
         void operator()(var *) {}
-        void operator()(app * a) {
-            if (a->get_num_args() == 0) return;
+        void operator()(app * a) { 
             m_ackr_helper.mark_non_select(a, m_non_select);
-            app_set* ts = nullptr;
-            if (m_ackr_helper.is_select(a)) {
-                app* sel = to_app(a->get_arg(0));
-                if (!m_sel2terms.find(sel, ts)) {
-                    ts = alloc(app_set);
-                    m_sel2terms.insert(sel, ts);
-                }
-            }
-            else if (m_ackr_helper.is_uninterp_fn(a)) {
-                func_decl* const fd = a->get_decl();
-                if (!m_fun2terms.find(fd, ts)) {
-                    ts = alloc(app_set);
-                    m_fun2terms.insert(fd, ts);
-                }
-            }
-            else {
-                return;
-            }
-
-            ts->insert(a);
+            m_ackr_helper.insert(m_fun2terms, m_sel2terms, a); 
         }
     };
 

src/ackermannization/ackr_helper.cpp

@@ -19,10 +19,12 @@
 double ackr_helper::calculate_lemma_bound(fun2terms_map const& occs1, sel2terms_map const& occs2) {
     double total = 0;
     for (auto const& kv : occs1) {
-        total += n_choose_2_chk(kv.m_value->size());
+        total += n_choose_2_chk(kv.m_value->var_args.size());
+        total += kv.m_value->const_args.size() * kv.m_value->var_args.size();
     }
     for (auto const& kv : occs2) {
-        total += n_choose_2_chk(kv.m_value->size());
+        total += n_choose_2_chk(kv.m_value->var_args.size());
+        total += kv.m_value->const_args.size() * kv.m_value->var_args.size();
     }
     return total;
 }

src/ackermannization/ackr_helper.h

@@ -22,9 +22,13 @@
 
 class ackr_helper {
 public:
-    typedef obj_hashtable<app>           app_set;
+    struct app_occ {
+        obj_hashtable<app> const_args;
+        obj_hashtable<app> var_args;
+    };
+    typedef app_occ  app_set;
     typedef obj_map<func_decl, app_set*> fun2terms_map;
-    typedef obj_map<app, app_set*>      sel2terms_map;
+    typedef obj_map<app, app_set*>       sel2terms_map;
 
     ackr_helper(ast_manager& m) : m_bvutil(m), m_autil(m) {}
 
@@ -88,13 +92,48 @@ class ackr_helper {
     static double calculate_lemma_bound(fun2terms_map const& occs1, sel2terms_map const& occs2);
 
     /** \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 unsigned n_choose_2(unsigned n) { return (n & 1) ? (n * (n >> 1)) : (n >> 1) * (n - 1); }
 
     /** \brief Calculate n choose 2 guarded for overflow. Returns infinity if unsafe. **/
     inline static double n_choose_2_chk(unsigned n) {
         SASSERT(std::numeric_limits<unsigned>().max() & 32);
         return n & (1 << 16) ? std::numeric_limits<double>().infinity() : n_choose_2(n);
     }
+
+    void insert(fun2terms_map& f2t, sel2terms_map& s2t, app* a) {
+        if (a->get_num_args() == 0) return;
+        ast_manager& m = m_bvutil.get_manager();
+        app_set* ts = nullptr;
+        bool is_const_args = true;
+        if (is_select(a)) {
+            app* sel = to_app(a->get_arg(0));
+            if (!s2t.find(sel, ts)) {
+                ts = alloc(app_set);
+                s2t.insert(sel, ts);
+            }
+        }
+        else if (is_uninterp_fn(a)) {
+            func_decl* const fd = a->get_decl();
+            if (!f2t.find(fd, ts)) {
+                ts = alloc(app_set);
+                f2t.insert(fd, ts);
+            }
+            is_const_args = m.is_value(a->get_arg(0));
+        }
+        else {
+            return;
+        }
+        for (unsigned i = 1; is_const_args && i < a->get_num_args(); ++i) {
+            is_const_args &= m.is_value(a->get_arg(i));
+        }
+
+        if (is_const_args) {
+            ts->const_args.insert(a);
+        }
+        else {
+            ts->var_args.insert(a);
+        }
+    }
 
 private:
     bv_util                              m_bvutil;

src/ackermannization/lackr.cpp

@@ -153,38 +153,57 @@ void lackr::eager_enc() {
 }
 
 void lackr::ackr(app_set const* ts) {
-    const app_set::iterator r = ts->end();
-    for (app_set::iterator j = ts->begin(); j != r; ++j) {
+    auto r = ts->var_args.end();
+    for (auto j = ts->var_args.begin(); j != r; ++j) {
         app * const t1 = *j;
-        app_set::iterator k = j;
+        auto k = j;
         ++k;
         for (; k != r; ++k) {
             app * const t2 = *k;
             if (t1 != t2) {
                 ackr(t1, t2);
             }
         }
+        for (app* t2 : ts->const_args) {
+            ackr(t1, t2);
+        }
     }
 }
 
-
-void lackr::abstract() {
-    for (auto const& kv : m_fun2terms) {
+void lackr::abstract_fun(fun2terms_map const& apps) {
+    for (auto const& kv : apps) {
         func_decl* fd = kv.m_key;
-        for (app * t : *kv.m_value) {
+        for (app * t : kv.m_value->var_args) {
+            app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
+            SASSERT(t->get_decl() == fd);
+            m_info->set_abstr(t, fc);
+        }
+        for (app * t : kv.m_value->const_args) {
             app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
             SASSERT(t->get_decl() == fd);
             m_info->set_abstr(t, fc);
         }
     }
 
-    for (auto& kv : m_sel2terms) {
+}
+
+void lackr::abstract_sel(sel2terms_map const& apps) {
+    for (auto const& kv : apps) {
         func_decl * fd = kv.m_key->get_decl();
-        for (app * t : *kv.m_value) {
+        for (app * t : kv.m_value->const_args) {
+            app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
+            m_info->set_abstr(t, fc);
+        }
+        for (app * t : kv.m_value->var_args) {
             app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
             m_info->set_abstr(t, fc);
         }
     }
+}
+
+void lackr::abstract() {
+    abstract_fun(m_fun2terms);
+    abstract_sel(m_sel2terms);
     m_info->seal();
     // perform abstraction of the formulas
     for (expr * f : m_formulas) {
@@ -194,28 +213,7 @@ void lackr::abstract() {
 }
 
 void lackr::add_term(app* a) {
-    app_set* ts = nullptr;
-    if (a->get_num_args() == 0) 
-        return;
-    if (m_ackr_helper.is_select(a)) {
-        app* sel = to_app(a->get_arg(0));
-        if (!m_sel2terms.find(sel, ts)) {
-            ts = alloc(app_set);
-            m_sel2terms.insert(sel, ts);
-        }
-    }
-    else if (m_ackr_helper.is_uninterp_fn(a)) {
-        func_decl* const fd = a->get_decl();
-        if (!m_fun2terms.find(fd, ts)) {
-            ts = alloc(app_set);
-            m_fun2terms.insert(fd, ts);
-        }
-    }
-    else {
-        return;
-    }
-    TRACE("ackermannize", tout << "term(" << mk_ismt2_pp(a, m, 2) << ")\n";);
-    ts->insert(a);
+    m_ackr_helper.insert(m_fun2terms, m_sel2terms, a);
 }
 
 void  lackr::push_abstraction() {

src/ackermannization/lackr.h

@@ -123,5 +123,9 @@ class lackr {
         // Collect all uninterpreted terms, skipping 0-arity.
         //
         bool collect_terms();
+
+        void abstract_sel(sel2terms_map const& apps);
+        void abstract_fun(fun2terms_map const& apps);
+
 };
 #endif /* LACKR_H_ */

src/opt/opt_context.cpp

@@ -38,6 +38,7 @@ Module Name:
 #include "tactic/arith/eq2bv_tactic.h"
 #include "tactic/bv/dt2bv_tactic.h"
 #include "tactic/generic_model_converter.h"
+#include "ackermannization/ackermannize_bv_tactic.h"
 #include "sat/sat_solver/inc_sat_solver.h"
 #include "qe/qsat.h"
 #include "opt/opt_context.h"
@@ -804,6 +805,7 @@ namespace opt {
             and_then(mk_simplify_tactic(m, m_params), 
                      mk_propagate_values_tactic(m),
                      mk_solve_eqs_tactic(m),
+                     mk_ackermannize_bv_tactic(m, m_params), 
                      // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
                      mk_simplify_tactic(m));   
         opt_params optp(m_params);