Packages

c

edu.cmu.cs.ls.keymaerax.btactics

TwoThreeTreePolynomialRing

case class TwoThreeTreePolynomialRing(variableOrdering: Ordering[Term], monomialOrdering: Ordering[IndexedSeq[(Term, Int)]]) extends PolynomialRing with Product with Serializable

A polynomial is represented as a set of monomials stored in a 2-3 Tree, the ordering is lexicographic A monomial is represented as a coefficient and a power-product. A coefficient is represented as a pair of BigDecimals for num/denom. A power product is represented densely as a list of exponents

All data-structures maintain a proof of input term = representation of data structure as Term

Representations of data structures (recursively applied on rhs):

  • 3-Node (l, v1, m, v2, r) is "l + v1 + m + v2 + r"
  • 2-Node (l, v, r) is "l + v + r"
  • monomial (c, pp) is "c * pp"
  • coefficient (num, denom) is "num / denom"
  • power product [e1, ..., en] is "x1e1 * ... * xn en", where instead of "x0", we write "1" in order to avoid trouble with 00, i.e., nonzero-assumptions on x or the like

All operations on the representations update the proofs accordingly.

Linear Supertypes
Serializable, Serializable, Product, Equals, PolynomialRing, AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TwoThreeTreePolynomialRing
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. PolynomialRing
  7. AnyRef
  8. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new TwoThreeTreePolynomialRing(variableOrdering: Ordering[Term], monomialOrdering: Ordering[IndexedSeq[(Term, Int)]])

