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 if (g) 57 to_goal(g)->dec_ref(); 58 Z3_CATCH; 59 } 60 Z3_goal_precision(Z3_context c,Z3_goal g)61 Z3_goal_prec Z3_API Z3_goal_precision(Z3_context c, Z3_goal g) { 62 Z3_TRY; 63 LOG_Z3_goal_precision(c, g); 64 RESET_ERROR_CODE(); 65 switch (to_goal_ref(g)->prec()) { 66 case goal::PRECISE: return Z3_GOAL_PRECISE; 67 case goal::UNDER: return Z3_GOAL_UNDER; 68 case goal::OVER: return Z3_GOAL_OVER; 69 case goal::UNDER_OVER: return Z3_GOAL_UNDER_OVER; 70 default: 71 UNREACHABLE(); 72 return Z3_GOAL_UNDER_OVER; 73 } 74 Z3_CATCH_RETURN(Z3_GOAL_UNDER_OVER); 75 } 76 Z3_goal_assert(Z3_context c,Z3_goal g,Z3_ast a)77 void Z3_API Z3_goal_assert(Z3_context c, Z3_goal g, Z3_ast a) { 78 Z3_TRY; 79 LOG_Z3_goal_assert(c, g, a); 80 RESET_ERROR_CODE(); 81 CHECK_FORMULA(a,); 82 to_goal_ref(g)->assert_expr(to_expr(a)); 83 Z3_CATCH; 84 } 85 Z3_goal_inconsistent(Z3_context c,Z3_goal g)86 bool Z3_API Z3_goal_inconsistent(Z3_context c, Z3_goal g) { 87 Z3_TRY; 88 LOG_Z3_goal_inconsistent(c, g); 89 RESET_ERROR_CODE(); 90 return to_goal_ref(g)->inconsistent(); 91 Z3_CATCH_RETURN(false); 92 } 93 Z3_goal_depth(Z3_context c,Z3_goal g)94 unsigned Z3_API Z3_goal_depth(Z3_context c, Z3_goal g) { 95 Z3_TRY; 96 LOG_Z3_goal_depth(c, g); 97 RESET_ERROR_CODE(); 98 return to_goal_ref(g)->depth(); 99 Z3_CATCH_RETURN(0); 100 } 101 Z3_goal_reset(Z3_context c,Z3_goal g)102 void Z3_API Z3_goal_reset(Z3_context c, Z3_goal g) { 103 Z3_TRY; 104 LOG_Z3_goal_reset(c, g); 105 RESET_ERROR_CODE(); 106 to_goal_ref(g)->reset(); 107 Z3_CATCH; 108 } 109 Z3_goal_size(Z3_context c,Z3_goal g)110 unsigned Z3_API Z3_goal_size(Z3_context c, Z3_goal g) { 111 Z3_TRY; 112 LOG_Z3_goal_size(c, g); 113 RESET_ERROR_CODE(); 114 return to_goal_ref(g)->size(); 115 Z3_CATCH_RETURN(0); 116 } 117 Z3_goal_formula(Z3_context c,Z3_goal g,unsigned idx)118 Z3_ast Z3_API Z3_goal_formula(Z3_context c, Z3_goal g, unsigned idx) { 119 Z3_TRY; 120 LOG_Z3_goal_formula(c, g, idx); 121 RESET_ERROR_CODE(); 122 if (idx >= to_goal_ref(g)->size()) { 123 SET_ERROR_CODE(Z3_IOB, nullptr); 124 RETURN_Z3(nullptr); 125 } 126 expr * result = to_goal_ref(g)->form(idx); 127 mk_c(c)->save_ast_trail(result); 128 RETURN_Z3(of_ast(result)); 129 Z3_CATCH_RETURN(nullptr); 130 } 131 Z3_goal_num_exprs(Z3_context c,Z3_goal g)132 unsigned Z3_API Z3_goal_num_exprs(Z3_context c, Z3_goal g) { 133 Z3_TRY; 134 LOG_Z3_goal_num_exprs(c, g); 135 RESET_ERROR_CODE(); 136 return to_goal_ref(g)->num_exprs(); 137 Z3_CATCH_RETURN(0); 138 } 139 Z3_goal_is_decided_sat(Z3_context c,Z3_goal g)140 bool Z3_API Z3_goal_is_decided_sat(Z3_context c, Z3_goal g) { 141 Z3_TRY; 142 LOG_Z3_goal_is_decided_sat(c, g); 143 RESET_ERROR_CODE(); 144 return to_goal_ref(g)->is_decided_sat(); 145 Z3_CATCH_RETURN(false); 146 } 147 Z3_goal_is_decided_unsat(Z3_context c,Z3_goal g)148 bool Z3_API Z3_goal_is_decided_unsat(Z3_context c, Z3_goal g) { 149 Z3_TRY; 150 LOG_Z3_goal_is_decided_unsat(c, g); 151 RESET_ERROR_CODE(); 152 return to_goal_ref(g)->is_decided_unsat(); 153 Z3_CATCH_RETURN(false); 154 } 155 Z3_goal_convert_model(Z3_context c,Z3_goal g,Z3_model m)156 Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m) { 157 Z3_TRY; 158 LOG_Z3_goal_convert_model(c, g, m); 159 RESET_ERROR_CODE(); 160 model_ref new_m; 161 Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c)); 162 mk_c(c)->save_object(m_ref); 163 if (m) m_ref->m_model = to_model_ref(m)->copy(); 164 if (to_goal_ref(g)->mc()) 165 (*to_goal_ref(g)->mc())(m_ref->m_model); 166 RETURN_Z3(of_model(m_ref)); 167 Z3_CATCH_RETURN(nullptr); 168 } 169 Z3_goal_translate(Z3_context c,Z3_goal g,Z3_context target)170 Z3_goal Z3_API Z3_goal_translate(Z3_context c, Z3_goal g, Z3_context target) { 171 Z3_TRY; 172 LOG_Z3_goal_translate(c, g, target); 173 RESET_ERROR_CODE(); 174 ast_translation translator(mk_c(c)->m(), mk_c(target)->m()); 175 Z3_goal_ref * _r = alloc(Z3_goal_ref, *mk_c(target)); 176 _r->m_goal = to_goal_ref(g)->translate(translator); 177 mk_c(target)->save_object(_r); 178 Z3_goal r = of_goal(_r); 179 RETURN_Z3(r); 180 Z3_CATCH_RETURN(nullptr); 181 } 182 Z3_goal_to_string(Z3_context c,Z3_goal g)183 Z3_string Z3_API Z3_goal_to_string(Z3_context c, Z3_goal g) { 184 Z3_TRY; 185 LOG_Z3_goal_to_string(c, g); 186 RESET_ERROR_CODE(); 187 std::ostringstream buffer; 188 to_goal_ref(g)->display(buffer); 189 // Hack for removing the trailing '\n' 190 std::string result = buffer.str(); 191 SASSERT(result.size() > 0); 192 result.resize(result.size()-1); 193 return mk_c(c)->mk_external_string(std::move(result)); 194 Z3_CATCH_RETURN(""); 195 } 196 Z3_goal_to_dimacs_string(Z3_context c,Z3_goal g,bool include_names)197 Z3_string Z3_API Z3_goal_to_dimacs_string(Z3_context c, Z3_goal g, bool include_names) { 198 Z3_TRY; 199 LOG_Z3_goal_to_dimacs_string(c, g, include_names); 200 RESET_ERROR_CODE(); 201 std::ostringstream buffer; 202 if (!to_goal_ref(g)->is_cnf()) { 203 SET_ERROR_CODE(Z3_INVALID_ARG, "If this is not what you want, then preprocess by optional bit-blasting and applying tseitin-cnf"); 204 RETURN_Z3(nullptr); 205 } 206 to_goal_ref(g)->display_dimacs(buffer, include_names); 207 // Hack for removing the trailing '\n' 208 std::string result = buffer.str(); 209 SASSERT(result.size() > 0); 210 result.resize(result.size()-1); 211 return mk_c(c)->mk_external_string(std::move(result)); 212 Z3_CATCH_RETURN(""); 213 } 214 215 }; 216