1 /*++ 2 Copyright (c) Microsoft Corporation, Arie Gurfinkel 2017 3 4 Module Name: 5 6 api_qe.cpp 7 8 Abstract: 9 10 Model-based Projection (MBP) and Quantifier Elimination (QE) API 11 12 Author: 13 14 Arie Gurfinkel (arie) 15 16 Notes: 17 18 --*/ 19 20 #include <iostream> 21 #include "ast/expr_map.h" 22 #include "api/z3.h" 23 #include "api/api_log_macros.h" 24 #include "api/api_context.h" 25 #include "api/api_util.h" 26 #include "api/api_model.h" 27 #include "api/api_ast_map.h" 28 #include "api/api_ast_vector.h" 29 #include "qe/qe_lite.h" 30 #include "muz/spacer/spacer_util.h" 31 32 extern "C" 33 { 34 35 static bool to_apps(unsigned n, Z3_app const es[], app_ref_vector& result) { 36 for (unsigned i = 0; i < n; ++i) { 37 if (!is_app(to_app(es[i]))) { 38 return false; 39 } 40 result.push_back (to_app (es [i])); 41 } 42 return true; 43 } 44 45 Z3_ast Z3_API Z3_qe_model_project (Z3_context c, 46 Z3_model m, 47 unsigned num_bounds, 48 Z3_app const bound[], 49 Z3_ast body) 50 { 51 Z3_TRY; 52 LOG_Z3_qe_model_project (c, m, num_bounds, bound, body); 53 RESET_ERROR_CODE(); 54 55 app_ref_vector vars(mk_c(c)->m ()); 56 if (!to_apps(num_bounds, bound, vars)) { 57 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 58 RETURN_Z3(nullptr); 59 } 60 61 expr_ref result (mk_c(c)->m ()); 62 result = to_expr (body); 63 model_ref model (to_model_ref (m)); 64 spacer::qe_project (mk_c(c)->m (), vars, result, *model); 65 mk_c(c)->save_ast_trail (result.get ()); 66 67 return of_expr (result.get ()); 68 Z3_CATCH_RETURN(nullptr); 69 } 70 71 Z3_ast Z3_API Z3_qe_model_project_skolem (Z3_context c, 72 Z3_model mdl, 73 unsigned num_bounds, 74 Z3_app const bound[], 75 Z3_ast body, 76 Z3_ast_map map) 77 { 78 Z3_TRY; 79 LOG_Z3_qe_model_project_skolem (c, mdl, num_bounds, bound, body, map); 80 RESET_ERROR_CODE(); 81 82 ast_manager& m = mk_c(c)->m(); 83 app_ref_vector vars(m); 84 if (!to_apps(num_bounds, bound, vars)) { 85 RETURN_Z3(nullptr); 86 } 87 88 expr_ref result (m); 89 result = to_expr (body); 90 model_ref model (to_model_ref (mdl)); 91 expr_map emap (m); 92 93 spacer::qe_project(m, vars, result, model, emap); 94 mk_c(c)->save_ast_trail(result); 95 96 obj_map<ast, ast*> &map_z3 = to_ast_map_ref(map); 97 98 for (auto& kv : emap) { 99 m.inc_ref(kv.m_key); 100 m.inc_ref(kv.m_value); 101 map_z3.insert(kv.m_key, kv.m_value); 102 } 103 104 return of_expr (result); 105 Z3_CATCH_RETURN(nullptr); 106 } 107 108 Z3_ast Z3_API Z3_model_extrapolate (Z3_context c, 109 Z3_model m, 110 Z3_ast fml) 111 { 112 Z3_TRY; 113 LOG_Z3_model_extrapolate (c, m, fml); 114 RESET_ERROR_CODE(); 115 116 model_ref model (to_model_ref (m)); 117 expr_ref_vector facts (mk_c(c)->m ()); 118 facts.push_back (to_expr (fml)); 119 flatten_and (facts); 120 121 expr_ref_vector lits = spacer::compute_implicant_literals (*model, facts); 122 123 expr_ref result (mk_c(c)->m ()); 124 result = mk_and (lits); 125 mk_c(c)->save_ast_trail (result); 126 127 return of_expr (result); 128 Z3_CATCH_RETURN(nullptr); 129 } 130 131 Z3_ast Z3_API Z3_qe_lite (Z3_context c, Z3_ast_vector vars, Z3_ast body) 132 { 133 Z3_TRY; 134 LOG_Z3_qe_lite (c, vars, body); 135 RESET_ERROR_CODE(); 136 ast_ref_vector &vVars = to_ast_vector_ref (vars); 137 138 app_ref_vector vApps (mk_c(c)->m()); 139 for (ast* v : vVars) { 140 app * a = to_app(v); 141 if (a->get_kind () != AST_APP) { 142 SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); 143 RETURN_Z3(nullptr); 144 } 145 vApps.push_back (a); 146 } 147 148 expr_ref result (mk_c(c)->m ()); 149 result = to_expr (body); 150 151 params_ref p; 152 qe_lite qe (mk_c(c)->m (), p); 153 qe (vApps, result); 154 155 // -- copy back variables that were not eliminated 156 if (vApps.size () < vVars.size ()) { 157 vVars.reset (); 158 for (app* v : vApps) { 159 vVars.push_back (v); 160 } 161 } 162 163 mk_c(c)->save_ast_trail (result); 164 return of_expr (result); 165 Z3_CATCH_RETURN(nullptr); 166 } 167 168 } 169