z3.scala

dsl

package dsl

Visibility
  1. Public
  2. All

Type Members

  1. case class Add [+A >: BottomSort <: IntSort] (args: Tree[A]*) extends Tree[IntSort] with Product with Serializable

  2. case class And [+A >: BottomSort <: BoolSort] (args: Tree[A]*) extends NAryPred[A] with Product with Serializable

  3. trait ArraySort extends TopSort

    Attributes
    sealed

  4. trait BVSort extends TopSort

    Attributes
    sealed

  5. trait BinaryOp [+A >: BottomSort <: TopSort, B >: BottomSort <: TopSort] extends Tree[B]

    Attributes
    sealed

  6. trait BinaryPred [+A >: BottomSort <: TopSort] extends BinaryOp[A, BoolSort]

    Attributes
    sealed

  7. case class BoolConstant (value: Boolean) extends Tree[BoolSort] with Product with Serializable

  8. trait BoolSort extends TopSort

    Attributes
    sealed

  9. case class BoolVar () extends Tree[BoolSort] with Product with Serializable

  10. trait BottomSort extends BoolSort with IntSort with RealSort with BVSort with SetSort with ArraySort

    Attributes
    sealed

  11. case class Distinct [+A >: BottomSort <: TopSort] (args: Tree[A]*) extends NAryPred[A] with Product with Serializable

  12. case class Div [+A >: BottomSort <: IntSort] (left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable

  13. case class EmptyIntSet () extends Tree[SetSort] with Product with Serializable

  14. case class Eq [+A >: BottomSort <: TopSort] (left: Tree[A], right: Tree[A]) extends BinaryPred[A] with Product with Serializable

  15. case class GE [+A >: BottomSort <: IntSort] (left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable

  16. case class GT [+A >: BottomSort <: IntSort] (left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable

  17. case class Iff [+A >: BottomSort <: BoolSort] (left: Tree[A], right: Tree[A]) extends BinaryPred[BoolSort] with Product with Serializable

  18. case class Implies [+A >: BottomSort <: BoolSort] (left: Tree[A], right: Tree[A]) extends BinaryPred[BoolSort] with Product with Serializable

  19. case class IntConstant (value: Int) extends Tree[IntSort] with Product with Serializable

  20. case class IntSetVar () extends Tree[SetSort] with Product with Serializable

  21. trait IntSort extends TopSort

    Attributes
    sealed

  22. case class IntVar () extends Tree[IntSort] with Product with Serializable

  23. case class LE [+A >: BottomSort <: IntSort] (left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable

  24. case class LT [+A >: BottomSort <: IntSort] (left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable

  25. case class MapSelect (map: z3.scala.dsl.Tree[_ >: z3.scala.dsl.BottomSort <: z3.scala.dsl.TopSort], index: z3.scala.dsl.Tree[_ >: z3.scala.dsl.BottomSort <: z3.scala.dsl.TopSort]) extends Tree[BottomSort] with Product with Serializable

  26. case class Mod [+A >: BottomSort <: IntSort] (left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable

  27. case class Mul [+A >: BottomSort <: IntSort] (args: Tree[A]*) extends Tree[IntSort] with Product with Serializable

  28. trait NAryPred [+A >: BottomSort <: TopSort] extends Tree[BoolSort]

    Attributes
    sealed

  29. case class Not [+A >: BottomSort <: BoolSort] (tree: Tree[A]) extends Tree[BoolSort] with Product with Serializable

  30. case class Or [+A >: BottomSort <: BoolSort] (args: Tree[A]*) extends NAryPred[A] with Product with Serializable

  31. class PointWiseFunction [-A, +B] extends (A) ⇒ B

    Instances of this class are used to represent models of Z3 maps, which are typically defined by a finite collection of pairs and a default value.

  32. trait RealSort extends TopSort

    Attributes
    sealed

  33. case class Rem [+A >: BottomSort <: IntSort] (left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable

  34. case class SetAdd [+A >: BottomSort <: TopSort] (set: Tree[SetSort], elem: Tree[A]) extends Tree[SetSort] with Product with Serializable

  35. case class SetDifference [+A >: BottomSort <: SetSort] (left: Tree[A], right: Tree[A]) extends Tree[SetSort] with Product with Serializable

  36. case class SetIntersect [+A >: BottomSort <: SetSort] (args: Tree[A]*) extends Tree[SetSort] with Product with Serializable

  37. trait SetSort extends TopSort

    Attributes
    sealed

  38. case class SetSubset [+A >: BottomSort <: SetSort] (left: Tree[A], right: Tree[A]) extends BinaryPred[SetSort] with Product with Serializable

  39. case class SetUnion [+A >: BottomSort <: SetSort] (args: Tree[A]*) extends Tree[SetSort] with Product with Serializable

  40. class SortMismatchException extends Exception

  41. case class Sub [+A >: BottomSort <: IntSort] (left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable

  42. trait TopSort extends AnyRef

    Attributes
    sealed

  43. trait Tree [+T >: BottomSort <: TopSort] extends AnyRef

    Attributes
    sealed

  44. class UnsatisfiableConstraintException extends Exception

  45. class Val [A] extends Tree[BottomSort]

    Instances of Val should never be created manually, but rather always through a ValHandler.

  46. class ValHandler [A] extends AnyRef

    A ValHandler encapsulates everything that is needed to build a Z3Sort representing A, a fresh identifier of that sort and to reconstruct a Scala value from a model.

  47. case class Xor [+A >: BottomSort <: BoolSort] (left: Tree[A], right: Tree[A]) extends BinaryPred[BoolSort] with Product with Serializable

  48. case class Z3ASTWrapper [+A >: BottomSort <: TopSort] (ast: Z3AST) extends Tree[A] with Product with Serializable

    This class is used to bridge the gap between non-DSL Z3ASTs and DSL ASTs.

Value Members

  1. object BooleanValHandler extends ValHandler[Boolean]

    Attributes
    implicit

  2. object IntValHandler extends ValHandler[Int]

    Attributes
    implicit

  3. object Operands extends AnyRef

    We call Operands what is otherwise known as "Rich" classes (from the "Pimp My Library" paradigm).

  4. implicit def boolOperandToBoolTree (operand: BoolOperand): Tree[BoolSort]

    Attributes
    implicit
    Definition Classes
    package

  5. implicit def boolTreeToBoolOperand [T >: BottomSort <: BoolSort] (tree: Tree[T]): BoolOperand

    Attributes
    implicit
    Definition Classes
    package

  6. implicit def booleanValueToBoolOperand (value: Boolean): BoolOperand

    Attributes
    implicit
    Definition Classes
    package

  7. implicit def booleanValueToBoolTree (value: Boolean): Tree[BoolSort]

    Attributes
    implicit
    Definition Classes
    package

  8. def choose [T1, T2, T3] (predicate: (Val[T1], Val[T2], Val[T3]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2], arg2: ValHandler[T3]): (T1, T2, T3)

    Definition Classes
    package

  9. def choose [T1, T2] (predicate: (Val[T1], Val[T2]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2]): (T1, T2)

    Definition Classes
    package

  10. def choose [T] (predicate: (Val[T]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T]): T

    Definition Classes
    package

  11. def find [T1, T2, T3] (predicate: (Val[T1], Val[T2], Val[T3]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2], arg2: ValHandler[T3]): Option[(T1, T2, T3)]

    Definition Classes
    package

  12. def find [T1, T2] (predicate: (Val[T1], Val[T2]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2]): Option[(T1, T2)]

    Definition Classes
    package

  13. def find [T] (predicate: (Val[T]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T]): Option[T]

    Definition Classes
    package

  14. def findAll [T1, T2, T3] (predicate: (Val[T1], Val[T2], Val[T3]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2], arg2: ValHandler[T3]): Iterator[(T1, T2, T3)]

    Definition Classes
    package

  15. def findAll [T1, T2] (predicate: (Val[T1], Val[T2]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2]): Iterator[(T1, T2)]

    Definition Classes
    package

  16. def findAll [T] (predicate: (Val[T]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T]): Iterator[T]

    Definition Classes
    package

  17. implicit def intOperandToIntTree (operand: IntOperand): Tree[IntSort]

    Attributes
    implicit
    Definition Classes
    package

  18. implicit def intSetValueToSetOperand (value: Set[Int]): SetOperand

    Attributes
    implicit
    Definition Classes
    package

  19. implicit def intSetValueToSetTree (value: Set[Int]): Tree[SetSort]

    Attributes
    implicit
    Definition Classes
    package

  20. implicit def intTreeToIntOperand [T >: BottomSort <: IntSort] (tree: Tree[T]): IntOperand

    Attributes
    implicit
    Definition Classes
    package

  21. implicit def intValueToIntOperand (value: Int): IntOperand

    Attributes
    implicit
    Definition Classes
    package

  22. implicit def intValueToIntTree (value: Int): Tree[IntSort]

    Attributes
    implicit
    Definition Classes
    package

  23. implicit def liftToFuncHandler [A, B] (implicit arg0: Default[A], arg1: ValHandler[A], arg2: Default[B], arg3: ValHandler[B]): ValHandler[(A) ⇒ B]

    Attributes
    implicit
    Definition Classes
    package

  24. implicit def liftToSetValHander [A] (implicit arg0: Default[A], arg1: ValHandler[A]): ValHandler[Set[A]]

    Attributes
    implicit
    Definition Classes
    package

  25. implicit def setOperandToSetTree (operand: SetOperand): Tree[SetSort]

    Attributes
    implicit
    Definition Classes
    package

  26. implicit def setTreeToSetOperand [T >: BottomSort <: SetSort] (tree: Tree[T]): SetOperand

    Attributes
    implicit
    Definition Classes
    package

  27. implicit def z3ASTToBoolOperand (ast: Z3AST): BoolOperand

    Attributes
    implicit
    Definition Classes
    package

  28. implicit def z3ASTToIntOperand (ast: Z3AST): IntOperand

    Attributes
    implicit
    Definition Classes
    package

  29. implicit def z3ASTToSetOperand (ast: Z3AST): SetOperand

    Attributes
    implicit
    Definition Classes
    package