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