public class TriggersSet
extends java.lang.Object
Trigger
s
for a quantified formula in Prenex CNF(PCNF).Modifier and Type | Class and Description |
---|---|
private class |
TriggersSet.ClauseTrigger
this class is used to find
Trigger s in a clause. |
Modifier and Type | Field and Description |
---|---|
private Term |
allTerm
Quantified formula of PCNF
|
private ImmutableSet<Trigger> |
allTriggers
all
Trigger s 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 |
Modifier | Constructor and Description |
---|---|
private |
TriggersSet(Term allTerm,
Services services) |
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
Trigger s by finding triggers in every clauses |
private final Term allTerm
private ImmutableSet<Trigger> allTriggers
Trigger
s for allTerm
private final java.util.Map<Term,Trigger> termToTrigger
HashMap
from Term
to Trigger
which stores different subterms of allTerm
with its according triggerprivate final ImmutableSet<QuantifiableVariable> uniQuantifiedVariables
allTerm
private final Substitution replacementWithMVs
allTerm
with
metavariables and constantsstatic TriggersSet create(Term allTerm, Services services)
private ImmutableSet<QuantifiableVariable> getAllUQS(Term allterm)
allterm
- allterm
private void initTriggers(Services services)
Trigger
s by finding triggers in every clausesprivate Trigger createUniTrigger(Term trigger, ImmutableSet<QuantifiableVariable> qvs, boolean isUnify, boolean isElement)
trigger
- a Term
qvs
- all universal variables of trigger
isUnify
- true if trigger
contains existential variableisElement
- true if the Trigger
to be created is taken as a
element of multi-triggerTrigger
with trigger
as its termprivate Trigger createMultiTrigger(ImmutableSet<Trigger> trs, Term clause, ImmutableSet<QuantifiableVariable> qvs)
trs
- clause
- a Term
of clause formqvs
- all universal varaibles of all clause
public Term getQuantifiedFormula()
public ImmutableSet<Trigger> getAllTriggers()
public Substitution getReplacementWithMVs()
public ImmutableSet<QuantifiableVariable> getUniQuantifiedVariables()