class DefaultLemmaGenerator extends java.lang.Object implements LemmaGenerator
Modifier and Type | Field and Description |
---|---|
private java.util.HashMap<SchemaVariable,Term> |
mapping |
Constructor and Description |
---|
DefaultLemmaGenerator() |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
checkForIllegalConditions(Taclet taclet) |
static java.lang.String |
checkForIllegalOps(Term formula,
Taclet owner,
boolean schemaVarsAreAllowed) |
static java.lang.String |
checkTaclet(Taclet taclet) |
private Term[] |
computeArgs(Taclet owner,
ImmutableSet<SchemaVariable> svSet,
TermServices services) |
private Sort[] |
computeArgSorts(ImmutableSet<SchemaVariable> svSet,
TermServices services) |
private Term |
createInstantiation(Taclet owner,
FormulaSV sv,
TermServices services)
Creates the instantiation for a schema variable of type term.
|
private Term |
createInstantiation(Taclet owner,
SchemaVariable sv,
TermServices services) |
private Term |
createInstantiation(Taclet owner,
TermSV sv,
TermServices services)
Creates the instantiation for a schema variable of type term.
|
private Term |
createInstantiation(Taclet owner,
VariableSV sv,
TermServices services)
Creates the instantiation for a schema variable of type variable, i.e
a new logical variable is returned.
|
private Term |
createSimpleInstantiation(Taclet owner,
SchemaVariable sv,
TermServices services)
Since only taclets are supported that contain only FOL-constituents,
there is no need to make it also dependend on program variables.
|
private Name |
createUniqueName(TermServices services,
java.lang.String baseName) |
private Term |
getInstantation(Taclet owner,
VariableSV var,
TermServices services)
Returns the instantiation of
var . |
protected Term |
getInstantiation(Taclet owner,
SchemaVariable var,
TermServices services)
Returns the instantiation for a certain schema variable, i.e. the
skolem term that is used for the instantiation.
|
private Term |
rebuild(Taclet taclet,
Term term,
TermServices services,
java.util.HashSet<QuantifiableVariable> boundedVariables)
Rebuilds a term recursively and replaces all schema variables with
skolem terms/variables.
|
private Term |
replace(Taclet taclet,
Term term,
TermServices services) |
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.
|
TacletFormula |
translate(Taclet taclet,
TermServices services) |
private java.util.HashMap<SchemaVariable,Term> mapping
public TacletFormula translate(Taclet taclet, TermServices services)
translate
in interface LemmaGenerator
private Term replace(Taclet taclet, Term term, TermServices services)
public static java.lang.String checkTaclet(Taclet taclet)
public static java.lang.String checkForIllegalConditions(Taclet taclet)
public static java.lang.String checkForIllegalOps(Term formula, Taclet owner, boolean schemaVarsAreAllowed)
protected final Term getInstantiation(Taclet owner, SchemaVariable var, TermServices services)
owner
- The taclet the schema variable belongs to.var
- The variable to be instantiated.services
- var
.private Term getInstantation(Taclet owner, VariableSV var, TermServices services)
var
. In the case that an
instantiation does not exist it is created.owner
- var
- services
- private Term createInstantiation(Taclet owner, SchemaVariable sv, TermServices services)
private Term createInstantiation(Taclet owner, VariableSV sv, TermServices services)
owner
- the taclet the schema variable belongs to.sv
- the schema variable to be instantiated.services
- some information about the proof currently considered.private Term createInstantiation(Taclet owner, TermSV sv, TermServices services)
sv
.private Term createInstantiation(Taclet owner, FormulaSV sv, TermServices services)
sv
.private Term createSimpleInstantiation(Taclet owner, SchemaVariable sv, TermServices services)
private Name createUniqueName(TermServices services, java.lang.String baseName)
private Sort[] computeArgSorts(ImmutableSet<SchemaVariable> svSet, TermServices services)
private Term[] computeArgs(Taclet owner, ImmutableSet<SchemaVariable> svSet, TermServices services)
private Term rebuild(Taclet taclet, Term term, TermServices services, java.util.HashSet<QuantifiableVariable> boundedVariables)
protected Operator replaceOp(Operator op, TermServices services)
By default, this method returns the argument op.
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.
sort
- the sort to be replaced, not null
services
- A services object for lookupsnull