final class GenZ3 extends AnyRef

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. GenZ3
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new GenZ3(solverType: Strategy.Value, core: Specification, numEvents: Int, print_streams: Boolean, asserts: Seq[(String, AssertType.Value)])

Type Members

  1. sealed class TestCase extends AnyRef
  2. final class TyStream extends AnyRef

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. val BITS: Int
  5. var allTypeArrays: HashMap[String, TyArray]
  6. def allUnresolved(): Unresolved

    Get all the unresolved values

  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. def avoidUB(ex: BoolExpr): Unit
  9. def build(): Unit

    Create a Z3 formula from specification.

  10. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate() @throws( ... )
  11. def constrain(ex: BoolExpr*): Unit
  12. val ctx: Context
  13. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  15. def evalExpr(expr: Expr, model: Model, ty: Type): String
  16. val eventIdx: Range
  17. def freshName(): String
  18. def genLiftedOp(name: ValueId, _out: TyArray, op: String, _args: Seq[ValueId]): Unit
  19. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  20. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  21. var ifDecisions: HashMap[(ValueId, Side.Value), BoolExpr]
  22. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  23. def isSat: Boolean
  24. def last(out: TyStream, values: TyStream, clock: TyStream): Unit
  25. var lastTestCases: Seq[TestCase]
  26. def liftValue(value: ValueOrError, ty: Type, prefix: String): TyExpr
  27. def member(expr: Expr, ty: Type, member: String): Expr
  28. def merge(out: TyStream, fst: TyStream, snd: TyStream): Unit
  29. def mkBoolArray(name: String): BoolArray
  30. def mkEq(a: TyExpr, b: TyExpr): BoolExpr
  31. def mkFresh(ty: Type): TyStream
  32. def mkITE[E <: Expr](cond: BoolExpr, l: E, r: E): E
  33. def mkIntArray(name: String): IntArray
  34. def mkTyArray(name: String, ty: Type): TyArray
  35. def mkTyStream(name: StreamId, ty: Type): TyStream
  36. def mkTyValArray(name: String, ty: Type): Array[TyExpr]
  37. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  38. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  39. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  40. def printFormula: String
  41. def print_ast(ast: Expr): String
  42. def run(): Solution[TestCase]

    Run the test gen.

    Run the test gen. Don't repeat on failure.

  43. val sizes: Map[Id, Stream[Int]]
  44. val solver: Strategy
  45. val solverType: Strategy.Value
  46. var streams: HashMap[StreamId, TyStream]
  47. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  48. var times: Array[Prim[IntExpr]]
  49. def toString(): String
    Definition Classes
    AnyRef → Any
  50. def typeArrays(v: ValueId): TyArray
  51. val types: Types
  52. def unique(s: String): String
  53. var unresolved: Unresolved

    unresolved stores all unresolved constraints.

  54. val vargen: TyExprGen
  55. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  56. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  57. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  58. object Z3List

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
    Deprecated

    (Since version ) see corresponding Javadoc for more information.

Inherited from AnyRef

Inherited from Any

Ungrouped