Expr class abstract

Inheritance

• Object
• AST
• Expr

Implementers

• App
• ArrayMap
• ArraySelect
• ArrayStore
• AsArray
• BinaryOp
• BoundVar
• BvExtract
• BvToInt
• Char
• ConstArray
• Divides
• EmptySeq
• EmptySet
• FullSet
• NaryOp
• NullaryOp
• Numeral
• Pat
• PbAtLeast
• PbAtMost
• PbEq
• PUnaryOp
• Quantifier
• QuaternaryOp
• ReAllchar
• ReEmpty
• ReFull
• ReLoop
• RePower
• Str
• TernaryOp
• UnaryOp
• UnitSeq
• Unknown

Available extensions

• ASTExtension
• ExprExtension

Constructors

Expr.new()

Properties

hashCode → int

The hash code for this object.

no setter, inherited

runtimeType → Type

A representation of the runtime type of the object.

no setter, inherited

Methods

between(Object a, Object b) → Expr

Available on Expr, provided by the ExprExtension extension

betweenIn(Object a, Object b) → Expr

Available on Expr, provided by the ExprExtension extension

build(Context c) → Z3_ast

inherited

declare() → A

Available on A, provided by the ASTExtension extension

eq(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

iff(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

implies(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

noSuchMethod(Invocation invocation) → dynamic

Invoked when a nonexistent method or property is accessed.

inherited

notEq(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

thenElse(Object a, Object b) → Expr

Available on Expr, provided by the ExprExtension extension

to<T>() → T

Available on Expr, provided by the ExprExtension extension

toBigInt() → BigInt

Available on Expr, provided by the ExprExtension extension

toBool() → bool

Available on Expr, provided by the ExprExtension extension

toDouble() → double

Available on Expr, provided by the ExprExtension extension

toInt() → int

Available on Expr, provided by the ExprExtension extension

toRat() → Rat

Available on Expr, provided by the ExprExtension extension

toString() → String

A string representation of this object.

inherited

Operators

operator %(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator &(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator *(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator +(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator -(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator /(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator <(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator <=(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator ==(Object other) → bool

The equality operator.

inherited

operator >(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator >=(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator [](Object index) → Expr

Available on Expr, provided by the ExprExtension extension

operator ^(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator unary-() → Expr

Available on Expr, provided by the ExprExtension extension

operator |(Object other) → Expr

Available on Expr, provided by the ExprExtension extension

operator ~() → Expr

Available on Expr, provided by the ExprExtension extension