de.uka.ilkd.key.strategy.quantifierHeuristics

Class Instantiation

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.Instantiation

class Instantiation
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableSet<Term>	assumedLiterals Literals occurring in the sequent at hand.
private QuantifiableVariable	firstVar universally quantifiable variable bound inallTerm
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

Constructor Summary

Constructors

Modifier	Constructor and Description
private	Instantiation(Term allterm, Sequent seq, Services services)

Method Summary

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)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

firstVar

private final QuantifiableVariable firstVar

universally quantifiable variable bound inallTerm

matrix

private final Term matrix

assumedLiterals

private ImmutableSet<Term> assumedLiterals

Literals occurring in the sequent at hand. This is used for branch prediction

instancesWithCosts

private final java.util.Map<Term,java.lang.Long> instancesWithCosts

HashMap from instance(Term) to cost Long

triggersSet

private final TriggersSet triggersSet

the TriggersSet of this allTerm

lastQuantifiedFormula

private static Term lastQuantifiedFormula

lastSequent

private static Sequent lastSequent

lastResult

private static Instantiation lastResult

Constructor Detail

Instantiation

private Instantiation(Term allterm,
                      Sequent seq,
                      Services services)

Method Detail

create

static Instantiation create(Term qf,
                            Sequent seq,
                            Services services)

sequentToTerms

private static ImmutableSet<Term> sequentToTerms(Sequent seq)

addInstances

private void addInstances(ImmutableSet<Term> terms,
                          Services services)

Parameters:

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

addArbitraryInstance

private void addArbitraryInstance(Services services)

createArbitraryInstantiation

private Term createArbitraryInstantiation(QuantifiableVariable var,
                                          TermServices services)

addInstance

private void addInstance(Substitution sub,
                         Services services)

addInstance

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.

Parameters:

sub -

cost -

initAssertLiterals

private ImmutableSet<Term> initAssertLiterals(Sequent seq,
                                              TermServices services)

Parameters:

seq -

services - TODO

Returns:

all literals in antesequent, and all negation of literal in succedent

computeCost

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.

computeCostHelp

private RuleAppCost computeCostHelp(Term inst)

getSubstitution

ImmutableSet<Term> getSubstitution()

get all instances from instancesCostCache subsCache

getMatrix

private Term getMatrix()