Packages

class Z3 extends ToolBase with QETool with ToolOperationManagement

Z3 quantifier elimination tool.

Created by smitsch on 4/27/15.

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Z3
  2. ToolOperationManagement
  3. ToolInterface
  4. QETool
  5. ToolBase
  6. Tool
  7. AnyRef
  8. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Z3()

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  6. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  7. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  8. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  9. def getAvailableWorkers: Int
    Definition Classes
    Z3ToolOperationManagement
  10. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  11. def getOperationTimeout: Int

    Returns the timeout duration.

    Returns the timeout duration.

    Definition Classes
    Z3ToolOperationManagement
  12. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def init(config: Map[String, String]): Unit

    Initializes the tool with tool-specific configuration parameters.

    Initializes the tool with tool-specific configuration parameters.

    Definition Classes
    Z3Tool
  14. var initialized: Boolean
    Attributes
    protected
    Definition Classes
    ToolBase
  15. def isInitialized: Boolean

    Checks whether this tool has been initialized already.

    Checks whether this tool has been initialized already.

    Definition Classes
    ToolBaseTool
  16. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  17. val name: String
    Definition Classes
    ToolBaseTool
  18. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  20. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. def qeEvidence(formula: Formula): (Formula, Evidence)

    Returns a quantifier-free formula that is equivalent to the specified formula, together with the actual input sent to this tool and the actual output it produced.

    Returns a quantifier-free formula that is equivalent to the specified formula, together with the actual input sent to this tool and the actual output it produced.

    formula

    The formula whose quantifier-free equivalent is sought.

    returns

    An equivalent quantifier-free formula, with tool evidence.

    Definition Classes
    Z3QETool
  22. def restart(): Unit

    Check whether the managed tool is still alive and restart it if need be.

    Check whether the managed tool is still alive and restart it if need be.

    Definition Classes
    Z3Tool
  23. def setOperationTimeout(timeout: Int): Unit

    Sets a maximum duration of this tool's operations (e.g., QE).

    Sets a maximum duration of this tool's operations (e.g., QE).

    Definition Classes
    Z3ToolOperationManagement
  24. def shutdown(): Unit

    Shutdown the tool

    Shutdown the tool

    Definition Classes
    Z3Tool
  25. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  26. def toString(): String
    Definition Classes
    AnyRef → Any
  27. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  28. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  29. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from ToolOperationManagement

Inherited from ToolInterface

Inherited from QETool

Inherited from ToolBase

Inherited from Tool

Inherited from AnyRef

Inherited from Any

Ungrouped