# SimpleSubstitution

### Related Docs: object SimpleSubstitution | package substitutions

#### abstract class SimpleSubstitution extends Substitution

A substitution that works by simple replacement of constants or variables with arbitrary terms

Linear Supertypes
Known Subclasses
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. SimpleSubstitution
2. Substitution
3. Sorted
4. Function1
5. AnyRef
6. Any
1. Hide All
2. Show all
Visibility
1. Public
2. All

### Abstract Value Members

1. #### abstract def applyToConstant(c: ConstantTerm): Term

Attributes
protected[ap.terfor.substitutions]
2. #### abstract def applyToVariable(v: VariableTerm): Term

Attributes
protected[ap.terfor.substitutions]
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]
Definition Classes
Substitution
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]
Definition Classes
Substitution
5. #### 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()
5. #### final def apply(lc: LinearCombination): LinearCombination

Definition Classes
SimpleSubstitutionSubstitution
6. #### final def apply(t: Term): Term

Simple substitutions work by simple replacement

Simple substitutions work by simple replacement

Definition Classes
SimpleSubstitutionSubstitution
7. #### def apply(conj: PredConj): PredConj

Definition Classes
Substitution
8. #### def apply(a: Atom): Atom

Definition Classes
Substitution
9. #### def apply(conjs: NegatedConjunctions): NegatedConjunctions

Definition Classes
Substitution
10. #### def apply(conj: Conjunction): Conjunction

Definition Classes
Substitution
11. #### def apply(conj: ArithConj): ArithConj

Definition Classes
Substitution
12. #### def apply(conj: InEqConj): InEqConj

Definition Classes
Substitution
13. #### def apply(negConj: NegEquationConj): NegEquationConj

Definition Classes
Substitution
14. #### def apply(conj: EquationConj): EquationConj

Definition Classes
Substitution
15. #### def apply(f: Formula): Formula

Definition Classes
Substitution
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. #### 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
SimpleSubstitutionSubstitution
31. #### final def synchronized[T0](arg0: ⇒ T0): T0

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

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

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )