case class Z3ASTWrapper[+A >: BottomSort <: TopSort] extends Tree[A] with Product with Serializable
This class is used to bridge the gap between non-DSL Z3ASTs and DSL ASTs. There are two important things to check: that the Z3Context is the correct one (when the DSL tree actually gets converted), and that the sort is the advertised one. This second check is currently not performed. It will need to be a runtime check that can happen through an implicit "checker" parameter.
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- Z3ASTWrapper
- Serializable
- Serializable
- Product
- Equals
- Tree
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- All
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
ast(z3: Z3Context): Z3AST
- Definition Classes
- Z3ASTWrapper → Tree
- val ast: Z3AST
-
def
build(z3: Z3Context): Z3AST
- Definition Classes
- Z3ASTWrapper → Tree
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )