From 34af1988166d012ad9a03c7274489d9bbec9886c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Nov 2013 08:51:01 -0800 Subject: [PATCH] missing file Signed-off-by: Nikolaj Bjorner --- src/api/api_pb.cpp | 57 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) create mode 100644 src/api/api_pb.cpp diff --git a/src/api/api_pb.cpp b/src/api/api_pb.cpp new file mode 100644 index 000000000..52290d28a --- /dev/null +++ b/src/api/api_pb.cpp @@ -0,0 +1,57 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + api_pb.cpp + +Abstract: + API for pb theory + +Author: + + Nikolaj Bjorner (nbjorner) 2013-11-13. + +Revision History: + +--*/ +#include +#include"z3.h" +#include"api_log_macros.h" +#include"api_context.h" +#include"api_util.h" +#include"card_decl_plugin.h" + +extern "C" { + + Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args, + Z3_ast const args[], unsigned k) { + Z3_TRY; + LOG_Z3_mk_atmost(c, num_args, args, k); + RESET_ERROR_CODE(); + parameter param(k); + card_util util(mk_c(c)->m()); + ast* a = util.mk_at_most_k(num_args, to_exprs(args), k); + mk_c(c)->save_ast_trail(a); + check_sorts(c, a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } + + + Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args, + Z3_ast const args[], int coeffs[], + int k) { + Z3_TRY; + LOG_Z3_mk_pble(c, num_args, args, coeffs, k); + RESET_ERROR_CODE(); + card_util util(mk_c(c)->m()); + ast* a = util.mk_le(num_args, coeffs, to_exprs(args), k); + mk_c(c)->save_ast_trail(a); + check_sorts(c, a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(0); + } + + +};