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: Map[String, AssertType.Value], timeout: Option[Int], stats: Statistics)

Type Members

  1. case class Function(id: FunctionId, fn: FunctionExpr, spec: Specification, called: TyArray[BoolExpr]) extends Product with Serializable

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: Map[String, AssertType.Value]
  8. def build(): Unit

    Create a Z3 formula from specification.

  9. var calledFrom: HashMap[(ValueId, Int, FunctionId), Int]
  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. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  19. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  20. val ifDecisions: HashMap[IfId, BoolExpr]
  21. val inStreamBound: Int
  22. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  23. def iterateList(size: Int, name: String, list: Expr): Seq[Expr]
  24. def iterateListElements(size: Int, name: String, list: Expr): Seq[Expr]
  25. def last[A <: Expr, B <: Expr](out: TyArray[A], values: TyArray[A], clock: TyArray[B]): Unit
  26. def liftValue(value: ValueOrError, ty: Type, prefix: String): TyExpr[Expr]
  27. def liftValueInner(value: ValueOrError, ty: Type, prefix: String): Option[TyExpr[Expr]]
  28. def member(expr: Expr, ty: Type, member: String): Expr
  29. def merge(i: Int, _out: TyArray[Expr], _fst: TyArray[Expr], _snd: TyArray[Expr]): Unit
  30. def mkBoolArray(name: String): TyArray[BoolExpr]
  31. def mkEq(a: Expr, b: Expr): BoolExpr
  32. def mkEq(a: TyExpr[Expr], b: TyExpr[Expr]): BoolExpr
  33. def mkITE[E <: Expr](cond: TyExpr[BoolExpr], l: E, r: E): E
  34. def mkIntArray(name: String): TyArray[IntExpr]
  35. def mkTyArray[T <: Expr](name: Id, ty: Type): TyArray[T]
  36. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  37. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  38. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  39. val numEvents: Int
  40. val panics: ArrayBuffer[(Id, String)]
  41. val sizes: DatastructureSize
  42. val solver: SolverInterface
  43. val solverType: Strategy.Value
  44. val stats: Statistics
  45. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  46. val timeout: Option[Int]
  47. val times: IndexedSeq[TyExpr[IntExpr]]
  48. def toString(): String
    Definition Classes
    AnyRef → Any
  49. val typeArrays: HashMap[Id, TyArray[Expr]]
  50. def unique(s: String): String
  51. var unresolved: Unresolved

    unresolved stores all unresolved constraints.

  52. implicit val vargen: TyExprGen
  53. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  54. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  55. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  56. def warn(s: String*): Unit
  57. def warn(s: String, loc: Location): Unit
  58. def warnings: Seq[String]
  59. def withCoverage[A](setConstraints: ⇒ Unit)(withModel: (Model) ⇒ A): Solution[A]
  60. object IfDecisions
  61. object Z3LazyErr
  62. object Z3List
  63. object Z3Option
  64. object functions

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