diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 04b974d6e..7af736a53 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -589,10 +589,8 @@ namespace smt { m_dep_manager.reset(); bool propagated = false; context & ctx = get_context(); - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (unsigned j = 0; j < m_nl_monomials.size(); ++j) { + theory_var v = m_nl_monomials[j]; 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::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (unsigned j = 0; j < m_nl_monomials.size(); ++j) { + theory_var v = m_nl_monomials[j]; if (is_real(v)) continue; bool computed_epsilon = false; @@ -2340,10 +2336,8 @@ namespace smt { bool theory_arith::max_min_nl_vars() { var_set already_found; svector vars; - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (unsigned j = 0; j < m_nl_monomials.size(); ++j) { + theory_var v = m_nl_monomials[j]; mark_var(v, vars, already_found); expr * n = var2expr(v); SASSERT(is_pure_monomial(n)); diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index d7d6c9811..2ecc80980 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -40,7 +40,6 @@ class dt2bv_tactic : public tactic { bv_util m_bv; obj_hashtable m_fd_sorts; obj_hashtable m_non_fd_sorts; - obj_map* 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* tr): - m(m), m_params(p), m_dt(m), m_bv(m), m_translate(tr), m_is_fd(*this) {} + dt2bv_tactic(ast_manager& m, params_ref const& p): + 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::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* tr) { - return alloc(dt2bv_tactic, m, p, tr); +tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p) { + return alloc(dt2bv_tactic, m, p); } diff --git a/src/tactic/bv/dt2bv_tactic.h b/src/tactic/bv/dt2bv_tactic.h index fd5aacda6..10ce0724f 100644 --- a/src/tactic/bv/dt2bv_tactic.h +++ b/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* 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)") diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp index 8c35bcfb1..febff0151 100644 --- a/src/test/get_consequences.cpp +++ b/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(m.get_plugin(m.get_family_id("datatype")))); - 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 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 tr; - obj_map rev_tr; - ref 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::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 fmls; - result[0]->get_formulas(fmls); - ref 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() { +void test2() { ast_manager m; reg_decl_plugins(m); bv_util bv(m); @@ -189,6 +112,4 @@ void test3() { void tst_get_consequences() { test1(); test2(); - test3(); - }