de.uka.ilkd.key.strategy.quantifierHeuristics

Class TriggersSet

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.TriggersSet

public class TriggersSet
extends java.lang.Object

This class is used to select and store Triggers for a quantified formula in Prenex CNF(PCNF).

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	TriggersSet.ClauseTrigger this class is used to find Triggers in a clause.

Field Summary

Fields

Modifier and Type	Field and Description
private Term	allTerm Quantified formula of PCNF
private ImmutableSet<Trigger>	allTriggers all Triggers for allTerm
private Substitution	replacementWithMVs Replacement of the bound variables in allTerm with metavariables and constants
private java.util.Map<Term,Trigger>	termToTrigger a HashMap from Term to Trigger which stores different subterms of allTerm with its according trigger
private ImmutableSet<QuantifiableVariable>	uniQuantifiedVariables all universal variables of allTerm

Constructor Summary

Constructors

Modifier	Constructor and Description
private	TriggersSet(Term allTerm, Services services)

Method Summary

Modifier and Type	Method and Description
(package private) static TriggersSet	create(Term allTerm, Services services)
private Trigger	createMultiTrigger(ImmutableSet<Trigger> trs, Term clause, ImmutableSet<QuantifiableVariable> qvs)
private Trigger	createUniTrigger(Term trigger, ImmutableSet<QuantifiableVariable> qvs, boolean isUnify, boolean isElement)
ImmutableSet<Trigger>	getAllTriggers()
private ImmutableSet<QuantifiableVariable>	getAllUQS(Term allterm)
Term	getQuantifiedFormula()
Substitution	getReplacementWithMVs()
ImmutableSet<QuantifiableVariable>	getUniQuantifiedVariables()
private void	initTriggers(Services services) initial all Triggers by finding triggers in every clauses

Methods inherited from class java.lang.Object

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

Field Detail

allTerm

private final Term allTerm

Quantified formula of PCNF

allTriggers

private ImmutableSet<Trigger> allTriggers

all Triggers for allTerm

termToTrigger

private final java.util.Map<Term,Trigger> termToTrigger

a HashMap from Term to Trigger which stores different subterms of allTerm with its according trigger

uniQuantifiedVariables

private final ImmutableSet<QuantifiableVariable> uniQuantifiedVariables

all universal variables of allTerm

replacementWithMVs

private final Substitution replacementWithMVs

Replacement of the bound variables in allTerm with metavariables and constants

Constructor Detail

TriggersSet

private TriggersSet(Term allTerm,
                    Services services)

Method Detail

create

static TriggersSet create(Term allTerm,
                          Services services)

getAllUQS

private ImmutableSet<QuantifiableVariable> getAllUQS(Term allterm)

Parameters:

allterm -

Returns:

return all univesal variables of allterm

initTriggers

private void initTriggers(Services services)

initial all Triggers by finding triggers in every clauses

createUniTrigger

private Trigger createUniTrigger(Term trigger,
                                 ImmutableSet<QuantifiableVariable> qvs,
                                 boolean isUnify,
                                 boolean isElement)

Parameters:

trigger - a Term

qvs - all universal variables of trigger

isUnify - true if triggercontains existential variable

isElement - true if the Trigger to be created is taken as a element of multi-trigger

Returns:

a Trigger with trigger as its term

createMultiTrigger

private Trigger createMultiTrigger(ImmutableSet<Trigger> trs,
                                   Term clause,
                                   ImmutableSet<QuantifiableVariable> qvs)

Parameters:

trs -

clause - a Term of clause form

qvs - all universal varaibles of all clause

Returns:

the MultTrigger for the given triggers

getQuantifiedFormula

public Term getQuantifiedFormula()

getAllTriggers

public ImmutableSet<Trigger> getAllTriggers()

getReplacementWithMVs

public Substitution getReplacementWithMVs()

getUniQuantifiedVariables

public ImmutableSet<QuantifiableVariable> getUniQuantifiedVariables()