Protected Member Functions | |
Context (long m_ctx) | |
The main interaction with Z3 happens via the Context. For applications that spawn an unbounded number of contexts, the proper use is within a try-with-resources scope so that the Context object gets garbage collected in a predictable way. Contexts maintain all data-structures related to terms and formulas that are created relative to them.
Definition at line 36 of file Context.java.
|
inline |
Definition at line 40 of file Context.java.
|
inlineprotected |
Definition at line 47 of file Context.java.
|
inline |
Constructor. Remarks: The following parameters can be set:
Global.setParameter
Definition at line 72 of file Context.java.
Create a probe that evaluates to true
when the value p1
and p2
evaluate to true
.
Definition at line 3070 of file Context.java.
Create a tactic that applies t1
to a Goal and then t2
to every subgoal produced by t1
Definition at line 2766 of file Context.java.
|
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 2644 of file Context.java.
|
inline |
Disposes of the context.
Definition at line 4154 of file Context.java.
Create a tactic that applies t1
to a given goal if the probe p
evaluates to true and t2
otherwise.
Definition at line 2848 of file Context.java.
|
inline |
Create a probe that always evaluates to val
.
Definition at line 3000 of file Context.java.
Create a probe that evaluates to true
when the value returned by p1
is equal to the value returned by p2
Definition at line 3059 of file Context.java.
Referenced by AstRef.__eq__(), UserPropagateBase.add_eq(), SortRef.cast(), and BoolSortRef.cast().
|
inline |
Create a tactic always fails.
Definition at line 2879 of file Context.java.
Create a tactic that fails if the probe p
evaluates to false.
Definition at line 2888 of file Context.java.
|
inline |
Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains ‘false’).
Definition at line 2899 of file Context.java.
Create a probe that evaluates to true
when the value returned by p1
is greater than or equal the value returned by p2
Definition at line 3047 of file Context.java.
|
inline |
Definition at line 4085 of file Context.java.
|
inline |
Definition at line 4070 of file Context.java.
|
inline |
Definition at line 4075 of file Context.java.
|
inline |
Definition at line 4080 of file Context.java.
|
inline |
Retrieves the Boolean sort of the context.
Definition at line 128 of file Context.java.
|
inline |
Definition at line 4062 of file Context.java.
|
inline |
Definition at line 4066 of file Context.java.
|
inline |
Definition at line 4140 of file Context.java.
|
inline |
Definition at line 4090 of file Context.java.
|
inline |
Definition at line 4095 of file Context.java.
|
inline |
Definition at line 4100 of file Context.java.
|
inline |
Retrieves the Integer sort of the context.
Definition at line 139 of file Context.java.
|
inline |
Definition at line 4105 of file Context.java.
|
inline |
The number of supported Probes.
Definition at line 2962 of file Context.java.
|
inline |
The number of supported tactics.
Definition at line 2727 of file Context.java.
|
inline |
Definition at line 4145 of file Context.java.
|
inline |
Definition at line 4115 of file Context.java.
|
inline |
Definition at line 4110 of file Context.java.
|
inline |
Returns a string containing a description of the probe with the given name.
Definition at line 2984 of file Context.java.
|
inline |
Definition at line 4120 of file Context.java.
|
inline |
The names of all supported Probes.
Definition at line 2970 of file Context.java.
|
inline |
Retrieves the Real sort of the context.
Definition at line 150 of file Context.java.
|
inline |
Retrieves parameter descriptions for simplifier.
Definition at line 3989 of file Context.java.
|
inline |
Definition at line 4125 of file Context.java.
|
inline |
Definition at line 4130 of file Context.java.
|
inline |
Retrieves the Integer sort of the context.
Definition at line 169 of file Context.java.
|
inline |
Returns a string containing a description of the tactic with the given name.
Definition at line 2749 of file Context.java.
|
inline |
Definition at line 4135 of file Context.java.
|
inline |
The names of all supported tactics.
Definition at line 2735 of file Context.java.
Create a probe that evaluates to true
when the value returned by p1
is greater than the value returned by p2
Definition at line 3021 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 2954 of file Context.java.
|
inline |
Convert an integer expression to a string.
Definition at line 2017 of file Context.java.
Create a probe that evaluates to true
when the value returned by p1
is less than or equal the value returned by p2
Definition at line 3034 of file Context.java.
Create a probe that evaluates to true
when the value returned by p1
is less than the value returned by p2
Definition at line 3009 of file Context.java.
Create an expression representing t[0] + t[1] + ...
.
Definition at line 829 of file Context.java.
Create an expression representing t[0] and t[1] and ...
.
Definition at line 807 of file Context.java.
Referenced by Goal.AsBoolExpr().
Create a new function application.
Definition at line 692 of file Context.java.
Referenced by ListSort< R extends Sort >.getNil().
Create an at-least-k constraint.
Definition at line 2263 of file Context.java.
Create an at-most-k constraint.
Definition at line 2254 of file Context.java.
|
inline |
|
inline |
|
inline |
Create a Boolean constant.
Definition at line 627 of file Context.java.
|
inline |
Create a new Boolean sort.
Definition at line 161 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 2456 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 2466 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 2446 of file Context.java.
|
inline |
Create an integer from the bit-vector argument t
. 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 [0..2^N-1]
, where N are the number of bits in t
. 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 1567 of file Context.java.
|
inline |
Two's complement addition. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1130 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 1579 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 1593 of file Context.java.
|
inline |
Bitwise conjunction. Remarks: The arguments must have a bit-vector sort.
Definition at line 1041 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 1475 of file Context.java.
|
inline |
Creates a bit-vector constant.
Definition at line 683 of file Context.java.
|
inline |
Creates a bit-vector constant.
Definition at line 675 of file Context.java.
|
inline |
Logical shift right Remarks: It is equivalent to unsigned division by 2^x
where x
is the value of t2
.
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 1455 of file Context.java.
|
inline |
Two's complement multiplication. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1156 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 1661 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 1675 of file Context.java.
|
inline |
Bitwise NAND. Remarks: The arguments must have a bit-vector sort.
Definition at line 1080 of file Context.java.
|
inline |
Standard two's complement unary minus. Remarks: The arguments must have a bit-vector sort.
Definition at line 1119 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 1649 of file Context.java.
|
inline |
Bitwise NOR. Remarks: The arguments must have a bit-vector sort.
Definition at line 1093 of file Context.java.
|
inline |
Bitwise negation. Remarks: The argument must have a bit-vector sort.
Definition at line 1006 of file Context.java.
|
inline |
Bitwise disjunction. Remarks: The arguments must have a bit-vector sort.
Definition at line 1054 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 1017 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 1029 of file Context.java.
|
inline |
Rotate Left. Remarks: Rotate bits of t1
to the left t2
times. The arguments must have the same bit-vector sort.
Definition at line 1513 of file Context.java.
|
inline |
Rotate Left. Remarks: Rotate bits of t
to the left i
times. The argument t
must have a bit-vector sort.
Definition at line 1488 of file Context.java.
|
inline |
Rotate Right. Remarks: Rotate bits of t1
to the rightt2
times. The arguments must have the same bit-vector sort.
Definition at line 1528 of file Context.java.
|
inline |
Rotate Right. Remarks: Rotate bits of t
to the right i
times. The argument t
must have a bit-vector sort.
Definition at line 1500 of file Context.java.
|
inline |
Signed division. Remarks: It is defined in the following way:
floor
of t1/t2
if t2
is different from zero, and t1*t2 >= 0
.ceiling
of t1/t2
if t2
is different from zero, and t1*t2 < 0
.If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1192 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 1635 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 1317 of file Context.java.
|
inline |
Two's complement signed greater-than. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1343 of file Context.java.
|
inline |
Shift left. Remarks: It is equivalent to multiplication by 2^x
where x
is the value of t2
.
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 1436 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 1291 of file Context.java.
|
inline |
Two's complement signed less-than Remarks: The arguments must have the same bit-vector sort.
Definition at line 1265 of file Context.java.
|
inline |
Two's complement signed remainder (sign follows divisor). Remarks: If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1239 of file Context.java.
|
inline |
Signed remainder. Remarks: It is defined as t1 - (t1 /s t2) * t2
, where /s
represents signed division. The most significant bit (sign) of the result is equal to the most significant bit of t1
.
If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1225 of file Context.java.
|
inline |
Two's complement subtraction. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1143 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 1607 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 1621 of file Context.java.
|
inline |
Unsigned division. Remarks: It is defined as the floor of t1/t2
if t2
is different from zero. If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1171 of file Context.java.
|
inline |
Unsigned greater than or equal to. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1304 of file Context.java.
|
inline |
Unsigned greater-than. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1330 of file Context.java.
|
inline |
Unsigned less-than or equal to. Remarks: The arguments must have the same bit-vector sort.
Definition at line 1278 of file Context.java.
|
inline |
Unsigned less-than Remarks: The arguments must have the same bit-vector sort.
Definition at line 1252 of file Context.java.
|
inline |
Unsigned remainder. Remarks: It is defined as t1 - (t1 /u t2) * t2
, where /u
represents unsigned division. If t2
is zero, then the result is undefined. The arguments must have the same bit-vector sort.
Definition at line 1207 of file Context.java.
|
inline |
Bitwise XNOR. Remarks: The arguments must have a bit-vector sort.
Definition at line 1106 of file Context.java.
|
inline |
Bitwise XOR. Remarks: The arguments must have a bit-vector sort.
Definition at line 1067 of file Context.java.
|
inline |
Bit-vector concatenation. Remarks: The arguments must have a bit-vector sort.
n1+n2
, where n1
(n2
) is the size of t1
(t2
). Definition at line 1361 of file Context.java.
Concatenate sequences.
Definition at line 2034 of file Context.java.
Create the concatenation of regular languages.
Definition at line 2199 of file Context.java.
|
inline |
Create mutually recursive data-types.
Definition at line 413 of file Context.java.
|
inline |
Create mutually recursive datatypes.
names | names of datatype sorts |
c | list of constructors, one list per sort. |
Definition at line 387 of file Context.java.
Creates a distinct
term.
Definition at line 738 of file Context.java.
Creates the equality x = y
Definition at line 726 of file Context.java.
|
inline |
Creates an existential quantifier using a list of constants that will form the set of bound variables.
Definition at line 2534 of file Context.java.
|
inline |
Creates an existential quantifier using de-Bruijn indexed variables.
Definition at line 2521 of file Context.java.
|
inline |
Bit-vector extraction. Remarks: Extract the bits high
down to low
from a bitvector of size m
to yield a new bitvector of size n
, where n = high - low + 1
. The argument t
must have a bit-vector sort.
Definition at line 1377 of file Context.java.
|
inline |
The false Term.
Definition at line 710 of file Context.java.
|
inline |
Create a Fixedpoint context.
Definition at line 3160 of file Context.java.
|
inline |
Creates a universal quantifier using a list of constants that will form the set of bound variables.
Definition at line 2508 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. |
weight
is the weight, patterns
is an array of patterns, sorts
is an array with the sorts of the bound variables, names
is an array with the 'names' of the bound variables, and body
is the body of the quantifier. Quantifiers are associated with weights indicating the importance of using the quantifier during instantiation. Note that the bound variables are de-Bruijn indices created using mkBound
. Z3 applies the convention that the last element in names
and sorts
refers to the variable with index 0, the second to last element of names
and sorts
refers to the variable with index 1, etc. Definition at line 2496 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 3490 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 3503 of file Context.java.
Create a numeral of FloatingPoint sort from a double.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3465 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 3788 of file Context.java.
Create a numeral of FloatingPoint sort from a float.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3454 of file Context.java.
Create a numeral of FloatingPoint sort from an int.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3477 of file Context.java.
Floating-point absolute value
t | floating-point term |
Z3Exception |
Definition at line 3514 of file Context.java.
Floating-point addition
rm | rounding mode term |
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3536 of file Context.java.
Floating-point division
rm | rounding mode term |
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3572 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 3700 of file Context.java.
|
inline |
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 3587 of file Context.java.
Floating-point greater than or equal.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3676 of file Context.java.
Floating-point greater than.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3687 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 3373 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 3740 of file Context.java.
Predicate indicating whether t is a NaN.
t | floating-point term |
Z3Exception |
Definition at line 3750 of file Context.java.
Predicate indicating whether t is a negative floating-point number.
t | floating-point term |
Z3Exception |
Definition at line 3760 of file Context.java.
Predicate indicating whether t is a normal floating-point number.\
t | floating-point term |
Z3Exception |
Definition at line 3710 of file Context.java.
Predicate indicating whether t is a positive floating-point number.
t | floating-point term |
Z3Exception |
Definition at line 3770 of file Context.java.
Predicate indicating whether t is a subnormal floating-point number.\
t | floating-point term |
Z3Exception |
Definition at line 3720 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 3730 of file Context.java.
Floating-point less than or equal.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3654 of file Context.java.
Floating-point less than.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3665 of file Context.java.
Maximum of floating-point numbers.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3643 of file Context.java.
Minimum of floating-point numbers.
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3632 of file Context.java.
Floating-point multiplication
rm | rounding mode term |
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3560 of file Context.java.
Create a NaN of sort s.
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3362 of file Context.java.
Floating-point negation
t | floating-point term |
Z3Exception |
Definition at line 3524 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 3430 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 3443 of file Context.java.
Create a numeral of FloatingPoint sort from a double.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3406 of file Context.java.
Create a numeral of FloatingPoint sort from a float.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3395 of file Context.java.
Create a numeral of FloatingPoint sort from an int.
v | numeral value. |
s | FloatingPoint sort. |
Z3Exception |
Definition at line 3417 of file Context.java.
Floating-point remainder
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3609 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Z3Exception |
Definition at line 3214 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3Exception |
Definition at line 3196 of file Context.java.
|
inline |
Create the floating-point RoundingMode sort.
Z3Exception |
Definition at line 3178 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
Z3Exception |
Definition at line 3205 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
Z3Exception |
Definition at line 3187 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 3621 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Z3Exception |
Definition at line 3241 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Z3Exception |
Definition at line 3223 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Z3Exception |
Definition at line 3259 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardNegative rounding mode.
Z3Exception |
Definition at line 3250 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardPositive rounding mode.
Z3Exception |
Definition at line 3232 of file Context.java.
|
inline |
Create a numeral of RoundingMode sort which represents the RoundTowardZero rounding mode.
Z3Exception |
Definition at line 3268 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 3279 of file Context.java.
|
inline |
Create the quadruple-precision (128-bit) FloatingPoint sort.
Z3Exception |
Definition at line 3351 of file Context.java.
|
inline |
Create the half-precision (16-bit) FloatingPoint sort.
Z3Exception |
Definition at line 3297 of file Context.java.
|
inline |
Create the single-precision (32-bit) FloatingPoint sort.
Z3Exception |
Definition at line 3315 of file Context.java.
|
inline |
Create the double-precision (64-bit) FloatingPoint sort.
Z3Exception |
Definition at line 3333 of file Context.java.
|
inline |
Create the double-precision (64-bit) FloatingPoint sort.
Z3Exception |
Definition at line 3324 of file Context.java.
|
inline |
Create the half-precision (16-bit) FloatingPoint sort.
Z3Exception |
Definition at line 3288 of file Context.java.
|
inline |
Create the quadruple-precision (128-bit) FloatingPoint sort.
Z3Exception |
Definition at line 3342 of file Context.java.
|
inline |
Create the single-precision (32-bit) FloatingPoint sort.
Z3Exception |
Definition at line 3306 of file Context.java.
Floating-point square root
rm | rounding mode term |
t | floating-point term |
Z3Exception |
Definition at line 3598 of file Context.java.
Floating-point subtraction
rm | rounding mode term |
t1 | floating-point term |
t2 | floating-point term |
Z3Exception |
Definition at line 3548 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-point 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 3889 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 3804 of file Context.java.
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 3854 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 3939 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 3820 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 3836 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 3872 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 representation of that NaN. |
Z3Exception |
Definition at line 3921 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-point 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 3906 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 3384 of file Context.java.
Create an expression representing t1 >= t2
Definition at line 955 of file Context.java.
|
inline |
Creates a new Goal. Remarks: Note that the Context must have been created with proof generation support if proofs
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 2711 of file Context.java.
Create an expression representing t1 > t2
Definition at line 944 of file Context.java.
Create an expression representing t1 iff t2
.
Definition at line 773 of file Context.java.
Create an expression representing t1 -> t2
.
Definition at line 784 of file Context.java.
|
inline |
Create an integer numeral.
v | value of the numeral. |
v
and sort Integer Definition at line 2421 of file Context.java.
|
inline |
Create an integer numeral.
v | value of the numeral. |
v
and sort Integer Definition at line 2434 of file Context.java.
|
inline |
Create an integer numeral.
v | A string representing the Term value in decimal notation. |
Definition at line 2408 of file Context.java.
|
inline |
Create an n
bit bit-vector from the integer argument t
. 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 1546 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 k
and asserting MakeInt2Real(k) <= t1 < MkInt2Real(k)+1
. The argument must be of integer sort.
Definition at line 973 of file Context.java.
|
inline |
Creates an integer constant.
Definition at line 651 of file Context.java.
Creates an integer constant.
Definition at line 643 of file Context.java.
Create the intersection of regular languages.
Definition at line 2219 of file Context.java.
|
inline |
Create a new integer sort.
Definition at line 197 of file Context.java.
Creates an expression that checks whether a real number is an integer.
Definition at line 995 of file Context.java.
Create an expression representing t1 <= t2
Definition at line 933 of file Context.java.
Create an expression representing t1 < t2
Definition at line 922 of file Context.java.
|
inline |
Maps f on the argument arrays. Remarks: Each element of args
must be of an array sort [domain_i -> range_i]
. The function declaration f
must have type range_1 .. range_n -> range
. v
must have sort range. The sort of the result is [domain_i -> range]
.
Definition at line 1827 of file Context.java.
Create an expression representing t1 mod t2
. Remarks: The arguments must have int type.
Definition at line 884 of file Context.java.
Create an expression representing t[0] * t[1] * ...
.
Definition at line 840 of file Context.java.
Create an expression representing not(a)
.
Definition at line 748 of file Context.java.
|
inline |
Create a Optimize context.
Definition at line 3168 of file Context.java.
Create an expression representing t[0] or t[1] or ...
.
Definition at line 818 of file Context.java.
|
inline |
Creates a new ParameterSet.
Definition at line 2719 of file Context.java.
Create a quantifier pattern.
Definition at line 570 of file Context.java.
Create a pseudo-Boolean equal constraint.
Definition at line 2290 of file Context.java.
Create a pseudo-Boolean greater-or-equal constraint.
Definition at line 2281 of file Context.java.
Create a pseudo-Boolean less-or-equal constraint.
Definition at line 2272 of file Context.java.
|
inline |
Creates a new Probe.
Definition at line 2992 of file Context.java.
|
inline |
Create a Quantifier
Definition at line 2565 of file Context.java.
|
inline |
Create a Quantifier.
Definition at line 2547 of file Context.java.
|
inline |
Create a real from a fraction.
num | numerator of rational. |
den | denominator of rational. |
num
/den
and sort Real Definition at line 2356 of file Context.java.
|
inline |
Create a real numeral.
v | value of the numeral. |
v
and sort Real Definition at line 2384 of file Context.java.
|
inline |
Create a real numeral.
v | value of the numeral. |
v
and sort Real Definition at line 2397 of file Context.java.
|
inline |
Create a real numeral.
v | A string representing the Term value in decimal notation. |
v
and sort Real Definition at line 2371 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 986 of file Context.java.
|
inline |
Creates a real constant.
Definition at line 667 of file Context.java.
Creates a real constant.
Definition at line 659 of file Context.java.
|
inline |
Create a real sort.
Definition at line 205 of file Context.java.
Create an expression representing t1 rem t2
. Remarks: The arguments must have int type.
Definition at line 897 of file Context.java.
|
inline |
Bit-vector repetition. Remarks: The argument t
must have a bit-vector sort.
Definition at line 1418 of file Context.java.
|
inline |
Take the intersection of a list of sets.
Definition at line 1929 of file Context.java.
|
inline |
Take the union of a list of sets.
Definition at line 1917 of file Context.java.
|
inline |
Bit-vector sign extension. Remarks: Sign-extends the given bit-vector to the (signed) equivalent bitvector of size m+i
, where m
is the size of the given bit-vector. The argument t
must have a bit-vector sort.
Definition at line 1392 of file Context.java.
|
inline |
Creates a new (incremental) solver.
Definition at line 3139 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 3105 of file Context.java.
Referenced by Tactic.getSolver().
|
inline |
Creates a new (incremental) solver.
Definition at line 3131 of file Context.java.
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 3117 of file Context.java.
Creates a solver that is implemented using the given tactic. Remarks: The solver supports the commands Push
and Pop
, but it will always solve each check from scratch.
Definition at line 3150 of file Context.java.
|
inline |
Create a string constant.
Definition at line 2009 of file Context.java.
|
inline |
Create a new string sort
Definition at line 242 of file Context.java.
Create an expression representing t[0] - t[1] - ...
.
Definition at line 851 of file Context.java.
|
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 94 of file Context.java.
|
inline |
Create a symbol using a string.
Definition at line 102 of file Context.java.
|
inline |
Creates a new Tactic.
Definition at line 2757 of file Context.java.
Referenced by Goal.simplify().
|
inline |
Create a new tuple sort.
Definition at line 267 of file Context.java.
|
inline |
Create a new uninterpreted sort.
Definition at line 189 of file Context.java.
|
inline |
Create a new uninterpreted sort.
Definition at line 180 of file Context.java.
Create the union of regular languages.
Definition at line 2209 of file Context.java.
Create an expression representing t1 xor t2
.
Definition at line 795 of file Context.java.
|
inline |
Bit-vector zero extension. Remarks: Extend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i
, where m
is the size of the given bit-vector. The argument t
must have a bit-vector sort.
Definition at line 1406 of file Context.java.
|
inline |
Definition at line 4008 of file Context.java.
Referenced by ASTVector.ASTVector(), ConstructorDecRefQueue.decRef(), ConstructorListDecRefQueue.decRef(), AST.equals(), FuncDecl< R extends Sort >.equals(), Sort.equals(), FPRMSort.FPRMSort(), FPSort.FPSort(), Quantifier.of(), Lambda< R extends Sort >.of(), ASTVector.set(), AST.translate(), ASTVector.translate(), Goal.translate(), and Solver.translate().
Create a probe that evaluates to true
when the value p
does not evaluate to true
.
Definition at line 3092 of file Context.java.
Create a probe that evaluates to true
when the value p1
or p2
evaluate to true
.
Definition at line 3081 of file Context.java.
Create a tactic that first applies t1
to a Goal and if it fails then returns the result of t2
applied to the Goal.
Definition at line 2808 of file Context.java.
Create a tactic that applies t1
to a given goal and then t2
to every subgoal produced by t1
. The subgoals are processed in parallel.
Definition at line 2941 of file Context.java.
|
inline |
Create a tactic that applies the given tactics in parallel until one of them succeeds (i.e., the first that doesn't fail).
Definition at line 2930 of file Context.java.
|
inline |
Parse the given file using the SMT-LIB2 parser.
Definition at line 2684 of file Context.java.
|
inline |
Parse the given string using the SMT-LIB2 parser.
If the string contains push/pop commands, the set of assertions returned are the ones in the last scope level.
Definition at line 2663 of file Context.java.
Create a tactic that keeps applying t
until the goal is not modified anymore or the maximum number of iterations max
is reached.
Definition at line 2861 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 2626 of file Context.java.
|
inline |
Return a string describing all available parameters to Expr.Simplify
.
Definition at line 3981 of file Context.java.
|
inline |
Create a tactic that just returns the given goal.
Definition at line 2871 of file Context.java.
|
inline |
Convert an integer expression to a string.
Definition at line 2025 of file Context.java.
Create a tactic that applies t1
to a Goal and then t2
to every subgoal produced by t1
Remarks: Shorthand for AndThen
.
Definition at line 2798 of file Context.java.
Create a tactic that applies t
to a goal for ms
milliseconds. Remarks: If t
does not terminate within ms
milliseconds, then it fails.
Definition at line 2822 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 3972 of file Context.java.
|
inline |
Update a mutable configuration parameter. Remarks: The list of all configuration parameters can be obtained using the Z3 executable: z3.exe -ini?
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 4002 of file Context.java.
Create a tactic that applies t
using the given set of parameters p
.
Definition at line 2908 of file Context.java.
Create a tactic that applies t
to a given goal if the probe p
evaluates to true. Remarks: If p
evaluates to false, then the new tactic behaves like the skip
tactic.
Definition at line 2835 of file Context.java.
Create a tactic that applies t
using the given set of parameters p
. Remarks: Alias for UsingParams
Definition at line 2922 of file Context.java.
|
inline |
Wraps an AST. Remarks: This function is used for transitions between native and managed objects. Note that nativeObject
must be a native object obtained from Z3 (e.g., through UnwrapAST
) and that it must have a correct reference count.
nativeObject | The native pointer to wrap. |
Definition at line 3955 of file Context.java.