Packages

class Mathematica extends Tool with QETacticTool with InvGenTool with ODESolverTool with CounterExampleTool with SimulationTool with DerivativeTool with EquationSolverTool with SimplificationTool with AlgebraTool with PDESolverTool with SOSsolveTool with LyapunovSolverTool with ToolOperationManagement

Mathematica/Wolfram Engine tool for quantifier elimination and solving differential equations.

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. LyapunovSolverTool
  4. SOSsolveTool
  5. PDESolverTool
  6. AlgebraTool
  7. SimplificationTool
  8. EquationSolverTool
  9. DerivativeTool
  10. SimulationTool
  11. CounterExampleTool
  12. ODESolverTool
  13. ToolInterface
  14. InvGenTool
  15. QETacticTool
  16. Tool
  17. AnyRef
  18. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new Mathematica(link: MathematicaLink, name: String)

    link

    How to connect to the tool, either JLink or WolframScript. Created by smitsch on 4/27/15.

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 cancel(): Boolean

    Cancels the current tool operation and returns true on success, false otherwise.

    Cancels the current tool operation and returns true on success, false otherwise.

    Definition Classes
    MathematicaTool
  6. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  7. 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
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  10. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  11. 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
  12. def genCLF(sys: List[ODESystem]): Option[Term]

    Computes a Common Lyapunov Function for the switched system sys.

    Computes a Common Lyapunov Function for the switched system sys.

    Definition Classes
    MathematicaLyapunovSolverTool
  13. def genMLF(sys: List[ODESystem], trans: List[(Int, Int, Formula)]): List[Term]

    Computes a Lyapunov function for the switched system sys.

    Computes a Lyapunov function for the switched system sys.

    Definition Classes
    MathematicaLyapunovSolverTool
  14. def genODECond(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): (List[Formula], List[Formula])

    Returns the sufficient/necessary condition for postCond to be invariant (left of pair) also returns necessary conditions for the safety question to be true at all with those assumptions (right of pair) In either case, all formulas in the returned list must be valid

    Returns the sufficient/necessary condition for postCond to be invariant (left of pair) also returns necessary conditions for the safety question to be true at all with those assumptions (right of pair) In either case, all formulas in the returned list must be valid

    Definition Classes
    MathematicaInvGenTool
  15. def getAvailableWorkers: Int

    <invalid inheritdoc annotation>

    <invalid inheritdoc annotation>

    Definition Classes
    MathematicaToolOperationManagement
  16. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  17. def getOperationTimeout: Int

    Returns the timeout duration.

    Returns the timeout duration.

    Definition Classes
    MathematicaToolOperationManagement
  18. 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). Gröbner Bases can be made unique for the fixed monomial order, when reduced, modulo scaling by constants.

    returns

    The Gröbner Basis of polynomials. The Gröbner Basis spans the same ideal as polynomials but has unique remainders of polynomialReduce.

    Definition Classes
    MathematicaAlgebraTool
    See also

    polynomialReduce()

    https://lfcps.org/orbital/Orbital-doc/api/orbital/math/AlgebraicAlgorithms.html#groebnerBasis(java.util.Set,%20java.util.Comparator)

  19. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  20. 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
  21. def invgen(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): Seq[Either[Seq[(Formula, String)], Seq[(Formula, String)]]]

    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
  22. def isInitialized: Boolean

    Checks whether this tool has been initialized already.

    Checks whether this tool has been initialized already.

    Definition Classes
    MathematicaTool
  23. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  24. 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
  25. val name: String

    Returns the name of the tool.

    Returns the name of the tool.

    Definition Classes
    MathematicaTool
  26. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  27. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  28. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  29. 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
  30. 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
  31. def polynomialReduce(polynomial: Term, GB: List[Term]): (List[Term], Term)

    Computes the multivariate 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 multivariate 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. Repeatedly divides the leading term of polynomial by a corresponding multiple of a polynomial of GB while possible. Each individual reduction divides the leading term of polynomial by the required multiple of the leading term of the polynomial of GB such that those cancel. Let l(p) be the leading monomial of p and lc(p) its leading coefficient. Then each round of reduction of p:=polynomial with leading term l*X^v picks a polynomial g in GB and turns it into

    p := p - l/lc(g) * X^v/l(g) * g

    alias

    p := p - (l/(lc(g) * l(g)))*X^v  * g

    The former leading monomial X^v no longer occurs in the resulting polynomial and p got smaller or is now 0. To determine leading terms, polynomial reduction uses the same fixed monomial order that groeberBasis() uses. The remainders will be unique (independent of the order of divisions) iff GB is a Gröbner Basis.

    polynomial

    the multivariate polynomial to divide by the elements of GB until saturation.

    GB

    the set of multivariate polynomials that polynomial will repeatedly be divided by. The result of this algorithm is particularly insightful (and has unique remainders) if GB is a Gröbner Basis.

    returns

    (coeff, rem) where rem is the result of multivariate polynomial division of polynomial by GB and coeff are the respective coefficients of the polynomials in GB that explain the result. That is

    polynomial == coeff(1)*GB(1) + coeff(2)*GB(2) + ... + coeff(n)*GB(n) + rem

    alias

    rem == polynomial - coeff(1)*GB(1) - coeff(2)*GB(2) - ... - coeff(n)*GB(n)

    In addition, the remainder rem is small in that its leading monomial cannot be divided by leading monomials of any polynomial in GB. The result rem is unique when GB is a Gröbner Basis.

    Definition Classes
    MathematicaAlgebraTool
    Example:
    1. polynomialReduce("y^3 + 2*x^2*y".asTerm, List("x^2-y".asTerm, "y^2+5".asTerm)) = ((2*y :: 2 + y), -5*y-10)
      // because y^3 + 2*x^2*y == (2*y) * (x^2-y) + (2+y) * (y^2+5) + (-5*y-10)
    See also

    groebnerBasis()

  32. def qe(goal: Goal, continueOnFalse: Boolean): (Goal, Formula)

    Returns the result of the first-to-finish (sub-)goal in g (result of the first-to-finish sub-goal of OneOf, else result of Atom or AllOf).

    Returns the result of the first-to-finish (sub-)goal in g (result of the first-to-finish sub-goal of OneOf, else result of Atom or AllOf). When continueOnFalse is set, continues trying other options in case a finished option's result is false.

    Definition Classes
    MathematicaQETacticTool
  33. def qe(formula: Formula): Lemma

    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

    A lemma showing equivalence between formula and a quantifier-free formula, with tool evidence.

    Definition Classes
    MathematicaQETacticTool
  34. 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.

    term

    the polynomial term to divide, considered as a univariate polynomial in variable v with coefficients that may have other variables.

    div

    the polynomial term to divide term by, considered as a univariate polynomial in variable v with coefficients that may have other variables.

    Definition Classes
    MathematicaAlgebraTool
    Example:
    1. quotientRemainder("6*x^2+4*x+8".asTerm, "2*x".asTerm, Variable("x")) == (3*x+2, 8)
      // because (6*x^2+4*x+8) == (3*x+2) * (2*x) + 8
      // so the result of division is 3*x+2 with remainder 8
  35. def refuteODE(ode: ODESystem, assumptions: Seq[Formula], postCond: Formula): Option[Map[NamedSymbol, Expression]]

    Finds counterexamples to an ODE safety conjecture.

    Finds counterexamples to an ODE safety conjecture.

    Definition Classes
    MathematicaInvGenTool
  36. def restart(): Unit

    Restarts the MathKernel with the current configuration

    Restarts the MathKernel with the current configuration

    Definition Classes
    MathematicaTool
  37. 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
  38. def shutdown(): Unit

    Closes the connection to Mathematica

    Closes the connection to Mathematica

    Definition Classes
    MathematicaTool
  39. def simplify(expr: Term, assumptions: List[Formula]): Term
    Definition Classes
    MathematicaSimplificationTool
  40. def simplify(expr: Formula, assumptions: List[Formula]): Formula
    Definition Classes
    MathematicaSimplificationTool
  41. 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
  42. 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
  43. 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
  44. def solve(equations: Formula, vars: List[Expression]): Option[Formula]

    Computes the symbolic solution of an equation system written as a conjunction of equations.

    Computes the symbolic solution of an equation system written as a conjunction of equations.

    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")
  45. def sosSolve(polynomials: List[Term], variables: List[Term], degree: Int, timeout: Option[Int]): Result

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

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

    returns

    (1 + sos, cofactors) such that (cofactors, polynomials).zipped.map(Times) = 1 + sos.

    Definition Classes
    MathematicaSOSsolveTool
  46. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  47. def toString(): String
    Definition Classes
    AnyRef → Any
  48. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  49. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  50. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from ToolOperationManagement

Inherited from LyapunovSolverTool

Inherited from SOSsolveTool

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 QETacticTool

Inherited from Tool

Inherited from AnyRef

Inherited from Any

Ungrouped