diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 4a5514a7b..247d0a14c 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -61,6 +61,7 @@ z3_add_component(api api_rcf.cpp api_seq.cpp api_solver.cpp + api_special_relations.cpp api_stats.cpp api_tactic.cpp z3_replayer.cpp diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index cabfdb101..999ebab6b 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1052,6 +1052,17 @@ extern "C" { } } + if (mk_c(c)->get_special_relations_fid() == _d->get_family_id()) { + switch(_d->get_decl_kind()) { + case OP_SPECIAL_RELATION_LO : return Z3_OP_SPECIAL_RELATION_LO; + case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO; + case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO; + case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO; + default: UNREACHABLE(); + } + } + + if (mk_c(c)->get_bv_fid() == _d->get_family_id()) { switch(_d->get_decl_kind()) { case OP_BV_NUM: return Z3_OP_BNUM; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 71bebef73..811cb30ee 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -101,6 +101,7 @@ namespace api { m_datalog_fid = m().mk_family_id("datalog_relation"); m_fpa_fid = m().mk_family_id("fpa"); m_seq_fid = m().mk_family_id("seq"); + m_special_relations_fid = m().mk_family_id("special_relations"); m_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); install_tactics(*this); diff --git a/src/api/api_context.h b/src/api/api_context.h index 8bd75aaa0..1c4145810 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -30,6 +30,7 @@ Revision History: #include "ast/dl_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/recfun_decl_plugin.h" +#include "ast/special_relations_decl_plugin.h" #include "smt/smt_kernel.h" #include "smt/params/smt_params.h" #include "util/event_handler.h" @@ -106,6 +107,7 @@ namespace api { family_id m_pb_fid; family_id m_fpa_fid; family_id m_seq_fid; + family_id m_special_relations_fid; datatype_decl_plugin * m_dt_plugin; std::string m_string_buffer; // temporary buffer used to cache strings sent to the "external" world. @@ -162,6 +164,7 @@ namespace api { family_id get_fpa_fid() const { return m_fpa_fid; } family_id get_seq_fid() const { return m_seq_fid; } datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; } + family_id get_special_relations_fid() const { return m_special_relations_fid; } Z3_error_code get_error_code() const { return m_error_code; } void reset_error_code(); diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 0c2544643..d48ce76e2 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -160,69 +160,40 @@ extern "C" { LOG_Z3_mk_list_sort(c, name, elem_sort, nil_decl, is_nil_decl, cons_decl, is_cons_decl, head_decl, tail_decl); RESET_ERROR_CODE(); ast_manager& m = mk_c(c)->m(); + func_decl_ref nil(m), is_nil(m), cons(m), is_cons(m), head(m), tail(m); datatype_util& dt_util = mk_c(c)->dtutil(); mk_c(c)->reset_last_result(); - datatype_util data_util(m); - accessor_decl* head_tail[2] = { - mk_accessor_decl(m, symbol("head"), type_ref(to_sort(elem_sort))), - mk_accessor_decl(m, symbol("tail"), type_ref(0)) - }; - constructor_decl* constrs[2] = { - mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, nullptr), - // Leo: SMT 2.0 document uses 'insert' instead of cons - mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail) - }; - - sort_ref_vector sorts(m); - { - datatype_decl * decl = mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, 2, constrs); - bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &decl, 0, nullptr, sorts); - del_datatype_decl(decl); - - if (!is_ok) { - SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - RETURN_Z3(nullptr); - } + sort_ref s = dt_util.mk_list_datatype(to_sort(elem_sort), to_symbol(name), cons, is_cons, head, tail, nil, is_nil); + + if (!s) { + SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); + RETURN_Z3(nullptr); } - sort * s = sorts.get(0); mk_c(c)->save_multiple_ast_trail(s); - ptr_vector const& cnstrs = *data_util.get_datatype_constructors(s); - SASSERT(cnstrs.size() == 2); - func_decl* f; if (nil_decl) { - f = cnstrs[0]; - mk_c(c)->save_multiple_ast_trail(f); - *nil_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(nil); + *nil_decl = of_func_decl(nil); } if (is_nil_decl) { - f = data_util.get_constructor_is(cnstrs[0]); - mk_c(c)->save_multiple_ast_trail(f); - *is_nil_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(is_nil); + *is_nil_decl = of_func_decl(is_nil); } if (cons_decl) { - f = cnstrs[1]; - mk_c(c)->save_multiple_ast_trail(f); - *cons_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(cons); + *cons_decl = of_func_decl(cons); } if (is_cons_decl) { - f = data_util.get_constructor_is(cnstrs[1]); - mk_c(c)->save_multiple_ast_trail(f); - *is_cons_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(is_cons); + *is_cons_decl = of_func_decl(is_cons); } if (head_decl) { - ptr_vector const& acc = *data_util.get_constructor_accessors(cnstrs[1]); - SASSERT(acc.size() == 2); - f = (acc)[0]; - mk_c(c)->save_multiple_ast_trail(f); - *head_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(head); + *head_decl = of_func_decl(head); } if (tail_decl) { - ptr_vector const& acc = *data_util.get_constructor_accessors(cnstrs[1]); - SASSERT(acc.size() == 2); - f = (acc)[1]; - mk_c(c)->save_multiple_ast_trail(f); - *tail_decl = of_func_decl(f); + mk_c(c)->save_multiple_ast_trail(tail); + *tail_decl = of_func_decl(tail); } RETURN_Z3_mk_list_sort(of_sort(s)); Z3_CATCH_RETURN(nullptr); diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp new file mode 100644 index 000000000..e852c2b34 --- /dev/null +++ b/src/api/api_special_relations.cpp @@ -0,0 +1,88 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + api_special_relations.cpp + +Abstract: + Basic API for Special relations + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-25 + Ashutosh Gupta 2016 + +Revision History: + +--*/ + +#include +#include "api/z3.h" +#include "api/api_log_macros.h" +#include "api/api_context.h" +#include "api/api_util.h" +#include "ast/ast_pp.h" +#include "ast/special_relations_decl_plugin.h" + +extern "C" { + +#if 0 + bool Z3_API Z3_is_sr_lo(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_lo(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_lo( to_expr(s) )); + Z3_CATCH_RETURN(false); + } + + bool Z3_API Z3_is_sr_po(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_po(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_po( to_expr(s) )); + Z3_CATCH_RETURN(false); + } + + bool Z3_API Z3_is_sr_po_ao(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_po_ao(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_po_ao( to_expr(s) )); + Z3_CATCH_RETURN(false); + } + + bool Z3_API Z3_is_sr_plo(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_plo(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_plo( to_expr(s) )); + Z3_CATCH_RETURN(false); + } + + bool Z3_API Z3_is_sr_to(Z3_context c, Z3_ast s) { + Z3_TRY; + LOG_Z3_is_sr_to(c, s); + RESET_ERROR_CODE(); + RETURN_Z3(mk_c(c)->sr_util().is_to( to_expr(s) )); + Z3_CATCH_RETURN(false); + } +#endif +#define MK_TERN(NAME, FID) \ + Z3_ast Z3_API NAME(Z3_context c, unsigned index, Z3_ast a, Z3_ast b) { \ + LOG_ ##NAME(c, index, a, b); \ + Z3_TRY; \ + expr* args[2] = { to_expr(a), to_expr(b) }; \ + parameter p(index); \ + ast* a = mk_c(c)->m().mk_app(mk_c(c)->get_special_relations_fid(), FID, 1, &p, 2, args); \ + mk_c(c)->save_ast_trail(a); \ + RETURN_Z3(of_ast(a)); \ + Z3_CATCH_RETURN(nullptr); \ +} + + MK_TERN(Z3_mk_linear_order, OP_SPECIAL_RELATION_LO); + MK_TERN(Z3_mk_partial_order, OP_SPECIAL_RELATION_PO); + MK_TERN(Z3_mk_piecewise_linear_order, OP_SPECIAL_RELATION_PLO); + MK_TERN(Z3_mk_tree_order, OP_SPECIAL_RELATION_TO); + +}; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4992015de..8df43d477 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1707,6 +1707,27 @@ namespace z3 { */ inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); } + typedef Z3_ast Z3_apply_order(Z3_context, unsigned, Z3_ast, Z3_ast); + + inline expr apply_order(Z3_apply_order app, unsigned index, expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = app(a.ctx(), index, a, b); + a.check_error(); + return expr(a.ctx(), r); + } + inline expr linear_order(unsigned index, expr const& a, expr const& b) { + return apply_order(Z3_mk_linear_order, index, a, b); + } + inline expr partial_order(unsigned index, expr const& a, expr const& b) { + return apply_order(Z3_mk_partial_order, index, a, b); + } + inline expr piecewise_linear_order(unsigned index, expr const& a, expr const& b) { + return apply_order(Z3_mk_piecewise_linear_order, index, a, b); + } + inline expr tree_order(unsigned index, expr const& a, expr const& b) { + return apply_order(Z3_mk_tree_order, index, a, b); + } + template class cast_ast; template<> class cast_ast { diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index e3995ddb5..267a24a20 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -10353,3 +10353,6 @@ def Range(lo, hi, ctx = None): lo = _coerce_seq(lo, ctx) hi = _coerce_seq(hi, ctx) return ReRef(Z3_mk_re_range(lo.ctx_ref(), lo.ast, hi.ast), lo.ctx) + +# Special Relations + diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e17378d94..e1fe76175 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1101,6 +1101,12 @@ typedef enum { Z3_OP_BUREM_I, Z3_OP_BSMOD_I, + // Special relations + Z3_OP_SPECIAL_RELATION_LO, + Z3_OP_SPECIAL_RELATION_PO, + Z3_OP_SPECIAL_RELATION_PLO, + Z3_OP_SPECIAL_RELATION_TO, + // Proofs Z3_OP_PR_UNDEF = 0x500, Z3_OP_PR_TRUE, @@ -3595,10 +3601,50 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re); - /*@}*/ + /** @name Special relations */ + /*@{*/ + /** + \brief declare \c a and \c b are in linear order over a relation indexed by \c id. + + \pre a and b are of same type. + + + def_API('Z3_mk_linear_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_linear_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are in partial order over a relation indexed by \c id. + + \pre a and b are of same type. + + def_API('Z3_mk_partial_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_partial_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are in piecewise linear order indexed by relation \c id. + + \pre a and b are of same type. + + def_API('Z3_mk_piecewise_linear_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_piecewise_linear_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are in tree order indexed by \c id. + + \pre a and b are of same type. + + def_API('Z3_mk_tree_order', AST ,(_in(CONTEXT), _in(UINT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_tree_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b); + + /*@}*/ + /** @name Quantifiers */ /*@{*/ /** diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 56ab78b8a..0bcc4d847 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -41,6 +41,7 @@ z3_add_component(ast reg_decl_plugins.cpp seq_decl_plugin.cpp shared_occs.cpp + special_relations_decl_plugin.cpp static_features.cpp used_vars.cpp well_sorted.cpp diff --git a/src/ast/ast.h b/src/ast/ast.h index 1c25ff9ec..baefc4685 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2122,6 +2122,7 @@ public: app * mk_or(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2); } app * mk_and(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2); } app * mk_or(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_OR, arg1, arg2, arg3); } + app * mk_or(expr* a, expr* b, expr* c, expr* d) { expr* args[4] = { a, b, c, d }; return mk_app(m_basic_family_id, OP_OR, 4, args); } app * mk_and(expr * arg1, expr * arg2, expr * arg3) { return mk_app(m_basic_family_id, OP_AND, arg1, arg2, arg3); } app * mk_implies(expr * arg1, expr * arg2) { return mk_app(m_basic_family_id, OP_IMPLIES, arg1, arg2); } app * mk_not(expr * n) { return mk_app(m_basic_family_id, OP_NOT, n); } diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index a45c65d82..a8c9131c7 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -111,6 +111,17 @@ app * mk_and(ast_manager & m, unsigned num_args, app * const * args); inline app_ref mk_and(app_ref_vector const& args) { return app_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); } inline expr_ref mk_and(expr_ref_vector const& args) { return expr_ref(mk_and(args.get_manager(), args.size(), args.c_ptr()), args.get_manager()); } +inline app_ref operator&(expr_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); } +inline app_ref operator&(app_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); } +inline app_ref operator&(var_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); } +inline app_ref operator&(quantifier_ref& a, expr* b) { return app_ref(a.m().mk_and(a, b), a.m()); } + +inline app_ref operator|(expr_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); } +inline app_ref operator|(app_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); } +inline app_ref operator|(var_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); } +inline app_ref operator|(quantifier_ref& a, expr* b) { return app_ref(a.m().mk_or(a, b), a.m()); } + + /** Return (or args[0] ... args[num_args-1]) if num_args >= 2 Return args[0] if num_args == 1 @@ -129,6 +140,10 @@ expr * mk_not(ast_manager & m, expr * arg); expr_ref mk_not(const expr_ref& e); +inline expr_ref not(const expr_ref& e) { return mk_not(e); } +inline app_ref not(const app_ref& e) { return app_ref(e.m().mk_not(e), e.m()); } + + /** Negate and push over conjunction or disjunction. */ diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 71b35f914..e8f276aa8 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -1188,6 +1188,85 @@ namespace datatype { } } } + + sort_ref util::mk_list_datatype(sort* elem, symbol const& name, + func_decl_ref& cons, func_decl_ref& is_cons, + func_decl_ref& hd, func_decl_ref& tl, + func_decl_ref& nil, func_decl_ref& is_nil) { + + accessor_decl* head_tail[2] = { + mk_accessor_decl(m, symbol("head"), type_ref(elem)), + mk_accessor_decl(m, symbol("tail"), type_ref(0)) + }; + constructor_decl* constrs[2] = { + mk_constructor_decl(symbol("nil"), symbol("is_nil"), 0, nullptr), + mk_constructor_decl(symbol("cons"), symbol("is_cons"), 2, head_tail) + }; + decl::plugin& p = *get_plugin(); + + sort_ref_vector sorts(m); + datatype_decl * decl = mk_datatype_decl(*this, name, 0, nullptr, 2, constrs); + bool is_ok = p.mk_datatypes(1, &decl, 0, nullptr, sorts); + del_datatype_decl(decl); + + if (!is_ok) { + return sort_ref(m); + } + sort* s = sorts.get(0); + ptr_vector const& cnstrs = *get_datatype_constructors(s); + SASSERT(cnstrs.size() == 2); + nil = cnstrs[0]; + is_nil = get_constructor_is(cnstrs[0]); + cons = cnstrs[1]; + is_cons = get_constructor_is(cnstrs[1]); + ptr_vector const& acc = *get_constructor_accessors(cnstrs[1]); + SASSERT(acc.size() == 2); + hd = acc[0]; + tl = acc[1]; + return sort_ref(s, m); + } + + sort_ref util::mk_pair_datatype(sort* a, sort* b, func_decl_ref& fst, func_decl_ref& snd, func_decl_ref& pair) { + type_ref t1(a), t2(b); + accessor_decl* fstd = mk_accessor_decl(m, symbol("fst"), t1); + accessor_decl* sndd = mk_accessor_decl(m, symbol("snd"), t2); + accessor_decl* accd[2] = { fstd, sndd }; + auto * p = mk_constructor_decl(symbol("pair"), symbol("is-pair"), 2, accd); + auto* dt = mk_datatype_decl(*this, symbol("pair"), 0, nullptr, 1, &p); + sort_ref_vector sorts(m); + VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts)); + del_datatype_decl(dt); + sort* s = sorts.get(0); + ptr_vector const& cnstrs = *get_datatype_constructors(s); + SASSERT(cnstrs.size() == 1); + ptr_vector const& acc = *get_constructor_accessors(cnstrs[0]); + SASSERT(acc.size() == 2); + fst = acc[0]; + snd = acc[1]; + pair = cnstrs[0]; + return sort_ref(s, m); + } + + sort_ref util::mk_tuple_datatype(svector> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs) { + ptr_vector accd; + for (auto const& e : elems) { + type_ref t(e.second); + accd.push_back(mk_accessor_decl(m, e.first, t)); + } + auto* tuple = mk_constructor_decl(name, test, accd.size(), accd.c_ptr()); + auto* dt = mk_datatype_decl(*this, name, 0, nullptr, 1, &tuple); + sort_ref_vector sorts(m); + VERIFY(get_plugin()->mk_datatypes(1, &dt, 0, nullptr, sorts)); + del_datatype_decl(dt); + sort* s = sorts.get(0); + ptr_vector const& cnstrs = *get_datatype_constructors(s); + SASSERT(cnstrs.size() == 1); + ptr_vector const& acc = *get_constructor_accessors(cnstrs[0]); + for (auto* f : acc) accs.push_back(f); + tup = cnstrs[0]; + return sort_ref(s, m); + } + } datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs) { diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index e9734ac0b..5292ab6b9 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -364,6 +364,12 @@ namespace datatype { decl::plugin* get_plugin() { return m_plugin; } void get_defs(sort* s, ptr_vector& defs); def const& get_def(sort* s) const; + sort_ref mk_list_datatype(sort* elem, symbol const& name, + func_decl_ref& cons, func_decl_ref& is_cons, + func_decl_ref& hd, func_decl_ref& tl, + func_decl_ref& nil, func_decl_ref& is_nil); + sort_ref mk_pair_datatype(sort* a, sort* b, func_decl_ref& fst, func_decl_ref& snd, func_decl_ref& pair); + sort_ref mk_tuple_datatype(svector> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs); }; }; diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp index 5cd3542df..8ae0dcbf2 100644 --- a/src/ast/pattern/expr_pattern_match.cpp +++ b/src/ast/pattern/expr_pattern_match.cpp @@ -52,35 +52,57 @@ expr_pattern_match::match_quantifier(quantifier* qf, app_ref_vector& patterns, u } m_regs[0] = qf->get_expr(); for (unsigned i = 0; i < m_precompiled.size(); ++i) { - quantifier* qf2 = m_precompiled[i].get(); - if (qf2->get_kind() != qf->get_kind() || is_lambda(qf)) { - continue; - } - if (qf2->get_num_decls() != qf->get_num_decls()) { - continue; - } - subst s; - if (match(qf->get_expr(), m_first_instrs[i], s)) { - for (unsigned j = 0; j < qf2->get_num_patterns(); ++j) { - app* p = static_cast(qf2->get_pattern(j)); - expr_ref p_result(m_manager); - instantiate(p, qf->get_num_decls(), s, p_result); - patterns.push_back(to_app(p_result.get())); - } - weight = qf2->get_weight(); - return true; + if (match_quantifier(i, qf, patterns, weight)) + return true; + } + return false; +} + +bool +expr_pattern_match::match_quantifier(unsigned i, quantifier* qf, app_ref_vector& patterns, unsigned& weight) { + quantifier* qf2 = m_precompiled[i].get(); + if (qf2->get_kind() != qf->get_kind() || is_lambda(qf)) { + return false; + } + if (qf2->get_num_decls() != qf->get_num_decls()) { + return false; + } + subst s; + if (match(qf->get_expr(), m_first_instrs[i], s)) { + for (unsigned j = 0; j < qf2->get_num_patterns(); ++j) { + app* p = static_cast(qf2->get_pattern(j)); + expr_ref p_result(m_manager); + instantiate(p, qf->get_num_decls(), s, p_result); + patterns.push_back(to_app(p_result.get())); } + weight = qf2->get_weight(); + return true; } return false; } +bool expr_pattern_match::match_quantifier_index(quantifier* qf, app_ref_vector& patterns, unsigned& index) { + if (m_regs.empty()) return false; + m_regs[0] = qf->get_expr(); + + for (unsigned i = 0; i < m_precompiled.size(); ++i) { + unsigned weight = 0; + if (match_quantifier(i, qf, patterns, weight)) { + index = i; + return true; + } + } + return false; +} + + void expr_pattern_match::instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result) { bound b; for (unsigned i = 0; i < num_bound; ++i) { b.insert(m_bound_dom[i], m_bound_rng[i]); } - + TRACE("expr_pattern_match", tout << mk_pp(a, m_manager) << " " << num_bound << "\n";); inst_proc proc(m_manager, s, b, m_regs); for_each_ast(proc, a); expr* v = nullptr; @@ -251,11 +273,7 @@ expr_pattern_match::match(expr* a, unsigned init, subst& s) break; } case CHECK_BOUND: - TRACE("expr_pattern_match", - tout - << "check bound " - << pc.m_num_bound << " " << pc.m_reg; - ); + TRACE("expr_pattern_match", tout << "check bound " << pc.m_num_bound << " " << pc.m_reg << "\n";); ok = m_bound_rng[pc.m_num_bound] == m_regs[pc.m_reg]; break; case BIND: @@ -396,11 +414,18 @@ expr_pattern_match::initialize(char const * spec_string) { for (expr * e : ctx.assertions()) { compile(e); } - TRACE("expr_pattern_match", display(tout); ); } -void -expr_pattern_match::display(std::ostream& out) const { +unsigned expr_pattern_match::initialize(quantifier* q) { + if (m_instrs.empty()) { + m_instrs.push_back(instr(BACKTRACK)); + } + compile(q); + return m_precompiled.size() - 1; +} + + +void expr_pattern_match::display(std::ostream& out) const { for (unsigned i = 0; i < m_instrs.size(); ++i) { display(out, m_instrs[i]); } @@ -414,7 +439,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const { break; case BIND: out << "bind "; - out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " "; out << mk_pp(pc.m_pat, m_manager) << "\n"; out << "next: " << pc.m_next << "\n"; out << "offset: " << pc.m_offset << "\n"; @@ -422,7 +446,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const { break; case BIND_AC: out << "bind_ac "; - out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " "; out << mk_pp(pc.m_pat, m_manager) << "\n"; out << "next: " << pc.m_next << "\n"; out << "offset: " << pc.m_offset << "\n"; @@ -430,7 +453,6 @@ expr_pattern_match::display(std::ostream& out, instr const& pc) const { break; case BIND_C: out << "bind_c "; - out << mk_pp(to_app(pc.m_pat)->get_decl(), m_manager) << " "; out << mk_pp(pc.m_pat, m_manager) << "\n"; out << "next: " << pc.m_next << "\n"; out << "offset: " << pc.m_offset << "\n"; diff --git a/src/ast/pattern/expr_pattern_match.h b/src/ast/pattern/expr_pattern_match.h index d1388b43f..6c472d708 100644 --- a/src/ast/pattern/expr_pattern_match.h +++ b/src/ast/pattern/expr_pattern_match.h @@ -80,13 +80,7 @@ class expr_pattern_match { } void operator()(var* v) { - var* b = nullptr; - if (m_bound.find(v, b)) { - m_memoize.insert(v, b); - } - else { - UNREACHABLE(); - } + m_memoize.insert(v, m_bound[v]); } void operator()(app * n) { @@ -98,15 +92,9 @@ class expr_pattern_match { if (m_subst.find(decl, r)) { decl = to_app(m_regs[r])->get_decl(); } - for (unsigned i = 0; i < num_args; ++i) { - expr* arg = nullptr; - if (m_memoize.find(n->get_arg(i), arg)) { - SASSERT(arg); - args.push_back(arg); - } - else { - UNREACHABLE(); - } + for (expr* arg : *n) { + arg = m_memoize[arg]; + args.push_back(arg); } if (m_manager.is_pattern(n)) { result = m_manager.mk_pattern(num_args, reinterpret_cast(args.c_ptr())); @@ -116,7 +104,6 @@ class expr_pattern_match { } m_pinned.push_back(result); m_memoize.insert(n, result); - return; } }; @@ -131,11 +118,14 @@ class expr_pattern_match { public: expr_pattern_match(ast_manager & manager); ~expr_pattern_match(); - virtual bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight); - virtual void initialize(char const * database); + bool match_quantifier(quantifier * qf, app_ref_vector & patterns, unsigned & weight); + bool match_quantifier_index(quantifier* qf, app_ref_vector & patterns, unsigned& index); + unsigned initialize(quantifier* qf); + void initialize(char const * database); void display(std::ostream& out) const; private: + bool match_quantifier(unsigned i, quantifier * qf, app_ref_vector & patterns, unsigned & weight); void instantiate(expr* a, unsigned num_bound, subst& s, expr_ref& result); void compile(expr* q); bool match(expr* a, unsigned init, subst& s); diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index ebdf86ca5..bdaf3fcf0 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -316,6 +316,7 @@ namespace recfun { return alloc(def, m(), m_fid, name, n, domain, range); } + void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) { d.set_definition(subst, n_vars, vars, rhs); } @@ -384,7 +385,17 @@ namespace recfun { promise_def plugin::mk_def(symbol const& name, unsigned n, sort *const * params, sort * range) { def* d = u().decl_fun(name, n, params, range); - SASSERT(! m_defs.contains(d->get_decl())); + SASSERT(!m_defs.contains(d->get_decl())); + m_defs.insert(d->get_decl(), d); + return promise_def(&u(), d); + } + + promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range) { + def* d = u().decl_fun(name, n, params, range); + def* d2 = nullptr; + if (m_defs.find(d->get_decl(), d2)) { + dealloc(d2); + } m_defs.insert(d->get_decl(), d); return promise_def(&u(), d); } diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h index b294cdfce..33b5294f5 100644 --- a/src/ast/recfun_decl_plugin.h +++ b/src/ast/recfun_decl_plugin.h @@ -172,6 +172,8 @@ namespace recfun { unsigned arity, sort * const * domain, sort * range) override; promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range); + + promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range); void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs); @@ -223,7 +225,6 @@ namespace recfun { //has_def(f)); return m_plugin->get_def(f); diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index 9f98ff0ed..d506c75b3 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -19,6 +19,7 @@ z3_add_component(rewriter factor_equivs.cpp factor_rewriter.cpp fpa_rewriter.cpp + func_decl_replace.cpp hoist_rewriter.cpp inj_axiom.cpp label_rewriter.cpp diff --git a/src/ast/rewriter/func_decl_replace.cpp b/src/ast/rewriter/func_decl_replace.cpp new file mode 100644 index 000000000..97451cb58 --- /dev/null +++ b/src/ast/rewriter/func_decl_replace.cpp @@ -0,0 +1,97 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + func_decl_replace.cpp + +Abstract: + + Replace functions in expressions. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-28 + +Revision History: + + +--*/ + + +#include "ast/rewriter/func_decl_replace.h" + +expr_ref func_decl_replace::operator()(expr* e) { + m_todo.push_back(e); + + while (!m_todo.empty()) { + expr* a = m_todo.back(), *b; + if (m_cache.contains(a)) { + m_todo.pop_back(); + } + else if (is_var(a)) { + m_cache.insert(a, a); + m_todo.pop_back(); + } + else if (is_app(a)) { + app* c = to_app(a); + unsigned n = c->get_num_args(); + m_args.reset(); + bool arg_differs = false; + for (unsigned i = 0; i < n; ++i) { + expr* d = nullptr, *arg = c->get_arg(i); + if (m_cache.find(arg, d)) { + m_args.push_back(d); + arg_differs |= arg != d; + SASSERT(m.get_sort(arg) == m.get_sort(d)); + } + else { + m_todo.push_back(arg); + } + } + if (m_args.size() == n) { + if (arg_differs) { + b = m.mk_app(c->get_decl(), m_args.size(), m_args.c_ptr()); + m_refs.push_back(b); + SASSERT(m.get_sort(a) == m.get_sort(b)); + } else { + b = a; + } + func_decl* f = nullptr; + if (m_subst.find(c->get_decl(), f)) { + b = m.mk_app(f, m_args.size(), m_args.c_ptr()); + m_refs.push_back(b); + } + m_cache.insert(a, b); + m_todo.pop_back(); + } + } + else { + quantifier* q = to_quantifier(a); + SASSERT(is_quantifier(a)); + expr* body = q->get_expr(), *new_body; + if (m_cache.find(body, new_body)) { + if (new_body == body) { + b = a; + } + else { + b = m.update_quantifier(q, new_body); + m_refs.push_back(b); + } + m_cache.insert(a, b); + m_todo.pop_back(); + } + else { + m_todo.push_back(body); + } + } + } + return expr_ref(m_cache.find(e), m); +} + +void func_decl_replace::reset() { + m_cache.reset(); + m_subst.reset(); + m_refs.reset(); + m_funs.reset(); +} diff --git a/src/ast/rewriter/func_decl_replace.h b/src/ast/rewriter/func_decl_replace.h new file mode 100644 index 000000000..7f37e8753 --- /dev/null +++ b/src/ast/rewriter/func_decl_replace.h @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + func_decl_replace.h + +Abstract: + + Replace functions in expressions. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-28 + +Revision History: + + +--*/ + +#ifndef FUNC_DECL_REPLACE_H_ +#define FUNC_DECL_REPLACE_H_ + +#include "ast/ast.h" + +class func_decl_replace { + ast_manager& m; + obj_map m_subst; + obj_map m_cache; + ptr_vector m_todo, m_args; + expr_ref_vector m_refs; + func_decl_ref_vector m_funs; + +public: + func_decl_replace(ast_manager& m): m(m), m_refs(m), m_funs(m) {} + + void insert(func_decl* src, func_decl* dst) { m_subst.insert(src, dst); m_funs.push_back(src), m_funs.push_back(dst); } + + expr_ref operator()(expr* e); + + void reset(); + + bool empty() const { return m_subst.empty(); } +}; + +#endif /* FUNC_DECL_REPLACE_H_ */ diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp new file mode 100644 index 000000000..6dd0af1b4 --- /dev/null +++ b/src/ast/special_relations_decl_plugin.cpp @@ -0,0 +1,75 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + special_relations_decl_plugin.cpp + +Abstract: + + + +Author: + + Nikolaj Bjorner (nbjorner) 2015-15-9. + +Revision History: + +--*/ + +#include +#include "ast/ast.h" +#include "ast/special_relations_decl_plugin.h" + + + +special_relations_decl_plugin::special_relations_decl_plugin(): + m_lo("linear-order"), + m_po("partial-order"), + m_plo("piecewise-linear-order"), + m_to("tree-order") +{} + +func_decl * special_relations_decl_plugin::mk_func_decl( + decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) +{ + if (arity != 2) { + m_manager->raise_exception("special relations should have arity 2"); + return nullptr; + } + if (domain[0] != domain[1]) { + m_manager->raise_exception("argument sort missmatch"); + return nullptr; + } + func_decl_info info(m_family_id, k, num_parameters, parameters); + symbol name; + switch(k) { + case OP_SPECIAL_RELATION_PO: name = m_po; break; + case OP_SPECIAL_RELATION_LO: name = m_lo; break; + case OP_SPECIAL_RELATION_PLO: name = m_plo; break; + case OP_SPECIAL_RELATION_TO: name = m_to; break; + } + return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), info); +} + +void special_relations_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { + if (logic == symbol::null) { + op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO)); + op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO)); + op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO)); + op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO)); + } +} + +sr_property special_relations_util::get_property(func_decl* f) const { + switch (f->get_decl_kind()) { + case OP_SPECIAL_RELATION_PO: return sr_po; + case OP_SPECIAL_RELATION_LO: return sr_lo; + case OP_SPECIAL_RELATION_PLO: return sr_plo; + case OP_SPECIAL_RELATION_TO: return sr_to; + default: + UNREACHABLE(); + return sr_po; + } +} diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h new file mode 100644 index 000000000..5926057f5 --- /dev/null +++ b/src/ast/special_relations_decl_plugin.h @@ -0,0 +1,99 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + special_relations_decl_plugin.h + +Abstract: + + + +Author: + + Nikolaj Bjorner (nbjorner) 2015-15-9. + Ashutosh Gupta 2016 + +Revision History: + +--*/ +#ifndef SPECIAL_RELATIONS_DECL_PLUGIN_H_ +#define SPECIAL_RELATIONS_DECL_PLUGIN_H_ + +#include "ast/ast.h" + + +enum special_relations_op_kind { + OP_SPECIAL_RELATION_LO, + OP_SPECIAL_RELATION_PO, + OP_SPECIAL_RELATION_PLO, + OP_SPECIAL_RELATION_TO, + LAST_SPECIAL_RELATIONS_OP +}; + +class special_relations_decl_plugin : public decl_plugin { + symbol m_lo; + symbol m_po; + symbol m_plo; + symbol m_to; +public: + special_relations_decl_plugin(); + + ~special_relations_decl_plugin() override {} + + decl_plugin * mk_fresh() override { + return alloc(special_relations_decl_plugin); + } + + func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) override; + + void get_op_names(svector & op_names, symbol const & logic) override; + + sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override { return nullptr; } +}; + +enum sr_property { + sr_none = 0x00, + sr_transitive = 0x01, // Rxy & Ryz -> Rxz + sr_reflexive = 0x02, // Rxx + sr_antisymmetric = 0x04, // Rxy & Ryx -> x = y + sr_lefttree = 0x08, // Ryx & Rzx -> Ryz | Rzy + sr_righttree = 0x10, // Rxy & Rxz -> Ryx | Rzy + sr_total = 0x20, // Rxy | Ryx + sr_po = 0x01 | 0x02 | 0x04, // partial order + sr_to = 0x01 | 0x02 | 0x04 | 0x10, // right-tree + sr_plo = 0x01 | 0x02 | 0x04 | 0x08 | 0x10, // piecewise linear order + sr_lo = 0x01 | 0x02 | 0x04 | 0x20, // linear order +}; + +class special_relations_util { + ast_manager& m; + family_id m_fid; +public: + special_relations_util(ast_manager& m) : m(m), m_fid(m.get_family_id("special_relations")) {} + + bool is_special_relation(func_decl* f) const { return f->get_family_id() == m_fid; } + bool is_special_relation(app* e) const { return is_special_relation(e->get_decl()); } + sr_property get_property(func_decl* f) const; + sr_property get_property(app* e) const { return get_property(e->get_decl()); } + + func_decl* mk_to_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_TO, 1, &p, 2, f->get_domain(), f->get_range()); } + func_decl* mk_po_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_PO, 1, &p, 2, f->get_domain(), f->get_range()); } + func_decl* mk_plo_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_PLO, 1, &p, 2, f->get_domain(), f->get_range()); } + func_decl* mk_lo_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_LO, 1, &p, 2, f->get_domain(), f->get_range()); } + + bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); } + bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); } + bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); } + bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); } + + app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO, arg1, arg2); } + app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO, arg1, arg2); } + app * mk_plo(expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PLO, arg1, arg2); } + app * mk_to (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_TO, arg1, arg2); } + +}; + + +#endif /* SPECIAL_RELATIONS_DECL_PLUGIN_H_ */ diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index e3530b4b5..e86475252 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -30,6 +30,7 @@ static_features::static_features(ast_manager & m): m_afid(m.mk_family_id("arith")), m_lfid(m.mk_family_id("label")), m_arrfid(m.mk_family_id("array")), + m_srfid(m.mk_family_id("special_relations")), m_label_sym("label"), m_pattern_sym("pattern"), m_expr_list_sym("expr-list") { @@ -78,6 +79,7 @@ void static_features::reset() { m_has_real = false; m_has_bv = false; m_has_fpa = false; + m_has_sr = false; m_has_str = false; m_has_seq_non_str = false; m_has_arrays = false; @@ -274,6 +276,8 @@ void static_features::update_core(expr * e) { m_has_bv = true; if (!m_has_fpa && (m_fpautil.is_float(e) || m_fpautil.is_rm(e))) m_has_fpa = true; + if (is_app(e) && to_app(e)->get_family_id() == m_srfid) + m_has_sr = true; if (!m_has_arrays && m_arrayutil.is_array(e)) m_has_arrays = true; if (!m_has_ext_arrays && m_arrayutil.is_array(e) && @@ -281,9 +285,8 @@ void static_features::update_core(expr * e) { m_has_ext_arrays = true; if (!m_has_str && m_sequtil.str.is_string_term(e)) m_has_str = true; - if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) { + if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) m_has_seq_non_str = true; - } if (is_app(e)) { family_id fid = to_app(e)->get_family_id(); mark_theory(fid); diff --git a/src/ast/static_features.h b/src/ast/static_features.h index 197947026..047c429b7 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -25,6 +25,7 @@ Revision History: #include "ast/array_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/seq_decl_plugin.h" +#include "ast/special_relations_decl_plugin.h" #include "util/map.h" struct static_features { @@ -38,6 +39,7 @@ struct static_features { family_id m_afid; family_id m_lfid; family_id m_arrfid; + family_id m_srfid; ast_mark m_already_visited; bool m_cnf; unsigned m_num_exprs; // @@ -79,6 +81,7 @@ struct static_features { bool m_has_real; // bool m_has_bv; // bool m_has_fpa; // + bool m_has_sr; // has special relations bool m_has_str; // has String-typed terms bool m_has_seq_non_str; // has non-String-typed Sequence terms bool m_has_arrays; // diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 9de183ca8..9fbeced71 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -31,6 +31,7 @@ Notes: #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/csp_decl_plugin.h" +#include "ast/special_relations_decl_plugin.h" #include "ast/ast_pp.h" #include "ast/rewriter/var_subst.h" #include "ast/pp.h" @@ -687,6 +688,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); register_plugin(symbol("csp"), alloc(csp_decl_plugin), smt_logics::logic_is_csp(m_logic)); + register_plugin(symbol("special_relations"), alloc(special_relations_decl_plugin), !has_logic()); } else { // the manager was created by an external module @@ -703,6 +705,7 @@ void cmd_context::init_manager_core(bool new_manager) { load_plugin(symbol("fpa"), logic_has_fpa(), fids); load_plugin(symbol("pb"), logic_has_pb(), fids); load_plugin(symbol("csp"), smt_logics::logic_is_csp(m_logic), fids); + for (family_id fid : fids) { decl_plugin * p = m_manager->get_plugin(fid); if (p) { diff --git a/src/model/model.cpp b/src/model/model.cpp index e6a3ffedf..aa3976cb9 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -217,6 +217,7 @@ void model::compress() { } } if (removed.empty()) break; + TRACE("model", tout << "remove\n"; for (func_decl* f : removed) tout << f->get_name() << "\n";); remove_decls(m_decls, removed); remove_decls(m_func_decls, removed); remove_decls(m_const_decls, removed); diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index d92e81421..0f811034a 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -66,6 +66,7 @@ void model_core::register_decl(func_decl * d, expr * v) { } void model_core::register_decl(func_decl * d, func_interp * fi) { + TRACE("model", tout << "register " << d->get_name() << "\n";); SASSERT(d->get_arity() > 0); SASSERT(&fi->m() == &m); decl2finterp::obj_map_entry * entry = m_finterp.insert_if_not_there2(d, nullptr); diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 52d3a5943..adc348633 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -62,6 +62,7 @@ z3_add_component(smt theory_pb.cpp theory_recfun.cpp theory_seq.cpp + theory_special_relations.cpp theory_str.cpp theory_utvpi.cpp theory_wmaxsat.cpp diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 44e858219..605390cf1 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -228,10 +228,7 @@ class dl_graph { int n = m_out_edges.size(); for (dl_var id = 0; id < n; id++) { const edge_id_vector & e_ids = m_out_edges[id]; - edge_id_vector::const_iterator it = e_ids.begin(); - edge_id_vector::const_iterator end = e_ids.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : e_ids) { SASSERT(static_cast(e_id) <= m_edges.size()); const edge & e = m_edges[e_id]; SASSERT(e.get_source() == id); @@ -239,10 +236,7 @@ class dl_graph { } for (dl_var id = 0; id < n; id++) { const edge_id_vector & e_ids = m_in_edges[id]; - edge_id_vector::const_iterator it = e_ids.begin(); - edge_id_vector::const_iterator end = e_ids.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : e_ids) { SASSERT(static_cast(e_id) <= m_edges.size()); const edge & e = m_edges[e_id]; SASSERT(e.get_target() == id); @@ -296,6 +290,9 @@ public: numeral const& get_weight(edge_id id) const { return m_edges[id].get_weight(); } + edge_id_vector const& get_out_edges(dl_var v) const { return m_out_edges[v]; } + + edge_id_vector const& get_in_edges(dl_var v) const { return m_in_edges[v]; } private: // An assignment is almost feasible if all but edge with idt edge are feasible. @@ -327,17 +324,16 @@ private: // Store in gamma the normalized weight. The normalized weight is given // by the formula // m_assignment[e.get_source()] - m_assignment[e.get_target()] + e.get_weight() - void set_gamma(const edge & e, numeral & gamma) { + numeral& set_gamma(const edge & e, numeral & gamma) { gamma = m_assignment[e.get_source()]; gamma -= m_assignment[e.get_target()]; gamma += e.get_weight(); + return gamma; } void reset_marks() { - dl_var_vector::iterator it = m_visited.begin(); - dl_var_vector::iterator end = m_visited.end(); - for (; it != end; ++it) { - m_mark[*it] = DL_UNMARKED; + for (dl_var v : m_visited) { + m_mark[v] = DL_UNMARKED; } m_visited.reset(); } @@ -378,7 +374,7 @@ private: TRACE("arith", tout << id << "\n";); dl_var source = target; - for(;;) { + while (true) { ++m_stats.m_propagation_cost; if (m_mark[root] != DL_UNMARKED) { // negative cycle was found @@ -389,10 +385,7 @@ private: return false; } - typename edge_id_vector::iterator it = m_out_edges[source].begin(); - typename edge_id_vector::iterator end = m_out_edges[source].end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_out_edges[source]) { edge & e = m_edges[e_id]; SASSERT(e.get_source() == source); if (!e.is_enabled()) { @@ -442,10 +435,7 @@ private: dl_var src = e->get_source(); dl_var dst = e->get_target(); numeral w = e->get_weight(); - typename edge_id_vector::iterator it = m_out_edges[src].begin(); - typename edge_id_vector::iterator end = m_out_edges[src].end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_out_edges[src]) { edge const& e2 = m_edges[e_id]; if (e2.get_target() == dst && e2.is_enabled() && // or at least not be inconsistent with current choices @@ -595,10 +585,7 @@ public: // // search for edges that can reduce size of negative cycle. // - typename edge_id_vector::iterator it = m_out_edges[src].begin(); - typename edge_id_vector::iterator end = m_out_edges[src].end(); - for (; it != end; ++it) { - edge_id e_id2 = *it; + for (edge_id e_id2 : m_out_edges[src]) { edge const& e2 = m_edges[e_id2]; dl_var src2 = e2.get_target(); if (e_id2 == e_id || !e2.is_enabled()) { @@ -661,6 +648,121 @@ public: } } + bool can_reach(dl_var src, dl_var dst) { + uint_set target, visited; + target.insert(dst); + return reachable(src, target, visited, dst); + } + + bool reachable(dl_var start, uint_set const& target, uint_set& visited, dl_var& dst) { + visited.reset(); + svector nodes; + nodes.push_back(start); + for (dl_var n : nodes) { + if (visited.contains(n)) continue; + visited.insert(n); + edge_id_vector & edges = m_out_edges[n]; + for (edge_id e_id : edges) { + edge & e = m_edges[e_id]; + if (e.is_enabled()) { + dst = e.get_target(); + if (target.contains(dst)) { + return true; + } + nodes.push_back(dst); + } + } + } + return false; + } + +private: + svector m_freq_hybrid; + int m_total_count = 0; + int m_run_counter = -1; + svector m_hybrid_visited, m_hybrid_parent; + + bool is_connected(numeral const& gamma, bool zero_edge, edge const& e, unsigned timestamp) const { + return (gamma.is_zero() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp; + } + + int_vector bfs_todo; + int_vector dfs_todo; + +public: + + + template + bool find_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { + auto zero_edge = true; + unsigned bfs_head = 0; + bfs_todo.reset(); + dfs_todo.reset(); + m_hybrid_visited.resize(m_assignment.size(), m_run_counter++); + m_hybrid_parent.resize(m_assignment.size(), -1); + bfs_todo.push_back(source); + m_hybrid_parent[source] = -1; + m_hybrid_visited[source] = m_run_counter; + numeral gamma; + while (bfs_head < bfs_todo.size() || !dfs_todo.empty()) { + m_total_count++; + dl_var v; + if (!dfs_todo.empty()) { + v = dfs_todo.back(); + dfs_todo.pop_back(); + } + else { + v = bfs_todo[bfs_head++]; + } + + edge_id_vector & edges = m_out_edges[v]; + for (edge_id e_id : edges) { + edge & e = m_edges[e_id]; + SASSERT(e.get_source() == v); + if (!e.is_enabled()) { + continue; + } + set_gamma(e, gamma); + if (is_connected(gamma, zero_edge, e, timestamp)) { + dl_var curr_target = e.get_target(); + if (curr_target == target) { + f(e.get_explanation()); + m_freq_hybrid[e_id]++; + while (true) { + int p = m_hybrid_parent[v]; + if (p == -1) + return true; + + edge_id eid; + bool ret = get_edge_id(p, v, eid); + if (eid == null_edge_id || !ret) { + return true; + } + else { + edge & e = m_edges[eid]; + f(e.get_explanation()); + m_freq_hybrid[eid]++; + v = p; + } + } + } + else if (m_hybrid_visited[curr_target] != m_run_counter) { + if (m_freq_hybrid[e_id] > 1) { + dfs_todo.push_back(curr_target); + } + else { + bfs_todo.push_back(curr_target); + } + m_hybrid_visited[curr_target] = m_run_counter; + m_hybrid_parent[curr_target] = v; + } + } + } + } + return false; + + } + // // Create fresh literals obtained by resolving a pair (or more) // literals associated with the edges. @@ -795,10 +897,8 @@ public: SASSERT(is_feasible()); if (!m_assignment[v].is_zero()) { numeral k = m_assignment[v]; - typename assignment::iterator it = m_assignment.begin(); - typename assignment::iterator end = m_assignment.end(); - for (; it != end; ++it) { - *it -= k; + for (auto& a : m_assignment) { + a -= k; } SASSERT(is_feasible()); } @@ -853,10 +953,7 @@ public: void display_agl(std::ostream & out) const { uint_set vars; - typename edges::const_iterator it = m_edges.begin(); - typename edges::const_iterator end = m_edges.end(); - for (; it != end; ++it) { - edge const& e = *it; + for (edge const& e : m_edges) { if (e.is_enabled()) { vars.insert(e.get_source()); vars.insert(e.get_target()); @@ -870,9 +967,7 @@ public: out << "\"" << v << "\" [label=\"" << v << ":" << m_assignment[v] << "\"]\n"; } } - it = m_edges.begin(); - for (; it != end; ++it) { - edge const& e = *it; + for (edge const& e : m_edges) { if (e.is_enabled()) { out << "\"" << e.get_source() << "\"->\"" << e.get_target() << "\"[label=\"" << e.get_weight() << "\"]\n"; } @@ -888,22 +983,19 @@ public: } void display_edges(std::ostream & out) const { - typename edges::const_iterator it = m_edges.begin(); - typename edges::const_iterator end = m_edges.end(); - for (; it != end; ++it) { - edge const& e = *it; + for (edge const& e : m_edges) { if (e.is_enabled()) { display_edge(out, e); } } } - void display_edge(std::ostream & out, edge_id id) const { - display_edge(out, m_edges[id]); + std::ostream& display_edge(std::ostream & out, edge_id id) const { + return display_edge(out, m_edges[id]); } - void display_edge(std::ostream & out, const edge & e) const { - out << e.get_explanation() << " (<= (- $" << e.get_target() << " $" << e.get_source() << ") " << e.get_weight() << ") " << e.get_timestamp() << "\n"; + std::ostream& display_edge(std::ostream & out, const edge & e) const { + return out << e.get_explanation() << " (<= (- $" << e.get_target() << " $" << e.get_source() << ") " << e.get_weight() << ") " << e.get_timestamp() << "\n"; } template @@ -920,11 +1012,8 @@ public: // If there is such edge, then the weight is stored in w and the explanation in ex. bool get_edge_weight(dl_var source, dl_var target, numeral & w, explanation & ex) { edge_id_vector & edges = m_out_edges[source]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); bool found = false; - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges) { edge & e = m_edges[e_id]; if (e.is_enabled() && e.get_target() == target && (!found || e.get_weight() < w)) { w = e.get_weight(); @@ -939,12 +1028,10 @@ public: // If there is such edge, return its edge_id in parameter id. bool get_edge_id(dl_var source, dl_var target, edge_id & id) const { edge_id_vector const & edges = m_out_edges[source]; - typename edge_id_vector::const_iterator it = edges.begin(); - typename edge_id_vector::const_iterator end = edges.end(); - for (; it != end; ++it) { - id = *it; - edge const & e = m_edges[id]; + for (edge_id e_id : edges) { + edge const & e = m_edges[e_id]; if (e.get_target() == target) { + id = e_id; return true; } } @@ -958,18 +1045,14 @@ public: void get_neighbours_undirected(dl_var current, svector & neighbours) { neighbours.reset(); edge_id_vector & out_edges = m_out_edges[current]; - typename edge_id_vector::iterator it = out_edges.begin(), end = out_edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : out_edges) { edge & e = m_edges[e_id]; SASSERT(e.get_source() == current); dl_var neighbour = e.get_target(); neighbours.push_back(neighbour); } edge_id_vector & in_edges = m_in_edges[current]; - typename edge_id_vector::iterator it2 = in_edges.begin(), end2 = in_edges.end(); - for (; it2 != end2; ++it2) { - edge_id e_id = *it2; + for (edge_id e_id : in_edges) { edge & e = m_edges[e_id]; SASSERT(e.get_target() == current); dl_var neighbour = e.get_source(); @@ -1052,10 +1135,7 @@ public: template void enumerate_edges(dl_var source, dl_var target, Functor& f) { edge_id_vector & edges = m_out_edges[source]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges) { edge const& e = m_edges[e_id]; if (e.get_target() == target) { f(e.get_weight(), e.get_explanation()); @@ -1112,10 +1192,7 @@ public: m_roots.push_back(v); numeral gamma; edge_id_vector & edges = m_out_edges[v]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges) { edge & e = m_edges[e_id]; if (!e.is_enabled()) { continue; @@ -1165,20 +1242,11 @@ public: m_dfs_time[v] = 0; succ.push_back(v); numeral gamma; - for (unsigned i = 0; i < succ.size(); ++i) { - v = succ[i]; - edge_id_vector & edges = m_out_edges[v]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; - edge & e = m_edges[e_id]; - if (!e.is_enabled()) { - continue; - } - SASSERT(e.get_source() == v); - set_gamma(e, gamma); - if (gamma.is_zero()) { + for (dl_var w : succ) { + for (edge_id e_id : m_out_edges[w]) { + edge & e = m_edges[e_id]; + if (e.is_enabled() && set_gamma(e, gamma).is_zero()) { + SASSERT(e.get_source() == w); dl_var target = e.get_target(); if (m_dfs_time[target] == -1) { succ.push_back(target); @@ -1269,50 +1337,57 @@ private: m_edge_id(e) { } }; - + public: // Find the shortest path from source to target using (normalized) zero edges with timestamp less than the given timestamp. // The functor f is applied on every explanation attached to the edges in the shortest path. + // Return true if the path exists, false otherwise. + + // Return true if the path exists, false otherwise. template bool find_shortest_zero_edge_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { + return find_shortest_path_aux(source, target, timestamp, f, true); + } + + template + bool find_shortest_reachable_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { + return find_shortest_path_aux(source, target, timestamp, f, false); + } + + template + bool find_shortest_path_aux(dl_var source, dl_var target, unsigned timestamp, Functor & f, bool zero_edge) { svector bfs_todo; - svector bfs_mark; + svector bfs_mark; bfs_mark.resize(m_assignment.size(), false); bfs_todo.push_back(bfs_elem(source, -1, null_edge_id)); bfs_mark[source] = true; - unsigned m_head = 0; numeral gamma; - while (m_head < bfs_todo.size()) { - bfs_elem & curr = bfs_todo[m_head]; - int parent_idx = m_head; - m_head++; - dl_var v = curr.m_var; + for (unsigned head = 0; head < bfs_todo.size(); ++head) { + bfs_elem & curr = bfs_todo[head]; + int parent_idx = head; + dl_var v = curr.m_var; TRACE("dl_bfs", tout << "processing: " << v << "\n";); edge_id_vector & edges = m_out_edges[v]; - typename edge_id_vector::iterator it = edges.begin(); - typename edge_id_vector::iterator end = edges.end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges) { edge & e = m_edges[e_id]; SASSERT(e.get_source() == v); if (!e.is_enabled()) { continue; } set_gamma(e, gamma); - TRACE("dl_bfs", tout << "processing edge: "; display_edge(tout, e); tout << "gamma: " << gamma << "\n";); - if (gamma.is_zero() && e.get_timestamp() < timestamp) { + TRACE("dl_bfs", display_edge(tout << "processing edge: ", e) << " gamma: " << gamma << "\n";); + if (is_connected(gamma, zero_edge, e, timestamp)) { dl_var curr_target = e.get_target(); - TRACE("dl_bfs", tout << "curr_target: " << curr_target << - ", mark: " << static_cast(bfs_mark[curr_target]) << "\n";); + TRACE("dl_bfs", tout << "curr_target: " << curr_target << ", mark: " << bfs_mark[curr_target] << "\n";); if (curr_target == target) { TRACE("dl_bfs", tout << "found path\n";); TRACE("dl_eq_bug", tout << "path: " << source << " --> " << target << "\n"; display_edge(tout, e); int tmp_parent_idx = parent_idx; - for (;;) { + while (true) { bfs_elem & curr = bfs_todo[tmp_parent_idx]; if (curr.m_edge_id == null_edge_id) { break; @@ -1322,11 +1397,10 @@ public: display_edge(tout, e); tmp_parent_idx = curr.m_parent_idx; } - tout.flush(); }); TRACE("dl_eq_bug", display_edge(tout, e);); f(e.get_explanation()); - for (;;) { + while (true) { SASSERT(parent_idx >= 0); bfs_elem & curr = bfs_todo[parent_idx]; if (curr.m_edge_id == null_edge_id) { @@ -1340,11 +1414,9 @@ public: } } } - else { - if (!bfs_mark[curr_target]) { - bfs_todo.push_back(bfs_elem(curr_target, parent_idx, e_id)); - bfs_mark[curr_target] = true; - } + else if (!bfs_mark[curr_target]) { + bfs_todo.push_back(bfs_elem(curr_target, parent_idx, e_id)); + bfs_mark[curr_target] = true; } } } @@ -1430,8 +1502,7 @@ private: numeral get_reduced_weight(dfs_state& state, dl_var n, edge const& e) { numeral gamma; - set_gamma(e, gamma); - return state.m_delta[n] + gamma; + return state.m_delta[n] + set_gamma(e, gamma); } template @@ -1477,11 +1548,7 @@ private: } TRACE("diff_logic", tout << "source: " << source << "\n";); - typename edge_id_vector::const_iterator it = edges[source].begin(); - typename edge_id_vector::const_iterator end = edges[source].end(); - - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges[source]) { edge const& e = m_edges[e_id]; if (&e == &e_init) { @@ -1569,11 +1636,9 @@ private: tout << "\n"; }); - typename heap::const_iterator it = state.m_heap.begin(); - typename heap::const_iterator end = state.m_heap.end(); - for (; it != end; ++it) { - SASSERT(m_mark[*it] != DL_PROP_UNMARKED); - m_mark[*it] = DL_PROP_UNMARKED;; + for (auto & s : state.m_heap) { + SASSERT(m_mark[s] != DL_PROP_UNMARKED); + m_mark[s] = DL_PROP_UNMARKED;; } state.m_heap.reset(); SASSERT(marks_are_clear()); @@ -1592,11 +1657,8 @@ private: for (unsigned i = 0; i < src.m_visited.size(); ++i) { dl_var c = src.m_visited[i]; - typename edge_id_vector::const_iterator it = edges[c].begin(); - typename edge_id_vector::const_iterator end = edges[c].end(); numeral n1 = n0 + src.m_delta[c] - m_assignment[c]; - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : edges[c]) { edge const& e1 = m_edges[e_id]; SASSERT(c == e1.get_source()); if (e1.is_enabled()) { @@ -1644,13 +1706,10 @@ public: edge_id_vector& out_edges = m_out_edges[src]; edge_id_vector& in_edges = m_in_edges[dst]; numeral w = e1.get_weight(); - typename edge_id_vector::const_iterator it, end; if (out_edges.size() < in_edges.size()) { - end = out_edges.end(); - for (it = out_edges.begin(); it != end; ++it) { + for (edge_id e_id : out_edges) { ++m_stats.m_implied_literal_cost; - edge_id e_id = *it; edge const& e2 = m_edges[e_id]; if (e_id != id && !e2.is_enabled() && e2.get_target() == dst && e2.get_weight() >= w) { subsumed.push_back(e_id); @@ -1659,10 +1718,8 @@ public: } } else { - end = in_edges.end(); - for (it = in_edges.begin(); it != end; ++it) { + for (edge_id e_id : in_edges) { ++m_stats.m_implied_literal_cost; - edge_id e_id = *it; edge const& e2 = m_edges[e_id]; if (e_id != id && !e2.is_enabled() && e2.get_source() == src && e2.get_weight() >= w) { subsumed.push_back(e_id); @@ -1696,20 +1753,14 @@ public: find_subsumed1(id, subsumed); typename edge_id_vector::const_iterator it, end, it3, end3; - it = m_in_edges[src].begin(); - end = m_in_edges[src].end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_in_edges[src]) { edge const& e2 = m_edges[e_id]; if (!e2.is_enabled() || e2.get_source() == dst) { continue; } w2 = e2.get_weight() + w; - it3 = m_out_edges[e2.get_source()].begin(); - end3 = m_out_edges[e2.get_source()].end(); - for (; it3 != end3; ++it3) { + for (edge_id e_id3 : m_out_edges[e2.get_source()]) { ++m_stats.m_implied_literal_cost; - edge_id e_id3 = *it3; edge const& e3 = m_edges[e_id3]; if (e3.is_enabled() || e3.get_target() != dst) { continue; @@ -1720,21 +1771,15 @@ public: } } } - it = m_out_edges[dst].begin(); - end = m_out_edges[dst].end(); - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_out_edges[dst]) { edge const& e2 = m_edges[e_id]; if (!e2.is_enabled() || e2.get_target() == src) { continue; } w2 = e2.get_weight() + w; - it3 = m_in_edges[e2.get_target()].begin(); - end3 = m_in_edges[e2.get_target()].end(); - for (; it3 != end3; ++it3) { + for (edge_id e_id3 : m_in_edges[e2.get_target()]) { ++m_stats.m_implied_literal_cost; - edge_id e_id3 = *it3; edge const& e3 = m_edges[e_id3]; if (e3.is_enabled() || e3.get_source() != src) { continue; @@ -1783,11 +1828,7 @@ public: m_mark[v] = DL_PROCESSED; TRACE("diff_logic", tout << v << "\n";); - typename edge_id_vector::iterator it = m_out_edges[v].begin(); - typename edge_id_vector::iterator end = m_out_edges[v].end(); - - for (; it != end; ++it) { - edge_id e_id = *it; + for (edge_id e_id : m_out_edges[v]) { edge const& e = m_edges[e_id]; if (!e.is_enabled() || e.get_timestamp() > timestamp) { continue; diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 63979e657..a40efe228 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4474,6 +4474,7 @@ namespace smt { fi->set_else(bodyr); m_model->register_decl(f, fi); } + TRACE("model", tout << *m_model << "\n";); } }; diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 731034921..5f916899b 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -33,6 +33,7 @@ Revision History: #include "smt/theory_dl.h" #include "smt/theory_seq_empty.h" #include "smt/theory_seq.h" +#include "smt/theory_special_relations.h" #include "smt/theory_pb.h" #include "smt/theory_fpa.h" #include "smt/theory_str.h" @@ -935,6 +936,10 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_jobscheduler, m_manager)); } + void setup::setup_special_relations() { + m_context.register_plugin(alloc(smt::theory_special_relations, m_manager)); + } + void setup::setup_unknown() { static_features st(m_manager); ptr_vector fmls; @@ -950,6 +955,7 @@ namespace smt { setup_seq_str(st); setup_card(); setup_fpa(); + if (st.m_has_sr) setup_special_relations(); } void setup::setup_unknown(static_features & st) { @@ -966,6 +972,7 @@ namespace smt { setup_card(); setup_fpa(); setup_recfuns(); + if (st.m_has_sr) setup_special_relations(); return; } diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h index 01a143301..53186f91c 100644 --- a/src/smt/smt_setup.h +++ b/src/smt/smt_setup.h @@ -82,6 +82,7 @@ namespace smt { void setup_QF_S(); void setup_LRA(); void setup_CSP(); + void setup_special_relations(); void setup_AUFLIA(bool simple_array = true); void setup_AUFLIA(static_features const & st); void setup_AUFLIRA(bool simple_array = true); diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp index af2d56cf1..cc7ec0e36 100644 --- a/src/smt/theory_recfun.cpp +++ b/src/smt/theory_recfun.cpp @@ -460,7 +460,7 @@ namespace smt { } void theory_recfun::display(std::ostream & out) const { - out << "recfun{}"; + out << "recfun{}\n"; } void theory_recfun::collect_statistics(::statistics & st) const { diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp new file mode 100644 index 000000000..e8c276206 --- /dev/null +++ b/src/smt/theory_special_relations.cpp @@ -0,0 +1,907 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + theory_special_relations.cpp + +Abstract: + + Special Relations theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-9-16 + Ashutosh Gupta 2016 + +Notes: + +--*/ + +#include + +#include "smt/smt_context.h" +#include "smt/theory_arith.h" +#include "smt/theory_special_relations.h" +#include "smt/smt_solver.h" +#include "solver/solver.h" +#include "ast/reg_decl_plugins.h" +#include "ast/datatype_decl_plugin.h" +#include "ast/recfun_decl_plugin.h" +#include "ast/ast_pp.h" +#include "ast/rewriter/recfun_replace.h" + + +namespace smt { + + void theory_special_relations::relation::push() { + m_scopes.push_back(scope()); + scope& s = m_scopes.back(); + s.m_asserted_atoms_lim = m_asserted_atoms.size(); + s.m_asserted_qhead_old = m_asserted_qhead; + m_graph.push(); + m_ufctx.get_trail_stack().push_scope(); + } + + void theory_special_relations::relation::pop(unsigned num_scopes) { + unsigned new_lvl = m_scopes.size() - num_scopes; + scope& s = m_scopes[new_lvl]; + m_asserted_atoms.shrink(s.m_asserted_atoms_lim); + m_asserted_qhead = s.m_asserted_qhead_old; + m_scopes.shrink(new_lvl); + m_graph.pop(num_scopes); + m_ufctx.get_trail_stack().pop_scope(num_scopes); + } + + void theory_special_relations::relation::ensure_var(theory_var v) { + while ((unsigned)v > m_uf.mk_var()); + if ((unsigned)v >= m_graph.get_num_nodes()) { + m_graph.init_var(v); + } + } + + bool theory_special_relations::relation::new_eq_eh(literal l, theory_var v1, theory_var v2) { + ensure_var(v1); + ensure_var(v2); + literal_vector ls; + ls.push_back(l); + return m_graph.add_non_strict_edge(v1, v2, ls) && m_graph.add_non_strict_edge(v2, v1, ls); + } + + std::ostream& theory_special_relations::relation::display(theory_special_relations const& th, std::ostream& out) const { + out << mk_pp(m_decl, th.get_manager()); + for (unsigned i = 0; i < m_decl->get_num_parameters(); ++i) { + th.get_manager().display(out << " ", m_decl->get_parameter(i)); + } + out << ":\n"; + m_graph.display(out); + out << "explanation: " << m_explanation << "\n"; + m_uf.display(out); + for (atom* ap : m_asserted_atoms) { + th.display_atom(out, *ap); + } + return out; + } + + theory_special_relations::theory_special_relations(ast_manager& m): + theory(m.mk_family_id("special_relations")), + m_util(m) { + } + + theory_special_relations::~theory_special_relations() { + reset_eh(); + } + + theory * theory_special_relations::mk_fresh(context * new_ctx) { + return alloc(theory_special_relations, new_ctx->get_manager()); + } + + bool theory_special_relations::internalize_atom(app * atm, bool gate_ctx) { + SASSERT(m_util.is_special_relation(atm)); + relation* r = 0; + if (!m_relations.find(atm->get_decl(), r)) { + r = alloc(relation, m_util.get_property(atm), atm->get_decl()); + m_relations.insert(atm->get_decl(), r); + for (unsigned i = 0; i < m_atoms_lim.size(); ++i) r->push(); + } + context& ctx = get_context(); + expr* arg0 = atm->get_arg(0); + expr* arg1 = atm->get_arg(1); + theory_var v0 = mk_var(arg0); + theory_var v1 = mk_var(arg1); + bool_var v = ctx.mk_bool_var(atm); + ctx.set_var_theory(v, get_id()); + atom* a = alloc(atom, v, *r, v0, v1); + m_atoms.push_back(a); + TRACE("special_relations", tout << mk_pp(atm, get_manager()) << " : bv" << v << " v" << a->v1() << " v" << a->v2() << ' ' << gate_ctx << "\n";); + m_bool_var2atom.insert(v, a); + return true; + } + + theory_var theory_special_relations::mk_var(expr* e) { + context& ctx = get_context(); + if (!ctx.e_internalized(e)) { + ctx.internalize(e, false); + } + enode * n = ctx.get_enode(e); + theory_var v = n->get_th_var(get_id()); + if (null_theory_var == v) { + v = theory::mk_var(n); + ctx.attach_th_var(n, this, v); + } + return v; + } + + void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) { + context& ctx = get_context(); + app* t1 = get_enode(v1)->get_owner(); + app* t2 = get_enode(v2)->get_owner(); + literal eq = mk_eq(t1, t2, false); + for (auto const& kv : m_relations) { + relation& r = *kv.m_value; + if (!r.new_eq_eh(eq, v1, v2)) { + set_neg_cycle_conflict(r); + break; + } + } + } + + final_check_status theory_special_relations::final_check_eh() { + TRACE("special_relations", tout << "\n";); + for (auto const& kv : m_relations) { + lbool r = final_check(*kv.m_value); + switch (r) { + case l_undef: + return FC_GIVEUP; + case l_false: + return FC_CONTINUE; + default: + break; + } + } + bool new_equality = false; + for (auto const& kv : m_relations) { + if (extract_equalities(*kv.m_value)) { + new_equality = true; + } + } + if (new_equality) { + return FC_CONTINUE; + } + else { + return FC_DONE; + } + } + + lbool theory_special_relations::final_check_lo(relation& r) { + // all constraints are saturated by propagation. + return l_true; + } + + enode* theory_special_relations::ensure_enode(expr* e) { + context& ctx = get_context(); + if (!ctx.e_internalized(e)) { + ctx.internalize(e, false); + } + enode* n = ctx.get_enode(e); + ctx.mark_as_relevant(n); + return n; + } + + literal theory_special_relations::mk_literal(expr* _e) { + expr_ref e(_e, get_manager()); + ensure_enode(e); + return get_context().get_literal(e); + } + + theory_var theory_special_relations::mk_var(enode* n) { + if (is_attached_to_var(n)) { + return n->get_th_var(get_id()); + } + else { + theory_var v = theory::mk_var(n); + get_context().attach_th_var(n, this, v); + get_context().mark_as_relevant(n); + return v; + } + } + + lbool theory_special_relations::final_check_plo(relation& r) { + // + // ensure that !Rxy -> Ryx between connected components + // (where Rzx & Rzy or Rxz & Ryz for some z) + // + lbool res = l_true; + for (unsigned i = 0; res == l_true && i < r.m_asserted_atoms.size(); ++i) { + atom& a = *r.m_asserted_atoms[i]; + if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { + res = enable(a); + } + } + return res; + } + + lbool theory_special_relations::final_check_to(relation& r) { + uint_set visited, target; + for (atom* ap : r.m_asserted_atoms) { + atom& a = *ap; + if (a.phase() || r.m_uf.find(a.v1()) != r.m_uf.find(a.v2())) { + continue; + } + target.reset(); + theory_var w; + // v2 !<= v1 is asserted + target.insert(a.v2()); + if (r.m_graph.reachable(a.v1(), target, visited, w)) { + // we already have v1 <= v2 + continue; + } + // the nodes visited from v1 become target for v2 + if (r.m_graph.reachable(a.v2(), visited, target, w)) { + // we have the following: + // v1 <= w + // v2 <= w + // v1 !<= v2 + // + // enforce the assertion + // + // v1 <= w & v2 <= w & v1 !<= v2 -> v2 <= v1 + // + unsigned timestamp = r.m_graph.get_timestamp(); + r.m_explanation.reset(); + r.m_graph.find_shortest_reachable_path(a.v1(), w, timestamp, r); + r.m_graph.find_shortest_reachable_path(a.v2(), w, timestamp, r); + r.m_explanation.push_back(a.explanation()); + literal_vector const& lits = r.m_explanation; + if (!r.m_graph.add_non_strict_edge(a.v2(), a.v1(), lits)) { + set_neg_cycle_conflict(r); + return l_false; + } + } + } + return l_true; + } + + lbool theory_special_relations::enable(atom& a) { + if (!a.enable()) { + relation& r = a.get_relation(); + set_neg_cycle_conflict(r); + return l_false; + } + else { + return l_true; + } + } + + void theory_special_relations::set_neg_cycle_conflict(relation& r) { + r.m_explanation.reset(); + r.m_graph.traverse_neg_cycle2(false, r); + set_conflict(r); + } + + void theory_special_relations::set_conflict(relation& r) { + literal_vector const& lits = r.m_explanation; + context & ctx = get_context(); + vector params; + ctx.set_conflict( + ctx.mk_justification( + ext_theory_conflict_justification( + get_id(), ctx.get_region(), + lits.size(), lits.c_ptr(), 0, 0, params.size(), params.c_ptr()))); + } + + lbool theory_special_relations::final_check(relation& r) { + lbool res = propagate(r); + if (res != l_true) return res; + switch (r.m_property) { + case sr_lo: + res = final_check_lo(r); + break; + case sr_po: + res = final_check_po(r); + break; + case sr_plo: + res = final_check_plo(r); + break; + case sr_to: + res = final_check_to(r); + break; + default: + UNREACHABLE(); + res = l_undef; + } + TRACE("special_relations", r.display(*this, tout);); + return res; + } + + bool theory_special_relations::extract_equalities(relation& r) { + bool new_eq = false; + int_vector scc_id; + u_map roots; + context& ctx = get_context(); + r.m_graph.compute_zero_edge_scc(scc_id); + for (unsigned i = 0, j = 0; !ctx.inconsistent() && i < scc_id.size(); ++i) { + if (scc_id[i] == -1) { + continue; + } + enode* n = get_enode(i); + if (roots.find(scc_id[i], j)) { + enode* m = get_enode(j); + if (n->get_root() != m->get_root()) { + new_eq = true; + unsigned timestamp = r.m_graph.get_timestamp(); + r.m_explanation.reset(); + r.m_graph.find_shortest_zero_edge_path(i, j, timestamp, r); + r.m_graph.find_shortest_zero_edge_path(j, i, timestamp, r); + eq_justification js(ctx.mk_justification(theory_axiom_justification(get_id(), ctx.get_region(), r.m_explanation.size(), r.m_explanation.c_ptr()))); + ctx.assign_eq(n, m, js); + } + } + else { + roots.insert(scc_id[i], i); + } + } + return new_eq; + } + + /* + \brief Propagation for piecewise linear orders + */ + lbool theory_special_relations::propagate_plo(atom& a) { + lbool res = l_true; + relation& r = a.get_relation(); + if (a.phase()) { + r.m_uf.merge(a.v1(), a.v2()); + res = enable(a); + } + else if (r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { + res = enable(a); + } + return res; + } + + lbool theory_special_relations::propagate_po(atom& a) { + lbool res = l_true; + relation& r = a.get_relation(); + if (a.phase()) { + r.m_uf.merge(a.v1(), a.v2()); + res = enable(a); + } + return res; + } + + lbool theory_special_relations::final_check_po(relation& r) { + for (atom* ap : r.m_asserted_atoms) { + atom& a = *ap; + if (!a.phase() && r.m_uf.find(a.v1()) == r.m_uf.find(a.v2())) { + // v1 !-> v2 + // find v1 -> v3 -> v4 -> v2 path + r.m_explanation.reset(); + unsigned timestamp = r.m_graph.get_timestamp(); + bool found_path = r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r); + if (found_path) { + r.m_explanation.push_back(a.explanation()); + set_conflict(r); + return l_false; + } + } + } + return l_true; + } + + lbool theory_special_relations::propagate(relation& r) { + lbool res = l_true; + while (res == l_true && r.m_asserted_qhead < r.m_asserted_atoms.size()) { + atom& a = *r.m_asserted_atoms[r.m_asserted_qhead]; + switch (r.m_property) { + case sr_lo: + res = enable(a); + break; + case sr_plo: + res = propagate_plo(a); + break; + case sr_po: + res = propagate_po(a); + break; + default: + if (a.phase()) { + res = enable(a); + } + break; + } + ++r.m_asserted_qhead; + } + return res; + } + + void theory_special_relations::reset_eh() { + for (auto const& kv : m_relations) { + dealloc(kv.m_value); + } + m_relations.reset(); + del_atoms(0); + } + + void theory_special_relations::assign_eh(bool_var v, bool is_true) { + TRACE("special_relations", tout << "assign bv" << v << " " << (is_true?" <- true":" <- false") << "\n";); + atom* a = m_bool_var2atom[v]; + a->set_phase(is_true); + a->get_relation().m_asserted_atoms.push_back(a); + } + + void theory_special_relations::push_scope_eh() { + for (auto const& kv : m_relations) { + kv.m_value->push(); + } + m_atoms_lim.push_back(m_atoms.size()); + } + + void theory_special_relations::pop_scope_eh(unsigned num_scopes) { + for (auto const& kv : m_relations) { + kv.m_value->pop(num_scopes); + } + unsigned new_lvl = m_atoms_lim.size() - num_scopes; + del_atoms(m_atoms_lim[new_lvl]); + m_atoms_lim.shrink(new_lvl); + } + + void theory_special_relations::del_atoms(unsigned old_size) { + atoms::iterator begin = m_atoms.begin() + old_size; + atoms::iterator it = m_atoms.end(); + while (it != begin) { + --it; + atom* a = *it; + m_bool_var2atom.erase(a->var()); + dealloc(a); + } + m_atoms.shrink(old_size); + } + + + void theory_special_relations::collect_statistics(::statistics & st) const { + for (auto const& kv : m_relations) { + kv.m_value->m_graph.collect_statistics(st); + } + } + + model_value_proc * theory_special_relations::mk_value(enode * n, model_generator & mg) { + UNREACHABLE(); + return nullptr; + } + + void theory_special_relations::ensure_strict(graph& g) { + unsigned sz = g.get_num_edges(); + for (unsigned i = 0; i < sz; ++i) { + if (!g.is_enabled(i)) continue; + if (g.get_weight(i) != s_integer(0)) continue; + dl_var src = g.get_source(i); + dl_var dst = g.get_target(i); + if (get_enode(src)->get_root() == get_enode(dst)->get_root()) continue; + VERIFY(g.add_strict_edge(src, dst, literal_vector())); + } + TRACE("special_relations", g.display(tout);); + } + + void theory_special_relations::ensure_tree(graph& g) { + unsigned sz = g.get_num_nodes(); + for (unsigned i = 0; i < sz; ++i) { + int_vector const& edges = g.get_in_edges(i); + for (unsigned j = 0; j < edges.size(); ++j) { + edge_id e1 = edges[j]; + if (g.is_enabled(e1)) { + SASSERT (i == g.get_target(e1)); + dl_var src1 = g.get_source(e1); + for (unsigned k = j + 1; k < edges.size(); ++k) { + edge_id e2 = edges[k]; + if (g.is_enabled(e2)) { + dl_var src2 = g.get_source(e2); + if (get_enode(src1)->get_root() != get_enode(src2)->get_root() && + disconnected(g, src1, src2)) { + VERIFY(g.add_strict_edge(src1, src2, literal_vector())); + } + } + } + } + } + } + TRACE("special_relations", g.display(tout);); + } + + bool theory_special_relations::disconnected(graph const& g, dl_var u, dl_var v) const { + s_integer val_u = g.get_assignment(u); + s_integer val_v = g.get_assignment(v); + if (val_u == val_v) return u != v; + if (val_u < val_v) { + std::swap(u, v); + std::swap(val_u, val_v); + } + SASSERT(val_u > val_v); + svector todo; + todo.push_back(u); + while (!todo.empty()) { + u = todo.back(); + todo.pop_back(); + if (u == v) { + return false; + } + SASSERT(g.get_assignment(u) <= val_u); + if (g.get_assignment(u) <= val_v) { + continue; + } + for (edge_id e : g.get_out_edges(u)) { + if (is_strict_neighbour_edge(g, e)) { + todo.push_back(g.get_target(e)); + } + } + } + return true; + } + + expr_ref theory_special_relations::mk_inj(relation& r, model_generator& mg) { + ast_manager& m = get_manager(); + r.push(); + ensure_strict(r.m_graph); + func_decl_ref fn(m); + expr_ref result(m); + arith_util arith(m); + sort* const* ty = r.decl()->get_domain(); + fn = m.mk_fresh_func_decl("inj", 1, ty, arith.mk_int()); + unsigned sz = r.m_graph.get_num_nodes(); + func_interp* fi = alloc(func_interp, m, 1); + for (unsigned i = 0; i < sz; ++i) { + s_integer val = r.m_graph.get_assignment(i); + expr* arg = get_enode(i)->get_owner(); + fi->insert_new_entry(&arg, arith.mk_numeral(val.to_rational(), true)); + } + TRACE("special_relations", r.m_graph.display(tout);); + r.pop(1); + fi->set_else(arith.mk_numeral(rational(0), true)); + mg.get_model().register_decl(fn, fi); + result = arith.mk_le(m.mk_app(fn,m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty))); + return result; + } + + expr_ref theory_special_relations::mk_class(relation& r, model_generator& mg) { + ast_manager& m = get_manager(); + expr_ref result(m); + func_decl_ref fn(m); + arith_util arith(m); + func_interp* fi = alloc(func_interp, m, 1); + sort* const* ty = r.decl()->get_domain(); + fn = m.mk_fresh_func_decl("class", 1, ty, arith.mk_int()); + unsigned sz = r.m_graph.get_num_nodes(); + for (unsigned i = 0; i < sz; ++i) { + unsigned val = r.m_uf.find(i); + expr* arg = get_enode(i)->get_owner(); + fi->insert_new_entry(&arg, arith.mk_numeral(rational(val), true)); + } + fi->set_else(arith.mk_numeral(rational(0), true)); + mg.get_model().register_decl(fn, fi); + result = m.mk_eq(m.mk_app(fn, m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty))); + return result; + } + + expr_ref theory_special_relations::mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi) { + graph const& g = r.m_graph; + ast_manager& m = get_manager(); + expr_ref result(m); + func_decl_ref lofn(m), hifn(m); + arith_util arith(m); + func_interp* lofi = alloc(func_interp, m, 1); + func_interp* hifi = alloc(func_interp, m, 1); + sort* const* ty = r.decl()->get_domain(); + lofn = m.mk_fresh_func_decl("lo", 1, ty, arith.mk_int()); + hifn = m.mk_fresh_func_decl("hi", 1, ty, arith.mk_int()); + unsigned sz = g.get_num_nodes(); + for (unsigned i = 0; i < sz; ++i) { + expr* arg = get_enode(i)->get_owner(); + lofi->insert_new_entry(&arg, arith.mk_numeral(rational(lo[i]), true)); + hifi->insert_new_entry(&arg, arith.mk_numeral(rational(hi[i]), true)); + } + lofi->set_else(arith.mk_numeral(rational(0), true)); + hifi->set_else(arith.mk_numeral(rational(0), true)); + mg.get_model().register_decl(lofn, lofi); + mg.get_model().register_decl(hifn, hifi); + result = m.mk_and(arith.mk_le(m.mk_app(lofn, m.mk_var(0, *ty)), m.mk_app(lofn, m.mk_var(1, *ty))), + arith.mk_le(m.mk_app(hifn, m.mk_var(1, *ty)), m.mk_app(hifn, m.mk_var(0, *ty)))); + return result; + } + + void theory_special_relations::init_model_lo(relation& r, model_generator& m) { + expr_ref inj = mk_inj(r, m); + func_interp* fi = alloc(func_interp, get_manager(), 2); + fi->set_else(inj); + m.get_model().register_decl(r.decl(), fi); + } + + void theory_special_relations::init_model_plo(relation& r, model_generator& mg) { + expr_ref inj = mk_inj(r, mg); + expr_ref cls = mk_class(r, mg); + func_interp* fi = alloc(func_interp, get_manager(), 2); + fi->set_else(get_manager().mk_and(inj, cls)); + mg.get_model().register_decl(r.decl(), fi); + } + + /** + \brief model for a partial order, + is a recursive function that evaluates membership in partial order over + a fixed set of edges. It runs in O(e*n^2) where n is the number of vertices and e + number of edges. + + connected1(x, y, v, w, S) = + if x = v then + if y = w then (S, true) else + if w in S then (S, false) else + connected2(w, y, S u { w }, edges) + else (S, false) + + connected2(x, y, S, []) = (S, false) + connected2(x, y, S, (u,w)::edges) = + let (S, c) = connected1(x, y, u, w, S) + if c then (S, true) else connected2(x, y, S, edges) + + */ + + + void theory_special_relations::init_model_po(relation& r, model_generator& mg) { + ast_manager& m = get_manager(); + sort* s = r.m_decl->get_domain(0); + context& ctx = get_context(); + datatype_util dt(m); + recfun::util rf(m); + recfun::decl::plugin& p = rf.get_plugin(); + func_decl_ref nil(m), is_nil(m), cons(m), is_cons(m), hd(m), tl(m); + sort_ref listS(dt.mk_list_datatype(s, symbol("List"), cons, is_cons, hd, tl, nil, is_nil), m); + func_decl_ref fst(m), snd(m), pair(m); + sort_ref tup(dt.mk_pair_datatype(listS, m.mk_bool_sort(), fst, snd, pair), m); + sort* dom1[5] = { s, s, listS, s, s }; + recfun::promise_def c1 = p.ensure_def(symbol("connected1"), 5, dom1, tup); + sort* dom2[3] = { s, s, listS }; + recfun::promise_def c2 = p.ensure_def(symbol("connected2"), 3, dom2, tup); + sort* dom3[2] = { s, listS }; + recfun::promise_def mem = p.ensure_def(symbol("member"), 2, dom3, m.mk_bool_sort()); + var_ref xV(m.mk_var(1, s), m); + var_ref SV(m.mk_var(0, listS), m); + var_ref yV(m), vV(m), wV(m); + + expr* x = xV, *S = SV; + expr* T = m.mk_true(); + expr* F = m.mk_false(); + func_decl* memf = mem.get_def()->get_decl(); + func_decl* conn1 = c1.get_def()->get_decl(); + func_decl* conn2 = c2.get_def()->get_decl(); + expr_ref mem_body(m); + mem_body = m.mk_ite(m.mk_app(is_nil, S), + F, + m.mk_ite(m.mk_eq(m.mk_app(hd, S), x), + T, + m.mk_app(memf, x, m.mk_app(tl, S)))); + recfun_replace rep(m); + var* vars[2] = { xV, SV }; + p.set_definition(rep, mem, 2, vars, mem_body); + + xV = m.mk_var(4, s); + yV = m.mk_var(3, s); + SV = m.mk_var(2, listS); + vV = m.mk_var(1, s); + wV = m.mk_var(0, s); + expr* y = yV, *v = vV, *w = wV; + x = xV, S = SV; + + expr_ref ST(m.mk_app(pair, S, T), m); + expr_ref SF(m.mk_app(pair, S, F), m); + + expr_ref connected_body(m); + connected_body = + m.mk_ite(m.mk_not(m.mk_eq(x, v)), + SF, + m.mk_ite(m.mk_eq(y, w), + ST, + m.mk_ite(m.mk_app(memf, w, S), + SF, + m.mk_app(conn2, w, y, m.mk_app(cons, w, S))))); + var* vars2[5] = { xV, yV, SV, vV, wV }; + p.set_definition(rep, c1, 5, vars2, connected_body); + + xV = m.mk_var(2, s); + yV = m.mk_var(1, s); + SV = m.mk_var(0, listS); + x = xV, y = yV, S = SV; + ST = m.mk_app(pair, S, T); + SF = m.mk_app(pair, S, F); + expr_ref connected_rec_body(m); + connected_rec_body = SF; + + for (atom* ap : r.m_asserted_atoms) { + atom& a = *ap; + if (!a.phase()) continue; + SASSERT(ctx.get_assignment(a.var()) == l_true); + expr* n1 = get_enode(a.v1())->get_root()->get_owner(); + expr* n2 = get_enode(a.v2())->get_root()->get_owner(); + expr* Sr = connected_rec_body; + expr* args[5] = { x, y, m.mk_app(fst, Sr), n1, n2}; + expr* Sc = m.mk_app(conn1, 5, args); + connected_rec_body = m.mk_ite(m.mk_app(snd, Sr), ST, Sc); + } + var* vars3[3] = { xV, yV, SV }; + p.set_definition(rep, c2, 3, vars3, connected_rec_body); + + // r.m_decl(x,y) -> snd(connected2(x,y,nil)) + xV = m.mk_var(0, s); + yV = m.mk_var(1, s); + x = xV, y = yV; + + func_interp* fi = alloc(func_interp, m, 2); + fi->set_else(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_app(cons, x, m.mk_const(nil))))); + mg.get_model().register_decl(r.decl(), fi); + + } + + /** + \brief map each node to an interval of numbers, such that + the children are proper sub-intervals. + Then the <= relation becomes interval containment. + + 1. For each vertex, count the number of nodes below it in the transitive closure. + Store the result in num_children. + 2. Identify each root. + 3. Process children, assigning unique (and disjoint) intervals. + 4. Extract interpretation. + + + */ + + void theory_special_relations::init_model_to(relation& r, model_generator& mg) { + unsigned_vector num_children, lo, hi; + graph const& g = r.m_graph; + r.push(); + ensure_strict(r.m_graph); + ensure_tree(r.m_graph); + count_children(g, num_children); + assign_interval(g, num_children, lo, hi); + expr_ref iv = mk_interval(r, mg, lo, hi); + r.pop(1); + func_interp* fi = alloc(func_interp, get_manager(), 2); + fi->set_else(iv); + mg.get_model().register_decl(r.decl(), fi); + } + + bool theory_special_relations::is_neighbour_edge(graph const& g, edge_id edge) const { + CTRACE("special_relations_verbose", g.is_enabled(edge), + tout << edge << ": " << g.get_source(edge) << " " << g.get_target(edge) << " "; + tout << (g.get_assignment(g.get_target(edge)) - g.get_assignment(g.get_source(edge))) << "\n";); + + return + g.is_enabled(edge) && + g.get_assignment(g.get_source(edge)) + s_integer(1) == g.get_assignment(g.get_target(edge)); + } + + bool theory_special_relations::is_strict_neighbour_edge(graph const& g, edge_id e) const { + return is_neighbour_edge(g, e) && g.get_weight(e) != s_integer(0); + } + + void theory_special_relations::count_children(graph const& g, unsigned_vector& num_children) { + unsigned sz = g.get_num_nodes(); + svector nodes; + num_children.resize(sz, 0); + svector processed(sz, false); + for (unsigned i = 0; i < sz; ++i) nodes.push_back(i); + while (!nodes.empty()) { + dl_var v = nodes.back(); + if (processed[v]) { + nodes.pop_back(); + continue; + } + unsigned nc = 1; + bool all_p = true; + for (edge_id e : g.get_out_edges(v)) { + if (is_strict_neighbour_edge(g, e)) { + dl_var dst = g.get_target(e); + TRACE("special_relations", tout << v << " -> " << dst << "\n";); + if (!processed[dst]) { + all_p = false; + nodes.push_back(dst); + } + nc += num_children[dst]; + } + } + if (all_p) { + nodes.pop_back(); + num_children[v] = nc; + processed[v] = true; + } + } + TRACE("special_relations", + for (unsigned i = 0; i < sz; ++i) { + tout << i << ": " << num_children[i] << "\n"; + }); + } + + void theory_special_relations::assign_interval(graph const& g, unsigned_vector const& num_children, unsigned_vector& lo, unsigned_vector& hi) { + svector nodes; + unsigned sz = g.get_num_nodes(); + lo.resize(sz, 0); + hi.resize(sz, 0); + unsigned offset = 0; + for (unsigned i = 0; i < sz; ++i) { + bool is_root = true; + int_vector const& edges = g.get_in_edges(i); + for (edge_id e_id : edges) { + is_root &= !g.is_enabled(e_id); + } + if (is_root) { + lo[i] = offset; + hi[i] = offset + num_children[i] - 1; + offset = hi[i] + 1; + nodes.push_back(i); + } + } + while (!nodes.empty()) { + dl_var v = nodes.back(); + int_vector const& edges = g.get_out_edges(v); + unsigned l = lo[v]; + unsigned h = hi[v]; + (void)h; + nodes.pop_back(); + for (unsigned i = 0; i < edges.size(); ++i) { + SASSERT(l <= h); + if (is_strict_neighbour_edge(g, edges[i])) { + dl_var dst = g.get_target(edges[i]); + lo[dst] = l; + hi[dst] = l + num_children[dst] - 1; + l = hi[dst] + 1; + nodes.push_back(dst); + } + } + SASSERT(l == h); + } + } + + void theory_special_relations::init_model(model_generator & m) { + for (auto const& kv : m_relations) { + switch (kv.m_value->m_property) { + case sr_lo: + init_model_lo(*kv.m_value, m); + break; + case sr_plo: + init_model_plo(*kv.m_value, m); + break; + case sr_to: + init_model_to(*kv.m_value, m); + break; + case sr_po: + init_model_po(*kv.m_value, m); + break; + default: + // other 28 combinations of 0x1F + NOT_IMPLEMENTED_YET(); + } + } + } + + void theory_special_relations::display(std::ostream & out) const { + if (m_relations.empty()) return; + out << "Theory Special Relations\n"; + display_var2enode(out); + for (auto const& kv : m_relations) { + kv.m_value->display(*this, out); + } + } + + void theory_special_relations::collect_asserted_po_atoms(vector>& atoms) const { + for (auto const& kv : m_relations) { + relation& r = *kv.m_value; + if (r.m_property != sr_po) continue; + for (atom* ap : r.m_asserted_atoms) { + atoms.push_back(std::make_pair(ap->var(), ap->phase())); + } + } + } + + void theory_special_relations::display_atom(std::ostream & out, atom& a) const { + context& ctx = get_context(); + expr* e = ctx.bool_var2expr(a.var()); + out << (a.phase() ? "" : "(not ") << mk_pp(e, get_manager()) << (a.phase() ? "" : ")") << "\n"; + } + +} diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h new file mode 100644 index 000000000..81a968e54 --- /dev/null +++ b/src/smt/theory_special_relations.h @@ -0,0 +1,199 @@ +/*++ +Copyright (c) 2015 Microsoft Corporation + +Module Name: + + theory_special_relations.h + +Abstract: + + Special Relations theory plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2015-9-16 + +Notes: + +--*/ + +#ifndef THEORY_SPECIAL_RELATIONS_H_ +#define THEORY_SPECIAL_RELATIONS_H_ + +#include "ast/special_relations_decl_plugin.h" +#include "smt/smt_theory.h" +#include "smt/theory_diff_logic.h" +#include "util/union_find.h" +#include "util/rational.h" + +namespace smt { + class theory_special_relations : public theory { + + + struct relation; + + class atom { + bool_var m_bvar; + relation& m_relation; + bool m_phase; + theory_var m_v1; + theory_var m_v2; + edge_id m_pos; + edge_id m_neg; + public: + atom(bool_var b, relation& r, theory_var v1, theory_var v2): + m_bvar(b), + m_relation(r), + m_phase(true), + m_v1(v1), + m_v2(v2) + { + r.ensure_var(v1); + r.ensure_var(v2); + literal_vector ls; + ls.push_back(literal(b, false)); + m_pos = r.m_graph.add_edge(v1, v2, s_integer(0), ls); // v1 <= v2 + ls[0] = literal(b, true); + m_neg = r.m_graph.add_edge(v2, v1, s_integer(-1), ls); // v2 + 1 <= v1 + } + bool_var var() const { return m_bvar;} + relation& get_relation() const { return m_relation; } + bool phase() const { return m_phase; } + void set_phase(bool b) { m_phase = b; } + theory_var v1() const { return m_v1; } + theory_var v2() const { return m_v2; } + literal explanation() const { return literal(m_bvar, !m_phase); } + bool enable() { + edge_id edge = m_phase?m_pos:m_neg; + return m_relation.m_graph.enable_edge(edge); + } + }; + typedef ptr_vector atoms; + + struct scope { + unsigned m_asserted_atoms_lim; + unsigned m_asserted_qhead_old; + }; + + struct int_ext : public sidl_ext { + typedef literal_vector explanation; + }; + struct graph : public dl_graph { + bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) { + // v1 + 1 <= v2 + return enable_edge(add_edge(v1, v2, s_integer(-1), j)); + } + bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) { + // v1 <= v2 + return enable_edge(add_edge(v1, v2, s_integer(0), j)); + } + }; + + typedef union_find union_find_t; + + struct relation { + sr_property m_property; + func_decl* m_decl; + atoms m_asserted_atoms; // set of asserted atoms + unsigned m_asserted_qhead; + svector m_scopes; + graph m_graph; + union_find_default_ctx m_ufctx; + union_find_t m_uf; + literal_vector m_explanation; + + relation(sr_property p, func_decl* d): m_property(p), m_decl(d), m_asserted_qhead(0), m_uf(m_ufctx) {} + + func_decl* decl() { return m_decl; } + void push(); + void pop(unsigned num_scopes); + void ensure_var(theory_var v); + bool new_eq_eh(literal l, theory_var v1, theory_var v2); + void operator()(literal_vector const & ex) { + m_explanation.append(ex); + } + void new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {} + + bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j); + bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j); + + std::ostream& display(theory_special_relations const& sr, std::ostream& out) const; + }; + + + + + typedef u_map bool_var2atom; + + special_relations_util m_util; + atoms m_atoms; + unsigned_vector m_atoms_lim; + obj_map m_relations; + bool_var2atom m_bool_var2atom; + + + void del_atoms(unsigned old_size); + lbool final_check(relation& r); + lbool final_check_po(relation& r); + lbool final_check_lo(relation& r); + lbool final_check_plo(relation& r); + lbool final_check_to(relation& r); + lbool propagate(relation& r); + lbool enable(atom& a); + bool extract_equalities(relation& r); + void set_neg_cycle_conflict(relation& r); + void set_conflict(relation& r); + lbool propagate_plo(atom& a); + lbool propagate_po(atom& a); + theory_var mk_var(expr* e); + void count_children(graph const& g, unsigned_vector& num_children); + void ensure_strict(graph& g); + void ensure_tree(graph& g); + void assign_interval(graph const& g, unsigned_vector const& num_children, unsigned_vector& lo, unsigned_vector& hi); + expr_ref mk_inj(relation& r, model_generator& m); + expr_ref mk_class(relation& r, model_generator& m); + expr_ref mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi); + void init_model_lo(relation& r, model_generator& m); + void init_model_to(relation& r, model_generator& m); + void init_model_po(relation& r, model_generator& m); + void init_model_plo(relation& r, model_generator& m); + bool is_neighbour_edge(graph const& g, edge_id id) const; + bool is_strict_neighbour_edge(graph const& g, edge_id id) const; + bool disconnected(graph const& g, dl_var u, dl_var v) const; + + literal mk_literal(expr* _e); + enode* ensure_enode(expr* e); + theory_var mk_var(enode* n); + + void collect_asserted_po_atoms(vector< std::pair >& atoms) const; + void display_atom(std::ostream & out, atom& a) const; + + public: + theory_special_relations(ast_manager& m); + ~theory_special_relations() override; + + theory * mk_fresh(context * new_ctx) override; + bool internalize_atom(app * atom, bool gate_ctx) override; + bool internalize_term(app * term) override { UNREACHABLE(); return false; } + void new_eq_eh(theory_var v1, theory_var v2) override; + void new_diseq_eh(theory_var v1, theory_var v2) override {} + bool use_diseqs() const override { return false; } + bool build_models() const override { return true; } + final_check_status final_check_eh() override; + void reset_eh() override; + void assign_eh(bool_var v, bool is_true) override; + void init_search_eh() override {} + void push_scope_eh() override; + void pop_scope_eh(unsigned num_scopes) override; + void restart_eh() override {} + void collect_statistics(::statistics & st) const override; + model_value_proc * mk_value(enode * n, model_generator & mg) override; + void init_model(model_generator & m) override; + bool can_propagate() override { return false; } + void propagate() override {} + void display(std::ostream & out) const override; + + }; +} + +#endif diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 44284b625..a247c7b20 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -19,6 +19,7 @@ z3_add_component(core_tactics reduce_invertible_tactic.cpp simplify_tactic.cpp solve_eqs_tactic.cpp + special_relations_tactic.cpp split_clause_tactic.cpp symmetry_reduce_tactic.cpp tseitin_cnf_tactic.cpp @@ -46,6 +47,7 @@ z3_add_component(core_tactics reduce_invertible_tactic.h simplify_tactic.h solve_eqs_tactic.h + special_relations_tactic.h split_clause_tactic.h symmetry_reduce_tactic.h tseitin_cnf_tactic.h diff --git a/src/tactic/core/special_relations_tactic.cpp b/src/tactic/core/special_relations_tactic.cpp new file mode 100644 index 000000000..75f8e270c --- /dev/null +++ b/src/tactic/core/special_relations_tactic.cpp @@ -0,0 +1,182 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + special_relations_tactic.cpp + +Abstract: + + Detect special relations in an axiomatization, + rewrite goal using special relations. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-28 + +Notes: + +--*/ +#include "tactic/core/special_relations_tactic.h" +#include "ast/rewriter/func_decl_replace.h" +#include "ast/ast_util.h" +#include "ast/ast_pp.h" + +void special_relations_tactic::collect_feature(goal const& g, unsigned idx, + obj_map& goal_features) { + expr* f = g.form(idx); + func_decl_ref p(m); + if (!is_quantifier(f)) return; + unsigned index = 0; + app_ref_vector patterns(m); + bool is_match = m_pm.match_quantifier_index(to_quantifier(f), patterns, index); + TRACE("special_relations", tout << "check " << is_match << " " << mk_pp(f, m) << "\n"; + if (is_match) tout << patterns << " " << index << "\n";); + if (is_match) { + p = to_app(patterns.get(0)->get_arg(0))->get_decl(); + insert(goal_features, p, idx, m_properties[index]); + } +} + +void special_relations_tactic::insert(obj_map& goal_features, func_decl* f, unsigned idx, sr_property p) { + sp_axioms ax; + goal_features.find(f, ax); + ax.m_goal_indices.push_back(idx); + ax.m_sp_features = (sr_property)(p | ax.m_sp_features); + goal_features.insert(f, ax); +} + + +void special_relations_tactic::initialize() { + if (!m_properties.empty()) return; + sort_ref A(m.mk_uninterpreted_sort(symbol("A")), m); + func_decl_ref R(m.mk_func_decl(symbol("?R"), A, A, m.mk_bool_sort()), m); + var_ref x(m.mk_var(0, A), m); + var_ref y(m.mk_var(1, A), m); + var_ref z(m.mk_var(2, A), m); + expr* _x = x, *_y = y, *_z = z; + + expr_ref Rxy(m.mk_app(R, _x, y), m); + expr_ref Ryz(m.mk_app(R, _y, z), m); + expr_ref Rxz(m.mk_app(R, _x, z), m); + expr_ref Rxx(m.mk_app(R, _x, x), m); + expr_ref Ryx(m.mk_app(R, _y, x), m); + expr_ref Rzy(m.mk_app(R, _z, y), m); + expr_ref Rzx(m.mk_app(R, _z, x), m); + expr_ref nRxy(m.mk_not(Rxy), m); + expr_ref nRyx(m.mk_not(Ryx), m); + expr_ref nRzx(m.mk_not(Rzx), m); + expr_ref nRxz(m.mk_not(Rxz), m); + + sort* As[3] = { A, A, A}; + symbol xyz[3] = { symbol("x"), symbol("y"), symbol("z") }; + expr_ref fml(m); + quantifier_ref q(m); + expr_ref pat(m.mk_pattern(to_app(Rxy)), m); + expr_ref pat0(m.mk_pattern(to_app(Rxx)), m); + expr* pats[1] = { pat }; + expr* pats0[1] = { pat0 }; + + fml = m.mk_or(m.mk_not(Rxy), m.mk_not(Ryz), Rxz); + q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_transitive); + fml = m.mk_or(not(Rxy & Ryz), Rxz); + q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_transitive); + + fml = Rxx; + q = m.mk_forall(1, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats0); + register_pattern(m_pm.initialize(q), sr_reflexive); + + fml = m.mk_or(nRxy, nRyx, m.mk_eq(x, y)); + q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_antisymmetric); + fml = m.mk_or(not(Rxy & Ryx), m.mk_eq(x, y)); + q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_antisymmetric); + + fml = m.mk_or(nRyx, nRzx, Ryz, Rzy); + q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_lefttree); + fml = m.mk_or(not (Ryx & Rzx), Ryz, Rzy); + q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_lefttree); + + fml = m.mk_or(nRxy, nRxz, Ryz, Rzy); + q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_righttree); + fml = m.mk_or(not(Rxy & Rxz), Ryz, Rzy); + q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_righttree); + + fml = m.mk_or(Rxy, Ryx); + q = m.mk_forall(2, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); + register_pattern(m_pm.initialize(q), sr_total); + + TRACE("special_relations", m_pm.display(tout);); +} + +void special_relations_tactic::register_pattern(unsigned index, sr_property p) { + SASSERT(index == m_properties.size()); + m_properties.push_back(p); +} + + + +void special_relations_tactic::operator()(goal_ref const & g, goal_ref_buffer & result) { + tactic_report report("special_relations", *g); + initialize(); + obj_map goal_features; + unsigned size = g->size(); + for (unsigned idx = 0; idx < size; idx++) { + collect_feature(*g, idx, goal_features); + } + special_relations_util u(m); + func_decl_replace replace(m); + unsigned_vector to_delete; + for(auto const& kv : goal_features) { + func_decl* sp = nullptr; + sr_property feature = kv.m_value.m_sp_features; + switch (feature) { + case sr_po: + replace.insert(kv.m_key, u.mk_po_decl(kv.m_key)); + to_delete.append(kv.m_value.m_goal_indices); + break; + case sr_to: + replace.insert(kv.m_key, u.mk_to_decl(kv.m_key)); + to_delete.append(kv.m_value.m_goal_indices); + break; + case sr_plo: + replace.insert(kv.m_key, u.mk_plo_decl(kv.m_key)); + to_delete.append(kv.m_value.m_goal_indices); + break; + case sr_lo: + replace.insert(kv.m_key, u.mk_lo_decl(kv.m_key)); + to_delete.append(kv.m_value.m_goal_indices); + break; + default: + TRACE("special_relations", tout << "unprocessed feature " << feature << "\n";); + break; + } + } + if (!replace.empty()) { + for (unsigned idx = 0; idx < size; idx++) { + if (to_delete.contains(idx)) { + g->update(idx, m.mk_true()); + } + else { + expr_ref new_f = replace(g->form(idx)); + g->update(idx, new_f); + } + } + g->elim_true(); + } + + g->inc_depth(); + result.push_back(g.get()); +} + +tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p) { + return alloc(special_relations_tactic, m, p); +} + diff --git a/src/tactic/core/special_relations_tactic.h b/src/tactic/core/special_relations_tactic.h new file mode 100644 index 000000000..c706c78e8 --- /dev/null +++ b/src/tactic/core/special_relations_tactic.h @@ -0,0 +1,72 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + special_relations_tactic.h + +Abstract: + + Detect special relations in an axiomatization, + rewrite goal using special relations. + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-28 + +Notes: + +--*/ +#ifndef SPECIAL_RELATIONS_TACTIC_H_ +#define SPECIAL_RELATIONS_TACTIC_H_ + +#include "tactic/tactic.h" +#include "tactic/tactical.h" +#include "ast/special_relations_decl_plugin.h" +#include "ast/pattern/expr_pattern_match.h" + +class special_relations_tactic : public tactic { + ast_manager& m; + params_ref m_params; + expr_pattern_match m_pm; + svector m_properties; + + struct sp_axioms { + unsigned_vector m_goal_indices; + sr_property m_sp_features; + sp_axioms():m_sp_features(sr_none) {} + }; + + void collect_feature(goal const& g, unsigned idx, obj_map& goal_features); + void insert(obj_map& goal_features, func_decl* f, unsigned idx, sr_property p); + + void initialize(); + void register_pattern(unsigned index, sr_property); + +public: + + special_relations_tactic(ast_manager & m, params_ref const & ref = params_ref()): + m(m), m_params(ref), m_pm(m) {} + + ~special_relations_tactic() override {} + + void updt_params(params_ref const & p) override { m_params = p; } + + void collect_param_descrs(param_descrs & r) override { } + + void operator()(goal_ref const & in, goal_ref_buffer & result) override; + + void cleanup() override {} + + tactic * translate(ast_manager & m) override { return alloc(special_relations_tactic, m, m_params); } + +}; + +tactic * mk_special_relations_tactic(ast_manager & m, params_ref const & p = params_ref()); + + +/* + ADD_TACTIC("special-relations", "detect and replace by special relations.", "mk_special_relations_tactic(m, p)") +*/ + +#endif