z3
library
Functions
$ (Object e → Expr
Convert a Dart value to an Expr .
$s <T > ()
→ Sort
Convert a Dart Type to a Sort .
abs (Expr x , [Sort ?sort → Expr
add (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
addN (Iterable <Expr args → NaryOp
and (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
andN (Iterable <Expr args → NaryOp
app (FuncDecl decl , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → App
appN (FuncDecl decl , Iterable <Expr args → App
arrayDefault (Expr x → Expr
arrayMap (FuncDecl f , Iterable <Expr arrays → ArrayMap
arraySort (Sort domain , Sort range → ArraySort
The type of an array from indices of type domain to elements of type
range.
arraySortN (List <Sort domain , Sort range → ArraySort
The type of an array from indices of types domain to elements of type
range.
arrayStore (Expr x , Expr index , Expr value → ArrayStore
arrayStoreN (Expr array , Iterable <Expr indices , Expr value → ArrayStore
astToString (AST ast → String
Prints an AST to a string.
benchmarkToSmtlib ({required String name , required String logic , required String status , required String attributes , required Iterable <AST assumptions , required AST formula → String
Convert the given benchmark into a SMT-LIB string.
bitToBool (Expr x , int y → PUnaryOp
boundVar (int index , Sort sort → BoundVar
Creates a de-Bruijn indexed BoundVar expression for use in quantifiers.
bvAdd (Expr x , Expr y → BinaryOp
bvAddNoOverflow (Expr x , Expr y , {required bool signed → Expr
bvAddNoUnderflow (Expr x , Expr y → Expr
bvAnd (Expr x , Expr y → BinaryOp
bvAshr (Expr x , Expr y → BinaryOp
bvBig (BigInt value , BitVecSort sort → BitVecNumeral
Creates a BitVecNumeral from a BigInt value.
bvConcat (Expr x , Expr y → BinaryOp
bvFrom (int value , [int size = 64 → BitVecNumeral
Creates a BitVecNumeral from an int value.
bvLshr (Expr x , Expr y → BinaryOp
bvMul (Expr x , Expr y → BinaryOp
bvMulNoOverflow (Expr x , Expr y , {required bool signed → Expr
bvNand (Expr x , Expr y → BinaryOp
bvNeg (Expr x → UnaryOp
bvNegNoOverflow (Expr x → Expr
bvNor (Expr x , Expr y → BinaryOp
bvNot (Expr x → UnaryOp
bvOr (Expr x , Expr y → BinaryOp
bvRedAnd (Expr x → UnaryOp
bvRedOr (Expr x → UnaryOp
bvRotl (Expr x , Expr y → BinaryOp
bvRotr (Expr x , Expr y → BinaryOp
bvSdiv (Expr x , Expr y → BinaryOp
bvSdivNoOverflow (Expr x , Expr y → Expr
bvSge (Expr x , Expr y → BinaryOp
bvSgt (Expr x , Expr y → BinaryOp
bvShl (Expr x , Expr y → BinaryOp
bvSignExt (Expr x , int y → PUnaryOp
bvSle (Expr x , Expr y → BinaryOp
bvSlt (Expr x , Expr y → BinaryOp
bvSmod (Expr x , Expr y → BinaryOp
bvSMulNoUnderflow (Expr x , Expr y → BinaryOp
bvSort (int width → BitVecSort
The type of a bit-vector with the given width.
bvSrem (Expr x , Expr y → BinaryOp
bvSub (Expr x , Expr y → BinaryOp
bvSubNoOverflow (Expr x , Expr y → Expr
bvSubNoUnderflow (Expr t1 , Expr t2 , {required bool signed → Expr
bvToChar (Expr x → Expr
bvToInt (Expr x , {bool signed = false → BvToInt
bvUdiv (Expr x , Expr y → BinaryOp
bvUge (Expr x , Expr y → BinaryOp
bvUgt (Expr x , Expr y → BinaryOp
bvUle (Expr x , Expr y → BinaryOp
bvUlt (Expr x , Expr y → BinaryOp
bvUrem (Expr x , Expr y → BinaryOp
bvXnor (Expr x , Expr y → BinaryOp
bvXor (Expr x , Expr y → BinaryOp
bvZeroExt (Expr x , int y → PUnaryOp
char (int value → Char
Create a Char expression from code point.
charIsDigit (Expr x → Expr
charLe (Expr x , Expr y → BinaryOp
charToBv (Expr x → Expr
charToInt (Expr x → Expr
codeToStr (Expr x → Expr
constArray (Sort sort , Expr value → ConstArray
Creates a constant array such that all elements are equal to value.
constructor (String name , Map <String Sort fields → Constructor
Creates a constructor used in a datatype declaration.
constVar (String name , Sort sort → ConstVar
Creates a ConstVar variable expression.
datatypeSort (String name , Iterable <Constructor constructors → DatatypeSort
The type of a datatype with the given name and constructors.
declare <A extends AST > (A ast → A
Declare an AST element in the current context, for most AST elements this
is not necessary as they are automatically declared when constructed.
declareDatatype (String name , Iterable <Constructor constructors → DatatypeInfo
Declare a datatype with the given name and constructors.
declareDatatypes (Map <String Iterable <Constructor datatypes → Map <String DatatypeInfo
Declare mutually recursive datatypes given a map from their name to their
constructors.
declareEnum (String name , Iterable <String elements → EnumInfo
Declares an enum with the given name and elements.
declareEnumValues (List <Enum values → EnumInfo
Declares an enum with the given values.
declareList (String name , Sort element → ListInfo
Declares a list with the given name and element type.
declareMaybe (Sort sort , {String ?name → MaybeInfo
Declares a datatype with a nothing and just constructor for the given
sort, similar to the Haskell Maybe type.
declareTuple (String name , Iterable <Sort sorts → TupleInfo
Declares a tuple with the given name and sorts, the fields of the
tuple are named name$0, name$1, etc.
declareTupleNamed (String name , Map <String Sort fields → TupleInfo
Declares a tuple with the given name and fields, like declareTuple
but the fields are explicitly named.
defineRecursiveFunc (RecursiveFunc func , Expr body → void
Define the body of a recursive function declared using recursiveFunc .
distinct (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
distinctN (Iterable <Expr args → NaryOp
div (Expr x , Expr y → BinaryOp
divides (int x , Expr y → Divides
Create a division predicate that is true if x divides y.
emptySeq (Sort sort → EmptySeq
Creates an empty Seq expression.
emptySet (Sort sort → EmptySet
eq (Expr x , Expr y → BinaryOp
eval (String str → String
Evaluate an SMT-LIB string, returning the result as a string.
exists (List <ConstVar bound , Expr body , {Expr ?when , int weight = 0 , List <Pat patterns = const [] , List <Expr noPatterns = const [] , Sym ?id , Sym ?skolem → Exists
Creates a Exists quantifier.
existsIndexed (Map <String Sort args , Expr body , {Expr ?when , int weight = 0 , Iterable <Pat patterns = const [] , Iterable <Expr noPatterns = const [] , String ?id , String ?skolem → Exists
Creates a Exists quantifier, like exists but arguments must manually
de-Bruijn indexed.
finiteDomainSort (String name , int size → FiniteDomainSort
The type of a finite domain with the given size, for use in the Datalog
engine.
float (num value , FloatSort sort → FloatNumeral
Creates a FloatNumeral from a num value.
float128 (num value → FloatNumeral
Creates a FloatNumeral from a num value.
float16 (num value → FloatNumeral
Creates a FloatNumeral from a num value.
float32 (num value → FloatNumeral
Creates a FloatNumeral from a num value.
float64 (num value → FloatNumeral
Creates a FloatNumeral from a num value.
floatSort (int ebits , int sbits → FloatSort
The type of a floating point number with the given ebits exponent bits and
sbits significand bits.
forall (List <ConstVar bound , Expr body , {Expr ?when , int weight = 0 , List <Pat patterns = const [] , List <Expr noPatterns = const [] , Sym ?id , Sym ?skolem → Forall
Creates a Forall quantifier.
forallIndexed (Map <String Sort args , Expr body , {Expr ?when , int weight = 0 , Iterable <Pat patterns = const [] , Iterable <Expr noPatterns = const [] , String ?id , String ?skolem → Forall
Creates a Forall quantifier, like forall but arguments must manually
de-Bruijn indexed.
forwardRefSort (String name → ForwardRefSort
A forward reference to a datatype with the given name, used in recursive
datatypes.
fpaAbs (Expr x → Expr
fpaAdd (Expr x , Expr y → TernaryOp
fpaDiv (Expr x , Expr y → TernaryOp
fpaEq (Expr x , Expr y → BinaryOp
fpaFma (Expr x , Expr y , Expr z , Expr w → QuaternaryOp
fpaFp (Expr sgn , Expr exp , Expr sig → TernaryOp
fpaGeq (Expr x , Expr y → BinaryOp
fpaGt (Expr x , Expr y → BinaryOp
fpaIsInfinite (Expr x → Expr
fpaIsNaN (Expr x → Expr
fpaIsNegative (Expr x → Expr
fpaIsNormal (Expr x → Expr
fpaIsPositive (Expr x → Expr
fpaIsSubnormal (Expr x → Expr
fpaIsZero (Expr x → Expr
fpaLeq (Expr x , Expr y → BinaryOp
fpaLt (Expr x , Expr y → BinaryOp
fpaMax (Expr x , Expr y → BinaryOp
fpaMin (Expr x , Expr y → BinaryOp
fpaMul (Expr x , Expr y → TernaryOp
fpaNeg (Expr x → Expr
fpaRem (Expr x , Expr y → BinaryOp
fpaSqrt (Expr x , Expr y → BinaryOp
fpaSub (Expr x , Expr y → TernaryOp
fpaToIeeeBv (Expr x → Expr
fpaToReal (Expr x → Expr
fullSet (Sort sort → FullSet
func (String name , Iterable <Sort domain , Sort range → Func
Declare an uninterpreted function with the given name, domain, and
range.
funcAsArray (FuncDecl f → AsArray
funcDeclsEqual (FuncDecl a , FuncDecl b → bool
Check if two FuncDecl s are equal.
ge (Expr x , Expr y → BinaryOp
getDatatypeInfo (DatatypeSort sort → DatatypeInfo
Gets the DatatypeInfo for the given sort.
getExprApp (Expr expr → App ?
Get the App representing an expression, this gives you access to the
underlying FuncDecl and parameters.
getSort <A extends Sort > (Expr value → A
Get the sort of an Expr .
getSortName (Sort sort → String
Get the name of a Sort .
gt (Expr x , Expr y → BinaryOp
iff (Expr x , Expr y → BinaryOp
ifThenElse (Expr x , Expr y , Expr z → TernaryOp
implies (Expr x , Expr y → BinaryOp
indexRefSort (int index → IndexRefSort
A reference to a datatype at the index index, only used in recursive
datatypes.
intBig (BigInt value → IntNumeral
Creates an IntNumeral from a BigInt value.
intFrom (int value → IntNumeral
Creates an IntNumeral from an int value.
intToBv (Expr x , int y → PUnaryOp
intToReal (Expr x → UnaryOp
intToStr (Expr x → Expr
isInt (Expr x → UnaryOp
ite (Expr x , Expr y , Expr z → TernaryOp
lambda (Iterable <ConstVar args , Expr body → Lambda
Creates a Lambda quantifier.
lambdaIndexed (Map <String Sort args , Expr body → Lambda
Creates a Lambda quantifier, like lambda but arguments must manually
de-Bruijn indexed.
le (Expr x , Expr y → BinaryOp
lt (Expr x , Expr y → BinaryOp
mod (Expr x , Expr y → BinaryOp
mul (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
mulN (Iterable <Expr args → NaryOp
not (Expr x → UnaryOp
notEq (Expr x , Expr y → UnaryOp
optimize ({Map <String Object params = const {} → Optimize
Create an optimization context.
or (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
orN (Iterable <Expr args → NaryOp
params ([Map <String Object params = const {} → Params
Create configuration parameters for various components of Z3.
parse (String str , {Map <String Sort sorts = const {} , Map <String FuncDecl decls = const {} → List <AST
Parse a SMT-LIB string, returning all of its assertions.
parser ()
→ ParserContext
Create a context for parsing and evaluating SMT-LIB strings.
patN (Iterable <Expr terms → Pat
Creates a Pat which can be used in quantifiers.
pbAtLeast (Iterable <Expr args , int n → PbAtLeast
Create the pseudo-boolean relation p1 + p2 + ... + pn >= k.
pbAtMost (Iterable <Expr args , int n → PbAtMost
Create the pseudo-boolean relation p1 + p2 + ... + pn <= k.
pbEq (Map <Expr int args , int k → PbEq
Create the pseudo-boolean relation p1 + p2 + ... + pn = k.
pbGe (Map <Expr int args , int k → Expr
Create the pseudo-boolean relation p1 + p2 + ... + pn >= k.
pbLe (Map <Expr int args , int k → Expr
Create the pseudo-boolean relation p1 + p2 + ... + pn <= k.
pow (Expr x , Expr y → BinaryOp
probe (double value → Probe
Create a constant probe that always evaluates to value.
rat (Rat rat → RatNumeral
Creates a RatNumeral from a Rat value.
ratFrom (int n , [int d = 1 → RatNumeral
Creates a RatNumeral from int numerator and denominator values.
reAllchar (Sort sort → ReAllchar
Create a regular expression that accepts all singleton sequences of the
regular expression sort.
realToInt (Expr x → UnaryOp
reComplement (Expr x → Expr
reConcat (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
reConcatN (Iterable <Expr args → NaryOp
recursiveFunc (String name , Iterable <Sort domain , Sort range , Expr ?body → RecursiveFunc
Declare a recursive function with the given name, domain, and range.
reDiff (Expr x , Expr y → BinaryOp
reEmpty (Sort sort → ReEmpty
The regular expression of sort sort rejecting every sequence.
reFull (Sort sort → ReFull
The regular expression of sort sort accepting every sequence.
reIntersect (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
reIntersectN (Iterable <Expr args → NaryOp
reLoop (Expr expr , int low , int high → ReLoop
Create a regular expression loop. The supplied regular expression expr is
repeated between low and high times. The low should be below high
with one exception: when supplying the value high as 0, the meaning is to
repeat the argument expr at least low number of times, and with an
unbounded upper bound.
rem (Expr x , Expr y → BinaryOp
reOption (Expr x → Expr
repeat (Expr x , int y → PUnaryOp
rePlus (Expr x → Expr
rePower (Sort sort , int n → RePower
Regular expression power. (?)
reRange (Expr x , Expr y → BinaryOp
reSort (Sort sort → ReSort
The type of a regular expression of sequences of elements of type sort.
reStar (Expr x → Expr
reUnion (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
reUnionN (Iterable <Expr args → NaryOp
root (Expr x , Expr n → Expr
Get the algebraic nth root of x.
rotateLeft (Expr x , int y → PUnaryOp
rotateRight (Expr x , int y → PUnaryOp
sbvToInt (Expr x , {bool signed = true → BvToInt
sbvToStr (Expr x → Expr
select (Expr x , Expr index → ArraySelect
selectN (Expr array , Iterable <Expr indices → ArraySelect
seqAt (Expr x , Expr y → BinaryOp
seqConcat (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
seqConcatN (Iterable <Expr args → NaryOp
seqContains (Expr x , Expr y → BinaryOp
seqIndex (Expr x , Expr y , Expr z → TernaryOp
seqInRe (Expr x , Expr y → BinaryOp
seqLastIndex (Expr x , Expr y → BinaryOp
seqLength (Expr x → Expr
seqNth (Expr x , Expr y → BinaryOp
seqPrefix (Expr x , Expr y → BinaryOp
seqReplace (Expr x , Expr y , Expr z → TernaryOp
seqSort (Sort sort → SeqSort
The type of a sequence of elements of type sort.
seqSuffix (Expr x , Expr y → BinaryOp
seqToRe (Expr x → Expr
seqUnit (Expr x → Expr
setAdd (Expr x , Expr y → Expr
setASTPrintMode (ASTPrintMode mode → void
Sets the ASTPrintMode of the current context used in astToString and
some other places.
setComplement (Expr x → Expr
setDel (Expr x , Expr y → Expr
setDifference (Expr x , Expr y → BinaryOp
setIntersect (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
setIntersectN (Iterable <Expr args → NaryOp
setMember (Expr x , Expr y → ArraySelect
setSort (Sort domain → SetSort
The sort of a set of elements of type domain.
setSubset (Expr x , Expr y → BinaryOp
setUnion (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
setUnionN (Iterable <Expr args → NaryOp
simpleSolver ()
→ Solver
Create a simple incremental solver.
simplify <A extends Expr > (Expr expr , [Params ?params → A
Simplifies an expression using basic algebraic rules and constant folding.
solver ({LogicKind ?logic , Map <String Object params = const {} → Solver
Creates a solver.
sortsEqual (Sort a , Sort b → bool
Check if two Sort s are equal.
sqrt (Expr x → Expr
Get the algebraic square root of x.
store (Expr x , Expr y , Expr z → TernaryOp
str (String value → Str
Creates a Str expression.
strLe (Expr x , Expr y → BinaryOp
strLt (Expr x , Expr y → BinaryOp
strToCode (Expr x → Expr
strToInt (Expr x → Expr
sub (Expr x , [Expr ?x1 , Expr ?x2 , Expr ?x3 , Expr ?x4 , Expr ?x5 , Expr ?x6 , Expr ?x7 , Expr ?x8 , Expr ?x9 → NaryOp
subN (Iterable <Expr args → NaryOp
substitute <A extends Expr > (Expr ast , Map <Expr Expr substitutions → A
Substitutes expressions in expr where the keys of substitutions are
replaced with their corresponding values.
substituteFuncs <A extends Expr > (Expr expr , Map <FuncDecl Expr substitutions → A
Substitute the arguments to FuncDecl s in expr with the expressions in
to.
substituteVars <A extends Expr > (Expr expr , Iterable <Expr to → A
Substitute BoundVar s in expr with the expressions in to.
translateTo <A extends AST > (Context other , A ast → A
Translate the given AST element to another context.
ubvToStr (Expr x → Expr
unaryMinus (Expr x → UnaryOp
uninterpretedSort (String name → Sort
Create a free (uninterpreted) type with the given name.
unitSeq (Sort sort → UnitSeq
Creates a Seq expression with a single element.
updateTerm <A extends Expr > (A expr , Iterable <Expr args → A
Updates the arguments of an App , Lambda , Exists , or Forall .
withContext <T > (Context context , T fn ()→ T
Runs fn in the specified context.
xor (Expr x , Expr y → BinaryOp
z3GlobalAppendLog (File file → void
Append API interactions to the given file.
z3GlobalCloseLog ()
→ void
Stop logging API interactions.
z3GlobalDisableTrace (String tag → void
Disables tracing for the given tag.
z3GlobalEnableTrace (String tag → void
Enables tracing for the given tag.
z3GlobalGetEstimatedAllocatedMemory ()
→ int
Returns the estimated amount of allocated memory by Z3, in bytes.
z3GlobalOpenLog (File file → void
Log API interactions to the given file, clearing the previous contents.
z3GlobalWarningMessages (bool enabled → void
Enable or disable printing warning messages to the console.
Exceptions / Errors
ContextError
An error that can be thrown while performing an operation in a Context .
