App class - z3 library

Constructors

App(FuncDecl decl, List<Expr> args): factory

Properties

args → List<Expr>: final
decl → FuncDecl: final
hashCode → int: The hash code for this object.
no setterinherited
runtimeType → Type: A representation of the runtime type of the object.
no setterinherited

Methods

between(Object a, Object b) → Expr: Available on Expr, provided by the ExprExtension extension
Create a predicate that checks if this expression is greater or equal to a and less than b.
betweenIn(Object a, Object b) → Expr: Available on Expr, provided by the ExprExtension extension
Create a predicate that checks if this expression is greater or equal to a and less than or equal to b.
build(Context c) → Z3_ast: override
declare() → A: Available on A, provided by the ASTExtension extension
Declare this AST element in the current context if it hasn't already.
eq(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Predicate that checks if this expression is equal to other.
iff(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Assert that this expression is true if and only if other is true.
implies(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Assert that if this expression is true other must also be true.
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
Predicate that checks if this expression is not equal to other.
thenElse(Object a, Object b) → Expr: Available on Expr, provided by the ExprExtension extension
If this is true then return then, otherwise return other.
to<T>() → T: Available on Expr, provided by the ExprExtension extension
Convert this expression to a T.
toBigInt() → BigInt: Available on Expr, provided by the ExprExtension extension
Convert this expression to a BigInt, requires that this expression is a Numeral.
toBool() → bool: Available on Expr, provided by the ExprExtension extension
Convert this expression to a bool, requires that this expression is either trueExpr or falseExpr.
toDouble() → double: Available on Expr, provided by the ExprExtension extension
Convert this expression to a double, requires that this expression is a Numeral.
toInt() → int: Available on Expr, provided by the ExprExtension extension
Convert this expression to an int, requires that this expression is a Numeral.
toMap() → Map<String, Expr>: Available on Expr, provided by the ExprExtension extension
Convert this expression to a Map, requires that this expression constructs a datatype.
toRat() → Rat: Available on Expr, provided by the ExprExtension extension
Convert this expression to a Rat, requires that this expression is a Numeral.
toString() → String: A string representation of this object.
override

Operators

operator %(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Arithmetic modulo operator. This is not an euclidean modulo, it is equivalent to the % operator in Dart.
operator &(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Boolean AND operator.
operator *(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Arithmetic multiplication operator.
operator +(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Arithmetic addition operator.
operator -(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Arithmetic subtraction operator.
operator /(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Arithmetic division operator.
operator <(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Predicate that checks if this expression is less than other.
operator <=(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Predicate that checks if this expression is less or equal to other.
operator ==(Object other) → bool: The equality operator.
inherited
operator >(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Predicate that checks if this expression is equal to other.
operator >=(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Predicate that checks if this expression is greater or equal to other.
operator [](Object index) → Expr: Available on Expr, provided by the ExprExtension extension
Indexes an array or tuple expression using the given index.
operator ^(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Boolean XOR operator.
operator unary-() → Expr: Available on Expr, provided by the ExprExtension extension
Negate this expression.
operator |(Object other) → Expr: Available on Expr, provided by the ExprExtension extension
Boolean OR operator.
operator ~() → Expr: Available on Expr, provided by the ExprExtension extension
Boolean NOT operator.