Packages

o

edu.cmu.cs.ls.keymaerax.btactics

TaylorModelArith

object TaylorModelArith

Taylor model arithmetic

Here, a Taylor model is a data structure maintaining a proof that some term is element of the Taylor model.

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TaylorModelArith
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class TM(elem: Term, poly: PolynomialArithV2.Polynomial, lower: Term, upper: Term, prv: ProvableSig) extends Product with Serializable

    data structure with certifying computations maintains the invariant prv: \exists err.

    data structure with certifying computations maintains the invariant prv: \exists err. elem = poly + err & err \in [lower; upper]

  2. class TemplateLemmas extends TaylorModel

    generic lemmas for evolution of ODE ode with Taylor model approiximations of order order

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. def Exact(elem: PolynomialArithV2.Polynomial, context: IndexedSeq[Formula]): TM

    constructs a Taylor model with zero interval part

  5. def TM(elem: Term, poly: PolynomialArithV2.Polynomial, lower: Term, upper: Term, context: IndexedSeq[Formula], be: BelleExpr): TM

    constructs a Taylor model by proving the required certificate with a tactic

  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  8. def cutEq(prv: ProvableSig, eq: Formula): ProvableSig
  9. def cutSeq(prvs: Seq[ProvableSig], prv: ProvableSig): ProvableSig
  10. def destTaylorModelFormula(fml: Formula): (Term, Term, Term, Term)

    takes a formula encoding a Taylor model and returns (elem, poly, lower, upper)

  11. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  12. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  13. def evalFormula(fml: Formula, context: IndexedSeq[Formula], argumentMap: Map[Term, TM])(implicit options: TaylorModelOptions): Option[ProvableSig]

    try to prove a formula using Taylor model arithmetic

  14. def evalTerm(t: Term, context: IndexedSeq[Formula], argumentMap: Map[Term, TM])(implicit options: TaylorModelOptions): TM

    evaluate a Term in Taylor model arithmetic

  15. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  16. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  17. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  18. def hideAntes(hides: Seq[Int], prv: ProvableSig): ProvableSig
  19. def identityPrecondition(x: Seq[TM], r: Seq[TM], prv: ProvableSig)(implicit options: TaylorModelOptions): (Seq[TM], Seq[TM], ProvableSig)

    x

    lTM(r) ... (left) Taylor model with variables in r r

    returns

    (x1, r1) ... x1 = r + c ... identity part of (lTM o rTM) r1 = rTM'(e, i) ... higher order terms + a fresh variable for symbolic remainders x = r + c r0 = TM(e, i)

  20. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  21. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  22. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  23. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  24. def partition(xs: Seq[TM], newElems: Seq[Term], P: (BigDecimal, BigDecimal, PolynomialArithV2.PowerProduct) ⇒ Boolean)(implicit options: TaylorModelOptions): (Seq[TM], Seq[TM], Seq[Equal])

    partition and weaken a sequence of Taylor models

  25. val refineConjunction: ProvableSig
  26. val refineLe1: ProvableSig
  27. val refineLe2: ProvableSig
  28. def refineTaylorModelFormula(fml: Formula, assms: IndexedSeq[Formula])(implicit options: TaylorModelOptions): (Exists, Exists, ProvableSig, (Term, PolynomialArithV2.Polynomial, Term, Term, ProvableSig))
  29. val refineTmExists: ProvableSig
  30. def subtermOf(t: Term, fml: Formula): Boolean

    t subterm of fml ?

  31. def subtermOf(t: Term, s: Term): Boolean

    t subterm of s ?

  32. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  33. val taylorModelApproxPrv: ProvableSig
  34. val taylorModelCollectPrv: ProvableSig
  35. val taylorModelDivideExactPrv: ProvableSig
  36. val taylorModelEmptyIntervalPrv: ProvableSig
  37. val taylorModelEvalPrv: ProvableSig
  38. val taylorModelExactPrv: ProvableSig
  39. val taylorModelIntervalGe: ProvableSig
  40. val taylorModelIntervalGt: ProvableSig
  41. val taylorModelIntervalLe: ProvableSig
  42. val taylorModelIntervalLt: ProvableSig
  43. val taylorModelIntervalPrv: ProvableSig
  44. val taylorModelMinusPrv: ProvableSig
  45. val taylorModelNegPrv: ProvableSig
  46. val taylorModelPartitionPrv1: ProvableSig
  47. val taylorModelPartitionPrv2: ProvableSig
  48. val taylorModelPlusPrv: ProvableSig

  49. val taylorModelPowerEven: ProvableSig
  50. val taylorModelPowerOdd: ProvableSig
  51. val taylorModelPowerOne: ProvableSig
  52. val taylorModelSquarePrv: ProvableSig
  53. val taylorModelTimesPrv: ProvableSig
  54. val taylorModelTransElem: ProvableSig
  55. def toString(): String
    Definition Classes
    AnyRef → Any
  56. def trimContext(context: Seq[Formula], ts: Seq[Term]): Seq[Formula]

    delete formulas that contain ts from context, written "context \ ts"

  57. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  58. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  59. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped