Modifier and Type | Field and Description |
---|---|
private Term |
clause |
private ImmutableSet<QuantifiableVariable> |
qvs |
private ImmutableSet<Trigger> |
triggers |
Constructor and Description |
---|
MultiTrigger(ImmutableSet<Trigger> triggers,
ImmutableSet<QuantifiableVariable> qvs,
Term clause) |
Modifier and Type | Method and Description |
---|---|
boolean |
equals(Object arg0) |
ImmutableSet<Substitution> |
getSubstitutionsFromTerms(ImmutableSet<Term> targetTerms,
TermServices services) |
Term |
getTriggerTerm() |
int |
hashCode() |
private ImmutableSet<Substitution> |
setMultiSubstitution(Iterator<? extends Trigger> ts,
ImmutableSet<Term> terms,
TermServices services)
help function for getMultiSubstitution
|
String |
toString() |
private Substitution |
unifySubstitution(Substitution sub0,
Substitution sub1)
unify two substitution, if same variable are bound with same term return
a new substitution with all universal quantifiable variables in two
substituition, otherwise return null
|
private final ImmutableSet<Trigger> triggers
private final ImmutableSet<QuantifiableVariable> qvs
private final Term clause
MultiTrigger(ImmutableSet<Trigger> triggers, ImmutableSet<QuantifiableVariable> qvs, Term clause)
public ImmutableSet<Substitution> getSubstitutionsFromTerms(ImmutableSet<Term> targetTerms, TermServices services)
getSubstitutionsFromTerms
in interface Trigger
private ImmutableSet<Substitution> setMultiSubstitution(Iterator<? extends Trigger> ts, ImmutableSet<Term> terms, TermServices services)
private Substitution unifySubstitution(Substitution sub0, Substitution sub1)
public Term getTriggerTerm()
getTriggerTerm
in interface Trigger