Merge branch 'master' of https://github.com/Z3Prover/z3

scripts/mk_project.py

@@ -36,6 +36,7 @@ def init_project_def():
     add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic')
     add_lib('aig_tactic', ['tactic'], 'tactic/aig')
     add_lib('solver', ['model', 'tactic'])
+    add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization')
     add_lib('interp', ['solver'])
     add_lib('cmd_context', ['solver', 'rewriter', 'interp'])
     add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds')
@@ -70,10 +71,10 @@ def init_project_def():
     add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality')
     add_lib('fp',  ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp')
     add_lib('nlsat_smt_tactic', ['nlsat_tactic', 'smt_tactic'], 'tactic/nlsat_smt')
-    add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
-    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
     add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
     add_lib('sat_solver', ['solver', 'core_tactics', 'aig_tactic', 'bv_tactics', 'arith_tactics', 'sat_tactic'], 'sat/sat_solver')
+    add_lib('smtlogic_tactics', ['ackermannization', 'sat_solver', 'arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe','nlsat_smt_tactic'], 'tactic/smtlogics')
+    add_lib('fpa_tactics', ['fpa', 'core_tactics', 'bv_tactics', 'sat_tactic', 'smt_tactic', 'arith_tactics', 'smtlogic_tactics'], 'tactic/fpa')
     add_lib('portfolio', ['smtlogic_tactics', 'sat_solver', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp',  'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
     add_lib('smtparser', ['portfolio'], 'parsers/smt')
     add_lib('opt', ['smt', 'smtlogic_tactics', 'sls_tactic', 'sat_solver'], 'opt')

src/ackermannization/ackermannization_params.pyg

@@ -0,0 +1,7 @@
+def_module_params('ackermannization',
+                  description='solving UF via ackermannization',
+                  export=True,
+                  params=(
+                          ('eager', BOOL, True, 'eagerly instantiate all congruence rules'),
+                          ))
+

src/ackermannization/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/ackermannization/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/ackermannization/ackermannize_bv_tactic.cpp

@@ -0,0 +1,97 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+ackermannize_bv_tactic.cpp
+
+Abstract:
+
+Author:
+
+Mikolas Janota
+
+Revision History:
+--*/
+#include"ackermannize_bv_tactic.h"
+#include"tactical.h"
+#include"lackr.h"
+#include"model_smt2_pp.h"
+#include"ackermannize_bv_tactic_params.hpp"
+#include"ackermannize_bv_model_converter.h"
+
+
+class ackermannize_bv_tactic : public tactic {
+public:
+    ackermannize_bv_tactic(ast_manager& m, params_ref const& p)
+        : m_m(m)
+        , m_p(p)
+    {}
+
+    virtual ~ackermannize_bv_tactic() { }
+
+    virtual void operator()(goal_ref const & g,
+        goal_ref_buffer & result,
+        model_converter_ref & mc,
+        proof_converter_ref & pc,
+        expr_dependency_ref & core) {
+        mc = 0;
+        ast_manager& m(g->m());
+        tactic_report report("ackermannize", *g);
+        fail_if_unsat_core_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));
+        scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, NULL);
+        flas.reset();
+        // mk result
+        goal_ref resg(alloc(goal, *g, true));
+        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_ackermannize_bv_model_converter(m, imp->get_info());
+        }
+
+		resg->inc_depth();
+		TRACE("ackermannize", resg->display(tout););
+		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);
+    }
+
+    virtual void reset_statistics() { m_st.reset(); }
+
+    virtual void cleanup() { }
+
+    virtual tactic* translate(ast_manager& m) {
+        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_bv_tactic(ast_manager & m, params_ref const & p) {
+    return alloc(ackermannize_bv_tactic, m, p);
+}

src/ackermannization/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/ackermannization/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/ackermannization/ackr_bound_probe.cpp

@@ -0,0 +1,77 @@
+/*++
+ 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"
+#include"ast_smt2_pp.h"
+
+/*
+  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 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) { }
+
+        ~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));
+        }
+        const double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms);
+        TRACE("ackr_bound_probe", tout << "total=" << total << std::endl;);
+        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/ackermannization/ackr_bound_probe.h

@@ -0,0 +1,29 @@
+ /*++
+ 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_
+#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()")
+*/
+
+#endif /* ACKR_BOUND_PROBE_H_ */

src/ackermannization/ackr_helper.cpp

@@ -0,0 +1,29 @@
+/*++
+ 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/ackermannization/ackr_helper.h

@@ -0,0 +1,69 @@
+ /*++
+ Copyright (c) 2016 Microsoft Corporation
+
+ Module Name:
+
+  ackr_helper.h
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+ --*/
+#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()) {
+                    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));
+        }
+
+        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); }
+
+        /** \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);
+        }
+    private:
+        bv_util                              m_bvutil;
+};
+#endif /* ACKR_HELPER_H_6475 */

src/ackermannization/ackr_info.h

@@ -0,0 +1,109 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+ackr_info.h
+
+Abstract:
+
+Author:
+
+Mikolas Janota
+
+Revision History:
+--*/
+#ifndef ACKR_INFO_H_
+#define ACKR_INFO_H_
+
+#include"obj_hashtable.h"
+#include"ast.h"
+#include"ref.h"
+#include"expr_replacer.h"
+
+/** \brief
+   Information about how a formula is being converted into
+   a formula without  uninterpreted function symbols via ackermannization.
+
+ The intended use is that new terms are added via set_abstr.
+ Once all terms are abstracted, call seal.
+ The function abstract may only be called when sealed.
+
+   The class enables reference counting.
+**/
+class ackr_info {
+    public:
+        ackr_info(ast_manager& m)
+        : m_m(m)
+        , m_consts(m)
+        , m_er(mk_default_expr_replacer(m))
+        , m_subst(m_m)
+        , m_ref_count(0)
+        , m_sealed(false)
+        {}
+
+        virtual ~ackr_info() {
+            m_consts.reset();
+        }
+
+        inline void set_abstr(app* term, app* c) {
+            SASSERT(!m_sealed);
+            SASSERT(c);
+            m_t2c.insert(term,c);
+            m_c2t.insert(c->get_decl(),term);
+            m_subst.insert(term, c);
+            m_consts.push_back(c);
+        }
+
+        inline void abstract(expr * e, expr_ref& res) {
+            SASSERT(m_sealed);
+            (*m_er)(e, res);
+        }
+
+        inline app* find_term(func_decl* c)  const {
+            app * rv = 0;
+            m_c2t.find(c,rv);
+            return rv;
+        }
+
+        inline app* get_abstr(app* term)  const {
+            app * const rv = m_t2c.find(term);
+            SASSERT(rv);
+            return rv;
+        }
+
+        inline void seal() {
+            m_sealed=true;
+            m_er->set_substitution(&m_subst);
+        }
+
+        //
+        // Reference counting
+        //
+        void inc_ref() { ++m_ref_count; }
+        void dec_ref() {
+            --m_ref_count;
+            if (m_ref_count == 0) {
+                dealloc(this);
+            }
+        }
+    private:
+        typedef obj_map<app, app*> t2ct;
+        typedef obj_map<func_decl, app*> c2tt;
+        ast_manager& m_m;
+
+        t2ct m_t2c; // terms to constants
+        c2tt m_c2t; // constants to terms (inversion of m_t2c)
+        expr_ref_vector m_consts; // the constants introduced during abstraction
+
+        // replacer and substitution used to compute abstractions
+        scoped_ptr<expr_replacer> m_er;
+        expr_substitution m_subst;
+
+        unsigned m_ref_count; // reference counting
+        bool m_sealed; // debugging
+};
+
+typedef ref<ackr_info> ackr_info_ref;
+
+#endif /* ACKR_INFO_H_ */

