Packages

package tools

Arithmetic back-ends and arithmetic utilities for tactics, including an SMT interface.

To do

Stub. Describe for real.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. tools
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. trait AlgebraTool extends ToolInterface

    Tool for computer algebraic computations.

    Tool for computer algebraic computations.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.ToolProvider

  2. abstract class BaseKeYmaeraMathematicaBridge[T] extends KeYmaeraMathematicaBridge[T]

    Base class for Mathematica bridges.

    Base class for Mathematica bridges. Running commands is synchronized.

  3. class ConversionException extends Exception
  4. trait CounterExampleTool extends ToolInterface

    Quantifier elimination tool.

    Quantifier elimination tool.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.ToolProvider

  5. trait DerivativeTool extends ToolInterface

    Tool for computing symbolic derivatives (oracle for tactics).

  6. trait EquationSolverTool extends ToolInterface

    Tool for computing the solution of an equation system.

    Tool for computing the solution of an equation system.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.ToolProvider

  7. case class HashEvidence(h: String) extends Evidence with Product with Serializable
  8. class JLinkMathematicaLink extends MathematicaLink with Logging

    A link to Mathematica using the JLink interface.

  9. trait K2MConverter[T] extends (T) ⇒ MExpr

    Converts KeYmaera -> Mathematica

    Converts KeYmaera -> Mathematica

    T

    usually Expression, but also other source types for non-soundness-critical conversions.

  10. class KMComparator extends AnyRef

    Compares Mathematica expressions for equality (handles conversion differences).

  11. trait KeYmaeraMathematicaBridge[T] extends AnyRef

    Bridge for MathematicaLink, bundles tool executor (thread pools) with converters.

  12. class KeYmaeraToMathematica extends K2MConverter[KExpr]
  13. trait M2KConverter[T] extends (MExpr) ⇒ T

    Converts Mathematica -> KeYmaera

    Converts Mathematica -> KeYmaera

    T

    usually Expression, but also other target types for non-soundness-critical conversions.

  14. class MKComparator[T] extends AnyRef
  15. class Mathematica extends ToolBase with QETool with InvGenTool with ODESolverTool with CounterExampleTool with SimulationTool with DerivativeTool with EquationSolverTool with SimplificationTool with AlgebraTool with PDESolverTool with ToolOperationManagement

    Mathematica tool for quantifier elimination and solving differential equations.

    Mathematica tool for quantifier elimination and solving differential equations.

    Created by smitsch on 4/27/15.

    To do

    Code Review: Move non-critical tool implementations into a separate package tactictools

  16. class MathematicaAlgebraTool extends BaseKeYmaeraMathematicaBridge[KExpr] with AlgebraTool

    A link to Mathematica using the JLink interface.

  17. class MathematicaCEXTool extends BaseKeYmaeraMathematicaBridge[KExpr] with CounterExampleTool with Logging

    Mathematica counter example implementation.

  18. class MathematicaComputationAbortedException extends ConversionException

    Internal abort of computations (e.g., by TimeConstrained).

  19. class MathematicaComputationExternalAbortException extends ConversionException

    Externally triggered abort (e.g., by stopping from the UI).

  20. class MathematicaComputationFailedException extends ConversionException
  21. class MathematicaEquationSolverTool extends BaseKeYmaeraMathematicaBridge[KExpr] with EquationSolverTool

    A link to Mathematica using the JLink interface.

  22. class MathematicaInvGenTool extends BaseKeYmaeraMathematicaBridge[KExpr] with InvGenTool with Logging

    A continuous invariant implementation using Mathematica over the JLink interface.

  23. trait MathematicaLink extends AnyRef

    An abstract interface to Mathematica link implementations.

    An abstract interface to Mathematica link implementations. The link may be used synchronously or asychronously. Multiple MathematicaLinks may be created by instantiating multiple copies of implementing classes (depends on license).

  24. class MathematicaODESolverTool extends BaseKeYmaeraMathematicaBridge[KExpr] with ODESolverTool with DerivativeTool

    A link to Mathematica using the JLink interface.

  25. class MathematicaPDESolverTool extends BaseKeYmaeraMathematicaBridge[KExpr] with PDESolverTool

    A link to Mathematica using the JLink interface.

  26. class MathematicaQETool extends BaseKeYmaeraMathematicaBridge[KExpr] with QETool with Logging

    A QE tool implementation using Mathematica over the JLink interface.

  27. class MathematicaSimplificationTool extends BaseKeYmaeraMathematicaBridge[KExpr] with SimplificationTool

    A link to Mathematica using the JLink interface.

  28. class MathematicaSimulationTool extends BaseKeYmaeraMathematicaBridge[Simulation] with SimulationTool

    A link to Mathematica using the JLink interface.

  29. class MathematicaToKeYmaera extends M2KConverter[KExpr]
  30. class NoCountExException extends Exception
  31. trait ODESolverTool extends ToolInterface

    Tool for computing the symbolic solution of a differential equation system.

    Tool for computing the symbolic solution of a differential equation system.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.ToolProvider

  32. trait PDESolverTool extends ToolInterface

    Tool for computing the symbolic solution of a partial differential equation system.

    Tool for computing the symbolic solution of a partial differential equation system.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.ToolProvider

  33. class Polya extends ToolBase with QETool

    Polya quantifier elimination tool.

    Polya quantifier elimination tool.

    Created by smitsch on 4/27/15.

  34. class PolyaSolver extends SMTSolver with Logging

    Created by ran on 4/24/15.

  35. class SMTConversionException extends ConversionException
  36. abstract class SMTConverter extends (Formula) ⇒ String with Logging

    Base class for SMT converters with conversion per SMTLib specification.

    Base class for SMT converters with conversion per SMTLib specification. Created by ran on 8/24/15.

  37. class SMTQeException extends Exception
  38. trait SMTSolver extends QETool

    Common interface for SMT solvers.

  39. trait SimplificationTool extends ToolInterface

    Tool for simplifying logical and/or arithmetical expressions.

    Tool for simplifying logical and/or arithmetical expressions.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.ToolProvider

  40. trait SimulationTool extends ToolInterface

    Simulation tool.

  41. class TestSynthesis extends BaseKeYmaeraMathematicaBridge[KExpr]

    Synthesize test case configurations from ModelPlex formulas.

    Synthesize test case configurations from ModelPlex formulas. Requires Mathematica.

    Created by smitsch on 12/6/16.

  42. trait Tool extends AnyRef

    Defines the lifecycle for external tools.

    Defines the lifecycle for external tools. A tool is available once init is called. It cannot be used after shutdown. For intermediate restarting, use check_and_recover.

  43. abstract class ToolBase extends Tool

    Base class for tool instances (e.g., a specific mathematica kernel)

  44. case class ToolEvidence(info: List[(String, String)]) extends Evidence with Product with Serializable
  45. case class ToolException(msg: String, cause: Throwable = null) extends ProverException with Product with Serializable

    Arithmetic tool exceptions

  46. class ToolExecutor[T] extends Logging
  47. trait ToolInterface extends AnyRef

    Base trait tagging interfaces to tools.

  48. trait ToolOperationManagement extends ToolInterface

    Manages how a tool's operations work (e.g., timeouts).

  49. abstract class ToolOperationManagementBase extends ToolOperationManagement

    Base class for tool operation management

  50. class UncheckedK2MConverter extends KeYmaeraToMathematica
  51. class UncheckedM2KConverter extends MathematicaToKeYmaera
  52. class Z3 extends ToolBase with QETool with ToolOperationManagement

    Z3 quantifier elimination tool.

    Z3 quantifier elimination tool.

    Created by smitsch on 4/27/15.

  53. class Z3Solver extends ToolOperationManagementBase with SMTSolver with Logging

    Created by ran on 3/27/15.

