mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

more #5164

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-09 13:11:53 -07:00
parent 070eba0fe8
commit 673d2d700e
2 changed files with 34 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

54
src/cmd_context/cmd_context.cpp
View file

@ -52,10 +52,9 @@ Notes:
#include "cmd_context/basic_cmds.h" #include "cmd_context/basic_cmds.h"
#include "cmd_context/cmd_context.h" #include "cmd_context/cmd_context.h"
func_decls::func_decls(ast_manager & _m, func_decl * f): func_decls::func_decls(ast_manager & m, func_decl * f):
m(&_m),
m_decls(TAG(func_decl*, f, 0)) { m_decls(TAG(func_decl*, f, 0)) {
_m.inc_ref(f); m.inc_ref(f);
} }
void func_decls::finalize(ast_manager & m) { void func_decls::finalize(ast_manager & m) {
@ -80,11 +79,13 @@ bool func_decls::signatures_collide(func_decl* f, func_decl* g) const {
} }
bool func_decls::signatures_collide(unsigned n, sort* const* domain, sort* range, func_decl* g) const { bool func_decls::signatures_collide(unsigned n, sort* const* domain, sort* range, func_decl* g) const {
if (g->get_range() != range) return false; if (g->get_range() != range)
if (n != g->get_arity()) return false; return false;
for (unsigned i = 0; i < n; ++i) { if (n != g->get_arity())
if (domain[i] != g->get_domain(i)) return false; return false;
} for (unsigned i = 0; i < n; ++i)
if (domain[i] != g->get_domain(i))
return false;
return true; return true;
} }
@ -197,42 +198,49 @@ func_decl * func_decls::first() const {
return *(fs->begin()); return *(fs->begin());
} }
bool func_decls::check_signature(func_decl* f, unsigned arity, sort * const* domain, sort* range) const { bool func_decls::check_signature(ast_manager& m, func_decl* f, unsigned arity, sort * const* domain, sort* range, bool& coerced) const {
if (range != nullptr && f->get_range() != range) if (range != nullptr && f->get_range() != range)
return false; return false;
if (f->get_arity() != arity) if (f->get_arity() != arity)
return false; return false;
unsigned i = 0; if (!domain)
for (i = 0; domain && i < arity; i++) { return true;
coerced = false;
for (unsigned i = 0; i < arity; i++) {
sort* s1 = f->get_domain(i); sort* s1 = f->get_domain(i);
sort* s2 = domain[i]; sort* s2 = domain[i];
if (s1 != s2) if (s1 == s2)
continue; continue;
if (!m) coerced = true;
return false; arith_util au(m);
arith_util au(*m);
if (au.is_real(s1) && au.is_int(s2)) if (au.is_real(s1) && au.is_int(s2))
continue; continue;
if (au.is_real(s2) && au.is_int(s1)) if (au.is_real(s2) && au.is_int(s1))
continue; continue;
return false; return false;
} }
return i == arity || !domain; return true;
} }
func_decl * func_decls::find(unsigned arity, sort * const * domain, sort * range) const { func_decl * func_decls::find(ast_manager& m, unsigned arity, sort * const * domain, sort * range) const {
bool coerced = false;
if (!more_than_one()) { if (!more_than_one()) {
func_decl* f = first(); func_decl* f = first();
if (check_signature(f, arity, domain, range)) if (check_signature(m, f, arity, domain, range, coerced))
return f; return f;
return nullptr; return nullptr;
} }
func_decl_set * fs = UNTAG(func_decl_set *, m_decls); func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
func_decl* best_f = nullptr;
for (func_decl * f : *fs) { for (func_decl * f : *fs) {
if (check_signature(f, arity, domain, range)) if (check_signature(m, f, arity, domain, range, coerced)) {
return f; if (coerced)
best_f = f;
else
return f;
}
} }
return nullptr; return best_f;
} }
func_decl * func_decls::find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const { func_decl * func_decls::find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const {
@ -241,7 +249,7 @@ func_decl * func_decls::find(ast_manager & m, unsigned num_args, expr * const *
ptr_buffer<sort> sorts; ptr_buffer<sort> sorts;
for (unsigned i = 0; i < num_args; i++) for (unsigned i = 0; i < num_args; i++)
sorts.push_back(args[i]->get_sort()); sorts.push_back(args[i]->get_sort());
return find(num_args, sorts.c_ptr(), range); return find(m, num_args, sorts.c_ptr(), range);
} }
unsigned func_decls::get_num_entries() const { unsigned func_decls::get_num_entries() const {
@ -1028,7 +1036,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices,
func_decl * f = nullptr; func_decl * f = nullptr;
func_decls fs; func_decls fs;
if (num_indices == 0 && m_func_decls.find(s, fs)) if (num_indices == 0 && m_func_decls.find(s, fs))
f = fs.find(arity, domain, range); f = fs.find(m(), arity, domain, range);
if (f) if (f)
return f; return f;
builtin_decl d; builtin_decl d;

7
src/cmd_context/cmd_context.h
View file

@ -43,7 +43,6 @@ Notes:
class func_decls { class func_decls {
ast_manager* m { nullptr };
func_decl * m_decls { nullptr }; func_decl * m_decls { nullptr };
bool signatures_collide(func_decl* f, func_decl* g) const; bool signatures_collide(func_decl* f, func_decl* g) const;
bool signatures_collide(unsigned n, sort*const* domain, sort* range, func_decl* g) const; bool signatures_collide(unsigned n, sort*const* domain, sort* range, func_decl* g) const;
@ -59,11 +58,11 @@ public:
bool clash(func_decl * f) const; bool clash(func_decl * f) const;
bool empty() const { return m_decls == nullptr; } bool empty() const { return m_decls == nullptr; }
func_decl * first() const; func_decl * first() const;
func_decl * find(unsigned arity, sort * const * domain, sort * range) const; func_decl * find(ast_manager & m, unsigned arity, sort * const * domain, sort * range) const;
func_decl * find(ast_manager & m, unsigned num_args, expr * const * args, sort * range) const; func_decl * find(ast_manager & m, unsigned arity, expr * const * args, sort * range) const;
unsigned get_num_entries() const; unsigned get_num_entries() const;
func_decl * get_entry(unsigned inx); func_decl * get_entry(unsigned inx);
bool check_signature(func_decl* f, unsigned arityh, sort * const* domain, sort * range) const; bool check_signature(ast_manager& m, func_decl* f, unsigned arityh, sort * const* domain, sort * range, bool& coerced) const;
}; };
struct macro_decl { struct macro_decl {