Trait/Object

util.translators

SMTContext

Related Docs: object SMTContext | package translators

Permalink

trait SMTContext extends Context

Trait for utility operations on Z3 SMT terms

Linear Supertypes
Context, IDisposable, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SMTContext
  2. Context
  3. IDisposable
  4. AnyRef
  5. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. def MOption(arg0: ReExpr): ReExpr

    Permalink
    Definition Classes
    Context
  5. def MPlus(arg0: ReExpr): ReExpr

    Permalink
    Definition Classes
    Context
  6. def MkAt(arg0: SeqExpr, arg1: IntExpr): SeqExpr

    Permalink
    Definition Classes
    Context
  7. def MkConcat(arg0: <repeated...>[ReExpr]): ReExpr

    Permalink
    Definition Classes
    Context
  8. def MkConcat(arg0: <repeated...>[SeqExpr]): SeqExpr

    Permalink
    Definition Classes
    Context
  9. def MkContains(arg0: SeqExpr, arg1: SeqExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  10. def MkEmptySeq(arg0: Sort): SeqExpr

    Permalink
    Definition Classes
    Context
  11. def MkExtract(arg0: SeqExpr, arg1: IntExpr, arg2: IntExpr): SeqExpr

    Permalink
    Definition Classes
    Context
  12. def MkInRe(arg0: SeqExpr, arg1: ReExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  13. def MkIndexOf(arg0: SeqExpr, arg1: SeqExpr, arg2: ArithExpr): IntExpr

    Permalink
    Definition Classes
    Context
  14. def MkLength(arg0: SeqExpr): IntExpr

    Permalink
    Definition Classes
    Context
  15. def MkPrefixOf(arg0: SeqExpr, arg1: SeqExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  16. def MkReplace(arg0: SeqExpr, arg1: SeqExpr, arg2: SeqExpr): SeqExpr

    Permalink
    Definition Classes
    Context
  17. def MkStar(arg0: ReExpr): ReExpr

    Permalink
    Definition Classes
    Context
  18. def MkString(arg0: String): SeqExpr

    Permalink
    Definition Classes
    Context
  19. def MkSuffixOf(arg0: SeqExpr, arg1: SeqExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  20. def MkToRe(arg0: SeqExpr): ReExpr

    Permalink
    Definition Classes
    Context
  21. def MkUnion(arg0: <repeated...>[ReExpr]): ReExpr

    Permalink
    Definition Classes
    Context
  22. def MkUnit(arg0: Expr): SeqExpr

    Permalink
    Definition Classes
    Context
  23. def MkUpdateField(arg0: FuncDecl, arg1: Expr, arg2: Expr): Expr

    Permalink
    Definition Classes
    Context
    Annotations
    @throws( ... )
  24. def SimplifyHelp(): String

    Permalink
    Definition Classes
    Context
  25. def and(arg0: Probe, arg1: Probe): Probe

    Permalink
    Definition Classes
    Context
  26. def andThen(arg0: Tactic, arg1: Tactic, arg2: <repeated...>[Tactic]): Tactic

    Permalink
    Definition Classes
    Context
  27. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  28. def atLeastNBDD(kids: List[BoolExpr], k: Int): BoolExpr

    Permalink

    BDD encoding of the at least n

    BDD encoding of the at least n

    kids

    the Boolean expression addressed by the at least

    k

    the bound

    returns

    the equivalent BDD expression expressed as if-then-else

  29. def atMostN(kids: List[BoolExpr], n: Int): BoolExpr

    Permalink

    Express at most n with Sequential encoding

    Express at most n with Sequential encoding

    kids

    the Boolean expression addressed by the at most

    n

    the bound

    returns

    the equivalent Boolean expression

  30. def benchmarkToSMTString(arg0: String, arg1: String, arg2: String, arg3: String, arg4: Array[BoolExpr], arg5: BoolExpr): String

    Permalink
    Definition Classes
    Context
  31. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  32. def cond(arg0: Probe, arg1: Tactic, arg2: Tactic): Tactic

    Permalink
    Definition Classes
    Context
  33. def constProbe(arg0: Double): Probe

    Permalink
    Definition Classes
    Context
  34. def dispose(): Unit

    Permalink
    Definition Classes
    Context → IDisposable
  35. def eq(arg0: Probe, arg1: Probe): Probe

    Permalink
    Definition Classes
    Context
  36. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  37. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  38. def fail(): Tactic

    Permalink
    Definition Classes
    Context
  39. def failIf(arg0: Probe): Tactic

    Permalink
    Definition Classes
    Context
  40. def failIfNotDecided(): Tactic

    Permalink
    Definition Classes
    Context
  41. def finalize(): Unit

    Permalink
    Attributes
    protected[com.microsoft.z3]
    Definition Classes
    Context → AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  42. def ge(arg0: Probe, arg1: Probe): Probe

    Permalink
    Definition Classes
    Context
  43. def getASTDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  44. def getASTMapDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  45. def getASTVectorDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  46. def getApplyResultDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  47. def getBoolSort(): BoolSort

    Permalink
    Definition Classes
    Context
  48. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  49. def getFixedpointDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  50. def getFuncEntryDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  51. def getFuncInterpDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  52. def getGoalDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  53. def getIntSort(): IntSort

    Permalink
    Definition Classes
    Context
  54. def getModelDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  55. def getNumProbes(): Int

    Permalink
    Definition Classes
    Context
  56. def getNumSMTLIBAssumptions(): Int

    Permalink
    Definition Classes
    Context
  57. def getNumSMTLIBDecls(): Int

    Permalink
    Definition Classes
    Context
  58. def getNumSMTLIBFormulas(): Int

    Permalink
    Definition Classes
    Context
  59. def getNumSMTLIBSorts(): Int

    Permalink
    Definition Classes
    Context
  60. def getNumTactics(): Int

    Permalink
    Definition Classes
    Context
  61. def getOptimizeDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  62. def getParamDescrsDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  63. def getParamsDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  64. def getProbeDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  65. def getProbeDescription(arg0: String): String

    Permalink
    Definition Classes
    Context
  66. def getProbeNames(): Array[String]

    Permalink
    Definition Classes
    Context
  67. def getRealSort(): RealSort

    Permalink
    Definition Classes
    Context
  68. def getSMTLIBAssumptions(): Array[BoolExpr]

    Permalink
    Definition Classes
    Context
  69. def getSMTLIBDecls(): Array[FuncDecl]

    Permalink
    Definition Classes
    Context
  70. def getSMTLIBFormulas(): Array[BoolExpr]

    Permalink
    Definition Classes
    Context
  71. def getSMTLIBSorts(): Array[Sort]

    Permalink
    Definition Classes
    Context
  72. def getSimplifyParameterDescriptions(): ParamDescrs

    Permalink
    Definition Classes
    Context
  73. def getSolverDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  74. def getStatisticsDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  75. def getStringSort(): SeqSort

    Permalink
    Definition Classes
    Context
  76. def getTacticDRQ(): IDecRefQueue

    Permalink
    Definition Classes
    Context
  77. def getTacticDescription(arg0: String): String

    Permalink
    Definition Classes
    Context
  78. def getTacticNames(): Array[String]

    Permalink
    Definition Classes
    Context
  79. def getValueAtPos(const: SubstitutionVar, index: Int): Option[Expr]

    Permalink

    Find the ith element of the enumeration sort of Z3 contained in a substitution variable

    Find the ith element of the enumeration sort of Z3 contained in a substitution variable

    const

    the substitution constant

    index

    the value to find

    returns

    the index of the value

  80. def getValuePos(const: SubstitutionVar, value: Expr): Option[Int]

    Permalink

    Return the index of a given element in the enumeration sort of Z3 contained in a substitution variable

    Return the index of a given element in the enumeration sort of Z3 contained in a substitution variable

    const

    the substitution constant

    value

    the value to find

    returns

    the index of the value

  81. def gt(arg0: Probe, arg1: Probe): Probe

    Permalink
    Definition Classes
    Context
  82. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  83. def interrupt(): Unit

    Permalink
    Definition Classes
    Context
  84. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  85. def le(arg0: Probe, arg1: Probe): Probe

    Permalink
    Definition Classes
    Context
  86. def lt(arg0: Probe, arg1: Probe): Probe

    Permalink
    Definition Classes
    Context
  87. def mkAdd(arg0: <repeated...>[ArithExpr]): ArithExpr

    Permalink
    Definition Classes
    Context
  88. def mkAnd(arg0: <repeated...>[BoolExpr]): BoolExpr

    Permalink
    Definition Classes
    Context
  89. def mkApp(arg0: FuncDecl, arg1: <repeated...>[Expr]): Expr

    Permalink
    Definition Classes
    Context
  90. def mkArrayConst(arg0: String, arg1: Sort, arg2: Sort): ArrayExpr

    Permalink
    Definition Classes
    Context
  91. def mkArrayConst(arg0: Symbol, arg1: Sort, arg2: Sort): ArrayExpr

    Permalink
    Definition Classes
    Context
  92. def mkArrayExt(arg0: ArrayExpr, arg1: ArrayExpr): Expr

    Permalink
    Definition Classes
    Context
  93. def mkArraySort(arg0: Sort, arg1: Sort): ArraySort

    Permalink
    Definition Classes
    Context
  94. def mkBV(arg0: Long, arg1: Int): BitVecNum

    Permalink
    Definition Classes
    Context
  95. def mkBV(arg0: Int, arg1: Int): BitVecNum

    Permalink
    Definition Classes
    Context
  96. def mkBV(arg0: String, arg1: Int): BitVecNum

    Permalink
    Definition Classes
    Context
  97. def mkBV2Int(arg0: BitVecExpr, arg1: Boolean): IntExpr

    Permalink
    Definition Classes
    Context
  98. def mkBVAND(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  99. def mkBVASHR(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  100. def mkBVAdd(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  101. def mkBVAddNoOverflow(arg0: BitVecExpr, arg1: BitVecExpr, arg2: Boolean): BoolExpr

    Permalink
    Definition Classes
    Context
  102. def mkBVAddNoUnderflow(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  103. def mkBVConst(arg0: String, arg1: Int): BitVecExpr

    Permalink
    Definition Classes
    Context
  104. def mkBVConst(arg0: Symbol, arg1: Int): BitVecExpr

    Permalink
    Definition Classes
    Context
  105. def mkBVLSHR(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  106. def mkBVMul(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  107. def mkBVMulNoOverflow(arg0: BitVecExpr, arg1: BitVecExpr, arg2: Boolean): BoolExpr

    Permalink
    Definition Classes
    Context
  108. def mkBVMulNoUnderflow(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  109. def mkBVNAND(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  110. def mkBVNOR(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  111. def mkBVNeg(arg0: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  112. def mkBVNegNoOverflow(arg0: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  113. def mkBVNot(arg0: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  114. def mkBVOR(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  115. def mkBVRedAND(arg0: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  116. def mkBVRedOR(arg0: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  117. def mkBVRotateLeft(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  118. def mkBVRotateLeft(arg0: Int, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  119. def mkBVRotateRight(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  120. def mkBVRotateRight(arg0: Int, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  121. def mkBVSDiv(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  122. def mkBVSDivNoOverflow(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  123. def mkBVSGE(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  124. def mkBVSGT(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  125. def mkBVSHL(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  126. def mkBVSLE(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  127. def mkBVSLT(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  128. def mkBVSMod(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  129. def mkBVSRem(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  130. def mkBVSub(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  131. def mkBVSubNoOverflow(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  132. def mkBVSubNoUnderflow(arg0: BitVecExpr, arg1: BitVecExpr, arg2: Boolean): BoolExpr

    Permalink
    Definition Classes
    Context
  133. def mkBVUDiv(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  134. def mkBVUGE(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  135. def mkBVUGT(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  136. def mkBVULE(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  137. def mkBVULT(arg0: BitVecExpr, arg1: BitVecExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  138. def mkBVURem(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  139. def mkBVXNOR(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  140. def mkBVXOR(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  141. def mkBitVecBound(index: Int, sort: BitVecSort): BitVecExpr

    Permalink

    Create a bit vector bounded variable

    Create a bit vector bounded variable

    index

    the De Bruijn index

    sort

    the bit vector sort

    returns

    bounded variable

  142. def mkBitVecConst(pathIdent: PathIdentType, sort: BitVecSort): BitVecExpr

    Permalink

    Create Z3 bit vector constant

    Create Z3 bit vector constant

    pathIdent

    the name of the constant

    sort

    the bit vector sort of the constant

    returns

    the bitvector constant

  143. def mkBitVecSort(arg0: Int): BitVecSort

    Permalink
    Definition Classes
    Context
  144. def mkBool(arg0: Boolean): BoolExpr

    Permalink
    Definition Classes
    Context
  145. def mkBoolBound(index: Int): BoolExpr

    Permalink

    Create a Boolean bounded variable

    Create a Boolean bounded variable

    index

    the De Bruijn index

    returns

    bounded variable

  146. def mkBoolConst(pathIdent: PathIdentType): BoolExpr

    Permalink

    Create an uninterpreted Boolean constant

    Create an uninterpreted Boolean constant

    pathIdent

    the identifier of the constant

    returns

    Z3 Boolean constant

  147. def mkBoolConst(arg0: String): BoolExpr

    Permalink
    Definition Classes
    Context
  148. def mkBoolConst(arg0: Symbol): BoolExpr

    Permalink
    Definition Classes
    Context
  149. def mkBoolFunDecl(name: String, domain: List[Sort]): FuncDecl

    Permalink

    Create a predicate declaration

    Create a predicate declaration

    name

    the name of the predicate

    domain

    its domain

    returns

    the function declaration

  150. def mkBoolSort(): BoolSort

    Permalink
    Definition Classes
    Context
  151. def mkBound(arg0: Int, arg1: Sort): Expr

    Permalink
    Definition Classes
    Context
  152. def mkConcat(arg0: BitVecExpr, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  153. def mkConst(arg0: FuncDecl): Expr

    Permalink
    Definition Classes
    Context
  154. def mkConst(arg0: String, arg1: Sort): Expr

    Permalink
    Definition Classes
    Context
  155. def mkConst(arg0: Symbol, arg1: Sort): Expr

    Permalink
    Definition Classes
    Context
  156. def mkConstArray(arg0: Sort, arg1: Expr): ArrayExpr

    Permalink
    Definition Classes
    Context
  157. def mkConstDecl(arg0: String, arg1: Sort): FuncDecl

    Permalink
    Definition Classes
    Context
  158. def mkConstDecl(arg0: Symbol, arg1: Sort): FuncDecl

    Permalink
    Definition Classes
    Context
  159. def mkConstructor(arg0: String, arg1: String, arg2: Array[String], arg3: Array[Sort], arg4: Array[Int]): Constructor

    Permalink
    Definition Classes
    Context
  160. def mkConstructor(arg0: Symbol, arg1: Symbol, arg2: Array[Symbol], arg3: Array[Sort], arg4: Array[Int]): Constructor

    Permalink
    Definition Classes
    Context
  161. def mkDatatypeSort(arg0: String, arg1: Array[Constructor]): DatatypeSort

    Permalink
    Definition Classes
    Context
  162. def mkDatatypeSort(arg0: Symbol, arg1: Array[Constructor]): DatatypeSort

    Permalink
    Definition Classes
    Context
  163. def mkDatatypeSorts(arg0: Array[String], arg1: Array[Array[Constructor]]): Array[DatatypeSort]

    Permalink
    Definition Classes
    Context
  164. def mkDatatypeSorts(arg0: Array[Symbol], arg1: Array[Array[Constructor]]): Array[DatatypeSort]

    Permalink
    Definition Classes
    Context
  165. def mkDistinct(arg0: <repeated...>[Expr]): BoolExpr

    Permalink
    Definition Classes
    Context
  166. def mkDiv(arg0: ArithExpr, arg1: ArithExpr): ArithExpr

    Permalink
    Definition Classes
    Context
  167. def mkEmptySet(arg0: Sort): ArrayExpr

    Permalink
    Definition Classes
    Context
  168. def mkEnumSort(arg0: String, arg1: <repeated...>[String]): EnumSort

    Permalink
    Definition Classes
    Context
  169. def mkEnumSort(arg0: Symbol, arg1: <repeated...>[Symbol]): EnumSort

    Permalink
    Definition Classes
    Context
  170. def mkEq(arg0: Expr, arg1: Expr): BoolExpr

    Permalink
    Definition Classes
    Context
  171. def mkExists(arg0: Array[Expr], arg1: Expr, arg2: Int, arg3: Array[Pattern], arg4: Array[Expr], arg5: Symbol, arg6: Symbol): Quantifier

    Permalink
    Definition Classes
    Context
  172. def mkExists(arg0: Array[Sort], arg1: Array[Symbol], arg2: Expr, arg3: Int, arg4: Array[Pattern], arg5: Array[Expr], arg6: Symbol, arg7: Symbol): Quantifier

    Permalink
    Definition Classes
    Context
  173. def mkExtract(arg0: Int, arg1: Int, arg2: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  174. def mkFP(arg0: BitVecExpr, arg1: BitVecExpr, arg2: BitVecExpr): FPExpr

    Permalink
    Definition Classes
    Context
  175. def mkFP(arg0: Boolean, arg1: Long, arg2: Long, arg3: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  176. def mkFP(arg0: Boolean, arg1: Int, arg2: Int, arg3: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  177. def mkFP(arg0: Int, arg1: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  178. def mkFP(arg0: Double, arg1: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  179. def mkFP(arg0: Float, arg1: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  180. def mkFPAbs(arg0: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  181. def mkFPAdd(arg0: FPRMExpr, arg1: FPExpr, arg2: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  182. def mkFPDiv(arg0: FPRMExpr, arg1: FPExpr, arg2: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  183. def mkFPEq(arg0: FPExpr, arg1: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  184. def mkFPFMA(arg0: FPRMExpr, arg1: FPExpr, arg2: FPExpr, arg3: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  185. def mkFPGEq(arg0: FPExpr, arg1: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  186. def mkFPGt(arg0: FPExpr, arg1: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  187. def mkFPInf(arg0: FPSort, arg1: Boolean): FPNum

    Permalink
    Definition Classes
    Context
  188. def mkFPIsInfinite(arg0: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  189. def mkFPIsNaN(arg0: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  190. def mkFPIsNegative(arg0: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  191. def mkFPIsNormal(arg0: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  192. def mkFPIsPositive(arg0: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  193. def mkFPIsSubnormal(arg0: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  194. def mkFPIsZero(arg0: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  195. def mkFPLEq(arg0: FPExpr, arg1: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  196. def mkFPLt(arg0: FPExpr, arg1: FPExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  197. def mkFPMax(arg0: FPExpr, arg1: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  198. def mkFPMin(arg0: FPExpr, arg1: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  199. def mkFPMul(arg0: FPRMExpr, arg1: FPExpr, arg2: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  200. def mkFPNaN(arg0: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  201. def mkFPNeg(arg0: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  202. def mkFPNumeral(arg0: Boolean, arg1: Long, arg2: Long, arg3: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  203. def mkFPNumeral(arg0: Boolean, arg1: Int, arg2: Int, arg3: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  204. def mkFPNumeral(arg0: Int, arg1: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  205. def mkFPNumeral(arg0: Double, arg1: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  206. def mkFPNumeral(arg0: Float, arg1: FPSort): FPNum

    Permalink
    Definition Classes
    Context
  207. def mkFPRNA(): FPRMNum

    Permalink
    Definition Classes
    Context
  208. def mkFPRNE(): FPRMNum

    Permalink
    Definition Classes
    Context
  209. def mkFPRTN(): FPRMNum

    Permalink
    Definition Classes
    Context
  210. def mkFPRTP(): FPRMNum

    Permalink
    Definition Classes
    Context
  211. def mkFPRTZ(): FPRMNum

    Permalink
    Definition Classes
    Context
  212. def mkFPRem(arg0: FPExpr, arg1: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  213. def mkFPRoundNearestTiesToAway(): FPRMNum

    Permalink
    Definition Classes
    Context
  214. def mkFPRoundNearestTiesToEven(): FPRMExpr

    Permalink
    Definition Classes
    Context
  215. def mkFPRoundToIntegral(arg0: FPRMExpr, arg1: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  216. def mkFPRoundTowardNegative(): FPRMNum

    Permalink
    Definition Classes
    Context
  217. def mkFPRoundTowardPositive(): FPRMNum

    Permalink
    Definition Classes
    Context
  218. def mkFPRoundTowardZero(): FPRMNum

    Permalink
    Definition Classes
    Context
  219. def mkFPRoundingModeSort(): FPRMSort

    Permalink
    Definition Classes
    Context
  220. def mkFPSort(arg0: Int, arg1: Int): FPSort

    Permalink
    Definition Classes
    Context
  221. def mkFPSort128(): FPSort

    Permalink
    Definition Classes
    Context
  222. def mkFPSort16(): FPSort

    Permalink
    Definition Classes
    Context
  223. def mkFPSort32(): FPSort

    Permalink
    Definition Classes
    Context
  224. def mkFPSort64(): FPSort

    Permalink
    Definition Classes
    Context
  225. def mkFPSortDouble(): FPSort

    Permalink
    Definition Classes
    Context
  226. def mkFPSortHalf(): FPSort

    Permalink
    Definition Classes
    Context
  227. def mkFPSortQuadruple(): FPSort

    Permalink
    Definition Classes
    Context
  228. def mkFPSortSingle(): FPSort

    Permalink
    Definition Classes
    Context
  229. def mkFPSqrt(arg0: FPRMExpr, arg1: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  230. def mkFPSub(arg0: FPRMExpr, arg1: FPExpr, arg2: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  231. def mkFPToBV(arg0: FPRMExpr, arg1: FPExpr, arg2: Int, arg3: Boolean): BitVecExpr

    Permalink
    Definition Classes
    Context
  232. def mkFPToFP(arg0: FPRMExpr, arg1: IntExpr, arg2: RealExpr, arg3: FPSort): BitVecExpr

    Permalink
    Definition Classes
    Context
  233. def mkFPToFP(arg0: FPSort, arg1: FPRMExpr, arg2: FPExpr): FPExpr

    Permalink
    Definition Classes
    Context
  234. def mkFPToFP(arg0: FPRMExpr, arg1: BitVecExpr, arg2: FPSort, arg3: Boolean): FPExpr

    Permalink
    Definition Classes
    Context
  235. def mkFPToFP(arg0: FPRMExpr, arg1: RealExpr, arg2: FPSort): FPExpr

    Permalink
    Definition Classes
    Context
  236. def mkFPToFP(arg0: FPRMExpr, arg1: FPExpr, arg2: FPSort): FPExpr

    Permalink
    Definition Classes
    Context
  237. def mkFPToFP(arg0: BitVecExpr, arg1: FPSort): FPExpr

    Permalink
    Definition Classes
    Context
  238. def mkFPToIEEEBV(arg0: FPExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  239. def mkFPToReal(arg0: FPExpr): RealExpr

    Permalink
    Definition Classes
    Context
  240. def mkFPZero(arg0: FPSort, arg1: Boolean): FPNum

    Permalink
    Definition Classes
    Context
  241. def mkFalse(): BoolExpr

    Permalink
    Definition Classes
    Context
  242. def mkFiniteDomainSort(arg0: String, arg1: Long): FiniteDomainSort

    Permalink
    Definition Classes
    Context
  243. def mkFiniteDomainSort(arg0: Symbol, arg1: Long): FiniteDomainSort

    Permalink
    Definition Classes
    Context
  244. def mkFixedpoint(): Fixedpoint

    Permalink
    Definition Classes
    Context
  245. def mkForall(arg0: Array[Expr], arg1: Expr, arg2: Int, arg3: Array[Pattern], arg4: Array[Expr], arg5: Symbol, arg6: Symbol): Quantifier

    Permalink
    Definition Classes
    Context
  246. def mkForall(arg0: Array[Sort], arg1: Array[Symbol], arg2: Expr, arg3: Int, arg4: Array[Pattern], arg5: Array[Expr], arg6: Symbol, arg7: Symbol): Quantifier

    Permalink
    Definition Classes
    Context
  247. def mkFreshConst(arg0: String, arg1: Sort): Expr

    Permalink
    Definition Classes
    Context
  248. def mkFreshConstDecl(arg0: String, arg1: Sort): FuncDecl

    Permalink
    Definition Classes
    Context
  249. def mkFreshFuncDecl(arg0: String, arg1: Array[Sort], arg2: Sort): FuncDecl

    Permalink
    Definition Classes
    Context
  250. def mkFullSet(arg0: Sort): ArrayExpr

    Permalink
    Definition Classes
    Context
  251. def mkFuncDecl(arg0: String, arg1: Sort, arg2: Sort): FuncDecl

    Permalink
    Definition Classes
    Context
  252. def mkFuncDecl(arg0: String, arg1: Array[Sort], arg2: Sort): FuncDecl

    Permalink
    Definition Classes
    Context
  253. def mkFuncDecl(arg0: Symbol, arg1: Sort, arg2: Sort): FuncDecl

    Permalink
    Definition Classes
    Context
  254. def mkFuncDecl(arg0: Symbol, arg1: Array[Sort], arg2: Sort): FuncDecl

    Permalink
    Definition Classes
    Context
  255. def mkGe(arg0: ArithExpr, arg1: ArithExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  256. def mkGoal(arg0: Boolean, arg1: Boolean, arg2: Boolean): Goal

    Permalink
    Definition Classes
    Context
  257. def mkGt(arg0: ArithExpr, arg1: ArithExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  258. def mkITE(arg0: BoolExpr, arg1: Expr, arg2: Expr): Expr

    Permalink
    Definition Classes
    Context
  259. def mkIff(arg0: BoolExpr, arg1: BoolExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  260. def mkImplies(arg0: BoolExpr, arg1: BoolExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  261. def mkInt(arg0: Long): IntNum

    Permalink
    Definition Classes
    Context
  262. def mkInt(arg0: Int): IntNum

    Permalink
    Definition Classes
    Context
  263. def mkInt(arg0: String): IntNum

    Permalink
    Definition Classes
    Context
  264. def mkInt2BV(arg0: Int, arg1: IntExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  265. def mkInt2Real(arg0: IntExpr): RealExpr

    Permalink
    Definition Classes
    Context
  266. def mkIntConst(arg0: String): IntExpr

    Permalink
    Definition Classes
    Context
  267. def mkIntConst(arg0: Symbol): IntExpr

    Permalink
    Definition Classes
    Context
  268. def mkIntSort(): IntSort

    Permalink
    Definition Classes
    Context
  269. def mkIsInteger(arg0: RealExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  270. def mkIte[T <: Expr](i: BoolExpr, t: T, e: T): T

    Permalink

    Create an if then else structure

    Create an if then else structure

    T

    the type of the else and then expression

    i

    the if expression

    t

    the then expression

    e

    the else expression

    returns

    the if-then-else term

  271. def mkLe(arg0: ArithExpr, arg1: ArithExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  272. def mkListSort(arg0: String, arg1: Sort): ListSort

    Permalink
    Definition Classes
    Context
  273. def mkListSort(arg0: Symbol, arg1: Sort): ListSort

    Permalink
    Definition Classes
    Context
  274. def mkLt(arg0: ArithExpr, arg1: ArithExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  275. def mkMap(arg0: FuncDecl, arg1: <repeated...>[ArrayExpr]): ArrayExpr

    Permalink
    Definition Classes
    Context
  276. def mkMod(arg0: IntExpr, arg1: IntExpr): IntExpr

    Permalink
    Definition Classes
    Context
  277. def mkMul(arg0: <repeated...>[ArithExpr]): ArithExpr

    Permalink
    Definition Classes
    Context
  278. def mkNot(arg0: BoolExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  279. def mkNumeral(arg0: Long, arg1: Sort): Expr

    Permalink
    Definition Classes
    Context
  280. def mkNumeral(arg0: Int, arg1: Sort): Expr

    Permalink
    Definition Classes
    Context
  281. def mkNumeral(arg0: String, arg1: Sort): Expr

    Permalink
    Definition Classes
    Context
  282. def mkOptimize(): Optimize

    Permalink
    Definition Classes
    Context
  283. def mkOr(arg0: <repeated...>[BoolExpr]): BoolExpr

    Permalink
    Definition Classes
    Context
  284. def mkParams(): Params

    Permalink
    Definition Classes
    Context
  285. def mkPattern(arg0: <repeated...>[Expr]): Pattern

    Permalink
    Definition Classes
    Context
  286. def mkPower(arg0: ArithExpr, arg1: ArithExpr): ArithExpr

    Permalink
    Definition Classes
    Context
  287. def mkProbe(arg0: String): Probe

    Permalink
    Definition Classes
    Context
  288. def mkQuantifier(arg0: Boolean, arg1: Array[Expr], arg2: Expr, arg3: Int, arg4: Array[Pattern], arg5: Array[Expr], arg6: Symbol, arg7: Symbol): Quantifier

    Permalink
    Definition Classes
    Context
  289. def mkQuantifier(arg0: Boolean, arg1: Array[Sort], arg2: Array[Symbol], arg3: Expr, arg4: Int, arg5: Array[Pattern], arg6: Array[Expr], arg7: Symbol, arg8: Symbol): Quantifier

    Permalink
    Definition Classes
    Context
  290. def mkReSort(arg0: Sort): ReSort

    Permalink
    Definition Classes
    Context
  291. def mkReal(arg0: Long): RatNum

    Permalink
    Definition Classes
    Context
  292. def mkReal(arg0: Int): RatNum

    Permalink
    Definition Classes
    Context
  293. def mkReal(arg0: String): RatNum

    Permalink
    Definition Classes
    Context
  294. def mkReal(arg0: Int, arg1: Int): RatNum

    Permalink
    Definition Classes
    Context
  295. def mkReal2Int(arg0: RealExpr): IntExpr

    Permalink
    Definition Classes
    Context
  296. def mkRealConst(arg0: String): RealExpr

    Permalink
    Definition Classes
    Context
  297. def mkRealConst(arg0: Symbol): RealExpr

    Permalink
    Definition Classes
    Context
  298. def mkRealSort(): RealSort

    Permalink
    Definition Classes
    Context
  299. def mkRem(arg0: IntExpr, arg1: IntExpr): IntExpr

    Permalink
    Definition Classes
    Context
  300. def mkRepeat(arg0: Int, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  301. def mkSelect(arg0: ArrayExpr, arg1: Expr): Expr

    Permalink
    Definition Classes
    Context
  302. def mkSeqSort(arg0: Sort): SeqSort

    Permalink
    Definition Classes
    Context
  303. def mkSetAdd(arg0: ArrayExpr, arg1: Expr): ArrayExpr

    Permalink
    Definition Classes
    Context
  304. def mkSetComplement(arg0: ArrayExpr): ArrayExpr

    Permalink
    Definition Classes
    Context
  305. def mkSetDel(arg0: ArrayExpr, arg1: Expr): ArrayExpr

    Permalink
    Definition Classes
    Context
  306. def mkSetDifference(arg0: ArrayExpr, arg1: ArrayExpr): ArrayExpr

    Permalink
    Definition Classes
    Context
  307. def mkSetIntersection(arg0: <repeated...>[ArrayExpr]): ArrayExpr

    Permalink
    Definition Classes
    Context
  308. def mkSetMembership(arg0: Expr, arg1: ArrayExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  309. def mkSetSort(arg0: Sort): SetSort

    Permalink
    Definition Classes
    Context
  310. def mkSetSubset(arg0: ArrayExpr, arg1: ArrayExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  311. def mkSetUnion(arg0: <repeated...>[ArrayExpr]): ArrayExpr

    Permalink
    Definition Classes
    Context
  312. def mkSignExt(arg0: Int, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  313. def mkSimpleSolver(): Solver

    Permalink
    Definition Classes
    Context
  314. def mkSolver(arg0: Tactic): Solver

    Permalink
    Definition Classes
    Context
  315. def mkSolver(arg0: String): Solver

    Permalink
    Definition Classes
    Context
  316. def mkSolver(arg0: Symbol): Solver

    Permalink
    Definition Classes
    Context
  317. def mkSolver(): Solver

    Permalink
    Definition Classes
    Context
  318. def mkStore(arg0: ArrayExpr, arg1: Expr, arg2: Expr): ArrayExpr

    Permalink
    Definition Classes
    Context
  319. def mkStringSort(): SeqSort

    Permalink
    Definition Classes
    Context
  320. def mkSub(arg0: <repeated...>[ArithExpr]): ArithExpr

    Permalink
    Definition Classes
    Context
  321. def mkSymbol(arg0: String): StringSymbol

    Permalink
    Definition Classes
    Context
  322. def mkSymbol(arg0: Int): IntSymbol

    Permalink
    Definition Classes
    Context
  323. def mkTactic(arg0: String): Tactic

    Permalink
    Definition Classes
    Context
  324. def mkTermArray(arg0: ArrayExpr): Expr

    Permalink
    Definition Classes
    Context
  325. def mkTrue(): BoolExpr

    Permalink
    Definition Classes
    Context
  326. def mkTupleSort(arg0: Symbol, arg1: Array[Symbol], arg2: Array[Sort]): TupleSort

    Permalink
    Definition Classes
    Context
  327. def mkUnaryMinus(arg0: ArithExpr): ArithExpr

    Permalink
    Definition Classes
    Context
  328. def mkUninterpretedSort(arg0: String): UninterpretedSort

    Permalink
    Definition Classes
    Context
  329. def mkUninterpretedSort(arg0: Symbol): UninterpretedSort

    Permalink
    Definition Classes
    Context
  330. def mkXor(arg0: BoolExpr, arg1: BoolExpr): BoolExpr

    Permalink
    Definition Classes
    Context
  331. def mkZeroExt(arg0: Int, arg1: BitVecExpr): BitVecExpr

    Permalink
    Definition Classes
    Context
  332. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  333. def not(arg0: Probe): Probe

    Permalink
    Definition Classes
    Context
  334. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  335. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  336. def or(arg0: Probe, arg1: Probe): Probe

    Permalink
    Definition Classes
    Context
  337. def orElse(arg0: Tactic, arg1: Tactic): Tactic

    Permalink
    Definition Classes
    Context
  338. def parAndThen(arg0: Tactic, arg1: Tactic): Tactic

    Permalink
    Definition Classes
    Context
  339. def parOr(arg0: <repeated...>[Tactic]): Tactic

    Permalink
    Definition Classes
    Context
  340. def parseSMTLIB2File(arg0: String, arg1: Array[Symbol], arg2: Array[Sort], arg3: Array[Symbol], arg4: Array[FuncDecl]): BoolExpr

    Permalink
    Definition Classes
    Context
  341. def parseSMTLIB2String(arg0: String, arg1: Array[Symbol], arg2: Array[Sort], arg3: Array[Symbol], arg4: Array[FuncDecl]): BoolExpr

    Permalink
    Definition Classes
    Context
  342. def parseSMTLIBFile(arg0: String, arg1: Array[Symbol], arg2: Array[Sort], arg3: Array[Symbol], arg4: Array[FuncDecl]): Unit

    Permalink
    Definition Classes
    Context
  343. def parseSMTLIBString(arg0: String, arg1: Array[Symbol], arg2: Array[Sort], arg3: Array[Symbol], arg4: Array[FuncDecl]): Unit

    Permalink
    Definition Classes
    Context
  344. def repeat(arg0: Tactic, arg1: Int): Tactic

    Permalink
    Definition Classes
    Context
  345. def setPrintMode(arg0: Z3_ast_print_mode): Unit

    Permalink
    Definition Classes
    Context
  346. def skip(): Tactic

    Permalink
    Definition Classes
    Context
  347. def substituteIn[T <: Expr, U <: Expr](in: T, by: Map[U, U]): T

    Permalink

    Substitute the variable of Z3 SMT expression by some other variables

    Substitute the variable of Z3 SMT expression by some other variables

    T

    the type of the expression

    U

    the type of the variables

    in

    the initial expression

    by

    the map from initial to new variables

    returns

    the expression where variables have been substituted

  348. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  349. def then(arg0: Tactic, arg1: Tactic, arg2: <repeated...>[Tactic]): Tactic

    Permalink
    Definition Classes
    Context
  350. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  351. def tryFor(arg0: Tactic, arg1: Int): Tactic

    Permalink
    Definition Classes
    Context
  352. def unwrapAST(arg0: AST): Long

    Permalink
    Definition Classes
    Context
  353. def updateParamValue(arg0: String, arg1: String): Unit

    Permalink
    Definition Classes
    Context
  354. def usingParams(arg0: Tactic, arg1: Params): Tactic

    Permalink
    Definition Classes
    Context
  355. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  356. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  357. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  358. def when(arg0: Probe, arg1: Tactic): Tactic

    Permalink
    Definition Classes
    Context
  359. def with(arg0: Tactic, arg1: Params): Tactic

    Permalink
    Definition Classes
    Context
  360. def wrapAST(arg0: Long): AST

    Permalink
    Definition Classes
    Context

Deprecated Value Members

  1. def toCube(cube: Traversable[(SubstitutionVar, Expr)]): BoolExpr

    Permalink

    Transform a set of

    Transform a set of

    cube

    the set of substitution variable / value couples

    returns

    the conjunction of the "sub = val" equalities

    Annotations
    @deprecated
    Deprecated

    (Since version KCR analyzer 1.0) Should use the Choose predicate to force value of a substitution predicate

Inherited from Context

Inherited from IDisposable

Inherited from AnyRef

Inherited from Any

Ungrouped