src/ackermannization/ackr_model_converter.cpp

@@ -0,0 +1,153 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+ackr_model_converter.cpp
+
+Abstract:
+
+Author:
+
+Mikolas Janota
+
+Revision History:
+--*/
+#include"ackr_model_converter.h"
+#include"model_evaluator.h"
+#include"ast_smt2_pp.h"
+#include"ackr_info.h"
+
+
+class ackr_model_converter : public model_converter {
+public:
+    ackr_model_converter(ast_manager & m,
+        const ackr_info_ref& info,
+        model_ref& abstr_model)
+        : m(m)
+        , info(info)
+        , abstr_model(abstr_model)
+        , fixed_model(true)
+    { }
+
+    ackr_model_converter(ast_manager & m,
+        const ackr_info_ref& info)
+        : m(m)
+        , info(info)
+        , fixed_model(false)
+    { }
+
+    virtual ~ackr_model_converter() { }
+
+    virtual void operator()(model_ref & md, unsigned goal_idx) {
+        SASSERT(goal_idx == 0);
+        SASSERT(!fixed_model || md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
+        model_ref& old_model = fixed_model ? abstr_model : md;
+        SASSERT(old_model.get());
+        model * new_model = alloc(model, m);
+        convert(old_model.get(), new_model);
+        md = new_model;
+    }
+
+    virtual void operator()(model_ref & md) { operator()(md, 0); }
+
+    //void display(std::ostream & out);
+
+    virtual model_converter * translate(ast_translation & translator) {NOT_IMPLEMENTED_YET();}
+protected:
+    ast_manager&              m;
+    const ackr_info_ref       info;
+    model_ref                 abstr_model;
+    bool                      fixed_model;
+    void convert(model * source, model * destination);
+    void add_entry(model_evaluator & evaluator,
+        app* term, expr* value,
+        obj_map<func_decl, func_interp*>& interpretations);
+    void convert_sorts(model * source, model * destination);
+    void convert_constants(model * source, model * destination);
+};
+
+void ackr_model_converter::convert(model * source, model * destination) {
+    //SASSERT(source->get_num_functions() == 0);
+    for (unsigned i = 0; i < source->get_num_functions(); i++) {
+        func_decl * const fd = source->get_function(i);
+        func_interp * const fi = source->get_func_interp(fd);
+        destination->register_decl(fd, fi);
+    }
+    convert_constants(source,destination);
+    convert_sorts(source,destination);
+}
+
+void ackr_model_converter::convert_constants(model * source, model * destination) {
+    TRACE("ackr_model", tout << "converting constants\n";);
+    obj_map<func_decl, func_interp*> interpretations;
+    model_evaluator evaluator(*source);
+    for (unsigned i = 0; i < source->get_num_constants(); i++) {
+        func_decl * const c = source->get_constant(i);
+        app * const term = info->find_term(c);
+        expr * value = source->get_const_interp(c);
+        if(!term) {
+            destination->register_decl(c, value);
+        } else {
+            add_entry(evaluator, term, value, interpretations);
+        }
+    }
+
+    obj_map<func_decl, func_interp*>::iterator e = interpretations.end();
+    for (obj_map<func_decl, func_interp*>::iterator i = interpretations.begin();
+            i!=e; ++i) {
+        func_decl* const fd = i->m_key;
+        func_interp* const fi = i->get_value();
+        fi->set_else(m.get_some_value(fd->get_range()));
+        destination->register_decl(fd, fi);
+    }
+}
+
+void ackr_model_converter::add_entry(model_evaluator & evaluator,
+        app* term, expr* value,
+        obj_map<func_decl, func_interp*>& interpretations) {
+    TRACE("ackr_model", tout << "add_entry"
+        << mk_ismt2_pp(term, m, 2)
+        << "->"
+        << mk_ismt2_pp(value, m, 2) << "\n";
+    );
+
+    func_interp* fi = 0;
+    func_decl * const declaration = term->get_decl();
+    const unsigned sz = declaration->get_arity();
+    SASSERT(sz == term->get_num_args());
+    if (!interpretations.find(declaration, fi))  {
+       fi = alloc(func_interp,m,sz);
+       interpretations.insert(declaration, fi);
+    }
+    expr_ref_vector args(m);
+    for (unsigned gi = 0; gi < sz; ++gi) {
+      expr * const arg = term->get_arg(gi);
+      expr_ref aarg(m);
+      info->abstract(arg, aarg);
+      expr_ref arg_value(m);
+      evaluator(aarg,arg_value);
+      args.push_back(arg_value);
+    }
+    if (fi->get_entry(args.c_ptr()) == 0) {
+        fi->insert_new_entry(args.c_ptr(), value);
+    } else {
+        TRACE("ackr_model", tout << "entry already present\n";);
+    }
+}
+
+void ackr_model_converter::convert_sorts(model * source, model * destination) {
+    for (unsigned i = 0; i < source->get_num_uninterpreted_sorts(); i++) {
+        sort * const s = source->get_uninterpreted_sort(i);
+        ptr_vector<expr> u = source->get_universe(s);
+        destination->register_usort(s, u.size(), u.c_ptr());
+    }
+}
+
+model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info) {
+    return alloc(ackr_model_converter, m, info);
+}
+
+model_converter * mk_ackr_model_converter(ast_manager & m, const ackr_info_ref& info, model_ref& abstr_model) {
+    return alloc(ackr_model_converter, m, info, abstr_model);
+}

