package dsl
- Alphabetic
- By Inheritance
- dsl
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Type Members
- case class Add[+A >: BottomSort <: IntSort](args: Tree[A]*) extends Tree[IntSort] with Product with Serializable
- case class And[+A >: BottomSort <: BoolSort](args: Tree[A]*) extends NAryPred[A] with Product with Serializable
- sealed trait ArraySort extends TopSort
- case class BVAdd[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVAddNoOverflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A], isSigned: Boolean) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVAddNoUnderflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVAnd[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVAshr[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVLshr[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVMul[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVMulNoOverflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A], isSigned: Boolean) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVMulNoUnderflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVNand[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVNeg[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
- case class BVNegNoOverflow[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
- case class BVNor[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVNot[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
- case class BVOr[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVRedAnd[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
- case class BVRedOr[+A >: BottomSort <: BVSort](tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
- case class BVSDivNoOverflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVSdiv[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVSge[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
- case class BVSgt[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
- case class BVShl[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVSle[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
- case class BVSlt[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
- case class BVSmod[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- sealed trait BVSort extends TopSort
- case class BVSrem[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVSub[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVSubNoOverflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVSubNoUnderflow[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A], isSigned: Boolean) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVUdiv[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVUge[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
- case class BVUgt[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
- case class BVUle[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
- case class BVUlt[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BVSort] with Product with Serializable
- case class BVUrem[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVXnor[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class BVXor[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- sealed trait BinaryOp[+A >: BottomSort <: TopSort, B >: BottomSort <: TopSort] extends Tree[B]
- sealed trait BinaryPred[+A >: BottomSort <: TopSort] extends BinaryOp[A, BoolSort]
- case class BoolConstant(value: Boolean) extends Tree[BoolSort] with Product with Serializable
- sealed trait BoolSort extends TopSort
- case class BoolVar() extends Tree[BoolSort] with Product with Serializable
- sealed trait BottomSort extends BoolSort with IntSort with RealSort with BVSort with SetSort with ArraySort
- case class CharConstant(value: Char) extends Tree[BVSort] with Product with Serializable
- case class CharVar() extends Tree[BVSort] with Product with Serializable
- case class Concat[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class Distinct[+A >: BottomSort <: TopSort](args: Tree[A]*) extends NAryPred[A] with Product with Serializable
- case class Div[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable
- case class EmptyIntSet() extends Tree[SetSort] with Product with Serializable
- case class Eq[+A >: BottomSort <: TopSort](left: Tree[A], right: Tree[A]) extends BinaryPred[A] with Product with Serializable
- case class ExtRotateLeft[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class ExtRotateRight[+A >: BottomSort <: BVSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, BVSort] with Product with Serializable
- case class Extract[+A >: BottomSort <: BVSort](high: Int, low: Int, tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
- case class GE[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable
- case class GT[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable
- case class Iff[+A >: BottomSort <: BoolSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BoolSort] with Product with Serializable
- case class Implies[+A >: BottomSort <: BoolSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BoolSort] with Product with Serializable
- case class IntConstant(value: Int) extends Tree[IntSort] with Product with Serializable
- case class IntSetVar() extends Tree[SetSort] with Product with Serializable
- sealed trait IntSort extends TopSort
- case class IntVar() extends Tree[IntSort] with Product with Serializable
- case class LE[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable
- case class LT[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryPred[IntSort] with Product with Serializable
- case class MapSelect(map: Tree[_ >: BottomSort <: TopSort], index: Tree[_ >: BottomSort <: TopSort]) extends Tree[BottomSort] with Product with Serializable
- case class Mod[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable
- case class Mul[+A >: BottomSort <: IntSort](args: Tree[A]*) extends Tree[IntSort] with Product with Serializable
- sealed trait NAryPred[+A >: BottomSort <: TopSort] extends Tree[BoolSort]
- case class Not[+A >: BottomSort <: BoolSort](tree: Tree[A]) extends Tree[BoolSort] with Product with Serializable
- case class Or[+A >: BottomSort <: BoolSort](args: Tree[A]*) extends NAryPred[A] with Product with Serializable
-
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.
- sealed trait RealSort extends TopSort
- case class Rem[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable
- case class Repeat[+A >: BottomSort <: BVSort](count: Int, tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
- case class SetAdd[+A >: BottomSort <: TopSort](set: Tree[SetSort], elem: Tree[A]) extends Tree[SetSort] with Product with Serializable
- case class SetDifference[+A >: BottomSort <: SetSort](left: Tree[A], right: Tree[A]) extends Tree[SetSort] with Product with Serializable
- case class SetIntersect[+A >: BottomSort <: SetSort](args: Tree[A]*) extends Tree[SetSort] with Product with Serializable
- sealed trait SetSort extends TopSort
- case class SetSubset[+A >: BottomSort <: SetSort](left: Tree[A], right: Tree[A]) extends BinaryPred[SetSort] with Product with Serializable
- case class SetUnion[+A >: BottomSort <: SetSort](args: Tree[A]*) extends Tree[SetSort] with Product with Serializable
- case class SignExt[+A >: BottomSort <: BVSort](extraSize: Int, tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
- class SortMismatchException extends Exception
- case class Sub[+A >: BottomSort <: IntSort](left: Tree[A], right: Tree[A]) extends BinaryOp[A, IntSort] with Product with Serializable
- sealed trait TopSort extends AnyRef
- sealed trait Tree[+T >: BottomSort <: TopSort] extends AnyRef
- class UnsatisfiableConstraintException extends Exception
-
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.
-
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( ... )
- abstract class ValTree[S >: BottomSort <: TopSort] extends Tree[S]
- case class Xor[+A >: BottomSort <: BoolSort](left: Tree[A], right: Tree[A]) extends BinaryPred[BoolSort] with Product with Serializable
-
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.
- case class ZeroExt[+A >: BottomSort <: BVSort](extraSize: Int, tree: Tree[A]) extends Tree[BVSort] with Product with Serializable
Value Members
- implicit def astvectorToSeq(v: Z3ASTVector): Seq[Z3AST]
- implicit def boolOperandToBoolTree(operand: BoolOperand): Tree[BoolSort]
- implicit def boolTreeToBoolOperand[T >: BottomSort <: BoolSort](tree: Tree[T]): BoolOperand
- implicit def booleanValToBoolOperand(value: Val[Boolean]): BoolOperand
- implicit def booleanValToBoolTree(value: Val[Boolean]): Tree[BoolSort]
- implicit def booleanValueToBoolOperand(value: Boolean): BoolOperand
- implicit def booleanValueToBoolTree(value: Boolean): Tree[BoolSort]
- implicit def bvOperandToBVTree(operand: BitVectorOperand): Tree[BVSort]
- implicit def bvTreeToBVOperand[T >: BottomSort <: BVSort](tree: Tree[T]): BitVectorOperand
- implicit def charValToBVOperand(value: Val[Char]): BitVectorOperand
- implicit def charValToCharTree(value: Val[Char]): Tree[BVSort]
- implicit def charValueToBVOperand(value: Char): BitVectorOperand
- implicit def charValueToBVTree(value: Char): Tree[BVSort]
- 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)
- def choose[T1, T2](predicate: (Val[T1], Val[T2]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2]): (T1, T2)
- def choose[T](predicate: (Val[T]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T]): T
- 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)]
- def find[T1, T2](predicate: (Val[T1], Val[T2]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2]): Option[(T1, T2)]
- def find[T](predicate: (Val[T]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T]): Option[T]
- 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)]
- def findAll[T1, T2](predicate: (Val[T1], Val[T2]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T1], arg1: ValHandler[T2]): Iterator[(T1, T2)]
- def findAll[T](predicate: (Val[T]) ⇒ Tree[BoolSort])(implicit arg0: ValHandler[T]): Iterator[T]
- implicit def intOperandToIntTree(operand: IntOperand): Tree[IntSort]
- implicit def intSetValueToSetOperand(value: Set[Int]): SetOperand
- implicit def intSetValueToSetTree(value: Set[Int]): Tree[SetSort]
- implicit def intTreeToIntOperand[T >: BottomSort <: IntSort](tree: Tree[T]): IntOperand
- implicit def intValToIntOperand(value: Val[Int]): IntOperand
- implicit def intValToIntTree(value: Val[Int]): Tree[IntSort]
- implicit def intValueToIntOperand(value: Int): IntOperand
- implicit def intValueToIntTree(value: Int): Tree[IntSort]
- implicit def liftDefaultToFun[A, B](implicit arg0: Default[B]): Default[(A) ⇒ B]
- implicit def liftDefaultToSet[A](implicit arg0: Default[A]): Default[Set[A]]
- implicit def liftToFuncHandler[A, B](implicit arg0: Default[A], arg1: ValHandler[A], arg2: Default[B], arg3: ValHandler[B]): ValHandler[(A) ⇒ B]
- implicit def setOperandToSetTree(operand: SetOperand): Tree[SetSort]
- implicit def setTreeToSetOperand[T >: BottomSort <: SetSort](tree: Tree[T]): SetOperand
- implicit def z3ASTToBoolOperand(ast: Z3AST): BoolOperand
- implicit def z3ASTToIntOperand(ast: Z3AST): IntOperand
- implicit def z3ASTToSetOperand(ast: Z3AST): SetOperand
- implicit object BooleanValHandler extends ValHandler[Boolean]
- implicit object CharValHandler extends ValHandler[Char]
- implicit object DefaultBoolean extends Default[Boolean]
- implicit object DefaultChar extends Default[Char]
- implicit object DefaultInt extends Default[Int]
- implicit object IntValHandler extends ValHandler[Int]
-
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.