# Substitution

### Related Docs: object Substitution | package substitutions

#### abstract class Substitution extends (TerFor) ⇒ TerFor with Sorted[Substitution]

A substitution is a mapping from `TerFor` to `TerFor` that replaces variables and constants with arbitrary other terms. It is required that a substitution is only applied to terms/formulas that are sorted according to `order`. There are two more concrete sub-traits: `SimpleSubstitution`, which performs a simple replacement of constants or variables, and `PseudoDivSubstitution`, which can make use of pseudo-division in order to replace expressions `n * c`.

Linear Supertypes
Sorted[Substitution], (TerFor) ⇒ TerFor, AnyRef, Any
Ordering
1. Alphabetic
2. By Inheritance
Inherited
1. Substitution
2. Sorted
3. Function1
4. AnyRef
5. Any
1. Hide All
2. Show All
Visibility
1. Public
2. All

### Abstract Value Members

3. #### abstract def order: TermOrder

The term order that is used for the resulting terms or formulas.

The term order that is used for the resulting terms or formulas. We require that a substitution is only applied to terms/formulas that are already sorted according to this order

Attributes
protected[ap.terfor.substitutions]
4. #### abstract def passQuantifiers(num: Int): Substitution

Substitution that is to be used underneath `num` quantifiers.

Substitution that is to be used underneath `num` quantifiers. Because we use De Bruijn indexes, passing quantifiers shifts the variables in a substitution

Attributes
protected[ap.terfor.substitutions]
5. #### abstract def pseudoApply(lc: LinearCombination): LinearCombination

Some kinds of substitutions can only be applied when pseudo-reduction is allowed to be performed.

Some kinds of substitutions can only be applied when pseudo-reduction is allowed to be performed. Implementations of the following method are allowed to multiply `lc` with arbitrary positive integers to achieve this.

Attributes
protected[ap.terfor.substitutions]
6. #### abstract def sortBy(order: TermOrder): Substitution

Re-sort an object with a new `TermOrder`.

Re-sort an object with a new `TermOrder`. It is guaranteed that the result `isSortedBy(order)`

Definition Classes
Sorted

### Concrete 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 andThen[A](g: (TerFor) ⇒ A): (TerFor) ⇒ A

Definition Classes
Function1
Annotations
@unspecialized()

14. #### final def apply(t: TerFor): TerFor

Definition Classes
Substitution → Function1
15. #### final def asInstanceOf[T0]: T0

Definition Classes
Any
16. #### def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
17. #### def compose[A](g: (A) ⇒ TerFor): (A) ⇒ TerFor

Definition Classes
Function1
Annotations
@unspecialized()
18. #### final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
19. #### def equals(arg0: Any): Boolean

Definition Classes
AnyRef → Any
20. #### final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
21. #### def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
22. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any
23. #### final def isSortedBy(otherOrder: TermOrder): Boolean

Compare the order of this `Substitution` with a given order.

Compare the order of this `Substitution` with a given order. We use equality here, because the behaviour would be quite confusing with the relation `isSubOrderOf` (remember that the substitution has to cope with arbitrary terms/formulas that are sorted by the order)

Definition Classes
SubstitutionSorted
24. #### final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
25. #### final def notify(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
26. #### final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
27. #### final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
28. #### def toString(): String

Definition Classes
Function1 → AnyRef → Any
29. #### final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
30. #### final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
31. #### final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )

### Deprecated Value Members

1. #### def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated