remove legacy interface to dt2bv tactic

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

src/smt/theory_arith_nl.h

@@ -589,10 +589,8 @@ namespace smt {
         m_dep_manager.reset();
         bool propagated = false;
         context & ctx = get_context();
-        svector<theory_var>::const_iterator it  = m_nl_monomials.begin();
+        for (unsigned j = 0; j < m_nl_monomials.size(); ++j) {
-        svector<theory_var>::const_iterator end = m_nl_monomials.end();
+            theory_var v = m_nl_monomials[j];
-        for (; it != end; ++it) {
-            theory_var v = *it;
             expr * m     = var2expr(v);
             if (!ctx.is_relevant(m))
                 continue;
@@ -706,10 +704,8 @@ namespace smt {
         bool bounded      = false;
         unsigned n        = 0;
         numeral range;
-        svector<theory_var>::const_iterator it  = m_nl_monomials.begin();
+        for (unsigned j = 0; j < m_nl_monomials.size(); ++j) {
-        svector<theory_var>::const_iterator end = m_nl_monomials.end();
+            theory_var v = m_nl_monomials[j];
-        for (; it != end; ++it) {
-            theory_var v = *it;
             if (is_real(v))
                 continue;
             bool computed_epsilon = false;
@@ -2340,10 +2336,8 @@ namespace smt {
     bool theory_arith<Ext>::max_min_nl_vars() {
         var_set             already_found;
         svector<theory_var> vars;
-        svector<theory_var>::const_iterator it  = m_nl_monomials.begin();
+        for (unsigned j = 0; j < m_nl_monomials.size(); ++j) {
-        svector<theory_var>::const_iterator end = m_nl_monomials.end();
+            theory_var v = m_nl_monomials[j];
-        for (; it != end; ++it) {
-            theory_var v = *it;
             mark_var(v, vars, already_found);
             expr * n     = var2expr(v);
             SASSERT(is_pure_monomial(n));

src/tactic/bv/dt2bv_tactic.cpp

@@ -40,7 +40,6 @@ class dt2bv_tactic : public tactic {
     bv_util       m_bv;
     obj_hashtable<sort> m_fd_sorts;
     obj_hashtable<sort> m_non_fd_sorts;
-    obj_map<func_decl, func_decl*>*     m_translate;
     
 
     bool is_fd(expr* a) { return is_fd(get_sort(a)); }
@@ -99,11 +98,11 @@ class dt2bv_tactic : public tactic {
     sort_pred m_is_fd;
 public:
 
-    dt2bv_tactic(ast_manager& m, params_ref const& p, obj_map<func_decl, func_decl*>* tr): 
+    dt2bv_tactic(ast_manager& m, params_ref const& p): 
-        m(m), m_params(p), m_dt(m), m_bv(m), m_translate(tr), m_is_fd(*this) {}
+        m(m), m_params(p), m_dt(m), m_bv(m), m_is_fd(*this) {}
     
     virtual tactic * translate(ast_manager & m) {
-        return alloc(dt2bv_tactic, m, m_params, 0);
+        return alloc(dt2bv_tactic, m, m_params);
     }
 
     virtual void updt_params(params_ref const & p) {
@@ -154,9 +153,6 @@ public:
                 obj_map<func_decl, func_decl*>::iterator it = rw.enum2bv().begin(), end = rw.enum2bv().end();
                 for (; it != end; ++it) {
                     filter->insert(it->m_value);
-                    if (m_translate) {
-                        m_translate->insert(it->m_key, it->m_value);
-                    }
                 }
             }
             {
@@ -182,6 +178,6 @@ public:
 
 };
 
-tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p, obj_map<func_decl, func_decl*>* tr) {
+tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p) {
-    return alloc(dt2bv_tactic, m, p, tr);
+    return alloc(dt2bv_tactic, m, p);
 }

src/tactic/bv/dt2bv_tactic.h

@@ -24,7 +24,7 @@ Revision History:
 class ast_manager;
 class tactic;
 
-tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref(), obj_map<func_decl, func_decl*>* tr = 0);
+tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref());
 
 /*
     ADD_TACTIC("dt2bv", "eliminate finite domain data-types. Replace by bit-vectors.", "mk_dt2bv_tactic(m, p)")

src/test/get_consequences.cpp

@@ -51,85 +51,8 @@ static void test1() {
     std::cout << conseq << "\n";
 }
 
-static void test2() {
-    ast_manager m;
-    reg_decl_plugins(m);
-    bv_util bv(m);
-    datatype_util dtutil(m);
-    params_ref p;
 
-    datatype_decl_plugin & dt = *(static_cast<datatype_decl_plugin*>(m.get_plugin(m.get_family_id("datatype"))));
+void test2() {
-    sort_ref_vector new_sorts(m);
-    constructor_decl* R = mk_constructor_decl(symbol("R"), symbol("is-R"), 0, 0);
-    constructor_decl* G = mk_constructor_decl(symbol("G"), symbol("is-G"), 0, 0);
-    constructor_decl* B = mk_constructor_decl(symbol("B"), symbol("is-B"), 0, 0);
-    constructor_decl* constrs[3] = { R, G, B };
-    datatype_decl * enum_sort = mk_datatype_decl(symbol("RGB"), 3, constrs);
-    VERIFY(dt.mk_datatypes(1, &enum_sort, new_sorts));    
-    del_constructor_decls(3, constrs);
-    sort* rgb = new_sorts[0].get();
-
-    expr_ref x = mk_const(m, "x", rgb), y = mk_const(m, "y", rgb), z = mk_const(m, "z", rgb);
-    ptr_vector<func_decl> const& enums = *dtutil.get_datatype_constructors(rgb);
-    expr_ref r = expr_ref(m.mk_const(enums[0]), m);
-    expr_ref g = expr_ref(m.mk_const(enums[1]), m);
-    expr_ref b = expr_ref(m.mk_const(enums[2]), m);
-    expr_ref val(m);
-
-    // Eliminate enumeration data-types:
-    goal_ref gl = alloc(goal, m);
-    gl->assert_expr(m.mk_not(m.mk_eq(x, r)));
-    gl->assert_expr(m.mk_not(m.mk_eq(x, b)));
-    gl->display(std::cout);
-    obj_map<func_decl, func_decl*> tr;
-    obj_map<func_decl, func_decl*> rev_tr;
-    ref<tactic> dt2bv = mk_dt2bv_tactic(m, p, &tr);
-    goal_ref_buffer result;
-    model_converter_ref mc;
-    proof_converter_ref pc;
-    expr_dependency_ref core(m);
-    (*dt2bv)(gl, result, mc, pc, core);
-
-    // Collect translations from enumerations to bit-vectors
-    obj_map<func_decl, func_decl*>::iterator it = tr.begin(), end = tr.end();
-    for (; it != end; ++it) {
-        rev_tr.insert(it->m_value, it->m_key);
-    }
-
-    // Create bit-vector implication problem
-    val = m.mk_const(tr.find(to_app(x)->get_decl()));
-    std::cout << val << "\n";
-    ptr_vector<expr> fmls;
-    result[0]->get_formulas(fmls);    
-    ref<solver> solver = mk_inc_sat_solver(m, p);
-    for (unsigned i = 0; i < fmls.size(); ++i) {
-        solver->assert_expr(fmls[i]);
-    }
-    expr_ref_vector asms(m), vars(m), conseq(m);
-    vars.push_back(val);
-
-    // retrieve consequences
-    solver->get_consequences(asms, vars, conseq);
-    
-    // Convert consequences over bit-vectors to enumeration types.
-    std::cout << conseq << "\n";
-    for (unsigned i = 0; i < conseq.size(); ++i) {
-        expr* a, *b, *u, *v;
-        func_decl* f;
-        rational num;
-        unsigned bvsize;
-        VERIFY(m.is_implies(conseq[i].get(), a, b));
-        if (m.is_eq(b, u, v) && rev_tr.find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) {
-            SASSERT(num.is_unsigned());
-            expr_ref head(m);
-            head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()]));
-            conseq[i] = m.mk_implies(a, head);
-        }
-    }
-    std::cout << conseq << "\n";
-}
-
-void test3() {
     ast_manager m;
     reg_decl_plugins(m);
     bv_util bv(m);
@@ -189,6 +112,4 @@ void test3() {
 void tst_get_consequences() {
     test1();
     test2();
-    test3();
-
 }