src/ackermannization/ackr_model_converter.h

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+ackr_model_converter.h
+
+Abstract:
+
+Author:
+
+Mikolas Janota
+
+Revision History:
+--*/
+#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_ */

src/ackermannization/lackr.cpp

@@ -0,0 +1,290 @@
+/*++
+ Copyright (c) 2015 Microsoft Corporation
+
+ Module Name:
+
+  lackr.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+--*/
+
+#include"lackr.h"
+#include"ackermannization_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)
+    , m_p(p)
+    , m_formulas(formulas)
+    , m_abstr(m)
+    , m_sat(uffree_solver)
+    , m_ackr_helper(m)
+    , m_simp(m)
+    , m_ackrs(m)
+    , m_st(st)
+    , m_is_init(false)
+{
+    updt_params(p);
+}
+
+void lackr::updt_params(params_ref const & _p) {
+    ackermannization_params p(_p);
+    m_eager = p.eager();
+}
+
+lackr::~lackr() {
+    const fun2terms_map::iterator e = m_fun2terms.end();
+    for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
+        dealloc(i->get_value());
+    }
+}
+
+lbool lackr::operator() () {
+    SASSERT(m_sat);
+    init();
+    const lbool rv = m_eager ? eager() : lazy();
+    if (rv == l_true) m_sat->get_model(m_model);
+    CTRACE("lackr", rv == l_true,
+        model_smt2_pp(tout << "abstr_model(\n", m_m, *(m_model.get()), 2); tout << ")\n"; );
+    return rv;
+}
+
+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() {
+    SASSERT(!m_is_init);
+    m_is_init = true;
+    params_ref simp_p(m_p);
+    m_simp.updt_params(simp_p);
+    m_info = alloc(ackr_info, m_m);
+    collect_terms();
+    abstract();
+}
+
+//
+// Introduce ackermann lemma for the two given terms.
+//
+bool lackr::ackr(app * const t1, app * const t2) {
+    TRACE("lackr", tout << "ackr "
+            << mk_ismt2_pp(t1, m_m, 2) << " , " << mk_ismt2_pp(t2, m_m, 2) << "\n";);
+    const unsigned sz = t1->get_num_args();
+    SASSERT(t2->get_num_args() == sz);
+    expr_ref_vector eqs(m_m);
+    for (unsigned i = 0; i < sz; ++i) {
+        expr * const arg1 = t1->get_arg(i);
+        expr * const arg2 = t2->get_arg(i);
+        if (arg1 == arg2) continue; // quickly skip syntactically equal
+        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";);
+            return false;
+        }
+        eqs.push_back(m_m.mk_eq(arg1, arg2));
+    }
+    app * const a1 = m_info->get_abstr(t1);
+    app * const a2 = m_info->get_abstr(t2);
+    SASSERT(a1 && a2);
+    TRACE("lackr", tout << "abstr1 " << mk_ismt2_pp(a1, m_m, 2) << "\n";);
+    TRACE("lackr", tout << "abstr2 " << mk_ismt2_pp(a2, m_m, 2) << "\n";);
+    expr_ref lhs(m_m.mk_and(eqs.size(), eqs.c_ptr()), m_m);
+    TRACE("lackr", tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m_m, 2) << "\n";);
+    expr_ref rhs(m_m.mk_eq(a1, a2),m_m);
+    TRACE("lackr", tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m_m, 2) << "\n";);
+    expr_ref cg(m_m.mk_implies(lhs, rhs), m_m);
+    TRACE("lackr", tout << "ackr constr" << mk_ismt2_pp(cg, m_m, 2) << "\n";);
+    expr_ref cga(m_m);
+    m_info->abstract(cg, cga); // constraint needs abstraction due to nested applications
+    m_simp(cga);
+    TRACE("lackr", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
+    if (m_m.is_true(cga)) return false;
+    m_st.m_ackrs_sz++;
+    m_ackrs.push_back(cga);
+    return true;
+}
+
+//
+// Introduce the ackermann lemma for each pair of terms.
+//
+void lackr::eager_enc() {
+    TRACE("lackr", tout << "#funs: " << m_fun2terms.size() << std::endl;);
+    const fun2terms_map::iterator e = m_fun2terms.end();
+    for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
+        checkpoint();
+        func_decl* const fd = i->m_key;
+        app_set * const  ts = i->get_value();
+        const app_set::iterator r = ts->end();
+        for (app_set::iterator j = ts->begin(); j != r; ++j) {
+            app_set::iterator k = j;
+            ++k;
+            for (;  k != r; ++k) {
+                app * const t1 = *j;
+                app * const t2 = *k;
+                SASSERT(t1->get_decl() == fd);
+                SASSERT(t2->get_decl() == fd);
+                if (t1 == t2) continue;
+                ackr(t1,t2);
+            }
+        }
+    }
+}
+
+
+void lackr::abstract() {
+    const fun2terms_map::iterator e = m_fun2terms.end();
+    for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
+        func_decl* const fd = i->m_key;
+        app_set * const ts = i->get_value();
+        sort* const s = fd->get_range();
+        const app_set::iterator r = ts->end();
+        for (app_set::iterator j = ts->begin(); j != r; ++j) {
+            app * const fc = m_m.mk_fresh_const(fd->get_name().str().c_str(), s);
+            app * const t = *j;
+            SASSERT(t->get_decl() == fd);
+            m_info->set_abstr(t, fc);
+            TRACE("lackr", tout << "abstr term "
+                    << mk_ismt2_pp(t, m_m, 2)
+                    << " -> "
+                    << mk_ismt2_pp(fc, m_m, 2)
+                    << "\n";);
+        }
+    }
+    m_info->seal();
+    // perform abstraction of the formulas
+    const unsigned sz = m_formulas.size();
+    for (unsigned i = 0; i < sz; ++i) {
+        expr_ref a(m_m);
+        m_info->abstract(m_formulas.get(i), a);
+        m_abstr.push_back(a);
+    }
+}
+
+void lackr::add_term(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);
+    }
+    TRACE("lackr", tout << "term(" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
+    ts->insert(a);
+}
+
+void  lackr::push_abstraction() {
+    const unsigned sz = m_abstr.size();
+    for (unsigned i = 0; i < sz; ++i) {
+        m_sat->assert_expr(m_abstr.get(i));
+    }
+}
+
+lbool lackr::eager() {
+    push_abstraction();
+    TRACE("lackr", tout << "run sat 0\n"; );
+    const lbool rv0 = m_sat->check_sat(0, 0);
+    if (rv0 == l_false) return l_false;
+    eager_enc();
+    expr_ref all(m_m);
+    all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr());
+    m_simp(all);
+    m_sat->assert_expr(all);
+    TRACE("lackr", tout << "run sat all\n"; );
+    return m_sat->check_sat(0, 0);
+}
+
+lbool lackr::lazy() {
+    lackr_model_constructor mc(m_m, m_info);
+    push_abstraction();
+    unsigned ackr_head = 0;
+    while (1) {
+        m_st.m_it++;
+        checkpoint();
+        TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";);
+        const lbool r = m_sat->check_sat(0, 0);
+        if (r == l_undef) return l_undef; // give up
+        if (r == l_false) return l_false; // abstraction unsat
+        // reconstruct model
+        model_ref am;
+        m_sat->get_model(am);
+        const bool mc_res = mc.check(am);
+        if (mc_res) return l_true; // model okay
+        // refine abstraction
+        const lackr_model_constructor::conflict_list conflicts = mc.get_conflicts();
+        for (lackr_model_constructor::conflict_list::const_iterator i = conflicts.begin();
+             i != conflicts.end(); ++i) {
+            ackr(i->first, i->second);
+        }
+        while (ackr_head < m_ackrs.size()) {
+            m_sat->assert_expr(m_ackrs.get(ackr_head++));
+        }
+    }
+}
+
+//
+// Collect all uninterpreted terms, skipping 0-arity.
+//
+void lackr::collect_terms() {
+    ptr_vector<expr> stack;
+    expr *           curr;
+    expr_mark        visited;
+    for(unsigned i = 0; i < m_formulas.size(); ++i) {
+        stack.push_back(m_formulas.get(i));
+        TRACE("lackr", tout << "infla: " <<mk_ismt2_pp(m_formulas.get(i), m_m, 2) <<  "\n";);
+    }
+
+    while (!stack.empty()) {
+        curr = stack.back();
+        if (visited.is_marked(curr)) {
+            stack.pop_back();
+            continue;
+        }
+
+        switch (curr->get_kind()) {
+            case AST_VAR:
+                visited.mark(curr, true);
+                stack.pop_back();
+                break;
+            case AST_APP:
+            {
+                app * const a = to_app(curr);
+                if (for_each_expr_args(stack, visited, a->get_num_args(), a->get_args())) {
+                    visited.mark(curr, true);
+                    stack.pop_back();
+                    add_term(a);
+                }
+            }
+                break;
+            case AST_QUANTIFIER:
+                UNREACHABLE();
+                break;
+            default:
+                UNREACHABLE();
+                return;
+        }
+    }
+    visited.reset();
+}

