From d060359f01b06c19bd4d65c4ba73d0f5c2393fc7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 18 Oct 2016 22:34:34 -0400 Subject: [PATCH] add fd solver for finite domain queries Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/ast/rewriter/CMakeLists.txt | 1 + .../cmake/src/tactic/portfolio/CMakeLists.txt | 1 + src/ast/expr_functors.h | 8 + src/ast/rewriter/fd_rewriter.cpp | 292 ++++++++++++++++++ src/ast/rewriter/fd_rewriter.h | 48 +++ src/cmd_context/check_logic.cpp | 17 +- src/cmd_context/cmd_context.cpp | 5 +- src/sat/sat_solver.cpp | 9 +- src/sat/sat_solver/inc_sat_solver.cpp | 2 +- src/tactic/bv/dt2bv_tactic.cpp | 228 +++----------- src/tactic/bv/dt2bv_tactic.h | 2 +- src/tactic/extension_model_converter.cpp | 2 +- src/tactic/portfolio/fd_solver.cpp | 161 ++++++++++ src/tactic/portfolio/fd_solver.h | 29 ++ src/tactic/portfolio/smt_strategic_solver.cpp | 4 +- src/test/get_consequences.cpp | 71 ++++- 16 files changed, 676 insertions(+), 204 deletions(-) create mode 100644 src/ast/rewriter/fd_rewriter.cpp create mode 100644 src/ast/rewriter/fd_rewriter.h create mode 100644 src/tactic/portfolio/fd_solver.cpp create mode 100644 src/tactic/portfolio/fd_solver.h diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt index 47323d821..b01a0e016 100644 --- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt +++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt @@ -12,6 +12,7 @@ z3_add_component(rewriter expr_replacer.cpp expr_safe_replace.cpp factor_rewriter.cpp + fd_rewriter.cpp fpa_rewriter.cpp label_rewriter.cpp mk_simplified_app.cpp diff --git a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt index d20af772b..201cdcf0f 100644 --- a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt +++ b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt @@ -1,6 +1,7 @@ z3_add_component(portfolio SOURCES default_tactic.cpp + fd_solver.cpp smt_strategic_solver.cpp COMPONENT_DEPENDENCIES aig_tactic diff --git a/src/ast/expr_functors.h b/src/ast/expr_functors.h index 32560e139..da2b43dea 100644 --- a/src/ast/expr_functors.h +++ b/src/ast/expr_functors.h @@ -31,6 +31,14 @@ public: virtual ~i_expr_pred() {} }; + +class i_sort_pred { +public: + virtual bool operator()(sort* s) = 0; + virtual ~i_sort_pred() {} +}; + + /** \brief Memoizing predicate functor on sub-expressions. diff --git a/src/ast/rewriter/fd_rewriter.cpp b/src/ast/rewriter/fd_rewriter.cpp new file mode 100644 index 000000000..026387e22 --- /dev/null +++ b/src/ast/rewriter/fd_rewriter.cpp @@ -0,0 +1,292 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + fd_rewriter.cpp + +Abstract: + + Conversion from enumeration types to bit-vectors. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-18 + +Notes: + +--*/ + +#include"rewriter.h" +#include"rewriter_def.h" +#include"fd_rewriter.h" +#include"ast_util.h" +#include"ast_pp.h" + +struct fd_rewriter::imp { + ast_manager& m; + params_ref m_params; + obj_map m_enum2bv; + obj_map m_bv2enum; + obj_map m_enum2def; + expr_ref_vector m_bounds; + datatype_util m_dt; + func_decl_ref_vector m_enum_consts; + func_decl_ref_vector m_enum_bvs; + expr_ref_vector m_enum_defs; + unsigned_vector m_enum_consts_lim; + unsigned m_num_translated; + i_sort_pred* m_sort_pred; + + struct rw_cfg : public default_rewriter_cfg { + imp& m_imp; + ast_manager& m; + datatype_util m_dt; + bv_util m_bv; + + rw_cfg(imp& i, ast_manager & m) : + m_imp(i), + m(m), + m_dt(m), + m_bv(m) + {} + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + expr_ref a0(m), a1(m); + expr_ref_vector _args(m); + if (m.is_eq(f) && reduce_arg(args[0], a0) && reduce_arg(args[1], a1)) { + result = m.mk_eq(a0, a1); + return BR_DONE; + } + else if (m.is_distinct(f) && reduce_args(num, args, _args)) { + result = m.mk_distinct(_args.size(), _args.c_ptr()); + return BR_DONE; + } + else if (m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) { + unsigned idx = m_dt.get_recognizer_constructor_idx(f); + a1 = m_bv.mk_numeral(rational(idx), get_sort(a0)); + result = m.mk_eq(a0, a1); + return BR_DONE; + } + else { + check_for_fd(num, args); + return BR_FAILED; + } + } + + bool reduce_args(unsigned sz, expr*const* as, expr_ref_vector& result) { + expr_ref tmp(m); + for (unsigned i = 0; i < sz; ++i) { + if (!reduce_arg(as[i], tmp)) return false; + result.push_back(tmp); + } + return true; + } + + void throw_non_fd(expr* e) { + std::stringstream strm; + strm << "unabled nested data-type expression " << mk_pp(e, m); + throw rewriter_exception(strm.str().c_str()); + } + + void check_for_fd(unsigned n, expr* const* args) { + for (unsigned i = 0; i < n; ++i) { + if (m_imp.is_fd(get_sort(args[i]))) { + throw_non_fd(args[i]); + } + } + } + + bool reduce_arg(expr* a, expr_ref& result) { + + sort* s = get_sort(a); + if (!m_imp.is_fd(s)) { + return false; + } + unsigned bv_size = get_bv_size(s); + + if (is_var(a)) { + result = m.mk_var(to_var(a)->get_idx(), m_bv.mk_sort(bv_size)); + return true; + } + SASSERT(is_app(a)); + func_decl* f = to_app(a)->get_decl(); + if (m_dt.is_constructor(f)) { + unsigned idx = m_dt.get_constructor_idx(f); + result = m_bv.mk_numeral(idx, bv_size); + } + else if (is_uninterp_const(a)) { + func_decl* f_fresh; + if (m_imp.m_enum2bv.find(f, f_fresh)) { + result = m.mk_const(f_fresh); + return true; + } + + // create a fresh variable, add bounds constraints for it. + unsigned nc = m_dt.get_datatype_num_constructors(s); + result = m.mk_fresh_const(f->get_name().str().c_str(), m_bv.mk_sort(bv_size)); + f_fresh = to_app(result)->get_decl(); + if (!is_power_of_two(nc)) { + m_imp.m_bounds.push_back(m_bv.mk_ule(result, m_bv.mk_numeral(nc-1, bv_size))); + } + expr_ref f_def(m); + ptr_vector const& cs = *m_dt.get_datatype_constructors(s); + f_def = m.mk_const(cs[nc-1]); + for (unsigned i = nc - 1; i > 0; ) { + --i; + f_def = m.mk_ite(m.mk_eq(result, m_bv.mk_numeral(i,bv_size)), m.mk_const(cs[i]), f_def); + } + m_imp.m_enum2def.insert(f, f_def); + m_imp.m_enum2bv.insert(f, f_fresh); + m_imp.m_bv2enum.insert(f_fresh, f); + m_imp.m_enum_consts.push_back(f); + m_imp.m_enum_bvs.push_back(f_fresh); + m_imp.m_enum_defs.push_back(f_def); + } + else { + throw_non_fd(a); + } + ++m_imp.m_num_translated; + return true; + } + + ptr_buffer m_sorts; + + bool reduce_quantifier( + quantifier * q, + expr * old_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + m_sorts.reset(); + expr_ref_vector bounds(m); + bool found = false; + for (unsigned i = 0; i < q->get_num_decls(); ++i) { + sort* s = q->get_decl_sort(i); + if (m_imp.is_fd(s)) { + unsigned bv_size = get_bv_size(s); + m_sorts.push_back(m_bv.mk_sort(bv_size)); + unsigned nc = m_dt.get_datatype_num_constructors(s); + if (!is_power_of_two(nc)) { + bounds.push_back(m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_bv.mk_numeral(nc-1, bv_size))); + } + found = true; + } + else { + m_sorts.push_back(s); + } + } + if (!found) { + return false; + } + expr_ref new_body_ref(old_body, m), tmp(m); + if (!bounds.empty()) { + if (q->is_forall()) { + new_body_ref = m.mk_implies(mk_and(bounds), new_body_ref); + } + else { + bounds.push_back(new_body_ref); + new_body_ref = mk_and(bounds); + } + } + result = m.mk_quantifier(q->is_forall(), q->get_num_decls(), m_sorts.c_ptr(), q->get_decl_names(), new_body_ref, + q->get_weight(), q->get_qid(), q->get_skid(), + q->get_num_patterns(), new_patterns, + q->get_num_no_patterns(), new_no_patterns); + result_pr = 0; + return true; + } + + unsigned get_bv_size(sort* s) { + unsigned nc = m_dt.get_datatype_num_constructors(s); + unsigned bv_size = 1; + while ((unsigned)(1 << bv_size) < nc) { + ++bv_size; + } + return bv_size; + } + }; + + struct rw : public rewriter_tpl { + rw_cfg m_cfg; + + rw(imp& t, ast_manager & m, params_ref const & p) : + rewriter_tpl(m, m.proofs_enabled(), m_cfg), + m_cfg(t, m) { + } + }; + + rw m_rw; + + imp(ast_manager& m, params_ref const& p): + m(m), m_params(p), m_bounds(m), + m_dt(m), + m_enum_consts(m), + m_enum_bvs(m), + m_enum_defs(m), + m_num_translated(0), + m_sort_pred(0), + m_rw(*this, m, p) { + } + + void updt_params(params_ref const & p) {} + unsigned get_num_steps() const { return m_rw.get_num_steps(); } + void cleanup() { m_rw.cleanup(); } + void operator()(expr * e, expr_ref & result, proof_ref & result_proof) { + m_rw(e, result, result_proof); + } + void push() { + m_enum_consts_lim.push_back(m_enum_consts.size()); + } + void pop(unsigned num_scopes) { + SASSERT(m_bounds.empty()); // bounds must be flushed before pop. + if (num_scopes > 0) { + SASSERT(num_scopes <= m_enum_consts_lim.size()); + unsigned new_sz = m_enum_consts_lim.size() - num_scopes; + unsigned lim = m_enum_consts_lim[new_sz]; + for (unsigned i = m_enum_consts.size(); i > lim; ) { + --i; + func_decl* f = m_enum_consts[i].get(); + func_decl* f_fresh = m_enum2bv.find(f); + m_bv2enum.erase(f_fresh); + m_enum2bv.erase(f); + m_enum2def.erase(f); + } + m_enum_consts_lim.resize(new_sz); + m_enum_consts.resize(lim); + m_enum_defs.resize(lim); + m_enum_bvs.resize(lim); + } + } + + void flush_side_constraints(expr_ref_vector& side_constraints) { + side_constraints.append(m_bounds); + m_bounds.reset(); + } + + bool is_fd(sort* s) { + return m_dt.is_enum_sort(s) && (!m_sort_pred || (*m_sort_pred)(s)); + } + + void set_is_fd(i_sort_pred* sp) { + m_sort_pred = sp; + } +}; + + +fd_rewriter::fd_rewriter(ast_manager & m, params_ref const& p) { m_imp = alloc(imp, m, p); } +fd_rewriter::~fd_rewriter() { dealloc(m_imp); } +void fd_rewriter::updt_params(params_ref const & p) { m_imp->updt_params(p); } +ast_manager & fd_rewriter::m() const { return m_imp->m; } +unsigned fd_rewriter::get_num_steps() const { return m_imp->get_num_steps(); } +void fd_rewriter::cleanup() { ast_manager& mgr = m(); params_ref p = m_imp->m_params; dealloc(m_imp); m_imp = alloc(imp, mgr, p); } +obj_map const& fd_rewriter::enum2bv() const { return m_imp->m_enum2bv; } +obj_map const& fd_rewriter::bv2enum() const { return m_imp->m_bv2enum; } +obj_map const& fd_rewriter::enum2def() const { return m_imp->m_enum2def; } +void fd_rewriter::operator()(expr * e, expr_ref & result, proof_ref & result_proof) { (*m_imp)(e, result, result_proof); } +void fd_rewriter::push() { m_imp->push(); } +void fd_rewriter::pop(unsigned num_scopes) { m_imp->pop(num_scopes); } +void fd_rewriter::flush_side_constraints(expr_ref_vector& side_constraints) { m_imp->flush_side_constraints(side_constraints); } +unsigned fd_rewriter::num_translated() const { return m_imp->m_num_translated; } +void fd_rewriter::set_is_fd(i_sort_pred* sp) const { m_imp->set_is_fd(sp); } diff --git a/src/ast/rewriter/fd_rewriter.h b/src/ast/rewriter/fd_rewriter.h new file mode 100644 index 000000000..3d4ecae9c --- /dev/null +++ b/src/ast/rewriter/fd_rewriter.h @@ -0,0 +1,48 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + fd_rewriter.h + +Abstract: + + Conversion from enumeration types to bit-vectors. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-18 + +Notes: + +--*/ +#ifndef ENUM_REWRITER_H_ +#define ENUM_REWRITER_H_ + +#include"datatype_decl_plugin.h" +#include"rewriter_types.h" +#include"expr_functors.h" + +class fd_rewriter { + struct imp; + imp* m_imp; +public: + fd_rewriter(ast_manager & m, params_ref const& p); + ~fd_rewriter(); + + void updt_params(params_ref const & p); + ast_manager & m() const; + unsigned get_num_steps() const; + void cleanup(); + obj_map const& enum2bv() const; + obj_map const& bv2enum() const; + obj_map const& enum2def() const; + void operator()(expr * e, expr_ref & result, proof_ref & result_proof); + void push(); + void pop(unsigned num_scopes); + void flush_side_constraints(expr_ref_vector& side_constraints); + unsigned num_translated() const; + void set_is_fd(i_sort_pred* sp) const; +}; + +#endif diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index 733689ac9..7a49f8fd0 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -21,8 +21,10 @@ Revision History: #include"array_decl_plugin.h" #include"bv_decl_plugin.h" #include"seq_decl_plugin.h" +#include"datatype_decl_plugin.h" #include"ast_pp.h" #include"for_each_expr.h" +#include struct check_logic::imp { ast_manager & m; @@ -31,6 +33,7 @@ struct check_logic::imp { bv_util m_bv_util; array_util m_ar_util; seq_util m_seq_util; + datatype_util m_dt_util; bool m_uf; // true if the logic supports uninterpreted functions bool m_arrays; // true if the logic supports arbitrary arrays bool m_bv_arrays; // true if the logic supports only bv arrays @@ -42,7 +45,7 @@ struct check_logic::imp { bool m_quantifiers; // true if the logic supports quantifiers bool m_unknown_logic; - imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m) { + imp(ast_manager & _m):m(_m), m_a_util(m), m_bv_util(m), m_ar_util(m), m_seq_util(m), m_dt_util(m) { reset(); } @@ -178,6 +181,11 @@ struct check_logic::imp { m_reals = true; m_quantifiers = false; } + else if (logic == "QF_FD") { + m_bvs = true; + m_uf = true; + m_ints = true; + } else { m_unknown_logic = true; } @@ -432,8 +440,13 @@ struct check_logic::imp { else if (fid == m_seq_util.get_family_id()) { // nothing to check } + else if (fid == m_dt_util.get_family_id() && m_logic == "QF_FD") { + // nothing to check + } else { - fail("logic does not support theory"); + std::stringstream strm; + strm << "logic does not support theory " << m.get_family_name(fid); + fail(strm.str().c_str()); } } diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 3260f02b0..1df28b8e5 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -568,6 +568,7 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const { s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL" || + s == "QF_FD" || s == "HORN"; } @@ -622,7 +623,7 @@ bool cmd_context::logic_has_array() const { } bool cmd_context::logic_has_datatype() const { - return !has_logic(); + return !has_logic() || m_logic == "QF_FD"; } void cmd_context::init_manager_core(bool new_manager) { @@ -705,7 +706,7 @@ void cmd_context::init_external_manager() { } bool cmd_context::supported_logic(symbol const & s) const { - return s == "QF_UF" || s == "UF" || s == "ALL" || + return s == "QF_UF" || s == "UF" || s == "ALL" || s == "QF_FD" || logic_has_arith_core(s) || logic_has_bv_core(s) || logic_has_array_core(s) || logic_has_seq_core(s) || logic_has_horn(s) || logic_has_fpa_core(s); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 915080c4a..1e667eccc 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3135,6 +3135,7 @@ namespace sat { if (is_sat != l_true) { return is_sat; } + model mdl = get_model(); for (unsigned i = 0; i < vars.size(); ++i) { bool_var v = vars[i]; switch (get_model()[v]) { @@ -3143,7 +3144,9 @@ namespace sat { default: break; } } - return get_consequences(asms, lits, conseq); + is_sat = get_consequences(asms, lits, conseq); + set_model(mdl); + return is_sat; } lbool solver::get_consequences(literal_vector const& asms, literal_vector const& lits, vector& conseq) { @@ -3164,13 +3167,11 @@ namespace sat { while (!unfixed.empty()) { checkpoint(); literal_set::iterator it = unfixed.begin(), end = unfixed.end(); - unsigned chunk_size = 100; - for (; it != end && chunk_size > 0; ++it) { + for (; it != end; ++it) { literal lit = *it; if (value(lit) != l_undef) { continue; } - --chunk_size; push(); assign(~lit, justification()); propagate(false); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 83ccfcac4..349b60f55 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -580,7 +580,7 @@ private: } void extract_model() { - TRACE("sat", tout << "retrieve model\n";); + TRACE("sat", tout << "retrieve model " << (m_solver.model_is_current()?"present":"absent") << "\n";); if (!m_solver.model_is_current()) { m_model = 0; return; diff --git a/src/tactic/bv/dt2bv_tactic.cpp b/src/tactic/bv/dt2bv_tactic.cpp index ab9df78ad..d7d6c9811 100644 --- a/src/tactic/bv/dt2bv_tactic.cpp +++ b/src/tactic/bv/dt2bv_tactic.cpp @@ -29,6 +29,7 @@ Revision History: #include "extension_model_converter.h" #include "var_subst.h" #include "ast_util.h" +#include "fd_rewriter.h" class dt2bv_tactic : public tactic { @@ -39,177 +40,8 @@ class dt2bv_tactic : public tactic { bv_util m_bv; obj_hashtable m_fd_sorts; obj_hashtable m_non_fd_sorts; - expr_ref_vector m_bounds; - 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; - ast_manager& m; - params_ref m_params; - obj_map m_cache; - expr_ref_vector m_trail; - - rw_cfg(dt2bv_tactic& t, ast_manager & m, params_ref const & p) : - m_t(t), - m(m), - m_params(p), - m_trail(m) - {} - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - expr_ref a0(m), a1(m); - expr_ref_vector _args(m); - if (m.is_eq(f) && reduce_arg(args[0], a0) && reduce_arg(args[1], a1)) { - result = m.mk_eq(a0, a1); - return BR_DONE; - } - else if (m.is_distinct(f) && reduce_args(num, args, _args)) { - result = m.mk_distinct(_args.size(), _args.c_ptr()); - return BR_DONE; - } - else if (m_t.m_dt.is_recognizer(f) && reduce_arg(args[0], a0)) { - unsigned idx = m_t.m_dt.get_recognizer_constructor_idx(f); - a1 = m_t.m_bv.mk_numeral(rational(idx), get_sort(a0)); - result = m.mk_eq(a0, a1); - return BR_DONE; - } - else { - return BR_FAILED; - } - } - - bool reduce_args(unsigned sz, expr*const* as, expr_ref_vector& result) { - expr_ref tmp(m); - for (unsigned i = 0; i < sz; ++i) { - if (!reduce_arg(as[i], tmp)) return false; - result.push_back(tmp); - } - return true; - } - - bool reduce_arg(expr* a, expr_ref& result) { - expr* b; - if (m_cache.find(a, b)) { - result = b; - return true; - } - - sort* s = get_sort(a); - if (!m_t.m_fd_sorts.contains(s)) { - return false; - } - unsigned bv_size = get_bv_size(s); - - if (is_var(a)) { - result = m.mk_var(to_var(a)->get_idx(), m_t.m_bv.mk_sort(bv_size)); - return true; - } - SASSERT(is_app(a)); - func_decl* f = to_app(a)->get_decl(); - if (m_t.m_dt.is_constructor(f)) { - unsigned idx = m_t.m_dt.get_constructor_idx(f); - result = m_t.m_bv.mk_numeral(idx, bv_size); - } - else if (is_uninterp_const(a)) { - // create a fresh variable, add bounds constraints for it. - 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-1, bv_size))); - } - expr_ref f_def(m); - ptr_vector const& cs = *m_t.m_dt.get_datatype_constructors(s); - f_def = m.mk_const(cs[nc-1]); - for (unsigned i = nc - 1; i > 0; ) { - --i; - f_def = m.mk_ite(m.mk_eq(result, m_t.m_bv.mk_numeral(i,bv_size)), m.mk_const(cs[i]), f_def); - } - // 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; - } - m_cache.insert(a, result); - ++m_t.m_num_translated; - return true; - } - - ptr_buffer m_sorts; - - bool reduce_quantifier( - quantifier * q, - expr * old_body, - expr * const * new_patterns, - expr * const * new_no_patterns, - expr_ref & result, - proof_ref & result_pr) { - m_sorts.reset(); - expr_ref_vector bounds(m); - bool found = false; - for (unsigned i = 0; i < q->get_num_decls(); ++i) { - sort* s = q->get_decl_sort(i); - if (m_t.m_fd_sorts.contains(s)) { - unsigned bv_size = get_bv_size(s); - m_sorts.push_back(m_t.m_bv.mk_sort(bv_size)); - unsigned nc = m_t.m_dt.get_datatype_num_constructors(s); - if (!is_power_of_two(nc)) { - bounds.push_back(m_t.m_bv.mk_ule(m.mk_var(q->get_num_decls()-i-1, m_sorts[i]), m_t.m_bv.mk_numeral(nc, bv_size))); - } - found = true; - } - else { - m_sorts.push_back(s); - } - } - if (!found) { - return false; - } - expr_ref new_body_ref(old_body, m), tmp(m); - if (!bounds.empty()) { - if (q->is_forall()) { - new_body_ref = m.mk_implies(mk_and(bounds), new_body_ref); - } - else { - bounds.push_back(new_body_ref); - new_body_ref = mk_and(bounds); - } - } - result = m.mk_quantifier(q->is_forall(), q->get_num_decls(), m_sorts.c_ptr(), q->get_decl_names(), new_body_ref, - q->get_weight(), q->get_qid(), q->get_skid(), - q->get_num_patterns(), new_patterns, - q->get_num_no_patterns(), new_no_patterns); - result_pr = 0; - return true; - } - - unsigned get_bv_size(sort* s) { - unsigned nc = m_t.m_dt.get_datatype_num_constructors(s); - unsigned bv_size = 1; - while ((unsigned)(1 << bv_size) < nc) { - ++bv_size; - } - return bv_size; - } - }; - - struct rw : public rewriter_tpl { - rw_cfg m_cfg; - - rw(dt2bv_tactic& t, ast_manager & m, params_ref const & p) : - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(t, m, p) { - } - }; - - + obj_map* m_translate; + bool is_fd(expr* a) { return is_fd(get_sort(a)); } bool is_fd(sort* a) { return m_dt.is_enum_sort(a); } @@ -255,10 +87,20 @@ class dt2bv_tactic : public tactic { void operator()(quantifier* q) {} }; + struct sort_pred : public i_sort_pred { + dt2bv_tactic& m_t; + sort_pred(dt2bv_tactic& t): m_t(t) {} + virtual ~sort_pred() {} + virtual bool operator()(sort* s) { + return m_t.m_fd_sorts.contains(s); + } + }; + + 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_bounds(m), m_translate(tr) {} + 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) {} virtual tactic * translate(ast_manager & m) { return alloc(dt2bv_tactic, m, m_params, 0); @@ -289,26 +131,43 @@ public: m_fd_sorts.remove(*it); } if (!m_fd_sorts.empty()) { - m_bounds.reset(); - m_num_translated = 0; - m_ext = alloc(extension_model_converter, m); - m_filter = alloc(filter_model_converter, m); - scoped_ptr r = alloc(rw, *this, m, m_params); + ref ext = alloc(extension_model_converter, m); + ref filter = alloc(filter_model_converter, m); + fd_rewriter rw(m, m_params); + rw.set_is_fd(&m_is_fd); expr_ref new_curr(m); proof_ref new_pr(m); for (unsigned idx = 0; idx < size; idx++) { - (*r)(g->form(idx), new_curr, new_pr); + rw(g->form(idx), new_curr, new_pr); if (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_bounds.size(); ++i) { - g->assert_expr(m_bounds[i].get()); + expr_ref_vector bounds(m); + rw.flush_side_constraints(bounds); + for (unsigned i = 0; i < bounds.size(); ++i) { + g->assert_expr(bounds[i].get()); } - mc = concat(m_filter.get(), m_ext.get()); - report_tactic_progress(":fd-num-translated", m_num_translated); + { + 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); + } + } + } + { + obj_map::iterator it = rw.enum2def().begin(), end = rw.enum2def().end(); + for (; it != end; ++it) { + ext->insert(it->m_key, it->m_value); + } + } + + mc = concat(filter.get(), ext.get()); + report_tactic_progress(":fd-num-translated", rw.num_translated()); } g->inc_depth(); result.push_back(g.get()); @@ -319,11 +178,10 @@ public: virtual void cleanup() { m_fd_sorts.reset(); m_non_fd_sorts.reset(); - m_bounds.reset(); } }; -tactic * mk_dt2bv_tactic(ast_manager & m, params_ref const & p, obj_map* tr) { +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 a8fb33fe8..fd5aacda6 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(), 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/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp index cdd096455..345ea5cc9 100644 --- a/src/tactic/extension_model_converter.cpp +++ b/src/tactic/extension_model_converter.cpp @@ -71,7 +71,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { void extension_model_converter::insert(func_decl * v, expr * def) { m_vars.push_back(v); - m_defs.push_back(def); + m_defs.push_back(def); } diff --git a/src/tactic/portfolio/fd_solver.cpp b/src/tactic/portfolio/fd_solver.cpp new file mode 100644 index 000000000..9447c158c --- /dev/null +++ b/src/tactic/portfolio/fd_solver.cpp @@ -0,0 +1,161 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + fd_solver.cpp + +Abstract: + + Finite domain solver. + + Enumeration data-types are translated into bit-vectors, and then + the incremental sat-solver is applied to the resulting assertions. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-17 + +Notes: + +--*/ + +#include "fd_solver.h" +#include "solver_na2as.h" +#include "tactic.h" +#include "inc_sat_solver.h" +#include "bv_decl_plugin.h" +#include "datatype_decl_plugin.h" +#include "fd_rewriter.h" +#include "extension_model_converter.h" +#include "filter_model_converter.h" +#include "ast_pp.h" +#include "model_smt2_pp.h" + +class fd_solver : public solver_na2as { + ast_manager& m; + params_ref m_params; + ref m_solver; + fd_rewriter m_rewriter; + +public: + + fd_solver(ast_manager& m, params_ref const& p): + solver_na2as(m), + m(m), + m_params(p), + m_solver(mk_inc_sat_solver(m, p)), + m_rewriter(m, p) + { + } + + virtual ~fd_solver() {} + + virtual solver* translate(ast_manager& m, params_ref const& p) { + return alloc(fd_solver, m, p); + } + + virtual void assert_expr(expr * t) { + expr_ref tmp(t, m); + expr_ref_vector bounds(m); + proof_ref tmp_proof(m); + m_rewriter(t, tmp, tmp_proof); + m_solver->assert_expr(tmp); + m_rewriter.flush_side_constraints(bounds); + m_solver->assert_expr(bounds); + } + + virtual void push_core() { + m_rewriter.push(); + m_solver->push(); + } + + virtual void pop_core(unsigned n) { + m_solver->pop(n); + m_rewriter.pop(n); + } + + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + return m_solver->check_sat(num_assumptions, assumptions); + } + + virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } + virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } + virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } + virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); } + virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } + virtual void get_model(model_ref & mdl) { + m_solver->get_model(mdl); + if (mdl) { + extend_model(mdl); + filter_model(mdl); + } + } + virtual proof * get_proof() { return m_solver->get_proof(); } + virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } + virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } + virtual void get_labels(svector & r) { m_solver->get_labels(r); } + virtual ast_manager& get_manager() const { return m; } + virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { return m_solver->find_mutexes(vars, mutexes); } + + virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + + datatype_util dt(m); + bv_util bv(m); + + // translate enumeration constants to bit-vectors. + expr_ref_vector bvars(m), conseq(m); + for (unsigned i = 0; i < vars.size(); ++i) { + func_decl* f; + if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) { + bvars.push_back(m.mk_const(f)); + } + else { + bvars.push_back(vars[i]); + } + } + lbool r = m_solver->get_consequences(asms, bvars, consequences); + + // translate bit-vector consequences back to enumeration types + for (unsigned i = 0; i < consequences.size(); ++i) { + expr* a, *b, *u, *v; + func_decl* f; + rational num; + unsigned bvsize; + VERIFY(m.is_implies(consequences[i].get(), a, b)); + if (m.is_eq(b, u, v) && is_uninterp_const(u) && m_rewriter.bv2enum().find(to_app(u)->get_decl(), f) && bv.is_numeral(v, num, bvsize)) { + SASSERT(num.is_unsigned()); + expr_ref head(m); + ptr_vector const& enums = *dt.get_datatype_constructors(f->get_range()); + head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); + consequences[i] = m.mk_implies(a, head); + } + } + return r; + } + + void filter_model(model_ref& mdl) { + filter_model_converter filter(m); + obj_map::iterator it = m_rewriter.enum2bv().begin(), end = m_rewriter.enum2bv().end(); + for (; it != end; ++it) { + filter.insert(it->m_value); + } + filter(mdl, 0); + } + + void extend_model(model_ref& mdl) { + extension_model_converter ext(m); + obj_map::iterator it = m_rewriter.enum2def().begin(), end = m_rewriter.enum2def().end(); + for (; it != end; ++it) { + ext.insert(it->m_key, it->m_value); + + } + ext(mdl, 0); + } + +}; + +solver * mk_fd_solver(ast_manager & m, params_ref const & p) { + return alloc(fd_solver, m, p); +} diff --git a/src/tactic/portfolio/fd_solver.h b/src/tactic/portfolio/fd_solver.h new file mode 100644 index 000000000..51abb087f --- /dev/null +++ b/src/tactic/portfolio/fd_solver.h @@ -0,0 +1,29 @@ +/*++ +Copyright (c) 2016 Microsoft Corporation + +Module Name: + + fd_solver.h + +Abstract: + + Finite domain solver. + +Author: + + Nikolaj Bjorner (nbjorner) 2016-10-17 + +Notes: + +--*/ +#ifndef FD_SOLVER_H_ +#define FD_SOLVER_H_ + +#include"ast.h" +#include"params.h" + +class solver; + +solver * mk_fd_solver(ast_manager & m, params_ref const & p); + +#endif diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index f9334bcb2..81825221e 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -38,6 +38,7 @@ Notes: #include"horn_tactic.h" #include"smt_solver.h" #include"inc_sat_solver.h" +#include"fd_solver.h" #include"bv_rewriter.h" @@ -98,6 +99,8 @@ static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol bv_rewriter rw(m); if (logic == "QF_BV" && rw.hi_div0()) return mk_inc_sat_solver(m, p); + if (logic == "QF_FD") + return mk_fd_solver(m, p); return mk_smt_solver(m, p, logic); } @@ -116,7 +119,6 @@ public: tactic * t = mk_tactic_for_logic(m, p, l); return mk_combined_solver(mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, l), mk_solver_for_logic(m, p, l), - //mk_smt_solver(m, p, l), p); } }; diff --git a/src/test/get_consequences.cpp b/src/test/get_consequences.cpp index 24f3a5d38..8c35bcfb1 100644 --- a/src/test/get_consequences.cpp +++ b/src/test/get_consequences.cpp @@ -11,7 +11,7 @@ Copyright (c) 2016 Microsoft Corporation #include "dt2bv_tactic.h" #include "tactic.h" #include "model_smt2_pp.h" -//include +#include "fd_solver.h" static expr_ref mk_const(ast_manager& m, char const* name, sort* s) { return expr_ref(m.mk_const(symbol(name), s), m); @@ -81,8 +81,8 @@ static void test2() { 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; + obj_map tr; + obj_map rev_tr; ref dt2bv = mk_dt2bv_tactic(m, p, &tr); goal_ref_buffer result; model_converter_ref mc; @@ -91,13 +91,13 @@ static void test2() { (*dt2bv)(gl, result, mc, pc, core); // Collect translations from enumerations to bit-vectors - obj_map::iterator it = tr.begin(), end = tr.end(); + 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()); + val = m.mk_const(tr.find(to_app(x)->get_decl())); std::cout << val << "\n"; ptr_vector fmls; result[0]->get_formulas(fmls); @@ -119,7 +119,7 @@ static void test2() { 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)) { + 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()])); @@ -129,9 +129,66 @@ static void test2() { std::cout << conseq << "\n"; } +void test3() { + 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); + + ref fd_solver = mk_fd_solver(m, p); + fd_solver->assert_expr(m.mk_not(m.mk_eq(x, r))); + fd_solver->assert_expr(m.mk_not(m.mk_eq(x, b))); + + expr_ref_vector asms(m), vars(m), conseq(m); + vars.push_back(x); + vars.push_back(y); + + VERIFY(l_true == fd_solver->get_consequences(asms, vars, conseq)); + std::cout << conseq << "\n"; + conseq.reset(); + + fd_solver->push(); + fd_solver->assert_expr(m.mk_not(m.mk_eq(x, g))); + VERIFY(l_false == fd_solver->check_sat(0,0)); + fd_solver->pop(1); + + VERIFY(l_true == fd_solver->get_consequences(asms, vars, conseq)); + + std::cout << conseq << "\n"; + conseq.reset(); + + model_ref mr; + fd_solver->get_model(mr); + model_smt2_pp(std::cout << "model:\n", m, *mr.get(), 0); + + VERIFY(l_true == fd_solver->check_sat(0,0)); + fd_solver->get_model(mr); + SASSERT(mr.get()); + model_smt2_pp(std::cout, m, *mr.get(), 0); + +} + void tst_get_consequences() { test1(); test2(); - + test3(); }