From 175008a6c6081107fa9309f3e34a008770ce24b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Mar 2019 16:59:13 -0700 Subject: [PATCH] adding po evaluator Signed-off-by: Nikolaj Bjorner --- src/api/api_datatype.cpp | 65 ++++-------- src/ast/datatype_decl_plugin.cpp | 79 +++++++++++++++ src/ast/datatype_decl_plugin.h | 6 ++ src/ast/special_relations_decl_plugin.h | 4 + src/model/model.cpp | 1 + src/model/model_core.cpp | 1 + src/smt/smt_context.cpp | 1 + src/smt/theory_special_relations.cpp | 128 +++++++++++++++++++++++- 8 files changed, 233 insertions(+), 52 deletions(-) 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/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/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index dbdd61805..e8260e154 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -26,6 +26,7 @@ Revision History: enum special_relations_op_kind { OP_SPECIAL_RELATION_LO, OP_SPECIAL_RELATION_PO, + OP_SPECIAL_RELATION_PO_AO, OP_SPECIAL_RELATION_PLO, OP_SPECIAL_RELATION_TO, LAST_SPECIAL_RELATIONS_OP @@ -34,6 +35,7 @@ enum special_relations_op_kind { class special_relations_decl_plugin : public decl_plugin { symbol m_lo; symbol m_po; + symbol m_po_ao; symbol m_plo; symbol m_to; public: @@ -78,11 +80,13 @@ public: 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_po_ao(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO_AO); } 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_po_ao (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO_AO, 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); } 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/smt_context.cpp b/src/smt/smt_context.cpp index 63979e657..0012f1433 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4453,6 +4453,7 @@ namespace smt { } recfun::util u(m); func_decl_ref_vector recfuns = u.get_rec_funs(); + std::cout << recfuns << "\n"; for (func_decl* f : recfuns) { auto& def = u.get_def(f); expr* rhs = def.get_rhs(); diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 65d30cea6..8339c658e 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -26,7 +26,11 @@ Notes: #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 { @@ -610,16 +614,130 @@ namespace smt { m.get_model().register_decl(r.decl(), fi); } - void theory_special_relations::init_model_plo(relation& r, model_generator& m) { - expr_ref inj = mk_inj(r, m); - expr_ref cls = mk_class(r, m); + 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)); - m.get_model().register_decl(r.decl(), fi); + 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) { - // NOT_IMPLEMENTED_YET(); + 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.mk_def(symbol("connected1"), 5, dom1, tup); + sort* dom2[3] = { s, s, listS }; + recfun::promise_def c2 = p.mk_def(symbol("connected2"), 3, dom2, tup); + sort* dom3[2] = { s, listS }; + recfun::promise_def mem = p.mk_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); + +#if 0 + // TBD: doesn't terminate with model_evaluator/rewriter + + // r.m_decl(x,y) -> snd(connected2(x,y,nil)) + + func_interp* fi = alloc(func_interp, m, 2); + fi->set_else(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_const(nil)))); + mg.get_model().register_decl(r.decl(), fi); +#endif + + } /**