1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 z3_v1.h 7 8 Abstract: 9 10 Z3 1.x backwards compatibility macros. 11 These macros are used to simulate the Z3 API using in the 1.x versions. 12 This file should only be used by users still using the Z3 1.x API. 13 14 Author: 15 16 Leonardo de Moura (leonardo) 2011-09-22 17 18 Notes: 19 20 --*/ 21 #pragma once 22 23 #include "api/z3.h" 24 25 // Backwards compatibility 26 #define Z3_type_ast Z3_sort 27 #define Z3_const_decl_ast Z3_func_decl 28 #define Z3_const Z3_app 29 #define Z3_pattern_ast Z3_pattern 30 #define Z3_UNINTERPRETED_TYPE Z3_UNINTERPRETED_SORT 31 #define Z3_BOOL_TYPE Z3_BOOL_SORT 32 #define Z3_INT_TYPE Z3_INT_SORT 33 #define Z3_REAL_TYPE Z3_REAL_SORT 34 #define Z3_BV_TYPE Z3_BV_SORT 35 #define Z3_ARRAY_TYPE Z3_ARRAY_SORT 36 #define Z3_TUPLE_TYPE Z3_DATATYPE_SORT 37 #define Z3_UNKNOWN_TYPE Z3_UNKNOWN_SORT 38 #define Z3_CONST_DECL_AST Z3_FUNC_DECL_AST 39 #define Z3_TYPE_AST Z3_SORT_AST 40 #define Z3_SORT_ERROR Z3_TYPE_ERROR 41 #define Z3_mk_uninterpreted_type Z3_mk_uninterpreted_sort 42 #define Z3_mk_bool_type Z3_mk_bool_sort 43 #define Z3_mk_int_type Z3_mk_int_sort 44 #define Z3_mk_real_type Z3_mk_real_sort 45 #define Z3_mk_bv_type Z3_mk_bv_sort 46 #define Z3_mk_array_type Z3_mk_array_sort 47 #define Z3_mk_tuple_type Z3_mk_tuple_sort 48 #define Z3_get_type Z3_get_sort 49 #define Z3_get_pattern_ast Z3_get_pattern 50 #define Z3_get_type_kind Z3_get_sort_kind 51 #define Z3_get_type_name Z3_get_sort_name 52 #define Z3_get_bv_type_size Z3_get_bv_sort_size 53 #define Z3_get_array_type_domain Z3_get_array_sort_domain 54 #define Z3_get_array_type_range Z3_get_array_sort_range 55 #define Z3_get_tuple_type_num_fields Z3_get_tuple_sort_num_fields 56 #define Z3_get_tuple_type_field_decl Z3_get_tuple_sort_field_decl 57 #define Z3_get_tuple_type_mk_decl Z3_get_tuple_sort_mk_decl 58 #define Z3_to_const_ast Z3_to_app 59 #define Z3_get_numeral_value_string Z3_get_numeral_string 60 #define Z3_get_const_ast_decl Z3_get_app_decl 61 #define Z3_get_value Z3_eval_func_decl 62 63