mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity

consolidate rule checking in separate class

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-25 19:05:49 -07:00
parent 8e2fedbc2e
commit 74053275cf
5 changed files with 297 additions and 198 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -211,7 +211,7 @@ namespace datalog {
m_var_subst(m),
m_rule_manager(*this),
m_contains_p(*this),
m_check_pred(m_contains_p, m),
m_rule_properties(m, m_rule_manager, *this, m_contains_p),
m_transf(*this),
m_trail(*this),
m_pinned(m),
@ -452,10 +452,7 @@ namespace datalog {
rm.mk_rule(fml, p, m_rule_set, m_rule_names[m_rule_fmls_head]);
++m_rule_fmls_head;
}
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
for (; it != end; ++it) {
check_rule(*(*it));
}
check_rules(m_rule_set);
}
//
@ -541,140 +538,49 @@ namespace datalog {
m_engine->add_cover(level, pred, property);
}
void context::check_uninterpreted_free(rule& r) {
func_decl* f = 0;
if (get_rule_manager().has_uninterpreted_non_predicates(r, f)) {
std::stringstream stm;
stm << "Uninterpreted '"
<< f->get_name()
<< "' in ";
r.display(*this, stm);
throw default_exception(stm.str());
}
}
void context::check_quantifier_free(rule& r) {
if (get_rule_manager().has_quantifiers(r)) {
std::stringstream stm;
stm << "cannot process quantifiers in rule ";
r.display(*this, stm);
throw default_exception(stm.str());
}
}
void context::check_existential_tail(rule& r) {
unsigned ut_size = r.get_uninterpreted_tail_size();
unsigned t_size = r.get_tail_size();
TRACE("dl", get_rule_manager().display_smt2(r, tout); tout << "\n";);
for (unsigned i = ut_size; i < t_size; ++i) {
app* t = r.get_tail(i);
TRACE("dl", tout << "checking: " << mk_ismt2_pp(t, get_manager()) << "\n";);
if (m_check_pred(t)) {
std::ostringstream out;
out << "interpreted body " << mk_ismt2_pp(t, get_manager()) << " contains recursive predicate";
throw default_exception(out.str());
}
}
}
void context::check_positive_predicates(rule& r) {
ast_mark visited;
ptr_vector<expr> todo, tocheck;
unsigned ut_size = r.get_uninterpreted_tail_size();
unsigned t_size = r.get_tail_size();
for (unsigned i = 0; i < ut_size; ++i) {
if (r.is_neg_tail(i)) {
tocheck.push_back(r.get_tail(i));
}
}
ast_manager& m = get_manager();
contains_pred contains_p(*this);
check_pred check_pred(contains_p, get_manager());
for (unsigned i = ut_size; i < t_size; ++i) {
todo.push_back(r.get_tail(i));
}
while (!todo.empty()) {
expr* e = todo.back(), *e1, *e2;
todo.pop_back();
if (visited.is_marked(e)) {
continue;
}
visited.mark(e, true);
if (is_predicate(e)) {
}
else if (m.is_and(e) || m.is_or(e)) {
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
}
else if (m.is_implies(e, e1, e2)) {
tocheck.push_back(e1);
todo.push_back(e2);
}
else if (is_quantifier(e)) {
todo.push_back(to_quantifier(e)->get_expr());
}
else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
m.is_true(e1)) {
todo.push_back(e2);
}
else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
m.is_true(e2)) {
todo.push_back(e1);
}
else {
tocheck.push_back(e);
}
}
for (unsigned i = 0; i < tocheck.size(); ++i) {
expr* e = tocheck[i];
if (check_pred(e)) {
std::ostringstream out;
out << "recursive predicate " << mk_ismt2_pp(e, get_manager()) << " occurs nested in body";
r.display(*this, out << "\n");
throw default_exception(out.str());
}
}
}
#if 0
void context::check_rules(rule_set& r) {
m_rule_properties.set_generate_proof(generate_proof_trace());
switch(get_engine()) {
case DATALOG_ENGINE:
collect_properties(r);
check_quantifier_free(r);
check_uninterpreted_free(r);
check_existential_tail(r);
case DATALOG_ENGINE:
m_rule_properties.collect(r);
m_rule_properties.check_quantifier_free();
m_rule_properties.check_uninterpreted_free();
m_rule_properties.check_nested_free();
break;
case PDR_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
check_uninterpreted_free(r);
m_rule_properties.collect(r);
m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates();
m_rule_properties.check_uninterpreted_free();
break;
case QPDR_ENGINE:
check_positive_predicates(r);
check_uninterpreted_free(r);
m_rule_properties.collect(r);
m_rule_properties.check_for_negated_predicates();
m_rule_properties.check_uninterpreted_free();
break;
case BMC_ENGINE:
check_positive_predicates(r);
m_rule_properties.collect(r);
m_rule_properties.check_for_negated_predicates();
break;
case QBMC_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
m_rule_properties.collect(r);
m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates();
break;
case TAB_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
m_rule_properties.collect(r);
m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates();
break;
case DUALITY_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
m_rule_properties.collect(r);
m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates();
break;
case CLP_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
m_rule_properties.collect(r);
m_rule_properties.check_existential_tail();
m_rule_properties.check_for_negated_predicates();
break;
case DDNF_ENGINE:
break;
@ -683,57 +589,6 @@ namespace datalog {
UNREACHABLE();
break;
}
if (generate_proof_trace() && !r.get_proof()) {
m_rule_manager.mk_rule_asserted_proof(r);
}
}
#endif
void context::check_rule(rule& r) {
switch(get_engine()) {
case DATALOG_ENGINE:
check_quantifier_free(r);
check_uninterpreted_free(r);
check_existential_tail(r);
break;
case PDR_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
check_uninterpreted_free(r);
break;
case QPDR_ENGINE:
check_positive_predicates(r);
check_uninterpreted_free(r);
break;
case BMC_ENGINE:
check_positive_predicates(r);
break;
case QBMC_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
break;
case TAB_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
break;
case DUALITY_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
break;
case CLP_ENGINE:
check_existential_tail(r);
check_positive_predicates(r);
break;
case DDNF_ENGINE:
break;
case LAST_ENGINE:
default:
UNREACHABLE();
break;
}
if (generate_proof_trace() && !r.get_proof()) {
m_rule_manager.mk_rule_asserted_proof(r);
}
}
void context::add_rule(rule_ref& r) {
@ -984,11 +839,7 @@ namespace datalog {
// TODO: what?
if(get_engine() != DUALITY_ENGINE) {
new_query();
rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
rule_ref r(m_rule_manager);
for (; it != end; ++it) {
check_rule(*(*it));
}
check_rules(m_rule_set);
}
#endif
m_mc = mk_skip_model_converter();

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

@ -42,6 +42,7 @@ Revision History:
#include"expr_functors.h"
#include"dl_engine_base.h"
#include"bind_variables.h"
#include"rule_properties.h"
struct fixedpoint_params;
@ -141,6 +142,17 @@ namespace datalog {
SK_UINT64,
SK_SYMBOL
};
class contains_pred : public i_expr_pred {
context const& ctx;
public:
contains_pred(context& ctx): ctx(ctx) {}
virtual ~contains_pred() {}
virtual bool operator()(expr* e) {
return ctx.is_predicate(e);
}
};
private:
class sort_domain;
@ -154,17 +166,6 @@ namespace datalog {
typedef obj_map<const func_decl, svector<symbol> > pred2syms;
typedef obj_map<const sort, sort_domain*> sort_domain_map;
class contains_pred : public i_expr_pred {
context const& ctx;
public:
contains_pred(context& ctx): ctx(ctx) {}
virtual ~contains_pred() {}
virtual bool operator()(expr* e) {
return ctx.is_predicate(e);
}
};
ast_manager & m;
register_engine_base& m_register_engine;
@ -179,7 +180,7 @@ namespace datalog {
var_subst m_var_subst;
rule_manager m_rule_manager;
contains_pred m_contains_p;
check_pred m_check_pred;
rule_properties m_rule_properties;
rule_transformer m_transf;
trail_stack<context> m_trail;
ast_ref_vector m_pinned;
@ -419,7 +420,7 @@ namespace datalog {
/**
\brief Check if rule is well-formed according to engine.
*/
void check_rule(rule& r);
void check_rules(rule_set& r);
/**
\brief Return true if facts to \c pred can be added using the \c add_table_fact() function.
@ -565,11 +566,6 @@ namespace datalog {
void ensure_engine();
void check_quantifier_free(rule& r);
void check_uninterpreted_free(rule& r);
void check_existential_tail(rule& r);
void check_positive_predicates(rule& r);
// auxilary functions for SMT2 pretty-printer.
void declare_vars(expr_ref_vector& rules, mk_fresh_name& mk_fresh, std::ostream& out);

189
src/muz/base/rule_properties.cpp Normal file
View file

@ -0,0 +1,189 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
rule_properties.cpp
Abstract:
Collect properties of rules.
Author:
Nikolaj Bjorner (nbjorner) 9-25-2014
Notes:
--*/
#include"expr_functors.h"
#include"rule_properties.h"
#include"dl_rule_set.h"
#include"for_each_expr.h"
#include"dl_context.h"
using namespace datalog;
rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p):
m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_generate_proof(false) {}
rule_properties::~rule_properties() {}
void rule_properties::collect(rule_set const& rules) {
reset();
rule_set::iterator it = rules.begin(), end = rules.end();
expr_sparse_mark visited;
for (; it != end; ++it) {
rule* r = *it;
m_rule = r;
unsigned ut_size = r->get_uninterpreted_tail_size();
unsigned t_size = r->get_tail_size();
if (r->has_negation()) {
m_negative_rules.push_back(r);
}
for (unsigned i = ut_size; i < t_size; ++i) {
for_each_expr_core<rule_properties,expr_sparse_mark, true, false>(*this, visited, r->get_tail(i));
}
if (m_generate_proof && !r->get_proof()) {
rm.mk_rule_asserted_proof(*r);
}
}
}
void rule_properties::check_quantifier_free() {
if (!m_quantifiers.empty()) {
quantifier* q = m_quantifiers.begin()->m_key;
rule* r = m_quantifiers.begin()->m_value;
std::stringstream stm;
stm << "cannot process quantifier in rule ";
r->display(m_ctx, stm);
throw default_exception(stm.str());
}
}
void rule_properties::check_for_negated_predicates() {
if (!m_negative_rules.empty()) {
rule* r = m_negative_rules[0];
std::stringstream stm;
stm << "Rule contains negative predicate ";
r->display(m_ctx, stm);
throw default_exception(stm.str());
}
}
void rule_properties::check_uninterpreted_free() {
if (!m_uninterp_funs.empty()) {
func_decl* f = m_uninterp_funs.begin()->m_key;
rule* r = m_uninterp_funs.begin()->m_value;
std::stringstream stm;
stm << "Uninterpreted '"
<< f->get_name()
<< "' in ";
r->display(m_ctx, stm);
throw default_exception(stm.str());
}
}
void rule_properties::check_nested_free() {
if (!m_interp_pred.empty()) {
std::stringstream stm;
rule* r = m_interp_pred[0];
stm << "Rule contains nested predicates ";
r->display(m_ctx, stm);
throw default_exception(stm.str());
}
}
void rule_properties::check_existential_tail() {
ast_mark visited;
ptr_vector<expr> todo, tocheck;
for (unsigned i = 0; i < m_interp_pred.size(); ++i) {
rule& r = *m_interp_pred[i];
unsigned ut_size = r.get_uninterpreted_tail_size();
unsigned t_size = r.get_tail_size();
for (unsigned i = ut_size; i < t_size; ++i) {
todo.push_back(r.get_tail(i));
}
}
context::contains_pred contains_p(m_ctx);
check_pred check_pred(contains_p, m);
while (!todo.empty()) {
expr* e = todo.back(), *e1, *e2;
todo.pop_back();
if (visited.is_marked(e)) {
continue;
}
visited.mark(e, true);
if (m_is_predicate(e)) {
}
else if (m.is_and(e) || m.is_or(e)) {
todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
}
else if (m.is_implies(e, e1, e2)) {
tocheck.push_back(e1);
todo.push_back(e2);
}
else if (is_quantifier(e)) {
todo.push_back(to_quantifier(e)->get_expr());
}
else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
m.is_true(e1)) {
todo.push_back(e2);
}
else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) &&
m.is_true(e2)) {
todo.push_back(e1);
}
else {
tocheck.push_back(e);
}
}
for (unsigned i = 0; i < tocheck.size(); ++i) {
expr* e = tocheck[i];
if (check_pred(e)) {
std::ostringstream out;
out << "recursive predicate " << mk_ismt2_pp(e, m) << " occurs nested in the body of a rule";
throw default_exception(out.str());
}
}
}
void rule_properties::insert(ptr_vector<rule>& rules, rule* r) {
if (rules.empty() || rules.back() != r) {
rules.push_back(r);
}
}
void rule_properties::operator()(var* n) { }
void rule_properties::operator()(quantifier* n) {
m_quantifiers.insert(n, m_rule);
}
void rule_properties::operator()(app* n) {
if (m_is_predicate(n)) {
insert(m_interp_pred, m_rule);
}
else if (is_uninterp(n)) {
m_uninterp_funs.insert(n->get_decl(), m_rule);
}
else if (m_dt.is_accessor(n)) {
sort* s = m.get_sort(n->get_arg(0));
SASSERT(m_dt.is_datatype(s));
if (m_dt.get_datatype_constructors(s)->size() > 1) {
m_uninterp_funs.insert(n->get_decl(), m_rule);
}
}
}
void rule_properties::reset() {
m_quantifiers.reset();
m_uninterp_funs.reset();
m_interp_pred.reset();
m_negative_rules.reset();
}

60
src/muz/base/rule_properties.h Normal file
View file

@ -0,0 +1,60 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
rule_properties.h
Abstract:
Collect properties of rules.
Author:
Nikolaj Bjorner (nbjorner) 9-25-2014
Notes:
--*/
#ifndef _RULE_PROPERTIES_H_
#define _RULE_PROPERTIES_H_
#include"ast.h"
#include"datatype_decl_plugin.h"
#include"dl_rule.h"
namespace datalog {
class rule_properties {
ast_manager& m;
rule_manager& rm;
context& m_ctx;
i_expr_pred& m_is_predicate;
datatype_util m_dt;
bool m_generate_proof;
rule* m_rule;
obj_map<quantifier, rule*> m_quantifiers;
obj_map<func_decl, rule*> m_uninterp_funs;
ptr_vector<rule> m_interp_pred;
ptr_vector<rule> m_negative_rules;
void insert(ptr_vector<rule>& rules, rule* r);
public:
rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& is_predicate);
~rule_properties();
void set_generate_proof(bool generate_proof) { m_generate_proof = generate_proof; }
void collect(rule_set const& r);
void check_quantifier_free();
void check_uninterpreted_free();
void check_existential_tail();
void check_for_negated_predicates();
void check_nested_free();
void operator()(var* n);
void operator()(quantifier* n);
void operator()(app* n);
void reset();
};
}
#endif /* _RULE_PROPERTIES_H_ */

5
src/test/dl_query.cpp
View file

@ -143,8 +143,11 @@ void dl_query_test_wpa(smt_params & fparams, params_ref& params) {
ctx.updt_params(params);
{
wpa_parser* p = wpa_parser::create(ctx, m);
TRUSTME( p->parse_directory(problem_dir) );
bool = ok = p->parse_directory(problem_dir);
dealloc(p);
if (!ok) {
std::cout << "Could not parse: " << problem_dir << "\n";
}
}
const unsigned attempts = 10;