001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.strategy.quantifierHeuristics;
019:
020: import java.util.HashMap;
021: import java.util.Map;
022:
023: import de.uka.ilkd.key.logic.IteratorOfTerm;
024: import de.uka.ilkd.key.logic.SetAsListOfTerm;
025: import de.uka.ilkd.key.logic.SetOfTerm;
026: import de.uka.ilkd.key.logic.Term;
027: import de.uka.ilkd.key.logic.op.Op;
028: import de.uka.ilkd.key.logic.op.Operator;
029: import de.uka.ilkd.key.logic.op.SetAsListOfQuantifiableVariable;
030: import de.uka.ilkd.key.logic.op.SetOfQuantifiableVariable;
031: import de.uka.ilkd.key.util.LRUCache;
032:
033: /**
034: * This class describes the relation between different clauses in a CNF.
035: * If two clauses have the same existential quantifiable variable, we say
036: * they are connected. And this property is transtitive.
037: */
038: class ClausesGraph {
039:
040: /**
041: * Map from <code>Term</code>(allTerm) to <code>ClausesGraph</code>
042: */
043: private final static Map graphCache = new LRUCache(1000);
044:
045: private final SetOfQuantifiableVariable exVars;
046:
047: /**
048: * Map from <code>Term</code> to <code>SetOfTerm</code>
049: */
050: private final Map connections = new HashMap();
051:
052: private final SetOfTerm clauses;
053:
054: static ClausesGraph create(Term quantifiedFormula) {
055: ClausesGraph graph = (ClausesGraph) graphCache
056: .get(quantifiedFormula);
057: if (graph == null) {
058: graph = new ClausesGraph(quantifiedFormula);
059: graphCache.put(quantifiedFormula, graph);
060: }
061: return graph;
062: }
063:
064: private ClausesGraph(Term quantifiedFormula) {
065: exVars = existentialVars(quantifiedFormula);
066: clauses = computeClauses(TriggerUtils
067: .discardQuantifiers(quantifiedFormula));
068: buildInitialGraph();
069: buildFixedPoint();
070: }
071:
072: private void buildFixedPoint() {
073: boolean changed;
074: do {
075: changed = false;
076:
077: final IteratorOfTerm forIt = clauses.iterator();
078: while (forIt.hasNext()) {
079: final Term formula = forIt.next();
080: final SetOfTerm oldConnections = getConnections(formula);
081: final SetOfTerm newConnections = getTransitiveConnections(oldConnections);
082:
083: if (newConnections.size() > oldConnections.size()) {
084: changed = true;
085: connections.put(formula, newConnections);
086: }
087: }
088:
089: } while (changed);
090: }
091:
092: private SetOfTerm getTransitiveConnections(SetOfTerm formulas) {
093: final IteratorOfTerm termIt = formulas.iterator();
094: while (termIt.hasNext())
095: formulas = formulas.union(getConnections(termIt.next()));
096: return formulas;
097: }
098:
099: /**
100: *
101: * @param formula0
102: * @param formula1
103: * @return ture if clause of formula0 and clause of formula1
104: * are connected.
105: */
106: boolean connected(Term formula0, Term formula1) {
107: final SetOfTerm subFormulas1 = computeClauses(formula1);
108: final IteratorOfTerm it = computeClauses(formula0).iterator();
109: while (it.hasNext()) {
110: if (intersect(getConnections(it.next()), subFormulas1)
111: .size() > 0)
112: return true;
113: }
114: return false;
115: }
116:
117: boolean isFullGraph() {
118: final IteratorOfTerm it = clauses.iterator();
119: if (it.hasNext()) {
120: if (getConnections(it.next()).size() < clauses.size())
121: return false;
122: }
123: return true;
124: }
125:
126: /**
127: * @param formula
128: * @return set of terms that connect to the formula.
129: */
130: private SetOfTerm getConnections(Term formula) {
131: return (SetOfTerm) connections.get(formula);
132: }
133:
134: /**
135: * initiate connection map.
136: *
137: */
138: private void buildInitialGraph() {
139: final IteratorOfTerm it = clauses.iterator();
140: while (it.hasNext()) {
141: final Term clause = it.next();
142: connections.put(clause, directConnections(clause));
143: }
144: }
145:
146: /**
147: *
148: * @param formula
149: * @return set of term that connect to formula.
150: */
151: private SetOfTerm directConnections(Term formula) {
152: SetOfTerm res = SetAsListOfTerm.EMPTY_SET;
153: final IteratorOfTerm it = clauses.iterator();
154: while (it.hasNext()) {
155: final Term clause = it.next();
156: if (directlyConnected(clause, formula))
157: res = res.add(clause);
158: }
159: return res;
160: }
161:
162: /**
163: *
164: * @param set
165: * @return ture if set contains one or more exists varaible that are also in
166: * exVars
167: */
168: private boolean containsExistentialVariables(
169: SetOfQuantifiableVariable set) {
170: return intersect(set, exVars).size() > 0;
171: }
172:
173: /**
174: * @param formula0
175: * @param formula1
176: * @return true if formula0 and formula1 have one or more exists varaible
177: * that are the same.
178: */
179: private boolean directlyConnected(Term formula0, Term formula1) {
180: return containsExistentialVariables(intersect(formula0
181: .freeVars(), formula1.freeVars()));
182: }
183:
184: /**
185: * @param formula
186: * @return retrun set of terms of all clauses under the formula
187: */
188:
189: private SetOfTerm computeClauses(Term formula) {
190: final Operator op = formula.op();
191: if (op == Op.NOT)
192: return computeClauses(formula.sub(0));
193: else if (op == Op.AND) {
194: return computeClauses(formula.sub(0)).union(
195: computeClauses(formula.sub(1)));
196: } else {
197: return SetAsListOfTerm.EMPTY_SET.add(formula);
198: }
199: }
200:
201: /**
202: * return the exists variables bound in the top level of
203: * a given cnf formula.
204: */
205: private SetOfQuantifiableVariable existentialVars(Term formula) {
206: final Operator op = formula.op();
207: if (op == Op.ALL)
208: return existentialVars(formula.sub(0));
209: if (op == Op.EX)
210: return existentialVars(formula.sub(0))
211: .add(
212: formula.varsBoundHere(0)
213: .lastQuantifiableVariable());
214: return SetAsListOfQuantifiableVariable.EMPTY_SET;
215: }
216:
217: /**
218: * @return a set of quantifiableVariable which are belonged to
219: * both set0 and set1 have
220: */
221: private SetOfQuantifiableVariable intersect(
222: SetOfQuantifiableVariable set0,
223: SetOfQuantifiableVariable set1) {
224: return TriggerUtils.intersect(set0, set1);
225: }
226:
227: /**
228: *
229: * @param set0
230: * @param set1
231: * @return a set of terms which are belonged to both set0 and set1.
232: */
233: private SetOfTerm intersect(SetOfTerm set0, SetOfTerm set1) {
234: SetOfTerm res = SetAsListOfTerm.EMPTY_SET;
235: if (set0 == null || set1 == null)
236: return res;
237: final IteratorOfTerm it = set0.iterator();
238: while (it.hasNext()) {
239: final Term el = it.next();
240: if (set1.contains(el))
241: res = res.add(el);
242: }
243: return res;
244: }
245:
246: }
|