z3

Z3Wrapper

object Z3Wrapper extends

Visibility
  1. Public
  2. All

Type Members

  1. class IntPtr extends AnyRef

Value Members

  1. def assertCnstr (contextPtr: Long, astPtr: Long): Unit

    Annotations
    @native()

  2. def astToString (contextPtr: Long, astPtr: Long): String

    Annotations
    @native()

  3. def benchmarkToSMTLIBString (contextPtr: Long, name: String, logic: String, status: String, attributes: String, numAssumptions: Int, assumptions: Array[Long], formulaPtr: Long): String

    Annotations
    @native()

  4. def blockLiterals (contextPtr: Long, lbls: Long): Unit

    Annotations
    @native()

  5. def check (contextPtr: Long): Int

    Annotations
    @native()

  6. def checkAndGetModel (contextPtr: Long, model: Pointer): Int

    Annotations
    @native()

  7. def checkAssumptions (contextPtr: Long, numAssumptions: Int, assumptions: Array[Long], model: Pointer, coreSizeIn: Int, coreSizeOut: IntPtr, core: Array[Long]): Int

    Annotations
    @native()

  8. def contextToString (contextPtr: Long): String

    Annotations
    @native()

  9. def delConfig (configPtr: Long): Unit

    Annotations
    @native()

  10. def delConstructorList (contextPtr: Long, constructorListPtr: Long): Unit

    Annotations
    @native()

  11. def delContext (contextPtr: Long): Unit

    Annotations
    @native()

  12. def delLiterals (contextPtr: Long, lbls: Long): Unit

    Annotations
    @native()

  13. def delModel (contextPtr: Long, modelPtr: Long): Unit

    Annotations
    @native()

  14. def disableLiteral (contextPtr: Long, lbls: Long, idx: Int): Unit

    Annotations
    @native()

  15. def eval (contextPtr: Long, modelPtr: Long, astPtr: Long, ast: Pointer): Boolean

    Annotations
    @native()

  16. def funcDeclToString (contextPtr: Long, funcDeclPtr: Long): String

    Annotations
    @native()

  17. def getASTKind (contextPtr: Long, astPtr: Long): Int

    Annotations
    @native()

  18. def getAppArg (contextPtr: Long, astPtr: Long, i: Int): Long

    Annotations
    @native()

  19. def getAppDecl (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  20. def getAppNumArgs (contextPtr: Long, astPtr: Long): Int

    Annotations
    @native()

  21. def getArrayValue (contextPtr: Long, modelPtr: Long, astPtr: Long, numEntries: Int, indices: Array[Long], values: Array[Long], elseValue: Pointer): Unit

    Annotations
    @native()

  22. def getBVSortSize (contextPtr: Long, sortPtr: Long): Int

    Annotations
    @native()

  23. def getBoolValue (contextPtr: Long, astPtr: Long): Int

    Annotations
    @native()

  24. def getDeclFuncDeclParameter (contextPtr: Long, funcDeclPtr: Long, idx: Int): Long

    Annotations
    @native()

  25. def getDeclKind (contextPtr: Long, funcDeclPtr: Long): Int

    Annotations
    @native()

  26. def getDeclName (contextPtr: Long, funcDeclPtr: Long): Long

    Annotations
    @native()

  27. def getDomain (contextPtr: Long, funcDeclPtr: Long, i: Int): Long

    Annotations
    @native()

  28. def getDomainSize (contextPtr: Long, funcDeclPtr: Long): Int

    Annotations
    @native()

  29. def getGuessedLiterals (contextPtr: Long): Long

    Annotations
    @native()

  30. def getLabelSymbol (contextPtr: Long, lbls: Long, idx: Int): Long

    Annotations
    @native()

  31. def getLiteral (contextPtr: Long, lbls: Long, idx: Int): Long

    Annotations
    @native()

  32. def getModelConstant (contextPtr: Long, modelPtr: Long, i: Int): Long

    Annotations
    @native()

  33. def getModelFuncDecl (contextPtr: Long, modelPtr: Long, i: Int): Long

    Annotations
    @native()

  34. def getModelFuncElse (contextPtr: Long, modelPtr: Long, i: Int): Long

    Annotations
    @native()

  35. def getModelFuncEntryArg (contextPtr: Long, modelPtr: Long, i: Int, j: Int, k: Int): Long

    Annotations
    @native()

  36. def getModelFuncEntryNumArgs (contextPtr: Long, modelPtr: Long, i: Int, j: Int): Int

    Annotations
    @native()

  37. def getModelFuncEntryValue (contextPtr: Long, modelPtr: Long, i: Int, j: Int): Long

    Annotations
    @native()

  38. def getModelFuncNumEntries (contextPtr: Long, modelPtr: Long, i: Int): Int

    Annotations
    @native()

  39. def getModelNumConstants (contextPtr: Long, modelPtr: Long): Int

    Annotations
    @native()

  40. def getModelNumFuncs (contextPtr: Long, modelPtr: Long): Int

    Annotations
    @native()

  41. def getNumLiterals (contextPtr: Long, lbls: Long): Int

    Annotations
    @native()

  42. def getNumScopes (contextPtr: Long): Int

    Annotations
    @native()

  43. def getNumeralInt (contextPtr: Long, astPtr: Long, i: IntPtr): Boolean

    Annotations
    @native()

  44. def getRange (contextPtr: Long, funcDeclPtr: Long): Long

    Annotations
    @native()

  45. def getRelevantLabels (contextPtr: Long): Long

    Annotations
    @native()

  46. def getRelevantLiterals (contextPtr: Long): Long

    Annotations
    @native()

  47. def getSMTLIBAssumption (contextPtr: Long, i: Int): Long

    Annotations
    @native()

  48. def getSMTLIBDecl (contextPtr: Long, i: Int): Long

    Annotations
    @native()

  49. def getSMTLIBError (contextPtr: Long): String

    Annotations
    @native()

  50. def getSMTLIBFormula (contextPtr: Long, i: Int): Long

    Annotations
    @native()

  51. def getSMTLIBNumAssumptions (contextPtr: Long): Int

    Annotations
    @native()

  52. def getSMTLIBNumDecls (contextPtr: Long): Int

    Annotations
    @native()

  53. def getSMTLIBNumFormulas (contextPtr: Long): Int

    Annotations
    @native()

  54. def getSMTLIBNumSorts (contextPtr: Long): Int

    Annotations
    @native()

  55. def getSMTLIBSort (contextPtr: Long, i: Int): Long

    Annotations
    @native()

  56. def getSearchFailure (contextPtr: Long): Int

    Annotations
    @native()

  57. def getSort (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  58. def getSymbolInt (contextPtr: Long, symbolPtr: Long): Int

    Annotations
    @native()

  59. def getSymbolKind (contextPtr: Long, symbolPtr: Long): Int

    Annotations
    @native()

  60. def getSymbolString (contextPtr: Long, symbolPtr: Long): String

    Annotations
    @native()

  61. def getVersion (major: IntPtr, minor: IntPtr, buildNumber: IntPtr, revisionNumber: IntPtr): Unit

    Annotations
    @native()

  62. def init (): Unit

  63. def isArrayValue (contextPtr: Long, modelPtr: Long, astPtr: Long, numEntries: IntPtr): Boolean

    Annotations
    @native()

  64. def isEqAST (contextPtr: Long, astPtr1: Long, astPtr2: Long): Boolean

    Annotations
    @native()

  65. def isEqFuncDecl (contextPtr: Long, fdPtr1: Long, fdPtr2: Long): Boolean

    Annotations
    @native()

  66. def isEqSort (contextPtr: Long, sortPtr1: Long, sortPtr2: Long): Boolean

    Annotations
    @native()

  67. def mkAdd (contextPtr: Long, numArgs: Int, args: Array[Long]): Long

    Annotations
    @native()

  68. def mkAnd (contextPtr: Long, numArgs: Int, args: Array[Long]): Long

    Annotations
    @native()

  69. def mkApp (contextPtr: Long, funcDeclPtr: Long, numArgs: Int, args: Array[Long]): Long

    Annotations
    @native()

  70. def mkArrayDefault (contextPtr: Long, astPtrArr: Long): Long

    Annotations
    @native()

  71. def mkArraySort (contextPtr: Long, domainSortPtr: Long, rangeSortPtr: Long): Long

    Annotations
    @native()

  72. def mkBV2Int (contextPtr: Long, astPtr: Long, isSigned: Boolean): Long

    Annotations
    @native()

  73. def mkBVAdd (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  74. def mkBVAddNoOverflow (contextPtr: Long, astPtr1: Long, astPtr2: Long, isSigned: Boolean): Long

    Annotations
    @native()

  75. def mkBVAddNoUnderflow (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  76. def mkBVAnd (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  77. def mkBVAshr (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  78. def mkBVLshr (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  79. def mkBVMul (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  80. def mkBVMulNoOverflow (contextPtr: Long, astPtr1: Long, astPtr2: Long, isSigned: Boolean): Long

    Annotations
    @native()

  81. def mkBVMulNoUnderflow (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  82. def mkBVNand (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  83. def mkBVNeg (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  84. def mkBVNegNoOverflow (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  85. def mkBVNor (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  86. def mkBVNot (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  87. def mkBVOr (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  88. def mkBVRedAnd (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  89. def mkBVRedOr (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  90. def mkBVSdiv (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  91. def mkBVSdivNoOverflow (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  92. def mkBVSge (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  93. def mkBVSgt (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  94. def mkBVShl (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  95. def mkBVSle (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  96. def mkBVSlt (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  97. def mkBVSmod (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  98. def mkBVSort (contextPtr: Long, size: Int): Long

    Annotations
    @native()

  99. def mkBVSrem (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  100. def mkBVSub (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  101. def mkBVSubNoOverflow (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  102. def mkBVSubNoUnderflow (contextPtr: Long, astPtr1: Long, astPtr2: Long, isSigned: Boolean): Long

    Annotations
    @native()

  103. def mkBVUdiv (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  104. def mkBVUge (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  105. def mkBVUgt (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  106. def mkBVUle (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  107. def mkBVUlt (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  108. def mkBVUrem (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  109. def mkBVXnor (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  110. def mkBVXor (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  111. def mkBoolSort (contextPtr: Long): Long

    Annotations
    @native()

  112. def mkBound (contextPtr: Long, index: Int, sortPtr: Long): Long

    Annotations
    @native()

  113. def mkConcat (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  114. def mkConfig (): Long

    Annotations
    @native()

  115. def mkConst (contextPtr: Long, symbolPtr: Long, sortPtr: Long): Long

    Annotations
    @native()

  116. def mkConstArray (contextPtr: Long, sortPtr: Long, astPtrVal: Long): Long

    Annotations
    @native()

  117. def mkConstructor (contextPtr: Long, symbolPtr1: Long, symbolPtr2: Long, numFields: Int, fieldNames: Array[Long], sorts: Array[Long], sortRefs: Array[Int]): Long

    Annotations
    @native()

  118. def mkConstructorList (contextPtr: Long, numConstructors: Int, constructors: Array[Long]): Long

    Annotations
    @native()

  119. def mkContext (configPtr: Long): Long

    Annotations
    @native()

  120. def mkDatatypes (contextPtr: Long, numSorts: Int, sortNames: Array[Long], constructorLists: Array[Long]): Array[Long]

    Annotations
    @native()

  121. def mkDistinct (contextPtr: Long, numArgs: Int, args: Array[Long]): Long

    Annotations
    @native()

  122. def mkDiv (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  123. def mkEmptySet (contextPtr: Long, sortPtr: Long): Long

    Annotations
    @native()

  124. def mkEq (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  125. def mkExtRotateLeft (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  126. def mkExtRotateRight (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  127. def mkExtract (contextPtr: Long, high: Int, low: Int, astPtr: Long): Long

    Annotations
    @native()

  128. def mkFalse (contextPtr: Long): Long

    Annotations
    @native()

  129. def mkFreshConst (contextPtr: Long, prefix: String, sortPtr: Long): Long

    Annotations
    @native()

  130. def mkFreshFuncDecl (contextPtr: Long, prefix: String, domainSize: Int, domainSortPtrs: Array[Long], rangeSortPtr: Long): Long

    Annotations
    @native()

  131. def mkFullSet (contextPtr: Long, sortPtr: Long): Long

    Annotations
    @native()

  132. def mkFuncDecl (contextPtr: Long, symbolPtr: Long, domainSize: Int, domainSortPtrs: Array[Long], rangeSortPtr: Long): Long

    Annotations
    @native()

  133. def mkGE (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  134. def mkGT (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  135. def mkITE (contextPtr: Long, astPtr1: Long, astPtr2: Long, astPtr3: Long): Long

    Annotations
    @native()

  136. def mkIff (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  137. def mkImplies (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  138. def mkInt (contextPtr: Long, v: Int, sortPtr: Long): Long

    Annotations
    @native()

  139. def mkInt2BV (contextPtr: Long, size: Int, astPtr: Long): Long

    Annotations
    @native()

  140. def mkInt2Real (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  141. def mkIntSort (contextPtr: Long): Long

    Annotations
    @native()

  142. def mkIntSymbol (contextPtr: Long, i: Int): Long

    Annotations
    @native()

  143. def mkIsInt (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  144. def mkLE (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  145. def mkLT (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  146. def mkLabel (contextPtr: Long, symbolPtr: Long, polarity: Boolean, astPtr: Long): Long

    Annotations
    @native()

  147. def mkMod (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  148. def mkMul (contextPtr: Long, numArgs: Int, args: Array[Long]): Long

    Annotations
    @native()

  149. def mkNot (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  150. def mkOr (contextPtr: Long, numArgs: Int, args: Array[Long]): Long

    Annotations
    @native()

  151. def mkPattern (contextPtr: Long, numPatterns: Int, terms: Array[Long]): Long

    Annotations
    @native()

  152. def mkQuantifier (contextPtr: Long, isForAll: Boolean, weight: Int, numPatterns: Int, patterns: Array[Long], numDecls: Int, declSorts: Array[Long], declNames: Array[Long], body: Long): Long

    Annotations
    @native()

  153. def mkReal2Int (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  154. def mkRealSort (contextPtr: Long): Long

    Annotations
    @native()

  155. def mkRem (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  156. def mkRepeat (contextPtr: Long, i: Int, astPtr: Long): Long

    Annotations
    @native()

  157. def mkRotateLeft (contextPtr: Long, i: Int, astPtr: Long): Long

    Annotations
    @native()

  158. def mkRotateRight (contextPtr: Long, i: Int, astPtr: Long): Long

    Annotations
    @native()

  159. def mkSelect (contextPtr: Long, astPtrArr: Long, astPtrInd: Long): Long

    Annotations
    @native()

  160. def mkSetAdd (contextPtr: Long, setPtr: Long, elemPtr: Long): Long

    Annotations
    @native()

  161. def mkSetComplement (contextPtr: Long, setPtr: Long): Long

    Annotations
    @native()

  162. def mkSetDel (contextPtr: Long, setPtr: Long, elemPtr: Long): Long

    Annotations
    @native()

  163. def mkSetDifference (contextPtr: Long, setPtr1: Long, setPtr2: Long): Long

    Annotations
    @native()

  164. def mkSetIntersect (contextPtr: Long, argCount: Int, args: Array[Long]): Long

    Annotations
    @native()

  165. def mkSetMember (contextPtr: Long, elemPtr: Long, setPtr: Long): Long

    Annotations
    @native()

  166. def mkSetSort (contextPtr: Long, sortPtr: Long): Long

    Annotations
    @native()

  167. def mkSetSubset (contextPtr: Long, setPtr1: Long, setPtr2: Long): Long

    Annotations
    @native()

  168. def mkSetUnion (contextPtr: Long, argCount: Int, args: Array[Long]): Long

    Annotations
    @native()

  169. def mkSignExt (contextPtr: Long, i: Int, astPtr: Long): Long

    Annotations
    @native()

  170. def mkStore (contextPtr: Long, astPtrArr: Long, astPtrInd: Long, astPtrVal: Long): Long

    Annotations
    @native()

  171. def mkStringSymbol (contextPtr: Long, s: String): Long

    Annotations
    @native()

  172. def mkSub (contextPtr: Long, numArgs: Int, args: Array[Long]): Long

    Annotations
    @native()

  173. def mkTheory (ctxPtr: Long, name: String): Long

    Annotations
    @native()

  174. def mkTrue (contextPtr: Long): Long

    Annotations
    @native()

  175. def mkTupleSort (contextPtr: Long, symPtr: Long, numFields: Int, fieldNames: Array[Long], fieldSorts: Array[Long], constructor: Pointer, projFuns: Array[Long]): Long

    Annotations
    @native()

  176. def mkUnaryMinus (contextPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  177. def mkUninterpretedSort (contextPtr: Long, symbolPtr: Long): Long

    Annotations
    @native()

  178. def mkXor (contextPtr: Long, astPtr1: Long, astPtr2: Long): Long

    Annotations
    @native()

  179. def mkZeroExt (contextPtr: Long, i: Int, astPtr: Long): Long

    Annotations
    @native()

  180. def modelToString (contextPtr: Long, modelPtr: Long): String

    Annotations
    @native()

  181. def parseSMTLIB2File (ctxPtr: Long, fileName: String, numSorts: Int, sortNames: Array[Long], sorts: Array[Long], numDecls: Int, declNames: Array[Long], decls: Array[Long]): Long

    Annotations
    @native()

  182. def parseSMTLIB2String (ctxPtr: Long, str: String, numSorts: Int, sortNames: Array[Long], sorts: Array[Long], numDecls: Int, declNames: Array[Long], decls: Array[Long]): Long

    Annotations
    @native()

  183. def parseSMTLIBFile (ctxPtr: Long, fileName: String, numSorts: Int, sortNames: Array[Long], sorts: Array[Long], numDecls: Int, declNames: Array[Long], decls: Array[Long]): Unit

    Annotations
    @native()

  184. def parseSMTLIBString (ctxPtr: Long, str: String, numSorts: Int, sortNames: Array[Long], sorts: Array[Long], numDecls: Int, declNames: Array[Long], decls: Array[Long]): Unit

    Annotations
    @native()

  185. def patternToString (contextPtr: Long, patternPtr: Long): String

    Annotations
    @native()

  186. def pop (contextPtr: Long, numScopes: Int): Unit

    Annotations
    @native()

  187. def printAST (contextPtr: Long, astPtr: Long): Unit

    Annotations
    @native()

  188. def printContext (contextPtr: Long): Unit

    Annotations
    @native()

  189. def printModel (contextPtr: Long, modelPtr: Long): Unit

    Annotations
    @native()

  190. def push (contextPtr: Long): Unit

    Annotations
    @native()

  191. def queryConstructor (contextPtr: Long, constructorPtr: Long, numFields: Int, constructor: Pointer, tester: Pointer, selectors: Array[Long]): Unit

    Annotations
    @native()

  192. def resetMemory (): Unit

    Annotations
    @native()

  193. def setParamValue (configPtr: Long, paramID: String, paramValue: String): Unit

    Annotations
    @native()

  194. def setTheoryCallbacks (thyPtr: Long, atp: AbstractTheoryProxy, setDelete: Boolean, setReduceEq: Boolean, setReduceApp: Boolean, setReduceDistinct: Boolean, setNewApp: Boolean, setNewElem: Boolean, setInitSearch: Boolean, setPush: Boolean, setPop: Boolean, setRestart: Boolean, setReset: Boolean, setFinalCheck: Boolean, setNewEq: Boolean, setNewDiseq: Boolean, setNewAssignment: Boolean, setNewRelevant: Boolean): Unit

    Annotations
    @native()

  195. def softCheckCancel (contextPtr: Long): Unit

    Annotations
    @native()

  196. def sortToString (contextPtr: Long, sortPtr: Long): String

    Annotations
    @native()

  197. def theoryAssertAxiom (thyPtr: Long, astPtr: Long): Unit

    Annotations
    @native()

  198. def theoryAssumeEq (thyPtr: Long, t1Ptr: Long, t2Ptr: Long): Unit

    Annotations
    @native()

  199. def theoryEnableAxiomSimplification (thyPtr: Long, flag: Boolean): Unit

    Annotations
    @native()

  200. def theoryGetApp (thyPtr: Long, i: Int): Long

    Annotations
    @native()

  201. def theoryGetElem (thyPtr: Long, i: Int): Long

    Annotations
    @native()

  202. def theoryGetEqCNext (thyPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  203. def theoryGetEqCRoot (thyPtr: Long, astPtr: Long): Long

    Annotations
    @native()

  204. def theoryGetNumApps (thyPtr: Long): Int

    Annotations
    @native()

  205. def theoryGetNumElems (thyPtr: Long): Int

    Annotations
    @native()

  206. def theoryGetNumParents (thyPtr: Long, astPtr: Long): Int

    Annotations
    @native()

  207. def theoryGetParent (thyPtr: Long, astPtr: Long, i: Int): Long

    Annotations
    @native()

  208. def theoryIsDecl (thyPtr: Long, declPtr: Long): Boolean

    Annotations
    @native()

  209. def theoryIsValue (thyPtr: Long, astPtr: Long): Boolean

    Annotations
    @native()

  210. def theoryMkConstant (ctxPtr: Long, thyPtr: Long, symPtr: Long, sortPtr: Long): Long

    Annotations
    @native()

  211. def theoryMkFuncDecl (ctxPtr: Long, thyPtr: Long, symPtr: Long, domainSize: Int, domainSorts: Array[Long], rangeSort: Long): Long

    Annotations
    @native()

  212. def theoryMkSort (ctxPtr: Long, thyPtr: Long, symPtr: Long): Long

    Annotations
    @native()

  213. def theoryMkValue (ctxPtr: Long, thyPtr: Long, symPtr: Long, sortPtr: Long): Long

    Annotations
    @native()

  214. def toPtrArray (ptrs: Array[Pointer]): Array[Long]

  215. def toggleWarningMessages (enabled: Boolean): Unit

    Annotations
    @native()

  216. def traceOff (contextPtr: Long): Unit

    Annotations
    @native()

  217. def traceToFile (contextPtr: Long, traceFile: String): Boolean

    Annotations
    @native()

  218. def traceToStderr (contextPtr: Long): Unit

    Annotations
    @native()

  219. def traceToStdout (contextPtr: Long): Unit

    Annotations
    @native()

  220. def updateParamValue (contextPtr: Long, paramID: String, paramValue: String): Unit

    Annotations
    @native()

  221. def wrapperVersionString (): String

  222. def z3VersionString (): String