mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fix query for non-relational engines

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-12 07:57:10 -08:00
parent 905fa56120
commit 01c3e02e99
2 changed files with 24 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/muz/base/dl_engine_base.h
View file

@ -44,7 +44,26 @@ namespace datalog {
virtual expr_ref get_answer() = 0;
virtual lbool query(expr* q) = 0;
virtual lbool query(unsigned num_rels, func_decl*const* rels) { return l_undef; }
virtual lbool query(unsigned num_rels, func_decl*const* rels) {
if (num_rels != 1) return l_undef;
expr_ref q(m);
expr_ref_vector args(m);
sort_ref_vector sorts(m);
svector<symbol> names;
func_decl* r = rels[0];
for (unsigned i = 0; i < r->get_arity(); ++i) {
args.push_back(m.mk_var(i, r->get_domain(i)));
sorts.push_back(r->get_domain(i));
names.push_back(symbol(i));
}
sorts.reverse();
names.reverse();
q = m.mk_app(r, args.size(), args.c_ptr());
if (!args.empty()) {
q = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), q);
}
return query(q);
}
virtual void reset_statistics() {}
virtual void display_profile(std::ostream& out) const {}

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

@ -268,10 +268,10 @@ public:
print_certificate(ctx);
break;
case l_undef:
if(dlctx.get_status() == datalog::BOUNDED){
ctx.regular_stream() << "bounded\n";
print_certificate(ctx);
break;
if (dlctx.get_status() == datalog::BOUNDED){
ctx.regular_stream() << "bounded\n";
print_certificate(ctx);
break;
}
ctx.regular_stream() << "unknown\n";
switch(dlctx.get_status()) {