mirror of
https://github.com/Z3Prover/z3
synced 2025-10-25 08:54:35 +00:00
tune and fix doc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
16f80fce92
commit
918d52f1b0
13 changed files with 188 additions and 103 deletions
|
|
@ -574,7 +574,7 @@ namespace datalog {
|
|||
|
||||
void context::check_uninterpreted_free(rule& r) {
|
||||
func_decl* f = 0;
|
||||
if (r.has_uninterpreted_non_predicates(m, f)) {
|
||||
if (get_rule_manager().has_uninterpreted_non_predicates(r, f)) {
|
||||
std::stringstream stm;
|
||||
stm << "Uninterpreted '"
|
||||
<< f->get_name()
|
||||
|
|
@ -585,7 +585,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void context::check_quantifier_free(rule& r) {
|
||||
if (r.has_quantifiers()) {
|
||||
if (get_rule_manager().has_quantifiers(r)) {
|
||||
std::stringstream stm;
|
||||
stm << "cannot process quantifiers in rule ";
|
||||
r.display(*this, stm);
|
||||
|
|
|
|||
|
|
@ -56,7 +56,8 @@ namespace datalog {
|
|||
m_hnf(m),
|
||||
m_qe(m),
|
||||
m_cfg(m),
|
||||
m_rwr(m, false, m_cfg) {}
|
||||
m_rwr(m, false, m_cfg),
|
||||
m_ufproc(m) {}
|
||||
|
||||
void rule_manager::inc_ref(rule * r) {
|
||||
if (r) {
|
||||
|
|
@ -911,83 +912,40 @@ namespace datalog {
|
|||
return false;
|
||||
}
|
||||
|
||||
struct uninterpreted_function_finder_proc {
|
||||
ast_manager& m;
|
||||
datatype_util m_dt;
|
||||
bool m_found;
|
||||
func_decl* m_func;
|
||||
uninterpreted_function_finder_proc(ast_manager& m):
|
||||
m(m), m_dt(m), m_found(false), m_func(0) {}
|
||||
void operator()(var * n) { }
|
||||
void operator()(quantifier * n) { }
|
||||
void operator()(app * n) {
|
||||
if (is_uninterp(n)) {
|
||||
m_found = true;
|
||||
m_func = n->get_decl();
|
||||
}
|
||||
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_found = true;
|
||||
m_func = n->get_decl();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool found(func_decl*& f) const { f = m_func; return m_found; }
|
||||
};
|
||||
|
||||
//
|
||||
// non-predicates may appear only in the interpreted tail, it is therefore
|
||||
// sufficient only to check the tail.
|
||||
//
|
||||
bool rule::has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const {
|
||||
unsigned sz = get_tail_size();
|
||||
uninterpreted_function_finder_proc proc(m);
|
||||
expr_mark visited;
|
||||
for (unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) {
|
||||
for_each_expr(proc, visited, get_tail(i));
|
||||
bool rule_manager::has_uninterpreted_non_predicates(rule const& r, func_decl*& f) const {
|
||||
unsigned sz = r.get_tail_size();
|
||||
m_ufproc.reset();
|
||||
m_visited.reset();
|
||||
for (unsigned i = r.get_uninterpreted_tail_size(); i < sz && !m_ufproc.found(f); ++i) {
|
||||
for_each_expr_core<uninterpreted_function_finder_proc,expr_sparse_mark, true, false>(m_ufproc, m_visited, r.get_tail(i));
|
||||
}
|
||||
return proc.found(f);
|
||||
return m_ufproc.found(f);
|
||||
}
|
||||
|
||||
|
||||
struct quantifier_finder_proc {
|
||||
bool m_exist;
|
||||
bool m_univ;
|
||||
quantifier_finder_proc() : m_exist(false), m_univ(false) {}
|
||||
void operator()(var * n) { }
|
||||
void operator()(quantifier * n) {
|
||||
if (n->is_forall()) {
|
||||
m_univ = true;
|
||||
}
|
||||
else {
|
||||
SASSERT(n->is_exists());
|
||||
m_exist = true;
|
||||
}
|
||||
}
|
||||
void operator()(app * n) { }
|
||||
};
|
||||
|
||||
//
|
||||
// Quantifiers may appear only in the interpreted tail, it is therefore
|
||||
// sufficient only to check the interpreted tail.
|
||||
//
|
||||
void rule::has_quantifiers(bool& existential, bool& universal) const {
|
||||
unsigned sz = get_tail_size();
|
||||
quantifier_finder_proc proc;
|
||||
expr_mark visited;
|
||||
for (unsigned i = get_uninterpreted_tail_size(); i < sz; ++i) {
|
||||
for_each_expr(proc, visited, get_tail(i));
|
||||
void rule_manager::has_quantifiers(rule const& r, bool& existential, bool& universal) const {
|
||||
unsigned sz = r.get_tail_size();
|
||||
m_qproc.reset();
|
||||
m_visited.reset();
|
||||
for (unsigned i = r.get_uninterpreted_tail_size(); i < sz; ++i) {
|
||||
for_each_expr_core<quantifier_finder_proc,expr_sparse_mark, true, false>(m_qproc, m_visited, r.get_tail(i));
|
||||
}
|
||||
existential = proc.m_exist;
|
||||
universal = proc.m_univ;
|
||||
existential = m_qproc.m_exist;
|
||||
universal = m_qproc.m_univ;
|
||||
}
|
||||
|
||||
bool rule::has_quantifiers() const {
|
||||
bool rule_manager::has_quantifiers(rule const& r) const {
|
||||
bool exist, univ;
|
||||
has_quantifiers(exist, univ);
|
||||
has_quantifiers(r, exist, univ);
|
||||
return exist || univ;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -31,6 +31,7 @@ Revision History:
|
|||
#include"hnf.h"
|
||||
#include"qe_lite.h"
|
||||
#include"var_subst.h"
|
||||
#include"datatype_decl_plugin.h"
|
||||
|
||||
namespace datalog {
|
||||
|
||||
|
|
@ -43,6 +44,57 @@ namespace datalog {
|
|||
typedef obj_ref<rule, rule_manager> rule_ref;
|
||||
typedef ref_vector<rule, rule_manager> rule_ref_vector;
|
||||
typedef ptr_vector<rule> rule_vector;
|
||||
|
||||
|
||||
struct quantifier_finder_proc {
|
||||
bool m_exist;
|
||||
bool m_univ;
|
||||
quantifier_finder_proc() : m_exist(false), m_univ(false) {}
|
||||
void operator()(var * n) { }
|
||||
void operator()(quantifier * n) {
|
||||
if (n->is_forall()) {
|
||||
m_univ = true;
|
||||
}
|
||||
else {
|
||||
SASSERT(n->is_exists());
|
||||
m_exist = true;
|
||||
}
|
||||
}
|
||||
void operator()(app * n) { }
|
||||
void reset() { m_exist = m_univ = false; }
|
||||
};
|
||||
|
||||
struct uninterpreted_function_finder_proc {
|
||||
ast_manager& m;
|
||||
datatype_util m_dt;
|
||||
bool m_found;
|
||||
func_decl* m_func;
|
||||
uninterpreted_function_finder_proc(ast_manager& m):
|
||||
m(m), m_dt(m), m_found(false), m_func(0) {}
|
||||
|
||||
void reset() { m_found = false; m_func = 0; }
|
||||
|
||||
void operator()(var * n) { }
|
||||
void operator()(quantifier * n) { }
|
||||
void operator()(app * n) {
|
||||
if (is_uninterp(n)) {
|
||||
m_found = true;
|
||||
m_func = n->get_decl();
|
||||
}
|
||||
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_found = true;
|
||||
m_func = n->get_decl();
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool found(func_decl*& f) const { f = m_func; return m_found; }
|
||||
};
|
||||
|
||||
|
||||
/**
|
||||
\brief Manager for the \c rule class
|
||||
|
||||
|
|
@ -75,6 +127,9 @@ namespace datalog {
|
|||
qe_lite m_qe;
|
||||
remove_label_cfg m_cfg;
|
||||
rewriter_tpl<remove_label_cfg> m_rwr;
|
||||
mutable uninterpreted_function_finder_proc m_ufproc;
|
||||
mutable quantifier_finder_proc m_qproc;
|
||||
mutable expr_sparse_mark m_visited;
|
||||
|
||||
|
||||
// only the context can create a rule_manager
|
||||
|
|
@ -220,6 +275,10 @@ namespace datalog {
|
|||
|
||||
std::ostream& display_smt2(rule const& r, std::ostream & out);
|
||||
|
||||
bool has_uninterpreted_non_predicates(rule const& r, func_decl*& f) const;
|
||||
void has_quantifiers(rule const& r, bool& existential, bool& universal) const;
|
||||
bool has_quantifiers(rule const& r) const;
|
||||
|
||||
};
|
||||
|
||||
class rule : public accounted_object {
|
||||
|
|
@ -295,9 +354,6 @@ namespace datalog {
|
|||
*/
|
||||
bool is_in_tail(const func_decl * p, bool only_positive=false) const;
|
||||
|
||||
bool has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const;
|
||||
void has_quantifiers(bool& existential, bool& universal) const;
|
||||
bool has_quantifiers() const;
|
||||
bool has_negation() const;
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -88,6 +88,7 @@ class hnf::imp {
|
|||
proof_ref_vector m_defs;
|
||||
contains_predicate_proc m_proc;
|
||||
expr_free_vars m_free_vars;
|
||||
ast_fast_mark1 m_mark1;
|
||||
|
||||
|
||||
public:
|
||||
|
|
@ -106,10 +107,37 @@ public:
|
|||
m_proc(*this) {
|
||||
}
|
||||
|
||||
bool is_horn(expr* n) {
|
||||
expr* n1, *n2;
|
||||
while (is_forall(n)) n = to_quantifier(n)->get_expr();
|
||||
if (m.is_implies(n, n1, n2) && is_predicate(n2)) {
|
||||
app* a1 = to_app(n1);
|
||||
if (m.is_and(a1)) {
|
||||
for (unsigned i = 0; i < a1->get_num_args(); ++i) {
|
||||
if (!is_predicate(a1->get_arg(i)) &&
|
||||
contains_predicate(a1->get_arg(i))) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (!is_predicate(a1) && contains_predicate(a1)) {
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
void operator()(expr * n,
|
||||
proof* p,
|
||||
expr_ref_vector& result,
|
||||
proof_ref_vector& ps) {
|
||||
if (is_horn(n)) {
|
||||
result.push_back(n);
|
||||
ps.push_back(p);
|
||||
return;
|
||||
}
|
||||
expr_ref fml(m);
|
||||
proof_ref pr(m);
|
||||
m_todo.reset();
|
||||
|
|
@ -184,9 +212,11 @@ private:
|
|||
|
||||
bool contains_predicate(expr* fml) {
|
||||
try {
|
||||
quick_for_each_expr(m_proc, fml);
|
||||
quick_for_each_expr(m_proc, m_mark1, fml);
|
||||
m_mark1.reset();
|
||||
}
|
||||
catch (contains_predicate_proc::found) {
|
||||
m_mark1.reset();
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue