Z3Context

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 (ast: Z3AST): Unit

8. def check (): Boolean

9. def checkAndGetModel (model: Z3Model): Boolean

10. def clone (): AnyRef

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

    @throws()

11. def delete (): Unit

12. def eq (arg0: AnyRef): Boolean

    Attributes

    final

    Definition Classes

    AnyRef

13. def equals (arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

14. def finalize (): Unit

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

    @throws()

15. def getBoolValue (ast: Z3AST): Boolean

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

    Attributes

    final

    Definition Classes

    AnyRef → Any

17. def getNumeralInt (ast: Z3AST): Integer

18. def hashCode (): Int

    Definition Classes

    AnyRef → Any

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

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

21. def isInstanceOf [T0] : Boolean

    Attributes

    final

    Definition Classes

    Any

22. def mkAdd (args: <repeated...>[Z3AST]): Z3AST

23. def mkAnd (args: <repeated...>[Z3AST]): Z3AST

24. def mkBoolSort (): Z3Sort

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

26. def mkDistinct (args: <repeated...>[Z3AST]): Z3AST

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

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

29. def mkFalse (): Z3AST

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

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

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

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

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

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

36. def mkInt2Real (ast: Z3AST): Z3AST

37. def mkIntSort (): Z3Sort

38. def mkIntSymbol (i: Int): Z3Symbol

39. def mkIsInt (ast: Z3AST): Z3AST

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

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

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

43. def mkModel (): Z3Model

44. def mkMul (args: <repeated...>[Z3AST]): Z3AST

45. def mkNot (ast: Z3AST): Z3AST

46. def mkOr (args: <repeated...>[Z3AST]): Z3AST

47. def mkReal2Int (ast: Z3AST): Z3AST

48. def mkRealSort (): Z3Sort

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

50. def mkStringSymbol (s: String): Z3Symbol

51. def mkSub (args: <repeated...>[Z3AST]): Z3AST

52. def mkTrue (): Z3AST

53. def mkUnaryMinus (ast: Z3AST): Z3AST

54. def mkUninterpretedSort (s: Z3Symbol): Z3Sort

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

56. def ne (arg0: AnyRef): Boolean

    Attributes

    final

    Definition Classes

    AnyRef

57. def notify (): Unit

    Attributes

    final

    Definition Classes

    AnyRef

58. def notifyAll (): Unit

    Attributes

    final

    Definition Classes

    AnyRef

59. def pop (numScopes: Int): Unit

60. def push (): Unit

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

    Attributes

    final

    Definition Classes

    AnyRef

62. def toString (): String

    Definition Classes

    AnyRef → Any

63. def traceOff (): Unit

64. def traceToFile (traceFile: String): Boolean

65. def traceToStderr (): Unit

66. def traceToStdout (): Unit

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

68. def wait (): Unit

    Attributes

    final

    Definition Classes

    AnyRef

    Annotations

    @throws()

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

    Attributes

    final

    Definition Classes

    AnyRef

    Annotations

    @throws()

70. def wait (arg0: Long): Unit

    Attributes

    final

    Definition Classes

    AnyRef

    Annotations

    @throws()