src/ackermannization/lackr.h

@@ -0,0 +1,123 @@
+ /*++
+ Copyright (c) 2015 Microsoft Corporation
+
+ Module Name:
+
+  lackr.h
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+ --*/
+#ifndef LACKR_H_
+#define LACKR_H_
+
+#include"ackr_info.h"
+#include"ackr_helper.h"
+#include"th_rewriter.h"
+#include"cooperate.h"
+#include"bv_decl_plugin.h"
+#include"lbool.h"
+#include"model.h"
+#include"solver.h"
+#include"util.h"
+#include"tactic_exception.h"
+#include"goal.h"
+
+struct lackr_stats {
+    lackr_stats() : m_it(0), m_ackrs_sz(0) {}
+    void reset() { m_it = m_ackrs_sz = 0; }
+    unsigned    m_it;       // number of lazy iterations
+    unsigned    m_ackrs_sz; // number of congruence constraints
+};
+
+/** \brief
+   A class to encode or directly solve problems with uninterpreted functions via ackermannization.
+   Currently, solving is supported only for QF_UFBV.
+**/
+class lackr {
+    public:
+        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);
+
+        /** \brief
+         * Solve the formula that the class was initialized with.
+         **/
+        lbool operator() ();
+
+
+        /** \brief
+          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
+        //
+        inline ackr_info_ref get_info() { return m_info; }
+        inline model_ref get_model() { return m_model; }
+
+        //
+        //  timeout mechanism
+        //
+        void checkpoint() {
+            if (m_m.canceled()) {
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+            }
+            cooperate("lackr");
+        }
+    private:
+        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;
+        expr_ref_vector                      m_abstr;
+        fun2terms_map                        m_fun2terms;
+        ackr_info_ref                        m_info;
+        solver*                              m_sat;
+        ackr_helper                          m_ackr_helper;
+        th_rewriter                          m_simp;
+        expr_ref_vector                      m_ackrs;
+        model_ref                            m_model;
+        bool                                 m_eager;
+        lackr_stats&                         m_st;
+        bool                                 m_is_init;
+
+        void init();
+        lbool eager();
+        lbool lazy();
+
+        //
+        // Introduce congruence ackermann lemma for the two given terms.
+        //
+        bool ackr(app * const t1, app * const t2);
+
+        //
+        // Introduce the ackermann lemma for each pair of terms.
+        //
+        void eager_enc();
+
+        void abstract();
+
+        void push_abstraction();
+
+        void add_term(app* a);
+
+        //
+        // Collect all uninterpreted terms, skipping 0-arity.
+        //
+        void collect_terms();
+};
+#endif /* LACKR_H_ */

src/ackermannization/lackr_model_constructor.cpp

