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