Packages

package qe

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. All

Type Members

  1. abstract class BaseMathematicaCommandRunner extends MathematicaCommandRunner

    Base class for running Mathematica commands synchronously.

  2. case class BinaryMathOpSpec(op: Expr) extends MathematicaOpSpec with Product with Serializable

    Binary Math operators.

  3. case class InterpretedMathOpSpec(op: Expr) extends MathematicaOpSpec with Product with Serializable

    Interpreted functions.

  4. case class JLinkMathematicaCommandRunner(ml: KernelLink) extends BaseMathematicaCommandRunner with Logging with Product with Serializable

    Runs a command using the supplied JLink ml.

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

    Converts KeYmaera X -> Mathematica.

    Converts KeYmaera X -> Mathematica.

    T

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

  6. class KMComparator extends AnyRef

    Compares Mathematica expressions for equality (handles conversion differences, since Mathematica silently converts some expressions, e.g.

    Compares Mathematica expressions for equality (handles conversion differences, since Mathematica silently converts some expressions, e.g. division 2/5 into rational 2/5).

  7. class KeYmaeraToMathematica extends K2MConverter[KExpr]
  8. case class LiteralMathOpSpec(op: Expr) extends MathematicaOpSpec with Product with Serializable

    Math literals.

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

    Converts Mathematica -> KeYmaera X.

    Converts Mathematica -> KeYmaera X.

    T

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

  10. class MKComparator[T] extends AnyRef
  11. trait MathematicaCommandRunner extends AnyRef

    Interface for running and cancelling a Mathematica command.

  12. trait MathematicaOpSpec extends AnyRef

    Mathematica operator notation.

  13. class MathematicaQETool extends QETool

    A QE tool implementation using the provided link to Mathematica/Wolfram Engine.

  14. class MathematicaToKeYmaera extends M2KConverter[KExpr]
  15. case class NameMathOpSpec(k2m: (NamedSymbol, Array[Expr]) ⇒ Expr, applies: (Expr) ⇒ Boolean) extends Product with Serializable

    NamedSymbol operators, with k2m converter

    NamedSymbol operators, with k2m converter 

    (name, args) => Expr

    . (name, args) => Expr }}}

  16. case class NaryMathOpSpec(op: Expr) extends MathematicaOpSpec with Product with Serializable

    Nary Math operators.

  17. case class QuantifiedMathOpSpec(op: Expr) extends MathematicaOpSpec with Product with Serializable

    Quantifier Math operators.

  18. abstract class SMTConverter extends (Formula) ⇒ String

    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.

  19. case class UnaryMathOpSpec(op: Expr) extends MathematicaOpSpec with Product with Serializable

    Unary Math operators.

  20. final class Z3QETool extends Tool with QETool with ToolOperationManagement

    Z3 trusted quantifier elimination tool.

    Z3 trusted quantifier elimination tool.

    See also

    edu.cmu.cs.ls.keymaerax.btactics.Z3ToolProvider to obtain instances of Z3 that are properly initialized and installed/updated. Created by smitsch on 4/27/15.

  21. class Z3Solver extends ToolOperationManagementBase with Logging

    Starts a Z3 process with the binary at z3Path, converting KeYmaera X datastructures to SMT-Lib format with converter.

Value Members

  1. object BigDecimalQETool extends Tool with QETool

    Proves quantifier- and variable-free arithmetic formulas by exact arithmetic evaluation using java.math.BigDecimal.

    Proves quantifier- and variable-free arithmetic formulas by exact arithmetic evaluation using java.math.BigDecimal. Ground term evaluation for formulas with concrete number arithmetic.

    Note

    Java's BigDecimal is clearer and has less indirection than Scala's BigDecimal.

  2. object DefaultSMTConverter extends SMTConverter

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

  3. object ExprFactory

    Creates Expr objects.

  4. object JLinkMathematicaCommandRunner extends Serializable

    JLink command runner companion: keeps track of issued queries.

  5. object KMComparator

    Implicit conversion from Mathematica expressions to comparator.

  6. object KeYmaeraToMathematica extends KeYmaeraToMathematica

    Converts KeYmaeara X expression data structures to Mathematica Expr objects.

  7. object MKComparator

    Implicit conversion from KeYmaera expressions to comparator.

  8. object MathematicaConversion

    Mathematica conversion support to check results for having failed/being aborted, and safely importing Mathematica expressions into KeYmaera X.

    Mathematica conversion support to check results for having failed/being aborted, and safely importing Mathematica expressions into KeYmaera X.

    See also

    M2KConverter for converting Mathematica -> KeYmaera X

    K2MConverter for converting KeYmaera X -> Mathematica

  9. object MathematicaOpSpec

    Mathematica operator specifications with conversions.

  10. object MathematicaToKeYmaera extends MathematicaToKeYmaera

    Converts com.wolfram.jlink.Expr to Expression.

Ungrouped