mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

adding po evaluator

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-27 16:59:13 -07:00
parent f55e4ccc41
commit 175008a6c6
8 changed files with 233 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
src/api/api_datatype.cpp
View file

@ -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 s = dt_util.mk_list_datatype(to_sort(elem_sort), to_symbol(name), cons, is_cons, head, tail, nil, is_nil);
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);
}
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<func_decl> 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<func_decl> 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<func_decl> 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);

79
src/ast/datatype_decl_plugin.cpp
View file

@ -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<func_decl> 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<func_decl> 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<func_decl> const& cnstrs = *get_datatype_constructors(s);
SASSERT(cnstrs.size() == 1);
ptr_vector<func_decl> 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<std::pair<symbol, sort*>> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs) {
ptr_vector<accessor_decl> 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<func_decl> const& cnstrs = *get_datatype_constructors(s);
SASSERT(cnstrs.size() == 1);
ptr_vector<func_decl> 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) {

6
src/ast/datatype_decl_plugin.h
View file

@ -364,6 +364,12 @@ namespace datatype {
decl::plugin* get_plugin() { return m_plugin; }
void get_defs(sort* s, ptr_vector<def>& 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<std::pair<symbol, sort*>> const& elems, symbol const& name, symbol const& test, func_decl_ref& tup, func_decl_ref_vector& accs);
};
};

4
src/ast/special_relations_decl_plugin.h
View file

@ -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); }

1
src/model/model.cpp
View file

@ -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);

1
src/model/model_core.cpp
View file

@ -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);

1
src/smt/smt_context.cpp
View file

@ -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();

128
src/smt/theory_special_relations.cpp
View file

@ -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
}
/**