class VariableSubst extends SimpleSubstitution
Substitute the variable starting from index offset with the
terms in replacements. I.e., VariableTerm(offset)
is going to be replaced with replacements(0), etc. All other
variables above offset+replacements.size are shifted downwards
by replacements.size
- Alphabetic
- By Inheritance
- VariableSubst
- SimpleSubstitution
- Substitution
- Sorted
- Function1
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- def andThen[A](g: (TerFor) => A): (TerFor) => A
- Definition Classes
- Function1
- Annotations
- @unspecialized()
- final def apply(lc: LinearCombination): LinearCombination
- Definition Classes
- SimpleSubstitution → Substitution
- final def apply(t: Term): Term
Simple substitutions work by simple replacement
Simple substitutions work by simple replacement
- Definition Classes
- SimpleSubstitution → Substitution
- def apply(conj: PredConj): PredConj
- Definition Classes
- Substitution
- def apply(a: Atom): Atom
- Definition Classes
- Substitution
- def apply(conjs: NegatedConjunctions): NegatedConjunctions
- Definition Classes
- Substitution
- def apply(conj: Conjunction): Conjunction
- Definition Classes
- Substitution
- def apply(conj: ArithConj): ArithConj
- Definition Classes
- Substitution
- def apply(conj: InEqConj): InEqConj
- Definition Classes
- Substitution
- def apply(negConj: NegEquationConj): NegEquationConj
- Definition Classes
- Substitution
- def apply(conj: EquationConj): EquationConj
- Definition Classes
- Substitution
- def apply(f: Formula): Formula
- Definition Classes
- Substitution
- final def apply(t: TerFor): TerFor
- Definition Classes
- Substitution → Function1
- def applyToConstant(c: ConstantTerm): Term
- Attributes
- protected[substitutions]
- Definition Classes
- VariableSubst → SimpleSubstitution
- def applyToVariable(v: VariableTerm): Term
- Attributes
- protected[substitutions]
- Definition Classes
- VariableSubst → SimpleSubstitution
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- def compose[A](g: (A) => TerFor): (A) => TerFor
- Definition Classes
- Function1
- Annotations
- @unspecialized()
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def isSortedBy(otherOrder: TermOrder): Boolean
Compare the order of this
Substitutionwith a given order.Compare the order of this
Substitutionwith a given order. We use equality here, because the behaviour would be quite confusing with the relationisSubOrderOf(remember that the substitution has to cope with arbitrary terms/formulas that are sorted by the order)- Definition Classes
- Substitution → Sorted
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- 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[substitutions]
- Definition Classes
- VariableSubst → Substitution
- def passQuantifiers(num: Int): Substitution
Substitution that is to be used underneath
numquantifiers.Substitution that is to be used underneath
numquantifiers. Because we use De Bruijn indexes, passing quantifiers shifts the variables in a substitution- Attributes
- protected[substitutions]
- Definition Classes
- VariableSubst → Substitution
- 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
lcwith arbitrary positive integers to achieve this.- Attributes
- protected[substitutions]
- Definition Classes
- SimpleSubstitution → Substitution
- def sortBy(newOrder: TermOrder): VariableSubst
Re-sort an object with a new
TermOrder.Re-sort an object with a new
TermOrder. It is guaranteed that the resultisSortedBy(order)- Definition Classes
- VariableSubst → Sorted
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- VariableSubst → Function1 → AnyRef → Any
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)