ComposeSubsts

Related Docs: object ComposeSubsts | package substitutions

class ComposeSubsts extends Substitution

Function composition for two substitutions

Linear Supertypes
Ordering
1. Alphabetic
2. By inheritance
Inherited
1. ComposeSubsts
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(lc: LinearCombination): LinearCombination

Definition Classes
ComposeSubstsSubstitution
6. def apply(t: Term): Term

For composition, we simply first apply the first substitution and then the second

For composition, we simply first apply the first substitution and then the second

Definition Classes
ComposeSubstsSubstitution
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. 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
ComposeSubstsSubstitution
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
ComposeSubstsSubstitution
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.

Definition Classes
ComposeSubstsSubstitution
33. def sortBy(newOrder: TermOrder): ComposeSubsts

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

Definition Classes
AnyRef
35. def toString(): String

Definition Classes
ComposeSubsts → 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( ... )