@@ -0,0 +1,376 @@
+/*++
+ Copyright (c) 2015 Microsoft Corporation
+
+ Module Name:
+
+  model_constructor.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+--*/
+#include"lackr_model_constructor.h"
+#include"model_evaluator.h"
+#include"ast_smt2_pp.h"
+#include"ackr_info.h"
+#include"for_each_expr.h"
+#include"bv_rewriter.h"
+#include"bool_rewriter.h"
+
+struct lackr_model_constructor::imp {
+    public:
+        imp(ast_manager & m,
+            ackr_info_ref info,
+            model_ref & abstr_model,
+            conflict_list & conflicts)
+            : m_m(m)
+            , m_info(info)
+            , m_abstr_model(abstr_model)
+            , m_conflicts(conflicts)
+            , m_b_rw(m)
+            , m_bv_rw(m)
+            , m_empty_model(m)
+            , m_ackr_helper(m)
+        {}
+
+        ~imp() {
+            {
+                values2val_t::iterator i = m_values2val.begin();
+                const values2val_t::iterator e = m_values2val.end();
+                for (; i != e; ++i) {
+                    m_m.dec_ref(i->m_key);
+                    m_m.dec_ref(i->m_value.value);
+                    m_m.dec_ref(i->m_value.source_term);
+                }
+            }
+            {
+                app2val_t::iterator i = m_app2val.begin();
+                const app2val_t::iterator e = m_app2val.end();
+                for (; i != e; ++i) {
+                    m_m.dec_ref(i->m_value);
+                    m_m.dec_ref(i->m_key);
+                }
+            }
+        }
+
+        //
+        // Returns true iff model was successfully constructed.
+        //
+        bool check() {
+            for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) {
+                func_decl * const c = m_abstr_model->get_constant(i);
+                app * const term = m_info->find_term(c);
+                if (term) m_stack.push_back(term);
+                else m_stack.push_back(m_m.mk_const(c));
+            }
+            return run();
+        }
+
+
+        void make_model(model_ref& destination) {
+            {
+                for (unsigned i = 0; i < m_abstr_model->get_num_uninterpreted_sorts(); i++) {
+                    sort * const s = m_abstr_model->get_uninterpreted_sort(i);
+                    ptr_vector<expr> u = m_abstr_model->get_universe(s);
+                    destination->register_usort(s, u.size(), u.c_ptr());
+                }
+            }
+            for (unsigned i = 0; i < m_abstr_model->get_num_functions(); i++) {
+                func_decl * const fd = m_abstr_model->get_function(i);
+                func_interp * const fi = m_abstr_model->get_func_interp(fd);
+                destination->register_decl(fd, fi);
+            }
+
+            {
+                const app2val_t::iterator e = m_app2val.end();
+                app2val_t::iterator i = m_app2val.end();
+                for (; i != e; ++i) {
+                    app * a = i->m_key;
+                    if (a->get_num_args()) continue;
+                    destination->register_decl(a->get_decl(), i->m_value);
+                }
+            }
+
+            obj_map<func_decl, func_interp*> interpretations;
+            {
+                const values2val_t::iterator e = m_values2val.end();
+                values2val_t::iterator i = m_values2val.end();
+                for (; i != e; ++i) add_entry(i->m_key, i->m_value.value, interpretations);
+            }
+
+            {
+                obj_map<func_decl, func_interp*>::iterator ie = interpretations.end();
+                obj_map<func_decl, func_interp*>::iterator ii = interpretations.begin();
+                for (; ii != ie; ++ii) {
+                    func_decl* const fd = ii->m_key;
+                    func_interp* const fi = ii->get_value();
+                    fi->set_else(m_m.get_some_value(fd->get_range()));
+                    destination->register_decl(fd, fi);
+                }
+            }
+        }
+
+        void add_entry(app* term, expr* value,
+            obj_map<func_decl, func_interp*>& interpretations) {
+            func_interp* fi = 0;
+            func_decl * const declaration = term->get_decl();
+            const unsigned sz = declaration->get_arity();
+            SASSERT(sz == term->get_num_args());
+            if (!interpretations.find(declaration, fi)) {
+                fi = alloc(func_interp, m_m, sz);
+                interpretations.insert(declaration, fi);
+            }
+            fi->insert_new_entry(term->get_args(), value);
+        }
+    private:
+        ast_manager&                    m_m;
+        ackr_info_ref                   m_info;
+        model_ref&                      m_abstr_model;
+        conflict_list&                  m_conflicts;
+        bool_rewriter                   m_b_rw;
+        bv_rewriter                     m_bv_rw;
+        scoped_ptr<model_evaluator>     m_evaluator;
+        model                           m_empty_model;
+    private:
+        struct val_info { expr * value; app * source_term; };
+        typedef obj_map<app, expr *> app2val_t;
+        typedef obj_map<app, val_info> values2val_t;
+        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;
+            rv.value = value;
+            rv.source_term = source_term;
+            return rv;
+        }
+
+        //
+        // Performs congruence check on terms on the stack.
+        // (Currently stops upon the first failure).
+        // Returns true if and only if congruence check succeeded.
+        bool run() {
+            m_evaluator = alloc(model_evaluator, m_empty_model);
+            expr_mark visited;
+            expr *  curr;
+            while (!m_stack.empty()) {
+                curr = m_stack.back();
+                if (visited.is_marked(curr)) {
+                    m_stack.pop_back();
+                    continue;
+                }
+
+                switch (curr->get_kind()) {
+                    case AST_VAR:
+                        UNREACHABLE();
+                        return false;
+                    case AST_APP: {
+                            app * a = to_app(curr);
+                            if (for_each_expr_args(m_stack, visited, a->get_num_args(), a->get_args())) {
+                                visited.mark(a, true);
+                                m_stack.pop_back();
+                                if (!mk_value(a)) return false;
+                            }
+                    }
+                        break;
+                    case AST_QUANTIFIER:
+                        UNREACHABLE();
+                        return false;
+                    default:
+                        UNREACHABLE();
+                        return false;
+                }
+            }
+            return true;
+        }
+
+        inline bool is_val(expr * e) { return m_m.is_value(e); }
+
+        inline bool eval_cached(app * a, expr *& val) {
+            if (is_val(a)) { val = a; return true; }
+            return m_app2val.find(a, val);
+        }
+
+        bool evaluate(app * const a, expr_ref& result) {
+            SASSERT(!is_val(a));
+            const unsigned num = a->get_num_args();
+            if (num == 0) { // handle constants
+                make_value_constant(a, result);
+                return true;
+            }
+            // evaluate arguments
+            expr_ref_vector values(m_m);
+            values.reserve(num);
+            expr * const * args = a->get_args();
+            for (unsigned i = 0; i < num; ++i) {
+                expr * val;
+                const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app?
+                CTRACE("model_constructor", !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2); );
+                TRACE("model_constructor", tout <<
+                    "arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2)
+                    << " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; );
+                SASSERT(b);
+                values[i] = val;
+            }
+            // handle functions
+            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;
+                }
+            }
+            else { // handle interpreted
+                make_value_interpreted_function(a, values, result);
+            }
+            return true;
+        }
+
+        //
+        // Check and record the value for a given term, given that all arguments are already checked.
+        //
+        bool mk_value(app * a) {
+            if (is_val(a)) return true; // skip numerals
+            TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
+            SASSERT(!m_app2val.contains(a));
+            expr_ref result(m_m);
+            if (!evaluate(a, result)) return false;
+            SASSERT(is_val(result));
+            TRACE("model_constructor",
+                tout << "map term(\n" << mk_ismt2_pp(a, m_m, 2) << "\n->"
+                << mk_ismt2_pp(result.get(), m_m, 2)<< ")\n"; );
+            CTRACE("model_constructor",
+                !is_val(result.get()),
+                tout << "eval fail\n" << mk_ismt2_pp(a, m_m, 2) << mk_ismt2_pp(result, m_m, 2) << "\n";
+            );
+            SASSERT(is_val(result.get()));
+            m_app2val.insert(a, result.get()); // memoize
+            m_m.inc_ref(a);
+            m_m.inc_ref(result.get());
+            return true;
+        }
+
+        // Constants from the abstract model are directly mapped to the concrete one.
+        void make_value_constant(app * const a, expr_ref& result) {
+            SASSERT(a->get_num_args() == 0);
+            func_decl * const fd = a->get_decl();
+            expr * val = m_abstr_model->get_const_interp(fd);
+            if (val == 0) { // TODO: avoid model completetion?
+                sort * s = fd->get_range();
+                val = m_abstr_model->get_some_value(s);
+            }
+            result = val;
+        }
+
+        bool make_value_uninterpreted_function(app* a,
+                expr_ref_vector& values,
+                app* key,
+                expr_ref& result) {
+            // get ackermann constant
+            app * const ac = m_info->get_abstr(a);
+            func_decl * const a_fd = a->get_decl();
+            SASSERT(ac->get_num_args() == 0);
+            SASSERT(a_fd->get_range() == ac->get_decl()->get_range());
+            expr_ref value(m_m);
+            value = m_abstr_model->get_const_interp(ac->get_decl());
+            // get ackermann constant's interpretation
+            if (value.get() == 0) { // TODO: avoid model completion?
+                sort * s = a_fd->get_range();
+                value = m_abstr_model->get_some_value(s);
+            }
+            // check congruence
+            val_info vi;
+            if(m_values2val.find(key,vi)) { // already is mapped to a value
+                SASSERT(vi.source_term);
+                const bool ok =  vi.value == value;
+                if (!ok) {
+                    TRACE("model_constructor",
+                        tout << "already mapped by(\n" << mk_ismt2_pp(vi.source_term, m_m, 2) << "\n->"
+                             << mk_ismt2_pp(vi.value, m_m, 2) << ")\n"; );
+                    m_conflicts.push_back(std::make_pair(a, vi.source_term));
+                }
+                result = vi.value;
+                return ok;
+            } else {                        // new value
+                result = value;
+                vi.value = value;
+                vi.source_term = a;
+                m_values2val.insert(key,vi);
+                m_m.inc_ref(vi.source_term);
+                m_m.inc_ref(vi.value);
+                m_m.inc_ref(key);
+                return true;
+            }
+            UNREACHABLE();
+            return true;
+        }
+    
+        void make_value_interpreted_function(app* a,
+                expr_ref_vector& values,
+                expr_ref& result) {
+            const unsigned num = values.size();
+            func_decl * const fd = a->get_decl();
+            const family_id fid = fd->get_family_id();
+            expr_ref term(m_m);
+            term = m_m.mk_app(a->get_decl(), num, values.c_ptr());
+            m_evaluator->operator() (term, result);
+            TRACE("model_constructor",
+                tout << "eval(\n" << mk_ismt2_pp(term.get(), m_m, 2) << "\n->"
+                << mk_ismt2_pp(result.get(), m_m, 2) << ")\n"; );
+            return;
+            if (fid == m_b_rw.get_fid()) {
+                decl_kind k = fd->get_decl_kind();
+                if (k == OP_EQ) {
+                    // theory dispatch for =
+                    SASSERT(num == 2);
+                    family_id s_fid = m_m.get_sort(values.get(0))->get_family_id();
+                    if (s_fid == m_bv_rw.get_fid())
+                        m_bv_rw.mk_eq_core(values.get(0), values.get(1), result);
+                } else {
+                    m_b_rw.mk_app_core(fd, num, values.c_ptr(), result);
+                }
+            } else {
+                if (fid == m_bv_rw.get_fid()) {
+                    m_bv_rw.mk_app_core(fd, num, values.c_ptr(), result);
+                }
+                else {
+                    UNREACHABLE();
+                }
+            }
+        }
+};
+
+lackr_model_constructor::lackr_model_constructor(ast_manager& m, ackr_info_ref info)
+    : m_imp(0)
+    , m_m(m)
+    , m_state(UNKNOWN)
+    , m_info(info)
+    , m_ref_count(0)
+{}
+
+lackr_model_constructor::~lackr_model_constructor() {
+    if (m_imp) dealloc(m_imp);
+}
+
+bool lackr_model_constructor::check(model_ref& abstr_model) {
+    m_conflicts.reset();
+    if (m_imp) {
+        dealloc(m_imp);
+        m_imp = 0;
+    }
+    m_imp = alloc(lackr_model_constructor::imp, m_m, m_info, abstr_model, m_conflicts);
+    const bool rv = m_imp->check();
+    m_state = rv ? CHECKED : CONFLICT;
+    return rv;
+}
+
+void lackr_model_constructor::make_model(model_ref& model) {
+    SASSERT(m_state == CHECKED);
+    m_imp->make_model(model);
+}

