Added tactic that translates BV arrays into BV UFs.

src/ast/array_decl_plugin.h

@@ -22,7 +22,7 @@ Revision History:
 #include"ast.h"
 
 
-inline sort* get_array_range(sort const * s) { 
+inline sort* get_array_range(sort const * s) {
     return to_sort(s->get_parameter(s->get_num_parameters() - 1).get_ast());
 }
 
@@ -104,20 +104,20 @@ class array_decl_plugin : public decl_plugin {
     }
 
     //
-    // Contract for sort: 
-    //   parameters[0]     - 1st dimension 
+    // Contract for sort:
+    //   parameters[0]     - 1st dimension
     //   ...
     //   parameters[n-1]   - nth dimension
     //   parameters[n]     - range
     //
     virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
-    
+
     //
     // Contract for func_decl:
     //   parameters[0]     - array sort
     // Contract for others:
     //   no parameters
-    virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
+    virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                      unsigned arity, sort * const * domain, sort * range);
 
     virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
@@ -184,6 +184,11 @@ public:
     sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); }
 
     sort * mk_array_sort(unsigned arity, sort* const* domain, sort* range);
+
+    app * mk_as_array(sort * s, func_decl * f) {
+        parameter param(f);
+        return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, &param, 0, 0, s);
+    }
 };
 
 

src/tactic/bv/bvarray2uf_rewriter.cpp

