1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6     api_ast_vector.cpp
7 
8 Abstract:
9     API for creating AST vectors
10 
11 Author:
12 
13     Leonardo de Moura (leonardo) 2012-03-09.
14 
15 Revision History:
16 
17 --*/
18 #include<iostream>
19 #include "api/z3.h"
20 #include "api/api_log_macros.h"
21 #include "api/api_context.h"
22 #include "api/api_ast_vector.h"
23 #include "ast/ast_translation.h"
24 #include "ast/ast_smt2_pp.h"
25 
26 extern "C" {
27 
28     Z3_ast_vector Z3_API Z3_mk_ast_vector(Z3_context c) {
29         Z3_TRY;
30         LOG_Z3_mk_ast_vector(c);
31         RESET_ERROR_CODE();
32         Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
33         mk_c(c)->save_object(v);
34         Z3_ast_vector r       = of_ast_vector(v);
35         RETURN_Z3(r);
36         Z3_CATCH_RETURN(nullptr);
37     }
38 
39     void Z3_API Z3_ast_vector_inc_ref(Z3_context c, Z3_ast_vector v) {
40         Z3_TRY;
41         LOG_Z3_ast_vector_inc_ref(c, v);
42         RESET_ERROR_CODE();
43         to_ast_vector(v)->inc_ref();
44         Z3_CATCH;
45     }
46 
47     void Z3_API Z3_ast_vector_dec_ref(Z3_context c, Z3_ast_vector v) {
48         Z3_TRY;
49         LOG_Z3_ast_vector_dec_ref(c, v);
50         RESET_ERROR_CODE();
51         to_ast_vector(v)->dec_ref();
52         Z3_CATCH;
53     }
54 
55     unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v) {
56         Z3_TRY;
57         LOG_Z3_ast_vector_size(c, v);
58         RESET_ERROR_CODE();
59         return to_ast_vector_ref(v).size();
60         Z3_CATCH_RETURN(0);
61     }
62 
63     Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i) {
64         Z3_TRY;
65         LOG_Z3_ast_vector_get(c, v, i);
66         RESET_ERROR_CODE();
67         if (i >= to_ast_vector_ref(v).size()) {
68             SET_ERROR_CODE(Z3_IOB, nullptr);
69             RETURN_Z3(nullptr);
70         }
71         // Remark: Don't need to invoke save_object.
72         ast * r = to_ast_vector_ref(v).get(i);
73         RETURN_Z3(of_ast(r));
74         Z3_CATCH_RETURN(nullptr);
75     }
76 
77     void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a) {
78         Z3_TRY;
79         LOG_Z3_ast_vector_set(c, v, i, a);
80         RESET_ERROR_CODE();
81         if (i >= to_ast_vector_ref(v).size()) {
82             SET_ERROR_CODE(Z3_IOB, nullptr);
83             return;
84         }
85         to_ast_vector_ref(v).set(i, to_ast(a));
86         Z3_CATCH;
87     }
88 
89     void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n) {
90         Z3_TRY;
91         LOG_Z3_ast_vector_resize(c, v, n);
92         RESET_ERROR_CODE();
93         to_ast_vector_ref(v).resize(n);
94         Z3_CATCH;
95     }
96 
97     void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a) {
98         Z3_TRY;
99         LOG_Z3_ast_vector_push(c, v, a);
100         RESET_ERROR_CODE();
101         to_ast_vector_ref(v).push_back(to_ast(a));
102         Z3_CATCH;
103     }
104 
105     Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context c, Z3_ast_vector v, Z3_context t) {
106         Z3_TRY;
107         LOG_Z3_ast_vector_translate(c, v, t);
108         RESET_ERROR_CODE();
109         if (c == t) {
110             RETURN_Z3(v);
111         }
112         ast_translation translator(mk_c(c)->m(), mk_c(t)->m());
113         Z3_ast_vector_ref * new_v = alloc(Z3_ast_vector_ref, *mk_c(t), mk_c(t)->m());
114         mk_c(t)->save_object(new_v);
115         unsigned sz = to_ast_vector_ref(v).size();
116         for (unsigned i = 0; i < sz; i++) {
117             ast * new_ast = translator(to_ast_vector_ref(v).get(i));
118             new_v->m_ast_vector.push_back(new_ast);
119         }
120         RETURN_Z3(of_ast_vector(new_v));
121         Z3_CATCH_RETURN(nullptr);
122     }
123 
124     Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v) {
125         Z3_TRY;
126         LOG_Z3_ast_vector_to_string(c, v);
127         RESET_ERROR_CODE();
128         std::ostringstream buffer;
129         buffer << "(ast-vector";
130         unsigned sz = to_ast_vector_ref(v).size();
131         for (unsigned i = 0; i < sz; i++) {
132             buffer << "\n  " << mk_ismt2_pp(to_ast_vector_ref(v).get(i), mk_c(c)->m(), 2);
133         }
134         buffer << ")";
135         return mk_c(c)->mk_external_string(buffer.str());
136         Z3_CATCH_RETURN(nullptr);
137     }
138 
139 };
140