src/ackermannization/lackr_model_constructor.h

@@ -0,0 +1,61 @@
+ /*++
+ Copyright (c) 2015 Microsoft Corporation
+
+ Module Name:
+
+  model_constructor.h
+
+ Abstract:
+   Given a propositional abstraction, attempt to construct a model.
+
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+ --*/
+#ifndef LACKR_MODEL_CONSTRUCTOR_H_
+#define LACKR_MODEL_CONSTRUCTOR_H_
+
+#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;
+        typedef vector<app_pair>                  conflict_list;
+        lackr_model_constructor(ast_manager& m, ackr_info_ref info);
+        ~lackr_model_constructor();
+        bool check(model_ref& abstr_model);
+        const conflict_list& get_conflicts() {
+            SASSERT(m_state == CONFLICT);
+            return m_conflicts;
+        }
+        void make_model(model_ref& model);
+
+        //
+        // Reference counting
+        //
+        void inc_ref() { ++m_ref_count; }
+        void dec_ref() {
+            --m_ref_count;
+            if (m_ref_count == 0) {
+                dealloc(this);
+            }
+        }
+    private:
+        struct imp;
+        imp * m_imp;
+        ast_manager &                      m_m;
+        enum {CHECKED, CONFLICT, UNKNOWN}  m_state;
+        conflict_list                      m_conflicts;
+        const ackr_info_ref                m_info;
+
+        unsigned m_ref_count; // reference counting
+};
+
+typedef ref<lackr_model_constructor> lackr_model_constructor_ref;
+#endif /* MODEL_CONSTRUCTOR_H_ */

src/ackermannization/lackr_model_converter_lazy.cpp