Type Members

  1. trait Polynomial extends AnyRef

    Interface to Polynomials: - a term that keeps track of how the polynomial was constructed - a proof for the internal representation of the polynomial - arithmetic - test for zero

    Interface to Polynomials: - a term that keeps track of how the polynomial was constructed - a proof for the internal representation of the polynomial - arithmetic - test for zero

    Definition Classes
    PolynomialRing
  2. trait PowerProduct extends AnyRef
    Definition Classes
    PolynomialRing
  3. case class Branch2(left: TreePolynomial, value: Monomial, right: TreePolynomial, prvO: Option[ProvableSig]) extends TreePolynomial with Product with Serializable
  4. case class Branch3(left: TreePolynomial, value1: Monomial, mid: TreePolynomial, value2: Monomial, right: TreePolynomial, prvO: Option[ProvableSig]) extends TreePolynomial with Product with Serializable
  5. case class Coefficient(num: BigDecimal, denom: BigDecimal, prvO: Option[ProvableSig] = None) extends Product with Serializable

    prv: lhs = rhs lhs: input term (arbitrary, trace of construction) rhs: Divide(Number(num), Number(denom))

  6. case class Empty(prvO: Option[ProvableSig]) extends TreePolynomial with Product with Serializable
  7. sealed trait Growth extends AnyRef

    2-3 Tree for monomials, keeping track of proofs.

  8. case class Monomial(coeff: Coefficient, powerProduct: SparsePowerProduct, prvO: Option[ProvableSig] = None) extends Product with Serializable

    prv: lhs = rhs lhs: input term (arbitrary, trace of construction) rhs: representation of coeff*powers.map(^)

  9. case class SparsePowerProduct(sparse: Seq[(Term, Int)]) extends PowerProduct with Product with Serializable
  10. case class Sprout(sprout: Branch2) extends Growth with Product with Serializable
  11. case class Stay(p: TreePolynomial) extends Growth with Product with Serializable
  12. sealed trait TreePolynomial extends Polynomial
  13. final case class UnknownPolynomialImplementationException(other: TwoThreeTreePolynomialRing.Polynomial) extends RuntimeException with Product with Serializable

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 Const(num: BigDecimal): TreePolynomial
  5. def Const(num: BigDecimal, denom: BigDecimal): TreePolynomial
  6. lazy val One: TreePolynomial
  7. def Var(term: Term, power: Int): TreePolynomial
  8. def Var(term: Term): TreePolynomial
  9. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  10. lazy val branch2GrowLeft: ProvableSig

    Note

    for the Left case, could actually just use branch2Left

  11. lazy val branch2GrowRight: ProvableSig
  12. lazy val branch2Left: ProvableSig
  13. lazy val branch2Right: ProvableSig
  14. lazy val branch2Value: ProvableSig
  15. lazy val branch3GrowLeft: ProvableSig
  16. lazy val branch3GrowMid: ProvableSig
  17. lazy val branch3GrowRight: ProvableSig
  18. lazy val branch3Left: ProvableSig
  19. lazy val branch3Mid: ProvableSig
  20. lazy val branch3Right: ProvableSig
  21. lazy val branch3Value1: ProvableSig
  22. lazy val branch3Value2: ProvableSig
  23. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  24. lazy val coefficientBigDecimalPrv: ProvableSig
  25. lazy val coefficientNegPrv: ProvableSig
  26. lazy val coefficientPlusPrv: ProvableSig
  27. lazy val coefficientTimesPrv: ProvableSig
  28. val constC: FuncOf
  29. val constCl: FuncOf
  30. val constCr: FuncOf
  31. val constF: UnitFunctional
  32. val constL: FuncOf
  33. val constLd: FuncOf
  34. lazy val constLemma: ProvableSig
  35. val constLn: FuncOf
  36. val constR_: FuncOf
  37. val constRd: FuncOf
  38. val constRn: FuncOf
  39. val constX: UnitFunctional
  40. lazy val divideIdentity: ProvableSig
  41. lazy val divideNeg: ProvableSig
  42. lazy val divideNumber: ProvableSig
  43. lazy val divideRat: ProvableSig
  44. lazy val emptySprout: ProvableSig
  45. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  46. lazy val equalReflexive: ProvableSig
  47. lazy val equalityBySubtraction: ProvableSig
  48. def equate(t1: Term, t2: Term): Option[ProvableSig]
  49. val equate: DependentPositionTactic
  50. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  51. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  52. lazy val identityTimes: ProvableSig
  53. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  54. lazy val minusBranch2: ProvableSig
  55. lazy val minusBranch3: ProvableSig
  56. lazy val minusEmpty: ProvableSig
  57. lazy val monTimesBranch2: ProvableSig
  58. lazy val monTimesBranch3: ProvableSig
  59. lazy val monTimesZero: ProvableSig
  60. val monomialOrdering: Ordering[IndexedSeq[(Term, Int)]]
  61. lazy val monomialTimesLemma: ProvableSig

    l = cl * xls r = cr * xrs c = cl*cr xs = xls ** xrs -> l*r=c*xs

  62. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  63. lazy val negTimes: ProvableSig
  64. lazy val negateBranch2: ProvableSig
  65. lazy val negateBranch3: ProvableSig
  66. lazy val negateEmpty: ProvableSig
  67. def normalize(term: Term): ProvableSig
  68. val normalizeAt: DependentPositionTactic
  69. lazy val normalizeBranch2: ProvableSig
  70. lazy val normalizeBranch3: ProvableSig
  71. lazy val normalizeCoeff0: ProvableSig
  72. lazy val normalizeCoeff1: ProvableSig
  73. lazy val normalizeMonom0: ProvableSig
  74. lazy val normalizeMonomCS: ProvableSig
  75. lazy val normalizeMonomNCS: ProvableSig
  76. lazy val normalizePowers1R: ProvableSig
  77. lazy val normalizePowers1V: ProvableSig
  78. lazy val normalizePowersC1: ProvableSig
  79. lazy val normalizePowersCP: ProvableSig
  80. lazy val normalizePowersCV: ProvableSig
  81. lazy val normalizePowersRP: ProvableSig
  82. lazy val normalizePowersRV: ProvableSig
  83. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  84. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  85. implicit def ofInt(i: Int): Polynomial
    Definition Classes
    PolynomialRing
  86. def ofSparse(powers: (Term, Int)*): SparsePowerProduct
  87. def ofSparse(seq: Seq[(Term, Int)]): SparsePowerProduct
  88. def ofTerm(t: Term): Polynomial
    Definition Classes
    PolynomialRing
  89. lazy val partition2: ProvableSig
  90. lazy val plusBranch2: ProvableSig
  91. lazy val plusBranch3: ProvableSig
  92. lazy val plusEmpty: ProvableSig
  93. lazy val plusMinus: ProvableSig
  94. lazy val plusTimes: ProvableSig
  95. def powerDivideLemma(i: Int): ProvableSig

    lookup or prove lemma of the form "(x_(||) / y_(||))i = x_(||)i / y_(||)^i "

  96. lazy val powerEven: ProvableSig
  97. lazy val powerLemma: ProvableSig
  98. lazy val powerOdd: ProvableSig
  99. lazy val powerOne: ProvableSig
  100. lazy val powerPoly: ProvableSig
  101. lazy val powerZero: ProvableSig
  102. def ratForm(term: Term): (Polynomial, Polynomial, ProvableSig)
  103. lazy val rationalLemma: ProvableSig
  104. def reassoc(prv: ProvableSig): ProvableSig

    drop parentheses of a sum of terms on the rhs of prv to the left, e.g., t = a + (b + c) ~~> t = a + b + c

  105. lazy val reassocLeft0RightConst: ProvableSig
  106. lazy val reassocRight0: ProvableSig
  107. lazy val reassocRightConst: ProvableSig
  108. lazy val reassocRightPlus: ProvableSig
  109. lazy val splitBranch2: ProvableSig
  110. lazy val splitBranch3: ProvableSig
  111. lazy val splitCoefficient: ProvableSig
  112. def splitCoefficientNumericCondition(n: Term, d: Term, n1: Term, d1: Term, n2: Term, d2: Term): And
  113. lazy val splitEmpty: ProvableSig
  114. lazy val splitMonomial: ProvableSig
  115. def symbols(t: Term): Seq[Term]
    Definition Classes
    PolynomialRing
  116. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  117. lazy val timesBranch2: ProvableSig
  118. lazy val timesBranch3: ProvableSig
  119. lazy val timesEmpty: ProvableSig
  120. lazy val timesIdentity: ProvableSig
  121. lazy val timesPowers1Left: ProvableSig
  122. lazy val timesPowers1Right: ProvableSig
  123. lazy val timesPowersBoth: ProvableSig
  124. lazy val timesPowersLeft: ProvableSig
  125. lazy val timesPowersRight: ProvableSig
  126. lazy val varLemma: ProvableSig
  127. lazy val varPowerLemma: ProvableSig
  128. val variableOrdering: Ordering[Term]
  129. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  130. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  131. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  132. lazy val zez: ProvableSig

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from PolynomialRing

Inherited from AnyRef

Inherited from Any

Ungrouped