z3

scala

package scala

Visibility
  1. Public
  2. All

Type Members

  1. trait Default [A] extends AnyRef

    A type class for Scala types that are representable in Z3 and that admit a default value.

  2. class ProceduralAttachment [T] extends Z3Theory

  3. class TheoryProxy extends AbstractTheoryProxy

    This class serves as a router for calls from Z3 to the Scala Z3Theory instances.

  4. class Z3AST extends AnyRef

    Attributes
    sealed

  5. class Z3ASTKind extends AnyRef

    Attributes
    sealed abstract

  6. case class Z3AppAST (decl: Z3FuncDecl, args: Seq[Z3AST]) extends Z3ASTKind with Product with Serializable

  7. class Z3Config extends AnyRef

    Attributes
    sealed

  8. class Z3Context extends AnyRef

    Attributes
    sealed

  9. class Z3FuncDecl extends AnyRef

    Attributes
    sealed

  10. class Z3Function extends AnyRef

    Attributes
    sealed

  11. case class Z3IntSymbol (value: Int) extends Z3SymbolKind[Int] with Product with Serializable

  12. class Z3Literals extends AnyRef

    Attributes
    sealed

  13. class Z3Model extends AnyRef

    Attributes
    sealed

  14. case class Z3NumeralAST (value: Option[Int]) extends Z3ASTKind with Product with Serializable

  15. class Z3Pattern extends AnyRef

    Attributes
    sealed

  16. class Z3SearchFailure extends AnyRef

    Attributes
    sealed abstract

  17. class Z3Sort extends AnyRef

    Attributes
    sealed

  18. case class Z3StringSymbol (value: String) extends Z3SymbolKind[String] with Product with Serializable

  19. class Z3Symbol extends AnyRef

    Attributes
    sealed

  20. class Z3SymbolKind [T] extends AnyRef

    Attributes
    sealed abstract

  21. class Z3Theory extends AnyRef

    This class is inherited to create user defined theories.

Value Members

  1. object DefaultBoolean extends Default[Boolean]

    Attributes
    implicit

  2. object DefaultInt extends Default[Int]

    Attributes
    implicit

  3. object Z3Canceled extends Z3SearchFailure with Product with Serializable

  4. object Z3Context extends AnyRef

  5. object Z3DeclKind extends Enumeration

  6. object Z3IncompleteTheory extends Z3SearchFailure with Product with Serializable

  7. object Z3MemoutWatermark extends Z3SearchFailure with Product with Serializable

  8. object Z3Model extends AnyRef

  9. object Z3NoFailure extends Z3SearchFailure with Product with Serializable

  10. object Z3NumConflicts extends Z3SearchFailure with Product with Serializable

  11. object Z3QuantifierAST extends Z3ASTKind with Product with Serializable

  12. object Z3Quantifiers extends Z3SearchFailure with Product with Serializable

  13. object Z3Timeout extends Z3SearchFailure with Product with Serializable

  14. object Z3Unknown extends Z3SearchFailure with Product with Serializable

  15. object Z3UnknownAST extends Z3ASTKind with Product with Serializable

  16. object Z3VarAST extends Z3ASTKind with Product with Serializable

  17. package dsl

  18. def error (any: Any): Nothing

    Definition Classes
    package

  19. implicit def liftDefaultToFun [A, B] (implicit arg0: Default[B]): Default[(A) ⇒ B]

    Attributes
    implicit
    Definition Classes
    package

  20. implicit def liftDefaultToSet [A] (implicit arg0: Default[A]): Default[Set[A]]

    Attributes
    implicit
    Definition Classes
    package

  21. def resetMemory : Unit

    Definition Classes
    package

  22. def toPtrArray (ptrs: Iterable[AnyRef { def ptr: Long }]): Array[Long]

    Attributes
    protected[z3]
    Definition Classes
    package

  23. def toggleWarningMessages (enabled: Boolean): Unit

    Definition Classes
    package

  24. lazy val version : String

    A string representation of the version numbers for Z3, and the API (including bindings)

    A string representation of the version numbers for Z3, and the API (including bindings)

    Definition Classes
    package