mirror of
https://github.com/Z3Prover/z3
synced 2025-06-03 12:51:22 +00:00
Updated declarations in decl_collector
This commit is contained in:
parent
ef3d340c85
commit
0fb3161113
1 changed files with 5 additions and 3 deletions
|
@ -21,6 +21,7 @@ Revision History:
|
||||||
#define SMT_DECL_COLLECTOR_H_
|
#define SMT_DECL_COLLECTOR_H_
|
||||||
|
|
||||||
#include"ast.h"
|
#include"ast.h"
|
||||||
|
#include"datatype_decl_plugin.h"
|
||||||
|
|
||||||
class decl_collector {
|
class decl_collector {
|
||||||
ast_manager & m_manager;
|
ast_manager & m_manager;
|
||||||
|
@ -28,9 +29,10 @@ class decl_collector {
|
||||||
ptr_vector<sort> m_sorts;
|
ptr_vector<sort> m_sorts;
|
||||||
ptr_vector<func_decl> m_decls;
|
ptr_vector<func_decl> m_decls;
|
||||||
ptr_vector<func_decl> m_preds;
|
ptr_vector<func_decl> m_preds;
|
||||||
ast_mark m_visited;
|
ast_mark m_visited;
|
||||||
family_id m_basic_fid;
|
family_id m_basic_fid;
|
||||||
family_id m_dt_fid;
|
family_id m_dt_fid;
|
||||||
|
datatype_util m_dt_util;
|
||||||
|
|
||||||
void visit_sort(sort* n);
|
void visit_sort(sort* n);
|
||||||
bool is_bool(sort* s);
|
bool is_bool(sort* s);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue