p

z3.scala

dsl

package dsl

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. dsl
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
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. sealed trait ArraySort extends TopSort
  4. case class BVAdd[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  5. case class BVAddNoOverflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A], isSigned: Boolean) extends BinaryOp[A, BVSort] with Product with Serializable
  6. case class BVAddNoUnderflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  7. case class BVAnd[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  8. case class BVAshr[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  9. case class BVLshr[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  10. case class BVMul[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  11. case class BVMulNoOverflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A], isSigned: Boolean) extends BinaryOp[A, BVSort] with Product with Serializable
  12. case class BVMulNoUnderflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  13. case class BVNand[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  14. case class BVNeg[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
  15. case class BVNegNoOverflow[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
  16. case class BVNor[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  17. case class BVNot[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
  18. case class BVOr[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  19. case class BVRedAnd[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
  20. case class BVRedOr[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
  21. case class BVSDivNoOverflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  22. case class BVSdiv[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  23. case class BVSge[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
  24. case class BVSgt[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
  25. case class BVShl[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  26. case class BVSle[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
  27. case class BVSlt[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
  28. case class BVSmod[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  29. sealed trait BVSort extends TopSort
  30. case class BVSrem[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  31. case class BVSub[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  32. case class BVSubNoOverflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  33. case class BVSubNoUnderflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A], isSigned: Boolean) extends BinaryOp[A, BVSort] with Product with Serializable
  34. case class BVUdiv[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  35. case class BVUge[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
  36. case class BVUgt[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
  37. case class BVUle[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
  38. case class BVUlt[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
  39. case class BVUrem[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  40. case class BVXnor[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  41. case class BVXor[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  42. sealed trait BinaryOp[+A >: BottomSort <: TopSort, B >: BottomSort <: TopSort] extends Tree[B]
  43. sealed trait BinaryPred[+A >: BottomSort <: TopSort] extends BinaryOp[A, BoolSort]
  44. case class BoolConstant(value: Boolean) extends Tree[BoolSort] with Product with Serializable
  45. sealed trait BoolSort extends TopSort
  46. case class BoolVar() extends Tree[BoolSort] with Product with Serializable
  47. sealed trait BottomSort extends BoolSort with IntSort with RealSort with BVSort with SetSort with ArraySort
  48. case class CharConstant(value: Char) extends Tree[BVSort] with Product with Serializable
  49. case class CharVar() extends Tree[BVSort] with Product with Serializable
  50. case class Concat[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  51. case class Distinct[+A >: BottomSort <: TopSort](args: Tree[A]*) extends NAryPred[A] with Product with Serializable
  52. case class Div[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable
  53. case class EmptyIntSet() extends Tree[SetSort] with Product with Serializable
  54. case class Eq[+A >: BottomSort <: TopSort](left: Tree[A], right: Tree[A]) extends BinaryPred[A] with Product with Serializable
  55. case class ExtRotateLeft[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  56. case class ExtRotateRight[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
  57. case class Extract[+A >: BottomSort <: BVSort](high: Int, low: Int, tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
  58. case class GE[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable
  59. case class GT[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable
  60. case class Iff[+A >: BottomSort <: BoolSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BoolSort] with Product with Serializable
  61. case class Implies[+A >: BottomSort <: BoolSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BoolSort] with Product with Serializable
  62. case class IntConstant(value: Int) extends Tree[IntSort] with Product with Serializable
  63. case class IntSetVar() extends Tree[SetSort] with Product with Serializable
  64. sealed trait IntSort extends TopSort
  65. case class IntVar() extends Tree[IntSort] with Product with Serializable
  66. case class LE[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable
  67. case class LT[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable
  68. case class MapSelect(map: Tree[_ >: BottomSort <: TopSort], index: Tree[_ >: BottomSort <: TopSort]) extends Tree[BottomSort] with Product with Serializable
  69. case class Mod[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable
  70. case class Mul[+A >: BottomSort <: IntSort](args: Tree[A]*) extends Tree[IntSort] with Product with Serializable
  71. sealed trait NAryPred[+A >: BottomSort <: TopSort] extends Tree[BoolSort]
  72. case class Not[+A >: BottomSort <: BoolSort](tree: Tree[A]) extends Tree[BoolSort] with Product with Serializable
  73. case class Or[+A >: BottomSort <: BoolSort](args: Tree[A]*) extends NAryPred[A] with Product with Serializable
  74. 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.

    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. More sophisticated representations à la functional programs that can sometimes be obtained from quantified formulas are not yet supported. PS.

  75. sealed trait RealSort extends TopSort
  76. case class Rem[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable
  77. case class Repeat[+A >: BottomSort <: BVSort](count: Int, tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
  78. case class SetAdd[+A >: BottomSort <: TopSort](set: Tree[SetSort], elem: Tree[A]) extends Tree[SetSort] with Product with Serializable
  79. case class SetDifference[+A >: BottomSort <: SetSort](left: Tree[A], right: Tree[A]) extends Tree[SetSort] with Product with Serializable
  80. case class SetIntersect[+A >: BottomSort <: SetSort](args: Tree[A]*) extends Tree[SetSort] with Product with Serializable
  81. sealed trait SetSort extends TopSort
  82. case class SetSubset[+A >: BottomSort <: SetSort](left: Tree[A], right: Tree[A]) extends BinaryPred[SetSort] with Product with Serializable
  83. case class SetUnion[+A >: BottomSort <: SetSort](args: Tree[A]*) extends Tree[SetSort] with Product with Serializable
  84. case class SignExt[+A >: BottomSort <: BVSort](extraSize: Int, tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
  85. class SortMismatchException extends Exception
  86. case class Sub[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable
  87. sealed trait TopSort extends AnyRef
  88. sealed trait Tree[+T >: BottomSort <: TopSort] extends AnyRef
  89. class UnsatisfiableConstraintException extends Exception
  90. class Val[A] extends AnyRef

    The type parameter refers to a Scala type for a value that the user wishes to obtain through a call to choose, find or findAll.

  91. abstract 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.

    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.

    Annotations
    @implicitNotFound( ... )
  92. abstract class ValTree[S >: BottomSort <: TopSort] extends Tree[S]
  93. case class Xor[+A >: BottomSort <: BoolSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BoolSort] with Product with Serializable
  94. case class Z3ASTWrapper[+A >: BottomSort <: TopSort] extends Tree[A] with Product with Serializable

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

    This class is used to bridge the gap between non-DSL Z3ASTs and DSL ASTs. There are two important things to check: that the Z3Context is the correct one (when the DSL tree actually gets converted), and that the sort is the advertised one. This second check is currently not performed. It will need to be a runtime check that can happen through an implicit "checker" parameter.

  95. case class ZeroExt[+A >: BottomSort <: BVSort](extraSize: Int, tree: Tree[A]) extends Tree[BVSort] with Product with Serializable

Value Members

  1. implicit def astvectorToSeq(v: Z3ASTVector): Seq[Z3AST]
  2. implicit def boolOperandToBoolTree(operand: BoolOperand): Tree[BoolSort]
  3. implicit def boolTreeToBoolOperand[T >: BottomSort <: BoolSort](tree: Tree[T]): BoolOperand
  4. implicit def booleanValToBoolOperand(value: Val[Boolean]): BoolOperand
  5. implicit def booleanValToBoolTree(value: Val[Boolean]): Tree[BoolSort]
  6. implicit def booleanValueToBoolOperand(value: Boolean): BoolOperand
  7. implicit def booleanValueToBoolTree(value: Boolean): Tree[BoolSort]
  8. implicit def bvOperandToBVTree(operand: BitVectorOperand): Tree[BVSort]
  9. implicit def bvTreeToBVOperand[T >: BottomSort <: BVSort](tree: Tree[T]): BitVectorOperand
  10. implicit def charValToBVOperand(value: Val[Char]): BitVectorOperand
  11. implicit def charValToCharTree(value: Val[Char]): Tree[BVSort]
  12. implicit def charValueToBVOperand(value: Char): BitVectorOperand
  13. implicit def charValueToBVTree(value: Char): Tree[BVSort]
  14. 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)
  15. def choose[T1, T2](predicate: (Val[T1], Val[T2]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2]): (T1, T2)
  16. def choose[T](predicate: (Val[T]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T]): T
  17. 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)]
  18. def find[T1, T2](predicate: (Val[T1], Val[T2]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2]): Option[(T1, T2)]
  19. def find[T](predicate: (Val[T]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T]): Option[T]
  20. 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)]
  21. def findAll[T1, T2](predicate: (Val[T1], Val[T2]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2]): Iterator[(T1, T2)]
  22. def findAll[T](predicate: (Val[T]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T]): Iterator[T]
  23. implicit def intOperandToIntTree(operand: IntOperand): Tree[IntSort]
  24. implicit def intSetValueToSetOperand(value: Set[Int]): SetOperand
  25. implicit def intSetValueToSetTree(value: Set[Int]): Tree[SetSort]
  26. implicit def intTreeToIntOperand[T >: BottomSort <: IntSort](tree: Tree[T]): IntOperand
  27. implicit def intValToIntOperand(value: Val[Int]): IntOperand
  28. implicit def intValToIntTree(value: Val[Int]): Tree[IntSort]
  29. implicit def intValueToIntOperand(value: Int): IntOperand
  30. implicit def intValueToIntTree(value: Int): Tree[IntSort]
  31. implicit def liftDefaultToFun[A, B](implicit arg0: Default[B]): Default[(A) ⇒ B]
  32. implicit def liftDefaultToSet[A](implicit arg0: Default[A]): Default[Set[A]]
  33. implicit def liftToFuncHandler[A, B](implicit arg0: Default[A], arg1: ValHandler[A], arg2: Default[B], arg3: ValHandler[B]): ValHandler[(A) ⇒ B]
  34. implicit def setOperandToSetTree(operand: SetOperand): Tree[SetSort]
  35. implicit def setTreeToSetOperand[T >: BottomSort <: SetSort](tree: Tree[T]): SetOperand
  36. implicit def z3ASTToBoolOperand(ast: Z3AST): BoolOperand
  37. implicit def z3ASTToIntOperand(ast: Z3AST): IntOperand
  38. implicit def z3ASTToSetOperand(ast: Z3AST): SetOperand
  39. implicit object BooleanValHandler extends ValHandler[Boolean]
  40. implicit object CharValHandler extends ValHandler[Char]
  41. implicit object DefaultBoolean extends Default[Boolean]
  42. implicit object DefaultChar extends Default[Char]
  43. implicit object DefaultInt extends Default[Int]
  44. implicit object IntValHandler extends ValHandler[Int]
  45. object Operands

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

    We call Operands what is otherwise known as "Rich" classes (from the "Pimp My Library" paradigm). For simplicity and to avoid ambiguous resolutions, operations on operands always return operands, never trees. Conversion from and to trees are done by implicit functions in the dsl package object.

Inherited from AnyRef

Inherited from Any

Ungrouped