package scala
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- scala
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- All
Type Members
-
trait
Default[A] extends AnyRef
A type class for Scala types that are representable in Z3 and that admit a default value.
A type class for Scala types that are representable in Z3 and that admit a default value. The default value is used for model reconstruction when no other value is available.
- Annotations
- @implicitNotFound( ... )
- sealed class Z3AST extends Z3ASTLike
- sealed abstract class Z3ASTKind extends AnyRef
- trait Z3ASTLike extends Z3Object
- final class Z3ASTVector extends Z3Object
- case class Z3AppAST extends Z3ASTKind with Product with Serializable
- sealed class Z3Context extends AnyRef
- sealed abstract class Z3DeclKind extends AnyRef
- sealed class Z3FuncDecl extends Z3ASTLike
- case class Z3FuncDeclAST extends Z3ASTKind with Product with Serializable
- case class Z3IntSymbol extends Z3SymbolKind[Int] with Product with Serializable
- sealed class Z3Model extends Z3Object
- sealed abstract class Z3NumeralAST extends Z3ASTKind
- case class Z3NumeralIntAST extends Z3NumeralAST with Product with Serializable
- case class Z3NumeralRealAST extends Z3NumeralAST with Product with Serializable
- trait Z3Object extends Z3Pointer
- class Z3Optimizer extends Z3Object
- sealed class Z3Pattern extends Z3ASTLike
- trait Z3Pointer extends AnyRef
- case class Z3QuantifierAST extends Z3ASTKind with Product with Serializable
- class Z3RefCountQueue[T <: Z3Object] extends AnyRef
- sealed abstract class Z3SearchFailure extends AnyRef
- class Z3Solver extends Z3Object
- sealed class Z3Sort extends Z3ASTLike
- case class Z3SortAST extends Z3ASTKind with Product with Serializable
- case class Z3StringSymbol extends Z3SymbolKind[String] with Product with Serializable
- sealed class Z3Symbol extends Z3Pointer
- sealed abstract class Z3SymbolKind[T] extends AnyRef
- class Z3Tactic extends Z3Object
- case class Z3VarAST extends Z3ASTKind with Product with Serializable
Value Members
- implicit def astvectorToSeq(v: Z3ASTVector): Seq[Z3AST]
- def error(any: Any): Nothing
-
def
i2ob(value: Int): Option[Boolean]
- Attributes
- protected[z3]
- def resetMemory: Unit
-
def
toPtrArray(ptrs: Iterable[Z3Pointer]): Array[Long]
- Attributes
- protected[z3]
- def toggleWarningMessages(enabled: Boolean): Unit
-
lazy val
version: String
A string representation of the version numbers for Z3, and the API (including bindings)
- object OpAGNum extends Z3DeclKind
- object OpANum extends Z3DeclKind
- object OpAdd extends Z3DeclKind
- object OpAnd extends Z3DeclKind
- object OpArrayDefault extends Z3DeclKind
- object OpArrayExt extends Z3DeclKind
- object OpArrayMap extends Z3DeclKind
- object OpAsArray extends Z3DeclKind
- object OpBAdd extends Z3DeclKind
- object OpBAnd extends Z3DeclKind
- object OpBAshr extends Z3DeclKind
- object OpBComp extends Z3DeclKind
- object OpBLshr extends Z3DeclKind
- object OpBMul extends Z3DeclKind
- object OpBNand extends Z3DeclKind
- object OpBNeg extends Z3DeclKind
- object OpBNor extends Z3DeclKind
- object OpBNot extends Z3DeclKind
- object OpBNum extends Z3DeclKind
- object OpBOr extends Z3DeclKind
- object OpBRedAnd extends Z3DeclKind
- object OpBRedOr extends Z3DeclKind
- object OpBSDiv extends Z3DeclKind
- object OpBSMod extends Z3DeclKind
- object OpBSRem extends Z3DeclKind
- object OpBShl extends Z3DeclKind
- object OpBSub extends Z3DeclKind
- object OpBUDiv extends Z3DeclKind
- object OpBURem extends Z3DeclKind
- object OpBVToInt extends Z3DeclKind
- object OpBXnor extends Z3DeclKind
- object OpBXor extends Z3DeclKind
- object OpBit0 extends Z3DeclKind
- object OpBit1 extends Z3DeclKind
- object OpCarry extends Z3DeclKind
- object OpConcat extends Z3DeclKind
- object OpConstArray extends Z3DeclKind
- object OpDTAccessor extends Z3DeclKind
- object OpDTConstructor extends Z3DeclKind
- object OpDTRecogniser extends Z3DeclKind
- object OpDTUpdateField extends Z3DeclKind
- object OpDistinct extends Z3DeclKind
- object OpDiv extends Z3DeclKind
- object OpEq extends Z3DeclKind
- object OpExtRotateLeft extends Z3DeclKind
- object OpExtRotateRight extends Z3DeclKind
- object OpExtract extends Z3DeclKind
- object OpFPAAbs extends Z3DeclKind
- object OpFPAAdd extends Z3DeclKind
- object OpFPADiv extends Z3DeclKind
- object OpFPAEq extends Z3DeclKind
- object OpFPAFMA extends Z3DeclKind
- object OpFPAFP extends Z3DeclKind
- object OpFPAGE extends Z3DeclKind
- object OpFPAGT extends Z3DeclKind
- object OpFPAIsInf extends Z3DeclKind
- object OpFPAIsNaN extends Z3DeclKind
- object OpFPAIsNegative extends Z3DeclKind
- object OpFPAIsNormal extends Z3DeclKind
- object OpFPAIsPositive extends Z3DeclKind
- object OpFPAIsSubnormal extends Z3DeclKind
- object OpFPAIsZero extends Z3DeclKind
- object OpFPALE extends Z3DeclKind
- object OpFPALT extends Z3DeclKind
- object OpFPAMax extends Z3DeclKind
- object OpFPAMin extends Z3DeclKind
- object OpFPAMinusInf extends Z3DeclKind
- object OpFPAMinusZero extends Z3DeclKind
- object OpFPAMul extends Z3DeclKind
- object OpFPANaN extends Z3DeclKind
- object OpFPANeg extends Z3DeclKind
- object OpFPANum extends Z3DeclKind
- object OpFPAPlusInf extends Z3DeclKind
- object OpFPAPlusZero extends Z3DeclKind
- object OpFPARem extends Z3DeclKind
- object OpFPARmNearestTiesToAway extends Z3DeclKind
- object OpFPARmNearestTiesToEven extends Z3DeclKind
- object OpFPARmTowardNegative extends Z3DeclKind
- object OpFPARmTowardPositive extends Z3DeclKind
- object OpFPARmTowardZero extends Z3DeclKind
- object OpFPARoundToIntegral extends Z3DeclKind
- object OpFPASqrt extends Z3DeclKind
- object OpFPASub extends Z3DeclKind
- object OpFPAToFP extends Z3DeclKind
- object OpFPAToFPUnsigned extends Z3DeclKind
- object OpFPAToIEEEBV extends Z3DeclKind
- object OpFPAToReal extends Z3DeclKind
- object OpFPAToSBV extends Z3DeclKind
- object OpFPAToUBV extends Z3DeclKind
- object OpFalse extends Z3DeclKind
- object OpFdConstant extends Z3DeclKind
- object OpFdLT extends Z3DeclKind
- object OpGE extends Z3DeclKind
- object OpGT extends Z3DeclKind
- object OpIDiv extends Z3DeclKind
- object OpITE extends Z3DeclKind
- object OpIff extends Z3DeclKind
- object OpImplies extends Z3DeclKind
- object OpIntToBV extends Z3DeclKind
- object OpInternal extends Z3DeclKind
- object OpIsInt extends Z3DeclKind
- object OpLE extends Z3DeclKind
- object OpLT extends Z3DeclKind
- object OpLabel extends Z3DeclKind
- object OpLabelLit extends Z3DeclKind
- object OpMod extends Z3DeclKind
- object OpMul extends Z3DeclKind
- object OpNot extends Z3DeclKind
- object OpOEq extends Z3DeclKind
- object OpOr extends Z3DeclKind
- object OpPBAtMost extends Z3DeclKind
- object OpPBGE extends Z3DeclKind
- object OpPBLE extends Z3DeclKind
- object OpPower extends Z3DeclKind
- object OpPrAndElim extends Z3DeclKind
- object OpPrApplyDef extends Z3DeclKind
- object OpPrAsserted extends Z3DeclKind
- object OpPrCommutativity extends Z3DeclKind
- object OpPrDER extends Z3DeclKind
- object OpPrDefAxiom extends Z3DeclKind
- object OpPrDefIntro extends Z3DeclKind
- object OpPrDistributivity extends Z3DeclKind
- object OpPrElimUnusedVars extends Z3DeclKind
- object OpPrGoal extends Z3DeclKind
- object OpPrHyperResolve extends Z3DeclKind
- object OpPrHypothesis extends Z3DeclKind
- object OpPrIffFalse extends Z3DeclKind
- object OpPrIffOEq extends Z3DeclKind
- object OpPrIffTrue extends Z3DeclKind
- object OpPrLemma extends Z3DeclKind
- object OpPrModusPonens extends Z3DeclKind
- object OpPrModusPonensOEq extends Z3DeclKind
- object OpPrMonotonicity extends Z3DeclKind
- object OpPrNNFNeg extends Z3DeclKind
- object OpPrNNFPos extends Z3DeclKind
- object OpPrNotOrElim extends Z3DeclKind
- object OpPrPullQuant extends Z3DeclKind
- object OpPrPushQuant extends Z3DeclKind
- object OpPrQuantInst extends Z3DeclKind
- object OpPrQuantIntro extends Z3DeclKind
- object OpPrReflexivity extends Z3DeclKind
- object OpPrRewrite extends Z3DeclKind
- object OpPrRewriteStar extends Z3DeclKind
- object OpPrSkolemize extends Z3DeclKind
- object OpPrSymmetry extends Z3DeclKind
- object OpPrThLemma extends Z3DeclKind
- object OpPrTransitivity extends Z3DeclKind
- object OpPrTransitivityStar extends Z3DeclKind
- object OpPrTrue extends Z3DeclKind
- object OpPrUndef extends Z3DeclKind
- object OpPrUnitResolution extends Z3DeclKind
- object OpRAClone extends Z3DeclKind
- object OpRAComplement extends Z3DeclKind
- object OpRAEmpty extends Z3DeclKind
- object OpRAFilter extends Z3DeclKind
- object OpRAIsEmpty extends Z3DeclKind
- object OpRAJoin extends Z3DeclKind
- object OpRANegationFilter extends Z3DeclKind
- object OpRAProject extends Z3DeclKind
- object OpRARename extends Z3DeclKind
- object OpRASelect extends Z3DeclKind
- object OpRAStore extends Z3DeclKind
- object OpRAUnion extends Z3DeclKind
- object OpRAWiden extends Z3DeclKind
- object OpREConcat extends Z3DeclKind
- object OpREOption extends Z3DeclKind
- object OpREPlus extends Z3DeclKind
- object OpREStar extends Z3DeclKind
- object OpREUnion extends Z3DeclKind
- object OpRem extends Z3DeclKind
- object OpRepeat extends Z3DeclKind
- object OpRotateLeft extends Z3DeclKind
- object OpRotateRight extends Z3DeclKind
- object OpSGE extends Z3DeclKind
- object OpSGT extends Z3DeclKind
- object OpSLE extends Z3DeclKind
- object OpSLT extends Z3DeclKind
- object OpSelect extends Z3DeclKind
- object OpSeqAt extends Z3DeclKind
- object OpSeqConcat extends Z3DeclKind
- object OpSeqContains extends Z3DeclKind
- object OpSeqEmpty extends Z3DeclKind
- object OpSeqExtract extends Z3DeclKind
- object OpSeqInRE extends Z3DeclKind
- object OpSeqIndex extends Z3DeclKind
- object OpSeqLength extends Z3DeclKind
- object OpSeqPrefix extends Z3DeclKind
- object OpSeqReplace extends Z3DeclKind
- object OpSeqSuffix extends Z3DeclKind
- object OpSeqToRE extends Z3DeclKind
- object OpSeqUnit extends Z3DeclKind
- object OpSetComplement extends Z3DeclKind
- object OpSetDifference extends Z3DeclKind
- object OpSetIntersect extends Z3DeclKind
- object OpSetSubset extends Z3DeclKind
- object OpSetUnion extends Z3DeclKind
- object OpSignExt extends Z3DeclKind
- object OpStore extends Z3DeclKind
- object OpSub extends Z3DeclKind
- object OpToInt extends Z3DeclKind
- object OpToReal extends Z3DeclKind
- object OpTrue extends Z3DeclKind
- object OpUGE extends Z3DeclKind
- object OpUGT extends Z3DeclKind
- object OpULE extends Z3DeclKind
- object OpULT extends Z3DeclKind
- object OpUMinus extends Z3DeclKind
- object OpUninterpreted extends Z3DeclKind
- object OpXor extends Z3DeclKind
- object OpXor3 extends Z3DeclKind
- object OpZeroExt extends Z3DeclKind
- object Other extends Z3DeclKind
- object Z3Canceled extends Z3SearchFailure with Product with Serializable
- object Z3Context
- object Z3DeclKind
- object Z3IncompleteTheory extends Z3SearchFailure with Product with Serializable
- object Z3MemoutWatermark extends Z3SearchFailure with Product with Serializable
- object Z3Model
- object Z3NoFailure extends Z3SearchFailure with Product with Serializable
- object Z3NumConflicts extends Z3SearchFailure with Product with Serializable
- object Z3Quantifiers extends Z3SearchFailure with Product with Serializable
- object Z3Timeout extends Z3SearchFailure with Product with Serializable
- object Z3Unknown extends Z3SearchFailure with Product with Serializable
- object Z3UnknownAST extends Z3ASTKind with Product with Serializable