mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

Final adjustments for the FP integration

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-21 17:58:31 +00:00
parent 1209302fe6
commit 2cb84280d8
7 changed files with 192 additions and 216 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
RELEASE_NOTES
View file

@ -3,11 +3,13 @@ RELEASE NOTES
Version 4.4 Version 4.4
============= =============
- New feature: Support for the theory of floating-point numbers. This comes in the form of logics (QF_FP and QF_FPBV), tactics (qffp and qffpbv), as well as a theory plugin that allows theory combinations. Z3 supports the official SMT theory definition of FP (see http://smtlib.cs.uiowa.edu/theories/FloatingPoint.smt2) in SMT2 files, as well as all APIs.
- New feature: Stochastic local search engine for bit-vector formulas (see the qfbv-sls tactic). - New feature: Stochastic local search engine for bit-vector formulas (see the qfbv-sls tactic).
See also: Froehlich, Biere, Wintersteiger, Hamadi: Stochastic Local Search See also: Froehlich, Biere, Wintersteiger, Hamadi: Stochastic Local Search
for Satisfiability Modulo Theories, AAAI 2015. for Satisfiability Modulo Theories, AAAI 2015.
- Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, and Codeplex users rsas, clockish, Heizmann. - Fixed various bugs reported by Marc Brockschmidt, Venkatesh-Prasad Ranganath, Enric Carbonell, Morgan Deters, Tom Ball, Malte Schwerhoff, and Codeplex users rsas, clockish, Heizmann.
Version 4.3.2 Version 4.3.2
============= =============

2
doc/mk_api_doc.py
View file

@ -31,6 +31,7 @@ try:
cleanup_API('../src/api/z3_polynomial.h', 'tmp/z3_polynomial.h') cleanup_API('../src/api/z3_polynomial.h', 'tmp/z3_polynomial.h')
cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h') cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h')
cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h') cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h')
cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h')
print "Removed annotations from z3_api.h." print "Removed annotations from z3_api.h."
try: try:
@ -46,6 +47,7 @@ try:
os.remove('tmp/z3_polynomial.h') os.remove('tmp/z3_polynomial.h')
os.remove('tmp/z3_rcf.h') os.remove('tmp/z3_rcf.h')
os.remove('tmp/z3_interp.h') os.remove('tmp/z3_interp.h')
os.remove('tmp/z3_fpa.h')
print "Removed temporary file z3_api.h." print "Removed temporary file z3_api.h."
os.remove('tmp/website.dox') os.remove('tmp/website.dox')
print "Removed temporary file website.dox" print "Removed temporary file website.dox"

33
doc/z3api.dox
View file

@ -713,39 +713,10 @@ FILE_PATTERNS = website.dox \
z3_polynomial.h \ z3_polynomial.h \
z3_rcf.h \ z3_rcf.h \
z3_interp.h \ z3_interp.h \
z3_fpa.h \
z3++.h \ z3++.h \
z3py.py \ z3py.py \
ApplyResult.cs \ *.cs \
AST.cs \
ASTMap.cs \
ASTVector.cs \
Config.cs \
Constructor.cs \
Context.cs \
DecRefQUeue.cs \
Enumerations.cs \
Expr.cs \
FuncDecl.cs \
FuncInterp.cs \
Goal.cs \
Log.cs \
Model.cs \
Native.cs \
Numeral.cs \
Params.cs \
Pattern.cs \
Probe.cs \
Quantifier.cs \
Solver.cs \
Sort.cs \
Statistics.cs \
Status.cs \
Symbol.cs \
Tactic.cs \
Util.cs \
Version.cs \
Z3Exception.cs \
Z3Object.cs \
*.java *.java
# The RECURSIVE tag can be used to turn specify whether or not subdirectories # The RECURSIVE tag can be used to turn specify whether or not subdirectories

21
src/api/java/Context.java
View file

