mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

test for undetermined accessor for PDR

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-09-20 12:32:16 -07:00
parent 37ad1f9807
commit 0a964c324e
3 changed files with 18 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -576,7 +576,7 @@ namespace datalog {
void context::check_uninterpreted_free(rule_ref& r) {
func_decl* f = 0;
if (r->has_uninterpreted_non_predicates(f)) {
if (r->has_uninterpreted_non_predicates(m, f)) {
std::stringstream stm;
stm << "Uninterpreted '"
<< f->get_name()

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

@ -43,6 +43,7 @@ Revision History:
#include"expr_safe_replace.h"
#include"filter_model_converter.h"
#include"scoped_proof.h"
#include"datatype_decl_plugin.h"
namespace datalog {
@ -881,9 +882,12 @@ namespace datalog {
}
struct uninterpreted_function_finder_proc {
ast_manager& m;
datatype_util m_dt;
bool m_found;
func_decl* m_func;
uninterpreted_function_finder_proc() : m_found(false), m_func(0) {}
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) {
@ -891,6 +895,14 @@ namespace datalog {
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; }
@ -900,9 +912,9 @@ namespace datalog {
// non-predicates may appear only in the interpreted tail, it is therefore
// sufficient only to check the tail.
//
bool rule::has_uninterpreted_non_predicates(func_decl*& f) const {
bool rule::has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const {
unsigned sz = get_tail_size();
uninterpreted_function_finder_proc proc;
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));
@ -910,6 +922,7 @@ namespace datalog {
return proc.found(f);
}
struct quantifier_finder_proc {
bool m_exist;
bool m_univ;

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

@ -293,7 +293,7 @@ namespace datalog {
*/
bool is_in_tail(const func_decl * p, bool only_positive=false) const;
bool has_uninterpreted_non_predicates(func_decl*& f) 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;