1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2017 SRI International. 4 * 5 * Yices is free software: you can redistribute it and/or modify 6 * it under the terms of the GNU General Public License as published by 7 * the Free Software Foundation, either version 3 of the License, or 8 * (at your option) any later version. 9 * 10 * Yices is distributed in the hope that it will be useful, 11 * but WITHOUT ANY WARRANTY; without even the implied warranty of 12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 * GNU General Public License for more details. 14 * 15 * You should have received a copy of the GNU General Public License 16 * along with Yices. If not, see <http://www.gnu.org/licenses/>. 17 */ 18 19 /* 20 * GLOBAL VARIABLES 21 */ 22 23 /* 24 * Several global tables and data structures are maintained by 25 * yices_api.c. If other modules need to access these internal 26 * data structures, they can use the following table of pointers. 27 * 28 * The table is initialized after a call to yices_init(); 29 */ 30 31 #ifndef __YICES_GLOBALS_H 32 #define __YICES_GLOBALS_H 33 34 #include "mt/yices_locks.h" 35 #include "frontend/yices/yices_parser.h" 36 #include "parser_utils/term_stack2.h" 37 #include "terms/free_var_collector.h" 38 #include "terms/term_manager.h" 39 40 typedef struct yices_globals_s { 41 #ifdef THREAD_SAFE 42 yices_lock_t lock; // a lock protecting the globals 43 #endif 44 type_table_t *types; // type table 45 term_table_t *terms; // term table 46 term_manager_t *manager; // full term manager (includes terms) 47 pprod_table_t *pprods; // pprod table 48 49 // parser, lexer, term stack: all are allocated on demand 50 parser_t *parser; // parser (or NULL) 51 lexer_t *lexer; // lexer (or NULL) 52 tstack_t *tstack; // term stack (or NULL) 53 54 fvar_collector_t *fvars; // to collect free variables of terms 55 56 } yices_globals_t; 57 58 extern yices_globals_t __yices_globals; 59 60 #endif /* __YICES_GLOBALS_H */ 61