mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

change queries to take function names instead of arbitrary predicates. This allows to bypass issues with having arbitrary query expressions compiled in arbitrary ways to auxiliary predicates where names of bound variables are reshuffled. See also Stackoverflow http://stackoverflow.com/questions/34693719/bug-in-z3-datalog

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-10 20:43:41 -08:00
parent 082dcda7f7
commit 131f9e2247
3 changed files with 23 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/muz/base/dl_context.cpp
View file

@ -891,6 +891,7 @@ namespace datalog {
}
lbool context::rel_query(unsigned num_rels, func_decl * const* rels) {
m_last_answer = 0;
ensure_engine();
return m_engine->query(num_rels, rels);
}

25
src/muz/fp/dl_cmds.cpp
View file

@ -114,9 +114,16 @@ struct dl_context {
}
}
bool collect_query(expr* q) {
bool collect_query(func_decl* q) {
if (m_collected_cmds) {
expr_ref qr = m_context->bind_vars(q, false);
ast_manager& m = m_cmd.m();
expr_ref qr(m);
expr_ref_vector args(m);
for (unsigned i = 0; i < q->get_arity(); ++i) {
args.push_back(m.mk_var(i, q->get_domain(i)));
}
qr = m.mk_app(q, args.size(), args.c_ptr());
qr = m_context->bind_vars(qr, false);
m_collected_cmds->m_queries.push_back(qr);
m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_queries));
return true;
@ -187,30 +194,30 @@ public:
virtual void finalize(cmd_context & ctx) {
}
virtual void execute(cmd_context & ctx) {
m_dl_ctx->add_rule(m_t, m_name, m_bound);
m_dl_ctx->add_rule(m_t, m_name, m_bound);
}
};
class dl_query_cmd : public parametric_cmd {
ref<dl_context> m_dl_ctx;
expr* m_target;
func_decl* m_target;
public:
dl_query_cmd(dl_context * dl_ctx):
parametric_cmd("query"),
m_dl_ctx(dl_ctx),
m_target(0) {
}
virtual char const * get_usage() const { return "(exists (q) (and body))"; }
virtual char const * get_usage() const { return "predicate"; }
virtual char const * get_main_descr() const {
return "pose a query based on the Horn rules.";
return "pose a query to a predicate based on the Horn rules.";
}
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
if (m_target == 0) return CPK_EXPR;
if (m_target == 0) return CPK_FUNC_DECL;
return parametric_cmd::next_arg_kind(ctx);
}
virtual void set_next_arg(cmd_context & ctx, expr * t) {
virtual void set_next_arg(cmd_context & ctx, func_decl* t) {
m_target = t;
}
@ -239,7 +246,7 @@ public:
scoped_timer timer(timeout, &eh);
cmd_context::scoped_watch sw(ctx);
try {
status = dlctx.query(m_target);
status = dlctx.rel_query(1, &m_target);
}
catch (z3_error & ex) {
ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl;

12
src/parsers/smt2/smt2parser.cpp
View file

@ -719,9 +719,9 @@ namespace smt2 {
SASSERT(sort_stack().size() == stack_pos + 1);
}
unsigned parse_sorts() {
unsigned sz = 0;
check_lparen_next("invalid list of sorts, '(' expected");
unsigned parse_sorts(char const* context) {
unsigned sz = 0;
check_lparen_next(context);
while (!curr_is_rparen()) {
parse_sort();
sz++;
@ -2019,7 +2019,7 @@ namespace smt2 {
symbol id = curr_id();
next();
unsigned spos = sort_stack().size();
unsigned num_params = parse_sorts();
unsigned num_params = parse_sorts("Parsing function declaration. Expecting sort list '('");
parse_sort();
func_decl_ref f(m());
f = m().mk_func_decl(id, num_params, sort_stack().c_ptr() + spos, sort_stack().back());
@ -2300,7 +2300,7 @@ namespace smt2 {
next();
}
unsigned spos = sort_stack().size();
parse_sorts();
parse_sorts("Parsing function name. Expecting sort list startig with '(' to disambiguate function name");
unsigned domain_size = sort_stack().size() - spos;
parse_sort();
func_decl * d = m_ctx.find_func_decl(id, indices.size(), indices.c_ptr(), domain_size, sort_stack().c_ptr() + spos, sort_stack().back());
@ -2380,7 +2380,7 @@ namespace smt2 {
return;
case CPK_SORT_LIST: {
unsigned spos = sort_stack().size();
unsigned num = parse_sorts();
unsigned num = parse_sorts("expecting sort list starting with '('");
m_curr_cmd->set_next_arg(m_ctx, num, sort_stack().c_ptr() + spos);
break;
}