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