z3 library

Properties

boolSort → BoolSort
no setter
builtinProbes → Map<String, BuiltinProbe>
no setter
builtinTactics → Map<String, BuiltinTactic>
no setter
charSort → CharSort
no setter
currentContext → Context
no setter
falseExpr → NullaryOp
no setter
float128Sort → Float128Sort
no setter
float16Sort → Float16Sort
no setter
float32Sort → Float32Sort
no setter
float64Sort → Float64Sort
no setter
fpaRna → NullaryOp
no setter
fpaRne → NullaryOp
no setter
fpaRoundingModeSort → FpaRoundingModeSort
no setter
fpaRoundNearestTiesToAway → NullaryOp
no setter
fpaRoundNearestTiesToEven → NullaryOp
no setter
fpaRoundTowardNegative → NullaryOp
no setter
fpaRoundTowardPositive → NullaryOp
no setter
fpaRoundTowardZero → NullaryOp
no setter
fpaRtn → NullaryOp
no setter
fpaRtp → NullaryOp
no setter
fpaRtz → NullaryOp
no setter
intSort → IntSort
no setter
libz3Override ↔ DynamicLibrary?
getter/setter pair
realSort → RealSort
no setter
rootContext ↔ Context
getter/setter pair
simplifyParamDescriptions → ParamDescs
no setter
stringSort → StringSort
no setter
trueExpr → NullaryOp
no setter
z3GlobalFullVersion → String
final
z3GlobalVersion → Version
final

Functions

$(Object e) → Expr
$s<T>() → 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
arraySortN(List<Sort> domain, Sort range) → ArraySort
arrayStore(Expr x, Expr index, Expr value) → ArrayStore
arrayStoreN(Expr array, Iterable<Expr> indices, Expr value) → ArrayStore
astToString(AST ast) → String
benchmarkToSmtlib({required String name, required String logic, required String status, required String attributes, required Iterable<AST> assumptions, required AST formula}) → String
bitToBool(Expr x, int y) → PUnaryOp
boundVar(int index, Sort sort) → BoundVar
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
bvConcat(Expr x, Expr y) → BinaryOp
bvExtract(Expr x, int high, int low) → BvExtract
bvFrom(int value, [int size = 64]) → BitVecNumeral
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
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
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
constructor(String name, String recognizer, Map<String, Sort> fields) → Constructor
constVar(String name, Sort sort) → ConstVar
datatypeSort(String name, Iterable<Constructor> constructors) → DatatypeSort
declare<A extends AST>(A ast) → A
declareDatatype(String name, Iterable<Constructor> constructors) → DatatypeInfo
declareDatatypes(Map<String, Iterable<Constructor>> datatypes) → Map<String, DatatypeInfo>
declareEnum(String name, Iterable<String> elements) → EnumInfo
declareEnumValues(List<Enum> values) → EnumInfo
declareList(String name, Sort element) → ListInfo
declareTuple(String name, Iterable<Sort> sorts) → TupleInfo
declareTupleNamed(String name, Map<String, Sort> fields) → TupleInfo
defineRecursiveFunc(RecursiveFunc func, Expr body) → void
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
emptySeq(Sort sort) → EmptySeq
emptySet(Sort sort) → EmptySet
eq(Expr x, Expr y) → BinaryOp
eval(String str) → 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
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
finiteDomainSort(String name, int size) → FiniteDomainSort
float(num value, FloatSort sort) → FloatNumeral
float128(num value) → FloatNumeral
float16(num value) → FloatNumeral
float32(num value) → FloatNumeral
float64(num value) → FloatNumeral
floatSort(int ebits, int sbits) → FloatSort
forall(List<ConstVar> bound, Expr body, {Expr? when, int weight = 0, List<Pat> patterns = const [], List<Expr> noPatterns = const [], Sym? id, Sym? skolem}) → Forall
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
forwardRefSort(String name) → ForwardRefSort
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
funcAsArray(FuncDecl f) → AsArray
funcDeclsEqual(FuncDecl a, FuncDecl b) → bool
ge(Expr x, Expr y) → BinaryOp
getDatatypeInfo(DatatypeSort sort) → DatatypeInfo
getExprApp(Expr expr) → App?
getSort<A extends Sort>(Expr value) → A
getSortName(Sort sort) → String
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
intBig(BigInt value) → IntNumeral
intFrom(int value) → IntNumeral
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(Map<String, Sort> args, Expr body) → Lambda
lambdaConst(Iterable<ConstVar> args, Expr body) → Lambda
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() → Optimize
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
parse(String str, {Map<String, Sort> sorts = const {}, Map<String, FuncDecl> decls = const {}}) → List<AST>
parser() → ParserContext
patN(Iterable<Expr> terms) → Pat
pbAtLeast(Iterable<Expr> args, int n) → PbAtLeast
pbAtMost(Iterable<Expr> args, int n) → PbAtMost
pbEq(Map<Expr, int> args, int k) → PbEq
pbGe(Map<Expr, int> args, int k) → Expr
pbLe(Map<Expr, int> args, int k) → Expr
pow(Expr x, Expr y) → BinaryOp
probe(double value) → Probe
rat(Rat rat) → RatNumeral
ratFrom(int n, int d) → RatNumeral
reAllchar(Sort sort) → ReAllchar
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
reDiff(Expr x, Expr y) → BinaryOp
reEmpty(Sort sort) → ReEmpty
reFull(Sort sort) → ReFull
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(Sort sort, int low, int high) → ReLoop
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
reRange(Expr x, Expr y) → BinaryOp
reSort(Sort sort) → ReSort
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
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
seqExtract(Expr x, Expr y, Expr z) → TernaryOp
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
seqSuffix(Expr x, Expr y) → BinaryOp
seqToRe(Expr x) → Expr
seqUnit(Expr x) → Expr
setAdd(Expr x, Expr y) → Expr
setASTPrintMode(ASTPrintMode mode) → void
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
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
simplify<A extends Expr>(Expr ast, [Params? params]) → A
solver({LogicKind? logic, Map<String, Object> params = const {}}) → Solver
sortsEqual(Sort a, Sort b) → bool
sqrt(Expr x) → Expr
store(Expr x, Expr y, Expr z) → TernaryOp
str(String value) → Str
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 AST>(AST ast, Iterable<AST> from, Iterable<AST> to) → A
substituteFuncs<A extends AST>(AST ast, Iterable<FuncDecl> from, Iterable<AST> to) → A
substituteVars<A extends AST>(AST ast, Iterable<AST> to) → A
translateTo<A extends AST>(Context other, A ast) → A
ubvToStr(Expr x) → Expr
unaryMinus(Expr x) → UnaryOp
uninterpretedSort(String name) → Sort
unitSeq(Sort sort) → UnitSeq
updateTerm<A extends AST>(AST ast, Iterable<AST> args) → A
withContext<T>(Context context, T fn()) → T
xor(Expr x, Expr y) → BinaryOp
z3GlobalAppendLog(File file) → void
z3GlobalCloseLog() → void
z3GlobalDisableTrace(String tag) → void
z3GlobalEnableTrace(String tag) → void
z3GlobalGetEstimatedAllocatedMemory() → int
z3GlobalOpenLog(File file) → void
z3GlobalWarningMessages(bool enabled) → void

Typedefs

Parameter = Object

Exceptions / Errors

ContextError