Refactoring ackermannization functionality.

src/tactic/ackr/ackermannize_tactic.cpp

@@ -38,7 +38,7 @@ public:
         expr_ref_vector flas(m);
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
-        scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas);
+        scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, NULL);
         flas.reset();
         // mk result
         goal_ref resg(alloc(goal, *g, true));

src/tactic/ackr/ackr.pyg

@@ -1,8 +1,7 @@
 def_module_params('ackr',
-                  description='solving UF via ackermannization (currently for QF_UFBV)',
+                  description='solving UF via ackermannization',
                   export=True,
                   params=(
                           ('eager', BOOL, True, 'eagerly instantiate all congruence rules'),
-                          ('sat_backend', BOOL, False, 'use SAT rather than SMT'),
                           ))
 

src/tactic/ackr/ackr_helper.h

@@ -0,0 +1,43 @@
+ /*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  ackr_helper.h
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+ --*/
+#ifndef ACKR_HELPER_H_6475
+#define ACKR_HELPER_H_6475
+#include"bv_decl_plugin.h"
+class ackr_helper {
+    public:
+        ackr_helper(ast_manager& m) : m_bvutil(m) {}
+        inline bool should_ackermannize(app const * a) const {
+            if (a->get_family_id() == m_bvutil.get_family_id()) {
+                switch (a->get_decl_kind()) {
+                    case OP_BSDIV0:
+                    case OP_BUDIV0:
+                    case OP_BSREM0:
+                    case OP_BUREM0:
+                    case OP_BSMOD0:
+                        return true;
+                    default:
+                        return is_uninterp(a);
+                }
+            }
+            return (is_uninterp(a));
+        }
+
+        bv_util& bvutil() { return m_bvutil; }
+    private:
+        bv_util                              m_bvutil;
+};
+#endif /* ACKR_HELPER_H_6475 */

src/tactic/ackr/lackr.cpp

@@ -22,20 +22,16 @@
 #include"ackr_info.h"
 #include"for_each_expr.h"
 ///////////////
-#include"inc_sat_solver.h"
-#include"qfaufbv_tactic.h"
-#include"qfbv_tactic.h"
-#include"tactic2solver.h"
-///////////////
 #include"model_smt2_pp.h"
 ///////////////
-lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas)
+lackr::lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas,
+    solver * uffree_solver)
     : m_m(m)
     , m_p(p)
     , m_formulas(formulas)
     , m_abstr(m)
-    , m_sat(NULL)
+    , m_sat(uffree_solver)
-    , m_bvutil(m)
+    , m_ackr_helper(m)
     , m_simp(m)
     , m_ackrs(m)
     , m_st(st)
