de.uka.ilkd.key.strategy.quantifierHeuristics

Class ClausesGraph

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.ClausesGraph

public class ClausesGraph
extends java.lang.Object

This class describes the relation between different clauses in a CNF. If two clauses have the same existential quantifiable variable, we say they are connected. And this property is transitive.

Field Summary

Fields

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

Constructor Summary

Constructors

Modifier	Constructor and Description
private	ClausesGraph(Term quantifiedFormula)

Method Summary

Modifier and Type	Method and Description
private void	buildFixedPoint()
private void	buildInitialGraph() initiate connection map.
private ImmutableSet<Term>	computeClauses(Term formula)
(package private) boolean	connected(Term formula0, Term formula1)
private boolean	containsExistentialVariables(ImmutableSet<QuantifiableVariable> set)
(package private) static ClausesGraph	create(Term quantifiedFormula, ServiceCaches caches)
private ImmutableSet<Term>	directConnections(Term formula)
private boolean	directlyConnected(Term formula0, Term formula1)
private ImmutableSet<QuantifiableVariable>	existentialVars(Term formula) return the exists variables bound in the top level of a given cnf formula.
private ImmutableSet<Term>	getConnections(Term formula)
private ImmutableSet<Term>	getTransitiveConnections(ImmutableSet<Term> formulas)
private ImmutableSet<Term>	intersect(ImmutableSet<Term> set0, ImmutableSet<Term> set1)
private ImmutableSet<QuantifiableVariable>	intersectQV(ImmutableSet<QuantifiableVariable> set0, ImmutableSet<QuantifiableVariable> set1)
(package private) boolean	isFullGraph()

Methods inherited from class java.lang.Object

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

Field Detail

exVars

private final ImmutableSet<QuantifiableVariable> exVars

connections

private final java.util.Map<Term,ImmutableSet<Term>> connections

Map from Term to ImmutableSet

clauses

private final ImmutableSet<Term> clauses

Constructor Detail

ClausesGraph

private ClausesGraph(Term quantifiedFormula)

Method Detail

create

static ClausesGraph create(Term quantifiedFormula,
                           ServiceCaches caches)

buildFixedPoint

private void buildFixedPoint()

getTransitiveConnections

private ImmutableSet<Term> getTransitiveConnections(ImmutableSet<Term> formulas)

connected

boolean connected(Term formula0,
                  Term formula1)

Parameters:

formula0 -

formula1 -

Returns:

ture if clause of formula0 and clause of formula1 are connected.

isFullGraph

boolean isFullGraph()

getConnections

private ImmutableSet<Term> getConnections(Term formula)

Parameters:

formula -

Returns:

set of terms that connect to the formula.

buildInitialGraph

private void buildInitialGraph()

initiate connection map.

directConnections

private ImmutableSet<Term> directConnections(Term formula)

Parameters:

formula -

Returns:

set of term that connect to formula.

containsExistentialVariables

private boolean containsExistentialVariables(ImmutableSet<QuantifiableVariable> set)

Parameters:

set -

Returns:

ture if set contains one or more exists varaible that are also in exVars

directlyConnected

private boolean directlyConnected(Term formula0,
                                  Term formula1)

Parameters:

formula0 -

formula1 -

Returns:

true if formula0 and formula1 have one or more exists varaible that are the same.

computeClauses

private ImmutableSet<Term> computeClauses(Term formula)

Parameters:

formula -

Returns:

retrun set of terms of all clauses under the formula

existentialVars

private ImmutableSet<QuantifiableVariable> existentialVars(Term formula)

return the exists variables bound in the top level of a given cnf formula.

intersectQV

private ImmutableSet<QuantifiableVariable> intersectQV(ImmutableSet<QuantifiableVariable> set0,
                                                       ImmutableSet<QuantifiableVariable> set1)

Returns:

a set of quantifiableVariable which are belonged to both set0 and set1 have

intersect

private ImmutableSet<Term> intersect(ImmutableSet<Term> set0,
                                     ImmutableSet<Term> set1)

Parameters:

set0 -

set1 -

Returns:

a set of terms which are belonged to both set0 and set1.