z3.scala

Z3Context

class Z3Context extends AnyRef

Attributes
sealed
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By inheritance
Inherited
  1. Hide All
  2. Show all
  1. Z3Context
  2. AnyRef
  3. Any
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Z3Context (params: (String, Any)*)

  2. new Z3Context (config: Z3Config)

Value Members

  1. def != (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef

  2. def != (arg0: Any): Boolean

    Attributes
    final
    Definition Classes
    Any

  3. def ## (): Int

    Attributes
    final
    Definition Classes
    AnyRef → Any

  4. def == (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef

  5. def == (arg0: Any): Boolean

    Attributes
    final
    Definition Classes
    Any

  6. def asInstanceOf [T0] : T0

    Attributes
    final
    Definition Classes
    Any

  7. def assertCnstr (tree: Tree[BoolSort]): Unit

  8. def assertCnstr (ast: Z3AST): Unit

  9. def astToString (ast: Z3AST): String

  10. def benchmarkToSMTLIBString (name: String, logic: String, status: String, attributes: String, assumptions: Seq[Z3AST], formula: Z3AST): String

  11. def blockLiterals (lbls: Z3Literals): Unit

  12. def check (): Option[Boolean]

  13. def checkAndGetAllEventualModels (): Iterator[(Option[Boolean], Z3Model)]

  14. def checkAndGetAllModels (): Iterator[Z3Model]

  15. def checkAndGetModel (): (Option[Boolean], Z3Model)

  16. def checkAssumptions (assumptions: Z3AST*): (Option[Boolean], Z3Model, Seq[Z3AST])

  17. def clone (): AnyRef

    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws()

  18. val config : Z3Config

  19. def delete (): Unit

  20. def disableLiteral (lbls: Z3Literals, idx: Int): Unit

  21. def eq (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef

  22. def equals (arg0: Any): Boolean

    Definition Classes
    AnyRef → Any

  23. def finalize (): Unit

    Definition Classes
    Z3Context → AnyRef

  24. def funcDeclToString (funcDecl: Z3FuncDecl): String

  25. def getASTKind (ast: Z3AST): Z3ASTKind

  26. def getAppDecl (ast: Z3AST, arity: Int = 1): Z3FuncDecl

  27. def getBoolValue (ast: Z3AST): Option[Boolean]

  28. def getClass (): java.lang.Class[_]

    Attributes
    final
    Definition Classes
    AnyRef → Any

  29. def getDeclFuncDeclParameter (fd: Z3FuncDecl, idx: Int, arity: Int = 1): Z3FuncDecl

  30. def getDeclKind (funcDecl: Z3FuncDecl): Value

  31. def getDeclName (fd: Z3FuncDecl): Z3Symbol

  32. def getDomain (funcDecl: Z3FuncDecl, i: Int): Z3Sort

  33. def getDomainSize (funcDecl: Z3FuncDecl): Int

  34. def getGuessedLiterals : Z3Literals

  35. def getLiteral (lbls: Z3Literals, idx: Int): Z3AST

  36. def getNumLiterals (lbls: Z3Literals): Int

  37. def getNumScopes (): Int

  38. def getNumeralInt (ast: Z3AST): Option[Int]

  39. def getRange (funcDecl: Z3FuncDecl): Z3Sort

  40. def getRelevantLiterals : Z3Literals

  41. def getSMTLIBAssumptions : Iterator[Z3AST]

    Returns an iterator of the assumptions created by the SMT-LIB parser.

  42. def getSMTLIBDecls : Iterator[Z3FuncDecl]

    Returns an iterator of the function and constant declarations created by the SMT-LIB parser.

  43. def getSMTLIBError : String

    Returns the last error issued by the SMT-LIB parser.

  44. def getSMTLIBFormulas : Iterator[Z3AST]

    Returns an iterator of the formulas created by the SMT-LIB parser.

  45. def getSMTLIBSorts : Iterator[Z3Sort]

    Returns an iterator of the sorts created by the SMT-LIB parser.

  46. def getSearchFailure : Z3SearchFailure

  47. def getSort (ast: Z3AST): Z3Sort

  48. def getSymbolKind (symbol: Z3Symbol): z3.scala.Z3SymbolKind[_]

  49. def hashCode (): Int

    Definition Classes
    AnyRef → Any

  50. def isEqAST (t1: Z3AST, t2: Z3AST): Boolean

  51. def isEqFuncDecl (fd1: Z3FuncDecl, fd2: Z3FuncDecl): Boolean

  52. def isEqSort (s1: Z3Sort, s2: Z3Sort): Boolean

  53. def isInstanceOf [T0] : Boolean

    Attributes
    final
    Definition Classes
    Any

  54. def mkADTSorts (defs: Seq[(String, Seq[String], Seq[Seq[(String, ADTSortReference)]])]): Seq[(Z3Sort, Seq[Z3FuncDecl], Seq[Z3FuncDecl], Seq[Seq[Z3FuncDecl]])]

  55. def mkAdd (args: Z3AST*): Z3AST

  56. def mkAnd (args: Z3AST*): Z3AST

  57. def mkApp (funcDecl: Z3FuncDecl, args: Z3AST*): Z3AST

  58. def mkArrayDefault (array: Z3AST): Z3AST

  59. def mkArraySort (domain: Z3Sort, range: Z3Sort): Z3Sort

  60. def mkBVAdd (ast1: Z3AST, ast2: Z3AST): Z3AST

  61. def mkBVAddNoOverflow (ast1: Z3AST, ast2: Z3AST, isSigned: Boolean): Z3AST

  62. def mkBVAnd (ast1: Z3AST, ast2: Z3AST): Z3AST

  63. def mkBVAshr (ast1: Z3AST, ast2: Z3AST): Z3AST

  64. def mkBVLshr (ast1: Z3AST, ast2: Z3AST): Z3AST

  65. def mkBVMul (ast1: Z3AST, ast2: Z3AST): Z3AST

  66. def mkBVNand (ast1: Z3AST, ast2: Z3AST): Z3AST

  67. def mkBVNeg (ast: Z3AST): Z3AST

  68. def mkBVNor (ast1: Z3AST, ast2: Z3AST): Z3AST

  69. def mkBVNot (ast: Z3AST): Z3AST

  70. def mkBVOr (ast1: Z3AST, ast2: Z3AST): Z3AST

  71. def mkBVRedAnd (ast: Z3AST): Z3AST

  72. def mkBVRedOr (ast: Z3AST): Z3AST

  73. def mkBVSdiv (ast1: Z3AST, ast2: Z3AST): Z3AST

  74. def mkBVSge (ast1: Z3AST, ast2: Z3AST): Z3AST

  75. def mkBVSgt (ast1: Z3AST, ast2: Z3AST): Z3AST

  76. def mkBVShl (ast1: Z3AST, ast2: Z3AST): Z3AST

  77. def mkBVSle (ast1: Z3AST, ast2: Z3AST): Z3AST

  78. def mkBVSlt (ast1: Z3AST, ast2: Z3AST): Z3AST

  79. def mkBVSmod (ast1: Z3AST, ast2: Z3AST): Z3AST

  80. def mkBVSort (size: Int): Z3Sort

  81. def mkBVSrem (ast1: Z3AST, ast2: Z3AST): Z3AST

  82. def mkBVSub (ast1: Z3AST, ast2: Z3AST): Z3AST

  83. def mkBVUdiv (ast1: Z3AST, ast2: Z3AST): Z3AST

  84. def mkBVUge (ast1: Z3AST, ast2: Z3AST): Z3AST

  85. def mkBVUgt (ast1: Z3AST, ast2: Z3AST): Z3AST

  86. def mkBVUle (ast1: Z3AST, ast2: Z3AST): Z3AST

  87. def mkBVUlt (ast1: Z3AST, ast2: Z3AST): Z3AST

  88. def mkBVUrem (ast1: Z3AST, ast2: Z3AST): Z3AST

  89. def mkBVXnor (ast1: Z3AST, ast2: Z3AST): Z3AST

  90. def mkBVXor (ast1: Z3AST, ast2: Z3AST): Z3AST

  91. def mkBoolConst (s: String): Z3AST

  92. def mkBoolConst (symbol: Z3Symbol): Z3AST

  93. def mkBoolSort (): Z3Sort

  94. def mkBound (index: Int, sort: Z3Sort): Z3AST

  95. def mkConcat (ast1: Z3AST, ast2: Z3AST): Z3AST

  96. def mkConst (s: String, sort: Z3Sort): Z3AST

  97. def mkConst (symbol: Z3Symbol, sort: Z3Sort): Z3AST

  98. def mkConstArray (sort: Z3Sort, value: Z3AST): Z3AST

  99. def mkDistinct (args: Z3AST*): Z3AST

  100. def mkDiv (ast1: Z3AST, ast2: Z3AST): Z3AST

  101. def mkEmptySet (sort: Z3Sort): Z3AST

  102. def mkEq (ast1: Z3AST, ast2: Z3AST): Z3AST

  103. def mkExists (weight: Int, patterns: Seq[Z3Pattern], decls: Seq[(Z3Symbol, Z3Sort)], body: Z3AST): Z3AST

  104. def mkExtRotateLeft (ast1: Z3AST, ast2: Z3AST): Z3AST

  105. def mkExtRotateRight (ast1: Z3AST, ast2: Z3AST): Z3AST

  106. def mkExtract (high: Int, low: Int, ast: Z3AST): Z3AST

  107. def mkFalse (): Z3AST

  108. def mkForAll (weight: Int, patterns: Seq[Z3Pattern], decls: Seq[(Z3Symbol, Z3Sort)], body: Z3AST): Z3AST

  109. def mkFreshBoolConst (prefix: String): Z3AST

  110. def mkFreshConst (prefix: String, sort: Z3Sort): Z3AST

  111. def mkFreshFuncDecl (prefix: String, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort): Z3FuncDecl

  112. def mkFreshIntConst (prefix: String): Z3AST

  113. def mkFreshIntSymbol : Z3Symbol

  114. def mkFreshStringSymbol (s: String): Z3Symbol

  115. def mkFullSet (sort: Z3Sort): Z3AST

  116. def mkFuncDecl (symbol: String, domainSort: Z3Sort, rangeSort: Z3Sort): Z3FuncDecl

  117. def mkFuncDecl (symbol: String, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort): Z3FuncDecl

  118. def mkFuncDecl (symbol: Z3Symbol, domainSort: Z3Sort, rangeSort: Z3Sort): Z3FuncDecl

  119. def mkFuncDecl (symbol: Z3Symbol, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort): Z3FuncDecl

  120. def mkGE (ast1: Z3AST, ast2: Z3AST): Z3AST

  121. def mkGT (ast1: Z3AST, ast2: Z3AST): Z3AST

  122. def mkITE (t1: Z3AST, t2: Z3AST, t3: Z3AST): Z3AST

  123. def mkIff (t1: Z3AST, t2: Z3AST): Z3AST

  124. def mkImplies (t1: Z3AST, t2: Z3AST): Z3AST

  125. def mkInt (value: Int, sort: Z3Sort): Z3AST

  126. def mkInt2Real (ast: Z3AST): Z3AST

  127. def mkIntConst (s: String): Z3AST

  128. def mkIntConst (symbol: Z3Symbol): Z3AST

  129. def mkIntSort (): Z3Sort

  130. def mkIntSymbol (i: Int): Z3Symbol

  131. def mkIsInt (ast: Z3AST): Z3AST

  132. def mkLE (ast1: Z3AST, ast2: Z3AST): Z3AST

  133. def mkLT (ast1: Z3AST, ast2: Z3AST): Z3AST

  134. def mkLabel (symbol: Z3Symbol, polarity: Boolean, ast: Z3AST): Z3AST

  135. def mkMod (ast1: Z3AST, ast2: Z3AST): Z3AST

  136. def mkMul (args: Z3AST*): Z3AST

  137. def mkNot (ast: Z3AST): Z3AST

  138. def mkOr (args: Z3AST*): Z3AST

  139. def mkPattern (args: Z3AST*): Z3Pattern

  140. def mkQuantifier (isForAll: Boolean, weight: Int, patterns: Seq[Z3Pattern], decls: Seq[(Z3Symbol, Z3Sort)], body: Z3AST): Z3AST

  141. def mkReal2Int (ast: Z3AST): Z3AST

  142. def mkRealSort (): Z3Sort

  143. def mkRem (ast1: Z3AST, ast2: Z3AST): Z3AST

  144. def mkSelect (array: Z3AST, index: Z3AST): Z3AST

  145. def mkSetAdd (set: Z3AST, elem: Z3AST): Z3AST

  146. def mkSetComplement (ast: Z3AST): Z3AST

  147. def mkSetDel (set: Z3AST, elem: Z3AST): Z3AST

  148. def mkSetDifference (ast1: Z3AST, ast2: Z3AST): Z3AST

  149. def mkSetIntersect (args: Z3AST*): Z3AST

  150. def mkSetMember (elem: Z3AST, set: Z3AST): Z3AST

  151. def mkSetSort (underlying: Z3Sort): Z3Sort

  152. def mkSetSubset (ast1: Z3AST, ast2: Z3AST): Z3AST

  153. def mkSetUnion (args: Z3AST*): Z3AST

  154. def mkSignExt (extraSize: Int, ast: Z3AST): Z3AST

  155. def mkStore (array: Z3AST, index: Z3AST, value: Z3AST): Z3AST

  156. def mkStringSymbol (s: String): Z3Symbol

  157. def mkSub (args: Z3AST*): Z3AST

  158. def mkTrue (): Z3AST

  159. def mkTupleSort (name: String, sorts: Z3Sort*): (Z3Sort, Z3FuncDecl, Seq[Z3FuncDecl])

  160. def mkTupleSort (name: Z3Symbol, sorts: Z3Sort*): (Z3Sort, Z3FuncDecl, Seq[Z3FuncDecl])

  161. def mkUnaryMinus (ast: Z3AST): Z3AST

  162. def mkUninterpretedSort (s: String): Z3Sort

  163. def mkUninterpretedSort (s: Z3Symbol): Z3Sort

  164. def mkXor (t1: Z3AST, t2: Z3AST): Z3AST

  165. def mkZeroExt (extraSize: Int, ast: Z3AST): Z3AST

  166. def modelToString (model: Z3Model): String

  167. def ne (arg0: AnyRef): Boolean

    Attributes
    final
    Definition Classes
    AnyRef

  168. def notify (): Unit

    Attributes
    final
    Definition Classes
    AnyRef

  169. def notifyAll (): Unit

    Attributes
    final
    Definition Classes
    AnyRef

  170. def parseSMTLIB2File (fileName: String, sorts: Map[Z3Symbol, Z3Sort], decls: Map[Z3Symbol, Z3FuncDecl]): Z3AST

    Uses the SMT-LIB 2 parser to read in a benchmark file.

    Uses the SMT-LIB 2 parser to read in a benchmark file. The maps are used to override symbols that would otherwise be created by the parser.

  171. def parseSMTLIB2File (fileName: String): Z3AST

    Uses the SMT-LIB 2 parser to read in a benchmark file.

  172. def parseSMTLIB2String (str: String, sorts: Map[Z3Symbol, Z3Sort], decls: Map[Z3Symbol, Z3FuncDecl]): Z3AST

    Uses the SMT-LIB 2 parser to read in a benchmark string.

    Uses the SMT-LIB 2 parser to read in a benchmark string. The maps are used to override symbols that would otherwise be created by the parser.

  173. def parseSMTLIB2String (str: String): Z3AST

    Uses the SMT-LIB 2 parser to read in a benchmark string.

  174. def parseSMTLIBFile (fileName: String, sorts: Map[Z3Symbol, Z3Sort], decls: Map[Z3Symbol, Z3FuncDecl]): Unit

    Uses the SMT-LIB parser to read in a benchmark file.

    Uses the SMT-LIB parser to read in a benchmark file. The maps are used to override symbols that would otherwise be created by the parser.

    See also

    getSMTLIBFormulas, getSMTLIBAssumptions, getSMTLIBDecls, getSMTLIBSorts, getSMTLIBError

  175. def parseSMTLIBFile (fileName: String): Unit

    Uses the SMT-LIB parser to read in a benchmark file.

    Uses the SMT-LIB parser to read in a benchmark file.

    See also

    getSMTLIBFormulas, getSMTLIBAssumptions, getSMTLIBDecls, getSMTLIBSorts, getSMTLIBError

  176. def parseSMTLIBString (str: String, sorts: Map[Z3Symbol, Z3Sort], decls: Map[Z3Symbol, Z3FuncDecl]): Unit

    Uses the SMT-LIB parser to read in a benchmark string.

    Uses the SMT-LIB parser to read in a benchmark string. The maps are used to override symbols that would otherwise be created by the parser.

    See also

    getSMTLIBFormulas, getSMTLIBAssumptions, getSMTLIBDecls, getSMTLIBSorts, getSMTLIBError

  177. def parseSMTLIBString (str: String): Unit

    Uses the SMT-LIB parser to read in a benchmark string.

    Uses the SMT-LIB parser to read in a benchmark string.

    See also

    getSMTLIBFormulas, getSMTLIBAssumptions, getSMTLIBDecls, getSMTLIBSorts, getSMTLIBError

  178. def patternToString (pattern: Z3Pattern): String

  179. def pop (numScopes: Int = 1): Unit

  180. val ptr : Long

  181. def push (): Unit

  182. def softCheckCancel (): Unit

  183. def sortToString (sort: Z3Sort): String

  184. def synchronized [T0] (arg0: ⇒ T0): T0

    Attributes
    final
    Definition Classes
    AnyRef

  185. def toString (): String

    Definition Classes
    Z3Context → AnyRef → Any

  186. def traceOff (): Unit

  187. def traceToFile (traceFile: String): Boolean

  188. def traceToStderr (): Unit

  189. def traceToStdout (): Unit

  190. def updateParamValue (paramID: String, paramValue: String): Unit

  191. def wait (): Unit

    Attributes
    final
    Definition Classes
    AnyRef
    Annotations
    @throws()

  192. def wait (arg0: Long, arg1: Int): Unit

    Attributes
    final
    Definition Classes
    AnyRef
    Annotations
    @throws()

  193. def wait (arg0: Long): Unit

    Attributes
    final
    Definition Classes
    AnyRef
    Annotations
    @throws()

Inherited from AnyRef

Inherited from Any