@@ -0,0 +1,59 @@
+/*++
+ Copyright (c) 2015 Microsoft Corporation
+
+ Module Name:
+
+  lackr_model_converter_lazy.cpp
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+--*/
+#include"lackr_model_converter_lazy.h"
+#include"model_evaluator.h"
+#include"ast_smt2_pp.h"
+#include"ackr_info.h"
+#include"lackr_model_constructor.h"
+
+class lackr_model_converter_lazy : public model_converter {
+public:
+    lackr_model_converter_lazy(ast_manager & m,
+        const lackr_model_constructor_ref& lmc)
+        : m(m)
+        , model_constructor(lmc)
+    { }
+
+    virtual ~lackr_model_converter_lazy() { }
+
+    virtual void operator()(model_ref & md, unsigned goal_idx) {
+        SASSERT(goal_idx == 0);
+        SASSERT(md.get() == 0 || (!md->get_num_constants() && !md->get_num_functions()));
+        SASSERT(model_constructor.get());
+        model * new_model = alloc(model, m);
+        md = new_model;
+        model_constructor->make_model(md);
+    }
+
+    virtual void operator()(model_ref & md) {
+        operator()(md, 0);
+    }
+
+    //void display(std::ostream & out);
+
+    virtual model_converter * translate(ast_translation & translator) {
+        NOT_IMPLEMENTED_YET();
+    }
+protected:
+    ast_manager&                       m;
+    const lackr_model_constructor_ref  model_constructor;
+};
+
+model_converter * mk_lackr_model_converter_lazy(ast_manager & m,
+    const lackr_model_constructor_ref&  model_constructor) {
+    return alloc(lackr_model_converter_lazy, m, model_constructor);
+}

src/ackermannization/lackr_model_converter_lazy.h

@@ -0,0 +1,25 @@
+ /*++
+ Copyright (c) 2015 Microsoft Corporation
+
+ Module Name:
+
+  lackr_model_converter_lazy.h
+
+ Abstract:
+
+
+ Author:
+
+ Mikolas Janota
+
+ Revision History:
+ --*/
+#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_ */

src/cmd_context/tactic_cmds.cpp

@@ -187,8 +187,8 @@ public:
         tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
         tref->set_logic(ctx.get_logic());
         ast_manager & m = ctx.m();
-        unsigned timeout   = p.get_uint("timeout", UINT_MAX);
-        unsigned rlimit  =   p.get_uint("rlimit", 0);
+        unsigned timeout   = p.get_uint("timeout", ctx.params().m_timeout);
+        unsigned rlimit  =   p.get_uint("rlimit", ctx.params().m_rlimit);
         goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
         assert_exprs_from(ctx, *g);
         TRACE("check_sat_using", g->display(tout););

src/muz/README

@@ -9,4 +9,4 @@ solving Datalog programs.
 - clp - Dart/Symbolic execution-based solver
 - tab - Tabulation based solver
 - bmc - Bounded model checking based solver
-- fp  - main exported routines
+- fp  - main exported routines

src/tactic/bv/bv1_blaster_tactic.cpp

