c

# 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

Linear Supertypes
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])
Definition Classes
MathematicaSimplificationTool
36. def simplify(expr: Expression, assumptions: List[Formula])

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)

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)

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( ... )