@@ -0,0 +1,377 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    bvarray2uf_rewriter.cpp
+
+Abstract:
+
+    Rewriter that rewrites bit-vector arrays into bit-vector
+    (uninterpreted) functions.
+
+Author:
+
+    Christoph (cwinter) 2015-11-04
+
+Notes:
+
+--*/
+
+#include"cooperate.h"
+#include"bv_decl_plugin.h"
+#include"array_decl_plugin.h"
+#include"params.h"
+#include"ast_pp.h"
+#include"bvarray2uf_rewriter.h"
+
+// [1] C. M. Wintersteiger, Y. Hamadi, and L. de Moura: Efficiently Solving
+//     Quantified Bit-Vector Formulas, in Formal Methods in System Design,
+//     vol. 42, no. 1, pp. 3-23, Springer, 2013.
+
+bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p) :
+    m_manager(m),
+    m_out(m),
+    m_bindings(m),
+    m_bv_util(m),
+    m_array_util(m),
+    m_emc(0),
+    m_fmc(0),
+    extra_assertions(m) {
+    updt_params(p);
+    // We need to make sure that the mananger has the BV and array plugins loaded.
+    symbol s_bv("bv");
+    if (!m_manager.has_plugin(s_bv))
+        m_manager.register_plugin(s_bv, alloc(bv_decl_plugin));
+    symbol s_array("array");
+    if (!m_manager.has_plugin(s_array))
+        m_manager.register_plugin(s_array, alloc(array_decl_plugin));
+}
+
+bvarray2uf_rewriter_cfg::~bvarray2uf_rewriter_cfg() {
+    for (obj_map<expr, func_decl*>::iterator it = m_arrays_fs.begin();
+    it != m_arrays_fs.end();
+        it++)
+        m_manager.dec_ref(it->m_value);
+}
+
+void bvarray2uf_rewriter_cfg::reset() {}
+
+sort * bvarray2uf_rewriter_cfg::get_index_sort(expr * e) {
+    return get_index_sort(m_manager.get_sort(e));
+}
+
+sort * bvarray2uf_rewriter_cfg::get_index_sort(sort * s) {
+    SASSERT(s->get_num_parameters() >= 2);
+    unsigned total_width = 0;
+    for (unsigned i = 0; i < s->get_num_parameters() - 1; i++) {
+        parameter const & p = s->get_parameter(i);
+        SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast())));
+        SASSERT(m_bv_util.is_bv_sort(to_sort(p.get_ast())));
+        total_width += m_bv_util.get_bv_size(to_sort(p.get_ast()));
+    }
+    return m_bv_util.mk_sort(total_width);
+}
+
+sort * bvarray2uf_rewriter_cfg::get_value_sort(expr * e) {
+    return get_value_sort(m_manager.get_sort(e));
+}
+
+sort * bvarray2uf_rewriter_cfg::get_value_sort(sort * s) {
+    SASSERT(s->get_num_parameters() >= 2);
+    parameter const & p = s->get_parameter(s->get_num_parameters() - 1);
+    SASSERT(p.is_ast() && is_sort(to_sort(p.get_ast())));
+    return to_sort(p.get_ast());
+}
+
+bool bvarray2uf_rewriter_cfg::is_bv_array(expr * e) {
+    return is_bv_array(m_manager.get_sort(e));
+}
+
+bool bvarray2uf_rewriter_cfg::is_bv_array(sort * s) {
+    if (!m_array_util.is_array(s))
+        return false;
+
+    SASSERT(s->get_num_parameters() >= 2);
+    for (unsigned i = 0; i < s->get_num_parameters(); i++) {
+        parameter const & p = s->get_parameter(i);
+        if (!p.is_ast() || !is_sort(to_sort(p.get_ast())) ||
+            !m_bv_util.is_bv_sort(to_sort(p.get_ast())))
+            return false;
+    }
+
+    return true;
+}
+
+func_decl_ref bvarray2uf_rewriter_cfg::mk_uf_for_array(expr * e) {
+    SASSERT(is_bv_array(e));
+
+    if (m_array_util.is_as_array(e))
+        return func_decl_ref(static_cast<func_decl*>(to_app(e)->get_decl()->get_parameter(0).get_ast()), m_manager);
+    else {
+        app * a = to_app(e);
+        func_decl * bv_f = 0;
+        if (!m_arrays_fs.find(e, bv_f)) {
+            sort * domain = get_index_sort(a);
+            sort * range = get_value_sort(a);
+            bv_f = m_manager.mk_fresh_func_decl("f_t", "", 1, &domain, range);
+            if (is_uninterp_const(e)) {
+                if (m_emc)
+                    m_emc->insert(to_app(e)->get_decl(),
+                                  m_array_util.mk_as_array(m_manager.get_sort(e), bv_f));
+            }
+            else if (m_fmc)
+                m_fmc->insert(bv_f);
+            m_arrays_fs.insert(e, bv_f);
+            m_manager.inc_ref(bv_f);
+        }
+
+        return func_decl_ref(bv_f, m_manager);
+    }
+}
+
+br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
+    br_status res = BR_FAILED;
+
+    if (m_manager.is_eq(f) && is_bv_array(f->get_domain()[0])) {
+        SASSERT(num == 2);
+        // From [1]: Finally, we replace equations of the form t = s,
+        // where t and s are arrays, with \forall x . f_t(x) = f_s(x).
+        func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
+        func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
+
+        sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) };
+        symbol names[1] = { symbol("x") };
+        var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+
+        expr_ref body(m_manager);
+        body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get()));
+
+        result = m_manager.mk_forall(1, sorts, names, body);
+        res = BR_DONE;
+    }
+    else if (m_manager.is_distinct(f) && is_bv_array(f->get_domain()[0])) {
+        result = m_manager.mk_distinct_expanded(num, args);
+        res = BR_REWRITE1;
+    }
+    else if (f->get_family_id() == null_family_id) {
+        TRACE("bvarray2uf_rw", tout << "UF APP: " << f->get_name() << std::endl; );
+
+        bool has_bv_arrays = false;
+        func_decl_ref f_t(m_manager);
+        for (unsigned i = 0; i < num; i++) {
+            if (is_bv_array(args[i])) {
+                SASSERT(m_array_util.is_as_array(args[i]));
+                has_bv_arrays = true;
+            }
+        }
+
+        expr_ref t(m_manager);
+        t = m_manager.mk_app(f, num, args);
+
+        if (is_bv_array(t)) {
+            // From [1]: For every array term t we create a fresh uninterpreted function f_t.
+            f_t = mk_uf_for_array(t);
+            result = m_array_util.mk_as_array(m_manager.get_sort(t), f_t);
+            res = BR_DONE;
+        }
+        else if (has_bv_arrays) {
+            result = t;
+            res = BR_DONE;
+        }
+        else
+            res = BR_FAILED;
+    }
+    else if (m_array_util.get_family_id() == f->get_family_id()) {
+        TRACE("bvarray2uf_rw", tout << "APP: " << f->get_name() << std::endl; );
+
+        if (m_array_util.is_select(f)) {
+            SASSERT(num == 2);
+            expr * t = args[0];
+            expr * i = args[1];
+            TRACE("bvarray2uf_rw", tout <<
+                "select; array: " << mk_ismt2_pp(t, m()) <<
+                " index: " << mk_ismt2_pp(i, m()) << std::endl;);
+
+            if (!is_bv_array(t))
+                res = BR_FAILED;
+            else {
+                // From [1]: Then, we replace terms of the form select(t, i) with f_t(i).
+                func_decl_ref f_t(mk_uf_for_array(t), m_manager);
+                result = m_manager.mk_app(f_t, i);
+                res = BR_DONE;
+            }
+        }
+        else {
+            if (!is_bv_array(f->get_range()))
+                res = BR_FAILED;
+            else {
+                if (m_array_util.is_const(f)) {
+                    SASSERT(num == 1);
+                    expr_ref t(m_manager.mk_app(f, num, args), m_manager);
+                    expr * v = args[0];
+                    func_decl_ref f_t(mk_uf_for_array(t), m_manager);
+
+                    result = m_array_util.mk_as_array(f->get_range(), f_t);
+                    res = BR_DONE;
+
+                    // Add \forall x . f_t(x) = v
+                    sort * sorts[1] = { get_index_sort(f->get_range()) };
+                    symbol names[1] = { symbol("x") };
+                    var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+
+                    expr_ref body(m_manager);
+                    body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), v);
+
+                    expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
+                    extra_assertions.push_back(frllx);
+                }
+                else if (m_array_util.is_as_array(f)) {
+                    res = BR_FAILED;
+                }
+                else if (m_array_util.is_map(f)) {
+                    SASSERT(f->get_num_parameters() == 1);
+                    SASSERT(f->get_parameter(0).is_ast());
+                    expr_ref t(m_manager.mk_app(f, num, args), m_manager);
+                    func_decl_ref f_t(mk_uf_for_array(t), m_manager);
+                    func_decl_ref map_f(to_func_decl(f->get_parameter(0).get_ast()), m_manager);
+
+                    func_decl_ref_vector ss(m_manager);
+                    for (unsigned i = 0; i < num; i++) {
+                        SASSERT(m_array_util.is_array(args[i]));
+                        func_decl_ref fd(mk_uf_for_array(args[i]), m_manager);
+                        ss.push_back(fd);
+                    }
+
+                    // Add \forall x . f_t(x) = map_f(a[x], b[x], ...)
+                    sort * sorts[1] = { get_index_sort(f->get_range()) };
+                    symbol names[1] = { symbol("x") };
+                    var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+
+                    expr_ref_vector new_args(m_manager);
+                    for (unsigned i = 0; i < num; i++)
+                        new_args.push_back(m_manager.mk_app(ss[i].get(), x.get()));
+
+                    expr_ref body(m_manager);
+                    body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()),
+                                           m_manager.mk_app(map_f, num, new_args.c_ptr()));
+
+                    expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
+                    extra_assertions.push_back(frllx);
+
+                    result = m_array_util.mk_as_array(f->get_range(), f_t);
+                    res = BR_DONE;
+                }
+                else if (m_array_util.is_store(f)) {
+                    SASSERT(num == 3);
+                    expr * s = args[0];
+                    expr * i = args[1];
+                    expr * v = args[2];
+                    TRACE("bvarray2uf_rw", tout <<
+                        "store; array: " << mk_ismt2_pp(s, m()) <<
+                        " index: " << mk_ismt2_pp(i, m()) <<
+                        " value: " << mk_ismt2_pp(v, m()) << std::endl;);
+                    if (!is_bv_array(s))
+                        res = BR_FAILED;
+                    else {
+                        expr_ref t(m_manager.mk_app(f, num, args), m_manager);
+                        // From [1]: For every term t of the form store(s, i, v), we add the universal
+                        // formula \forall x . x = i \vee f_t(x) = f_s(x), and the ground atom f_t(i) = v.
+                        func_decl_ref f_s(mk_uf_for_array(s), m_manager);
+                        func_decl_ref f_t(mk_uf_for_array(t), m_manager);
+
+                        result = m_array_util.mk_as_array(f->get_range(), f_t);
+                        res = BR_DONE;
+
+                        sort * sorts[1] = { get_index_sort(f->get_range()) };
+                        symbol names[1] = { symbol("x") };
+                        var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
+
+                        expr_ref body(m_manager);
+                        body = m_manager.mk_or(m_manager.mk_eq(x, i),
+                                               m_manager.mk_eq(m_manager.mk_app(f_t, x.get()),
+                                                               m_manager.mk_app(f_s, x.get())));
+
+                        expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager);
+                        extra_assertions.push_back(frllx);
+
+                        expr_ref ground_atom(m_manager);
+                        ground_atom = m_manager.mk_eq(m_manager.mk_app(f_t, i), v);
+                        extra_assertions.push_back(ground_atom);
+                        TRACE("bvarray2uf_rw", tout << "ground atom: " << mk_ismt2_pp(ground_atom, m()) << std::endl; );
+                    }
+                }
+                else {
+                    NOT_IMPLEMENTED_YET();
+                    res = BR_FAILED;
+                }
+            }
+        }
+    }
+
+    CTRACE("bvarray2uf_rw", res==BR_DONE, tout << "result: " << mk_ismt2_pp(result, m()) << std::endl; );
+    return res;
+}
+
+bool bvarray2uf_rewriter_cfg::pre_visit(expr * t)
+{
+    TRACE("bvarray2uf_rw_q", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;);
+
+    if (is_quantifier(t)) {
+        quantifier * q = to_quantifier(t);
+        TRACE("bvarray2uf_rw_q", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;);
+        sort_ref_vector new_bindings(m_manager);
+        for (unsigned i = 0; i < q->get_num_decls(); i++)
+            new_bindings.push_back(q->get_decl_sort(i));
+        SASSERT(new_bindings.size() == q->get_num_decls());
+        m_bindings.append(new_bindings);
+    }
+    return true;
+}
+
+bool bvarray2uf_rewriter_cfg::reduce_quantifier(quantifier * old_q,
+    expr * new_body,
+    expr * const * new_patterns,
+    expr * const * new_no_patterns,
+    expr_ref & result,
+    proof_ref & result_pr) {
+    unsigned curr_sz = m_bindings.size();
+    SASSERT(old_q->get_num_decls() <= curr_sz);
+    unsigned num_decls = old_q->get_num_decls();
+    unsigned old_sz = curr_sz - num_decls;
+    string_buffer<> name_buffer;
+    ptr_buffer<sort> new_decl_sorts;
+    sbuffer<symbol>  new_decl_names;
+    for (unsigned i = 0; i < num_decls; i++) {
+        symbol const & n = old_q->get_decl_name(i);
+        sort * s = old_q->get_decl_sort(i);
+
+        NOT_IMPLEMENTED_YET();
+
+    }
+    result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
+        new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
+        old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
+    result_pr = 0;
+    m_bindings.shrink(old_sz);
+    TRACE("bvarray2uf_rw_q", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
+        mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
+        " new body: " << mk_ismt2_pp(new_body, m()) << std::endl;
+    tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;);
+    return true;
+}
+
+bool bvarray2uf_rewriter_cfg::bvarray2uf_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) {
+    if (t->get_idx() >= m_bindings.size())
+        return false;
+
+    expr_ref new_exp(m());
+    sort * s = t->get_sort();
+
+    NOT_IMPLEMENTED_YET();
+
+    result = new_exp;
+    result_pr = 0;
+    TRACE("bvarray2uf_rw_q", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
+    return true;
+}

src/tactic/bv/bvarray2uf_rewriter.h

@@ -0,0 +1,87 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    bvarray2uf_rewriter.h
+
+Abstract:
+
+    Rewriter that rewrites bit-vector arrays into bit-vector
+    (uninterpreted) functions.
+
+Author:
+
+    Christoph (cwinter) 2015-11-04
+
+Notes:
+
+--*/
+#ifndef BVARRAY2UF_REWRITER_H_
+#define BVARRAY2UF_REWRITER_H_
+
+#include"rewriter_def.h"
+#include"extension_model_converter.h"
+#include"filter_model_converter.h"
+
+class bvarray2uf_rewriter_cfg : public default_rewriter_cfg {
+    ast_manager       & m_manager;
+    expr_ref_vector     m_out;
+    sort_ref_vector     m_bindings;
+    bv_util             m_bv_util;
+    array_util          m_array_util;
+    extension_model_converter * m_emc;
+    filter_model_converter * m_fmc;
+
+    obj_map<expr, func_decl*> m_arrays_fs;
+
+public:
+    bvarray2uf_rewriter_cfg(ast_manager & m, params_ref const & p);
+    ~bvarray2uf_rewriter_cfg();
+
+    ast_manager & m() const { return m_manager; }
+    void updt_params(params_ref const & p) {}
+
+    void reset();
+
+    bool pre_visit(expr * t);
+
+    br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr);
+
+    bool reduce_quantifier(quantifier * old_q,
+                           expr * new_body,
+                           expr * const * new_patterns,
+                           expr * const * new_no_patterns,
+                           expr_ref & result,
+                           proof_ref & result_pr);
+
+    bool reduce_var(var * t, expr_ref & result, proof_ref & result_pr);
+
+    expr_ref_vector extra_assertions;
+
+    void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_emc = emc; m_fmc = fmc; }
+
+protected:
+    sort * get_index_sort(expr * e);
+    sort * get_index_sort(sort * s);
+    sort * get_value_sort(expr * e);
+    sort * get_value_sort(sort * s);
+    bool is_bv_array(expr * e);
+    bool is_bv_array(sort * e);
+    func_decl_ref mk_uf_for_array(expr * e);
+};
+
+template class rewriter_tpl<bvarray2uf_rewriter_cfg>;
+
+struct bvarray2uf_rewriter : public rewriter_tpl<bvarray2uf_rewriter_cfg> {
+    bvarray2uf_rewriter_cfg m_cfg;
+    bvarray2uf_rewriter(ast_manager & m, params_ref const & p) :
+        rewriter_tpl<bvarray2uf_rewriter_cfg>(m, m.proofs_enabled(), m_cfg),
+        m_cfg(m, p) {
+    }
+
+    void set_mcs(extension_model_converter * emc, filter_model_converter * fmc) { m_cfg.set_mcs(emc, fmc); }
+};
+
+#endif
+

