Packages

object SimplifierV2

Created by yongkiat on 9/29/16.

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

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. lazy val Fand: ProvableSig
  5. lazy val Fequiv: ProvableSig
  6. lazy val Fimply: ProvableSig
  7. lazy val For: ProvableSig
  8. lazy val Tand: ProvableSig
  9. lazy val Tequiv: ProvableSig
  10. lazy val Timply: ProvableSig
  11. lazy val Tor: ProvableSig
  12. def addContext(f: Formula, ctx: IndexedSeq[Formula]): (IndexedSeq[Formula], BelleExpr)
  13. lazy val andF: ProvableSig
  14. lazy val andT: ProvableSig
  15. lazy val arithProps: List[(Term, ProvableSig)]
  16. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  17. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  18. def closeHeuristics(ctx: IndexedSeq[Formula], f: Formula, flip: Boolean = true): Option[ProvableSig]
  19. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  20. lazy val eqGtFalse: ProvableSig
  21. lazy val eqLtFalse: ProvableSig
  22. lazy val eqNeqFalse: ProvableSig
  23. lazy val equalReflex: ProvableSig
  24. def equalityRewrites(t: Term, ctx: IndexedSeq[Formula]): ProvableSig

    Takes a term t, with an equality context ctx and returns ctx |- t = t' using all equalities of the shape t = n:Number This is probably hopelessly slow...

  25. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  26. lazy val equivF: ProvableSig
  27. lazy val equivT: ProvableSig
  28. lazy val existsFalse: ProvableSig
  29. lazy val existsTrue: ProvableSig
  30. lazy val falseReflex: ProvableSig
  31. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  32. def flattenPlus(t: Term): (Term, BigDecimal)
  33. def flattenTimes(t: Term): (Term, BigDecimal)
  34. def flip[A1, A2, B](f: (A1, A2) ⇒ B): (A2, A1) ⇒ B
  35. lazy val forallFalse: ProvableSig
  36. lazy val forallTrue: ProvableSig
  37. def formulaSimp(f: Formula, ctx: IndexedSeq[Formula] = IndexedSeq()): (Formula, ProvableSig)

    Recursive formula simplification under a context using chase, proving ctx |- f <-> f' The recursion always occurs left-to-right

    Recursive formula simplification under a context using chase, proving ctx |- f <-> f' The recursion always occurs left-to-right

    f

    formula to simplify

    ctx

    context in which to simplify

    returns

    f',pr where pr proves the equivalence

  38. lazy val fullSimpTac: DependentTactic
  39. lazy val geEqTrue: ProvableSig
  40. lazy val geGtTrue: ProvableSig
  41. lazy val geLtFalse: ProvableSig
  42. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  43. lazy val greaterequalReflex: ProvableSig
  44. def groundTermEval(t: Term): Option[(Term, ProvableSig)]
  45. lazy val gtEqFalse: ProvableSig
  46. lazy val gtLeFalse: ProvableSig
  47. lazy val gtLtFalse: ProvableSig
  48. lazy val gtNotReflex: ProvableSig
  49. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  50. lazy val implyF: ProvableSig
  51. lazy val implyT: ProvableSig
  52. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  53. def isNop(p: Program): Boolean
  54. lazy val leEqTrue: ProvableSig
  55. lazy val leGtFalse: ProvableSig
  56. lazy val leLtTrue: ProvableSig
  57. lazy val lessequalReflex: ProvableSig
  58. lazy val ltEqFalse: ProvableSig
  59. lazy val ltGeFalse: ProvableSig
  60. lazy val ltGtFalse: ProvableSig
  61. lazy val ltNotReflex: ProvableSig
  62. def mksubst(s: TactixLibrary.Subst): TactixLibrary.Subst
  63. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  64. lazy val neEqFalse: ProvableSig
  65. lazy val neGtTrue: ProvableSig
  66. lazy val neLtTrue: ProvableSig
  67. lazy val neqNotReflex: ProvableSig
  68. lazy val neqSym: ProvableSig
  69. lazy val notF: ProvableSig
  70. lazy val notT: ProvableSig
  71. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  72. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  73. lazy val orF: ProvableSig
  74. lazy val orT: ProvableSig
  75. def qeHeuristics(eq: ProvableSig): Option[ProvableSig]
  76. def reassoc(t: Term): ProvableSig
  77. def rewriteLoopAux(f: Formula, targets: List[Variable]): (Formula, ProvableSig)
  78. def rewriteProgramAux(p: Program, targets: List[Variable], rewrites: Map[Variable, Term] = Map()): (Program, Map[Variable, Term])
  79. def rsimpTac(ipos: IndexedSeq[Integer]): DependentPositionTactic
  80. lazy val safeFullSimpTac: DependentPositionTactic
  81. def search(ctx: IndexedSeq[Formula], f: Formula, g: Formula, h: Formula, lem: ProvableSig): Option[ProvableSig]
  82. lazy val simpTac: DependentPositionTactic
  83. def splitEquiv(pr: ProvableSig): (ProvableSig, ProvableSig)
  84. def stripNoOp(p: Program): Program
  85. lazy val swapImply: ProvableSig
  86. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  87. def termSimp(t: Term): (Term, ProvableSig)

    Recursive term simplification using chase, proving |- t = t'

    Recursive term simplification using chase, proving |- t = t'

    t

    The term to be simplifed

  88. def termSimpWithRewrite(t: Term, ctx: IndexedSeq[Formula]): (Term, ProvableSig)
  89. def toString(): String
    Definition Classes
    AnyRef → Any
  90. lazy val trueReflex: ProvableSig
  91. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  92. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  93. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped