Packages

c

z3.java

Z3Context

class Z3Context extends Z3Pointer

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

Instance Constructors

  1. 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. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  6. def delete(): Unit
  7. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  8. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  9. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  10. def getBoolValue(ast: Z3AST): Boolean
  11. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def getNumeralInt(ast: Z3AST): Integer
  13. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. def isEqAST(t1: Z3AST, t2: Z3AST): Boolean
  15. def isEqSort(s1: Z3Sort, s2: Z3Sort): Boolean
  16. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  17. def mkAdd(args: <repeated...>[Z3AST]): Z3AST
  18. def mkAnd(args: <repeated...>[Z3AST]): Z3AST
  19. def mkBoolSort(): Z3Sort
  20. def mkConst(symbol: Z3Symbol, sort: Z3Sort): Z3AST
  21. def mkDistinct(args: <repeated...>[Z3AST]): Z3AST
  22. def mkDiv(ast1: Z3AST, ast2: Z3AST): Z3AST
  23. def mkEq(ast1: Z3AST, ast2: Z3AST): Z3AST
  24. def mkFalse(): Z3AST
  25. def mkGE(ast1: Z3AST, ast2: Z3AST): Z3AST
  26. def mkGT(ast1: Z3AST, ast2: Z3AST): Z3AST
  27. def mkITE(t1: Z3AST, t2: Z3AST, t3: Z3AST): Z3AST
  28. def mkIff(t1: Z3AST, t2: Z3AST): Z3AST
  29. def mkImplies(t1: Z3AST, t2: Z3AST): Z3AST
  30. def mkInt(value: Int, sort: Z3Sort): Z3AST
  31. def mkInt2Real(ast: Z3AST): Z3AST
  32. def mkIntSort(): Z3Sort
  33. def mkIntSymbol(i: Int): Z3Symbol
  34. def mkIsInt(ast: Z3AST): Z3AST
  35. def mkLE(ast1: Z3AST, ast2: Z3AST): Z3AST
  36. def mkLT(ast1: Z3AST, ast2: Z3AST): Z3AST
  37. def mkMod(ast1: Z3AST, ast2: Z3AST): Z3AST
  38. def mkMul(args: <repeated...>[Z3AST]): Z3AST
  39. def mkNot(ast: Z3AST): Z3AST
  40. def mkOr(args: <repeated...>[Z3AST]): Z3AST
  41. def mkReal(value: Double, numerator: Int, denominator: Int): Z3AST
  42. def mkReal2Int(ast: Z3AST): Z3AST
  43. def mkRealSort(): Z3Sort
  44. def mkRem(ast1: Z3AST, ast2: Z3AST): Z3AST
  45. def mkStringSymbol(s: String): Z3Symbol
  46. def mkSub(args: <repeated...>[Z3AST]): Z3AST
  47. def mkTrue(): Z3AST
  48. def mkUnaryMinus(ast: Z3AST): Z3AST
  49. def mkUninterpretedSort(s: Z3Symbol): Z3Sort
  50. def mkXor(t1: Z3AST, t2: Z3AST): Z3AST
  51. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  52. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  53. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  54. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  55. def toString(): String
    Definition Classes
    AnyRef → Any
  56. def updateParamValue(paramID: String, paramValue: String): Unit
  57. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  58. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  59. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Z3Pointer

Inherited from LongPtr

Inherited from AnyRef

Inherited from Any

Ungrouped