@@ -481,8 +481,6 @@ tactic * mk_bv1_blaster_tactic(ast_manager & m, params_ref const & p) {
 class is_qfbv_eq_probe : public probe {
 public:
     virtual result operator()(goal const & g) {
-        bv_rewriter rw(g.m());
-        if (!rw.hi_div0()) return false;
         bv1_blaster_tactic t(g.m());
         return t.is_target(g);
 

src/tactic/bv/bvarray2uf_tactic.h

@@ -30,4 +30,4 @@ tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref
 */
 
 
-#endif
+#endif

src/tactic/fpa/fpa2bv_model_converter.h

@@ -107,4 +107,4 @@ protected:
 
 model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv);
 
-#endif
+#endif

src/tactic/probe.cpp

@@ -285,9 +285,16 @@ struct is_non_qfbv_predicate {
             throw found();
         family_id fid = n->get_family_id();
         if (fid == m.get_basic_family_id()) 
-            return; 
-        if (fid == u.get_family_id())
-            return;
+            return;				
+        if (fid == u.get_family_id()) {
+			if (n->get_decl_kind() == OP_BSDIV0 ||
+				n->get_decl_kind() == OP_BUDIV0 ||
+				n->get_decl_kind() == OP_BSREM0 ||
+				n->get_decl_kind() == OP_BUREM0 ||
+				n->get_decl_kind() == OP_BSMOD0)				
+				throw found();
+			return;
+		}
         if (is_uninterp_const(n))
             return;
         throw found();
@@ -301,11 +308,10 @@ public:
     }
 };
 
+
 class is_qfbv_probe : public probe {
 public:
     virtual result operator()(goal const & g) {
-        bv_rewriter rw(g.m());
-        if (!rw.hi_div0()) return false;
         return !test<is_non_qfbv_predicate>(g);
     }
 };
@@ -356,6 +362,46 @@ probe * mk_is_qfaufbv_probe() {
     return alloc(is_qfaufbv_probe);
 }
 
+
+struct is_non_qfufbv_predicate {
+    struct found {};
+    ast_manager & m;
+    bv_util       m_bv_util;
+
+    is_non_qfufbv_predicate(ast_manager & _m) : m(_m), m_bv_util(_m) {}
+
+    void operator()(var *) { throw found(); }
+
+    void operator()(quantifier *) { throw found(); }
+
+    void operator()(app * n) {
+        if (!m.is_bool(n) && !m_bv_util.is_bv(n))
+            throw found();
+        family_id fid = n->get_family_id();
+        if (fid == m.get_basic_family_id())
+            return;
+        if (fid == m_bv_util.get_family_id())
+            return;
+        if (is_uninterp(n))
+            return;
+
+        throw found();
+    }
+};
+
+class is_qfufbv_probe : public probe {
+public:
+    virtual result operator()(goal const & g) {
+        return !test<is_non_qfufbv_predicate>(g);
+    }
+};
+
+probe * mk_is_qfufbv_probe() {
+    return alloc(is_qfufbv_probe);
+}
+
+
+
 class num_consts_probe : public probe {
     bool         m_bool;   // If true, track only boolean constants. Otherwise, track only non boolean constants.
     char const * m_family; // (Ignored if m_bool == true), if != 0 and m_bool == true, then track only constants of the given family.

src/tactic/probe.h

@@ -112,6 +112,7 @@ probe * mk_div(probe * p1, probe * p2);
 probe * mk_is_propositional_probe();
 probe * mk_is_qfbv_probe();
 probe * mk_is_qfaufbv_probe();
+probe * mk_is_qfufbv_probe();
 
 /*
   ADD_PROBE("is-propositional", "true if the goal is in propositional logic.", "mk_is_propositional_probe()")

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_bv_tactic.h"
 
 #define MEMLIMIT 300
 
@@ -46,7 +47,6 @@ 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
 
-
     params_ref hoist_p;
     hoist_p.set_bool("hoist_mul", true);
     hoist_p.set_bool("som", false);
@@ -66,7 +66,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_bv_tactic(m,p)
+            );
 }
 
 static tactic * main_p(tactic* t) {
@@ -98,14 +100,14 @@ 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 
-                                  cond(mk_is_qfbv_probe(),
-                                       cond(mk_is_qfbv_eq_probe(),
-                                            and_then(mk_bv1_blaster_tactic(m),
-                                                     using_params(smt, solver_p)),
+                                  // symbols. In this case, we should not use the `sat', but instead `smt'. Alternatively,
+								  // the UFs can be eliminated by eager ackermannization in the preamble.
+                                  cond(mk_is_qfbv_eq_probe(),
+                                       and_then(mk_bv1_blaster_tactic(m),
+                                                using_params(smt, solver_p)),
+                                       cond(mk_is_qfbv_probe(),
                                             and_then(mk_bit_blaster_tactic(m),
                                                      when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)),
                                                           and_then(using_params(and_then(mk_simplify_tactic(m),
@@ -115,8 +117,8 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti
                                                                                      mk_aig_tactic(),
                                                                                      using_params(mk_aig_tactic(),
                                                                                                   big_aig_p))))),
-                                                     sat)),
-                                       smt)));
+                                                     sat),
+                                            smt))));
     
     st->updt_params(p);
     return st;

src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp

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

src/tactic/smtlogics/qfufbv_ackr_model_converter.h

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

src/tactic/smtlogics/qfufbv_tactic.cpp

@@ -12,6 +12,7 @@ Abstract:
 Author:
 
     Leonardo (leonardo) 2012-02-27
+    Mikolas Janota
 
 Notes:
 
@@ -26,27 +27,163 @@ Notes:
 #include"bv_size_reduction_tactic.h"
 #include"reduce_args_tactic.h"
 #include"qfbv_tactic.h"
+#include"qfufbv_tactic_params.hpp"
+///////////////
+#include"model_smt2_pp.h"
+#include"cooperate.h"
+#include"lackr.h"
+#include"ackermannization_params.hpp"
+#include"qfufbv_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() { }
+
+    virtual void operator()(goal_ref const & g,
+        goal_ref_buffer & result,
+        model_converter_ref & mc,
+        proof_converter_ref & pc,
+        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);
+        const unsigned sz = g->size();
+        for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
+        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
+        goal_ref resg(alloc(goal, *g, true));
+        if (o == l_false) resg->assert_expr(m.mk_false());
+        if (o != l_undef) result.push_back(resg.get());
+        // report model
+        if (g->models_enabled() && (o == l_true)) {
+            model_ref abstr_model = imp->get_model();
+            mc = mk_qfufbv_ackr_model_converter(m, imp->get_info(), abstr_model);
+        }
+    }
+
+    void updt_params(params_ref const & _p) {
+        qfufbv_tactic_params p(_p);
+        m_use_sat = p.sat_backend();
+    }
+
+    virtual void collect_statistics(statistics & st) const {
+        ackermannization_params p(m_p);
+        if (!p.eager()) st.update("lackr-its", m_st.m_it);
+        st.update("ackr-constraints", m_st.m_ackrs_sz);
+    }
+
+    virtual void reset_statistics() { m_st.reset(); }
+
+    virtual void cleanup() { }
+
+    virtual tactic* translate(ast_manager& m) {
+        return alloc(qfufbv_ackr_tactic, m, m_p);
+    }
+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_preamble1(ast_manager & m, params_ref const & p) {
+    params_ref simp2_p = p;
+    simp2_p.set_bool("pull_cheap_ite", true);
+    simp2_p.set_bool("push_ite_bv", false);
+    simp2_p.set_bool("local_ctx", true);
+    simp2_p.set_uint("local_ctx_limit", 10000000);
+
+    simp2_p.set_bool("ite_extra_rules", true);
+    simp2_p.set_bool("mul2concat", true);
+
+    params_ref ctx_simp_p;
+    ctx_simp_p.set_uint("max_depth", 32);
+    ctx_simp_p.set_uint("max_steps", 5000000);
+
+    return and_then(
+        mk_simplify_tactic(m),
+        mk_propagate_values_tactic(m),
+        //using_params(mk_ctx_simplify_tactic(m_m), ctx_simp_p),
+        mk_solve_eqs_tactic(m),
+        mk_elim_uncnstr_tactic(m),
+        if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
+        mk_max_bv_sharing_tactic(m),
+        using_params(mk_simplify_tactic(m), simp2_p)
+        );
+}
+
+tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
+    params_ref main_p;
+    main_p.set_bool("elim_and", true);
+    main_p.set_bool("blast_distinct", true);
+
+    return and_then(mk_simplify_tactic(m),
+        mk_propagate_values_tactic(m),
+        mk_solve_eqs_tactic(m),
+        mk_elim_uncnstr_tactic(m),
+        if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
+        if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
+        mk_max_bv_sharing_tactic(m)
+        );
+}
 
 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) {
     params_ref main_p;
     main_p.set_bool("elim_and", true);
     main_p.set_bool("blast_distinct", true);
 
-    tactic * preamble_st = and_then(mk_simplify_tactic(m),
-                                    mk_propagate_values_tactic(m),
-                                    mk_solve_eqs_tactic(m),
-                                    mk_elim_uncnstr_tactic(m),
-                                    if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
-                                    if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
-                                    mk_max_bv_sharing_tactic(m)
-                                    );
+    tactic * const preamble_st = mk_qfufbv_preamble(m, p);
 
     tactic * st = using_params(and_then(preamble_st,
-                                        cond(mk_is_qfbv_probe(),
-                                            mk_qfbv_tactic(m),
-                                            mk_smt_tactic())),
-                               main_p);
+        cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic())),
+        main_p);
 
     st->updt_params(p);
     return st;
 }
+
+tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) {
+    tactic * const preamble_t = mk_qfufbv_preamble1(m, p);
+
+    tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p);
+    return and_then(preamble_t,
+        cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic()));
+}

src/tactic/smtlogics/qfufbv_tactic.h

@@ -25,8 +25,11 @@ class tactic;
 
 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p);
+
 /*
   ADD_TACTIC("qfufbv", "builtin strategy for solving QF_UFBV problems.", "mk_qfufbv_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/qfufbv_tactic_params.pyg

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