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, dbgPrintStreams: Boolean, asserts: Seq[(String, AssertType.Value)], timeout: Option[Int])

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. def allUnresolved(): Unresolved

    Get all the unresolved values

  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. val asserts: Seq[(String, AssertType.Value)]
  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 core: Specification
  13. implicit val ctx: Context
  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  16. def errFreeInput(ex: TyExpr[Expr]): Unit

    Recursively mark an expression and all subexpressions as error-free input stream.

    Recursively mark an expression and all subexpressions as error-free input stream. All Datastructures are bound by inStreamBound

  17. val eventIdx: Range
  18. val eventList: LazyList[Int]
  19. def genLiftedOp(name: ValueId, _out: TyArray, op: String, _args: Seq[ValueId]): Unit
  20. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  21. def hasEvent(evt: TyExpr[Expr]): BoolExpr

    check whether an expression has an element, i.e.

    check whether an expression has an element, i.e. neither None nor †.

  22. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  23. val ifDecisions: HashMap[(ValueId, Side.Value), BoolExpr]
  24. val inStreamBound: Int
  25. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  26. def isOk(evt: TyExpr[Expr]): BoolExpr

    check whether an expression is ok.

    check whether an expression is ok. The inverse of isError.

  27. def iterateList(size: Int, name: String, list: Expr): Seq[Expr]
  28. def iterateListElements(size: Int, name: String, list: Expr): Seq[Expr]
  29. def last(out: TyArray, values: TyArray, clock: TyArray): Unit
  30. var lastTestCases: Seq[TestCase]
  31. def liftValue(value: ValueOrError, ty: Type, prefix: String): TyExpr[Expr]
  32. def liftValueInner(value: ValueOrError, ty: Type, prefix: String): Option[TyExpr[Expr]]
  33. def member(expr: Expr, ty: Type, member: String): Expr
  34. def merge(i: Int, _out: TyArray, _fst: TyArray, _snd: TyArray): Unit
  35. def mkBoolArray(name: String): BoolArray
  36. def mkEq(a: Expr, b: Expr): BoolExpr
  37. def mkEq(a: TyExpr[Expr], b: TyExpr[Expr]): BoolExpr
  38. def mkFresh(ty: Type, name: String): TyArray
  39. def mkITE[E <: Expr](cond: TyExpr[BoolExpr], l: TyExpr[E], r: TyExpr[E]): TyExpr[E]
  40. def mkITE[E <: Expr](cond: TyExpr[BoolExpr], l: E, r: E): E
  41. def mkIntArray(name: String): IntArray
  42. def mkTyArray(name: Id, ty: Type): TyArray
  43. def mkTyValArray(name: String, ty: Type): LazyList[TyExpr[Expr]]
  44. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  45. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  46. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  47. val numEvents: Int
  48. val panics: ArrayBuffer[(Id, String)]
  49. val sizes: Map[Id, Stream[Sized]]
  50. val solver: SolverInterface
  51. val solverType: Strategy.Value
  52. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  53. val timeout: Option[Int]
  54. val times: LazyList[TyExpr[IntExpr]]
  55. def toString(): String
    Definition Classes
    AnyRef → Any
  56. val typeArrays: HashMap[Id, TyArray]
  57. val types: Map[ValueId, Type]
  58. def unique(s: String): String
  59. var unresolved: Unresolved

    unresolved stores all unresolved constraints.

  60. implicit val vargen: TyExprGen
  61. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  62. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  63. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  64. def withCoverage[A](setConstraints: ⇒ Unit)(withModel: (Model) ⇒ A): Option[A]
  65. object Z3LazyErr
  66. object Z3List
  67. object Z3Option

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