diff options
author | Kenji Hosokawa <khosokawa@jp.adit-jv.com> | 2021-09-27 17:23:10 +0900 |
---|---|---|
committer | Kenji Hosokawa <khosokawa@jp.adit-jv.com> | 2021-09-27 17:23:10 +0900 |
commit | 05417f782cb2377a4105969f910d2ed0416a8c47 (patch) | |
tree | 245300cbb1d501035de708ab93f174e7093c2f4c /tool_bin/lib/linux/z3/include/z3_v1.h | |
parent | 44a3da18a257cc46aa0dbfd01947deeb377ab049 (diff) |
push pre-built toolneedlefish_13.93.0needlefish/13.93.0marlin_12.93.0marlin_12.92.0marlin_12.91.0marlin_12.90.1marlin/12.93.0marlin/12.92.0marlin/12.91.0marlin/12.90.1lamprey_12.1.6lamprey_12.1.5lamprey_12.1.4lamprey_12.1.3lamprey_12.1.2lamprey_12.1.1lamprey_12.1.0lamprey/12.1.6lamprey/12.1.5lamprey/12.1.4lamprey/12.1.3lamprey/12.1.2lamprey/12.1.1lamprey/12.1.0koi_11.0.5koi/11.0.513.93.012.93.012.92.012.91.012.90.112.1.612.1.512.1.412.1.312.1.212.1.112.1.011.0.5
Signed-off-by: Kenji Hosokawa <khosokawa@jp.adit-jv.com>
Diffstat (limited to 'tool_bin/lib/linux/z3/include/z3_v1.h')
-rw-r--r-- | tool_bin/lib/linux/z3/include/z3_v1.h | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/tool_bin/lib/linux/z3/include/z3_v1.h b/tool_bin/lib/linux/z3/include/z3_v1.h new file mode 100644 index 0000000..66de943 --- /dev/null +++ b/tool_bin/lib/linux/z3/include/z3_v1.h @@ -0,0 +1,64 @@ +/*++ +Copyright (c) 2011 Microsoft Corporation + +Module Name: + + z3_v1.h + +Abstract: + + Z3 1.x backwards compatibility macros. + These macros are used to simulate the Z3 API using in the 1.x versions. + This file should only be used by users still using the Z3 1.x API. + +Author: + + Leonardo de Moura (leonardo) 2011-09-22 + +Notes: + +--*/ +#ifndef Z3_V1_H_ +#define Z3_V1_H_ + +#include "api/z3.h" + +// Backwards compatibility +#define Z3_type_ast Z3_sort +#define Z3_const_decl_ast Z3_func_decl +#define Z3_const Z3_app +#define Z3_pattern_ast Z3_pattern +#define Z3_UNINTERPRETED_TYPE Z3_UNINTERPRETED_SORT +#define Z3_BOOL_TYPE Z3_BOOL_SORT +#define Z3_INT_TYPE Z3_INT_SORT +#define Z3_REAL_TYPE Z3_REAL_SORT +#define Z3_BV_TYPE Z3_BV_SORT +#define Z3_ARRAY_TYPE Z3_ARRAY_SORT +#define Z3_TUPLE_TYPE Z3_DATATYPE_SORT +#define Z3_UNKNOWN_TYPE Z3_UNKNOWN_SORT +#define Z3_CONST_DECL_AST Z3_FUNC_DECL_AST +#define Z3_TYPE_AST Z3_SORT_AST +#define Z3_SORT_ERROR Z3_TYPE_ERROR +#define Z3_mk_uninterpreted_type Z3_mk_uninterpreted_sort +#define Z3_mk_bool_type Z3_mk_bool_sort +#define Z3_mk_int_type Z3_mk_int_sort +#define Z3_mk_real_type Z3_mk_real_sort +#define Z3_mk_bv_type Z3_mk_bv_sort +#define Z3_mk_array_type Z3_mk_array_sort +#define Z3_mk_tuple_type Z3_mk_tuple_sort +#define Z3_get_type Z3_get_sort +#define Z3_get_pattern_ast Z3_get_pattern +#define Z3_get_type_kind Z3_get_sort_kind +#define Z3_get_type_name Z3_get_sort_name +#define Z3_get_bv_type_size Z3_get_bv_sort_size +#define Z3_get_array_type_domain Z3_get_array_sort_domain +#define Z3_get_array_type_range Z3_get_array_sort_range +#define Z3_get_tuple_type_num_fields Z3_get_tuple_sort_num_fields +#define Z3_get_tuple_type_field_decl Z3_get_tuple_sort_field_decl +#define Z3_get_tuple_type_mk_decl Z3_get_tuple_sort_mk_decl +#define Z3_to_const_ast Z3_to_app +#define Z3_get_numeral_value_string Z3_get_numeral_string +#define Z3_get_const_ast_decl Z3_get_app_decl +#define Z3_get_value Z3_eval_func_decl + +#endif |