src/tactic/bv/bvarray2uf_tactic.cpp

@@ -0,0 +1,168 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    bvarray2uf_tactic.cpp
+
+Abstract:
+
+    Tactic that rewrites bit-vector arrays into bit-vector
+    (uninterpreted) functions.
+
+Author:
+
+    Christoph (cwinter) 2015-11-04
+
+Notes:
+
+--*/
+#include"tactical.h"
+#include"bv_decl_plugin.h"
+#include"expr_replacer.h"
+#include"extension_model_converter.h"
+#include"filter_model_converter.h"
+#include"ast_smt2_pp.h"
+
+#include"bvarray2uf_tactic.h"
+#include"bvarray2uf_rewriter.h"
+
+class bvarray2uf_tactic : public tactic {
+
+    struct imp {
+        ast_manager &       m_manager;
+        bool                m_produce_models;
+        bool                m_produce_proofs;
+        bool                m_produce_cores;
+        volatile bool       m_cancel;
+        bvarray2uf_rewriter m_rw;
+
+        ast_manager & m() { return m_manager; }
+
+        imp(ast_manager & m, params_ref const & p) :
+            m_manager(m),
+            m_produce_models(false),
+            m_cancel(false),
+            m_produce_proofs(false),
+            m_produce_cores(false),
+            m_rw(m, p) {
+            updt_params(p);
+        }
+
+        void set_cancel(bool f) {
+            m_cancel = f;
+        }
+
+        void checkpoint() {
+            if (m_cancel)
+                throw tactic_exception(TACTIC_CANCELED_MSG);
+        }
+
+        void operator()(goal_ref const & g,
+                        goal_ref_buffer & result,
+                        model_converter_ref & mc,
+                        proof_converter_ref & pc,
+                        expr_dependency_ref & core)
+        {
+            SASSERT(g->is_well_sorted());
+            tactic_report report("bvarray2uf", *g);
+            mc = 0; pc = 0; core = 0; result.reset();
+            fail_if_proof_generation("bvarray2uf", g);
+            fail_if_unsat_core_generation("bvarray2uf", g);
+
+            TRACE("bvarray2uf", tout << "Before: " << std::endl; g->display(tout); );
+            m_produce_models = g->models_enabled();
+
+            if (m_produce_models) {
+                extension_model_converter * emc = alloc(extension_model_converter, m_manager);
+                filter_model_converter * fmc = alloc(filter_model_converter, m_manager);
+                mc = concat(emc, fmc);
+                m_rw.set_mcs(emc, fmc);
+
+            }
+
+
+            m_rw.reset();
+            expr_ref   new_curr(m_manager);
+            proof_ref  new_pr(m_manager);
+            unsigned size = g->size();
+            for (unsigned idx = 0; idx < size; idx++) {
+                if (g->inconsistent())
+                    break;
+                expr * curr = g->form(idx);
+                m_rw(curr, new_curr, new_pr);
+                //if (m_produce_proofs) {
+                //    proof * pr = g->pr(idx);
+                //    new_pr = m.mk_modus_ponens(pr, new_pr);
+                //}
+                g->update(idx, new_curr, new_pr, g->dep(idx));
+            }
+
+            for (unsigned i = 0; i < m_rw.m_cfg.extra_assertions.size(); i++)
+                g->assert_expr(m_rw.m_cfg.extra_assertions[i].get());
+
+            g->inc_depth();
+            result.push_back(g.get());
+            TRACE("bvarray2uf", tout << "After: " << std::endl; g->display(tout););
+            SASSERT(g->is_well_sorted());
+        }
+
+        void updt_params(params_ref const & p) {
+        }
+    };
+
+    imp *      m_imp;
+    params_ref m_params;
+
+public:
+    bvarray2uf_tactic(ast_manager & m, params_ref const & p) :
+        m_params(p) {
+        m_imp = alloc(imp, m, p);
+    }
+
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(bvarray2uf_tactic, m, m_params);
+    }
+
+    virtual ~bvarray2uf_tactic() {
+        dealloc(m_imp);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+        m_params = p;
+        m_imp->updt_params(p);
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+        insert_produce_models(r);
+    }
+
+    virtual void operator()(goal_ref const & in,
+                            goal_ref_buffer & result,
+                            model_converter_ref & mc,
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        (*m_imp)(in, result, mc, pc, core);
+    }
+
+    virtual void cleanup() {
+        ast_manager & m = m_imp->m();
+        imp * d = alloc(imp, m, m_params);
+    #pragma omp critical (tactic_cancel)
+        {
+            std::swap(d, m_imp);
+        }
+        dealloc(d);
+    }
+
+    virtual void set_cancel(bool f) {
+        if (m_imp)
+            m_imp->set_cancel(f);
+    }
+
+};
+
+
+tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(bvarray2uf_tactic, m, p));
+}

src/tactic/bv/bvarray2uf_tactic.h

@@ -0,0 +1,33 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    bvarray2ufbvarray2uf_tactic.h
+
+Abstract:
+
+    Tactic that rewrites bit-vector arrays into bit-vector
+    (uninterpreted) functions.
+
+Author:
+
+    Christoph (cwinter) 2015-11-04
+
+Notes:
+
+--*/
+#ifndef BV_ARRAY2UF_TACTIC_H_
+#define BV_ARRAY2UF_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref());
+/*
+    ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)")
+*/
+
+
+#endif