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, 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 BITWISE_OPS_BITS: Int

    The number of bits an integer has for bitwise operators.

  5. def allUnresolved(): Unresolved

    Get all the unresolved values

  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def build(): Unit

    Create a Z3 formula from specification.

  8. val calledFrom: HashMap[(ValueId, Int, FunctionId), Int]
  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate() @throws( ... )
  10. def constrain(ex: BoolExpr*): Unit
  11. val core: Specification
  12. implicit 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 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

  16. val eventIdx: Range
  17. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  18. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  19. val ifDecisions: HashMap[IfId, BoolExpr]
  20. val inStreamBound: Int
  21. val inputRanges: Map[Id, Range]
  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. def restrictList(size: Int, name: String, list: Expr): BoolExpr
  42. val sizes: DatastructureSize
  43. val solver: SolverInterface
  44. val solverType: Strategy.Value
  45. val stats: Statistics
  46. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  47. val timeout: Option[Int]
  48. val times: IndexedSeq[TyExpr[IntExpr]]
  49. def toString(): String
    Definition Classes
    AnyRef → Any
  50. val typeArrays: HashMap[Id, TyArray[Expr]]
  51. def unique(s: String): String
  52. var unresolved: Unresolved

    unresolved stores all unresolved constraints.

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