sealed class Z3Context extends AnyRef
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- Z3Context
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- All
Instance Constructors
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
- val astQueue: Z3RefCountQueue[Z3ASTLike]
- def astToString(ast: Z3AST): String
- val astVectorQueue: Z3RefCountQueue[Z3ASTVector]
- def benchmarkToSMTLIBString(name: String, logic: String, status: String, attributes: String, assumptions: Seq[Z3AST], formula: Z3AST): String
-
def
clone(): AnyRef
- Attributes
- protected[java.lang]
- Definition Classes
- AnyRef
- Annotations
- @native() @throws( ... )
- val config: Map[String, String]
- def delete(): Unit
- val entryQueue: Z3RefCountQueue[Z3FuncInterpEntry]
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
finalize(): Unit
- Definition Classes
- Z3Context → AnyRef
- def funcDeclToString(funcDecl: Z3FuncDecl): String
- def getASTKind(ast: Z3AST): Z3ASTKind
- def getAbsFuncDecl(): Z3FuncDecl
- def getAppDecl(ast: Z3AST, arity: Int = -1): Z3FuncDecl
- def getBoolValue(ast: Z3AST): Option[Boolean]
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- def getDeclFuncDeclParameter(fd: Z3FuncDecl, idx: Int, arity: Int = 1): Z3FuncDecl
- def getDeclKind(funcDecl: Z3FuncDecl): Z3DeclKind
- def getDeclName(fd: Z3FuncDecl): Z3Symbol
- def getDomain(funcDecl: Z3FuncDecl, i: Int): Z3Sort
- def getDomainSize(funcDecl: Z3FuncDecl): Int
- def getFuncDecl(op: Z3DeclKind, sorts: Z3Sort*): Z3FuncDecl
- def getIndexValue(ast: Z3AST): Int
- def getNumeralInt(ast: Z3AST): Z3NumeralIntAST
- def getNumeralReal(ast: Z3AST): Z3NumeralRealAST
- def getQuantifierBody(ast: Z3AST): Z3AST
- def getQuantifierBoundName(ast: Z3AST, i: Int): Z3Symbol
- def getQuantifierNumBound(ast: Z3AST): Int
- def getRange(funcDecl: Z3FuncDecl): Z3Sort
- def getSort(ast: Z3AST): Z3Sort
- def getString(ast: Z3AST): String
- def getSymbolKind(symbol: Z3Symbol): Z3SymbolKind[_]
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- val interpQueue: Z3RefCountQueue[Z3FuncInterp]
- def interrupt(): Unit
- def isEqAST(t1: Z3AST, t2: Z3AST): Boolean
- def isEqFuncDecl(fd1: Z3FuncDecl, fd2: Z3FuncDecl): Boolean
- def isEqSort(s1: Z3Sort, s2: Z3Sort): Boolean
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def isQuantifierForall(ast: Z3AST): Boolean
- def mkADTSorts(defs: Seq[(String, Seq[String], Seq[Seq[(String, ADTSortReference)]])]): Seq[(Z3Sort, Seq[Z3FuncDecl], Seq[Z3FuncDecl], Seq[Seq[Z3FuncDecl]])]
- def mkAdd(args: Z3AST*): Z3AST
- def mkAnd(args: Z3AST*): Z3AST
- def mkApp(funcDecl: Z3FuncDecl, args: Z3AST*): Z3AST
- def mkArrayDefault(array: Z3AST): Z3AST
- def mkArrayMap(op: Z3DeclKind, args: Z3AST*): Z3AST
- def mkArrayMap(f: Z3FuncDecl, args: Z3AST*): Z3AST
- def mkArraySort(domain: Z3Sort, range: Z3Sort): Z3Sort
- def mkBV2Int(ast: Z3AST, isSigned: Boolean): Z3AST
- def mkBVAdd(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVAddNoOverflow(ast1: Z3AST, ast2: Z3AST, isSigned: Boolean): Z3AST
- def mkBVAddNoUnderflow(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVAnd(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVAshr(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVLshr(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVMul(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVMulNoOverflow(ast1: Z3AST, ast2: Z3AST, isSigned: Boolean): Z3AST
- def mkBVMulNoUnderflow(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVNand(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVNeg(ast: Z3AST): Z3AST
- def mkBVNegNoOverflow(ast: Z3AST): Z3AST
- def mkBVNor(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVNot(ast: Z3AST): Z3AST
- def mkBVOr(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVRedAnd(ast: Z3AST): Z3AST
- def mkBVRedOr(ast: Z3AST): Z3AST
- def mkBVSDivNoOverflow(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSdiv(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSge(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSgt(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVShl(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSle(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSlt(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSmod(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSort(size: Int): Z3Sort
- def mkBVSrem(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSub(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSubNoOverflow(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVSubNoUnderflow(ast1: Z3AST, ast2: Z3AST, isSigned: Boolean): Z3AST
- def mkBVUdiv(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVUge(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVUgt(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVUle(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVUlt(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVUrem(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVXnor(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBVXor(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkBoolConst(s: String): Z3AST
- def mkBoolConst(symbol: Z3Symbol): Z3AST
- def mkBoolSort(): Z3Sort
- def mkBound(index: Int, sort: Z3Sort): Z3AST
- def mkConcat(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkConst(s: String, sort: Z3Sort): Z3AST
- def mkConst(symbol: Z3Symbol, sort: Z3Sort): Z3AST
- def mkConstArray(sort: Z3Sort, value: Z3AST): Z3AST
- def mkDistinct(args: Z3AST*): Z3AST
- def mkDiv(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkEmptySeq(sort: Z3Sort): Z3AST
- def mkEmptySet(sort: Z3Sort): Z3AST
- def mkEq(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkExists(weight: Int, patterns: Seq[Z3Pattern], decls: Seq[(Z3Symbol, Z3Sort)], body: Z3AST): Z3AST
- def mkExistsConst(weight: Int, patterns: Seq[Z3Pattern], bounds: Seq[Z3AST], body: Z3AST): Z3AST
- def mkExtRotateLeft(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkExtRotateRight(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkExtract(high: Int, low: Int, ast: Z3AST): Z3AST
- def mkFalse(): Z3AST
- def mkForAllConst(weight: Int, patterns: Seq[Z3Pattern], bounds: Seq[Z3AST], body: Z3AST): Z3AST
- def mkForall(weight: Int, patterns: Seq[Z3Pattern], decls: Seq[(Z3Symbol, Z3Sort)], body: Z3AST): Z3AST
- def mkFreshBoolConst(prefix: String): Z3AST
- def mkFreshConst(prefix: String, sort: Z3Sort): Z3AST
- def mkFreshFuncDecl(prefix: String, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort): Z3FuncDecl
- def mkFreshIntConst(prefix: String): Z3AST
- def mkFreshIntSymbol: Z3Symbol
- def mkFreshStringSymbol(s: String): Z3Symbol
- def mkFullSet(sort: Z3Sort): Z3AST
- def mkFuncDecl(symbol: String, domainSort: Z3Sort, rangeSort: Z3Sort): Z3FuncDecl
- def mkFuncDecl(symbol: String, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort): Z3FuncDecl
- def mkFuncDecl(symbol: Z3Symbol, domainSort: Z3Sort, rangeSort: Z3Sort): Z3FuncDecl
- def mkFuncDecl(symbol: Z3Symbol, domainSorts: Seq[Z3Sort], rangeSort: Z3Sort): Z3FuncDecl
- 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 mkInt2BV(size: Int, ast: Z3AST): Z3AST
- def mkInt2Real(ast: Z3AST): Z3AST
- def mkIntConst(s: String): Z3AST
- def mkIntConst(symbol: Z3Symbol): 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: Z3AST*): Z3AST
- def mkNot(ast: Z3AST): Z3AST
- def mkNumeral(value: String, sort: Z3Sort): Z3AST
- def mkOptimizer(): Z3Optimizer
- def mkOr(args: Z3AST*): Z3AST
- def mkPattern(args: Z3AST*): Z3Pattern
- def mkPower(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkQuantifier(isForAll: Boolean, weight: Int, patterns: Seq[Z3Pattern], decls: Seq[(Z3Symbol, Z3Sort)], body: Z3AST): Z3AST
- def mkQuantifierConst(isForAll: Boolean, weight: Int, patterns: Seq[Z3Pattern], bounds: Seq[Z3AST], body: Z3AST): Z3AST
- def mkReConcat(args: Z3AST*): Z3AST
- def mkReOption(re: Z3AST): Z3AST
- def mkRePlus(re: Z3AST): Z3AST
- def mkReStar(re: Z3AST): Z3AST
- def mkReUnion(args: Z3AST*): Z3AST
- def mkReal(numerator: Int, denominator: Int): Z3AST
- def mkReal2Int(ast: Z3AST): Z3AST
- def mkRealSort(): Z3Sort
- def mkRem(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkRepeat(count: Int, ast: Z3AST): Z3AST
- def mkSelect(array: Z3AST, index: Z3AST): Z3AST
- def mkSeqAt(seq: Z3AST, i: Z3AST): Z3AST
- def mkSeqConcat(args: Z3AST*): Z3AST
- def mkSeqContains(seq1: Z3AST, seq2: Z3AST): Z3AST
- def mkSeqExtract(seq: Z3AST, start: Z3AST, length: Z3AST): Z3AST
- def mkSeqInRe(seq: Z3AST, re: Z3AST): Z3AST
- def mkSeqIndexOf(seq: Z3AST, sub: Z3AST, offset: Z3AST): Z3AST
- def mkSeqLength(e: Z3AST): Z3AST
- def mkSeqPrefix(seq1: Z3AST, seq2: Z3AST): Z3AST
- def mkSeqReplace(seq: Z3AST, src: Z3AST, dest: Z3AST): Z3AST
- def mkSeqSort(underlying: Z3Sort): Z3Sort
- def mkSeqSuffix(seq1: Z3AST, seq2: Z3AST): Z3AST
- def mkSeqToRe(seq: Z3AST): Z3AST
- def mkSetAdd(set: Z3AST, elem: Z3AST): Z3AST
- def mkSetComplement(ast: Z3AST): Z3AST
- def mkSetDel(set: Z3AST, elem: Z3AST): Z3AST
- def mkSetDifference(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkSetIntersect(args: Z3AST*): Z3AST
- def mkSetMember(elem: Z3AST, set: Z3AST): Z3AST
- def mkSetSort(underlying: Z3Sort): Z3Sort
- def mkSetSubset(ast1: Z3AST, ast2: Z3AST): Z3AST
- def mkSetUnion(args: Z3AST*): Z3AST
- def mkSignExt(extraSize: Int, ast: Z3AST): Z3AST
- def mkSimpleSolver(): Z3Solver
- def mkSolver(tactic: Z3Tactic): Z3Solver
- def mkSolver(): Z3Solver
- def mkStore(array: Z3AST, index: Z3AST, value: Z3AST): Z3AST
- def mkString(s: String): Z3AST
- def mkStringSort(): Z3AST
- def mkStringSymbol(s: String): Z3Symbol
- def mkSub(args: Z3AST*): Z3AST
- def mkSymbol(s: String): Z3Symbol
- def mkSymbol(i: Int): Z3Symbol
- def mkTactic(name: String): Z3Tactic
- def mkTacticAndThen(tactic1: Z3Tactic, tactic2: Z3Tactic): Z3Tactic
- def mkTrue(): Z3AST
- def mkTupleSort(name: String, sorts: Z3Sort*): (Z3Sort, Z3FuncDecl, Seq[Z3FuncDecl])
- def mkTupleSort(name: Z3Symbol, sorts: Z3Sort*): (Z3Sort, Z3FuncDecl, Seq[Z3FuncDecl])
- def mkUnaryMinus(ast: Z3AST): Z3AST
- def mkUninterpretedSort(s: String): Z3Sort
- def mkUninterpretedSort(s: Z3Symbol): Z3Sort
- def mkUnitSeq(e: Z3AST): Z3AST
- def mkXor(t1: Z3AST, t2: Z3AST): Z3AST
- def mkZeroExt(extraSize: Int, ast: Z3AST): Z3AST
- val modelQueue: Z3RefCountQueue[Z3Model]
- def modelToString(model: Z3Model): String
-
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()
- def onError(code: Long): Nothing
- val optimizerQueue: Z3RefCountQueue[Z3Optimizer]
- val paramsQueue: Z3RefCountQueue[Z3Params]
-
def
parseSMTLIB2File(fileName: String, sorts: Map[Z3Symbol, Z3Sort], decls: Map[Z3Symbol, Z3FuncDecl]): Z3AST
Uses the SMT-LIB 2 parser to read in a benchmark file.
Uses the SMT-LIB 2 parser to read in a benchmark file. The maps are used to override symbols that would otherwise be created by the parser.
-
def
parseSMTLIB2File(fileName: String): Z3AST
Uses the SMT-LIB 2 parser to read in a benchmark file.
-
def
parseSMTLIB2String(str: String, sorts: Map[Z3Symbol, Z3Sort], decls: Map[Z3Symbol, Z3FuncDecl]): Z3AST
Uses the SMT-LIB 2 parser to read in a benchmark string.
Uses the SMT-LIB 2 parser to read in a benchmark string. The maps are used to override symbols that would otherwise be created by the parser.
-
def
parseSMTLIB2String(str: String): Z3AST
Uses the SMT-LIB 2 parser to read in a benchmark string.
- def patternToString(pattern: Z3Pattern): String
- val ptr: Long
- def setAstPrintMode(printMode: AstPrintMode): Unit
- def simplifyAst(ast: Z3AST): Z3AST
- val solverQueue: Z3RefCountQueue[Z3Solver]
- def sortToString(sort: Z3Sort): String
- def substitute(ast: Z3AST, from: Array[Z3AST], to: Array[Z3AST]): Z3AST
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
- val tacticQueue: Z3RefCountQueue[Z3Tactic]
-
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( ... )
Deprecated Value Members
-
def
softCheckCancel(): Unit
- Annotations
- @deprecated
- Deprecated
(Since version ) Use interrupt instead