mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Formatting, whitespace, and Z3_API annotations.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-01-10 21:05:27 +00:00
parent d8d869822f
commit 9f49905582
1 changed files with 10 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/api/z3_api.h
View file

@ -1953,7 +1953,7 @@ extern "C" {
The datatype may be recursive. Return the datatype sort.
\param c logical context.
\param name name of datatype.
\param name name of datatype.
\param num_constructors number of constructors passed in.
\param constructors array of constructor containers.
@ -3088,7 +3088,7 @@ extern "C" {
\param c logical context.
\param numeral A string representing the numeral value in decimal notation. The string may be of the form \code{[num]*[.[num]*][E[+|-][num]+]}.
If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [num]*}.
If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [num]*}.
\param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size.
\sa Z3_mk_int
@ -3393,7 +3393,7 @@ extern "C" {
\c lo number of times, and with an unbounded upper bound.
def_API('Z3_mk_re_loop', AST, (_in(CONTEXT), _in(AST), _in(UINT), _in(UINT)))
*/
*/
Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi);
/**
@ -3430,7 +3430,7 @@ extern "C" {
def_API('Z3_mk_re_full' ,AST ,(_in(CONTEXT), _in(SORT)))
*/
Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re);
/*@}*/
@ -3966,11 +3966,9 @@ extern "C" {
def_API('Z3_mk_atmost', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in(UINT)))
*/
Z3_ast Z3_API Z3_mk_atmost(Z3_context c, unsigned num_args,
Z3_ast const args[], unsigned k);
/**
\brief Pseudo-Boolean relations.
@ -3978,9 +3976,9 @@ extern "C" {
def_API('Z3_mk_atleast', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in(UINT)))
*/
Z3_ast Z3_mk_atleast(Z3_context c, unsigned num_args,
Z3_ast Z3_API Z3_mk_atleast(Z3_context c, unsigned num_args,
Z3_ast const args[], unsigned k);
/**
\brief Pseudo-Boolean relations.
@ -3988,12 +3986,10 @@ extern "C" {
def_API('Z3_mk_pble', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
*/
Z3_ast Z3_API Z3_mk_pble(Z3_context c, unsigned num_args,
Z3_ast const args[], int coeffs[],
int k);
/**
\brief Pseudo-Boolean relations.
@ -4001,8 +3997,7 @@ extern "C" {
def_API('Z3_mk_pbge', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
*/
Z3_ast Z3_mk_pbge(Z3_context c, unsigned num_args,
Z3_ast Z3_API Z3_mk_pbge(Z3_context c, unsigned num_args,
Z3_ast const args[], int coeffs[],
int k);
@ -4013,7 +4008,6 @@ extern "C" {
def_API('Z3_mk_pbeq', AST, (_in(CONTEXT), _in(UINT), _in_array(1,AST), _in_array(1,INT), _in(INT)))
*/
Z3_ast Z3_API Z3_mk_pbeq(Z3_context c, unsigned num_args,
Z3_ast const args[], int coeffs[],
int k);
@ -5228,7 +5222,7 @@ extern "C" {
/*@}*/
/**
\brief Return a string describing the given error code.
\brief Return a string describing the given error code.
Retained function name for backwards compatibility within v4.1
*/
Z3_string Z3_API Z3_get_error_msg_ex(Z3_context c, Z3_error_code err);
@ -6001,11 +5995,11 @@ extern "C" {
/**
\brief retrieve consequences from solver that determine values of the supplied function symbols.
def_API('Z3_solver_get_consequences', INT, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(AST_VECTOR), _in(AST_VECTOR)))
*/
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,
Z3_lbool Z3_API Z3_solver_get_consequences(Z3_context c,
Z3_solver s,
Z3_ast_vector assumptions,
Z3_ast_vector variables,