class Instantiation
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ImmutableSet<Term> |
assumedLiterals
Literals occurring in the sequent at hand.
|
private QuantifiableVariable |
firstVar
universally quantifiable variable bound in
allTerm |
private java.util.Map<Term,java.lang.Long> |
instancesWithCosts
HashMap from instance(
Term ) to cost Long |
private static Term |
lastQuantifiedFormula |
private static Instantiation |
lastResult |
private static Sequent |
lastSequent |
private Term |
matrix |
private TriggersSet |
triggersSet
the
TriggersSet of this allTerm |
Modifier | Constructor and Description |
---|---|
private |
Instantiation(Term allterm,
Sequent seq,
Services services) |
Modifier and Type | Method and Description |
---|---|
private void |
addArbitraryInstance(Services services) |
private void |
addInstance(Substitution sub,
long cost)
add instance of
var in sub with
cost to instancesCostCache if this instance is
exist, compare thire cost and store the less one. |
private void |
addInstance(Substitution sub,
Services services) |
private void |
addInstances(ImmutableSet<Term> terms,
Services services) |
(package private) static RuleAppCost |
computeCost(Term inst,
Term form,
Sequent seq,
Services services)
Try to find the cost of an instance(inst) according its quantified
formula and current goal.
|
private RuleAppCost |
computeCostHelp(Term inst) |
(package private) static Instantiation |
create(Term qf,
Sequent seq,
Services services) |
private Term |
createArbitraryInstantiation(QuantifiableVariable var,
TermServices services) |
private Term |
getMatrix() |
(package private) ImmutableSet<Term> |
getSubstitution()
get all instances from instancesCostCache subsCache
|
private ImmutableSet<Term> |
initAssertLiterals(Sequent seq,
TermServices services) |
private static ImmutableSet<Term> |
sequentToTerms(Sequent seq) |
private final QuantifiableVariable firstVar
allTerm
private final Term matrix
private ImmutableSet<Term> assumedLiterals
private final java.util.Map<Term,java.lang.Long> instancesWithCosts
Term
) to cost Long
private final TriggersSet triggersSet
TriggersSet
of this allTerm
private static Term lastQuantifiedFormula
private static Sequent lastSequent
private static Instantiation lastResult
static Instantiation create(Term qf, Sequent seq, Services services)
private static ImmutableSet<Term> sequentToTerms(Sequent seq)
private void addInstances(ImmutableSet<Term> terms, Services services)
terms
- on which trigger are doning matching search every
Substitution
s by matching triggers
from triggersSet
to terms
compute
their cost and store the pair of instance (Term) and
cost(Long) in instancesCostCache
private void addArbitraryInstance(Services services)
private Term createArbitraryInstantiation(QuantifiableVariable var, TermServices services)
private void addInstance(Substitution sub, Services services)
private void addInstance(Substitution sub, long cost)
var
in sub
with
cost
to instancesCostCache
if this instance is
exist, compare thire cost and store the less one.sub
- cost
- private ImmutableSet<Term> initAssertLiterals(Sequent seq, TermServices services)
seq
- services
- TODOstatic RuleAppCost computeCost(Term inst, Term form, Sequent seq, Services services)
private RuleAppCost computeCostHelp(Term inst)
ImmutableSet<Term> getSubstitution()
private Term getMatrix()