class Z3Context extends Z3Pointer
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- Z3Context
- Z3Pointer
- LongPtr
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- All
Instance Constructors
- new Z3Context(config: Map[String, String])
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
- def delete(): Unit
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
- def getBoolValue(ast: Z3AST): Boolean
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- def getNumeralInt(ast: Z3AST): Integer
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- def isEqAST(t1: Z3AST, t2: Z3AST): Boolean
- def isEqSort(s1: Z3Sort, s2: Z3Sort): Boolean
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def mkAdd(args: <repeated...>[Z3AST]): Z3AST
- def mkAnd(args: <repeated...>[Z3AST]): Z3AST
- def mkBoolSort(): Z3Sort
- def mkConst(symbol: Z3Symbol, sort: Z3Sort): Z3AST
- def mkDistinct(args: <repeated...>[Z3AST]): Z3AST
- def mkDiv(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkEq(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkFalse(): Z3AST
- def mkGE(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkGT(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkITE(t1: Z3AST, t2: Z3AST, t3: Z3AST): Z3AST
- def mkIff(t1: Z3AST, t2: Z3AST): Z3AST
- def mkImplies(t1: Z3AST, t2: Z3AST): Z3AST
- def mkInt(value: Int, sort: Z3Sort): Z3AST
- def mkInt2Real(ast: Z3AST): Z3AST
- def mkIntSort(): Z3Sort
- def mkIntSymbol(i: Int): Z3Symbol
- def mkIsInt(ast: Z3AST): Z3AST
- def mkLE(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkLT(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkMod(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkMul(args: <repeated...>[Z3AST]): Z3AST
- def mkNot(ast: Z3AST): Z3AST
- def mkOr(args: <repeated...>[Z3AST]): Z3AST
- def mkReal(value: Double, numerator: Int, denominator: Int): Z3AST
- def mkReal2Int(ast: Z3AST): Z3AST
- def mkRealSort(): Z3Sort
- def mkRem(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkStringSymbol(s: String): Z3Symbol
- def mkSub(args: <repeated...>[Z3AST]): Z3AST
- def mkTrue(): Z3AST
- def mkUnaryMinus(ast: Z3AST): Z3AST
- def mkUninterpretedSort(s: Z3Symbol): Z3Sort
- def mkXor(t1: Z3AST, t2: Z3AST): Z3AST
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toString(): String
- Definition Classes
- AnyRef → Any
- def updateParamValue(paramID: String, paramValue: String): Unit
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )