From 9e4450228eb4537e7cf87192c53ba4bcb69107bb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Oct 2016 14:52:37 -0400 Subject: [PATCH] adding unit test for enumeration types Signed-off-by: Nikolaj Bjorner --- src/ast/ast_smt2_pp.cpp | 5 ++- src/tactic/bv/dt2bv_tactic.cpp | 16 +++++--- src/tactic/bv/dt2bv_tactic.h | 3 +- src/test/get_consequences.cpp | 74 ++++++++++++++++++++++++++-------- 4 files changed, 74 insertions(+), 24 deletions(-) diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 2e2d99a38..98c3b7962 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -1205,13 +1205,16 @@ mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent, unsigned num } std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p) { - smt2_pp_environment_dbg env(p.m_manager); + smt2_pp_environment_dbg env(p.m_manager); if (is_expr(p.m_ast)) { ast_smt2_pp(out, to_expr(p.m_ast), env, p.m_params, p.m_indent, p.m_num_vars, p.m_var_prefix); } else if (is_sort(p.m_ast)) { ast_smt2_pp(out, to_sort(p.m_ast), env, p.m_params, p.m_indent); } + else if (p.m_ast == 0) { + out << "null"; + } else { SASSERT(is_func_decl(p.m_ast)); ast_smt2_pp(out, to_func_decl(p.m_ast), env, p.m_params, p.m_indent); diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index e8763475b..ab9df78ad 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -43,6 +43,7 @@ class dt2bv_tactic : public tactic { ref m_ext; ref m_filter; unsigned m_num_translated; + obj_map* m_translate; struct rw_cfg : public default_rewriter_cfg { dt2bv_tactic& m_t; @@ -117,7 +118,7 @@ class dt2bv_tactic : public tactic { unsigned nc = m_t.m_dt.get_datatype_num_constructors(s); result = m.mk_fresh_const(f->get_name().str().c_str(), m_t.m_bv.mk_sort(bv_size)); if (!is_power_of_two(nc)) { - m_t.m_bounds.push_back(m_t.m_bv.mk_ule(result, m_t.m_bv.mk_numeral(nc, bv_size))); + m_t.m_bounds.push_back(m_t.m_bv.mk_ule(result, m_t.m_bv.mk_numeral(nc-1, bv_size))); } expr_ref f_def(m); ptr_vector const& cs = *m_t.m_dt.get_datatype_constructors(s); @@ -129,6 +130,9 @@ class dt2bv_tactic : public tactic { // update model converters. m_t.m_ext->insert(f, f_def); m_t.m_filter->insert(to_app(result)->get_decl()); + if (m_t.m_translate) { + m_t.m_translate->insert(f, result); + } } else { return false; @@ -253,11 +257,11 @@ class dt2bv_tactic : public tactic { public: - dt2bv_tactic(ast_manager& m, params_ref const& p): - m(m), m_params(p), m_dt(m), m_bv(m), m_bounds(m) {} + dt2bv_tactic(ast_manager& m, params_ref const& p, obj_map* tr): + m(m), m_params(p), m_dt(m), m_bv(m), m_bounds(m), m_translate(tr) {} virtual tactic * translate(ast_manager & m) { - return alloc(dt2bv_tactic, m, m_params); + return alloc(dt2bv_tactic, m, m_params, 0); } virtual void updt_params(params_ref const & p) { @@ -320,6 +324,6 @@ public: }; -tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p) { - return alloc(dt2bv_tactic, m, p); +tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p, obj_map* tr) { + return alloc(dt2bv_tactic, m, p, tr); } diff --git a/src/tactic/bv/dt2bv_tactic.h b/src/tactic/bv/dt2bv_tactic.h index 64d1d5497..a8fb33fe8 100644 --- a/src/tactic/bv/dt2bv_tactic.h +++ b/src/tactic/bv/dt2bv_tactic.h @@ -20,10 +20,11 @@ Revision History: #define DT2BV_TACTIC_H_ #include"params.h" +#include"obj_hashtable.h" class ast_manager; class tactic; -tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref()); +tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p = params_ref(), obj_map* tr = 0); /* 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 f35a12ede..24f3a5d38 100644 --- a/src/test/get_consequences.cpp +++ b/src/test/get_consequences.cpp @@ -8,7 +8,9 @@ Copyright (c) 2016 Microsoft Corporation #include "datatype_decl_plugin.h" #include "reg_decl_plugins.h" #include "ast_pp.h" -#include "dt2bv.h" +#include "dt2bv_tactic.h" +#include "tactic.h" +#include "model_smt2_pp.h" //include static expr_ref mk_const(ast_manager& m, char const* name, sort* s) { @@ -53,38 +55,78 @@ 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"))); + 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 const* enum_sort = mk_datatype_decl(symbol("RGB"), 3, constrs); + 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 = dt.geet_datatype_constructors(rgb); - expr_ref r = expr_ref(m.mk_const(enums[0], m), m), g = expr_ref(m.mk_const(enums[1], m), m), b = expr_ref(m.mk_const(enums[2], m), m); + 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); - goal_ref g = alloc(goal, m); - g->assert_expr(m.mk_not(m.mk_eq(x, r))); - g->assert_expr(m.mk_not(m.mk_eq(x, b))); - g->display(std::cout); - tactic_ref dt2bv = mk_dt2bv_tactic(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; - (*dt2bv)(g, result, mc, pc, core); - model_ref mdl1 = alloc(model, m); - model_ref mdl2 = (*mc)(*mdl1); - expr_ref val(m); - mdl2->eval(x, val); + 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 = 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(u, 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 tst_get_consequences() {