Value Members

  1. def diagnostic: String

    Gather diagnostic information about the system configuration relevant to KeYmaera X and its tool integrations.

  2. object CEXK2MConverter extends UncheckedK2MConverter
  3. object CEXM2KConverter extends UncheckedM2KConverter
  4. object DefaultSMTConverter extends SMTConverter

    A default SMT converter with output as preferred by KeYmaera X.

  5. object DiffUncheckedM2KConverter
  6. object KMComparator

    Implicit conversion from Mathematica expressions to comparator.

  7. object KeYmaeraToMathematica extends KeYmaeraToMathematica

    Converts KeYmaeara X expression data structures to Mathematica Expr objects.

  8. object KeYmaeraXTool extends ToolBase

    The KeYmaera X tool.

    The KeYmaera X tool.

    Created by smitsch on 4/27/15.

  9. object MKComparator

    Implicit conversion from KeYmaera expressions to comparator.

  10. object MathematicaConversion

    Mathematica conversion stuff.

  11. object MathematicaToKeYmaera extends MathematicaToKeYmaera

    Converts com.wolfram.jlink.Expr -> edu.cmu...keymaerax.core.Expr

  12. object PegasusM2KConverter extends UncheckedM2KConverter
  13. object SimulationK2MConverter extends K2MConverter[Simulation]
  14. object SimulationM2KConverter extends M2KConverter[Simulation]
  15. object SimulationTool

Deprecated Value Members

  1. object ToolConversions
    Annotations
    @deprecated
    Deprecated

Inherited from AnyRef

Inherited from Any

Ungrouped