Function composition for two substitutions
Replace a constant with an arbitrary term
Replace a constant with an arbitrary term
Trait for substitutions that can also replace constants or variables with
coefficient, like n * c
.
A substitution that works by simple replacement of constants or variables with arbitrary terms
A substitution is a mapping from TerFor
to TerFor
that replaces variables and constants with arbitrary other terms.
A substitution is a mapping from TerFor
to TerFor
that replaces variables and constants with arbitrary other terms. It is
required that a substitution is only applied to terms/formulas that are
sorted according to order
. There are two more concrete
sub-traits: SimpleSubstitution
, which performs a simple
replacement of constants or variables, and PseudoDivSubstitution
,
which can make use of pseudo-division in order to replace expressions
n * c
.
Substitution for renaming variables.
Substitution for renaming variables. The arguments of the substitution
is a pair (List[Int], Int)
that describes how each
variable should be shifted: (List(0, 2, -1), 1)
specifies that
variable 0 stays the same, variable 1 is increased by 2 (renamed to 3),
variable 2 is renamed to 1, and all other variables n are renamed to n+1.
Substitute the variable starting from index offset
with the
terms in replacements
.
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
Trait for substitutions that can also replace constants or variables with coefficient, like
n * c
. This is done through pseudo-division if necessary (and possible)