mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

Merge pull request #2012 from waywardmonkeys/doc-fixups

Browse source 
Fix up more documentation formatting.
This commit is contained in:
Nikolaj Bjorner 2018-12-04 10:16:27 -08:00 • committed by GitHub
commit 2372d1bdeb
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
6 changed files with 111 additions and 112 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/api/z3_api.h
View file

@ -1515,19 +1515,19 @@ extern "C" {
although some parameters can be changed using #Z3_update_param_value.
All main interaction with Z3 happens in the context of a \c Z3_context.
In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects
In contrast to #Z3_mk_context_rc, the life time of \c Z3_ast objects
are determined by the scope level of #Z3_solver_push and #Z3_solver_pop.
In other words, a Z3_ast object remains valid until there is a
call to Z3_solver_pop that takes the current scope below the level where
In other words, a \c Z3_ast object remains valid until there is a
call to #Z3_solver_pop that takes the current scope below the level where
the object was created.
Note that all other reference counted objects, including Z3_model,
Z3_solver, Z3_func_interp have to be managed by the caller.
Note that all other reference counted objects, including \c Z3_model,
\c Z3_solver, \c Z3_func_interp have to be managed by the caller.
Their reference counts are not handled by the context.
Further remarks:
- Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
- Z3 uses hash-consing, i.e., when the same Z3_ast is created twice,
- \c Z3_sort, \c Z3_func_decl, \c Z3_app, \c Z3_pattern are \c Z3_ast's.
- Z3 uses hash-consing, i.e., when the same \c Z3_ast is created twice,
Z3 will return the same pointer twice.
\sa Z3_del_context
@ -1540,20 +1540,20 @@ extern "C" {
\brief Create a context using the given configuration.
This function is similar to #Z3_mk_context. However,
in the context returned by this function, the user
is responsible for managing Z3_ast reference counters.
is responsible for managing \c Z3_ast reference counters.
Managing reference counters is a burden and error-prone,
but allows the user to use the memory more efficiently.
The user must invoke #Z3_inc_ref for any Z3_ast returned
by Z3, and #Z3_dec_ref whenever the Z3_ast is not needed
The user must invoke #Z3_inc_ref for any \c Z3_ast returned
by Z3, and #Z3_dec_ref whenever the \c Z3_ast is not needed
anymore. This idiom is similar to the one used in
BDD (binary decision diagrams) packages such as CUDD.
Remarks:
- Z3_sort, Z3_func_decl, Z3_app, Z3_pattern are Z3_ast's.
- \c Z3_sort, \c Z3_func_decl, \c Z3_app, \c Z3_pattern are \c Z3_ast's.
- After a context is created, the configuration cannot be changed.
- All main interaction with Z3 happens in the context of a \c Z3_context.
- Z3 uses hash-consing, i.e., when the same Z3_ast is created twice,
- Z3 uses hash-consing, i.e., when the same \c Z3_ast is created twice,
Z3 will return the same pointer twice.
def_API('Z3_mk_context_rc', CONTEXT, (_in(CONFIG),))
@ -1615,7 +1615,7 @@ extern "C" {
Starting at Z3 4.0, parameter sets are used to configure many components such as:
simplifiers, tactics, solvers, etc.
\remark Reference counting must be used to manage parameter sets, even when the Z3_context was
\remark Reference counting must be used to manage parameter sets, even when the \c Z3_context was
created using #Z3_mk_context instead of #Z3_mk_context_rc.
def_API('Z3_mk_params', PARAMS, (_in(CONTEXT),))
@ -4998,7 +4998,7 @@ extern "C" {
Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s);
/**
\brief translate model from context c to context \c dst.
\brief translate model from context \c c to context \c dst.
def_API('Z3_model_translate', MODEL, (_in(CONTEXT), _in(MODEL), _in(CONTEXT)))
*/

152
src/api/z3_fpa.h
View file

@ -134,7 +134,7 @@ extern "C" {
\param ebits number of exponent bits
\param sbits number of significand bits
\remark ebits must be larger than 1 and sbits must be larger than 2.
\remark \c ebits must be larger than 1 and \c sbits must be larger than 2.
def_API('Z3_mk_fpa_sort', SORT, (_in(CONTEXT), _in(UINT), _in(UINT)))
*/
@ -213,7 +213,7 @@ extern "C" {
Z3_sort Z3_API Z3_mk_fpa_sort_128(Z3_context c);
/**
\brief Create a floating-point NaN of sort s.
\brief Create a floating-point NaN of sort \c s.
\param c logical context
\param s target sort
@ -223,7 +223,7 @@ extern "C" {
Z3_ast Z3_API Z3_mk_fpa_nan(Z3_context c, Z3_sort s);
/**
\brief Create a floating-point infinity of sort s.
\brief Create a floating-point infinity of sort \c s.
\param c logical context
\param s target sort
@ -236,7 +236,7 @@ extern "C" {
Z3_ast Z3_API Z3_mk_fpa_inf(Z3_context c, Z3_sort s, bool negative);
/**
\brief Create a floating-point zero of sort s.
\brief Create a floating-point zero of sort \c s.
\param c logical context
\param s target sort
@ -252,7 +252,7 @@ extern "C" {
\brief Create an expression of FloatingPoint sort from three bit-vector expressions.
This is the operator named `fp' in the SMT FP theory definition.
Note that \c sign is required to be a bit-vector of size 1. Significand and exponent
Note that \c sgn is required to be a bit-vector of size 1. Significand and exponent
are required to be longer than 1 and 2 respectively. The FloatingPoint sort
of the resulting expression is automatically determined from the bit-vector sizes
of the arguments. The exponent is assumed to be in IEEE-754 biased representation.
@ -276,7 +276,7 @@ extern "C" {
\param v value
\param ty sort
ty must be a FloatingPoint sort
\c ty must be a FloatingPoint sort
\sa Z3_mk_numeral
@ -294,7 +294,7 @@ extern "C" {
\param v value
\param ty sort
ty must be a FloatingPoint sort
\c ty must be a FloatingPoint sort
\sa Z3_mk_numeral
@ -309,7 +309,7 @@ extern "C" {
\param v value
\param ty result sort
ty must be a FloatingPoint sort
\c ty must be a FloatingPoint sort
\sa Z3_mk_numeral
@ -326,7 +326,7 @@ extern "C" {
\param exp exponent
\param ty result sort
ty must be a FloatingPoint sort
\c ty must be a FloatingPoint sort
\sa Z3_mk_numeral
@ -343,7 +343,7 @@ extern "C" {
\param exp exponent
\param ty result sort
ty must be a FloatingPoint sort
\c ty must be a FloatingPoint sort
\sa Z3_mk_numeral
@ -379,7 +379,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
\c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_add', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
@ -393,7 +393,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
\c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_sub', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
@ -407,7 +407,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
\c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_mul', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
@ -421,7 +421,7 @@ extern "C" {
\param t1 term of FloatingPoint sort.
\param t2 term of FloatingPoint sort
The nodes rm must be of RoundingMode sort t1 and t2 must have the same FloatingPoint sort.
The nodes \c rm must be of RoundingMode sort, \c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_div', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST)))
*/
@ -436,9 +436,9 @@ extern "C" {
\param t2 term of FloatingPoint sort
\param t3 term of FloatingPoint sort
The result is round((t1 * t2) + t3)
The result is \ccode{round((t1 * t2) + t3)}.
rm must be of RoundingMode sort, t1, t2, and t3 must have the same FloatingPoint sort.
\c rm must be of RoundingMode sort, \c t1, \c t2, and \c t3 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_fma', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(AST)))
*/
@ -451,7 +451,7 @@ extern "C" {
\param rm term of RoundingMode sort
\param t term of FloatingPoint sort
rm must be of RoundingMode sort, t must have FloatingPoint sort.
\c rm must be of RoundingMode sort, \c t must have FloatingPoint sort.
def_API('Z3_mk_fpa_sqrt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
@ -464,7 +464,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
\c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_rem', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
@ -478,7 +478,7 @@ extern "C" {
\param rm term of RoundingMode sort
\param t term of FloatingPoint sort
t must be of FloatingPoint sort.
\c t must be of FloatingPoint sort.
def_API('Z3_mk_fpa_round_to_integral', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
@ -491,7 +491,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
t1, t2 must have the same FloatingPoint sort.
\c t1, \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_min', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
@ -504,7 +504,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
t1, t2 must have the same FloatingPoint sort.
\c t1, \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_max', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
@ -517,7 +517,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
\c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_leq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
@ -530,7 +530,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
\c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_lt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
@ -543,7 +543,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
\c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_geq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
@ -556,7 +556,7 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort.
\c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_gt', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
@ -569,93 +569,93 @@ extern "C" {
\param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort
Note that this is IEEE 754 equality (as opposed to SMT-LIB =).
Note that this is IEEE 754 equality (as opposed to SMT-LIB \ccode{=}).
t1 and t2 must have the same FloatingPoint sort.
\c t1 and \c t2 must have the same FloatingPoint sort.
def_API('Z3_mk_fpa_eq', AST, (_in(CONTEXT),_in(AST),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_eq(Z3_context c, Z3_ast t1, Z3_ast t2);
/**
\brief Predicate indicating whether t is a normal floating-point number.
\brief Predicate indicating whether \c t is a normal floating-point number.
\param c logical context
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
\c t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_normal', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_normal(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a subnormal floating-point number.
\brief Predicate indicating whether \c t is a subnormal floating-point number.
\param c logical context
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
\c t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_subnormal', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_subnormal(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
\brief Predicate indicating whether \c t is a floating-point number with zero value, i.e., +zero or -zero.
\param c logical context
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
\c t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_zero', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_zero(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a floating-point number representing +oo or -oo.
\brief Predicate indicating whether \c t is a floating-point number representing +oo or -oo.
\param c logical context
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
\c t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_infinite', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_infinite(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a NaN.
\brief Predicate indicating whether \c t is a NaN.
\param c logical context
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
\c t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_nan', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_nan(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a negative floating-point number.
\brief Predicate indicating whether \c t is a negative floating-point number.
\param c logical context
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
\c t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_negative', AST, (_in(CONTEXT),_in(AST)))
*/
Z3_ast Z3_API Z3_mk_fpa_is_negative(Z3_context c, Z3_ast t);
/**
\brief Predicate indicating whether t is a positive floating-point number.
\brief Predicate indicating whether \c t is a positive floating-point number.
\param c logical context
\param t term of FloatingPoint sort
t must have FloatingPoint sort.
\c t must have FloatingPoint sort.
def_API('Z3_mk_fpa_is_positive', AST, (_in(CONTEXT),_in(AST)))
*/
@ -664,15 +664,15 @@ extern "C" {
/**
\brief Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Produces a term that represents the conversion of a bit-vector term bv to a
floating-point term of sort s.
Produces a term that represents the conversion of a bit-vector term \c bv to a
floating-point term of sort \c s.
\param c logical context
\param bv a bit-vector term
\param s floating-point sort
s must be a FloatingPoint sort, t must be of bit-vector sort, and the bit-vector
size of bv must be equal to ebits+sbits of s. The format of the bit-vector is
\c s must be a FloatingPoint sort, \c t must be of bit-vector sort, and the bit-vector
size of \c bv must be equal to \ccode{ebits+sbits} of \c s. The format of the bit-vector is
as defined by the IEEE 754-2008 interchange format.
def_API('Z3_mk_fpa_to_fp_bv', AST, (_in(CONTEXT),_in(AST),_in(SORT)))
@ -682,16 +682,16 @@ extern "C" {
/**
\brief Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Produces a term that represents the conversion of a floating-point term t to a
floating-point term of sort s. If necessary, the result will be rounded according
to rounding mode rm.
Produces a term that represents the conversion of a floating-point term \c t to a
floating-point term of sort \c s. If necessary, the result will be rounded according
to rounding mode \c rm.
\param c logical context
\param rm term of RoundingMode sort
\param t term of FloatingPoint sort
\param s floating-point sort
s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of floating-point sort.
\c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of floating-point sort.
def_API('Z3_mk_fpa_to_fp_float', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
*/
@ -700,16 +700,16 @@ extern "C" {
/**
\brief Conversion of a term of real sort into a term of FloatingPoint sort.
Produces a term that represents the conversion of term t of real sort into a
floating-point term of sort s. If necessary, the result will be rounded according
to rounding mode rm.
Produces a term that represents the conversion of term \c t of real sort into a
floating-point term of sort \c s. If necessary, the result will be rounded according
to rounding mode \c rm.
\param c logical context
\param rm term of RoundingMode sort
\param t term of Real sort
\param s floating-point sort
s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort.
\c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of real sort.
def_API('Z3_mk_fpa_to_fp_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
*/
@ -718,17 +718,17 @@ extern "C" {
/**
\brief Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
Produces a term that represents the conversion of the bit-vector term t into a
floating-point term of sort s. The bit-vector t is taken to be in signed
Produces a term that represents the conversion of the bit-vector term \c t into a
floating-point term of sort \c s. The bit-vector \c t is taken to be in signed
2's complement format. If necessary, the result will be rounded according
to rounding mode rm.
to rounding mode \c rm.
\param c logical context
\param rm term of RoundingMode sort
\param t term of bit-vector sort
\param s floating-point sort
s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort.
\c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of bit-vector sort.
def_API('Z3_mk_fpa_to_fp_signed', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
*/
@ -737,17 +737,17 @@ extern "C" {
/**
\brief Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
Produces a term that represents the conversion of the bit-vector term t into a
floating-point term of sort s. The bit-vector t is taken to be in unsigned
Produces a term that represents the conversion of the bit-vector term \c t into a
floating-point term of sort \c s. The bit-vector \c t is taken to be in unsigned
2's complement format. If necessary, the result will be rounded according
to rounding mode rm.
to rounding mode \c rm.
\param c logical context
\param rm term of RoundingMode sort
\param t term of bit-vector sort
\param s floating-point sort
s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort.
\c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c t must be of bit-vector sort.
def_API('Z3_mk_fpa_to_fp_unsigned', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(SORT)))
*/
@ -756,9 +756,9 @@ extern "C" {
/**
\brief Conversion of a floating-point term into an unsigned bit-vector.
Produces a term that represents the conversion of the floating-point term t into a
bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
Produces a term that represents the conversion of the floating-point term \c t into a
bit-vector term of size \c sz in unsigned 2's complement format. If necessary, the result
will be rounded according to rounding mode \c rm.
\param c logical context
\param rm term of RoundingMode sort
@ -772,9 +772,9 @@ extern "C" {
/**
\brief Conversion of a floating-point term into a signed bit-vector.
Produces a term that represents the conversion of the floating-point term t into a
bit-vector term of size sz in signed 2's complement format. If necessary, the result
will be rounded according to rounding mode rm.
Produces a term that represents the conversion of the floating-point term \c t into a
bit-vector term of size \c sz in signed 2's complement format. If necessary, the result
will be rounded according to rounding mode \c rm.
\param c logical context
\param rm term of RoundingMode sort
@ -788,7 +788,7 @@ extern "C" {
/**
\brief Conversion of a floating-point term into a real-numbered term.
Produces a term that represents the conversion of the floating-point term t into a
Produces a term that represents the conversion of the floating-point term \c t into a
real number. Note that this type of conversion will often result in non-linear
constraints over real terms.
@ -936,7 +936,7 @@ extern "C" {
\param c logical context
\param t a floating-point numeral
Remarks: The significand s is always 0.0 <= s < 2.0; the resulting string is long
Remarks: The significand \c s is always \ccode{0.0 <= s < 2.0}; the resulting string is long
enough to represent the real significand precisely.
def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
@ -951,8 +951,8 @@ extern "C" {
\param n pointer to output uint64
Remarks: This function extracts the significand bits in `t`, without the
hidden bit or normalization. Sets the Z3_INVALID_ARG error code if the
significand does not fit into a uint64. NaN is an invalid argument.
hidden bit or normalization. Sets the \c Z3_INVALID_ARG error code if the
significand does not fit into a \c uint64. NaN is an invalid argument.
def_API('Z3_fpa_get_numeral_significand_uint64', BOOL, (_in(CONTEXT), _in(AST), _out(UINT64)))
*/
@ -1007,7 +1007,7 @@ extern "C" {
\param c logical context
\param t term of FloatingPoint sort
t must have FloatingPoint sort. The size of the resulting bit-vector is automatically
\c t must have FloatingPoint sort. The size of the resulting bit-vector is automatically
determined.
Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
@ -1021,9 +1021,9 @@ extern "C" {
/**
\brief Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
Produces a term that represents the conversion of sig * 2^exp into a
floating-point term of sort s. If necessary, the result will be rounded
according to rounding mode rm.
Produces a term that represents the conversion of \ccode{sig * 2^exp} into a
floating-point term of sort \c s. If necessary, the result will be rounded
according to rounding mode \c rm.
\param c logical context
\param rm term of RoundingMode sort
@ -1031,7 +1031,7 @@ extern "C" {
\param sig significand term of Real sort
\param s FloatingPoint sort
s must be a FloatingPoint sort, rm must be of RoundingMode sort, exp must be of int sort, sig must be of real sort.
\c s must be a FloatingPoint sort, \c rm must be of RoundingMode sort, \c exp must be of int sort, \c sig must be of real sort.
def_API('Z3_mk_fpa_to_fp_int_real', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(AST),_in(SORT)))
*/

6
src/api/z3_optimization.h
View file

@ -228,8 +228,8 @@ extern "C" {
/**
\brief Retrieve lower bound value or approximation for the i'th optimization objective.
The returned vector is of length 3. It always contains numerals.
The three numerals are coefficients a, b, c and encode the result of \c Z3_optimize_get_lower
a * infinity + b + c * epsilon.
The three numerals are coefficients \c a, \c b, \c c and encode the result of
#Z3_optimize_get_lower \ccode{a * infinity + b + c * epsilon}.
\param c - context
\param o - optimization context
@ -330,7 +330,7 @@ extern "C" {
/**
\brief Return objectives on the optimization context.
If the objective function is a max-sat objective it is returned
as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...)
as a Pseudo-Boolean (minimization) sum of the form \ccode{(+ (if f1 w1 0) (if f2 w2 0) ...)}
If the objective function is entered as a maximization objective, then return
the corresponding minimization objective. In this way the resulting objective
function is always returned as a minimization objective.

5
src/api/z3_polynomial.h
View file

@ -36,9 +36,8 @@ extern "C" {
\pre \c p, \c q and \c x are Z3 expressions where \c p and \c q are arithmetic terms.
Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable.
Example: f(a) is a considered to be a variable in the polynomial
f(a)*f(a) + 2*f(a) + 1
Example: \ccode{f(a)} is a considered to be a variable in the polynomial \ccode{
f(a)*f(a) + 2*f(a) + 1}
def_API('Z3_polynomial_subresultants', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/

30
src/api/z3_rcf.h
View file

@ -74,7 +74,7 @@ extern "C" {
Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c);
/**
\brief Store in roots the roots of the polynomial <tt>a[n-1]*x^{n-1} + ... + a[0]</tt>.
\brief Store in roots the roots of the polynomial \ccode{a[n-1]*x^{n-1} + ... + a[0]}.
The output vector \c roots must have size \c n.
It returns the number of roots of the polynomial.
@ -85,91 +85,91 @@ extern "C" {
unsigned Z3_API Z3_rcf_mk_roots(Z3_context c, unsigned n, Z3_rcf_num const a[], Z3_rcf_num roots[]);
/**
\brief Return the value a + b.
\brief Return the value \ccode{a + b}.
def_API('Z3_rcf_add', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_add(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value a - b.
\brief Return the value \ccode{a - b}.
def_API('Z3_rcf_sub', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_sub(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value a * b.
\brief Return the value \ccode{a * b}.
def_API('Z3_rcf_mul', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_mul(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value a / b.
\brief Return the value \ccode{a / b}.
def_API('Z3_rcf_div', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_div(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return the value -a
\brief Return the value \ccode{-a}.
def_API('Z3_rcf_neg', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_neg(Z3_context c, Z3_rcf_num a);
/**
\brief Return the value 1/a
\brief Return the value \ccode{1/a}.
def_API('Z3_rcf_inv', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM)))
*/
Z3_rcf_num Z3_API Z3_rcf_inv(Z3_context c, Z3_rcf_num a);
/**
\brief Return the value a^k
\brief Return the value \ccode{a^k}.
def_API('Z3_rcf_power', RCF_NUM, (_in(CONTEXT), _in(RCF_NUM), _in(UINT)))
*/
Z3_rcf_num Z3_API Z3_rcf_power(Z3_context c, Z3_rcf_num a, unsigned k);
/**
\brief Return \c true if a < b
\brief Return \c true if \ccode{a < b}.
def_API('Z3_rcf_lt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_lt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if a > b
\brief Return \c true if \ccode{a > b}.
def_API('Z3_rcf_gt', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_gt(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if a <= b
\brief Return \c true if \ccode{a <= b}.
def_API('Z3_rcf_le', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_le(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if a >= b
\brief Return \c true if \ccode{a >= b}.
def_API('Z3_rcf_ge', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_ge(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if a == b
\brief Return \c true if \ccode{a == b}.
def_API('Z3_rcf_eq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
bool Z3_API Z3_rcf_eq(Z3_context c, Z3_rcf_num a, Z3_rcf_num b);
/**
\brief Return \c true if a != b
\brief Return \c true if \ccode{a != b}.
def_API('Z3_rcf_neq', BOOL, (_in(CONTEXT), _in(RCF_NUM), _in(RCF_NUM)))
*/
@ -191,7 +191,7 @@ extern "C" {
/**
\brief Extract the "numerator" and "denominator" of the given RCF numeral.
We have that a = n/d, moreover n and d are not represented using rational functions.
We have that \ccode{a = n/d}, moreover \c n and \c d are not represented using rational functions.
def_API('Z3_rcf_get_numerator_denominator', VOID, (_in(CONTEXT), _in(RCF_NUM), _out(RCF_NUM), _out(RCF_NUM)))
*/

2
src/api/z3_spacer.h
View file

@ -48,7 +48,7 @@ extern "C" {
/**
\brief Retrieve a bottom-up (from query) sequence of ground facts
The previous call to Z3_fixedpoint_query must have returned \c Z3_L_TRUE.
The previous call to #Z3_fixedpoint_query must have returned \c Z3_L_TRUE.
def_API('Z3_fixedpoint_get_ground_sat_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT)))
*/