PseudoConstantSubst

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[ap.terfor.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 is n * v |-> t

Attributes
protected[ap.terfor.substitutions]
Definition Classes
PseudoConstantSubst → PseudoDivSubstitution
final def asInstanceOf[T0]: T0

Definition Classes
Any
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
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: Any): Boolean

Definition Classes
AnyRef → Any
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
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
Substitution → Sorted
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
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
PseudoConstantSubst → Substitution
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
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 lc with arbitrary positive integers to achieve this.

Attributes
protected[ap.terfor.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 result isSortedBy(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( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )

Deprecated Value Members

def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated
(Since version ) see corresponding Javadoc for more information.

Related Docs: object PseudoConstantSubst | package substitutions

class PseudoConstantSubst extends PseudoDivSubstitution

Instance Constructors

new PseudoConstantSubst(coeff: IdealInt, constant: ConstantTerm, replacement: Term, order: TermOrder)

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

def andThen[A](g: (TerFor) ⇒ A): (TerFor) ⇒ A

def apply(lc: LinearCombination): LinearCombination

def apply(t: Term): Term

def apply(conj: PredConj): PredConj

def apply(a: Atom): Atom

def apply(conjs: NegatedConjunctions): NegatedConjunctions

def apply(conj: Conjunction): Conjunction

def apply(conj: ArithConj): ArithConj

def apply(conj: InEqConj): InEqConj

def apply(negConj: NegEquationConj): NegEquationConj

def apply(conj: EquationConj): EquationConj

def apply(f: Formula): Formula

final def apply(t: TerFor): TerFor

def applyToConstant(c: ConstantTerm): (IdealInt, Term)

def applyToVariable(v: VariableTerm): (IdealInt, Term)

final def asInstanceOf[T0]: T0

def clone(): AnyRef

def compose[A](g: (A) ⇒ TerFor): (A) ⇒ TerFor

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

final def getClass(): Class[_]

def hashCode(): Int

final def isInstanceOf[T0]: Boolean

final def isSortedBy(otherOrder: TermOrder): Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

val order: TermOrder

def passQuantifiers(num: Int): Substitution

def pseudoApply(lc: LinearCombination): LinearCombination

def sortBy(newOrder: TermOrder): PseudoConstantSubst

final def synchronized[T0](arg0: ⇒ T0): T0

def toString(): String

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

Deprecated Value Members

def finalize(): Unit

Inherited from PseudoDivSubstitution

Inherited from Substitution

Inherited from Sorted[Substitution]

Inherited from (TerFor) ⇒ TerFor

Inherited from AnyRef

Inherited from Any

Ungrouped