mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix bug in double collection of declarations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-11 14:09:34 -08:00
parent 6d729f1f15
commit 35a3523fd6
3 changed files with 14 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/ast.h
View file

@ -622,6 +622,9 @@ public:
sort * const * get_domain() const { return m_domain; } sort * const * get_domain() const { return m_domain; }
sort * get_range() const { return m_range; } sort * get_range() const { return m_range; }
unsigned get_size() const { return get_obj_size(m_arity); } unsigned get_size() const { return get_obj_size(m_arity); }
sort * const * begin() const { return get_domain(); }
sort * const * end() const { return get_domain() + get_arity(); }
}; };
// ----------------------------------- // -----------------------------------

25
src/ast/decl_collector.cpp
View file

@ -20,20 +20,15 @@ Revision History:
#include "ast/decl_collector.h" #include "ast/decl_collector.h"
void decl_collector::visit_sort(sort * n) { void decl_collector::visit_sort(sort * n) {
SASSERT(!m_visited.is_marked(n));
family_id fid = n->get_family_id(); family_id fid = n->get_family_id();
if (m().is_uninterp(n)) if (m().is_uninterp(n))
m_sorts.push_back(n); m_sorts.push_back(n);
if (fid == m_dt_fid) { else if (fid == m_dt_fid) {
m_sorts.push_back(n); m_sorts.push_back(n);
for (func_decl* cnstr : *m_dt_util.get_datatype_constructors(n)) {
unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
for (unsigned i = 0; i < num_cnstr; i++) {
func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i);
m_decls.push_back(cnstr); m_decls.push_back(cnstr);
ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr); for (func_decl * accsr : *m_dt_util.get_constructor_accessors(cnstr)) {
unsigned num_cas = cnstr_acc.size();
for (unsigned j = 0; j < num_cas; j++) {
func_decl * accsr = cnstr_acc.get(j);
m_decls.push_back(accsr); m_decls.push_back(accsr);
} }
} }
@ -53,6 +48,7 @@ void decl_collector::visit_func(func_decl * n) {
else else
m_decls.push_back(n); m_decls.push_back(n);
} }
m_visited.mark(n, true);
} }
} }
@ -72,11 +68,10 @@ void decl_collector::visit(ast* n) {
if (!m_visited.is_marked(n)) { if (!m_visited.is_marked(n)) {
switch(n->get_kind()) { switch(n->get_kind()) {
case AST_APP: { case AST_APP: {
app * a = to_app(n); for (expr * e : *to_app(n)) {
for (unsigned i = 0; i < a->get_num_args(); ++i) { m_todo.push_back(e);
m_todo.push_back(a->get_arg(i));
} }
m_todo.push_back(a->get_decl()); m_todo.push_back(to_app(n)->get_decl());
break; break;
} }
case AST_QUANTIFIER: { case AST_QUANTIFIER: {
@ -96,8 +91,8 @@ void decl_collector::visit(ast* n) {
break; break;
case AST_FUNC_DECL: { case AST_FUNC_DECL: {
func_decl * d = to_func_decl(n); func_decl * d = to_func_decl(n);
for (unsigned i = 0; i < d->get_arity(); ++i) { for (sort* srt : *d) {
m_todo.push_back(d->get_domain(i)); m_todo.push_back(srt);
} }
m_todo.push_back(d->get_range()); m_todo.push_back(d->get_range());
visit_func(d); visit_func(d);

2
src/ast/decl_collector.h
View file

@ -41,7 +41,7 @@ class decl_collector {
public: public:
// if preds == true, then predicates are stored in a separate collection. // if preds == true, then predicates are stored in a separate collection.
decl_collector(ast_manager & m, bool preds=true); decl_collector(ast_manager & m, bool preds = true);
ast_manager & m() { return m_manager; } ast_manager & m() { return m_manager; }
void visit_func(func_decl* n); void visit_func(func_decl* n);