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

print output predicates as part of displaying rules

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-22 21:17:05 -07:00
parent da8c9134f8
commit 9b893c625b
4 changed files with 45 additions and 50 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/api/api_datalog.cpp
View file

@ -125,7 +125,7 @@ namespace api {
return "unknown";
}
}
std::string to_string(unsigned num_queries, expr*const* queries) {
std::string to_string(unsigned num_queries, expr* const* queries) {
std::stringstream str;
m_context.display_smt2(num_queries, queries, str);
return str.str();
@ -466,13 +466,16 @@ extern "C" {
ast_manager& m = mk_c(c)->m();
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
mk_c(c)->save_object(v);
expr_ref_vector rules(m);
expr_ref_vector rules(m), queries(m);
svector<symbol> names;
to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, names);
to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, queries, names);
for (unsigned i = 0; i < rules.size(); ++i) {
v->m_ast_vector.push_back(rules[i].get());
}
for (unsigned i = 0; i < queries.size(); ++i) {
v->m_ast_vector.push_back(m.mk_not(queries[i].get()));
}
RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0);
}

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

@ -1117,7 +1117,7 @@ namespace datalog {
}
}
void context::get_rules_as_formulas(expr_ref_vector& rules, svector<symbol>& names) {
void context::get_rules_as_formulas(expr_ref_vector& rules, expr_ref_vector& queries, svector<symbol>& names) {
expr_ref fml(m);
datalog::rule_manager& rm = get_rule_manager();
@ -1136,9 +1136,30 @@ namespace datalog {
}
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
for (; it != end; ++it) {
(*it)->to_formula(fml);
rules.push_back(fml);
names.push_back((*it)->name());
rule* r = *it;
r->to_formula(fml);
func_decl* h = r->get_decl();
if (m_rule_set.is_output_predicate(h)) {
expr* body = fml;
expr* e2;
if (is_quantifier(body)) {
quantifier* q = to_quantifier(body);
expr* e = q->get_expr();
VERIFY(m.is_implies(e, body, e2));
fml = m.mk_quantifier(false, q->get_num_decls(),
q->get_decl_sorts(), q->get_decl_names(),
body);
}
else {
VERIFY(m.is_implies(body, body, e2));
fml = body;
}
queries.push_back(fml);
}
else {
rules.push_back(fml);
names.push_back(r->name());
}
}
for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) {
rules.push_back(m_rule_fmls[i].get());
@ -1146,10 +1167,7 @@ namespace datalog {
}
}
void context::display_smt2(
unsigned num_queries,
expr* const* queries,
std::ostream& out) {
void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) {
ast_manager& m = get_manager();
free_func_visitor visitor(m);
expr_mark visited;
@ -1157,7 +1175,7 @@ namespace datalog {
unsigned num_axioms = m_background.size();
expr* const* axioms = m_background.c_ptr();
expr_ref fml(m);
expr_ref_vector rules(m);
expr_ref_vector rules(m), queries(m);
svector<symbol> names;
bool use_fixedpoint_extensions = m_params->print_fixedpoint_extensions();
bool print_low_level = m_params->print_low_level_smt2();
@ -1165,13 +1183,14 @@ namespace datalog {
#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env);
get_rules_as_formulas(rules, names);
get_rules_as_formulas(rules, queries, names);
queries.append(num_queries, qs);
smt2_pp_environment_dbg env(m);
mk_fresh_name fresh_names;
collect_free_funcs(num_axioms, axioms, visited, visitor, fresh_names);
collect_free_funcs(rules.size(), rules.c_ptr(), visited, visitor, fresh_names);
collect_free_funcs(num_queries, queries, visited, visitor, fresh_names);
collect_free_funcs(queries.size(), queries.c_ptr(), visited, visitor, fresh_names);
func_decl_set funcs;
func_decl_set::iterator it = visitor.funcs().begin();
func_decl_set::iterator end = visitor.funcs().end();
@ -1257,22 +1276,22 @@ namespace datalog {
out << ")\n";
}
if (use_fixedpoint_extensions) {
for (unsigned i = 0; i < num_queries; ++i) {
for (unsigned i = 0; i < queries.size(); ++i) {
out << "(query ";
PP(queries[i]);
PP(queries[i].get());
out << ")\n";
}
}
else {
for (unsigned i = 0; i < num_queries; ++i) {
if (num_queries > 1) out << "(push)\n";
for (unsigned i = 0; i < queries.size(); ++i) {
if (queries.size() > 1) out << "(push)\n";
out << "(assert ";
expr_ref q(m);
q = m.mk_not(queries[i]);
q = m.mk_not(queries[i].get());
PP(q);
out << ")\n";
out << "(check-sat)\n";
if (num_queries > 1) out << "(pop)\n";
if (queries.size() > 1) out << "(pop)\n";
}
}
}

4
src/muz/base/dl_context.h
View file

@ -362,7 +362,7 @@ namespace datalog {
rule_set & get_rules() { flush_add_rules(); return m_rule_set; }
void get_rules_as_formulas(expr_ref_vector& fmls, svector<symbol>& names);
void get_rules_as_formulas(expr_ref_vector& fmls, expr_ref_vector& qs, svector<symbol>& names);
void get_raw_rule_formulas(expr_ref_vector& fmls, svector<symbol>& names);
void add_fact(app * head);
@ -463,7 +463,7 @@ namespace datalog {
void display(std::ostream & out) const;
void display_smt2(unsigned num_queries, expr* const* queries, std::ostream& out);
void display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out);
void display_profile(std::ostream& out) const;

29
src/muz/ddnf/ddnf.cpp
View file

@ -25,7 +25,6 @@ Revision History:
#include "dl_context.h"
#include "scoped_proof.h"
#include "bv_decl_plugin.h"
//#include "dl_decl_plugin.h"
namespace datalog {
@ -485,7 +484,6 @@ namespace datalog {
ast_manager& m;
rule_manager& rm;
bv_util bv;
// dl_decl_util dl;
volatile bool m_cancel;
ptr_vector<expr> m_todo;
ast_mark m_visited1, m_visited2;
@ -502,7 +500,6 @@ namespace datalog {
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
bv(m),
// dl(m),
m_cancel(false),
m_trail(m),
m_inner_ctx(m, m_ctx.get_register_engine(), m_ctx.get_fparams())
@ -688,25 +685,7 @@ namespace datalog {
void dump_rules(rule_set& rules) {
init_ctx(rules);
func_decl* q = rules.get_output_predicate();
rule_vector const& qs = rules.get_predicate_rules(q);
SASSERT(qs.size() == 1);
app* qa = qs[0]->get_head();
expr_ref query(m);
ptr_vector<sort> sorts;
vector<symbol> names;
get_free_vars(qa, sorts);
// TBD: get the real names from the original query.
for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[i]) sorts[i] = m.mk_bool_sort();
std::ostringstream strm;
strm << "q" << i;
names.push_back(symbol(strm.str().c_str()));
}
sorts.reverse();
query = m.mk_quantifier(false, sorts.size(), sorts.c_ptr(), names.c_ptr(), qa);
expr* qe = query;
m_inner_ctx.display_smt2(1, &qe, std::cout);
m_inner_ctx.display_smt2(0, 0, std::cout);
}
lbool execute_rules(rule_set& rules) {
@ -806,12 +785,6 @@ namespace datalog {
++nb;
}
return bv.mk_sort(nb);
#if 0
std::ostringstream strm;
strm << "S" << num_elems;
symbol name(strm.str().c_str());
return dl.mk_sort(name, num_elems);
#endif
}
UNREACHABLE();
return 0;