1 /*++ 2 Copyright (c) 2013 Microsoft Corporation 3 4 Module Name: 5 6 api_pb.cpp 7 8 Abstract: 9 API for pb theory 10 11 Author: 12 13 Nikolaj Bjorner (nbjorner) 2013-11-13. 14 15 Revision History: 16 17 --*/ 18 #include "api/z3.h" 19 #include "api/api_log_macros.h" 20 #include "api/api_context.h" 21 #include "api/api_util.h" 22 #include "ast/pb_decl_plugin.h" 23 24 extern "C" { 25 26 Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, 27 Z3_ast const args[], unsigned k) { 28 Z3_TRY; 29 LOG_Z3_mk_atmost(c, num_args, args, k); 30 RESET_ERROR_CODE(); 31 parameter param(k); 32 pb_util util(mk_c(c)->m()); 33 ast* a = util.mk_at_most_k(num_args, to_exprs(num_args, args), k); 34 mk_c(c)->save_ast_trail(a); 35 check_sorts(c, a); 36 RETURN_Z3(of_ast(a)); 37 Z3_CATCH_RETURN(nullptr); 38 } 39 40 Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args, 41 Z3_ast const args[], unsigned k) { 42 Z3_TRY; 43 LOG_Z3_mk_atmost(c, num_args, args, k); 44 RESET_ERROR_CODE(); 45 parameter param(k); 46 pb_util util(mk_c(c)->m()); 47 ast* a = util.mk_at_least_k(num_args, to_exprs(num_args, args), k); 48 mk_c(c)->save_ast_trail(a); 49 check_sorts(c, a); 50 RETURN_Z3(of_ast(a)); 51 Z3_CATCH_RETURN(nullptr); 52 } 53 54 Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, 55 Z3_ast const args[], int const _coeffs[], 56 int k) { 57 Z3_TRY; 58 LOG_Z3_mk_pble(c, num_args, args, _coeffs, k); 59 RESET_ERROR_CODE(); 60 pb_util util(mk_c(c)->m()); 61 vector<rational> coeffs; 62 for (unsigned i = 0; i < num_args; ++i) { 63 coeffs.push_back(rational(_coeffs[i])); 64 } 65 ast* a = util.mk_le(num_args, coeffs.c_ptr(), to_exprs(num_args, args), rational(k)); 66 mk_c(c)->save_ast_trail(a); 67 check_sorts(c, a); 68 RETURN_Z3(of_ast(a)); 69 Z3_CATCH_RETURN(nullptr); 70 } 71 72 Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args, 73 Z3_ast const args[], int const _coeffs[], 74 int k) { 75 Z3_TRY; 76 LOG_Z3_mk_pble(c, num_args, args, _coeffs, k); 77 RESET_ERROR_CODE(); 78 pb_util util(mk_c(c)->m()); 79 vector<rational> coeffs; 80 for (unsigned i = 0; i < num_args; ++i) { 81 coeffs.push_back(rational(_coeffs[i])); 82 } 83 ast* a = util.mk_ge(num_args, coeffs.c_ptr(), to_exprs(num_args, args), rational(k)); 84 mk_c(c)->save_ast_trail(a); 85 check_sorts(c, a); 86 RETURN_Z3(of_ast(a)); 87 Z3_CATCH_RETURN(nullptr); 88 } 89 90 Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args, 91 Z3_ast const args[], int const _coeffs[], 92 int k) { 93 Z3_TRY; 94 LOG_Z3_mk_pble(c, num_args, args, _coeffs, k); 95 RESET_ERROR_CODE(); 96 pb_util util(mk_c(c)->m()); 97 vector<rational> coeffs; 98 for (unsigned i = 0; i < num_args; ++i) { 99 coeffs.push_back(rational(_coeffs[i])); 100 } 101 ast* a = util.mk_eq(num_args, coeffs.c_ptr(), to_exprs(num_args, args), rational(k)); 102 mk_c(c)->save_ast_trail(a); 103 check_sorts(c, a); 104 RETURN_Z3(of_ast(a)); 105 Z3_CATCH_RETURN(nullptr); 106 } 107 108 109 }; 110