Packages

p

z3

scala

package scala

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. scala
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
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.

    A type class for Scala types that are representable in Z3 and that admit a default value. The default value is used for model reconstruction when no other value is available.

    Annotations
    @implicitNotFound( ... )
  2. sealed class Z3AST extends Z3ASTLike
  3. sealed abstract class Z3ASTKind extends AnyRef
  4. trait Z3ASTLike extends Z3Object
  5. final class Z3ASTVector extends Z3Object
  6. case class Z3AppAST extends Z3ASTKind with Product with Serializable
  7. sealed class Z3Context extends AnyRef
  8. sealed abstract class Z3DeclKind extends AnyRef
  9. sealed class Z3FuncDecl extends Z3ASTLike
  10. case class Z3FuncDeclAST extends Z3ASTKind with Product with Serializable
  11. case class Z3IntSymbol extends Z3SymbolKind[Int] with Product with Serializable
  12. sealed class Z3Model extends Z3Object
  13. sealed abstract class Z3NumeralAST extends Z3ASTKind
  14. case class Z3NumeralIntAST extends Z3NumeralAST with Product with Serializable
  15. case class Z3NumeralRealAST extends Z3NumeralAST with Product with Serializable
  16. trait Z3Object extends Z3Pointer
  17. class Z3Optimizer extends Z3Object
  18. sealed class Z3Pattern extends Z3ASTLike
  19. trait Z3Pointer extends AnyRef
  20. case class Z3QuantifierAST extends Z3ASTKind with Product with Serializable
  21. class Z3RefCountQueue[T <: Z3Object] extends AnyRef
  22. sealed abstract class Z3SearchFailure extends AnyRef
  23. class Z3Solver extends Z3Object
  24. sealed class Z3Sort extends Z3ASTLike
  25. case class Z3SortAST extends Z3ASTKind with Product with Serializable
  26. case class Z3StringSymbol extends Z3SymbolKind[String] with Product with Serializable
  27. sealed class Z3Symbol extends Z3Pointer
  28. sealed abstract class Z3SymbolKind[T] extends AnyRef
  29. class Z3Tactic extends Z3Object
  30. case class Z3VarAST extends Z3ASTKind with Product with Serializable

