mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

fix #3775

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-05 14:04:00 -07:00
parent bb1119a6ca
commit 406c0792f1
2 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/muz/base/dl_rule.cpp
View file

@ -912,7 +912,7 @@ namespace datalog {
// Quantifiers may appear only in the interpreted tail, it is therefore // Quantifiers may appear only in the interpreted tail, it is therefore
// sufficient only to check the interpreted tail. // sufficient only to check the interpreted tail.
// //
void rule_manager::has_quantifiers(rule const& r, bool& existential, bool& universal) const { void rule_manager::has_quantifiers(rule const& r, bool& existential, bool& universal, bool& lam) const {
unsigned sz = r.get_tail_size(); unsigned sz = r.get_tail_size();
m_qproc.reset(); m_qproc.reset();
m_visited.reset(); m_visited.reset();
@ -921,12 +921,13 @@ namespace datalog {
} }
existential = m_qproc.m_exist; existential = m_qproc.m_exist;
universal = m_qproc.m_univ; universal = m_qproc.m_univ;
lam = m_qproc.m_lambda;
} }
bool rule_manager::has_quantifiers(rule const& r) const { bool rule_manager::has_quantifiers(rule const& r) const {
bool exist, univ; bool exist, univ, lam;
has_quantifiers(r, exist, univ); has_quantifiers(r, exist, univ, lam);
return exist || univ; return exist || univ || lam;
} }
bool rule_manager::is_finite_domain(rule const& r) const { bool rule_manager::is_finite_domain(rule const& r) const {

9
src/muz/base/dl_rule.h
View file

@ -79,17 +79,18 @@ namespace datalog {
struct quantifier_finder_proc { struct quantifier_finder_proc {
bool m_exist; bool m_exist;
bool m_univ; bool m_univ;
quantifier_finder_proc() : m_exist(false), m_univ(false) {} bool m_lambda;
quantifier_finder_proc() : m_exist(false), m_univ(false), m_lambda(false) {}
void operator()(var * n) { } void operator()(var * n) { }
void operator()(quantifier * n) { void operator()(quantifier * n) {
switch (n->get_kind()) { switch (n->get_kind()) {
case forall_k: m_univ = true; break; case forall_k: m_univ = true; break;
case exists_k: m_exist = true; break; case exists_k: m_exist = true; break;
case lambda_k: UNREACHABLE(); case lambda_k: m_lambda = true; break;
} }
} }
void operator()(app * n) { } void operator()(app * n) { }
void reset() { m_exist = m_univ = false; } void reset() { m_exist = m_univ = m_lambda = false; }
}; };
struct fd_finder_proc { struct fd_finder_proc {
@ -278,7 +279,7 @@ namespace datalog {
std::ostream& display_smt2(rule const& r, std::ostream & out); std::ostream& display_smt2(rule const& r, std::ostream & out);
bool has_uninterpreted_non_predicates(rule const& r, func_decl*& f) const; bool has_uninterpreted_non_predicates(rule const& r, func_decl*& f) const;
void has_quantifiers(rule const& r, bool& existential, bool& universal) const; void has_quantifiers(rule const& r, bool& existential, bool& universal, bool& lam) const;
bool has_quantifiers(rule const& r) const; bool has_quantifiers(rule const& r) const;
bool is_finite_domain(rule const& r) const; bool is_finite_domain(rule const& r) const;