Packages

sealed class Z3Context extends AnyRef

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Z3Context
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Z3Context(params: (String, Any)*)
  2. new Z3Context(config: Map[String, String])

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. val astQueue: Z3RefCountQueue[Z3ASTLike]
  6. def astToString(ast: Z3AST): String
  7. val astVectorQueue: Z3RefCountQueue[Z3ASTVector]
  8. def benchmarkToSMTLIBString(name: String, logic: String, status: String, attributes: String, assumptions: Seq[Z3AST], formula: Z3AST): String
  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  10. val config: Map[String, String]
  11. def delete(): Unit
  12. val entryQueue: Z3RefCountQueue[Z3FuncInterpEntry]
  13. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  15. def finalize(): Unit
    Definition Classes
    Z3Context → AnyRef
  16. def funcDeclToString(funcDecl: Z3FuncDecl): String
  17. def getASTKind(ast: Z3AST): Z3ASTKind
  18. def getAbsFuncDecl(): Z3FuncDecl
  19. def getAppDecl(ast: Z3AST, arity: Int = -1): Z3FuncDecl
  20. def getBoolValue(ast: Z3AST): Option[Boolean]
  21. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  22. def getDeclFuncDeclParameter(fd: Z3FuncDecl, idx: Int, arity: Int = 1): Z3FuncDecl
  23. def getDeclKind(funcDecl: Z3FuncDecl): Z3DeclKind
  24. def getDeclName(fd: Z3FuncDecl): Z3Symbol
  25. def getDomain(funcDecl: Z3FuncDecl, i: Int): Z3Sort
  26. def getDomainSize(funcDecl: Z3FuncDecl): Int
  27. def getFuncDecl(op: Z3DeclKind, sorts: Z3Sort*): Z3FuncDecl
  28. def getIndexValue(ast: Z3AST): Int
  29. def getNumeralInt(ast: Z3AST): Z3NumeralIntAST
  30. def getNumeralReal(ast: Z3AST): Z3NumeralRealAST
  31. def getQuantifierBody(ast: Z3AST): Z3AST
  32. def getQuantifierBoundName(ast: Z3AST, i: Int): Z3Symbol
  33. def getQuantifierNumBound(ast: Z3AST): Int
  34. def getRange(funcDecl: Z3FuncDecl): Z3Sort
  35. def getSort(ast: Z3AST): Z3Sort
  36. def getString(ast: Z3AST): String
  37. def getSymbolKind(symbol: Z3Symbol): Z3SymbolKind[_]
  38. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  39. val interpQueue: Z3RefCountQueue[Z3FuncInterp]
  40. def interrupt(): Unit
  41. def isEqAST(t1: Z3AST, t2: Z3AST): Boolean
  42. def isEqFuncDecl(fd1: Z3FuncDecl, fd2: Z3FuncDecl): Boolean
  43. def isEqSort(s1: Z3Sort, s2: Z3Sort): Boolean
  44. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  45. def isQuantifierForall(ast: Z3AST): Boolean
  46. def mkADTSorts(defs: Seq[(String, Seq[String], Seq[Seq[(String, ADTSortReference)]])]): Seq[(Z3Sort, Seq[Z3FuncDecl], Seq[Z3FuncDecl], Seq[Seq[Z3FuncDecl]])]
  47. def mkAdd(args: Z3AST*): Z3AST
  48. def mkAnd(args: Z3AST*): Z3AST
  49. def mkApp(funcDecl: Z3FuncDecl, args: Z3AST*): Z3AST
  50. def mkArrayDefault(array: Z3AST): Z3AST
  51. def mkArrayMap(op: Z3DeclKind, args: Z3AST*): Z3AST
  52. def mkArrayMap(f: Z3FuncDecl, args: Z3AST*): Z3AST
  53. def mkArraySort(domain: Z3Sort, range: Z3Sort): Z3Sort
  54. def mkBV2Int(ast: Z3AST, isSigned: Boolean): Z3AST
  55. def mkBVAdd(ast1: Z3AST, ast2: Z3AST): Z3AST
  56. def mkBVAddNoOverflow(ast1: Z3AST, ast2: Z3AST, isSigned: Boolean): Z3AST
  57. def mkBVAddNoUnderflow(ast1: Z3AST, ast2: Z3AST): Z3AST
  58. def mkBVAnd(ast1: Z3AST, ast2: Z3AST): Z3AST
  59. def mkBVAshr(ast1: Z3AST, ast2: Z3AST): Z3AST
  60. def mkBVLshr(ast1: Z3AST, ast2: Z3AST): Z3AST
  61. def mkBVMul(ast1: Z3AST, ast2: Z3AST): Z3AST
  62. def mkBVMulNoOverflow(ast1: Z3AST, ast2: Z3AST, isSigned: Boolean): Z3AST
  63. def mkBVMulNoUnderflow(ast1: Z3AST, ast2: Z3AST): Z3AST
  64. def mkBVNand(ast1: Z3AST, ast2: Z3AST): Z3AST
  65. def mkBVNeg(ast: Z3AST): Z3AST
  66. def mkBVNegNoOverflow(ast: Z3AST): Z3AST
  67. def mkBVNor(ast1: Z3AST, ast2: Z3AST): Z3AST
  68. def mkBVNot(ast: Z3AST): Z3AST
  69. def mkBVOr(ast1: Z3AST, ast2: Z3AST): Z3AST
  70. def mkBVRedAnd(ast: Z3AST): Z3AST
  71. def mkBVRedOr(ast: Z3AST): Z3AST
  72. def mkBVSDivNoOverflow(ast1: Z3AST, ast2: 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 mkBVSubNoOverflow(ast1: Z3AST, ast2: Z3AST): Z3AST
  84. def mkBVSubNoUnderflow(ast1: Z3AST, ast2: Z3AST, isSigned: Boolean): Z3AST
  85. def mkBVUdiv(ast1: Z3AST, ast2: Z3AST): Z3AST
  86. def mkBVUge(ast1: Z3AST, ast2: Z3AST): Z3AST
  87. def mkBVUgt(ast1: Z3AST, ast2: Z3AST): Z3AST
  88. def mkBVUle(ast1: Z3AST, ast2: Z3AST): Z3AST
  89. def mkBVUlt(ast1: Z3AST, ast2: Z3AST): Z3AST
  90. def mkBVUrem(ast1: Z3AST, ast2: Z3AST): Z3AST
  91. def mkBVXnor(ast1: Z3AST, ast2: Z3AST): Z3AST
  92. def mkBVXor(ast1: Z3AST, ast2: Z3AST): Z3AST
  93. def mkBoolConst(s: String): Z3AST
  94. def mkBoolConst(symbol: Z3Symbol): Z3AST
  95. def mkBoolSort(): Z3Sort
  96. def mkBound(index: Int, sort: Z3Sort): Z3AST
  97. def mkConcat(ast1: Z3AST, ast2: Z3AST): Z3AST
  98. def mkConst(s: String, sort: Z3Sort): Z3AST
  99. def mkConst(symbol: Z3Symbol, sort: Z3Sort): Z3AST
  100. def mkConstArray(sort: Z3Sort, value: Z3AST): Z3AST
  101. def mkDistinct(args: Z3AST*): Z3AST
  102. def mkDiv(ast1: Z3AST, ast2: Z3AST): Z3AST
  103. def mkEmptySeq(sort: Z3Sort): Z3AST
  104. def mkEmptySet(sort: Z3Sort): Z3AST
  105. def mkEq(ast1: Z3AST, ast2: Z3AST): Z3AST
  106. def mkExists(weight: Int, patterns: Seq[Z3Pattern], decls: Seq[(Z3Symbol, Z3Sort)], body: Z3AST): Z3AST
  107. def mkExistsConst(weight: Int, patterns: Seq[Z3Pattern], bounds: Seq[Z3AST], body: Z3AST): Z3AST
  108. def mkExtRotateLeft(ast1: Z3AST, ast2: Z3AST): Z3AST
  109. def mkExtRotateRight(ast1: Z3AST, ast2: Z3AST): Z3AST
  110. def mkExtract(high: Int, low: Int, ast: Z3AST): Z3AST
  111. def mkFalse(): Z3AST
  112. def mkForAllConst(weight: Int, patterns: Seq[Z3Pattern], bounds: Seq[Z3AST], body: Z3AST): Z3AST
  113. def mkForall(weight: Int, patterns: Seq[Z3Pattern], decls: Seq[(Z3Symbol, Z3Sort)], body: Z3AST): Z3AST
  114. def mkFreshBoolConst(prefix: String): Z3AST
  115. def mkFreshConst(prefix: String, sort: Z3Sort): Z3AST
  116. def mkFreshFuncDecl(prefix: String, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort): Z3FuncDecl
  117. def mkFreshIntConst(prefix: String): Z3AST
  118. def mkFreshIntSymbol: Z3Symbol
  119. def mkFreshStringSymbol(s: String): Z3Symbol
  120. def mkFullSet(sort: Z3Sort): Z3AST
  121. def mkFuncDecl(symbol: String, domainSort: Z3Sort, rangeSort: Z3Sort): Z3FuncDecl
  122. def mkFuncDecl(symbol: String, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort): Z3FuncDecl
  123. def mkFuncDecl(symbol: Z3Symbol, domainSort: Z3Sort, rangeSort: Z3Sort): Z3FuncDecl
  124. def mkFuncDecl(symbol: Z3Symbol, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort): Z3FuncDecl
  125. def mkGE(ast1: Z3AST, ast2: Z3AST): Z3AST
  126. def mkGT(ast1: Z3AST, ast2: Z3AST): Z3AST
  127. def mkITE(t1: Z3AST, t2: Z3AST, t3: Z3AST): Z3AST
  128. def mkIff(t1: Z3AST, t2: Z3AST): Z3AST
  129. def mkImplies(t1: Z3AST, t2: Z3AST): Z3AST
  130. def mkInt(value: Int, sort: Z3Sort): Z3AST
  131. def mkInt2BV(size: Int, ast: Z3AST): Z3AST
  132. def mkInt2Real(ast: Z3AST): Z3AST
  133. def mkIntConst(s: String): Z3AST
  134. def mkIntConst(symbol: Z3Symbol): Z3AST
  135. def mkIntSort(): Z3Sort
  136. def mkIntSymbol(i: Int): Z3Symbol
  137. def mkIsInt(ast: Z3AST): Z3AST
  138. def mkLE(ast1: Z3AST, ast2: Z3AST): Z3AST
  139. def mkLT(ast1: Z3AST, ast2: Z3AST): Z3AST
  140. def mkMod(ast1: Z3AST, ast2: Z3AST): Z3AST
  141. def mkMul(args: Z3AST*): Z3AST
  142. def mkNot(ast: Z3AST): Z3AST
  143. def mkNumeral(value: String, sort: Z3Sort): Z3AST
  144. def mkOptimizer(): Z3Optimizer
  145. def mkOr(args: Z3AST*): Z3AST
  146. def mkPattern(args: Z3AST*): Z3Pattern
  147. def mkPower(ast1: Z3AST, ast2: Z3AST): Z3AST
  148. def mkQuantifier(isForAll: Boolean, weight: Int, patterns: Seq[Z3Pattern], decls: Seq[(Z3Symbol, Z3Sort)], body: Z3AST): Z3AST
  149. def mkQuantifierConst(isForAll: Boolean, weight: Int, patterns: Seq[Z3Pattern], bounds: Seq[Z3AST], body: Z3AST): Z3AST
  150. def mkReConcat(args: Z3AST*): Z3AST
  151. def mkReOption(re: Z3AST): Z3AST
  152. def mkRePlus(re: Z3AST): Z3AST
  153. def mkReStar(re: Z3AST): Z3AST
  154. def mkReUnion(args: Z3AST*): Z3AST
  155. def mkReal(numerator: Int, denominator: Int): Z3AST
  156. def mkReal2Int(ast: Z3AST): Z3AST
  157. def mkRealSort(): Z3Sort
  158. def mkRem(ast1: Z3AST, ast2: Z3AST): Z3AST
  159. def mkRepeat(count: Int, ast: Z3AST): Z3AST
  160. def mkSelect(array: Z3AST, index: Z3AST): Z3AST
  161. def mkSeqAt(seq: Z3AST, i: Z3AST): Z3AST
  162. def mkSeqConcat(args: Z3AST*): Z3AST
  163. def mkSeqContains(seq1: Z3AST, seq2: Z3AST): Z3AST
  164. def mkSeqExtract(seq: Z3AST, start: Z3AST, length: Z3AST): Z3AST
  165. def mkSeqInRe(seq: Z3AST, re: Z3AST): Z3AST
  166. def mkSeqIndexOf(seq: Z3AST, sub: Z3AST, offset: Z3AST): Z3AST
  167. def mkSeqLength(e: Z3AST): Z3AST
  168. def mkSeqPrefix(seq1: Z3AST, seq2: Z3AST): Z3AST
  169. def mkSeqReplace(seq: Z3AST, src: Z3AST, dest: Z3AST): Z3AST
  170. def mkSeqSort(underlying: Z3Sort): Z3Sort
  171. def mkSeqSuffix(seq1: Z3AST, seq2: Z3AST): Z3AST
  172. def mkSeqToRe(seq: Z3AST): Z3AST
  173. def mkSetAdd(set: Z3AST, elem: Z3AST): Z3AST
  174. def mkSetComplement(ast: Z3AST): Z3AST
  175. def mkSetDel(set: Z3AST, elem: Z3AST): Z3AST
  176. def mkSetDifference(ast1: Z3AST, ast2: Z3AST): Z3AST
  177. def mkSetIntersect(args: Z3AST*): Z3AST
  178. def mkSetMember(elem: Z3AST, set: Z3AST): Z3AST
  179. def mkSetSort(underlying: Z3Sort): Z3Sort
  180. def mkSetSubset(ast1: Z3AST, ast2: Z3AST): Z3AST
  181. def mkSetUnion(args: Z3AST*): Z3AST
  182. def mkSignExt(extraSize: Int, ast: Z3AST): Z3AST
  183. def mkSimpleSolver(): Z3Solver
  184. def mkSolver(tactic: Z3Tactic): Z3Solver
  185. def mkSolver(): Z3Solver
  186. def mkStore(array: Z3AST, index: Z3AST, value: Z3AST): Z3AST
  187. def mkString(s: String): Z3AST
  188. def mkStringSort(): Z3AST
  189. def mkStringSymbol(s: String): Z3Symbol
  190. def mkSub(args: Z3AST*): Z3AST
  191. def mkSymbol(s: String): Z3Symbol
  192. def mkSymbol(i: Int): Z3Symbol
  193. def mkTactic(name: String): Z3Tactic
  194. def mkTacticAndThen(tactic1: Z3Tactic, tactic2: Z3Tactic): Z3Tactic
  195. def mkTrue(): Z3AST
  196. def mkTupleSort(name: String, sorts: Z3Sort*): (Z3Sort, Z3FuncDecl, Seq[Z3FuncDecl])
  197. def mkTupleSort(name: Z3Symbol, sorts: Z3Sort*): (Z3Sort, Z3FuncDecl, Seq[Z3FuncDecl])
  198. def mkUnaryMinus(ast: Z3AST): Z3AST
  199. def mkUninterpretedSort(s: String): Z3Sort
  200. def mkUninterpretedSort(s: Z3Symbol): Z3Sort
  201. def mkUnitSeq(e: Z3AST): Z3AST
  202. def mkXor(t1: Z3AST, t2: Z3AST): Z3AST
  203. def mkZeroExt(extraSize: Int, ast: Z3AST): Z3AST
  204. val modelQueue: Z3RefCountQueue[Z3Model]
  205. def modelToString(model: Z3Model): String
  206. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  207. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  208. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  209. def onError(code: Long): Nothing
  210. val optimizerQueue: Z3RefCountQueue[Z3Optimizer]
  211. val paramsQueue: Z3RefCountQueue[Z3Params]
  212. 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.

  213. def parseSMTLIB2File(fileName: String): Z3AST

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

  214. 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.

  215. def parseSMTLIB2String(str: String): Z3AST

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

  216. def patternToString(pattern: Z3Pattern): String
  217. val ptr: Long
  218. def setAstPrintMode(printMode: AstPrintMode): Unit
  219. def simplifyAst(ast: Z3AST): Z3AST
  220. val solverQueue: Z3RefCountQueue[Z3Solver]
  221. def sortToString(sort: Z3Sort): String
  222. def substitute(ast: Z3AST, from: Array[Z3AST], to: Array[Z3AST]): Z3AST
  223. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  224. val tacticQueue: Z3RefCountQueue[Z3Tactic]
  225. def toString(): String
    Definition Classes
    AnyRef → Any
  226. def updateParamValue(paramID: String, paramValue: String): Unit
  227. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  228. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  229. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Deprecated Value Members

  1. def softCheckCancel(): Unit
    Annotations
    @deprecated
    Deprecated

    (Since version ) Use interrupt instead

Inherited from AnyRef

Inherited from Any

Ungrouped