Packages

c

edu.cmu.cs.ls.keymaerax.btactics

Z3ToolProvider

case class Z3ToolProvider(config: ToolProvider.Configuration = Map("z3Path" -> Z3Installer.z3Path)) extends PreferredToolProvider[Tool] with Product with Serializable

A tool provider that provides Z3 as QE tool and our own bundled algebra tool and diff. solution tool, everything else is None. Initializes the Z3 installation and updates the Z3 binary on version updates.

Linear Supertypes
Serializable, Serializable, Product, Equals, PreferredToolProvider[Tool], ToolProvider, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Z3ToolProvider
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. PreferredToolProvider
  7. ToolProvider
  8. AnyRef
  9. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Z3ToolProvider(config: ToolProvider.Configuration = Map("z3Path" -> Z3Installer.z3Path))

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. def algebraTool(): Option[AlgebraTool]

    Returns an algebra tool for algebraic computations.

    Returns an algebra tool for algebraic computations.

    Definition Classes
    PreferredToolProviderToolProvider
  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def cexTool(): Option[CounterExampleTool]

    Returns a counterexample tool.

    Returns a counterexample tool.

    Definition Classes
    PreferredToolProviderToolProvider
  7. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  8. val config: ToolProvider.Configuration
  9. def defaultTool(): Option[Tool]

    Returns the default tool

    Returns the default tool

    Definition Classes
    PreferredToolProviderToolProvider
  10. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  11. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  12. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def init(): Boolean

    Initializes the tools.

    Initializes the tools.

    Definition Classes
    Z3ToolProviderPreferredToolProviderToolProvider
  14. def invGenTool(name: Option[String] = None): Option[InvGenTool]
    Definition Classes
    PreferredToolProviderToolProvider
  15. def isInitialized: Boolean

    Indicates whether the tool is initialized.

    Indicates whether the tool is initialized.

    Definition Classes
    PreferredToolProviderToolProvider
  16. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  17. def lyapunovTool(): Option[LyapunovSolverTool]

    Returns a Control Lyapunov Function solver.

    Returns a Control Lyapunov Function solver.

    Definition Classes
    PreferredToolProviderToolProvider
  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 odeTool(): Option[ODESolverTool]

    Returns an ODE tool.

    Returns an ODE tool.

    Definition Classes
    PreferredToolProviderToolProvider
  22. def pdeTool(): Option[PDESolverTool]

    Returns a PDE tool.

    Returns a PDE tool.

    Definition Classes
    PreferredToolProviderToolProvider
  23. def qeTool(name: Option[String] = None): Option[QETacticTool]

    Returns a QE tool.

    Returns a QE tool.

    Definition Classes
    PreferredToolProviderToolProvider
  24. def shutdown(): Unit

    Shutdown the tools provided by this provider.

    Shutdown the tools provided by this provider. After shutdown, the provider hands out None only.

    Definition Classes
    PreferredToolProviderToolProvider
  25. def simplifierTool(): Option[SimplificationTool]

    Returns an arithmetic/logical simplification tool

    Returns an arithmetic/logical simplification tool

    Definition Classes
    PreferredToolProviderToolProvider
  26. def simulationTool(): Option[SimulationTool]

    Returns a simulation tool.

    Returns a simulation tool.

    Definition Classes
    PreferredToolProviderToolProvider
  27. def solverTool(): Option[EquationSolverTool]

    Returns an equation solver tool.

    Returns an equation solver tool.

    Definition Classes
    PreferredToolProviderToolProvider
  28. def sosSolveTool(): Option[SOSsolveTool]

    Returns a SOSsolve tool.

    Returns a SOSsolve tool.

    Definition Classes
    PreferredToolProviderToolProvider
  29. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  30. def tool(): Z3

    Returns the main Z3 tool.

  31. def tool(name: String): Option[Tool]

    Returns the tool with name

    Returns the tool with name

    Definition Classes
    ToolProvider
  32. val toolPreferences: List[Tool]
    Definition Classes
    PreferredToolProvider
  33. def tools(): List[Tool]

    The provided tools.

    The provided tools.

    Definition Classes
    PreferredToolProviderToolProvider
  34. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  35. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  36. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from PreferredToolProvider[Tool]

Inherited from ToolProvider

Inherited from AnyRef

Inherited from Any

Ungrouped