Packages

object SimpleAPI

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

Type Members

  1. class SimpleAPIException extends Exception
  2. class SimpleAPIForwardedException extends SimpleAPIException

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 COMMON_PART_NR: Int
    Attributes
    protected[api]
  5. def apply(enableAssert: Boolean = false, sanitiseNames: Boolean = true, dumpSMT: Boolean = false, smtDumpBasename: String = SMTDumpBasename, dumpScala: Boolean = false, scalaDumpBasename: String = ScalaDumpBasename, dumpDirectory: File = null, tightFunctionScopes: Boolean = true, genTotalityAxioms: Boolean = false, randomSeed: Option[Int] = Some(1234567), otherSettings: GlobalSettings = GlobalSettings.DEFAULT): SimpleAPI

    Create a new prover.

    Create a new prover. Note that the prover has to be shut down explicitly by calling the method SimpleAPI.shutDown after use.

  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  10. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  11. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  12. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  13. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  15. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @HotSpotIntrinsicCandidate() @native()
  16. def pp(f: IExpression): String

    Pretty-print a formula or term.

  17. def smtPP(f: IExpression): String

    Pretty-print a formula or term in SMT-LIB format.

  18. def spawn: SimpleAPI
  19. def spawnNoSanitise: SimpleAPI
  20. def spawnWithAssertions: SimpleAPI
  21. def spawnWithAssertionsLogNoSanitise(basename: String, directory: File): SimpleAPI
  22. def spawnWithAssertionsNoSanitise: SimpleAPI
  23. def spawnWithLog(basename: String, directory: File): SimpleAPI
  24. def spawnWithLog(basename: String): SimpleAPI
  25. def spawnWithLog: SimpleAPI
  26. def spawnWithLogNoSanitise(basename: String, directory: File): SimpleAPI
  27. def spawnWithScalaLog: SimpleAPI
  28. def spawnWithScalaLogNoSanitise(basename: String): SimpleAPI
  29. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  30. def toString(): String
    Definition Classes
    AnyRef → Any
  31. val version: String
  32. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  33. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  34. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  35. def withProver[A](enableAssert: Boolean = false, sanitiseNames: Boolean = true, dumpSMT: Boolean = false, smtDumpBasename: String = SMTDumpBasename, dumpScala: Boolean = false, scalaDumpBasename: String = ScalaDumpBasename, dumpDirectory: File = null, tightFunctionScopes: Boolean = true, genTotalityAxioms: Boolean = false, randomSeed: Option[Int] = Some(1234567), otherSettings: GlobalSettings = GlobalSettings.DEFAULT)(f: (SimpleAPI) => A): A

    Run the given function with a fresh prover, and shut down the prover afterwards.

  36. def withProver[A](f: (SimpleAPI) => A): A

    Run the given function with a fresh prover, and shut down the prover afterwards.

  37. object FunctionalityMode extends Enumeration
  38. object NoModelException extends SimpleAPIException
  39. object ProverStatus extends Enumeration
  40. object TimeoutException extends SimpleAPIException

Deprecated Value Members

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

    (Since version 9)

Inherited from AnyRef

Inherited from Any

Ungrouped