Packages

c

edu.cmu.cs.ls.keymaerax.tools.ext

MathematicaCEXTool

class MathematicaCEXTool extends BaseKeYmaeraMathematicaBridge[Either[KExpr, NamedSymbol]] with CounterExampleTool with Logging

Mathematica counter example implementation.

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. MathematicaCEXTool
  2. Logging
  3. LazyLogging
  4. LoggerHolder
  5. CounterExampleTool
  6. ToolInterface
  7. BaseKeYmaeraMathematicaBridge
  8. KeYmaeraMathematicaBridge
  9. AnyRef
  10. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new MathematicaCEXTool(link: MathematicaLink)

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. val DEBUG: Boolean
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  5. val MEMORY_LIMIT_OFF: Long

    Default memory limit: no limit.

    Default memory limit: no limit.

    Definition Classes
    BaseKeYmaeraMathematicaBridge
  6. val TIMEOUT_OFF: Int

    Default timeout for Mathematica requests: no timeout.

    Default timeout for Mathematica requests: no timeout.

    Definition Classes
    BaseKeYmaeraMathematicaBridge
  7. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  8. def availableWorkers: Int
  9. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  10. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  11. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  12. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  13. def findCounterExample(fml: Formula): Option[Map[NamedSymbol, Expression]]

    Returns a counterexample for the specified formula.

    Returns a counterexample for the specified formula.

    returns

    A counterexample, if found. None otherwise.

    Definition Classes
    MathematicaCEXToolCounterExampleTool
  14. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  15. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  16. def init(): Boolean
  17. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  18. val k2m: K2MConverter[Either[KExpr, NamedSymbol]]
  19. val link: MathematicaLink
  20. lazy val logger: Logger
    Attributes
    protected
    Definition Classes
    LazyLogging → LoggerHolder
  21. final val loggerName: String
    Attributes
    protected
    Definition Classes
    LoggerHolder
  22. val m2k: M2KConverter[Either[KExpr, NamedSymbol]]
  23. var mathematicaExecutor: ToolExecutor
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  24. def memoryConstrained(cmd: String): String
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  25. def memoryConstrained(cmd: MExpr): MExpr
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  26. var memoryLimit: Long

    Memory limit for Mathematica requests in MB, set to MEMORY_LIMIT_OFF to disable.

    Memory limit for Mathematica requests in MB, set to MEMORY_LIMIT_OFF to disable.

    Definition Classes
    BaseKeYmaeraMathematicaBridge
  27. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  28. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  29. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  30. def run(cmd: MExpr): (String, Either[KExpr, NamedSymbol])

    Runs Mathematica command cmd, with Mathematica exception checking.

    Runs Mathematica command cmd, with Mathematica exception checking.

    Definition Classes
    BaseKeYmaeraMathematicaBridgeKeYmaeraMathematicaBridge
  31. def runUnchecked(cmd: String): (String, Either[KExpr, NamedSymbol])

    Runs Mathematica command cmd without safeguarding by exception checking for Mathematica results.

    Runs Mathematica command cmd without safeguarding by exception checking for Mathematica results.

    Definition Classes
    BaseKeYmaeraMathematicaBridgeKeYmaeraMathematicaBridge
  32. def shutdown(): Unit
  33. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  34. def timeConstrained(cmd: String): String
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  35. def timeConstrained(cmd: MExpr): MExpr
    Attributes
    protected
    Definition Classes
    BaseKeYmaeraMathematicaBridge
  36. var timeout: Int

    Timeout for Mathematica requests in seconds, set to TIMEOUT_OFF to disable.

    Timeout for Mathematica requests in seconds, set to TIMEOUT_OFF to disable.

    Definition Classes
    BaseKeYmaeraMathematicaBridge
  37. def toString(): String
    Definition Classes
    AnyRef → Any
  38. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  39. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  40. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Logging

Inherited from LazyLogging

Inherited from LoggerHolder

Inherited from CounterExampleTool

Inherited from ToolInterface

Inherited from KeYmaeraMathematicaBridge[Either[KExpr, NamedSymbol]]

Inherited from AnyRef

Inherited from Any

Ungrouped