@@ -52,7 +48,7 @@ lackr::~lackr() {
 }
 
 lbool lackr::operator() () {
-    setup_sat();
+    SASSERT(m_sat);
     init();
     const lbool rv = m_eager ? eager() : lazy();
     if (rv == l_true) m_sat->get_model(m_model);
@@ -91,7 +87,7 @@ bool lackr::ackr(app * const t1, app * const t2) {
         expr * const arg1 = t1->get_arg(i);
         expr * const arg2 = t2->get_arg(i);
         if (arg1 == arg2) continue; // quickly skip syntactically equal
-        if (m_bvutil.is_numeral(arg1) && m_bvutil.is_numeral(arg2)) {
+        if (m_ackr_helper.bvutil().is_numeral(arg1) && m_ackr_helper.bvutil().is_numeral(arg2)) {
             // quickly abort if there are two distinct numerals
             SASSERT(arg1 != arg2);
             TRACE("lackr", tout << "never eq\n";);
@@ -178,9 +174,8 @@ void lackr::abstract() {
 
 void lackr::add_term(app* a) {
     if (a->get_num_args() == 0) return;
-    if (!should_ackermannize(a)) return;
+    if (!m_ackr_helper.should_ackermannize(a)) return;
     func_decl* const fd = a->get_decl();
-    SASSERT(m_bvutil.is_bv_sort(fd->get_range()) || m_m.is_bool(a));
     app_set* ts = 0;
     if (!m_fun2terms.find(fd, ts)) {
         ts = alloc(app_set);
@@ -239,21 +234,6 @@ lbool lackr::lazy() {
     }
 }
 
-void lackr::setup_sat() {
-    SASSERT(m_sat == NULL);
-    if (m_use_sat) {
-        tactic_ref t = mk_qfbv_tactic(m_m, m_p);
-        m_sat = mk_tactic2solver(m_m, t.get(), m_p);
-    }
-    else {
-        tactic_ref t = mk_qfaufbv_tactic(m_m, m_p);
-        m_sat = mk_tactic2solver(m_m, t.get(), m_p);
-    }
-    SASSERT(m_sat != NULL);
-    m_sat->set_produce_models(true);
-}
-
-
 //
 // Collect all uninterpreted terms, skipping 0-arity.
 //

src/tactic/ackr/lackr.h

@@ -18,6 +18,7 @@
 #define LACKR_H_15079
 ///////////////
 #include"ackr_info.h"
+#include"ackr_helper.h"
 #include"ackr_params.hpp"
 #include"th_rewriter.h"
 #include"cooperate.h"
@@ -42,12 +43,12 @@ struct lackr_stats {
 **/
 class lackr {
     public:
-        lackr(ast_manager& m, params_ref p, lackr_stats& st, expr_ref_vector& formulas);
+        lackr(ast_manager& m, params_ref p, lackr_stats& st,
+            expr_ref_vector& formulas, solver * uffree_solver);
         ~lackr();
         void updt_params(params_ref const & _p) {
             ackr_params p(_p);
             m_eager = p.eager();
-            m_use_sat = p.sat_backend();
         }
 
         /** \brief
@@ -87,18 +88,16 @@ class lackr {
         expr_ref_vector                      m_abstr;
         fun2terms_map                        m_fun2terms;
         ackr_info_ref                        m_info;
-        scoped_ptr<solver>                   m_sat;
+        solver*                              m_sat;
-        bv_util                              m_bvutil;
+        ackr_helper                          m_ackr_helper;
         th_rewriter                          m_simp;
         expr_ref_vector                      m_ackrs;
         model_ref                            m_model;
         bool                                 m_eager;
-        bool                                 m_use_sat;
         lackr_stats&                         m_st;
         bool                                 m_is_init;
 
         void init();
-        void setup_sat();
         lbool eager();
         lbool lazy();
 
@@ -122,24 +121,5 @@ class lackr {
         // Collect all uninterpreted terms, skipping 0-arity.
         //
         void collect_terms();
-
-        inline bool should_ackermannize(app const * a) const;
 };
-
-inline bool lackr::should_ackermannize(app const * a) const {
-    if (a->get_family_id() == m_bvutil.get_family_id()) {
-        switch (a->get_decl_kind()) {
-        case OP_BSDIV0:
-        case OP_BUDIV0:
-        case OP_BSREM0:
-        case OP_BUREM0:
-        case OP_BSMOD0:
-            return true;
-        default:
-            return is_uninterp(a);
-        }
-    }
-    return (is_uninterp(a));
-}
-
 #endif /* LACKR_H_15079 */

src/tactic/ackr/lackr_model_constructor.cpp

@@ -34,6 +34,7 @@ struct lackr_model_constructor::imp {
             , m_b_rw(m)
             , m_bv_rw(m)
             , m_empty_model(m)
+            , m_ackr_helper(m)
         {}
 
         ~imp() {
@@ -141,6 +142,7 @@ struct lackr_model_constructor::imp {
         values2val_t     m_values2val;
         app2val_t        m_app2val;
         ptr_vector<expr> m_stack;
+        ackr_helper      m_ackr_helper;
 
         static inline val_info mk_val_info(expr* value, app* source_term) {
             val_info rv;
@@ -227,7 +229,7 @@ struct lackr_model_constructor::imp {
                 values[i] = val;
             }
             // handle functions
-            if (a->get_family_id() == null_family_id) { // handle uninterpreted
+            if (m_ackr_helper.should_ackermannize(a)) { // handle uninterpreted
                 app_ref key(m_m.mk_app(a->get_decl(), values.c_ptr()), m_m);
                 if (!make_value_uninterpreted_function(a, values, key.get(), result)) {
                     return false;

src/tactic/ackr/lackr_model_constructor.h

@@ -19,7 +19,9 @@
 #define LACKR_MODEL_CONSTRUCTOR_H_626
 #include"ast.h"
 #include"ackr_info.h"
+#include"ackr_helper.h"
 #include"model.h"
+
 class lackr_model_constructor {
     public:
         typedef std::pair<app *, app *>           app_pair;
@@ -50,6 +52,7 @@ class lackr_model_constructor {
         conflict_list                      m_conflicts;
         ast_manager&                       m_m;
         const ackr_info_ref                m_info;
+
         unsigned m_ref_count; // reference counting
 };
 

src/tactic/ackr_tactics/ackr_tactics.pyg

@@ -0,0 +1,7 @@
+def_module_params('ackr_tactics',
+                  description='tactics based on solving UF-theories via ackermannization (see also ackr module)',
+                  export=True,
+                  params=(
+                          ('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'),
+                          ))
+

src/tactic/ackr_tactics/qfufbv_ackr_tactic.cpp

@@ -28,14 +28,22 @@ Revision History:
 #include"model_smt2_pp.h"
 #include"cooperate.h"
 #include"lackr.h"
-#include"ackr_params.hpp"
+#include"ackr_tactics_params.hpp"
 #include"ackr_model_converter.h"
+///////////////
+#include"inc_sat_solver.h"
+#include"qfaufbv_tactic.h"
+#include"qfbv_tactic.h"
+#include"tactic2solver.h"
+///////////////
+
 
 class qfufbv_ackr_tactic : public tactic {
 public:
     qfufbv_ackr_tactic(ast_manager& m, params_ref const& p)
         : m_m(m)
         , m_p(p)
+        , m_use_sat(false)
     {}
 
     virtual ~qfufbv_ackr_tactic() { }
@@ -47,12 +55,13 @@ public:
         expr_dependency_ref & core) {
         mc = 0;
         ast_manager& m(g->m());
-        TRACE("lackr", g->display(tout << "goal:\n"););
+        TRACE("qfufbv_ackr_tactic", g->display(tout << "goal:\n"););
         // running implementation
         expr_ref_vector flas(m);
         const unsigned sz = g->size();
         for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
-        scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas);
+        scoped_ptr<solver> uffree_solver = setup_sat();
+        scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, uffree_solver.get());
         const lbool o = imp->operator()();
         flas.reset();
         // report result
@@ -66,6 +75,11 @@ public:
         }
     }
 
+    void updt_params(params_ref const & _p) {
+        ackr_tactics_params p(_p);
+        m_use_sat = p.sat_backend();
+    }
+
     virtual void collect_statistics(statistics & st) const {
         ackr_params p(m_p);
         if (!p.eager()) st.update("lackr-its", m_st.m_it);
@@ -83,6 +97,24 @@ private:
     ast_manager&                         m_m;
     params_ref                           m_p;
     lackr_stats                          m_st;
+    bool                                 m_use_sat;
+
+    solver* setup_sat() {
+        solver * sat(NULL);
+        if (m_use_sat) {
+            tactic_ref t = mk_qfbv_tactic(m_m, m_p);
+            sat = mk_tactic2solver(m_m, t.get(), m_p);
+        }
+        else {
+            tactic_ref t = mk_qfaufbv_tactic(m_m, m_p);
+            sat = mk_tactic2solver(m_m, t.get(), m_p);
+        }
+        SASSERT(sat != NULL);
+        sat->set_produce_models(true);
+        return sat;
+    }
+
+
 };
 
 tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {

src/tactic/ackr_tactics/qfufbv_ackr_tactic.h

@@ -14,8 +14,8 @@ Mikolas Janota
 Revision History:
 --*/
 
-#ifndef _QFUFBF_ACKR_TACTIC_H_
+#ifndef _QFUFBV_ACKR_TACTIC_H_
-#define _QFUFBF_ACKR_TACTIC_H_
+#define _QFUFBV_ACKR_TACTIC_H_
 #include"tactical.h"
 
 tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p);

src/tactic/smtlogics/qfbv_tactic.cpp

@@ -28,6 +28,7 @@ Notes:
 #include"bv_size_reduction_tactic.h"
 #include"aig_tactic.h"
 #include"sat_tactic.h"
+#include"ackermannize_tactic.h"
 
 #define MEMLIMIT 300
 
@@ -66,7 +67,9 @@ tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
             // We should decide later, if we keep it or not.
             //
             using_params(mk_simplify_tactic(m), hoist_p),
-            mk_max_bv_sharing_tactic(m));
+            mk_max_bv_sharing_tactic(m),
+            mk_ackermannize_tactic(m,p)
+            );
 }
 
 static tactic * main_p(tactic* t) {
@@ -98,7 +101,6 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
     big_aig_p.set_bool("aig_per_assertion", false);
     
     tactic* preamble_st = mk_qfbv_preamble(m, p);
-    
     tactic * st = main_p(and_then(preamble_st,
                                   // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
                                   // symbols. In this case, we should not use