private class TriggersSet.ClauseTrigger
extends java.lang.Object
Trigger
s in a clause. And it
will try to find triggers from every literals in this clause. Every
substerm of literal that satify the conditions:(1)it should not be a
variable, (2) it doesn't contain propersitional connectives, (3) it is
not in loop, (4) it should contains all universal variables in the clause
and the first variable of allTerm
(5) it doesn't contain
subtrigger, will be selected as an Uni-trigger. If a literal does not
contain all universal variables in clause, a set of subterms of this
literal will be selected as Multi-trigger's elements which are actually
uni-triggers except that condition (2) will be changedand into that it
contains all universal variables in the literal in. Afterwards, a set of
multi-triggers will be constructed by combining thoes elements so that
all variables in clause should be include by some of them.Modifier and Type | Field and Description |
---|---|
(package private) Term |
clause |
private ImmutableSet<Trigger> |
elementsOfMultiTrigger
elements which are uni-trigges and will be used to construct
several multi-triggers for
clause |
(package private) ImmutableSet<QuantifiableVariable> |
selfUQVS
all unversal variables of
clause |
Constructor and Description |
---|
ClauseTrigger(Term clause) |
Modifier and Type | Method and Description |
---|---|
private boolean |
addMultiTrigger(ImmutableSet<Trigger> trs)
try to construct a multi-trigger by given
ts |
private void |
addUniTrigger(Term term,
Services services)
add a uni-trigger to triggers set or add an element of
multi-triggers for this clause
|
private java.util.Set<Term> |
combineSubterms(Term oriTerm,
java.util.Set<Term>[] possibleSubs,
Term[] chosenSubs,
ImmutableArray<QuantifiableVariable> boundVars,
int i,
TermServices services) |
void |
createTriggers(Services services)
Searching uni-triggers and elements of multi-triggers in every
literal in this
clause and add those uni-triggers
to the goal trigger set. |
private java.util.Set<Term> |
expandIfThenElse(Term t,
TermServices services) |
private boolean |
isAcceptableTrigger(Term term,
Services services)
Further criteria for triggers.
|
private boolean |
mightContainTriggers(Term term)
Check whether a given term (or a subterm of the term) might be a
trigger candidate
|
private boolean |
recAddTriggers(Term term,
Services services) |
private java.util.Set<ImmutableSet<Trigger>> |
setMultiTriggers(java.util.Iterator<Trigger> ts)
find all possible combination of
ts . |
final Term clause
final ImmutableSet<QuantifiableVariable> selfUQVS
clause
private ImmutableSet<Trigger> elementsOfMultiTrigger
clause
public ClauseTrigger(Term clause)
public void createTriggers(Services services)
clause
and add those uni-triggers
to the goal trigger set. At last construct multi-triggers from
those elements.private boolean recAddTriggers(Term term, Services services)
term
- one atom at the beginingservices
- the Servicesterm
private java.util.Set<Term> expandIfThenElse(Term t, TermServices services)
private java.util.Set<Term> combineSubterms(Term oriTerm, java.util.Set<Term>[] possibleSubs, Term[] chosenSubs, ImmutableArray<QuantifiableVariable> boundVars, int i, TermServices services)
private boolean mightContainTriggers(Term term)
private boolean isAcceptableTrigger(Term term, Services services)
private void addUniTrigger(Term term, Services services)
private java.util.Set<ImmutableSet<Trigger>> setMultiTriggers(java.util.Iterator<Trigger> ts)
ts
. Once a
combination of elements contains all variables of this clause,
it will be used to construct the multi-trigger which will be
add to triggers setts
- elements of multi-triggers at the beginningprivate boolean addMultiTrigger(ImmutableSet<Trigger> trs)
ts
trs
- a set of triggertrs
contains all universal varaibles
of this clause, and add the contstructed multi-trigger to
triggers set