# PseudoConstantSubst

### Related Docs: object PseudoConstantSubst | package substitutions

#### class PseudoConstantSubst extends PseudoDivSubstitution

Replace a constant with an arbitrary term

Linear Supertypes
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. PseudoConstantSubst
2. PseudoDivSubstitution
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. #### def apply(lc: LinearCombination): LinearCombination

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

Application to terms is not supported, because it would not be possible to do pseudo-division

Application to terms is not supported, because it would not be possible to do pseudo-division

Definition Classes
PseudoDivSubstitutionSubstitution
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): (IdealInt, Term)

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

The subclasses can specify both the coefficient of the variable or constant that is supposed to be replaced and the actual replacement.

The subclasses can specify both the coefficient of the variable or constant that is supposed to be replaced and the actual replacement. I.e., for `applyToVariable(v)==(n, t)` the described substitution is ` n * v |-> t `

Attributes
protected[ap.terfor.substitutions]
Definition Classes
PseudoConstantSubstPseudoDivSubstitution
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[A](g: (A) ⇒ TerFor): (A) ⇒ TerFor

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

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

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

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

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

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

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

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

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

Definition Classes
AnyRef
32. #### 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
PseudoConstantSubstSubstitution
33. #### 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
PseudoConstantSubstSubstitution
34. #### 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
PseudoDivSubstitutionSubstitution
35. #### def sortBy(newOrder: TermOrder): PseudoConstantSubst

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

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

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

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

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

Definition Classes
AnyRef
Annotations
@throws( ... )