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. def delete(): Unit
  2. def getBoolValue(ast: Z3AST): Boolean
  3. def getNumeralInt(ast: Z3AST): Integer
  4. def isEqAST(t1: Z3AST, t2: Z3AST): Boolean
  5. def isEqSort(s1: Z3Sort, s2: Z3Sort): Boolean
  6. def mkAdd(args: <repeated...>[Z3AST]): Z3AST
  7. def mkAnd(args: <repeated...>[Z3AST]): Z3AST
  8. def mkBoolSort(): Z3Sort
  9. def mkConst(symbol: Z3Symbol, sort: Z3Sort): Z3AST
  10. def mkDistinct(args: <repeated...>[Z3AST]): Z3AST
  11. def mkDiv(ast1: Z3AST, ast2: Z3AST): Z3AST
  12. def mkEq(ast1: Z3AST, ast2: Z3AST): Z3AST
  13. def mkFalse(): Z3AST
  14. def mkGE(ast1: Z3AST, ast2: Z3AST): Z3AST
  15. def mkGT(ast1: Z3AST, ast2: Z3AST): Z3AST
  16. def mkITE(t1: Z3AST, t2: Z3AST, t3: Z3AST): Z3AST
  17. def mkIff(t1: Z3AST, t2: Z3AST): Z3AST
  18. def mkImplies(t1: Z3AST, t2: Z3AST): Z3AST
  19. def mkInt(value: Int, sort: Z3Sort): Z3AST
  20. def mkInt2Real(ast: Z3AST): Z3AST
  21. def mkIntSort(): Z3Sort
  22. def mkIntSymbol(i: Int): Z3Symbol
  23. def mkIsInt(ast: Z3AST): Z3AST
  24. def mkLE(ast1: Z3AST, ast2: Z3AST): Z3AST
  25. def mkLT(ast1: Z3AST, ast2: Z3AST): Z3AST
  26. def mkMod(ast1: Z3AST, ast2: Z3AST): Z3AST
  27. def mkMul(args: <repeated...>[Z3AST]): Z3AST
  28. def mkNot(ast: Z3AST): Z3AST
  29. def mkOr(args: <repeated...>[Z3AST]): Z3AST
  30. def mkReal(value: Double, numerator: Int, denominator: Int): Z3AST
  31. def mkReal2Int(ast: Z3AST): Z3AST
  32. def mkRealSort(): Z3Sort
  33. def mkRem(ast1: Z3AST, ast2: Z3AST): Z3AST
  34. def mkStringSymbol(s: String): Z3Symbol
  35. def mkSub(args: <repeated...>[Z3AST]): Z3AST
  36. def mkTrue(): Z3AST
  37. def mkUnaryMinus(ast: Z3AST): Z3AST
  38. def mkUninterpretedSort(s: Z3Symbol): Z3Sort
  39. def mkXor(t1: Z3AST, t2: Z3AST): Z3AST
  40. def updateParamValue(paramID: String, paramValue: String): Unit