# ConstantSubst

### Related Docs: object ConstantSubst | package substitutions

#### class ConstantSubst extends SimpleSubstitution

Replace a constant with an arbitrary term

Linear Supertypes
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. ConstantSubst
2. SimpleSubstitution
3. Substitution
4. Sorted
5. Function1
6. AnyRef
7. 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. #### 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. #### def applyToConstant(c: ConstantTerm): Term

Attributes
protected[ap.terfor.substitutions]
Definition Classes
ConstantSubstSimpleSubstitution
18. #### def applyToVariable(v: VariableTerm): Term

Attributes
protected[ap.terfor.substitutions]
Definition Classes
ConstantSubstSimpleSubstitution
19. #### final def asInstanceOf[T0]: T0

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

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@throws( ... )
21. #### def compose(that: ConstantSubst): ConstantSubst

Attributes
protected[ap.terfor.substitutions]
22. #### def compose[A](g: (A) ⇒ TerFor): (A) ⇒ TerFor

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

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

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

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

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

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

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

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

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

Definition Classes
AnyRef
33. #### 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
ConstantSubstSubstitution
34. #### 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
ConstantSubstSubstitution
35. #### 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
36. #### def sortBy(newOrder: TermOrder): ConstantSubst

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

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

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

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )