# IdentitySubst

### Related Docs: object IdentitySubst | package substitutions

#### class IdentitySubst extends Substitution

Linear Supertypes
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. IdentitySubst
2. Substitution
3. Sorted
4. Function1
5. AnyRef
6. 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. #### def andThen[A](g: (TerFor) ⇒ A): (TerFor) ⇒ A

Definition Classes
Function1
Annotations
@unspecialized()
5. #### def apply(conj: PredConj): PredConj

Definition Classes
IdentitySubstSubstitution
6. #### def apply(a: Atom): Atom

Definition Classes
IdentitySubstSubstitution
7. #### def apply(conjs: NegatedConjunctions): NegatedConjunctions

Definition Classes
IdentitySubstSubstitution
8. #### def apply(conj: Conjunction): Conjunction

Definition Classes
IdentitySubstSubstitution
9. #### def apply(conj: ArithConj): ArithConj

Definition Classes
IdentitySubstSubstitution
10. #### def apply(conj: InEqConj): InEqConj

Definition Classes
IdentitySubstSubstitution
11. #### def apply(negConj: NegEquationConj): NegEquationConj

Definition Classes
IdentitySubstSubstitution
12. #### def apply(conj: EquationConj): EquationConj

Definition Classes
IdentitySubstSubstitution
13. #### def apply(f: Formula): Formula

Definition Classes
IdentitySubstSubstitution
14. #### def apply(lc: LinearCombination): LinearCombination

Definition Classes
IdentitySubstSubstitution
15. #### def apply(t: Term): Term

Definition Classes
IdentitySubstSubstitution
16. #### final def apply(t: TerFor): TerFor

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

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

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

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

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

Definition Classes
AnyRef → Any
22. #### def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( classOf[java.lang.Throwable] )
23. #### final def getClass(): Class[_]

Definition Classes
AnyRef → Any
24. #### def hashCode(): Int

Definition Classes
AnyRef → Any
25. #### final def isInstanceOf[T0]: Boolean

Definition Classes
Any
26. #### 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
27. #### final def ne(arg0: AnyRef): Boolean

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

Definition Classes
AnyRef
29. #### final def notifyAll(): Unit

Definition Classes
AnyRef
30. #### val 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]
Definition Classes
IdentitySubstSubstitution
31. #### 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]
Definition Classes
IdentitySubstSubstitution
32. #### 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]
Definition Classes
IdentitySubstSubstitution
33. #### def sortBy(newOrder: TermOrder): IdentitySubst

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
IdentitySubstSorted
34. #### final def synchronized[T0](arg0: ⇒ T0): T0

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

Definition Classes
IdentitySubst → Function1 → AnyRef → Any
36. #### final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
37. #### final def wait(arg0: Long, arg1: Int): Unit

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

Definition Classes
AnyRef
Annotations
@throws( ... )