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)], 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. val ctx: Context
  14. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  15. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  16. val eventIdx: Range
  17. val eventList: LazyList[Int]
  18. def freshName(): String
  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 hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  22. val ifDecisions: HashMap[(ValueId, Side.Value), BoolExpr]
  23. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  24. def isSat: Boolean
  25. def last(out: TyArray, values: TyArray, clock: TyArray): Unit
  26. var lastTestCases: Seq[TestCase]
  27. def liftValue(value: ValueOrError, ty: Type, prefix: String): TyExpr
  28. def member(expr: Expr, ty: Type, member: String): Expr
  29. def merge(i: Int, out: TyArray, fst: TyArray, snd: TyArray): Unit
  30. def mkBoolArray(name: String): BoolArray
  31. def mkEq(a: TyExpr, b: TyExpr): BoolExpr
  32. def mkFresh(ty: Type): TyArray
  33. def mkITE[E <: Expr](cond: BoolExpr, l: E, r: E): E
  34. def mkIntArray(name: String): IntArray
  35. def mkTyArray(name: Id, ty: Type): TyArray
  36. def mkTyValArray(name: String, ty: Type): LazyList[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. val numEvents: Int
  41. def printFormula: String
  42. val sizes: Map[Id, Stream[Sized]]
  43. val solver: SolverInterface
  44. val solverType: Strategy.Value
  45. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  46. val timeout: Option[Int]
  47. val times: LazyList[Prim[IntExpr]]
  48. def toString(): String
    Definition Classes
    AnyRef → Any
  49. val typeArrays: HashMap[Id, TyArray]
  50. val types: Map[ValueId, Type]
  51. def unique(s: String): String
  52. var unresolved: Unresolved

    unresolved stores all unresolved constraints.

  53. 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 withCoverage[A](setConstraints: ⇒ Unit)(withModel: (Model) ⇒ A): Option[A]
  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