Z3Context
public class Z3Context
Main interaction point to Z3.
-
Gets or sets a reference to a rounding mode for floating-point operations performed on
Z3FloatingPoint
instances created by this context.Changes to this value change the rounding mode that is passed to the underlying
Z3_mk_fpa_*
methods that are generated via overloaded operators onZ3FloatingPoint
instances.Defaults to NearestTiesToEven rounding mode, if not configured.
Declaration
Swift
public var currentFpaRoundingMode: Z3RoundingMode { get set }
-
Return the error code for the last API call.
Declaration
Swift
public var errorCode: Z3ErrorCode { get }
-
Return
true
if the last API call resulted in an error.Declaration
Swift
public var hasError: Bool { get }
-
Return the number of builtin probes available in Z3.
Declaration
Swift
public var probeCount: UInt32 { get }
-
Return the number of builtin tactics available in Z3.
Declaration
Swift
public var tacticCount: UInt32 { get }
-
Declaration
Swift
public init(configuration: Z3Config? = nil)
-
Return a string describing the given error code.
Declaration
Swift
public func errorMessage(_ code: Z3ErrorCode) -> String
-
Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.
Declaration
Swift
public func interrupt()
-
Create a Z3 (empty) parameter set.
Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.
Declaration
Swift
public func makeParams() -> Z3Params
-
Create a new optimize context.
Declaration
Swift
public func makeOptimize() -> Z3Optimize
-
Return a string describing all available parameters.
Seealso
simplifyEx
Seealso
getSimplifyParamDescrs
Declaration
Swift
public func getSimplifyHelp() -> String
-
Return the parameter description set for the simplify procedure.
Seealso
simplifyEx
Seealso
getSimplifyHelp
Declaration
Swift
public func getSimplifyParamDescrs() -> Z3ParamDescrs
-
Interface to simplifier.
Provides an interface to the AST simplifier used by Z3. It returns an AST object which is equal to the argument. The returned AST is simplified using algebraic simplification rules, such as constant propagation (propagating true/false over logical connectives).
Seealso
simplifyEx
-
Interface to simplifier.
Provides an interface to the AST simplifier used by Z3. This procedure is similar to #Z3_simplify, but the behavior of the simplifier can be configured using the given parameter set.
Seealso
simplify
Seealso
getSimplifyHelp
Seealso
getSimplifyParamDescrs
-
Select mode for the format used for pretty-printing AST nodes.
The default mode for pretty printing AST nodes is to produce SMT-LIB style output where common subexpressions are printed at each occurrence. The mode is called
Z3AstPrintMode.printSmtlibFull
. To print shared common subexpressions only once, use theZ3AstPrintMode.printLowLevel
mode. To print in way that conforms to SMT-LIB standards and uses let expressions to share common sub-expressions useZ3AstPrintMode.printSmtlib2Compliant
.Declaration
Swift
public func setAstPrintMode(_ mode: Z3AstPrintMode)
-
Convert the given benchmark into SMT-LIB formatted string.
Declaration
Parameters
name
- name of 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.
num_assumptions
- number of assumptions.
assumptions
- auxiliary assumptions.
formula
- formula to be checked for consistency in conjunction with assumptions.
-
Return
Z3_INT_SYMBOL
if the symbol was constructed usingmakeIntSymbol
, andZ3_STRING_SYMBOL
if the symbol was constructed usingmakeStringSymbol
.Declaration
Swift
func getSymbolKind(_ symbol: Z3Symbol) -> Z3_symbol_kind
-
Return the symbol int value.
Precondition
getSymbolKind(s) == Z3_INT_SYMBOL
Declaration
Swift
func getSymbolInt(_ symbol: Z3Symbol) -> Int32
-
Return the symbol name.
Precondition
getSymbolKind(s) == Z3_STRING_SYMBOL
Seealso
makeStringSymbol
Declaration
Swift
func getSymbolString(_ symbol: Z3Symbol) -> String
-
Return the sort kind (e.g., array, tuple, int, bool, etc).
Seealso
Z3_sort_kind
Declaration
Swift
func getSortKind(_ sort: Z3Sort) -> Z3_sort_kind
-
Return the size of the given bit-vector sort.
Precondition
getSortKind(t) == Z3_BV_SORT
Seealso
makeBvSort
Seealso
getSortKind
Declaration
Swift
func getBvSortSize(_ sort: Z3Sort) -> UInt32
-
Returns
true
ifast
can be used as value in the Z3 real algebraic number package.Declaration
Swift
func algebraicIsValue(_ ast: Z3AstBase) -> Bool
-
Returns
true
ifast
is positive,false
otherwise.Declaration
Swift
func algebraicIsPos(_ ast: Z3Algebraic) -> Bool
-
Returns
true
ifast
is negative,false
otherwise.Declaration
Swift
func algebraicIsNeg(_ ast: Z3Algebraic) -> Bool
-
Returns
true
ifast
is zero,false
otherwise.Declaration
Swift
func algebraicIsZero(_ ast: Z3Algebraic) -> Bool
-
Returns
1
ifast
is positive,0
ifast
is zero, and-1
if it is negative.Declaration
Swift
func algebraicSign(_ ast: Z3Algebraic) -> Int
-
Return the value lhs + rhs.
Declaration
Swift
func algebraicAdd(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Z3Algebraic
-
Return the value lhs - rhs.
Declaration
Swift
func algebraicSub(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Z3Algebraic
-
Return the value lhs * rhs.
Declaration
Swift
func algebraicMul(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Z3Algebraic
-
Return the value lhs / rhs.
Declaration
Swift
func algebraicDiv(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Z3Algebraic
-
Return the ast^(1/k)
Declaration
Swift
func algebraicRoot(_ ast: Z3Algebraic, _ k: UInt32) -> Z3Algebraic
-
Return the ast^k
Declaration
Swift
func algebraicPower(_ ast: Z3Algebraic, _ k: UInt32) -> Z3Algebraic
-
Return
true
iflhs < rhs
,false
otherwise.Declaration
Swift
func algebraicLt(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs > rhs
,false
otherwise.Declaration
Swift
func algebraicGt(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs <= rhs
,false
otherwise.Declaration
Swift
func algebraicLe(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs >= rhs
,false
otherwise.Declaration
Swift
func algebraicGe(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs == rhs
,false
otherwise.Declaration
Swift
func algebraicEq(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Bool
-
Return
true
iflhs != rhs
,false
otherwise.Declaration
Swift
func algebraicNeq(_ lhs: Z3Algebraic, _ rhs: Z3Algebraic) -> Bool
-
Given a multivariate polynomial
polynomial(x_0, ..., x_{n-1}, x_n)
, returns the roots of the univariate polynomialpolynomial(a[0], ..., a[n-1], x_n)
.Precondition
polynomial
is a Z3 expression that contains only arithmetic terms and free variables.Declaration
Swift
func algebraicRoots(_ polynomial: Z3Algebraic, _ a: [Z3Algebraic]) -> Z3AstVector
-
Given a multivariate polynomial
polynomial(x_0, ..., x_{n-1})
, return the sign ofpolynomial(a[0], ..., a[n-1])
.Precondition
polynomial
is a Z3 expression that contains only arithmetic terms and free variables.Declaration
Swift
func algebraicEval(_ polynomial: Z3Algebraic, _ a: [Z3Algebraic]) -> Int
-
Return the coefficients of the defining polynomial.
Declaration
Swift
func algebraicGetPoly(_ polynomial: Z3Algebraic) -> Z3AstVector
-
Return which root of the polynomial the algebraic number represents.
Declaration
Swift
func algebraicGetI(_ polynomial: Z3Algebraic) -> UInt32
-
Create an AST node representing
args[0] + ... + args[num_args-1]
.All arguments must have int or real sort.
Remark
The number of arguments must be greater than zero.Declaration
Swift
func makeAdd<T>(_ arguments: [Z3Ast<T>]) -> Z3Ast<T> where T : ArithmeticSort
-
Create an AST node representing
args[0] * ... * args[num_args-1]
.All arguments must have int or real sort.
Remark
Z3 has limited support for non-linear arithmetic.Remark
The number of arguments must be greater than zero.Declaration
Swift
func makeMul<T>(_ arguments: [Z3Ast<T>]) -> Z3Ast<T> where T : ArithmeticSort
-
Create an AST node representing
args[0] + ... + args[num_args-1]
.All arguments must have int or real sort.
Remark
The number of arguments must be greater than zero.Declaration
Swift
func makeSub<T>(_ arguments: [Z3Ast<T>]) -> Z3Ast<T> where T : ArithmeticSort
-
Create an AST node representing
- arg
. The arguments must have int or real type.Declaration
Swift
func makeUnaryMinus<T>(_ ast: Z3Ast<T>) -> Z3Ast<T> where T : ArithmeticSort
-
Create an AST node representing
arg1 div arg2
.The arguments must either both have int type or both have real type. If the arguments have int type, then the result type is an int type, otherwise the the result type is real.
Declaration
Swift
func makeDiv<T>(_ arg1: Z3Ast<T>, _ arg2: Z3Ast<T>) -> Z3Ast<T> where T : ArithmeticSort
-
Create an AST node representing
arg1 ^ arg2
.The arguments must have int or real type.
Declaration
Swift
func makePower<T>(_ arg1: Z3Ast<T>, _ arg2: Z3Ast<T>) -> Z3Ast<T> where T : ArithmeticSort
-
Create less than. The nodes
t1
andt2
must have the same sort, and must be int or real.Declaration
Swift
func makeLessThan<T>(_ t1: Z3Ast<T>, _ t2: Z3Ast<T>) -> Z3Bool where T : ArithmeticSort
-
Create less than or equal to. The nodes
t1
andt2
must have the same sort, and must be int or real.Declaration
Swift
func makeLessThanOrEqualTo<T>(_ t1: Z3Ast<T>, _ t2: Z3Ast<T>) -> Z3Bool where T : ArithmeticSort
-
Create greater than. The nodes
t1
andt2
must have the same sort, and must be int or real.Declaration
Swift
func makeGreaterThan<T>(_ t1: Z3Ast<T>, _ t2: Z3Ast<T>) -> Z3Bool where T : ArithmeticSort
-
Create greater than or equal to. The nodes
t1
andt2
must have the same sort, and must be int or real.Declaration
Swift
func makeGreaterThanOrEqualTo<T>(_ t1: Z3Ast<T>, _ t2: Z3Ast<T>) -> Z3Bool where T : ArithmeticSort
-
Coerce an integer to a real.
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 constant
k
and and assertingmk_int2real(k) <= t1 < mk_int2real(k)+1
.The node
t1
must have sort integer.Seealso
makeReal2Int
Seealso
makeIsInt
-
Coerce an integer to a float.
Declaration
Swift
func makeIntToFloat<T>(_ t1: Z3Int, sort: T.Type) -> Z3Ast<T> where T : FloatingSort
-
Array read.
The argument
a
is the array andi
is the index of the array that gets read.The node
a
must have an array sort[domain -> range]
, andi
must have the sortdomain
. The sort of the result isrange
.makeArraySort
makeStore
-
Array read.
Type-erased version.
The argument
a
is the array andi
is the index of the array that gets read.The node
a
must have an array sort[domain -> range]
, andi
must have the sortdomain
. The sort of the result isrange
.makeArraySort
makeStore
-
Array update.
The node
a
must have an array sort[domain -> range]
,i
must have sortdomain
,v
must have sort range. The sort of the result is[domain -> range]
. 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 toa
(with respect toselect
) on all indices except fori
, where it maps tov
(and theselect
ofa
with respect toi
may be a different value). -
Array update.
Type-erased version.
The node
a
must have an array sort[domain -> range]
,i
must have sortdomain
,v
must have sort range. The sort of the result is[domain -> range]
. 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 toa
(with respect toselect
) on all indices except fori
, where it maps tov
(and theselect
ofa
with respect toi
may be a different value). -
Map f on the argument arrays.
The
n
nodesargs
must be of array sorts[domain_i -> range_i]
. The function declarationf
must have typerange_1 .. range_n -> range
.v
must have sort range. The sort of the result is[domain_i -> range]
.Seealso
makeArraySort
Seealso
makeStore
Seealso
makeSelect
Declaration
Swift
func makeMap(_ f: Z3FuncDecl, args: [AnyZ3Ast]) -> AnyZ3Ast
-
Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.
Declaration
Parameters
array
array value whose default range value is accessed.
-
Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.
Type-erased version.
Parameters
array
array value whose default range value is accessed.
-
Create array with the same interpretation as a function. The array satisfies the property
(f x) = (select (_ as-array f) x)
for every argumentx
.Declaration
Swift
func makeAsArray(_ f: Z3FuncDecl) -> AnyZ3Ast
-
Creates a bit vector out of a given integer value.
Declaration
Swift
func makeBitVector<T>(_ value: Int32) -> Z3BitVector<T> where T : BitVectorSort
-
Creates a bit vector out of a given integer value.
Declaration
Swift
func makeBitVectorAny(_ value: Int32, bitWidth: UInt32) -> AnyZ3Ast
-
Bitwise negation.
The node
t1
must have a bit-vector sort.Declaration
Swift
func makeBvNot<T>(_ t1: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Take conjunction of bits in vector, return vector of length 1.
The node
t1
must have a bit-vector sort.Declaration
Swift
func makeBvRedAnd<T>(_ t1: Z3BitVector<T>) -> Z3BitVector<BitVectorSort1> where T : BitVectorSort
-
Take disjunction of bits in vector, return vector of length 1.
The node
t1
must have a bit-vector sort.Declaration
Swift
func makeBvRedOr<T>(_ t1: Z3BitVector<T>) -> Z3BitVector<BitVectorSort1> where T : BitVectorSort
-
Bitwise and.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvAnd<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Bitwise or.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvOr<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Bitwise exclusive-or.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvXor<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Bitwise nand.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvNand<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Bitwise nor.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvNor<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Bitwise xnor.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvXnor<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Standard two’s complement unary minus.
The node
t1
must have bit-vector sort.Declaration
Swift
func makeBvNeg<T>(_ t1: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Standard two’s complement addition.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvAdd<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Standard two’s complement subtraction.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvSub<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Standard two’s complement multiplication.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvMul<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Unsigned division.
It is defined as the
floor
oft1/t2
ift2
is different from zero. Ift2
is zero, then the result is undefined.Declaration
Swift
func makeBvDiv<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Two’s complement signed division.
It is defined in the following way:
The
floor
oft1/t2
ift2
is different from zero, andt1*t2 >= 0
.The
ceiling
oft1/t2
ift2
is different from zero, andt1*t2 < 0
.
If
t2
is zero, then the result is undefined.The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvSDiv<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Unsigned remainder.
It is defined as
t1 - (t1 /u t2) * t2
, where/u
represents unsigned division.If
t2
is zero, then the result is undefined.The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvURem<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Two’s complement signed remainder (sign follows dividend).
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 oft1
.If
t2
is zero, then the result is undefined.The nodes
t1
andt2
must have the same bit-vector sort.Seealso
makeBvSMod
Declaration
Swift
func makeBvSRem<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Two’s complement signed remainder (sign follows divisor).
If
t2
is zero, then the result is undefined.The nodes
t1
andt2
must have the same bit-vector sort.Seealso
makeBvSRem
Declaration
Swift
func makeBvSMod<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Unsigned less than.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvUlt<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Two’s complement signed less than.
It abbreviates:
(or (and (= (extract[|m-1|:|m-1|] t1) bit1) (= (extract[|m-1|:|m-1|] t2) bit0)) (and (= (extract[|m-1|:|m-1|] t1) (extract[|m-1|:|m-1|] t2)) (bvult t1 t2)))
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvSlt<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Unsigned less than or equal to.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvUle<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Two’s complement signed less than or equal to.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvSle<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Unsigned greater than or equal to.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvUge<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Two’s complement signed greater than or equal to.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvSge<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Unsigned greater than.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvUgt<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Two’s complement signed greater than.
The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvSgt<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Concatenate the given bit-vectors.
The nodes
t1
andt2
must have (possibly different) bit-vector sortsThe result is a bit-vector of size
n1+n2
, wheren1
(n2
) is the size oft1
(t2
).Declaration
Swift
func makeConcat<T, U>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<U>) -> AnyZ3BitVector where T : BitVectorSort, U : BitVectorSort
-
Extract the bits
high
down tolow
from a bit-vector of sizem
to yield a new bit-vector of sizen
, wheren = high - low + 1
.The node
t1
must have a bit-vector sort.Declaration
Swift
func makeExtract<T>(high: UInt32, low: UInt32, _ t1: Z3BitVector<T>) -> AnyZ3BitVector where T : BitVectorSort
-
Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size
m+i
, wherem
is the size of the given bit-vector.The node
t1
must have a bit-vector sort.Declaration
Swift
func makeSignExtend<T>(_ i: UInt32, _ t1: Z3BitVector<T>) -> AnyZ3BitVector where T : BitVectorSort
-
Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size
m+i
, wherem
is the size of the given bit-vector.The node
t1
must have a bit-vector sort.Declaration
Swift
func makeZeroExtend<T>(_ i: UInt32, _ t1: Z3BitVector<T>) -> AnyZ3BitVector where T : BitVectorSort
-
Repeat the given bit-vector up length
i
.The node
t1
must have a bit-vector sort.Declaration
Swift
func makeRepeat<T>(_ i: UInt32, _ t1: Z3BitVector<T>) -> AnyZ3BitVector where T : BitVectorSort
-
Shift left.
It is equivalent to multiplication by
2^x
wherex
is the value 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 nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvShl<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Logical shift right.
It is equivalent to unsigned division by
2^x
wherex
is the value 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 nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvLShr<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Arithmetic shift right.
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.
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 nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeBvAShr<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Rotate bits of
t1
to the lefti
times.The node
t1
must have a bit-vector sort.Declaration
Swift
func makeRotateLeft<T>(_ i: UInt32, _ t1: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Rotate bits of
t1
to the righti
times.The node
t1
must have a bit-vector sort.Declaration
Swift
func makeRotateRight<T>(_ i: UInt32, _ t1: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Rotate bits of
t1
to the leftt2
times.The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeExtRotateLeft<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Rotate bits of
t1
to the rightt2
times.The nodes
t1
andt2
must have the same bit-vector sort.Declaration
Swift
func makeExtRotateRight<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3BitVector<T> where T : BitVectorSort
-
Create an
n
bit bit-vector from the integer argumentt1
.The resulting bit-vector has
n
bits, where the i'th bit (counting from 0 ton-1
) is 1 if(t1 div 2^i)
mod 2 is 1.The node
t1
must have integer sort.Declaration
Swift
func makeIntToBv(_ n: UInt32, _ t1: Z3Int) -> AnyZ3BitVector
-
Create an integer from the bit-vector argument
t1
.If
isSigned
is false, then the bit-vectort1
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 int1
. IfisSigned
is true,t1
is treated as a signed bit-vector.The node
t1
must have a bit-vector sort.Declaration
Swift
func makeBvToInt<T>(_ t1: Z3BitVector<T>, isSigned: Bool) -> Z3Int where T : BitVectorSort
-
Create an integer from the bit-vector argument
t1
.If
isSigned
is false, then the bit-vectort1
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 int1
. IfisSigned
is true,t1
is treated as a signed bit-vector.The node
t1
must have a bit-vector sort.Type-erased version.
Declaration
Swift
func makeBvToIntAny(_ t1: AnyZ3BitVector, isSigned: Bool) -> Z3Int
-
Create a predicate that checks that the bit-wise addition of
t1
andt2
does not overflow.The nodes
t1
andt2
must have the same bit-vector sort. The returned node is of sort Bool.Declaration
Swift
func makeBvAddNoOverflow<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>, isSigned: Bool) -> Z3Bool where T : BitVectorSort
-
Create a predicate that checks that the bit-wise addition of
t1
andt2
does not underflow.The nodes
t1
andt2
must have the same bit-vector sort. The returned node is of sort Bool.Declaration
Swift
func makeBvAddNoUnderflow<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>, isSigned: Bool) -> Z3Bool where T : BitVectorSort
-
Create a predicate that checks that the bit-wise subtraction of
t1
andt2
does not overflow.The nodes
t1
andt2
must have the same bit-vector sort. The returned node is of sort Bool.Declaration
Swift
func makeBvSubNoOverflow<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Create a predicate that checks that the bit-wise subtraction of
t1
andt2
does not underflow.The nodes
t1
andt2
must have the same bit-vector sort. The returned node is of sort Bool.Declaration
Swift
func makeBvSubNoUnderflow<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>, isSigned: Bool) -> Z3Bool where T : BitVectorSort
-
Create a predicate that checks that the bit-wise signed division of
t1
andt2
does not underflow.The nodes
t1
andt2
must have the same bit-vector sort. The returned node is of sort Bool.Declaration
Swift
func makeBvSDivNoOverflow<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Check that bit-wise negation does not overflow when
t1
is interpreted as a signed bit-vector.The node
t1
must have bit-vector sort. The returned node is of sort Bool.Declaration
Swift
func makeBvNegNoOverflow<T>(_ t1: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Create a predicate that checks that the bit-wise multiplication of
t1
andt2
does not overflow.The nodes
t1
andt2
must have the same bit-vector sort. The returned node is of sort Bool.Declaration
Swift
func makeBvMulNoOverflow<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>, isSigned: Bool) -> Z3Bool where T : BitVectorSort
-
Create a predicate that checks that the bit-wise multiplication of
t1
andt2
does not underflow.The nodes
t1
andt2
must have the same bit-vector sort. The returned node is of sort Bool.Declaration
Swift
func makeBvMulNoUnderflow<T>(_ t1: Z3BitVector<T>, _ t2: Z3BitVector<T>) -> Z3Bool where T : BitVectorSort
-
Create a bit-vector numeral from a vector of Booleans.
Seealso
makeNumeral
Declaration
Swift
func makeBvNumeral(_ bits: [Bool]) -> AnyZ3Ast
-
Declare a constant or function.
After declaring a constant or function, the function
makeApp()
can be used to create a constant or function application.Seealso
makeApply
Seealso
makeFreshFuncDecl
Seealso
makeRecFuncDecl
Declaration
Swift
func makeFuncDecl(name: Z3Symbol, domain: [Z3Sort], range: Z3Sort) -> Z3FuncDecl
Parameters
name
name of the constant or function.
domain
array containing the sort of each argument. Must be empty when declaring a constant.
range
sort of the constant or the return sort of the function.
-
Create a constant or function application.
Seealso
makeFreshFuncDecl
Seealso
makeFuncDecl
Seealso
makeRecFuncDecl
Declaration
Swift
func makeApply(_ decl: Z3FuncDecl, args: [AnyZ3Ast]) -> AnyZ3Ast
-
Declare and create a constant.
This function is a shorthand for:
let symbol = context.makeStringSymbol(name) let n = context.makeConstant(name: symbol, sort: sort.getSort(self)).unsafeCastTo<T>()
Seealso
makeApply
Seealso
makeFreshConst
Seealso
makeFuncDecl
-
Declare and create a constant.
This function is a shorthand for:
let symbol = context.makeStringSymbol(name) let n = context.makeConstant(name: symbol, sort: sort.getSort(self)).unsafeCastTo<T>()
Seealso
makeApply
Seealso
makeFreshConst
Seealso
makeFuncDecl
-
Declare a fresh constant or function.
Z3 will generate an unique name for this function declaration. If prefix is different from
nil
, then the name generate by Z3 will start withprefix
.Remark
Ifprefix
isnil
, then it is assumed to be the empty string.Seealso
makeFuncDecl
Declaration
Swift
func makeFreshFuncDecl(prefix: String?, domain: [Z3Sort], range: Z3Sort) -> Z3FuncDecl
-
Declare and create a fresh constant.
This function is a shorthand for:
let decl = context.makeFreshFuncDecl(prefix: prefix, domain: [], range: sort) let n = context.makeApply(decl, args: [])
Remark
Ifprefix
isnil
, then it is assumed to be the empty string.Seealso
makeApply
Seealso
makeConstant
Seealso
makeFreshFuncDecl
Seealso
makeFuncDecl
-
Declare a recursive function
After declaring recursive function, it should be associated with a recursive definition
addRecDef
. The functionmakeApply()
can be used to create a constant or function application.Seealso
addRecDef
Seealso
makeApply
Seealso
makeFuncDecl
Declaration
Swift
func makeRecFuncDecl(name: Z3Symbol, domain: [Z3Sort], range: Z3Sort) -> Z3FuncDecl
Parameters
name
name of the function.
domain
array containing the sort of each argument. The array must not be empty.
range
sort of the constant or the return sort of the function.
-
Define the body of a recursive function.
After declaring a recursive function or a collection of mutually recursive functions, use this function to provide the definition for the recursive function.
Seealso
makeRecFuncDecl
Declaration
Swift
func addRecDef(_ f: Z3FuncDecl, args: [AnyZ3Ast], body: AnyZ3Ast)
Parameters
f
function declaration.
args
constants that are used as arguments to the recursive function in the definition.
body
body of the recursive function
-
Create a new fixedpoint context.
Declaration
Swift
func makeFixedPoint() -> Z3FixedPoint
-
Create the
RoundingMode
sort.Declaration
Swift
func makeFpaRoundingModeSort() -> Z3Sort
-
Create a numeral of
RoundingMode
sort which represents the NearestTiesToEven rounding mode.Declaration
Swift
func makeFpaRoundNearestTiesToEven() -> Z3RoundingMode
-
Create a numeral of
RoundingMode
sort which represents the NearestTiesToEven rounding mode.Declaration
Swift
func makeFpaRNE() -> Z3RoundingMode
-
Create a numeral of
RoundingMode
sort which represents the NearestTiesToAway rounding mode.Declaration
Swift
func makeFpaRoundNearestTiesToAway() -> Z3RoundingMode
-
Create a numeral of
RoundingMode
sort which represents the NearestTiesToAway rounding mode.Declaration
Swift
func makeFpaRNA() -> Z3RoundingMode
-
Create a numeral of
RoundingMode
sort which represents the TowardPositive rounding mode.Declaration
Swift
func makeFpaRoundTowardPositive() -> Z3RoundingMode
-
Create a numeral of
RoundingMode
sort which represents the TowardPositive rounding mode.Declaration
Swift
func makeFpaRTP() -> Z3RoundingMode
-
Create a numeral of
RoundingMode
sort which represents the TowardNegative rounding mode.Declaration
Swift
func makeFpaRoundTowardNegative() -> Z3RoundingMode
-
Create a numeral of
RoundingMode
sort which represents the TowardNegative rounding mode.Declaration
Swift
func makeFpaRTN() -> Z3RoundingMode
-
Create a numeral of
RoundingMode
sort which represents the TowardZero rounding mode.Declaration
Swift
func makeFpaRoundTowardZero() -> Z3RoundingMode
-
Create a numeral of
RoundingMode
sort which represents the TowardZero rounding mode.Declaration
Swift
func makeFpaRTZ() -> Z3RoundingMode
-
Create a FloatingPoint sort.
Remark
ebits
must be larger than 1 andsbits
must be larger than 2.Declaration
Swift
func floatingPointSort(ebits: UInt32, sbits: UInt32) -> Z3Sort
Parameters
c
logical context
ebits
number of exponent bits
sbits
number of significand bits
-
Create the half-precision (16-bit) FloatingPoint sort.
Declaration
Swift
func floatingPoint16Sort() -> Z3Sort
-
Create the single-precision (32-bit) FloatingPoint sort.
Declaration
Swift
func floatingPoint32Sort() -> Z3Sort
-
Create the double-precision (64-bit) FloatingPoint sort.
Declaration
Swift
func floatingPoint64Sort() -> Z3Sort
-
Create the quadruple-precision (128-bit) FloatingPoint sort.
Declaration
Swift
func floatingPoint128Sort() -> Z3Sort
-
Create a floating-point NaN of sort
sort
.Declaration
Swift
func makeFpaNan(sort: Z3Sort) -> AnyZ3FloatingPoint
Parameters
sort
target sort
-
Create a floating-point NaN of sort
sort
.Declaration
Swift
func makeFpaNan<T>(sort: T.Type) -> Z3FloatingPoint<T> where T : FloatingSort
Parameters
sort
target sort
-
Create a floating-point infinity of sort
sort
.When
negative
istrue
, -oo will be generated instead of +oo.Declaration
Swift
func makeFpaInfinite(sort: Z3Sort, negative: Bool) -> AnyZ3FloatingPoint
Parameters
sort
target sort
negative
indicates whether the result should be negative
-
Create a floating-point infinity of sort
sort
.When
negative
istrue
, -oo will be generated instead of +oo.Declaration
Swift
func makeFpaInfinite<T>(sort: T.Type, negative: Bool) -> Z3FloatingPoint<T> where T : FloatingSort
Parameters
sort
target sort
negative
indicates whether the result should be negative
-
Create a floating-point zero of sort
sort
.When
negative
istrue
, -zero will be generated instead of +zero.Declaration
Swift
func makeFpaZero(sort: Z3Sort, negative: Bool) -> AnyZ3FloatingPoint
Parameters
sort
target sort
negative
indicates whether the result should be negative
-
Create a floating-point zero of sort
sort
.When
negative
istrue
, -zero will be generated instead of +zero.Declaration
Swift
func makeFpaZero<T>(sort: T.Type, negative: Bool) -> Z3FloatingPoint<T> where T : FloatingSort
Parameters
sort
target sort
negative
indicates whether the result should be negative
-
Create an expression of FloatingPoint sort from three bit-vector expressions.
This is the operator named
fp' in the SMT FP theory definition. Note that
sgn` is required to be a bit-vector of size 1. Significand and exponent are required to be longer than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments. The exponent is assumed to be in IEEE-754 biased representation.Declaration
Swift
func makeFpaFp<T: BitVectorSort, U: BitVectorSort, V: BitVectorSort>( sgn: Z3BitVector<T>, exp: Z3BitVector<U>, sig: Z3BitVector<V> ) -> AnyZ3FloatingPoint
Parameters
sgn
sign
exp
exponent
sig
significand
-
Create an expression of FloatingPoint sort from three bit-vector expressions.
Type-erased version.
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 longer than 1 and 2 respectively. The FloatingPoint sort of the resulting expression is automatically determined from the bit-vector sizes of the arguments. The exponent is assumed to be in IEEE-754 biased representation.Declaration
Swift
func makeFpaFpAny(sgn: AnyZ3Ast, exp: AnyZ3Ast, sig: AnyZ3Ast) -> AnyZ3FloatingPoint
Parameters
sgn
sign
exp
exponent
sig
significand
-
Create a numeral of FloatingPoint sort from a float.
This function is used to create numerals that fit in a float value. It is slightly faster than
makeNumeral
since it is not necessary to parse a string.Declaration
Swift
func makeFpaNumeralFloat(_ value: Float, sort: Z3Sort) -> AnyZ3FloatingPoint
Parameters
value
value
sort
sort
-
Create a numeral of FloatingPoint sort from a float.
This function is used to create numerals that fit in a float value. It is slightly faster than
makeNumeral
since it is not necessary to parse a string.Declaration
Swift
func makeFpaNumeralFloat<T>(_ value: Float, sort: T.Type) -> Z3FloatingPoint<T> where T : FloatingSort
Parameters
value
value
sort
sort
-
Create a numeral of FloatingPoint sort from a double.
This function is used to create numerals that fit in a float value. It is slightly faster than
makeNumeral
since it is not necessary to parse a string.Declaration
Swift
func makeFpaNumeralDouble(_ value: Double, sort: Z3Sort) -> AnyZ3FloatingPoint
Parameters
value
value
sort
sort
-
Create a numeral of FloatingPoint sort from a double.
This function is used to create numerals that fit in a float value. It is slightly faster than
makeNumeral
since it is not necessary to parse a string.Declaration
Swift
func makeFpaNumeralDouble<T>(_ value: Double, sort: T.Type) -> Z3FloatingPoint<T> where T : FloatingSort
Parameters
value
value
sort
sort
-
Create a numeral of FloatingPoint sort from a floating point value.
This function is used to create numerals that fit in a Double value. It is slightly faster than
makeNumeral
since it is not necessary to parse a string.Declaration
Swift
func makeFpaNumeral<T>(_ value: T) -> Z3FloatingPoint<T> where T : BinaryFloatingPoint, T : LosslessStringConvertible, T : FloatingSort
Parameters
value
value
-
Create a numeral of FloatingPoint sort from a floating point value.
Alias for
makeFpaNumeral
Declaration
Swift
func makeFloat<T>(_ value: T) -> Z3FloatingPoint<T> where T : BinaryFloatingPoint, T : LosslessStringConvertible, T : FloatingSort
Parameters
value
value
-
Create a numeral of FloatingPoint sort from a signed integer.
Declaration
Swift
func makeFpaNumeralInt(_ value: Int32, sort: Z3Sort) -> AnyZ3FloatingPoint
Parameters
value
value
sort
result sort
-
Create a numeral of FloatingPoint sort from a signed integer.
Declaration
Swift
func makeFpaNumeralInt<T>(_ value: Int32, sort: T.Type = T.self) -> Z3FloatingPoint<T> where T : FloatingSort
Parameters
value
value
sort
result sort
-
Create a numeral of FloatingPoint sort from a sign bit and two integers.
Declaration
Swift
func makeFpaNumeralUInt(_ sgn: Bool, _ exp: Int32, _ sig: UInt32, sort: Z3Sort) -> AnyZ3FloatingPoint
Parameters
sgn
sign bit (true == negative)
exp
exponent
sig
significand
sort
result sort
-
Create a numeral of FloatingPoint sort from a sign bit and two integers.
Declaration
Swift
func makeFpaNumeralUInt<T>(_ sgn: Bool, _ exp: Int32, _ sig: UInt32, sort: T.Type) -> Z3FloatingPoint<T> where T : FloatingSort
Parameters
sgn
sign bit (true == negative)
exp
exponent
sig
significand
sort
result sort
-
Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
Declaration
Swift
func makeFpaNumeralUInt<T>(_ sgn: Bool, _ exp: Int64, _ sig: UInt64, sort: T.Type) -> Z3FloatingPoint<T> where T : FloatingSort
Parameters
sgn
sign bit (true == negative)
exp
exponent
sig
significand
sort
result sort
-
Floating-point absolute value
Declaration
Swift
func makeFpaAbs<T>(_ t: Z3FloatingPoint<T>) -> Z3FloatingPoint<T> where T : FloatingSort
-
Floating-point negation
Declaration
Swift
func makeFpaNeg<T>(_ t: Z3FloatingPoint<T>) -> Z3FloatingPoint<T> where T : FloatingSort
-
Floating-point addition
rm
must be ofRoundingMode
sort,t1
andt2
must have the same FloatingPoint sort.Declaration
Swift
func makeFpaAdd<T: FloatingSort>(_ rm: Z3RoundingMode, _ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3FloatingPoint<T>
Parameters
rm
term of
RoundingMode
sort -
Floating-point subtraction
rm
must be ofRoundingMode
sort,t1
andt2
must have the same FloatingPoint sort.Declaration
Swift
func makeFpaSubtract<T: FloatingSort>(_ rm: Z3RoundingMode, _ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3FloatingPoint<T>
Parameters
rm
term of RoundingModeSort sort
-
Floating-point multiplication
rm
must be ofRoundingMode
sort,t1
andt2
must have the same FloatingPoint sort.Declaration
Swift
func makeFpaMultiply<T: FloatingSort>(_ rm: Z3RoundingMode, _ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3FloatingPoint<T>
Parameters
rm
term of
RoundingMode
sort -
Floating-point division
rm
must be ofRoundingMode
sort,t1
andt2
must have the same FloatingPoint sort.Declaration
Swift
func makeFpaDivide<T: FloatingSort>(_ rm: Z3RoundingMode, _ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3FloatingPoint<T>
Parameters
rm
term of
RoundingMode
sort -
Floating-point fused multiply-add.
The result is
round((t1 * t2) + t3)
.rm
must be ofRoundingMode
sort,t1
,t2
, andt3
must have the same FloatingPoint sort.Declaration
Swift
func makeFpaDivide<T: FloatingSort>(_ rm: Z3RoundingMode, _ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>, _ t3: Z3FloatingPoint<T>) -> Z3FloatingPoint<T>
Parameters
rm
term of
RoundingMode
sort -
Floating-point square root
Declaration
Swift
func makeFpaSquareRoot<T: FloatingSort>(_ rm: Z3RoundingMode, _ t1: Z3FloatingPoint<T>) -> Z3FloatingPoint<T>
-
Floating-point remainder
Declaration
Swift
func makeFpaRemainder<T: FloatingSort>(_ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3FloatingPoint<T>
-
Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
Declaration
Swift
func makeFpaRoundToIntegral<T: FloatingSort>(_ rm: Z3RoundingMode, _ t: Z3FloatingPoint<T>) -> Z3FloatingPoint<T>
-
Minimum of floating-point numbers.
Declaration
Swift
func makeFpaMin<T>(_ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3FloatingPoint<T> where T : FloatingSort
-
Maximum of floating-point numbers.
Declaration
Swift
func makeFpaMax<T>(_ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3FloatingPoint<T> where T : FloatingSort
-
Floating-point less than or equal.
Declaration
Swift
func makeFpaLeq<T>(_ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Floating-point less than.
Declaration
Swift
func makeFpaLt<T>(_ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Floating-point greater than or equal.
Declaration
Swift
func makeFpaGeq<T>(_ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Floating-point greater than.
Declaration
Swift
func makeFpaGt<T>(_ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Floating-point equality.
Declaration
Swift
func makeFpaEq<T>(_ t1: Z3FloatingPoint<T>, _ t2: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Predicate indicating whether
t
is a normal floating-point number.Declaration
Swift
func makeFpaIsNormal<T>(_ t: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Predicate indicating whether
t
is a subnormal floating-point number.Declaration
Swift
func makeFpaIsSubnormal<T>(_ t: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Predicate indicating whether
t
is a floating-point number with zero value, i.e., +zero or -zero.Declaration
Swift
func makeFpaIsZero<T>(_ t: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Predicate indicating whether
t
is a floating-point number representing +oo or -oo.Declaration
Swift
func makeFpaIsInfinite<T>(_ t: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Predicate indicating whether
t
is a NaN.Declaration
Swift
func makeFpaIsNan<T>(_ t: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Predicate indicating whether
t
is a negative floating-point number.Declaration
Swift
func makeFpaIsNegative<T>(_ t: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Predicate indicating whether
t
is a positive floating-point number.Declaration
Swift
func makeFpaIsPositive<T>(_ t: Z3FloatingPoint<T>) -> Z3Bool where T : FloatingSort
-
Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
Produces a term that represents the conversion of a bit-vector term
bv
to a floating-point term of sortsort
.sort
must be a FloatingPoint sort,t
must be of bit-vector sort, and the bit-vector size ofbv
must be equal toebits+sbits
ofsort
. The format of the bit-vector is as defined by the IEEE 754-2008 interchange format.Declaration
Swift
func makeFpaToFPBv<T, U>(_ bv: Z3BitVector<T>, sort: U.Type) -> Z3FloatingPoint<U> where T : BitVectorSort, U : FloatingSort
Parameters
bv
a bit-vector term
sort
floating-point sort
-
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
t
must have FloatingPoint sort. The size of the resulting bit-vector is automatically determined.Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN.
Declaration
Swift
func makeFpaToIEEEBv<T>(_ t: Z3FloatingPoint<T>) -> AnyZ3BitVector where T : FloatingSort
-
Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
Type-erased version.
t
must have FloatingPoint sort. The size of the resulting bit-vector is automatically determined.Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion knows only one NaN and it will always produce the same bit-vector representation of that NaN.
Declaration
Swift
func makeFpaToIEEEBvAny(_ t: AnyZ3Ast) -> AnyZ3BitVector
-
Alias for
makeFpaToFPBv
Declaration
Swift
func makeBitVectorToFloat<T, U>(_ bv: Z3BitVector<T>, sort: U.Type) -> Z3FloatingPoint<U> where T : BitVectorSort, U : FloatingSort
-
Produces a term that represents the conversion of the floating-point term
t
into a bit-vector term of sizesz
in 2’s complement format (signed when signed==true). If necessary, the result will be rounded according to rounding mode rm.Declaration
Swift
func makeFpaToBvAny(_ rm: AnyZ3Ast, _ t: AnyZ3Ast, _ sz: UInt32, signed: Bool) -> AnyZ3BitVector
-
Produces a term that represents the conversion of the floating-point term
t
into a bit-vector term of bitWidthT.bitWidth
in 2’s complement format (signed when signed==true). If necessary, the result will be rounded according to rounding mode rm.Declaration
Swift
func makeFpaToBv<T, F>(_ rm: Z3RoundingMode, _ t: Z3FloatingPoint<F>, _ bvSort: T.Type, signed: Bool) -> Z3BitVector<T> where T : BitVectorSort, F : FloatingSort
-
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Produces a term that represents the conversion of a floating-point term
t
to a floating-point term of sortsort
. If necessary, the result will be rounded according to rounding moderm
.Declaration
Swift
func makeFpaToFPFloat<T: FloatingSort, U: FloatingSort>(_ rm: Z3RoundingMode, _ t: Z3FloatingPoint<T>, sort: U.Type) -> Z3FloatingPoint<U>
Parameters
bv
a bit-vector term
sort
floating-point sort
-
Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
Produces a term that represents the conversion of a floating-point term
t
to a floating-point term of sortsort
. If necessary, the result will be rounded according to rounding moderm
.Type-erased version.
Declaration
Swift
func makeFpaToFPFloatAny(_ rm: Z3RoundingMode, _ t: AnyZ3Ast, sort: Z3Sort) -> AnyZ3FloatingPoint
Parameters
rm
term of RoundingMode sort
t
a floating-point term
sort
floating-point sort
-
Conversion of a term of real sort into a term of FloatingPoint sort.
Produces a term that represents the conversion of term
t
of real sort into a floating-point term of sortsort
. If necessary, the result will be rounded according to rounding moderm
.Declaration
Swift
func makeFpaToFPReal<T: FloatingSort>(_ rm: Z3RoundingMode, _ t: Z3Real, sort: T.Type) -> Z3FloatingPoint<T>
-
Conversion of a term of real sort into a term of FloatingPoint sort.
Type-erased version.
Produces a term that represents the conversion of term
t
of real sort into a floating-point term of sortsort
. If necessary, the result will be rounded according to rounding moderm
.Declaration
Swift
func makeFpaToFPReal(_ rm: Z3RoundingMode, _ t: Z3Real, sort: Z3Sort) -> AnyZ3FloatingPoint
-
Conversion of a floating-point term into a real-numbered term.
Produces a term that represents the conversion of the floating-point term t into a real number. Note that this type of conversion will often result in non-linear constraints over real terms.
Declaration
Swift
func makeFpaToReal<T>(_ t: Z3FloatingPoint<T>) -> Z3Real where T : FloatingSort
-
Conversion of a floating-point term into a real-numbered term.
Produces a term that represents the conversion of the floating-point term t into a real number. Note that this type of conversion will often result in non-linear constraints over real terms.
Declaration
Swift
func makeFpaToReal(_ t: AnyZ3FloatingPoint) -> Z3Real
-
Coerce a floating-point number to an integer, rounding with a given rounding mode.
Equivalent to:
let rounded = makeFpaRoundToIntegral(roundingMode, t1) let real = makeFpaToReal(rounded) return makeReal2Int(real)
Declaration
Swift
func makeFpaToInt<T>(roundingMode: Z3RoundingMode, _ t1: Z3FloatingPoint<T>) -> Z3Int where T : FloatingSort
-
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
Declaration
Swift
func fpaGetEbits<T>(sort: T.Type) -> UInt32 where T : FloatingSort
-
Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
Declaration
Swift
func fpaGetEbits(sort: Z3Sort) -> UInt32
-
Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
Declaration
Swift
func fpaGetSbits<T>(sort: T.Type) -> UInt32 where T : FloatingSort
-
Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
Declaration
Swift
func fpaGetSbits(sort: Z3Sort) -> UInt32
-
Checks whether a given floating-point numeral is a NaN.
Declaration
Swift
func fpaIsNumeralNan<T>(_ ast: Z3Ast<T>) -> Bool where T : FloatingSort
-
Checks whether a given floating-point numeral is a +oo or -oo.
Declaration
Swift
func fpaIsNumeralInfinite<T>(_ ast: Z3Ast<T>) -> Bool where T : FloatingSort
-
Checks whether a given floating-point numeral is +zero or -zero.
Declaration
Swift
func fpaIsNumeralZero<T>(_ ast: Z3Ast<T>) -> Bool where T : FloatingSort
-
Checks whether a given floating-point numeral is normal.
Declaration
Swift
func fpaIsNumeralNormal<T>(_ ast: Z3Ast<T>) -> Bool where T : FloatingSort
-
Checks whether a given floating-point numeral is subnormal.
Declaration
Swift
func fpaIsNumeralSubnormal<T>(_ ast: Z3Ast<T>) -> Bool where T : FloatingSort
-
Checks whether a given floating-point numeral is positive.
Declaration
Swift
func fpaIsNumeralPositive<T>(_ ast: Z3Ast<T>) -> Bool where T : FloatingSort
-
Checks whether a given floating-point numeral is negative.
Declaration
Swift
func fpaIsNumeralNegative<T>(_ ast: Z3Ast<T>) -> Bool where T : FloatingSort
-
Retrieves the sign of a floating-point literal.
Declaration
Swift
func fpaGetNumeralSign<T>(_ ast: Z3Ast<T>) -> Int32 where T : FloatingSort
-
Return the significand value of a floating-point numeral as a string.
Declaration
Swift
func fpaGetNumeralSignificandString<T>(_ ast: Z3Ast<T>) -> String where T : FloatingSort
-
Return the exponent value of a floating-point numeral as a string.
Declaration
Swift
func fpaGetNumeralExponentString<T>(_ ast: Z3Ast<T>, biased: Bool) -> String where T : FloatingSort
Parameters
ast
a floating-point numeral
biased
flag to indicate whether the result is in biased representation
-
Create an AST node representing
true
.Declaration
Swift
func makeTrue() -> Z3Bool
-
Create an AST node representing
false
.Declaration
Swift
func makeFalse() -> Z3Bool
-
Create an AST node representing
distinct(args[0], ..., args[num_args-1])
.The
distinct
construct is used for declaring the arguments pairwise distinct. That is,Forall 0 <= i < j < num_args. not args[i] = args[j]
.All arguments must have the same sort.
Precondition
The number of arguments of a distinct construct must be greater than one. -
Create an AST node representing
distinct(args[0], ..., args[num_args-1])
.The
distinct
construct is used for declaring the arguments pairwise distinct. That is,Forall 0 <= i < j < num_args. not args[i] = args[j]
.All arguments must have the same sort.
Type-erased version.
Precondition
The number of arguments of a distinct construct must be greater than one. -
Create an AST node representing an if-then-else:
ite(t1, t2, t3)
.The node
t1
must have Boolean sort,t2
andt3
must have the same sort. The sort of the new node is equal to the sort oft2
andt3
.
-
Create a numeral of a given sort.
Seealso
makeInteger()
Seealso
makeUnsignedInteger()
Declaration
Swift
func makeNumeral<T>(number: String, sort: T.Type) -> Z3Ast<T> where T : NumericalSort
Parameters
number
A string representing the numeral value in decimal notation. The string may be of the form
[num]*[.[num]*][E[+|-][num]+]
. If the given sort is a real, then the numeral can be a rational, that is, a string of the form[num]* / [num]*
.sort
The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size.
-
Create a numeral of a given sort.
Seealso
makeInteger()
Seealso
makeUnsignedInteger()
Parameters
number
A string representing the numeral value in decimal notation. The string may be of the form
[num]*[.[num]*][E[+|-][num]+]
. If the given sort is a real, then the numeral can be a rational, that is, a string of the form[num]* / [num]*
.sort
The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size.
-
Create a real from a fraction.
Seealso
makeNumeral
Seealso
makeInteger
Seealso
makeUnsignedInteger
Precondition
den != 0
Declaration
Swift
func makeReal(_ num: Int32, _ den: Int32 = 1) -> Z3Real
Parameters
num
numerator of rational.
den
denominator of rational.
-
Create a numeral of an int, bit-vector, or finite-domain sort.
This method can be used to create numerals that fit in a machine integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.
Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeInteger(_ value: Int32) -> Z3Int
-
Create a numeral of a bit-vector.
This method can be used to create numerals that fit in a machine integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.
Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeIntegerBv(_ value: Int32) -> Z3BitVector32
-
Create a numeral of a bit-vector of one bit.
This method can be used to create numerals that fit in a machine integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.
Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeInteger1Bv(_ value: UInt32) -> Z3BitVector1
-
Create a numeral of an int, bit-vector, or finite-domain sort.
This method can be used to create numerals that fit in a machine unsigned integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.
Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeUnsignedInteger(_ value: UInt32) -> Z3Int
-
Create a numeral of a bit-vector.
This method can be used to create numerals that fit in a machine integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.
Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeUnsignedIntegerBv(_ value: UInt32) -> Z3BitVectorU32
-
Create a numeral of an int, bit-vector, or finite-domain sort.
This method can be used to create numerals that fit in a machine
Int64
integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeInteger64(_ value: Int64) -> Z3Int
-
Create a numeral of a bit-vector.
This method can be used to create numerals that fit in a machine
Int64
integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeInteger64Bv(_ value: Int64) -> Z3BitVector64
-
Create a numeral of an int, bit-vector, or finite-domain sort.
This method can be used to create numerals that fit in a machine
UInt64
integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeUnsignedInteger64(_ value: UInt64) -> Z3Int
-
Create a numeral of an int, bit-vector, or finite-domain sort.
This method can be used to create numerals that fit in a machine
UInt64
integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.Seealso
makeNumeral(number:sort:)
Seealso
makeUnsignedInteger64(_:)
-
Create a numeral of a bit-vector.
This method can be used to create numerals that fit in a machine
Int64
integer. It is slightly faster than makeNumeral since it is not necessary to parse a string.Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeUnsignedInteger64Bv(_ value: UInt64) -> Z3BitVectorU64
-
Create a numeral of a bit-vector.
This method can be used to create numerals that fit in a 128-bit integer. The initial value is split into two
UInt64
bit patterns that fit the low (0-63) and high (64-127) bit ranges.Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeInteger128Bv(highBits: UInt64, lowBits: UInt64) -> Z3BitVector128
-
Create a numeral of a bit-vector.
This method can be used to create numerals that fit in a 128-bit integer.
Seealso
makeNumeral(number:sort:)
Declaration
Swift
func makeUnsignedInteger128Bv(highBits: UInt64, lowBits: UInt64) -> Z3BitVector128
-
Create a bit-vector numeral from a vector of Booleans.
Precondition
!values.isEmpty
Seealso
Declaration
Swift
func makeIntegerBvFromBools(_ values: [Bool]) -> AnyZ3BitVector
-
Return numeral value, as a decimal string of a numeric constant term
Declaration
Swift
func getNumeralString(_ numeral: AnyZ3Ast) -> String
-
Similar to
getNumeralString(_:)
, but only succeeds if the value can fit in a machineInt64
int. Returnsnil
if it fails.Declaration
Swift
func getNumeralInt64(_ numeral: AnyZ3Ast) -> Int64?
-
Similar to
getNumeralString(_:)
, but only succeeds if the value can fit in a machineUInt64
int. Returnsnil
if it fails.Declaration
Swift
func getNumeralUInt64(_ numeral: AnyZ3Ast) -> UInt64?
-
Parse the given string using the SMT-LIB2 parser.
It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the string.
Declaration
Swift
func parseSmtlib2String( _ str: String, sorts: [(name: Z3Symbol, Z3Sort)], decls: [(name: Z3Symbol, Z3FuncDecl)] ) throws -> Z3AstVector
-
Parse the contents of a given file path using the SMT-LIB2 parser.
It returns a formula comprising of the conjunction of assertions in the scope (up to push/pop) at the end of the file.
Similar to
parseSmtlib2String(_:sorts:decls:)
, but reads the benchmark from a file.Declaration
Swift
func parseSmtlib2File( filePath: String, sorts: [(name: Z3Symbol, Z3Sort)], decls: [(name: Z3Symbol, Z3FuncDecl)] ) throws -> Z3AstVector
-
Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next evaluation builds on top of the previous call.
Declaration
Swift
func evalSmtlib2String(_ str: String) -> String
-
Create a parser context.
A parser context maintains state between calls to
Z3ParserContext.parseString(_:)
where the caller can pass in a set of SMTLIB2 commands. It maintains all the declarations from previous calls together with of sorts and function declarations (including 0-ary) that are added directly to the context.Declaration
Swift
func createParserContext() -> Z3ParserContext
-
Return the nonzero subresultants of
p
andq
with respect to the “variable”x
.\pre
p
,q
andx
are Z3 expressions wherep
andq
are arithmetic terms. Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable. Example:f(a)
is a considered to be a variable in the polynomialf(a)*f(a) + 2*f(a) + 1
Declaration
Swift
func polynomialSubresultants<PSort: ArithmeticSort, QSort: ArithmeticSort>( _ p: Z3Ast<PSort>, _ q: Z3Ast<QSort>, _ x: AnyZ3Ast ) -> Z3AstVector?
-
Create a pattern for quantifier instantiation.
Z3 uses pattern matching to instantiate quantifiers. If a pattern is not provided for a quantifier, then Z3 will automatically compute a set of patterns for it. However, for optimal performance, the user should provide the patterns.
Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is a called a multi-pattern.
In general, one can pass in a list of (multi-)patterns in the quantifier constructor.
Seealso
makeForAll
Seealso
makeExists
-
Create a bound variable.
Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.
abs(forall (x1) phi) = forall (x1) abs1(phi, x1, 0) abs(forall (x1, x2) phi) = abs(forall (x1) abs(forall (x2) phi)) abs1(x, x, n) = b_n abs1(y, x, n) = y abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n)) abs1(forall (x1) phi, x, n) = forall (x1) (abs1(phi, x, n+1))
The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.
Seealso
makeForAll
Seealso
makeExists
Parameters
index
de-Bruijn index
ty
sort of the bound variable
-
Create a forall formula. It takes an expression
body
that contains bound variables of the same sorts as the sorts listed in the arraydeclarations
. The bound variables are de-Bruijn indices created usingmakeBound
. The arraydeclarations
contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in thedeclarations
array refers to the variable with index 0, the second to last element ofdeclarations
refers to the variable with index 1, etc.Seealso
makePattern
Seealso
makeBound
Seealso
makeExists
Declaration
Parameters
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
makePattern
declarations
an array of declarations containing the sorts and names of the bound variables.
body
the body of the quantifier.
-
Create an exists formula. Similar to
makeForall
.Seealso
makePattern
Seealso
makeBound
Seealso
makeForall
Seealso
makeQuantifier
Declaration
Parameters
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
makePattern
declarations
an array of declarations containing the sorts and names of the bound variables.
body
the body of the quantifier.
-
Create a quantifier - universal or existential, with pattern hints.
Seealso
makePattern
Seealso
makeBound
Seealso
makeForall
Seealso
makeExists
Declaration
Parameters
isForall
flag to indicate if this is a universal or existential 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
makePattern
declarations
an array of declarations containing the sorts and names of the bound variables.
body
the body of the quantifier.
-
Create the regular language
re+
.Declaration
Swift
func makeRePlus<Element>(_ re: Z3RegularExp<Element>) -> Z3RegularExp<Element> where Element : SortKind
-
Create the regular language
re*
.Declaration
Swift
func makeReStar<Element>(_ re: Z3RegularExp<Element>) -> Z3RegularExp<Element> where Element : SortKind
-
Create the regular language
[re]
.Declaration
Swift
func makeReOption<Element>(_ re: Z3RegularExp<Element>) -> Z3RegularExp<Element> where Element : SortKind
-
Create the union of the regular languages.
Precondition
asts.count > 0
.Declaration
Swift
func makeReUnion<Element>(_ asts: [Z3RegularExp<Element>]) -> Z3RegularExp<Element> where Element : SortKind
-
Create the concatenation of the regular languages.
Precondition
asts.count > 0
.Declaration
Swift
func makeReConcat<Element>(_ asts: [Z3RegularExp<Element>]) -> Z3RegularExp<Element> where Element : SortKind
-
Create the range regular expression over two sequences of length 1.
Declaration
Swift
func makeReRange<Element>( low: Z3Seq<Element>, high: Z3Seq<Element> ) -> Z3RegularExp<Element>
-
Create a regular expression that accepts all singleton sequences of the regular expression sort.
Declaration
Swift
func makeReAllChar<Element>( _ sort: ReSort<Element>.Type = ReSort<Element>.self ) -> Z3RegularExp<Element>
-
Create a regular expression loop.
The supplied regular expression
ast
is repeated betweenlow
andhigh
times. Thelow
should be belowhigh
with one exception: when supplying the valuehigh
as 0, the meaning is to repeat the argumentast
at leastlow
number of times, and with an unbounded upper bound.Declaration
Swift
func makeReLoop<Element>( _ ast: Z3RegularExp<Element>, low: UInt32, high: UInt32 ) -> Z3RegularExp<Element>
-
Create a regular expression loop.
The supplied regular expression
ast
is repeated betweenlow
andhigh
times. Thelow
should be belowhigh
with one exception: when supplying the valuehigh
as 0, the meaning is to repeat the argumentast
at leastlow
number of times, and with an unbounded upper bound.Type-erased version.
Precondition
ast
is of a regular expression sort. -
Create a power regular expression.
Declaration
Swift
func makeRePower<Element>(_ ast: Z3RegularExp<Element>, count: UInt32) -> Z3RegularExp<Element> where Element : SortKind
-
Create the intersection of the regular languages.
Precondition
asts.count > 0
.Declaration
Swift
func makeReIntersect<Element>(_ asts: [Z3RegularExp<Element>]) -> Z3RegularExp<Element> where Element : SortKind
-
Create the complement of the regular language
re
.Declaration
Swift
func makeReComplement<Element>(_ re: Z3RegularExp<Element>) -> Z3RegularExp<Element> where Element : SortKind
-
Create the difference of regular expressions.
Declaration
Swift
func makeReDiff<Element>(_ re1: Z3RegularExp<Element>, _ re2: Z3RegularExp<Element>) -> Z3RegularExp<Element> where Element : SortKind
-
Create an empty regular expression of sort
sort
.Declaration
Swift
func makeReEmpty<Element>( _ sort: ReSort<Element>.Type = ReSort<Element>.self ) -> Z3RegularExp<Element>
-
Create an universal regular expression of sort
sort
.Declaration
Swift
func makeReFull<Element>( _ sort: ReSort<Element>.Type = ReSort<Element>.self ) -> Z3RegularExp<Element>
-
Creates a character literal.
Declaration
Swift
func makeChar(_ character: UInt32) -> Z3Char
-
Create a bit-vector (code point) from character.
Declaration
Swift
func makeCharToBv(_ char: Z3Char) -> AnyZ3BitVector
-
Create a character from a bit-vector (code point).
Declaration
Swift
func makeCharFromBv<Sort>(_ bv: Z3BitVector<Sort>) -> Z3Char where Sort : BitVectorSort
-
Return index of the first occurrence of
substr
insequence
starting fromoffset
.If
sequence
does not containsubstr
, then the value is -1, ifoffset
is the length ofsequence
, then the value is -1 as well. The value is -1 ifoffset
is negative or larger than the length ofsequence
. -
Return index of the first occurrence of
substr
insequence
starting fromoffset
.If
sequence
does not containsubstr
, then the value is -1, ifoffset
is the length ofsequence
, then the value is -1 as well. The value is -1 ifoffset
is negative or larger than the length ofsequence
.Type-erased version.
Precondition
sequence
andsubstr
are the same sequence sort,offset
is int sort. -
Create a regular expression that accepts the sequence
sequence
.Declaration
Swift
func makeSeqToRe<Element>(_ sequence: Z3Seq<Element>) -> Z3RegularExp<Element> where Element : SortKind
-
Check for regular expression membership.
Declaration
Swift
func makeSeqInRe<Element>(_ sequence: Z3Seq<Element>, regex: Z3RegularExp<Element>) -> Z3Bool where Element : SortKind
-
Create a new solver. This solver is a “combined solver” (see combined_solver module) that internally uses a non-incremental (solver1) and an incremental solver (solver2). This combined solver changes its behaviour based on how it is used and how its parameters are set.
If the solver is used in a non incremental way (i.e. no calls to
Z3Solver.push()
orZ3Solver.pop(_:)
, and no calls toZ3Solver.assert()
orZ3Solver.assertAndTrack
after checking satisfiability without an interveningSolver.reset()
) then solver1 will be used. This solver will apply Z3’s “default” tactic.The “default” tactic will attempt to probe the logic used by the assertions and will apply a specialized tactic if one is supported. Otherwise the general
(and-then simplify smt)
tactic will be used.If the solver is used in an incremental way then the combined solver will switch to using solver2 (which behaves similarly to the general “smt” tactic).
Note however it is possible to set the
solver2_timeout
,solver2_unknown
, andignore_solver1
parameters of the combined solver to change its behaviour.The method
Z3Solver.getModel()
retrieves a model if the assertions is satisfiable (i.e., the result isZ3LBool.lUndef
) and model construction is enabled.The method
Z3Solver.getModel()
can also be used even if the result isZ3LBool.lUndef
, but the returned model is not guaranteed to satisfy quantified assertions.Seealso
makeSimpleSolver()
Seealso
makeSolverForLogic(_:)
Seealso
makeSolver(fromTactic:)
Declaration
Swift
func makeSolver() -> Z3Solver
-
Create a new incremental solver.
This is equivalent to applying the “smt” tactic.
Unlike
Z3Context.makeSolver()
this solver - Does not attempt to apply any logic specific tactics. - Does not change its behaviour based on whether it used incrementally/non-incrementally.Note that these differences can result in very different performance compared to
Z3Context.makeSolver()
.The function
Z3Solver.getModel()
retrieves a model if the assertions is satisfiable (i.e., the result isZ3_L_TRUE
) and model construction is enabled. The functionZ3Solver.getModel()
can also be used even if the result isZ3_L_UNDEF
, but the returned model is not guaranteed to satisfy quantified assertions.Seealso
makeSolver()
Seealso
makeSolverForLogic(_:)
Seealso
makeSolver(fromTactic:)
Declaration
Swift
func makeSimpleSolver() -> Z3Solver
-
Create a new solver customized for the given logic. It behaves like
makeSolver()
if the logic is unknown or unsupported.Seealso
makeSolver()
Seealso
makeSimpleSolver()
Seealso
makeSolver(fromTactic:)
-
Create a new solver that is implemented using the given tactic. The solver supports the commands
Z3Solver.push()
andZ3Solver.pop()
, but it will always solve eachZ3Solver.check()
from scratch.Seealso
makeSolver()
Seealso
makeSimpleSolver()
Seealso
makeSolverForLogic(_:)
-
Create the integer type.
This type is not the int type found in programming languages. A machine integer can be represented using bit-vectors. The function
bitVectorSort(size:)
creates a bit-vector type.Seealso
Z3_mk_bv_sort
Declaration
Swift
func intSort() -> Z3Sort
-
Create the Boolean type. This type is used to create propositional variables and predicates.
Declaration
Swift
func boolSort() -> Z3Sort
-
Create the real type.
Note that this type is not a floating point number.
Declaration
Swift
func realSort() -> Z3Sort
-
Create a bit-vector type of the given size. This type can also be seen as a machine integer.
Remark
The size of the bit-vector type must be greater than zero.Declaration
Swift
func bitVectorSort(size: UInt32) -> Z3Sort
-
Create a named finite domain sort.
To create constants that belong to the finite domain, use the APIs for creating numerals and pass a numeric constant together with the sort returned by this call. The numeric constant should be between 0 and the less than the size of the domain.
Seealso
getFiniteDomainSortSize
Declaration
Swift
func makeFiniteDomainSort(name: Z3Symbol, size: UInt64) -> Z3FiniteDomainSort
-
Create a tuple type.
A tuple with
n
fields has a constructor andn
projections. This function will also declare the constructor and projection functions.Declaration
Swift
func makeTupleSort(mkTupleName: Z3Symbol, fieldNames: [Z3Symbol], fieldSorts: [Z3Sort]) -> (mkTupleDecl: Z3FuncDecl, projDecl: [Z3FuncDecl], tupleSort: Z3Sort)
Parameters
mkTupleName
name of the constructor function associated with the tuple type.
fieldNames
name of the projection functions.
fieldSorts
type of the tuple fields. Must be at least the same size as
fieldNames
.Return Value
A tuple containing:
mkTupleDecl
: output that will contain the constructor declaration.projDecl
: output that will contain the projection function declarations.tupleSort
: the proper generated tuple sort
-
Create a enumeration sort.
An enumeration sort with
n
elements. This function will also declare the functions corresponding to the enumerations.For example, if this function is called with three symbols A, B, C and the name S, then
s
is a sort whose name is S, and the function returns three terms corresponding to A, B, C inenumConstants
. The arrayenumTesters
has three predicates of type(s -> Bool)
. The first predicate (corresponding to A) is true when applied to A, and false otherwise. Similarly for the other predicates.Declaration
Swift
func makeEnumerationSort(name: Z3Symbol, enumNames: [Z3Symbol]) -> (enumConstants: [Z3FuncDecl], enumTesters: [Z3FuncDecl], sort: Z3Sort)
Parameters
name
name of the enumeration sort.
n
number of elements in enumeration sort.
enumNames
names of the enumerated elements.
Return Value
A tuple containing:
enumConstants
: constants corresponding to the enumerated elements.parameter
: predicates testing if terms of the enumeration sort correspond to an enumeration.sort
: The resulting sort
-
Create a constructor.
Seealso
makeConstructorList
Seealso
queryConstructor
Declaration
Swift
func makeConstructor(name: Z3Symbol, recognizer: Z3Symbol, fieldNames: [Z3Symbol], sorts: [Z3Sort], sortRefs: [UInt32]) -> Z3Constructor
Parameters
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
sortRefs
should be an index referring to one of the recursive data types that is declared. -
Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
Seealso
makeConstructor
Seealso
makeConstructorList
Seealso
makeDatatypes
Declaration
Swift
func makeDatatype(name: Z3Symbol, constructors: inout [Z3Constructor]) -> Z3Sort
Parameters
name
name of datatype.
constructors
array of constructor containers.
-
Create list of constructors.
Seealso
makeConstructor
Declaration
Swift
func makeConstructorList(_ constructors: [Z3Constructor]) -> Z3ConstructorList
-
Create mutually recursive datatypes
Seealso
makeConstructor
Seealso
makeConstructorList
Seealso
makeDatatype
Declaration
Swift
func makeDatatypes(sortNames: [Z3Symbol], constructorLists: [Z3ConstructorList]) -> [Z3Sort]
Parameters
sortNames
names of datatype sorts.
constructorLists
list of constructors, one list per sort.
Return Value
array of datatype sorts
-
Query constructor for declared functions.
Seealso
makeConstructor
Declaration
Swift
func queryConstructor(constructor: Z3Constructor, numFields: UInt32) -> (constructor: Z3FuncDecl, tester: Z3FuncDecl, accessors: [Z3FuncDecl])
Parameters
constr
constructor container. The container must have been passed in to a
makeDatatype
call.numFields
number of accessor fields in the constructor.
Return Value
A tuple containing:
constructor
: constructor function declaration, allocated by user.tester
: constructor test function declaration, allocated by user.accessors
: array of accessor function declarations allocated by user. The array containsnumFields
elements.
-
Returns whether
sort
is a sequence sort.Declaration
Swift
func isSeqSort(_ sort: Z3Sort) -> Bool
-
Check if
sort
is a regular expression sort.Declaration
Swift
func isReSort(_ sort: Z3Sort) -> Bool
-
Create a sort for unicode strings.
The sort for characters can be changed to ASCII by setting the global parameter
encoding
toascii
, or alternatively to 16 bit characters by settingencoding
tobmp
.Declaration
Swift
func stringSort() -> Z3Sort
-
Check if
sort
is a string sort.Declaration
Swift
func isStringSort(_ sort: Z3Sort) -> Bool
-
Create a sort for unicode characters.
The sort for characters can be changed to ASCII by setting the global parameter encoding to ascii, or alternative to 16 bit characters by setting encoding to bmp.
Declaration
Swift
func charSort() -> Z3Sort
-
Check if
sort
is a character sort.Declaration
Swift
func isCharSort(_ sort: Z3Sort) -> Bool
-
Create a string constant out of the string that is passed in The string may contain escape encoding for non-printable characters or characters outside of the basic printable ASCII range. For example, the escape encoding
\\u{0}
represents the character 0 and the encoding\\u{100}
represents the character 256.Declaration
Swift
func makeString(_ value: String) -> Z3String
-
Determine if
ast
is a string constant.Declaration
Swift
func isString(_ ast: Z3AstBase) -> Bool
-
Unsigned bit-vector to string conversion.
Declaration
Swift
func makeUbvToStr<Sort>(_ ast: Z3BitVector<Sort>) -> Z3String where Sort : BitVectorSort
-
Unsigned bit-vector to string conversion.
Declaration
Swift
func makeUbvToStr(_ ast: AnyZ3BitVector) -> Z3String
-
ned bit-vector to string conversion.
Declaration
Swift
func makeSbvToStr<Sort>(_ ast: Z3BitVector<Sort>) -> Z3String where Sort : BitVectorSort
-
ned bit-vector to string conversion.
Declaration
Swift
func makeSbvToStr(_ ast: AnyZ3BitVector) -> Z3String
-
Create a Z3 symbol using an integer.
Symbols are used to name several term and type constructors.
NB. Not all integers can be passed to this function. The legal range of unsigned integers is 0 to 2^30-1.
Seealso
getSymbolInt
Seealso
makeStringSymbol
Declaration
Swift
func makeIntSymbol(_ i: Int32) -> Z3Symbol
-
Create a Z3 symbol using a C string.
Symbols are used to name several term and type constructors.
Seealso
getSymbolString
Seealso
makeIntSymbol
Declaration
Swift
func makeStringSymbol(_ s: String) -> Z3Symbol
-
Return a tactic associated with the given name.
The complete list of tactics may be obtained using the procedures
getNumTactics
andgetTacticName
. It may also be obtained using the command(help-tactic)
in the SMT 2.0 front-end.Tactics are the basic building block for creating custom solvers for specific problem domains.
Throws
Ifname
is not a valid/known tactic name.Declaration
Swift
func makeTactic(name: String) throws -> Z3Tactic
-
Return the number of builtin tactics available in Z3.
Declaration
Swift
func getNumTactics() -> UInt32
-
Return the name of the idx tactic.
Precondition
index < getNumTactics()
Declaration
Swift
func getTacticName(index: UInt32) -> String
-
Return a string containing a description of the tactic with the given name.
Declaration
Swift
func getTacticDescription(name: String) -> String
-
Return a tactic that just return the given goal.
Declaration
Swift
func tacticSkip() -> Z3Tactic
-
Return a tactic that always fails.
Declaration
Swift
func tacticFail() -> Z3Tactic
-
Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false).
Declaration
Swift
func tacticFailIfNotDecided() -> Z3Tactic
-
Return a probe associated with the given name. The complete list of probes may be obtained using the methods
probeCount
andprobeName(_:)
. It may also be obtained using the command(help-tactic)
in the SMT 2.0 front-end.Declaration
Swift
func probe(named name: String) -> Z3Probe
-
Return a probe that always evaluates to
value
.Declaration
Swift
func probeConst(_ value: Double) -> Z3Probe
-
Return the name of the tactic of index
index
.Precondition
index < self.tacticCount
Declaration
Swift
func tacticName(atIndex index: UInt32) -> String
-
Return the name of the probe of index
index
.Precondition
index < self.probeCount
Declaration
Swift
func probeName(atIndex index: UInt32) -> String
-
Return a string containing a description of the tactic with the given name.
Declaration
Swift
func tacticDescription(tacticName: String) -> String
-
Return a string containing a description of the probe with the given name.
Declaration
Swift
func probeDescription(probeName: String) -> String