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 
Z3_mk_ast_vector(Z3_context c)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 
Z3_ast_vector_inc_ref(Z3_context c,Z3_ast_vector v)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 
Z3_ast_vector_dec_ref(Z3_context c,Z3_ast_vector v)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         if (v)
52             to_ast_vector(v)->dec_ref();
53         Z3_CATCH;
54     }
55 
Z3_ast_vector_size(Z3_context c,Z3_ast_vector v)56     unsigned Z3_API Z3_ast_vector_size(Z3_context c, Z3_ast_vector v) {
57         Z3_TRY;
58         LOG_Z3_ast_vector_size(c, v);
59         RESET_ERROR_CODE();
60         return to_ast_vector_ref(v).size();
61         Z3_CATCH_RETURN(0);
62     }
63 
Z3_ast_vector_get(Z3_context c,Z3_ast_vector v,unsigned i)64     Z3_ast Z3_API Z3_ast_vector_get(Z3_context c, Z3_ast_vector v, unsigned i) {
65         Z3_TRY;
66         LOG_Z3_ast_vector_get(c, v, i);
67         RESET_ERROR_CODE();
68         if (i >= to_ast_vector_ref(v).size()) {
69             SET_ERROR_CODE(Z3_IOB, nullptr);
70             RETURN_Z3(nullptr);
71         }
72         // Remark: Don't need to invoke save_object.
73         ast * r = to_ast_vector_ref(v).get(i);
74         RETURN_Z3(of_ast(r));
75         Z3_CATCH_RETURN(nullptr);
76     }
77 
Z3_ast_vector_set(Z3_context c,Z3_ast_vector v,unsigned i,Z3_ast a)78     void Z3_API Z3_ast_vector_set(Z3_context c, Z3_ast_vector v, unsigned i, Z3_ast a) {
79         Z3_TRY;
80         LOG_Z3_ast_vector_set(c, v, i, a);
81         RESET_ERROR_CODE();
82         if (i >= to_ast_vector_ref(v).size()) {
83             SET_ERROR_CODE(Z3_IOB, nullptr);
84             return;
85         }
86         to_ast_vector_ref(v).set(i, to_ast(a));
87         Z3_CATCH;
88     }
89 
Z3_ast_vector_resize(Z3_context c,Z3_ast_vector v,unsigned n)90     void Z3_API Z3_ast_vector_resize(Z3_context c, Z3_ast_vector v, unsigned n) {
91         Z3_TRY;
92         LOG_Z3_ast_vector_resize(c, v, n);
93         RESET_ERROR_CODE();
94         to_ast_vector_ref(v).resize(n);
95         Z3_CATCH;
96     }
97 
Z3_ast_vector_push(Z3_context c,Z3_ast_vector v,Z3_ast a)98     void Z3_API Z3_ast_vector_push(Z3_context c, Z3_ast_vector v, Z3_ast a) {
99         Z3_TRY;
100         LOG_Z3_ast_vector_push(c, v, a);
101         RESET_ERROR_CODE();
102         to_ast_vector_ref(v).push_back(to_ast(a));
103         Z3_CATCH;
104     }
105 
Z3_ast_vector_translate(Z3_context c,Z3_ast_vector v,Z3_context t)106     Z3_ast_vector Z3_API Z3_ast_vector_translate(Z3_context c, Z3_ast_vector v, Z3_context t) {
107         Z3_TRY;
108         LOG_Z3_ast_vector_translate(c, v, t);
109         RESET_ERROR_CODE();
110         if (c == t) {
111             RETURN_Z3(v);
112         }
113         ast_translation translator(mk_c(c)->m(), mk_c(t)->m());
114         Z3_ast_vector_ref * new_v = alloc(Z3_ast_vector_ref, *mk_c(t), mk_c(t)->m());
115         mk_c(t)->save_object(new_v);
116         unsigned sz = to_ast_vector_ref(v).size();
117         for (unsigned i = 0; i < sz; i++) {
118             ast * new_ast = translator(to_ast_vector_ref(v).get(i));
119             new_v->m_ast_vector.push_back(new_ast);
120         }
121         RETURN_Z3(of_ast_vector(new_v));
122         Z3_CATCH_RETURN(nullptr);
123     }
124 
Z3_ast_vector_to_string(Z3_context c,Z3_ast_vector v)125     Z3_string Z3_API Z3_ast_vector_to_string(Z3_context c, Z3_ast_vector v) {
126         Z3_TRY;
127         LOG_Z3_ast_vector_to_string(c, v);
128         RESET_ERROR_CODE();
129         std::ostringstream buffer;
130         buffer << "(ast-vector";
131         unsigned sz = to_ast_vector_ref(v).size();
132         for (unsigned i = 0; i < sz; i++) {
133             buffer << "\n  " << mk_ismt2_pp(to_ast_vector_ref(v).get(i), mk_c(c)->m(), 2);
134         }
135         buffer << ")";
136         return mk_c(c)->mk_external_string(buffer.str());
137         Z3_CATCH_RETURN(nullptr);
138     }
139 
140 };
141