Packages

p

ap

terfor

package terfor

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. Protected

Package Members

  1. package arithconj
  2. package conjunctions
  3. package equations
  4. package inequalities
  5. package linearcombination
  6. package preds
  7. package substitutions

Type Members

  1. trait AliasChecker extends AnyRef

    Trait for classes providing term alias information.

  2. trait ComputationLogger extends AnyRef

    Trait that can be used to track the computation taking place in systems of equations, inequalities, etc.

    Trait that can be used to track the computation taking place in systems of equations, inequalities, etc. This is used to produce proofs.

  3. class ConstantTerm extends Term with Cloneable

    Class for representing constants.

    Class for representing constants. This is not a case class, two constants are the same iff the object that they are represented by are the same.

  4. abstract class Formula extends TerFor
  5. class RichLinearCombination extends AnyRef

    Various infix operators terms and linear combinations

  6. class RichLinearCombinationSeq extends AnyRef

    Various functions to work with vectors of terms

  7. class RichPredicate extends AnyRef

    A few functions to work with predicates

  8. trait Sorted[+T] extends AnyRef

    Trait for objects that can be sorted by a TermOrder.

    Trait for objects that can be sorted by a TermOrder. It is a design decision that the used order cannot be queried from an object (so that it must not be stored in the object). It can be checked whether an object is consistent with a certain given order, however.

  9. trait SortedWithOrder[+T] extends Sorted[T]

    Extension of Sorted where also the actual TermOrder can be queried

  10. abstract class TerFor extends AnyRef
  11. abstract class Term extends TerFor
  12. class TermOrder extends AnyRef
  13. case class VariableTerm(index: Int) extends Term with Product with Serializable

Value Members

  1. object AliasStatus extends Enumeration

    Enumeration to represent whether two terms cannot, may, or must have the same value.

    Enumeration to represent whether two terms cannot, may, or must have the same value. The value CannotDueToFreedom expresses that the free-constant heuristic tells that the terms can be assumed to be different

  2. object ComputationLogger
  3. object Formula
  4. object OneTerm extends Term

    The term representing the literal 1

  5. object TerForConvenience

    Collection of functions that makes it easier to use the term/formula datastructures by adding lots of syntactic sugar

  6. object TermOrder

    Class for representing total orderings on constants (and variables), and their extension to arbitrary terms.

    Class for representing total orderings on constants (and variables), and their extension to arbitrary terms. For the time being, we do not consider arbitrary (non-nullary) functions apart from the pre-defined arithmetic operations.

    constantSeq is the list of constants that are totally ordered by this TermOrder, starting with the biggest constant. In addition, variable terms are by default ordered as bigger as all constants. We use the List datatype for the constant order, so that new large constants can efficiently be added.

  7. object VariableTerm extends Serializable

Ungrouped