Value Members

  1. implicit def astvectorToSeq(v: Z3ASTVector): Seq[Z3AST]
  2. def error(any: Any): Nothing
  3. def i2ob(value: Int): Option[Boolean]
    Attributes
    protected[z3]
  4. def resetMemory: Unit
  5. def toPtrArray(ptrs: Iterable[Z3Pointer]): Array[Long]
    Attributes
    protected[z3]
  6. def toggleWarningMessages(enabled: Boolean): Unit
  7. lazy val version: String

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

  8. object OpAGNum extends Z3DeclKind
  9. object OpANum extends Z3DeclKind
  10. object OpAdd extends Z3DeclKind
  11. object OpAnd extends Z3DeclKind
  12. object OpArrayDefault extends Z3DeclKind
  13. object OpArrayExt extends Z3DeclKind
  14. object OpArrayMap extends Z3DeclKind
  15. object OpAsArray extends Z3DeclKind
  16. object OpBAdd extends Z3DeclKind
  17. object OpBAnd extends Z3DeclKind
  18. object OpBAshr extends Z3DeclKind
  19. object OpBComp extends Z3DeclKind
  20. object OpBLshr extends Z3DeclKind
  21. object OpBMul extends Z3DeclKind
  22. object OpBNand extends Z3DeclKind
  23. object OpBNeg extends Z3DeclKind
  24. object OpBNor extends Z3DeclKind
  25. object OpBNot extends Z3DeclKind
  26. object OpBNum extends Z3DeclKind
  27. object OpBOr extends Z3DeclKind
  28. object OpBRedAnd extends Z3DeclKind
  29. object OpBRedOr extends Z3DeclKind
  30. object OpBSDiv extends Z3DeclKind
  31. object OpBSMod extends Z3DeclKind
  32. object OpBSRem extends Z3DeclKind
  33. object OpBShl extends Z3DeclKind
  34. object OpBSub extends Z3DeclKind
  35. object OpBUDiv extends Z3DeclKind
  36. object OpBURem extends Z3DeclKind
  37. object OpBVToInt extends Z3DeclKind
  38. object OpBXnor extends Z3DeclKind
  39. object OpBXor extends Z3DeclKind
  40. object OpBit0 extends Z3DeclKind
  41. object OpBit1 extends Z3DeclKind
  42. object OpCarry extends Z3DeclKind
  43. object OpConcat extends Z3DeclKind
  44. object OpConstArray extends Z3DeclKind
  45. object OpDTAccessor extends Z3DeclKind
  46. object OpDTConstructor extends Z3DeclKind
  47. object OpDTRecogniser extends Z3DeclKind
  48. object OpDTUpdateField extends Z3DeclKind
  49. object OpDistinct extends Z3DeclKind
  50. object OpDiv extends Z3DeclKind
  51. object OpEq extends Z3DeclKind
  52. object OpExtRotateLeft extends Z3DeclKind
  53. object OpExtRotateRight extends Z3DeclKind
  54. object OpExtract extends Z3DeclKind
  55. object OpFPAAbs extends Z3DeclKind
  56. object OpFPAAdd extends Z3DeclKind
  57. object OpFPADiv extends Z3DeclKind
  58. object OpFPAEq extends Z3DeclKind
  59. object OpFPAFMA extends Z3DeclKind
  60. object OpFPAFP extends Z3DeclKind
  61. object OpFPAGE extends Z3DeclKind
  62. object OpFPAGT extends Z3DeclKind
  63. object OpFPAIsInf extends Z3DeclKind
  64. object OpFPAIsNaN extends Z3DeclKind
  65. object OpFPAIsNegative extends Z3DeclKind
  66. object OpFPAIsNormal extends Z3DeclKind
  67. object OpFPAIsPositive extends Z3DeclKind
  68. object OpFPAIsSubnormal extends Z3DeclKind
  69. object OpFPAIsZero extends Z3DeclKind
  70. object OpFPALE extends Z3DeclKind
  71. object OpFPALT extends Z3DeclKind
  72. object OpFPAMax extends Z3DeclKind
  73. object OpFPAMin extends Z3DeclKind
  74. object OpFPAMinusInf extends Z3DeclKind
  75. object OpFPAMinusZero extends Z3DeclKind
  76. object OpFPAMul extends Z3DeclKind
  77. object OpFPANaN extends Z3DeclKind
  78. object OpFPANeg extends Z3DeclKind
  79. object OpFPANum extends Z3DeclKind
  80. object OpFPAPlusInf extends Z3DeclKind
  81. object OpFPAPlusZero extends Z3DeclKind
  82. object OpFPARem extends Z3DeclKind
  83. object OpFPARmNearestTiesToAway extends Z3DeclKind
  84. object OpFPARmNearestTiesToEven extends Z3DeclKind
  85. object OpFPARmTowardNegative extends Z3DeclKind
  86. object OpFPARmTowardPositive extends Z3DeclKind
  87. object OpFPARmTowardZero extends Z3DeclKind
  88. object OpFPARoundToIntegral extends Z3DeclKind
  89. object OpFPASqrt extends Z3DeclKind
  90. object OpFPASub extends Z3DeclKind
  91. object OpFPAToFP extends Z3DeclKind
  92. object OpFPAToFPUnsigned extends Z3DeclKind
  93. object OpFPAToIEEEBV extends Z3DeclKind
  94. object OpFPAToReal extends Z3DeclKind
  95. object OpFPAToSBV extends Z3DeclKind
  96. object OpFPAToUBV extends Z3DeclKind
  97. object OpFalse extends Z3DeclKind
  98. object OpFdConstant extends Z3DeclKind
  99. object OpFdLT extends Z3DeclKind
  100. object OpGE extends Z3DeclKind
  101. object OpGT extends Z3DeclKind
  102. object OpIDiv extends Z3DeclKind
  103. object OpITE extends Z3DeclKind
  104. object OpIff extends Z3DeclKind
  105. object OpImplies extends Z3DeclKind
  106. object OpIntToBV extends Z3DeclKind
  107. object OpInternal extends Z3DeclKind
  108. object OpIsInt extends Z3DeclKind
  109. object OpLE extends Z3DeclKind
  110. object OpLT extends Z3DeclKind
  111. object OpLabel extends Z3DeclKind
  112. object OpLabelLit extends Z3DeclKind
  113. object OpMod extends Z3DeclKind
  114. object OpMul extends Z3DeclKind
  115. object OpNot extends Z3DeclKind
  116. object OpOEq extends Z3DeclKind
  117. object OpOr extends Z3DeclKind
  118. object OpPBAtMost extends Z3DeclKind
  119. object OpPBGE extends Z3DeclKind
  120. object OpPBLE extends Z3DeclKind
  121. object OpPower extends Z3DeclKind
  122. object OpPrAndElim extends Z3DeclKind
  123. object OpPrApplyDef extends Z3DeclKind
  124. object OpPrAsserted extends Z3DeclKind
  125. object OpPrCommutativity extends Z3DeclKind
  126. object OpPrDER extends Z3DeclKind
  127. object OpPrDefAxiom extends Z3DeclKind
  128. object OpPrDefIntro extends Z3DeclKind
  129. object OpPrDistributivity extends Z3DeclKind
  130. object OpPrElimUnusedVars extends Z3DeclKind
  131. object OpPrGoal extends Z3DeclKind
  132. object OpPrHyperResolve extends Z3DeclKind
  133. object OpPrHypothesis extends Z3DeclKind
  134. object OpPrIffFalse extends Z3DeclKind
  135. object OpPrIffOEq extends Z3DeclKind
  136. object OpPrIffTrue extends Z3DeclKind
  137. object OpPrLemma extends Z3DeclKind
  138. object OpPrModusPonens extends Z3DeclKind
  139. object OpPrModusPonensOEq extends Z3DeclKind
  140. object OpPrMonotonicity extends Z3DeclKind
  141. object OpPrNNFNeg extends Z3DeclKind
  142. object OpPrNNFPos extends Z3DeclKind
  143. object OpPrNotOrElim extends Z3DeclKind
  144. object OpPrPullQuant extends Z3DeclKind
  145. object OpPrPushQuant extends Z3DeclKind
  146. object OpPrQuantInst extends Z3DeclKind
  147. object OpPrQuantIntro extends Z3DeclKind
  148. object OpPrReflexivity extends Z3DeclKind
  149. object OpPrRewrite extends Z3DeclKind
  150. object OpPrRewriteStar extends Z3DeclKind
  151. object OpPrSkolemize extends Z3DeclKind
  152. object OpPrSymmetry extends Z3DeclKind
  153. object OpPrThLemma extends Z3DeclKind
  154. object OpPrTransitivity extends Z3DeclKind
  155. object OpPrTransitivityStar extends Z3DeclKind
  156. object OpPrTrue extends Z3DeclKind
  157. object OpPrUndef extends Z3DeclKind
  158. object OpPrUnitResolution extends Z3DeclKind
  159. object OpRAClone extends Z3DeclKind
  160. object OpRAComplement extends Z3DeclKind
  161. object OpRAEmpty extends Z3DeclKind
  162. object OpRAFilter extends Z3DeclKind
  163. object OpRAIsEmpty extends Z3DeclKind
  164. object OpRAJoin extends Z3DeclKind
  165. object OpRANegationFilter extends Z3DeclKind
  166. object OpRAProject extends Z3DeclKind
  167. object OpRARename extends Z3DeclKind
  168. object OpRASelect extends Z3DeclKind
  169. object OpRAStore extends Z3DeclKind
  170. object OpRAUnion extends Z3DeclKind
  171. object OpRAWiden extends Z3DeclKind
  172. object OpREConcat extends Z3DeclKind
  173. object OpREOption extends Z3DeclKind
  174. object OpREPlus extends Z3DeclKind
  175. object OpREStar extends Z3DeclKind
  176. object OpREUnion extends Z3DeclKind
  177. object OpRem extends Z3DeclKind
  178. object OpRepeat extends Z3DeclKind
  179. object OpRotateLeft extends Z3DeclKind
  180. object OpRotateRight extends Z3DeclKind
  181. object OpSGE extends Z3DeclKind
  182. object OpSGT extends Z3DeclKind
  183. object OpSLE extends Z3DeclKind
  184. object OpSLT extends Z3DeclKind
  185. object OpSelect extends Z3DeclKind
  186. object OpSeqAt extends Z3DeclKind
  187. object OpSeqConcat extends Z3DeclKind
  188. object OpSeqContains extends Z3DeclKind
  189. object OpSeqEmpty extends Z3DeclKind
  190. object OpSeqExtract extends Z3DeclKind
  191. object OpSeqInRE extends Z3DeclKind
  192. object OpSeqIndex extends Z3DeclKind
  193. object OpSeqLength extends Z3DeclKind
  194. object OpSeqPrefix extends Z3DeclKind
  195. object OpSeqReplace extends Z3DeclKind
  196. object OpSeqSuffix extends Z3DeclKind
  197. object OpSeqToRE extends Z3DeclKind
  198. object OpSeqUnit extends Z3DeclKind
  199. object OpSetComplement extends Z3DeclKind
  200. object OpSetDifference extends Z3DeclKind
  201. object OpSetIntersect extends Z3DeclKind
  202. object OpSetSubset extends Z3DeclKind
  203. object OpSetUnion extends Z3DeclKind
  204. object OpSignExt extends Z3DeclKind
  205. object OpStore extends Z3DeclKind
  206. object OpSub extends Z3DeclKind
  207. object OpToInt extends Z3DeclKind
  208. object OpToReal extends Z3DeclKind
  209. object OpTrue extends Z3DeclKind
  210. object OpUGE extends Z3DeclKind
  211. object OpUGT extends Z3DeclKind
  212. object OpULE extends Z3DeclKind
  213. object OpULT extends Z3DeclKind
  214. object OpUMinus extends Z3DeclKind
  215. object OpUninterpreted extends Z3DeclKind
  216. object OpXor extends Z3DeclKind
  217. object OpXor3 extends Z3DeclKind
  218. object OpZeroExt extends Z3DeclKind
  219. object Other extends Z3DeclKind
  220. object Z3Canceled extends Z3SearchFailure with Product with Serializable
  221. object Z3Context
  222. object Z3DeclKind
  223. object Z3IncompleteTheory extends Z3SearchFailure with Product with Serializable
  224. object Z3MemoutWatermark extends Z3SearchFailure with Product with Serializable
  225. object Z3Model
  226. object Z3NoFailure extends Z3SearchFailure with Product with Serializable
  227. object Z3NumConflicts extends Z3SearchFailure with Product with Serializable
  228. object Z3Quantifiers extends Z3SearchFailure with Product with Serializable
  229. object Z3Timeout extends Z3SearchFailure with Product with Serializable
  230. object Z3Unknown extends Z3SearchFailure with Product with Serializable
  231. object Z3UnknownAST extends Z3ASTKind with Product with Serializable

Inherited from AnyRef

Inherited from Any

Ungrouped