@ -2000,6 +2000,15 @@ public class Context extends IDisposable
/** /**
* Create a universal Quantifier. * Create a universal Quantifier.
* @param sorts the sorts of the bound variables.
* @param names names of the bound variables
* @param body the body of the quantifier.
* @param weight quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0.
* @param patterns array containing the patterns created using {@code MkPattern}.
* @param noPatterns array containing the anti-patterns created using {@code MkPattern}.
* @param quantifierID optional symbol to track quantifier.
* @param skolemID optional symbol to track skolem constants.
*
* Remarks: Creates a forall formula, where * Remarks: Creates a forall formula, where
* {@code weight"/> is the weight, <paramref name="patterns} is * {@code weight"/> is the weight, <paramref name="patterns} is
* an array of patterns, {@code sorts} is an array with the sorts * an array of patterns, {@code sorts} is an array with the sorts
@ -2007,18 +2016,6 @@ public class Context extends IDisposable
* 'names' of the bound variables, and {@code body} is the body * 'names' of the bound variables, and {@code body} is the body
* of the quantifier. Quantifiers are associated with weights indicating the * of the quantifier. Quantifiers are associated with weights indicating the
* importance of using the quantifier during instantiation. * importance of using the quantifier during instantiation.
*
* @param sorts the sorts of the bound variables.
* @param names names of the bound variables
* @param body the body of the quantifier.
* @param weight quantifiers are
* associated with weights indicating the importance of using the quantifier
* during instantiation. By default, pass the weight 0.
* @param patterns array containing the patterns created using
* {@code MkPattern}.
* @param noPatterns array containing the anti-patterns created using {@code MkPattern}.
* @param quantifierID optional symbol to track quantifier.
* @param skolemID optional symbol to track skolem constants.
**/ **/
public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body, public Quantifier mkForall(Sort[] sorts, Symbol[] names, Expr body,
int weight, Pattern[] patterns, Expr[] noPatterns, int weight, Pattern[] patterns, Expr[] noPatterns,

2
src/api/java/Fixedpoint.java
View file

@ -173,7 +173,7 @@ public class Fixedpoint extends Z3Object
/** /**
* Backtrack one backtracking point. * Backtrack one backtracking point.
* Remarks: Note that an exception is thrown if {#code pop} * Remarks: Note that an exception is thrown if {@code pop}
* is called without a corresponding {@code push} * is called without a corresponding {@code push}
* *
* @see push * @see push

336
src/api/z3_fpa.h
View file

@ -38,7 +38,7 @@ extern "C" {
/** /**
\brief Create the RoundingMode sort. \brief Create the RoundingMode sort.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_rounding_mode_sort', SORT, (_in(CONTEXT),)) def_API('Z3_mk_fpa_rounding_mode_sort', SORT, (_in(CONTEXT),))
*/ */
@ -47,7 +47,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_round_nearest_ties_to_even', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_round_nearest_ties_to_even', AST, (_in(CONTEXT),))
*/ */
@ -56,7 +56,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode. \brief Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_rne', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_rne', AST, (_in(CONTEXT),))
*/ */
@ -65,7 +65,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_round_nearest_ties_to_away', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_round_nearest_ties_to_away', AST, (_in(CONTEXT),))
*/ */
@ -74,7 +74,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode. \brief Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_rna', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_rna', AST, (_in(CONTEXT),))
*/ */
@ -83,7 +83,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_round_toward_positive', AST, (_in(CONTEXT),))
*/ */
@ -92,7 +92,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode. \brief Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_rtp', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_rtp', AST, (_in(CONTEXT),))
*/ */
@ -101,7 +101,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_round_toward_negative', AST, (_in(CONTEXT),))
*/ */
@ -110,7 +110,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode. \brief Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_rtn', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_rtn', AST, (_in(CONTEXT),))
*/ */
@ -119,7 +119,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_round_toward_zero', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_round_toward_zero', AST, (_in(CONTEXT),))
*/ */
@ -128,7 +128,7 @@ extern "C" {
/** /**
\brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode. \brief Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_rtz', AST, (_in(CONTEXT),)) def_API('Z3_mk_fpa_rtz', AST, (_in(CONTEXT),))
*/ */
@ -137,9 +137,9 @@ extern "C" {
/** /**
\brief Create a FloatingPoint sort. \brief Create a FloatingPoint sort.
\param c logical context. \param c logical context
\param ebits number of exponent bits. \param ebits number of exponent bits
\param sbits number of significand bits. \param sbits number of significand bits
\remark ebits must be larger than 1 and sbits must be larger than 2. \remark ebits must be larger than 1 and sbits must be larger than 2.
@ -150,7 +150,7 @@ extern "C" {
/** /**
\brief Create the half-precision (16-bit) FloatingPoint sort. \brief Create the half-precision (16-bit) FloatingPoint sort.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),)) def_API('Z3_mk_fpa_sort_half', SORT, (_in(CONTEXT),))
*/ */
@ -159,7 +159,7 @@ extern "C" {
/** /**
\brief Create the half-precision (16-bit) FloatingPoint sort. \brief Create the half-precision (16-bit) FloatingPoint sort.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),)) def_API('Z3_mk_fpa_sort_16', SORT, (_in(CONTEXT),))
*/ */
@ -177,7 +177,7 @@ extern "C" {
/** /**
\brief Create the single-precision (32-bit) FloatingPoint sort. \brief Create the single-precision (32-bit) FloatingPoint sort.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),)) def_API('Z3_mk_fpa_sort_32', SORT, (_in(CONTEXT),))
*/ */
@ -186,7 +186,7 @@ extern "C" {
/** /**
\brief Create the double-precision (64-bit) FloatingPoint sort. \brief Create the double-precision (64-bit) FloatingPoint sort.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),)) def_API('Z3_mk_fpa_sort_double', SORT, (_in(CONTEXT),))
*/ */
@ -195,7 +195,7 @@ extern "C" {
/** /**
\brief Create the double-precision (64-bit) FloatingPoint sort. \brief Create the double-precision (64-bit) FloatingPoint sort.
\param c logical context. \param c logical context
def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),)) def_API('Z3_mk_fpa_sort_64', SORT, (_in(CONTEXT),))
*/ */
@ -204,11 +204,7 @@ extern "C" {
/** /**
\brief Create the quadruple-precision (128-bit) FloatingPoint sort. \brief Create the quadruple-precision (128-bit) FloatingPoint sort.
\param c logical context. \param c logical context
\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.
def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),)) def_API('Z3_mk_fpa_sort_quadruple', SORT, (_in(CONTEXT),))
*/ */
@ -217,11 +213,7 @@ extern "C" {
/** /**
\brief Create the quadruple-precision (128-bit) FloatingPoint sort. \brief Create the quadruple-precision (128-bit) FloatingPoint sort.
\param c logical context. \param c logical context
\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.
def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),)) def_API('Z3_mk_fpa_sort_128', SORT, (_in(CONTEXT),))
*/ */
@ -230,7 +222,7 @@ extern "C" {
/** /**
\brief Create a floating-point NaN of sort s. \brief Create a floating-point NaN of sort s.
\param c logical context. \param c logical context
\param s target sort \param s target sort
def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT))) def_API('Z3_mk_fpa_nan', AST, (_in(CONTEXT),_in(SORT)))
@ -240,7 +232,7 @@ extern "C" {
/** /**
\brief Create a floating-point infinity of sort s. \brief Create a floating-point infinity of sort s.
\param c logical context. \param c logical context
\param s target sort \param s target sort
\param negative indicates whether the result should be negative \param negative indicates whether the result should be negative
@ -253,7 +245,7 @@ extern "C" {
/** /**
\brief Create a floating-point zero of sort s. \brief Create a floating-point zero of sort s.
\param c logical context. \param c logical context
\param s target sort \param s target sort
\param negative indicates whether the result should be negative \param negative indicates whether the result should be negative
@ -272,10 +264,10 @@ extern "C" {
of the resulting expression is automatically determined from the bit-vector sizes of the resulting expression is automatically determined from the bit-vector sizes
of the arguments. of the arguments.
\params c logical context. \param c logical context
\params sgn sign \param sgn sign
\params exp exponent \param exp exponent
\params sig significand \param sig significand
def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST))) def_API('Z3_mk_fpa_fp', AST, (_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/ */
@ -287,9 +279,9 @@ extern "C" {
This function is used to create numerals that fit in a float value. This function is used to create numerals that fit in a float value.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\params c logical context. \param c logical context
\params v value. \param v value
\params ty sort. \param ty sort
ty must be a FloatingPoint sort ty must be a FloatingPoint sort
@ -305,9 +297,9 @@ extern "C" {
This function is used to create numerals that fit in a double value. This function is used to create numerals that fit in a double value.
It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string. It is slightly faster than #Z3_mk_numeral since it is not necessary to parse a string.
\params c logical context. \param c logical context
\params v value. \param v value
\params ty sort. \param ty sort
ty must be a FloatingPoint sort ty must be a FloatingPoint sort
@ -320,8 +312,9 @@ extern "C" {
/** /**
\brief Create a numeral of FloatingPoint sort from a signed integer. \brief Create a numeral of FloatingPoint sort from a signed integer.
\params c logical context. \param c logical context
\params v value. \param v value
\param ty result sort
ty must be a FloatingPoint sort ty must be a FloatingPoint sort
@ -334,10 +327,11 @@ extern "C" {
/** /**
\brief Create a numeral of FloatingPoint sort from a sign bit and two integers. \brief Create a numeral of FloatingPoint sort from a sign bit and two integers.
\params c logical context. \param c logical context
\params sgn sign bit (true == negative). \param sgn sign bit (true == negative)
\params sig significand. \param sig significand
\params exp exponent. \param exp exponent
\param ty result sort
ty must be a FloatingPoint sort ty must be a FloatingPoint sort
@ -350,10 +344,11 @@ extern "C" {
/** /**
\brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers. \brief Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
\params c logical context. \param c logical context
\params sgn sign bit (true == negative). \param sgn sign bit (true == negative)
\params sig significand. \param sig significand
\params exp exponent. \param exp exponent
\param ty result sort
ty must be a FloatingPoint sort ty must be a FloatingPoint sort
@ -366,8 +361,8 @@ extern "C" {
/** /**
\brief Floating-point absolute value \brief Floating-point absolute value
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST))) def_API('Z3_mk_fpa_abs', AST, (_in(CONTEXT),_in(AST)))
*/ */
@ -376,8 +371,8 @@ extern "C" {
/** /**
\brief Floating-point negation \brief Floating-point negation
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST))) def_API('Z3_mk_fpa_neg', AST, (_in(CONTEXT),_in(AST)))
*/ */
@ -386,10 +381,10 @@ extern "C" {
/** /**
\brief Floating-point addition \brief Floating-point addition
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 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. rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
@ -400,10 +395,10 @@ extern "C" {
/** /**
\brief Floating-point subtraction \brief Floating-point subtraction
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 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. rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
@ -414,10 +409,10 @@ extern "C" {
/** /**
\brief Floating-point multiplication \brief Floating-point multiplication
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 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. rm must be of RoundingMode sort, t1 and t2 must have the same FloatingPoint sort.
@ -428,10 +423,10 @@ extern "C" {
/** /**
\brief Floating-point division \brief Floating-point division
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort.
\param t2 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 rm must be of RoundingMode sort t1 and t2 must have the same FloatingPoint sort.
@ -442,10 +437,11 @@ extern "C" {
/** /**
\brief Floating-point fused multiply-add. \brief Floating-point fused multiply-add.
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort. \param t2 term of FloatingPoint sor
\param t3 term of FloatingPoint sort
The result is round((t1 * t2) + t3) The result is round((t1 * t2) + t3)
@ -458,9 +454,9 @@ extern "C" {
/** /**
\brief Floating-point square root \brief Floating-point square root
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
rm must be of RoundingMode sort, t must have FloatingPoint sort. rm must be of RoundingMode sort, t must have FloatingPoint sort.
@ -471,9 +467,9 @@ extern "C" {
/** /**
\brief Floating-point remainder \brief Floating-point remainder
\param c logical context. \param c logical context
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort. \param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort. t1 and t2 must have the same FloatingPoint sort.
@ -485,9 +481,9 @@ extern "C" {
\brief Floating-point roundToIntegral. Rounds a floating-point number to \brief Floating-point roundToIntegral. Rounds a floating-point number to
the closest integer, again represented as a floating-point number. the closest integer, again represented as a floating-point number.
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
t must be of FloatingPoint sort. t must be of FloatingPoint sort.
@ -498,9 +494,9 @@ extern "C" {
/** /**
\brief Minimum of floating-point numbers. \brief Minimum of floating-point numbers.
\param c logical context. \param c logical context
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort. \param t2 term of FloatingPoint sort
t1, t2 must have the same FloatingPoint sort. t1, t2 must have the same FloatingPoint sort.
@ -511,9 +507,9 @@ extern "C" {
/** /**
\brief Maximum of floating-point numbers. \brief Maximum of floating-point numbers.
\param c logical context. \param c logical context
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort. \param t2 term of FloatingPoint sort
t1, t2 must have the same FloatingPoint sort. t1, t2 must have the same FloatingPoint sort.
@ -524,9 +520,9 @@ extern "C" {
/** /**
\brief Floating-point less than or equal. \brief Floating-point less than or equal.
\param c logical context. \param c logical context
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort. \param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort. t1 and t2 must have the same FloatingPoint sort.
@ -537,9 +533,9 @@ extern "C" {
/** /**
\brief Floating-point less than. \brief Floating-point less than.
\param c logical context. \param c logical context
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort. \param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort. t1 and t2 must have the same FloatingPoint sort.
@ -550,9 +546,9 @@ extern "C" {
/** /**
\brief Floating-point greater than or equal. \brief Floating-point greater than or equal.
\param c logical context. \param c logical context
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort. \param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort. t1 and t2 must have the same FloatingPoint sort.
@ -563,9 +559,9 @@ extern "C" {
/** /**
\brief Floating-point greater than. \brief Floating-point greater than.
\param c logical context. \param c logical context
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 term of FloatingPoint sort. \param t2 term of FloatingPoint sort
t1 and t2 must have the same FloatingPoint sort. t1 and t2 must have the same FloatingPoint sort.
@ -576,9 +572,9 @@ extern "C" {
/** /**
\brief Floating-point equality. \brief Floating-point equality.
\param c logical context. \param c logical context
\param t1 term of FloatingPoint sort. \param t1 term of FloatingPoint sort
\param t2 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 =).
@ -591,8 +587,8 @@ extern "C" {
/** /**
\brief Predicate indicating whether t is a normal floating-point number. \brief Predicate indicating whether t is a normal floating-point number.
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
t must have FloatingPoint sort. t must have FloatingPoint sort.
@ -603,8 +599,8 @@ extern "C" {
/** /**
\brief Predicate indicating whether t is a subnormal floating-point number. \brief Predicate indicating whether t is a subnormal floating-point number.
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
t must have FloatingPoint sort. t must have FloatingPoint sort.
@ -615,8 +611,8 @@ extern "C" {
/** /**
\brief Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero. \brief Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
t must have FloatingPoint sort. t must have FloatingPoint sort.
@ -627,8 +623,8 @@ extern "C" {
/** /**
\brief Predicate indicating whether t is a floating-point number representing +oo or -oo. \brief Predicate indicating whether t is a floating-point number representing +oo or -oo.
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
t must have FloatingPoint sort. t must have FloatingPoint sort.
@ -639,8 +635,8 @@ extern "C" {
/** /**
\brief Predicate indicating whether t is a NaN. \brief Predicate indicating whether t is a NaN.
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
t must have FloatingPoint sort. t must have FloatingPoint sort.
@ -651,8 +647,8 @@ extern "C" {
/** /**
\brief Predicate indicating whether t is a negative floating-point number. \brief Predicate indicating whether t is a negative floating-point number.
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
t must have FloatingPoint sort. t must have FloatingPoint sort.
@ -663,8 +659,8 @@ extern "C" {
/** /**
\brief Predicate indicating whether t is a positive floating-point number. \brief Predicate indicating whether t is a positive floating-point number.
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
t must have FloatingPoint sort. t must have FloatingPoint sort.
@ -678,9 +674,9 @@ extern "C" {
Produces a term that represents the conversion of a bit-vector term bv to a Produces a term that represents the conversion of a bit-vector term bv to a
floating-point term of sort s. floating-point term of sort s.
\param c logical context. \param c logical context
\param bv a bit-vector term. \param bv a bit-vector term
\param s floating-point sort. \param s floating-point sort
s must be a FloatingPoint sort, t must be of bit-vector sort, and the bit-vector 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 size of bv must be equal to ebits+sbits of s. The format of the bit-vector is
@ -697,10 +693,10 @@ extern "C" {
floating-point term of sort s. If necessary, the result will be rounded according floating-point term of sort s. If necessary, the result will be rounded according
to rounding mode rm. to rounding mode rm.
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
\param s floating-point 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. s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of floating-point sort.
@ -715,10 +711,10 @@ extern "C" {
floating-point term of sort s. If necessary, the result will be rounded according floating-point term of sort s. If necessary, the result will be rounded according
to rounding mode rm. to rounding mode rm.
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t term of Real sort. \param t term of Real sort
\param s floating-point sort. \param s floating-point sort
s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort. s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort.
@ -734,10 +730,10 @@ extern "C" {
2's complement format. If necessary, the result will be rounded according 2's complement format. If necessary, the result will be rounded according
to rounding mode rm. to rounding mode rm.
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t term of bit-vector sort. \param t term of bit-vector sort
\param s floating-point 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. s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort.
@ -753,10 +749,10 @@ extern "C" {
2's complement format. If necessary, the result will be rounded according 2's complement format. If necessary, the result will be rounded according
to rounding mode rm. to rounding mode rm.
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t term of bit-vector sort. \param t term of bit-vector sort
\param s floating-point 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. s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of bit-vector sort.
@ -771,10 +767,10 @@ extern "C" {
bit-vector term of size sz in unsigned 2's complement format. If necessary, the result bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
will be rounded according to rounding mode rm. will be rounded according to rounding mode rm.
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
\param sz size of the resulting bit-vector. \param sz size of the resulting bit-vector
def_API('Z3_mk_fpa_to_ubv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT))) def_API('Z3_mk_fpa_to_ubv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
*/ */
@ -787,10 +783,10 @@ extern "C" {
bit-vector term of size sz in signed 2's complement format. If necessary, the result bit-vector term of size sz in signed 2's complement format. If necessary, the result
will be rounded according to rounding mode rm. will be rounded according to rounding mode rm.
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
\param sz size of the resulting bit-vector. \param sz size of the resulting bit-vector
def_API('Z3_mk_fpa_to_sbv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT))) def_API('Z3_mk_fpa_to_sbv', AST, (_in(CONTEXT),_in(AST),_in(AST),_in(UINT)))
*/ */
@ -803,8 +799,8 @@ extern "C" {
real number. Note that this type of conversion will often result in non-linear real number. Note that this type of conversion will often result in non-linear
constraints over real terms. constraints over real terms.
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
def_API('Z3_mk_fpa_to_real', AST, (_in(CONTEXT),_in(AST))) def_API('Z3_mk_fpa_to_real', AST, (_in(CONTEXT),_in(AST)))
*/ */
@ -812,14 +808,15 @@ extern "C" {
/** /**
@name Z3-specific extensions @name Z3-specific floating-point extensions
*/ */
/*@{*/ /*@{*/
/** /**
\brief Retrieves the number of bits reserved for the exponent in a FloatingPoint sort. \brief Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
\param s FloatingPoint sort. \param c logical context
\param s FloatingPoint sort
def_API('Z3_fpa_get_ebits', UINT, (_in(CONTEXT),_in(SORT))) def_API('Z3_fpa_get_ebits', UINT, (_in(CONTEXT),_in(SORT)))
*/ */
@ -828,31 +825,35 @@ extern "C" {
/** /**
\brief Retrieves the number of bits reserved for the significand in a FloatingPoint sort. \brief Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
\param s FloatingPoint sort. \param c logical context
\param s FloatingPoint sort
def_API('Z3_fpa_get_sbits', UINT, (_in(CONTEXT),_in(SORT))) def_API('Z3_fpa_get_sbits', UINT, (_in(CONTEXT),_in(SORT)))
*/ */
unsigned Z3_API Z3_fpa_get_sbits(__in Z3_context c, __in Z3_sort s); unsigned Z3_API Z3_fpa_get_sbits(__in Z3_context c, __in Z3_sort s);
/** /**
\brief Retrieves the sign of a floating-point literal \brief Retrieves the sign of a floating-point literal.
\param c logical context
\param t a floating-point numeral
\param sgn sign
Remarks: sets \c sgn to 0 if the literal is NaN or positive and to 1 otherwise. Remarks: sets \c sgn to 0 if the literal is NaN or positive and to 1 otherwise.
\param t a floating-point numeral.
def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT))) def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
*/ */
Z3_bool Z3_API Z3_fpa_get_numeral_sign(__in Z3_context c, __in Z3_ast t, __out int * sgn); Z3_bool Z3_API Z3_fpa_get_numeral_sign(__in Z3_context c, __in Z3_ast t, __out int * sgn);
/** /**
\brief Return the significand value of a floating-point numeral as a string \brief Return the significand value of a floating-point numeral as a string.
\param c logical context
\param t a floating-point numeral
Remarks: The significand s is always 0 < s < 2.0; the resulting string is long Remarks: The significand s is always 0 < s < 2.0; the resulting string is long
enough to represent the real significand precisely. enough to represent the real significand precisely.
\param t a floating-point numeral.
def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST))) def_API('Z3_fpa_get_numeral_significand_string', STRING, (_in(CONTEXT), _in(AST)))
*/ */
Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t); Z3_string Z3_API Z3_fpa_get_numeral_significand_string(__in Z3_context c, __in Z3_ast t);
@ -860,7 +861,8 @@ extern "C" {
/** /**
\brief Return the exponent value of a floating-point numeral as a string \brief Return the exponent value of a floating-point numeral as a string
\param t a floating-point numeral. \param c logical context
\param t a floating-point numeral
def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST))) def_API('Z3_fpa_get_numeral_exponent_string', STRING, (_in(CONTEXT), _in(AST)))
*/ */
@ -869,7 +871,9 @@ extern "C" {
/** /**
\brief Return the exponent value of a floating-point numeral as a signed 64-bit integer \brief Return the exponent value of a floating-point numeral as a signed 64-bit integer
\param t a floating-point numeral. \param c logical context
\param t a floating-point numeral
\param n exponent
def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64))) def_API('Z3_fpa_get_numeral_exponent_int64', BOOL, (_in(CONTEXT), _in(AST), _out(INT64)))
*/ */
@ -878,8 +882,8 @@ extern "C" {
/** /**
\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format. \brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
\param c logical context. \param c logical context
\param t term of FloatingPoint sort. \param t term of FloatingPoint sort
t must have FloatingPoint sort. The size of the resulting bit-vector is automatically t must have FloatingPoint sort. The size of the resulting bit-vector is automatically
determined. determined.
@ -899,11 +903,11 @@ extern "C" {
floating-point term of sort s. If necessary, the result will be rounded floating-point term of sort s. If necessary, the result will be rounded
according to rounding mode rm. according to rounding mode rm.
\param c logical context. \param c logical context
\param rm term of RoundingMode sort. \param rm term of RoundingMode sort
\param sig significand term of Real sort. \param sig significand term of Real sort
\param exp exponent term of Int sort. \param exp exponent term of Int sort
\param s FloatingPoint sort. \param s FloatingPoint sort
s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort. s must be a FloatingPoint sort, rm must be of RoundingMode sort, t must be of real sort.