1 /*++ 2 Copyright (c) 2012 Microsoft Corporation 3 4 Module Name: 5 6 api_goal.cpp 7 8 Abstract: 9 API for creating goals 10 11 Author: 12 13 Leonardo de Moura (leonardo) 2012-03-06. 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_goal.h" 23 #include "ast/ast_translation.h" 24 #include "api/api_model.h" 25 26 extern "C" { 27 Z3_mk_goal(Z3_context c,bool models,bool unsat_cores,bool proofs)28 Z3_goal Z3_API Z3_mk_goal(Z3_context c, bool models, bool unsat_cores, bool proofs) { 29 Z3_TRY; 30 LOG_Z3_mk_goal(c, models, unsat_cores, proofs); 31 RESET_ERROR_CODE(); 32 if (proofs != 0 && !mk_c(c)->m().proofs_enabled()) { 33 SET_ERROR_CODE(Z3_INVALID_ARG, "proofs are required, but proofs are not enabled on the context"); 34 RETURN_Z3(nullptr); 35 } 36 Z3_goal_ref * g = alloc(Z3_goal_ref, *mk_c(c)); 37 g->m_goal = alloc(goal, mk_c(c)->m(), proofs != 0, models != 0, unsat_cores != 0); 38 mk_c(c)->save_object(g); 39 Z3_goal r = of_goal(g); 40 RETURN_Z3(r); 41 Z3_CATCH_RETURN(nullptr); 42 } 43 Z3_goal_inc_ref(Z3_context c,Z3_goal g)44 void Z3_API Z3_goal_inc_ref(Z3_context c, Z3_goal g) { 45 Z3_TRY; 46 LOG_Z3_goal_inc_ref(c, g); 47 RESET_ERROR_CODE(); 48 to_goal(g)->inc_ref(); 49 Z3_CATCH; 50 } 51 Z3_goal_dec_ref(Z3_context c,Z3_goal g)52 void Z3_API Z3_goal_dec_ref(Z3_context c, Z3_goal g) { 53 Z3_TRY; 54 LOG_Z3_goal_dec_ref(c, g); 55 RESET_ERROR_CODE(); 56 to_goal(g)->dec_ref(); 57 Z3_CATCH; 58 } 59 Z3_goal_precision(Z3_context c,Z3_goal g)60 Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g) { 61 Z3_TRY; 62 LOG_Z3_goal_precision(c, g); 63 RESET_ERROR_CODE(); 64 switch (to_goal_ref(g)->prec()) { 65 case goal::PRECISE: return Z3_GOAL_PRECISE; 66 case goal::UNDER: return Z3_GOAL_UNDER; 67 case goal::OVER: return Z3_GOAL_OVER; 68 case goal::UNDER_OVER: return Z3_GOAL_UNDER_OVER; 69 default: 70 UNREACHABLE(); 71 return Z3_GOAL_UNDER_OVER; 72 } 73 Z3_CATCH_RETURN(Z3_GOAL_UNDER_OVER); 74 } 75 Z3_goal_assert(Z3_context c,Z3_goal g,Z3_ast a)76 void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a) { 77 Z3_TRY; 78 LOG_Z3_goal_assert(c, g, a); 79 RESET_ERROR_CODE(); 80 CHECK_FORMULA(a,); 81 to_goal_ref(g)->assert_expr(to_expr(a)); 82 Z3_CATCH; 83 } 84 Z3_goal_inconsistent(Z3_context c,Z3_goal g)85 bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g) { 86 Z3_TRY; 87 LOG_Z3_goal_inconsistent(c, g); 88 RESET_ERROR_CODE(); 89 return to_goal_ref(g)->inconsistent(); 90 Z3_CATCH_RETURN(false); 91 } 92 Z3_goal_depth(Z3_context c,Z3_goal g)93 unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g) { 94 Z3_TRY; 95 LOG_Z3_goal_depth(c, g); 96 RESET_ERROR_CODE(); 97 return to_goal_ref(g)->depth(); 98 Z3_CATCH_RETURN(0); 99 } 100 Z3_goal_reset(Z3_context c,Z3_goal g)101 void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g) { 102 Z3_TRY; 103 LOG_Z3_goal_reset(c, g); 104 RESET_ERROR_CODE(); 105 to_goal_ref(g)->reset(); 106 Z3_CATCH; 107 } 108 Z3_goal_size(Z3_context c,Z3_goal g)109 unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g) { 110 Z3_TRY; 111 LOG_Z3_goal_size(c, g); 112 RESET_ERROR_CODE(); 113 return to_goal_ref(g)->size(); 114 Z3_CATCH_RETURN(0); 115 } 116 Z3_goal_formula(Z3_context c,Z3_goal g,unsigned idx)117 Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx) { 118 Z3_TRY; 119 LOG_Z3_goal_formula(c, g, idx); 120 RESET_ERROR_CODE(); 121 if (idx >= to_goal_ref(g)->size()) { 122 SET_ERROR_CODE(Z3_IOB, nullptr); 123 RETURN_Z3(nullptr); 124 } 125 expr * result = to_goal_ref(g)->form(idx); 126 mk_c(c)->save_ast_trail(result); 127 RETURN_Z3(of_ast(result)); 128 Z3_CATCH_RETURN(nullptr); 129 } 130 Z3_goal_num_exprs(Z3_context c,Z3_goal g)131 unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g) { 132 Z3_TRY; 133 LOG_Z3_goal_num_exprs(c, g); 134 RESET_ERROR_CODE(); 135 return to_goal_ref(g)->num_exprs(); 136 Z3_CATCH_RETURN(0); 137 } 138 Z3_goal_is_decided_sat(Z3_context c,Z3_goal g)139 bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g) { 140 Z3_TRY; 141 LOG_Z3_goal_is_decided_sat(c, g); 142 RESET_ERROR_CODE(); 143 return to_goal_ref(g)->is_decided_sat(); 144 Z3_CATCH_RETURN(false); 145 } 146 Z3_goal_is_decided_unsat(Z3_context c,Z3_goal g)147 bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g) { 148 Z3_TRY; 149 LOG_Z3_goal_is_decided_unsat(c, g); 150 RESET_ERROR_CODE(); 151 return to_goal_ref(g)->is_decided_unsat(); 152 Z3_CATCH_RETURN(false); 153 } 154 Z3_goal_convert_model(Z3_context c,Z3_goal g,Z3_model m)155 Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m) { 156 Z3_TRY; 157 LOG_Z3_goal_convert_model(c, g, m); 158 RESET_ERROR_CODE(); 159 model_ref new_m; 160 Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 161 mk_c(c)->save_object(m_ref); 162 if (m) m_ref->m_model = to_model_ref(m)->copy(); 163 if (to_goal_ref(g)->mc()) 164 (*to_goal_ref(g)->mc())(m_ref->m_model); 165 RETURN_Z3(of_model(m_ref)); 166 Z3_CATCH_RETURN(nullptr); 167 } 168 Z3_goal_translate(Z3_context c,Z3_goal g,Z3_context target)169 Z3_goal Z3_API Z3_goal_translate(Z3_context c, Z3_goal g, Z3_context target) { 170 Z3_TRY; 171 LOG_Z3_goal_translate(c, g, target); 172 RESET_ERROR_CODE(); 173 ast_translation translator(mk_c(c)->m(), mk_c(target)->m()); 174 Z3_goal_ref * _r = alloc(Z3_goal_ref, *mk_c(target)); 175 _r->m_goal = to_goal_ref(g)->translate(translator); 176 mk_c(target)->save_object(_r); 177 Z3_goal r = of_goal(_r); 178 RETURN_Z3(r); 179 Z3_CATCH_RETURN(nullptr); 180 } 181 Z3_goal_to_string(Z3_context c,Z3_goal g)182 Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g) { 183 Z3_TRY; 184 LOG_Z3_goal_to_string(c, g); 185 RESET_ERROR_CODE(); 186 std::ostringstream buffer; 187 to_goal_ref(g)->display(buffer); 188 // Hack for removing the trailing '\n' 189 std::string result = buffer.str(); 190 SASSERT(result.size() > 0); 191 result.resize(result.size()-1); 192 return mk_c(c)->mk_external_string(std::move(result)); 193 Z3_CATCH_RETURN(""); 194 } 195 Z3_goal_to_dimacs_string(Z3_context c,Z3_goal g,bool include_names)196 Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names) { 197 Z3_TRY; 198 LOG_Z3_goal_to_dimacs_string(c, g, include_names); 199 RESET_ERROR_CODE(); 200 std::ostringstream buffer; 201 if (!to_goal_ref(g)->is_cnf()) { 202 SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf"); 203 RETURN_Z3(nullptr); 204 } 205 to_goal_ref(g)->display_dimacs(buffer, include_names); 206 // Hack for removing the trailing '\n' 207 std::string result = buffer.str(); 208 SASSERT(result.size() > 0); 209 result.resize(result.size()-1); 210 return mk_c(c)->mk_external_string(std::move(result)); 211 Z3_CATCH_RETURN(""); 212 } 213 214 }; 215