class PseudoConstantSubst extends PseudoDivSubstitution
Replace a constant with an arbitrary term
- Alphabetic
- By Inheritance
- PseudoConstantSubst
- PseudoDivSubstitution
- Substitution
- Sorted
- Function1
- AnyRef
- Any
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new PseudoConstantSubst(coeff: IdealInt, constant: ConstantTerm, replacement: Term, order: TermOrder)
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()
- def apply(lc: LinearCombination): LinearCombination
- Definition Classes
- PseudoDivSubstitution → Substitution
- 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
- PseudoDivSubstitution → 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): (IdealInt, Term)
- Attributes
- protected[substitutions]
- Definition Classes
- PseudoConstantSubst → PseudoDivSubstitution
- 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 isn * v |-> t- Attributes
- protected[substitutions]
- Definition Classes
- PseudoConstantSubst → PseudoDivSubstitution
- 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
- PseudoConstantSubst → 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
- PseudoConstantSubst → 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
- PseudoDivSubstitution → Substitution
- 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 resultisSortedBy(order)- Definition Classes
- PseudoConstantSubst → Sorted
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toString(): String
- Definition Classes
- PseudoConstantSubst → 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)