public class ClausesGraph
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ImmutableSet<Term> |
clauses |
private java.util.Map<Term,ImmutableSet<Term>> |
connections
Map from
Term to ImmutableSet |
private ImmutableSet<QuantifiableVariable> |
exVars |
Modifier | Constructor and Description |
---|---|
private |
ClausesGraph(Term quantifiedFormula) |
private final ImmutableSet<QuantifiableVariable> exVars
private final java.util.Map<Term,ImmutableSet<Term>> connections
Term
to ImmutableSet
private final ImmutableSet<Term> clauses
private ClausesGraph(Term quantifiedFormula)
static ClausesGraph create(Term quantifiedFormula, ServiceCaches caches)
private void buildFixedPoint()
private ImmutableSet<Term> getTransitiveConnections(ImmutableSet<Term> formulas)
boolean connected(Term formula0, Term formula1)
formula0
- formula1
- boolean isFullGraph()
private ImmutableSet<Term> getConnections(Term formula)
formula
- private void buildInitialGraph()
private ImmutableSet<Term> directConnections(Term formula)
formula
- private boolean containsExistentialVariables(ImmutableSet<QuantifiableVariable> set)
set
- private boolean directlyConnected(Term formula0, Term formula1)
formula0
- formula1
- private ImmutableSet<Term> computeClauses(Term formula)
formula
- private ImmutableSet<QuantifiableVariable> existentialVars(Term formula)
private ImmutableSet<QuantifiableVariable> intersectQV(ImmutableSet<QuantifiableVariable> set0, ImmutableSet<QuantifiableVariable> set1)
private ImmutableSet<Term> intersect(ImmutableSet<Term> set0, ImmutableSet<Term> set1)
set0
- set1
-