Packages

c

edu.cmu.cs.ls.keymaerax.tools

Mathematica

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.

Created by smitsch on 4/27/15.

To do

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

Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Mathematica
  2. ToolOperationManagement
  3. PDESolverTool
  4. AlgebraTool
  5. SimplificationTool
  6. EquationSolverTool
  7. DerivativeTool
  8. SimulationTool
  9. CounterExampleTool
  10. ODESolverTool
  11. ToolInterface
  12. InvGenTool
  13. QETool
  14. ToolBase
  15. Tool
  16. AnyRef
  17. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Mathematica()

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. def deriveBy(term: Term, v: Variable): Term

    Computes the symbolic partial derivative of the given term by v.

    Computes the symbolic partial derivative of the given term by v.

    d(term)
    ------
      dv
    term

    The term whose partial derivative is sought.

    v

    The variable to derive by.

    returns

    The partial derivative of term by v.

    Definition Classes
    MathematicaDerivativeTool
  7. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  8. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  9. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  10. def findCounterExample(formula: Formula): Option[Map[NamedSymbol, Expression]]

    Returns a counterexample for the specified formula.

    Returns a counterexample for the specified formula.

    formula

    The formula.

    returns

    A counterexample, if found. None otherwise.

    Definition Classes
    MathematicaCounterExampleTool
  11. def getAvailableWorkers: Int
    Definition Classes
    MathematicaToolOperationManagement
  12. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def getOperationTimeout: Int

    Returns the timeout duration.

    Returns the timeout duration.

    Definition Classes
    MathematicaToolOperationManagement
  14. def groebnerBasis(polynomials: List[Term]): List[Term]

    Computes the Gröbner Basis of the given set of polynomials (with respect to some fixed monomial order).

    Computes the Gröbner Basis of the given set of polynomials (with respect to some fixed monomial order).

    Definition Classes
    MathematicaAlgebraTool
    See also

    polynomialReduce()

  15. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  16. 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
    MathematicaTool
  17. var initialized: Boolean
    Attributes
    protected
    Definition Classes
    ToolBase
  18. def invgen(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): Seq[Either[Seq[Formula], Seq[Formula]]]

    Returns a continuous invariant for a safety problem sent to the tool.

    Returns a continuous invariant for a safety problem sent to the tool.

    ode

    The differential equation for which to generate a continuous invariants.

    assumptions

    Assumptions on the initial state of the ODE.

    postCond

    What to prove from the invariants.

    returns

    A sequence of continuous invariants, each to be proved with a diffcut chain (left=invariant, right=candidate).

    Definition Classes
    MathematicaInvGenTool
  19. def isInitialized: Boolean

    Checks whether this tool has been initialized already.

    Checks whether this tool has been initialized already.

    Definition Classes
    ToolBaseTool
  20. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  21. def lzzCheck(ode: ODESystem, inv: Formula): Boolean

    Fast check whether or not inv is worth proving to be an invariant of ode.

    Fast check whether or not inv is worth proving to be an invariant of ode.

    Definition Classes
    MathematicaInvGenTool
  22. val name: String
    Definition Classes
    ToolBaseTool
  23. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  24. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  25. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  26. def odeSolve(diffSys: DifferentialProgram, diffArg: Variable, iv: Map[Variable, Variable]): Option[Formula]

    Returns a formula describing the symbolic solution of the specified differential equation system.

    Returns a formula describing the symbolic solution of the specified differential equation system.

    diffSys

    The differential equation system

    diffArg

    The independent variable of the ODE, usually time

    iv

    Names of initial values per variable, e.g., x -> x_0

    returns

    The solution, if found. None otherwise.

    Definition Classes
    MathematicaODESolverTool
  27. def pdeSolve(diffSys: DifferentialProgram): Iterator[Term]

    Computes the symbolic solution of the inverse characteristic partial differential equation corresponding to an ordinary differential equation.

    Computes the symbolic solution of the inverse characteristic partial differential equation corresponding to an ordinary differential equation.

    diffSys

    The system of differential equations of the form x'=theta,y'=eta.

    returns

    A list of solutions for f of the inverse characteristic PDE

    theta*df/dx + eta*df/dy = 0

    if found.

    Definition Classes
    MathematicaPDESolverTool
  28. def polynomialReduce(polynomial: Term, GB: List[Term]): (List[Term], Term)

    Computes the multi-variate polynomial reduction of polynomial divided with respect to the set of polynomials GB, which is guaranteed to be unique iff GB is a Gröbner basis.

    Computes the multi-variate polynomial reduction of polynomial divided with respect to the set of polynomials GB, which is guaranteed to be unique iff GB is a Gröbner basis. Returns the list of cofactors and the remainder.

    Definition Classes
    MathematicaAlgebraTool
    See also

    groebnerBasis()

  29. def qeEvidence(formula: Formula): (Formula, Evidence)

    Quantifier elimination on the specified formula, returns an equivalent quantifier-free formula plus Mathematica input/output as evidence

    Quantifier elimination on the specified formula, returns an equivalent quantifier-free formula plus Mathematica input/output as evidence

    formula

    The formula whose quantifier-free equivalent is sought.

    returns

    An equivalent quantifier-free formula, with tool evidence.

    Definition Classes
    MathematicaQETool
  30. def quotientRemainder(term: Term, div: Term, x: Variable): (Term, Term)

    Computes the quotient and remainder of term divided by div.

    Computes the quotient and remainder of term divided by div.

    Definition Classes
    MathematicaAlgebraTool
    Example:
    1. quotientRemainder(6*x^2+4*x+8, 2*x, x) == (3*x+2, 8)
  31. def restart(): Unit

    Restarts the MathKernel with the current configuration

    Restarts the MathKernel with the current configuration

    Definition Classes
    MathematicaTool
  32. 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
    MathematicaToolOperationManagement
  33. def shutdown(): Unit

    Closes the connection to Mathematica

    Closes the connection to Mathematica

    Definition Classes
    MathematicaTool
  34. def simplify(expr: Term, assumptions: List[Formula]): Term
    Definition Classes
    MathematicaSimplificationTool
  35. def simplify(expr: Formula, assumptions: List[Formula]): Formula
    Definition Classes
    MathematicaSimplificationTool
  36. def simplify(expr: Expression, assumptions: List[Formula]): Expression

    Simplifies the given expression expr, under the list of assumptions.

    Simplifies the given expression expr, under the list of assumptions.

    expr

    The formula or term to simplify.

    assumptions

    The list of logical formulas whose conjunction is assumed to hold during the simplification. The assumptions are allowed to contain additional conjunctions.

    returns

    A simplified version of expr.

    Definition Classes
    MathematicaSimplificationTool
    Example:
    1. simplify("a*x^2+b^2 > a*x^3+b*abs(b)".asFormula, "x>1".asFormula :: "b>0".asFormula::Nil) == "a<0".asFormula
      simplify("a*x^2+b^2 > a*x^3+b*abs(b)".asFormula, "x>1 && b>0".asFormula::Nil) == "a<0".asFormula
  37. def simulate(initial: Formula, stateRelation: Formula, steps: Int = 10, n: Int = 1): Simulation

    Returns a list of simulated states, where consecutive states in the list satisfy 'stateRelation'.

    Returns a list of simulated states, where consecutive states in the list satisfy 'stateRelation'. The state relation is a modality-free first-order formula. The simulation starts in a state where initial holds (first-order formula).

    initial

    A first-order formula describing the initial state.

    stateRelation

    A first-order formula describing the relation between consecutive states. The relationship is by name convention: postfix 'pre': prior state; no postfix: posterior state.

    steps

    The length of the simulation run (i.e., number of states).

    n

    The number of simulations (different initial states) to create.

    returns

    'n' lists (length 'steps') of simulated states.

    Definition Classes
    MathematicaSimulationTool
  38. def simulateRun(initial: SimState, stateRelation: Formula, steps: Int = 10): SimRun

    Returns a list of simulated states, where consecutive states in the list satisfy 'stateRelation'.

    Returns a list of simulated states, where consecutive states in the list satisfy 'stateRelation'. The state relation is a modality-free first-order formula. The simulation starts in the specified initial state.

    initial

    The initial state: concrete values .

    stateRelation

    A first-order formula describing the relation between consecutive states. The relationship is by name convention: postfix 'pre': prior state; no postfix: posterior state.

    steps

    The length of the simulation run (i.e., number of states).

    returns

    A list (length 'steps') of simulated states.

    Definition Classes
    MathematicaSimulationTool
  39. def solve(equations: Formula, vars: List[Expression]): Option[Formula]

    Computes the symbolic solution of an equation system.

    Computes the symbolic solution of an equation system.

    equations

    The system of equations as a conjunction of equations.

    vars

    The variables or symbols to solve for. Within reason, it may also be possible to solve for compound expressions like solve for j(z).

    returns

    The solution if found; None otherwise The solution should be a conjunction of explicit equations for the vars. Or a disjunction of a conjunction of explicit equations for the vars.

    Definition Classes
    MathematicaEquationSolverTool
    Example:
    1. solve("z+1=3&x+5=z-1".asFormula, Variable("z")::Variable("x")::Nil) == Some("z=2&x=-4")
  40. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  41. def toString(): String
    Definition Classes
    AnyRef → Any
  42. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  43. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  44. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from ToolOperationManagement

Inherited from PDESolverTool

Inherited from AlgebraTool

Inherited from SimplificationTool

Inherited from EquationSolverTool

Inherited from DerivativeTool

Inherited from SimulationTool

Inherited from CounterExampleTool

Inherited from ODESolverTool

Inherited from ToolInterface

Inherited from InvGenTool

Inherited from QETool

Inherited from ToolBase

Inherited from Tool

Inherited from AnyRef

Inherited from Any

Ungrouped