Packages

object TreeForm

Represent terms as recursive lists of logical symbols. This simplified structure is useful for certain analyses that treat all the operators in a relatively uniform way. This representation flattens the term's structure as much as possible (e.g. turning a+(b+c) into (a+b+c)), to make analyses that consider the depth of a term more meaningful. Created by bbohrer on 10/23/15.

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

Type Members

  1. final case class Constant(value: Number) extends TermSymbol with Product with Serializable
  2. class DepthKBOrdering extends Ordering[Term]

    Variant of Knuth-Bendix ordering where the weight of every occurrence of a symbol is multiplied by its depth in the formula, which has the affect of penalizing values at the leaves of a term.

  3. final case class DiffVar(name: String) extends TermSymbol with Product with Serializable
  4. final case class Func(name: String) extends TermSymbol with Product with Serializable
  5. class GenericKBOrdering extends Ordering[Term]

    Generalization of Knuth-Bendix ordering that allows arbitrary comparisons on the Stat's computed for the terms and tweaking the depth/size by replacing each depth with depthFactor(depth) and each size with sizeFactor(size)

  6. class KnuthBendixOrdering extends Ordering[Term]

    Knuth-Bendix orderings assign a constant weight to each symbol and then weigh the terms based on the sum of all the symbols within and compare by the weight.

    Knuth-Bendix orderings assign a constant weight to each symbol and then weigh the terms based on the sum of all the symbols within and compare by the weight. Weights for operators without an arity specified apply to all arities for that operator.

    See also

    Knuth, D. E., Bendix, P. B.Simple word problems in universal algebras.

  7. class LexicographicOrdering extends Ordering[Term]

    General lexicographic ordering: given a list of orderings, tries each ordering in turn until some ordering declares the terms to be unequal.

    General lexicographic ordering: given a list of orderings, tries each ordering in turn until some ordering declares the terms to be unequal. For performance reasons, it may be preferable to reimplement this logic for each lexicographic ordering of interest, but this class is useful for quickly writing experiments.

  8. class LexicographicSymbolOrdering extends Ordering[Term]

    Given a list of symbols, and two terms x and y, a LexicographicSymbolOrdering counts the number of occurrences of each symbol in x and y, and considers x > y if x has more occurrences of the first symbol for which they differ.

  9. type Multiset[A] = Set[(A, Int)]
  10. final case class Operator(name: String, arity: Option[Int]) extends TermSymbol with Product with Serializable
  11. class RecursivePathOrdering extends Ordering[Term]

    Recursive path orderings are one general way to extend orderings on logical symbols to orderings on terms.

    Recursive path orderings are one general way to extend orderings on logical symbols to orderings on terms. They obey some of the intuition one might want from a term ordering. For example, if the most complex symbol in t1 is more complex than the most complex symbol of t2, then t1 > t2.

    See also

    Nachum Dershowitz. Orderings for Term-Rewriting Systems. Theoretical Computer Science, 1982.

  12. class SizeKBOrdering extends Ordering[Term]

    Variant of Knuth-Bendix ordering where the weight of every occurrence of a symbol is multiplied by the size of the subterm starting at that symbol.

    Variant of Knuth-Bendix ordering where the weight of every occurrence of a symbol is multiplied by the size of the subterm starting at that symbol. This has the effect of penalizing large terms over small terms with the same root symbol.

  13. case class Stat(count: Int, depthWeighted: Int, sizeWeighted: Int) extends Product with Serializable
  14. class StatOrdering extends Ordering[Term]
  15. case class Stats(t: Term, depthFactor: (Int) ⇒ Int = {case i => 1}, sizeFactor: (Int) ⇒ Int = {case i => 1}) extends Product with Serializable

    A Stats accumulates data about a term that can be used to implement a variety of useful orderings.

  16. sealed trait TermSymbol extends AnyRef
  17. final case class Tree(sym: TermSymbol, args: List[Tree]) extends Product with Serializable
  18. final case class Var(name: String) extends TermSymbol 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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  6. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  7. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  8. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  9. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  10. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  11. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  12. def multiset[A](l: List[A]): Multiset[A]
  13. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  14. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  15. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  16. def subtract[A](x: Multiset[A], y: Multiset[A]): Multiset[A]
  17. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  18. def toSet[A](x: Multiset[A]): Set[A]
  19. def toString(): String
    Definition Classes
    AnyRef → Any
  20. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  21. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  22. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  23. def weightOrdering(f: (Stats) ⇒ Int): Ordering[Term]
  24. object Stat extends Serializable
  25. object Tree extends Serializable

Inherited from AnyRef

Inherited from Any

Ungrouped