Protected Member Functions | |
void | finalize () |
Protected Attributes | |
long | m_refCount = 0 |
The main interaction with Z3 happens via the Context.
Definition at line 27 of file Context.java.
|
inline |
Definition at line 32 of file Context.java.
|
inline |
Constructor. Remarks: The following parameters can be set:
Definition at line 56 of file Context.java.
Create a probe that evaluates to "true" when the value
and
evaluate to "true".
Definition at line 2704 of file Context.java.
Create a tactic that applies
to a Goal and then
.
Definition at line 2401 of file Context.java.
Referenced by Context.then().
|
inline |
Convert a benchmark into an SMT-LIB formatted string.
name | Name of the benchmark. The argument is optional. |
logic | The benchmark logic. |
status | The status string (sat, unsat, or unknown) |
attributes | Other attributes, such as source, difficulty or category. |
assumptions | Auxiliary assumptions. |
formula | Formula to be checked for consistency in conjunction with assumptions. |
Definition at line 2141 of file Context.java.
Create a tactic that applies
to a given goal if the probe
otherwise.
Definition at line 2482 of file Context.java.
|
inline |
|
inline |
Disposes of the context.
Definition at line 3792 of file Context.java.
Referenced by Context.finalize().
Create a probe that evaluates to "true" when the value returned by
is equal to the value returned by
Definition at line 2693 of file Context.java.
Referenced by SortRef.cast(), and BoolSortRef.cast().
|
inline |
Create a tactic always fails.
Definition at line 2513 of file Context.java.
Create a tactic that fails if the probe
evaluates to false.
Definition at line 2522 of file Context.java.
|
inline |
Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains `false').
Definition at line 2533 of file Context.java.
|
inlineprotected |
Create a probe that evaluates to "true" when the value returned by
is greater than or equal the value returned by
Definition at line 2681 of file Context.java.
|
inline |
Definition at line 3699 of file Context.java.
Referenced by ApplyResult.toString().
|
inline |
Definition at line 3684 of file Context.java.
Referenced by AST.getSExpr().
|
inline |
Definition at line 3689 of file Context.java.
|
inline |
Definition at line 3694 of file Context.java.
Referenced by ASTVector.toString().
|
inline |
Retrieves the Boolean sort of the context.
Definition at line 105 of file Context.java.
Referenced by Context.mkBoolConst().
|
inline |
Definition at line 3754 of file Context.java.
Referenced by Fixedpoint.ParseString().
|
inline |
Definition at line 3704 of file Context.java.
Referenced by FuncInterp.Entry.toString().
|
inline |
Definition at line 3709 of file Context.java.
Referenced by FuncInterp.toString().
|
inline |
Definition at line 3714 of file Context.java.
Referenced by Goal.AsBoolExpr().
|
inline |
Retrieves the Integer sort of the context.
Definition at line 115 of file Context.java.
Referenced by Context.mkInt(), and Context.mkIntConst().
|
inline |
Definition at line 3719 of file Context.java.
Referenced by Model.toString().
|
inline |
The number of supported Probes.
Definition at line 2596 of file Context.java.
Referenced by Context.getProbeNames().
|
inline |
The number of SMTLIB assumptions parsed by the last call to
or
.
Definition at line 2223 of file Context.java.
Referenced by Context.getSMTLIBAssumptions().
|
inline |
The number of SMTLIB declarations parsed by the last call to
or
.
Definition at line 2247 of file Context.java.
Referenced by Context.getSMTLIBDecls().
|
inline |
The number of SMTLIB formulas parsed by the last call to
or
.
Definition at line 2199 of file Context.java.
Referenced by Context.getSMTLIBFormulas().
|
inline |
The number of SMTLIB sorts parsed by the last call to
or
.
Definition at line 2270 of file Context.java.
Referenced by Context.getSMTLIBSorts().
|
inline |
The number of supported tactics.
Definition at line 2362 of file Context.java.
Referenced by Context.getTacticNames().
|
inline |
Definition at line 3759 of file Context.java.
|
inline |
Definition at line 3729 of file Context.java.
Referenced by ParamDescrs.toString().
|
inline |
Definition at line 3724 of file Context.java.
Referenced by Params.toString().
|
inline |
Returns a string containing a description of the probe with the given name.
Definition at line 2618 of file Context.java.
|
inline |
Definition at line 3734 of file Context.java.
Referenced by Probe.apply().
|
inline |
|
inline |
Retrieves the Real sort of the context.
Definition at line 125 of file Context.java.
Referenced by Context.mkReal(), and Context.mkRealConst().
|
inline |
Retrieves parameter descriptions for simplifier.
Definition at line 3623 of file Context.java.
|
inline |
The assumptions parsed by the last call to
or
.
Definition at line 2232 of file Context.java.
|
inline |
The declarations parsed by the last call to
or
.
Definition at line 2256 of file Context.java.
|
inline |
The formulas parsed by the last call to
or
.
Definition at line 2208 of file Context.java.
|
inline |
The declarations parsed by the last call to
or
.
Definition at line 2279 of file Context.java.
|
inline |
Definition at line 3739 of file Context.java.
Referenced by Solver.toString().
|
inline |
Definition at line 3744 of file Context.java.
|
inline |
Returns a string containing a description of the tactic with the given name.
Definition at line 2384 of file Context.java.
|
inline |
Definition at line 3749 of file Context.java.
Referenced by Tactic.getSolver().
|
inline |
Create a probe that evaluates to "true" when the value returned by
is greater than the value returned by
Definition at line 2655 of file Context.java.
|
inline |
Interrupt the execution of a Z3 procedure. Remarks: This procedure can be used to interrupt: solvers, simplifiers and tactics.
Definition at line 2588 of file Context.java.
Create a probe that evaluates to "true" when the value returned by
is less than or equal the value returned by
Definition at line 2668 of file Context.java.
Create a probe that evaluates to "true" when the value returned by
is less than the value returned by
Definition at line 2643 of file Context.java.
|
inline |
|
inline |
Create an expression representing
.
Definition at line 723 of file Context.java.
Referenced by Goal.AsBoolExpr().
Create a new function application.
Definition at line 610 of file Context.java.
Referenced by EnumSort.getConst(), EnumSort.getConsts(), ListSort.getNil(), and Context.mkConst().
Create an array constant.
Definition at line 1601 of file Context.java.
Create an array constant.
Definition at line 1610 of file Context.java.
Create a new array sort.
Definition at line 184 of file Context.java.
Referenced by Context.mkArrayConst().
|
inline |
Create a new bit-vector sort.
Definition at line 176 of file Context.java.
Referenced by Context.mkBV(), and Context.mkBVConst().
|
inline |
|
inline |
|
inline |
Creates a new bound variable.
index | The de-Bruijn index of the variable |
ty | The sort of the variable |
Definition at line 480 of file Context.java.
|
inline |
Create a bit-vector numeral.
v | A string representing the value in decimal notation. |
size | the size of the bit-vector |
Definition at line 1986 of file Context.java.
|
inline |
Create a bit-vector numeral.
v | value of the numeral. |
size | the size of the bit-vector |
Definition at line 1996 of file Context.java.
|
inline |
Create a bit-vector numeral.
v | value of the numeral. * |
size | the size of the bit-vector |
Definition at line 2006 of file Context.java.
|
inline |
Create an integer from the bit-vector argument
. Remarks: If is_signed
is false, then the bit-vector t1
is treated as unsigned. So the result is non-negative and in the range
, where N are the number of bits in
. If is_signed
is true, t1
is treated as a signed bit-vector.
NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.
The argument must be of bit-vector sort.
Definition at line 1478 of file Context.java.
|
inline |
Two's complement addition. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1041 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise addition does not overflow. Remarks: The arguments must be of bit-vector sort.
Definition at line 1490 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise addition does not underflow. Remarks: The arguments must be of bit-vector sort.
Definition at line 1505 of file Context.java.
|
inline |
Bitwise conjunction. Remarks: The arguments must have a bit-vector sort.
Definition at line 952 of file Context.java.
|
inline |
Arithmetic shift right Remarks: It is like logical shift right except that the most significant bits of the result always copy the most significant bit of the second argument.
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1386 of file Context.java.
|
inline |
|
inline |
|
inline |
Logical shift right Remarks: It is equivalent to unsigned division by
where x
is the value of
.
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1366 of file Context.java.
|
inline |
Two's complement multiplication. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1067 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise multiplication does not overflow. Remarks: The arguments must be of bit-vector sort.
Definition at line 1574 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise multiplication does not underflow. Remarks: The arguments must be of bit-vector sort.
Definition at line 1589 of file Context.java.
|
inline |
Bitwise NAND. Remarks: The arguments must have a bit-vector sort.
Definition at line 991 of file Context.java.
|
inline |
Standard two's complement unary minus. Remarks: The arguments must have a bit-vector sort.
Definition at line 1030 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise negation does not overflow. Remarks: The arguments must be of bit-vector sort.
Definition at line 1562 of file Context.java.
|
inline |
Bitwise NOR. Remarks: The arguments must have a bit-vector sort.
Definition at line 1004 of file Context.java.
|
inline |
Bitwise negation. Remarks: The argument must have a bit-vector sort.
Definition at line 917 of file Context.java.
|
inline |
Bitwise disjunction. Remarks: The arguments must have a bit-vector sort.
Definition at line 965 of file Context.java.
|
inline |
Take conjunction of bits in a vector, return vector of length 1.
Remarks: The argument must have a bit-vector sort.
Definition at line 928 of file Context.java.
|
inline |
Take disjunction of bits in a vector, return vector of length 1.
Remarks: The argument must have a bit-vector sort.
Definition at line 940 of file Context.java.
|
inline |
Rotate Left. Remarks: Rotate bits of t
to the left i
times. The argument
must have a bit-vector sort.
Definition at line 1399 of file Context.java.
|
inline |
Rotate Left. Remarks: Rotate bits of
to the left
times. The arguments must have the same bit-vector sort.
Definition at line 1424 of file Context.java.
|
inline |
Rotate Right. Remarks: Rotate bits of t
to the right i
times. The argument
must have a bit-vector sort.
Definition at line 1411 of file Context.java.
|
inline |
Rotate Right. Remarks: Rotate bits of
to the right
times. The arguments must have the same bit-vector sort.
Definition at line 1439 of file Context.java.
|
inline |
Signed division. Remarks: It is defined in the following way:
floor
oft2
is different from zero, and ceiling
oft2
is different from zero, andIf
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1103 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise signed division does not overflow. Remarks: The arguments must be of bit-vector sort.
Definition at line 1548 of file Context.java.
|
inline |
Two's complement signed greater than or equal to. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1228 of file Context.java.
|
inline |
Two's complement signed greater-than. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1254 of file Context.java.
|
inline |
Shift left. Remarks: It is equivalent to multiplication by
where x
is the value of
.
NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.
The arguments must have a bit-vector sort.
Definition at line 1347 of file Context.java.
|
inline |
Two's complement signed less-than or equal to. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1202 of file Context.java.
|
inline |
Two's complement signed less-than Remarks: The arguments must have the same bit-vector sort.
Definition at line 1176 of file Context.java.
|
inline |
Two's complement signed remainder (sign follows divisor). Remarks: If
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1150 of file Context.java.
|
inline |
Signed remainder. Remarks: It is defined as
, where
represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1
.
If
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1136 of file Context.java.
|
inline |
Two's complement subtraction. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1054 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise subtraction does not overflow. Remarks: The arguments must be of bit-vector sort.
Definition at line 1519 of file Context.java.
|
inline |
Create a predicate that checks that the bit-wise subtraction does not underflow. Remarks: The arguments must be of bit-vector sort.
Definition at line 1533 of file Context.java.
|
inline |
Unsigned division. Remarks: It is defined as the floor of
if t2
is different from zero. If
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1082 of file Context.java.
|
inline |
Unsigned greater than or equal to. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1215 of file Context.java.
|
inline |
Unsigned greater-than. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1241 of file Context.java.
|
inline |
Unsigned less-than or equal to. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1189 of file Context.java.
|
inline |
Unsigned less-than Remarks: The arguments must have the same bit-vector sort.
Definition at line 1163 of file Context.java.
|
inline |
Unsigned remainder. Remarks: It is defined as
, where
represents unsigned division. If
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1118 of file Context.java.
|
inline |
Bitwise XNOR. Remarks: The arguments must have a bit-vector sort.
Definition at line 1017 of file Context.java.
|
inline |
Bitwise XOR. Remarks: The arguments must have a bit-vector sort.
Definition at line 978 of file Context.java.
|
inline |
Bit-vector concatenation. Remarks: The arguments must have a bit-vector sort.
Definition at line 1272 of file Context.java.
Creates a new Constant of sort
and named
.
Definition at line 503 of file Context.java.
Referenced by Context.mkArrayConst(), Context.mkBoolConst(), Context.mkBVConst(), Context.mkConst(), Context.mkIntConst(), and Context.mkRealConst().
Creates a fresh constant from the FuncDecl
.
f | A decl of a 0-arity function |
Definition at line 538 of file Context.java.
Create a constant array. Remarks: The resulting term is an array, such that a
on an arbitrary index produces the value
.
Definition at line 1673 of file Context.java.
Creates a new constant function declaration.
Definition at line 446 of file Context.java.
|
inline |
Create a datatype constructor.
name | constructor name |
recognizer | name of recognizer function. |
fieldNames | names of the constructor fields. |
sorts | field sorts, 0 if the field sort refers to a recursive sort. |
sortRefs | reference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared. |
Definition at line 273 of file Context.java.
|
inline |
Create a datatype constructor.
name | |
recognizer | |
fieldNames | |
sorts | |
sortRefs |
Definition at line 292 of file Context.java.
|
inline |
Create a new datatype sort.
Definition at line 304 of file Context.java.
|
inline |
|
inline |
Create mutually recursive datatypes.
names | names of datatype sorts |
c | list of constructors, one list per sort. |
Definition at line 327 of file Context.java.
Referenced by Context.mkDatatypeSorts().
|
inline |
Create mutually recursive data-types.
names | |
c |
Definition at line 358 of file Context.java.
|
inline |
Create an empty set.
Definition at line 1728 of file Context.java.
|
inline |
|
inline |
Create an existential Quantifier.
Definition at line 2055 of file Context.java.
Referenced by Context.mkQuantifier().
|
inline |
Create an existential Quantifier.
Definition at line 2067 of file Context.java.
|
inline |
Bit-vector extraction. Remarks: Extract the bits
down to
from a bitvector of size
to yield a new bitvector of size
, where
. The argument
must have a bit-vector sort.
Definition at line 1288 of file Context.java.
|
inline |
|
inline |
|
inline |
|
inline |
Create a Fixedpoint context.
Definition at line 2794 of file Context.java.
|
inline |
Create a universal Quantifier.
sorts | the sorts of the bound variables. |
names | names of the bound variables |
body | the body of the quantifier. |
weight | quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. By default, pass the weight 0. |
patterns | array containing the patterns created using MkPattern |
noPatterns | array containing the anti-patterns created using MkPattern |
quantifierID | optional symbol to track quantifier. |
skolemID | optional symbol to track skolem constants. |
Remarks: Creates a forall formula, where
is an array of patterns,
is an array with the sorts of the bound variables,
is an array with the 'names' of the bound variables, and
is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation.
Definition at line 2030 of file Context.java.
Referenced by Context.mkQuantifier().
|
inline |
Create a universal Quantifier.
Definition at line 2042 of file Context.java.
Create a numeral of FloatingPoint sort from a float.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3088 of file Context.java.
Create a numeral of FloatingPoint sort from a float.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3099 of file Context.java.
Create a numeral of FloatingPoint sort from an int.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3111 of file Context.java.
Create a numeral of FloatingPoint sort from a sign bit and two integers.
sgn | the sign. |
exp | the exponent. |
sig | the significand. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3124 of file Context.java.
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
sgn | the sign. |
exp | the exponent. |
sig | the significand. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3137 of file Context.java.
|
inline |
Create an expression of FloatingPoint sort from three bit-vector expressions.
sgn | bit-vector term (of size 1) representing the sign. |
sig | bit-vector term representing the significand. |
exp | bit-vector term representing the exponent. Remarks: This is the operator named `fp' in the SMT FP theory definition. Note that sgn is required to be a bit-vector of size 1. Significand and exponent are required to be greater than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments. |
Z3Exception |
Definition at line 3422 of file Context.java.
Floating-point absolute value
t | floating-point term |
Z3Exception |
Definition at line 3148 of file Context.java.
Floating-point addition
rm | rounding mode term |
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3170 of file Context.java.
Floating-point division
rm | rounding mode term |
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3206 of file Context.java.
Floating-point equality.
t1 | floating-point term |
t2 | floating-point term Remarks: Note that this is IEEE 754 equality (as opposed to standard =). |
Z3Exception |
Definition at line 3334 of file Context.java.
Floating-point fused multiply-add
rm | rounding mode term |
t1 | floating-point term |
t2 | floating-point term |
t3 | floating-point term Remarks: The result is round((t1 * t2) + t3) |
Z3Exception |
Definition at line 3221 of file Context.java.
Floating-point greater than or equal.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3310 of file Context.java.
Floating-point greater than.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3321 of file Context.java.
Create a floating-point infinity of sort s.
s | FloatingPoint sort. |
negative | indicates whether the result should be negative. |
Z3Exception |
Definition at line 3007 of file Context.java.
Predicate indicating whether t is a floating-point number representing +oo or -oo.
t | floating-point term |
Z3Exception |
Definition at line 3374 of file Context.java.
Predicate indicating whether t is a NaN.
t | floating-point term |
Z3Exception |
Definition at line 3384 of file Context.java.
Predicate indicating whether t is a negative floating-point number.
t | floating-point term |
Z3Exception |
Definition at line 3394 of file Context.java.
Predicate indicating whether t is a normal floating-point number.\
t | floating-point term |
Z3Exception |
Definition at line 3344 of file Context.java.
Predicate indicating whether t is a positive floating-point number.
t | floating-point term |
Z3Exception |
Definition at line 3404 of file Context.java.
Predicate indicating whether t is a subnormal floating-point number.\
t | floating-point term |
Z3Exception |
Definition at line 3354 of file Context.java.
Predicate indicating whether t is a floating-point number with zero value, i.e., +0 or -0.
t | floating-point term |
Z3Exception |
Definition at line 3364 of file Context.java.
Floating-point less than or equal.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3288 of file Context.java.
Floating-point less than.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3299 of file Context.java.
Maximum of floating-point numbers.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3277 of file Context.java.
Minimum of floating-point numbers.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3266 of file Context.java.
Floating-point multiplication
rm | rounding mode term |
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3194 of file Context.java.
Create a NaN of sort s.
s | FloatingPoint sort. |
Z3Exception |
Definition at line 2996 of file Context.java.
Floating-point negation
t | floating-point term |
Z3Exception |
Definition at line 3158 of file Context.java.
Create a numeral of FloatingPoint sort from a float.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3029 of file Context.java.
Referenced by Context.mkFP().
Create a numeral of FloatingPoint sort from a float.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3040 of file Context.java.
Create a numeral of FloatingPoint sort from an int.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3051 of file Context.java.
Create a numeral of FloatingPoint sort from a sign bit and two integers.
sgn | the sign. |
sig | the significand. |
exp | the exponent. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3064 of file Context.java.
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
sgn | the sign. |
sig | the significand. |
exp | the exponent. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3077 of file Context.java.
Floating-point remainder
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3243 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Z3Exception |
Definition at line 2848 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3Exception |
Definition at line 2830 of file Context.java.
|
inline |
Create the floating-point RoundingMode sort.
Z3Exception |
Definition at line 2812 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Z3Exception |
Definition at line 2839 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3Exception |
Definition at line 2821 of file Context.java.
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
rm | term of RoundingMode sort |
t | floating-point term |
Z3Exception |
Definition at line 3255 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Z3Exception |
Definition at line 2875 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Z3Exception |
Definition at line 2857 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Z3Exception |
Definition at line 2893 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Z3Exception |
Definition at line 2884 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Z3Exception |
Definition at line 2866 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Z3Exception |
Definition at line 2902 of file Context.java.
|
inline |
Create a FloatingPoint sort.
ebits | exponent bits in the FloatingPoint sort. |
sbits | significand bits in the FloatingPoint sort. |
Z3Exception |
Definition at line 2913 of file Context.java.
|
inline |
Create the quadruple-precision (128-bit) FloatingPoint sort.
Z3Exception |
Definition at line 2985 of file Context.java.
|
inline |
Create the half-precision (16-bit) FloatingPoint sort.
Z3Exception |
Definition at line 2931 of file Context.java.
|
inline |
Create the single-precision (32-bit) FloatingPoint sort.
Z3Exception |
Definition at line 2949 of file Context.java.
|
inline |
Create the double-precision (64-bit) FloatingPoint sort.
Z3Exception |
Definition at line 2967 of file Context.java.
|
inline |
Create the double-precision (64-bit) FloatingPoint sort.
Z3Exception |
Definition at line 2958 of file Context.java.
|
inline |
Create the half-precision (16-bit) FloatingPoint sort.
Z3Exception |
Definition at line 2922 of file Context.java.
|
inline |
Create the quadruple-precision (128-bit) FloatingPoint sort.
Z3Exception |
Definition at line 2976 of file Context.java.
|
inline |
Create the single-precision (32-bit) FloatingPoint sort.
Z3Exception |
Definition at line 2940 of file Context.java.
Floating-point square root
rm | rounding mode term |
t | floating-point term |
Z3Exception |
Definition at line 3232 of file Context.java.
Floating-point subtraction
rm | rounding mode term |
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3182 of file Context.java.
|
inline |
Conversion of a floating-point term into a bit-vector.
rm | RoundingMode term. |
t | FloatingPoint term |
sz | Size of the resulting bit-vector. |
signed | Indicates whether the result is a signed or unsigned bit-vector. Remarks: Produces a term that represents the conversion of the floating-poiunt term t into a bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, the result will be rounded according to rounding mode rm. |
Z3Exception |
Definition at line 3523 of file Context.java.
|
inline |
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
bv | bit-vector value (of size m). |
s | FloatingPoint sort (ebits+sbits == m) Remarks: Produces a term that represents the conversion of a bit-vector term bv to a floating-point term of sort s. The bit-vector size of bv (m) must be equal to ebits+sbits of s. The format of the bit-vector is as defined by the IEEE 754-2008 interchange format. |
Z3Exception |
Definition at line 3438 of file Context.java.
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
rm | RoundingMode term. |
t | FloatingPoint term. |
s | FloatingPoint sort. Remarks: 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. |
Z3Exception |
Definition at line 3454 of file Context.java.
Conversion of a term of real sort into a term of FloatingPoint sort.
rm | RoundingMode term. |
t | term of Real sort. |
s | FloatingPoint sort. Remarks: 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. |
Z3Exception |
Definition at line 3470 of file Context.java.
|
inline |
Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
rm | RoundingMode term. |
t | term of bit-vector sort. |
s | FloatingPoint sort. |
signed | flag indicating whether t is interpreted as signed or unsigned bit-vector. Remarks: 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 2's complement format (when signed==true, otherwise unsigned). If necessary, the result will be rounded according to rounding mode rm. |
Z3Exception |
Definition at line 3488 of file Context.java.
Conversion of a floating-point number to another FloatingPoint sort s.
s | FloatingPoint sort |
rm | floating-point rounding mode term |
t | floating-point term Remarks: Produces a term that represents the conversion of a floating-point term t to a different FloatingPoint sort s. If necessary, rounding according to rm is applied. |
Z3Exception |
Definition at line 3506 of file Context.java.
|
inline |
Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
rm | RoundingMode term. |
exp | Exponent term of Int sort. |
sig | Significand term of Real sort. |
s | FloatingPoint sort. Remarks: 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. |
Z3Exception |
Definition at line 3573 of file Context.java.
|
inline |
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
t | FloatingPoint term. Remarks: The size of the resulting bit-vector is automatically determined. Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector represenatation of that NaN. |
Z3Exception |
Definition at line 3555 of file Context.java.
Conversion of a floating-point term into a real-numbered term.
t | FloatingPoint term Remarks: Produces a term that represents the conversion of the floating-poiunt term t into a real number. Note that this type of conversion will often result in non-linear constraints over real terms. |
Z3Exception |
Definition at line 3540 of file Context.java.
Create a floating-point zero of sort s.
s | FloatingPoint sort. |
negative | indicates whether the result should be negative. |
Z3Exception |
Definition at line 3018 of file Context.java.
Creates a fresh Constant of sort
and a name prefixed with
.
Definition at line 527 of file Context.java.
Creates a fresh constant function declaration with a name prefixed with
.
Definition at line 468 of file Context.java.
Creates a fresh function declaration with a name prefixed with
.
Definition at line 435 of file Context.java.
Create the full set.
Definition at line 1738 of file Context.java.
Creates a new function declaration.
Definition at line 384 of file Context.java.
Creates a new function declaration.
Definition at line 396 of file Context.java.
|
inline |
Creates a new Goal. Remarks: Note that the Context must have been created with proof generation support if
is set to true here.
models | Indicates whether model generation should be enabled. |
unsatCores | Indicates whether unsat core generation should be enabled. |
proofs | Indicates whether proof generation should be enabled. |
Definition at line 2345 of file Context.java.
|
inline |
Create an integer numeral.
v | A string representing the Term value in decimal notation. |
Definition at line 1948 of file Context.java.
|
inline |
Create an integer numeral.
v | value of the numeral. |
Definition at line 1961 of file Context.java.
|
inline |
Create an integer numeral.
v | value of the numeral. |
Definition at line 1974 of file Context.java.
|
inline |
Create an
bit bit-vector from the integer argument
. Remarks: NB. This function is essentially treated as uninterpreted. So you cannot expect Z3 to precisely reflect the semantics of this function when solving constraints with this function.
The argument must be of integer sort.
Definition at line 1457 of file Context.java.
Coerce an integer to a real. Remarks: There is also a converse operation exposed. It follows the semantics prescribed by the SMT-LIB standard.
You can take the floor of a real by creating an auxiliary integer Term
and and asserting
. The argument must be of integer sort.
Definition at line 884 of file Context.java.
|
inline |
|
inline |
Create a new integer sort.
Definition at line 160 of file Context.java.
Creates an expression that checks whether a real number is an integer.
Definition at line 906 of file Context.java.
Create an expression representing an if-then-else:
.
t1 | An expression with Boolean sort |
t2 | An expression |
t3 | An expression with the same sort as t2 |
Definition at line 678 of file Context.java.
Create a new list sort.
Definition at line 227 of file Context.java.
Maps f on the argument arrays. Remarks: Eeach element of
must be of an array sort
. The function declaration
must have type
.
must have sort range. The sort of the result is
.
Definition at line 1694 of file Context.java.
Create an expression representing
. Remarks: The arguments must have int type.
Definition at line 796 of file Context.java.
|
inline |
Create a Term of a given sort.
v | A string representing the term value in decimal notation. If the given sort is a real, then the Term can be a rational, that is, a string of the form [num]* / [num]* |
ty | The sort of the numeral. In the current implementation, the given sort can be an int, real, or bit-vectors of arbitrary size. |
Definition at line 1848 of file Context.java.
Referenced by Context.mkBV().
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than
since it is not necessary to parse a string.
v | Value of the numeral |
ty | Sort of the numeral |
Definition at line 1865 of file Context.java.
Create a Term of a given sort. This function can be use to create numerals that fit in a machine integer. It is slightly faster than
since it is not necessary to parse a string.
v | Value of the numeral |
ty | Sort of the numeral |
Definition at line 1881 of file Context.java.
|
inline |
Create a Optimize context.
Definition at line 2802 of file Context.java.
|
inline |
|
inline |
Creates a new ParameterSet.
Definition at line 2354 of file Context.java.
|
inline |
Create a quantifier pattern.
Definition at line 489 of file Context.java.
|
inline |
Creates a new Probe.
Definition at line 2626 of file Context.java.
|
inline |
Create a Quantifier.
Definition at line 2079 of file Context.java.
|
inline |
Create a Quantifier.
Definition at line 2096 of file Context.java.
|
inline |
Create a real from a fraction.
num | numerator of rational. |
den | denominator of rational. |
Definition at line 1897 of file Context.java.
|
inline |
Create a real numeral.
v | A string representing the Term value in decimal notation. |
Definition at line 1911 of file Context.java.
|
inline |
Create a real numeral.
v | value of the numeral. |
Definition at line 1924 of file Context.java.
|
inline |
Create a real numeral.
v | value of the numeral. |
Definition at line 1937 of file Context.java.
Coerce a real to an integer. Remarks: The semantics of this function follows the SMT-LIB standard for the function to_int. The argument must be of real sort.
Definition at line 897 of file Context.java.
|
inline |
|
inline |
Create an expression representing
. Remarks: The arguments must have int type.
Definition at line 809 of file Context.java.
|
inline |
Bit-vector repetition. Remarks: The argument
must have a bit-vector sort.
Definition at line 1329 of file Context.java.
Array read. Remarks: The argument
is the array and
is the index of the array that gets read.
The node
must have an array sort
, and
must have the sort
. The sort of the result is
.
Definition at line 1629 of file Context.java.
Add an element to the set.
Definition at line 1748 of file Context.java.
Take the complement of a set.
Definition at line 1806 of file Context.java.
Remove an element from a set.
Definition at line 1760 of file Context.java.
Take the difference between two sets.
Definition at line 1794 of file Context.java.
|
inline |
Take the intersection of a list of sets.
Definition at line 1783 of file Context.java.
Check for set membership.
Definition at line 1816 of file Context.java.
Create a set type.
Definition at line 1719 of file Context.java.
Check for subsetness of sets.
Definition at line 1828 of file Context.java.
|
inline |
Take the union of a list of sets.
Definition at line 1772 of file Context.java.
|
inline |
Bit-vector sign extension. Remarks: Sign-extends the given bit-vector to the (signed) equivalent bitvector of size
, where m
is the size of the given bit-vector. The argument
must have a bit-vector sort.
Definition at line 1303 of file Context.java.
|
inline |
Creates a new (incremental) solver.
Definition at line 2773 of file Context.java.
|
inline |
Creates a new (incremental) solver. Remarks: This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.
Definition at line 2739 of file Context.java.
Referenced by Tactic.getSolver(), and Context.mkSolver().
Creates a new (incremental) solver. Remarks: This solver also uses a set of builtin tactics for handling the first check-sat command, and check-sat commands that take more than a given number of milliseconds to be solved.
Definition at line 2751 of file Context.java.
|
inline |
Creates a new (incremental) solver.
Definition at line 2765 of file Context.java.
Creates a solver that is implemented using the given tactic. Remarks: The solver supports the commands
and
, but it will always solve each check from scratch.
Definition at line 2784 of file Context.java.
Array update. Remarks: The node
must have an array sort
,
must have sort
,
must have sort range. The sort of the result is
. The semantics of this function is given by the theory of arrays described in the SMT-LIB standard. See http://smtlib.org for more details. The result of this function is an array that is equal to
(with respect to
) on all indices except for
, where it maps to
(and the
of
with respect to
may be a different value).
Definition at line 1655 of file Context.java.
|
inline |
|
inline |
Creates a new symbol using an integer. Remarks: Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.
Definition at line 72 of file Context.java.
Referenced by Params.add(), Context.mkArrayConst(), Context.mkBoolConst(), Context.mkConst(), Context.mkConstDecl(), Context.mkConstructor(), Context.mkDatatypeSort(), Context.mkEnumSort(), Context.mkFiniteDomainSort(), Context.mkFuncDecl(), Context.mkListSort(), Context.mkSolver(), Context.mkSymbol(), and Context.mkUninterpretedSort().
|
inline |
Create a symbol using a string.
Definition at line 80 of file Context.java.
|
inline |
Access the array default value. Remarks: Produces the default range value, for arrays that can be represented as finite maps with a default range value.
Definition at line 1709 of file Context.java.
|
inline |
The true Term.
Definition at line 620 of file Context.java.
Referenced by Goal.AsBoolExpr(), and Context.mkBool().
Create a new tuple sort.
Definition at line 194 of file Context.java.
|
inline |
Create a new uninterpreted sort.
Definition at line 143 of file Context.java.
Referenced by Context.mkUninterpretedSort().
|
inline |
Create a new uninterpreted sort.
Definition at line 152 of file Context.java.
|
inline |
Update a datatype field at expression t with value v. The function performs a record update at t. The field that is passed in as argument is updated with value v, the remainig fields of t are unchanged.
Definition at line 370 of file Context.java.
|
inline |
Bit-vector zero extension. Remarks: Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size
, where m
is the size of the given bit-vector. The argument
must have a bit-vector sort.
Definition at line 1317 of file Context.java.
Create a probe that evaluates to "true" when the value
does not evaluate to "true".
Definition at line 2726 of file Context.java.
Create a probe that evaluates to "true" when the value
or
evaluate to "true".
Definition at line 2715 of file Context.java.
Create a tactic that first applies
to a Goal and if it fails then returns the result of
applied to the Goal.
Definition at line 2442 of file Context.java.
Create a tactic that applies
to a given goal and then
to every subgoal produced by
. The subgoals are processed in parallel.
Definition at line 2575 of file Context.java.
|
inline |
Create a tactic that applies the given tactics in parallel.
Definition at line 2564 of file Context.java.
|
inline |
Parse the given file using the SMT-LIB2 parser.
Definition at line 2317 of file Context.java.
|
inline |
Parse the given string using the SMT-LIB2 parser.
Definition at line 2296 of file Context.java.
|
inline |
Parse the given file using the SMT-LIB parser.
Definition at line 2179 of file Context.java.
|
inline |
Parse the given string using the SMT-LIB parser. Remarks: The symbol table of the parser can be initialized using the given sorts and declarations. The symbols in the arrays
and
don't need to match the names of the sorts and declarations in the arrays
and
. This is a useful feature since we can use arbitrary names to reference sorts and declarations.
Definition at line 2160 of file Context.java.
Create a tactic that keeps applying
until the goal is not modified anymore or the maximum number of iterations
is reached.
Definition at line 2495 of file Context.java.
|
inline |
Selects the format used for pretty-printing expressions. Remarks: The default mode for pretty printing expressions is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called Z3_PRINT_SMTLIB_FULL. To print shared common subexpressions only once, use the Z3_PRINT_LOW_LEVEL mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions use Z3_PRINT_SMTLIB_COMPLIANT.
Definition at line 2123 of file Context.java.
Referenced by Context.updateParamValue().
|
inline |
Return a string describing all available parameters to
.
Definition at line 3615 of file Context.java.
|
inline |
Create a tactic that just returns the given goal.
Definition at line 2505 of file Context.java.
Create a tactic that applies
to a Goal and then
.
Remarks: Shorthand for
.
Definition at line 2432 of file Context.java.
Create a tactic that applies
to a goal for
milliseconds. Remarks: If
does not terminate within
milliseconds, then it fails.
Definition at line 2456 of file Context.java.
|
inline |
Unwraps an AST. Remarks: This function is used for transitions between native and managed objects. It returns the native pointer to the AST. Note that AST objects are reference counted and unwrapping an AST disables automatic reference counting, i.e., all references to the IntPtr that is returned must be handled externally and through native calls (see e.g.,
a | The AST to unwrap. |
Definition at line 3606 of file Context.java.
|
inline |
Update a mutable configuration parameter. Remarks: The list of all configuration parameters can be obtained using the Z3 executable:
Only a few configuration parameters are mutable once the context is created. An exception is thrown when trying to modify an immutable parameter.
Definition at line 3636 of file Context.java.
Create a tactic that applies
using the given set of parameters
.
Definition at line 2542 of file Context.java.
Referenced by Context.with().
Create a tactic that applies
to a given goal if the probe
evaluates to true. Remarks: If
evaluates to false, then the new tactic behaves like the
tactic.
Definition at line 2469 of file Context.java.
Create a tactic that applies
using the given set of parameters
. Remarks: Alias for
Definition at line 2556 of file Context.java.
|
inline |
Wraps an AST. Remarks: This function is used for transitions between native and managed objects. Note that
must be a native object obtained from Z3 (e.g., through
) and that it must have a correct reference count.
nativeObject | The native pointer to wrap. |
Definition at line 3589 of file Context.java.
|
protected |
Definition at line 3764 of file Context.java.
Referenced by Z3Object.dispose().