public class GenericRemovingLemmaGenerator extends DefaultLemmaGenerator
GenericSort
s are replaced to equally named ProxySort
s.
This is done since the resulting term is to be used as a proof obligation in which generic sorts must not appear; proxy sorts, however, may. For every generic sort, precisely one proxy sort is introduced.
Modifier and Type | Field and Description |
---|---|
private java.util.Map<Sort,Sort> |
sortMap
The map from generic sorts to proxy sorts.
|
Constructor and Description |
---|
GenericRemovingLemmaGenerator() |
Modifier and Type | Method and Description |
---|---|
protected Operator |
replaceOp(Operator op,
TermServices services)
Sometimes operators must be replaced during lemma generation.
|
protected Sort |
replaceSort(Sort sort,
TermServices services)
Sometimes sorts must be replaced during lemma generation.
|
private ImmutableSet<Sort> |
replaceSorts(ImmutableSet<Sort> extendsSorts,
TermServices services)
Replace sorts.
|
checkForIllegalConditions, checkForIllegalOps, checkTaclet, getInstantiation, translate
protected Operator replaceOp(Operator op, TermServices services)
By default, this method returns the argument op.
The generic removing implementation replaces sort depending functions if their sort argument is a generic sort.
replaceOp
in class DefaultLemmaGenerator
op
- the operator to be replaced, not null
services
- A services object for lookupsnull
protected Sort replaceSort(Sort sort, TermServices services)
By default, this method returns the argument sort.
The generic removing implementation replaces generic sorts by equally named proxy sorts.
replaceSort
in class DefaultLemmaGenerator
sort
- the sort to be replaced, not null
services
- A services object for lookupsnull
private ImmutableSet<Sort> replaceSorts(ImmutableSet<Sort> extendsSorts, TermServices services)
extendsSorts
- the extends sortsservices
- the services