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: package de.uka.ilkd.key.strategy.quantifierHeuristics;
018:
019: import java.util.HashSet;
020: import java.util.Iterator;
021: import java.util.Map;
022: import java.util.Set;
023:
024: import de.uka.ilkd.key.gui.Main;
025: import de.uka.ilkd.key.logic.IteratorOfTerm;
026: import de.uka.ilkd.key.logic.SetAsListOfTerm;
027: import de.uka.ilkd.key.logic.SetOfTerm;
028: import de.uka.ilkd.key.logic.Term;
029: import de.uka.ilkd.key.logic.TermBuilder;
030: import de.uka.ilkd.key.logic.op.Op;
031: import de.uka.ilkd.key.logic.op.Operator;
032:
033: /**
034: * TODO: rewrite, this seems pretty inefficient ...
035: */
036: class PredictCostProver {
037:
038: private final static TermBuilder tb = TermBuilder.DF;
039:
040: private final static Term trueT = tb.tt(), falseT = tb.ff();
041:
042: /**assume that all literal in <code>assertLiterals</code> are true*/
043: private SetOfTerm assertLiterals = SetAsListOfTerm.EMPTY_SET;
044:
045: /**clauses from <code>instance</code> of CNF*/
046: private Set clauses = new HashSet();
047:
048: private PredictCostProver(Term instance, SetOfTerm assertList) {
049: this .assertLiterals = this .assertLiterals.union(assertList);
050: initClauses(instance);
051: }
052:
053: public static long computerInstanceCost(Substitution sub,
054: Term matrix, SetOfTerm assertList) {
055:
056: final PredictCostProver prover = new PredictCostProver(sub
057: .applyWithoutCasts(matrix), assertList);
058: return prover.cost();
059: }
060:
061: //init context
062: private void initClauses(Term instance) {
063: IteratorOfTerm it = TriggerUtils.iteratorByOperator(instance,
064: Op.AND);
065: while (it.hasNext()) {
066: SetOfTerm literals = TriggerUtils.setByOperator(it.next(),
067: Op.OR);
068: //clauses.add(new Clause(literals));
069: Iterator lit = createClause(literals.toArray(), 0)
070: .iterator();
071: while (lit.hasNext()) {
072: clauses.add(new Clause((SetOfTerm) lit.next()));
073: }
074: }
075: }
076:
077: private Set createClause(Term[] terms, int i) {
078: Set res = new HashSet();
079: if (i >= terms.length)
080: return res;
081: Term self = terms[i];
082: boolean ifthen = terms[i].op() == Op.IF_EX_THEN_ELSE;
083: Set next = createClause(terms, i + 1);
084: if (next.size() == 0) {
085: if (ifthen) {
086: res.add(SetAsListOfTerm.EMPTY_SET.add(
087: tb.not(self.sub(0))).add(self.sub(1)));
088: res.add(SetAsListOfTerm.EMPTY_SET.add(self.sub(0)).add(
089: self.sub(2)));
090: } else
091: res.add(SetAsListOfTerm.EMPTY_SET.add(self));
092: } else {
093: Iterator it = next.iterator();
094: while (it.hasNext()) {
095: SetOfTerm ts = (SetOfTerm) it.next();
096: if (ifthen) {
097: res.add(ts.add(tb.not(self.sub(0)))
098: .add(self.sub(1)));
099: res.add(ts.add(self.sub(0)).add(self.sub(2)));
100: } else {
101: res.add(ts.add(self));
102: }
103: }
104: }
105: return res;
106: }
107:
108: //end
109:
110: //rules of thie sub prover
111: //(1) cache rule
112: /**
113: * Find in the cache wether this <code>problem</code> has
114: * ever been proved
115: */
116: private Term provedFromCache(Term problem, Map cache) {
117: boolean positive = true;
118: Term pro = problem;
119: Operator op = pro.op();
120: while (op == Op.NOT) {
121: pro = pro.sub(0);
122: op = pro.op();
123: positive = !positive;
124: }
125: Term res = (Term) cache.get(pro);
126: if (res != null)
127: return positive ? res : tb.not(res);
128: return problem;
129: }
130:
131: /**
132: * add the problem with its result(res) to cache. if the problem is
133: * not an atom, add its subterm with according changed res to cache.
134: */
135: private void addToCache(Term problem, Term res, Map cache) {
136: boolean temp = true;
137: Term pro = problem;
138: Operator op = pro.op();
139: while (op == Op.NOT) {
140: pro = pro.sub(0);
141: op = pro.op();
142: temp = !temp;
143: }
144: cache.put(pro, temp ? res : tb.not(res));
145: }
146:
147: //(2)self-proved rule
148: /**
149: * If the given <code>problem</code>'s operation is equal,or mathmetic
150: * operation(=,>=, <=), this method will try to prove it by finding the
151: * relation between its two subterms.
152: */
153: private Term provedBySelf(Term problem) {
154: boolean temp = true;
155: Term pro = problem;
156: Operator op = pro.op();
157: if (op == Op.NOT) {
158: temp = !temp;
159: pro = pro.sub(0);
160: op = pro.op();
161: }
162: if (op == Op.EQUALS && pro.sub(0).equals(pro.sub(1)))
163: return temp ? trueT : falseT;
164: Term arithRes = HandleArith.provedByArith(pro, Main
165: .getInstance().mediator().getServices());
166: if (TriggerUtils.isTrueOrFalse(arithRes))
167: return temp ? arithRes : tb.not(arithRes);
168: else
169: return problem;
170: }
171:
172: //(3)equal rule
173: /***
174: * @return trueT if problem is equal axiom, false if problem's negation
175: * is equal axiom. Otherwise retrun problem.
176: */
177: private Term provedByequal(Term problem, Term axiom) {
178: boolean temp = true;
179: Term pro = problem;
180: if (pro.op() == Op.NOT) {
181: pro = pro.sub(0);
182: temp = !temp;
183: }
184: Term ax = axiom;
185: if (ax.op() == Op.NOT) {
186: ax = ax.sub(0);
187: temp = !temp;
188: }
189: if (pro.equals(ax))
190: return temp ? trueT : falseT;
191: return problem;
192: }
193:
194: //(4)combine provedByequal and provedByArith .
195: /**
196: * @param problem
197: * @param axiom
198: * @return if axiom conduct problem then return trueT. If axiom conduct
199: * negation of problem return fastT. Otherwise, return problem
200: */
201: private Term provedByAnother(Term problem, Term axiom) {
202: Term res = provedByequal(problem, axiom);
203: if (TriggerUtils.isTrueOrFalse(res))
204: return res;
205: return HandleArith.provedByArith(problem, axiom, Main
206: .getInstance().mediator().getServices());
207: }
208:
209: //(5) combine rules
210: /**
211: * try to prove <code>problem</code> by know <code>assertLits</code>
212: *
213: * @param problem a literal
214: * to be proved
215: * @param assLits a set of term
216: * assertLiterals in which all literals are true
217: * @param cache a HashMap
218: * used to store proved literals
219: * @return return <code>trueT</code> if if formu is proved to true,
220: * <code> falseT</code> if false, and <code>atom</code> if it
221: * cann't be proved.
222: */
223: private Term proveLiteral(Term problem, SetOfTerm assertLits) {
224: Term res;
225: /* res = provedFromCache(problem, cache);
226: if (res.equals(trueT) || res.equals(falseT)) {
227: return res;
228: } */
229: res = provedBySelf(problem);
230: if (TriggerUtils.isTrueOrFalse(res)) {
231: // addToCache(problem,res,cache);
232: return res;
233: }
234: final IteratorOfTerm it = assertLits.iterator();
235: while (it.hasNext()) {
236: Term t = it.next();
237: res = provedByAnother(problem, t);
238: if (TriggerUtils.isTrueOrFalse(res)) {
239: // addToCache(problem, res,cache);
240: return res;
241: }
242: }
243: return problem;
244: }
245:
246: //end
247:
248: //cost computation
249: /**do two step refinement and return the cost */
250: private long cost() {
251: return firstRefine();
252: }
253:
254: /**refine every clause, by assume assertList are true and
255: * if a clause's cost is 0 which means it is refined to false, then
256: * cost 0 returned. If every clause's cost is -1 which means every clause
257: * is refined to true, cost -1 returned. Otherwise, multiply of every
258: * cost is return. Beside, if a clause is refined to a situation that
259: * only one literal is left, the literal will be add to assertLiterals.
260: */
261: private long firstRefine() {
262: long cost = 1;
263: boolean assertChanged = false;
264: Set res = new HashSet();
265: Iterator it = clauses.iterator();
266: while (it.hasNext()) {
267: Clause c = (Clause) (it.next());
268: c.firstRefine();
269: long cCost = c.cost();
270: if (cCost == 0) {
271: cost = 0;
272: res.clear();
273: break;
274: }
275: if (cCost == -1) {
276: continue;
277: }
278: if (c.literals.size() == 1) {
279: assertChanged = true;
280: assertLiterals = assertLiterals.union(c.literals);
281: } else
282: res.add(c);
283: cost = cost * cCost;
284: }
285: clauses = res;
286: if (cost == 0)
287: return 0;
288: if (res.size() == 0 && !assertChanged)
289: return -1;
290: return cost;
291: }
292:
293: /** A sat() procedure with back searching */
294: /* private long secondRefineX(SetOfTerm assertLits, Map cache, Object[] cls,
295: int index) {
296: long cost = 1;
297: for ( int i = index; i < cls.length; i++ ) {
298: Clause c = (Clause)cls[i];
299: final SetOfTerm ls = c.refine ( assertLits, cache );
300: if ( ls.contains ( falseT ) ) return 0;
301: if ( ls.contains ( trueT ) )
302: return secondRefine ( assertLits, cache, cls, i + 1 );
303: final IteratorOfTerm it = ls.iterator ();
304: while ( it.hasNext () ) {
305: SetOfTerm nextLits = SetAsListOfTerm.EMPTY_SET.union ( assertLits );
306: nextLits = nextLits.add ( it.next () );
307: final Map nextCache = new HashMap ();
308: nextCache.putAll ( cache );
309: long nextCost = secondRefine ( nextLits, nextCache, cls, i + 1 );
310: cost = cost + nextCost;
311:
312: }
313: }
314: return cost;
315: } */
316:
317: private class Clause {
318:
319: /**all literals contains in this clause*/
320: public SetOfTerm literals = SetAsListOfTerm.EMPTY_SET;
321:
322: public Clause(SetOfTerm lits) {
323: literals = lits;
324: }
325:
326: public IteratorOfTerm iterator() {
327: return literals.iterator();
328: }
329:
330: /**
331: * @return 0 if this clause is refine to false. 1 if true.
332: * Otherwise,return the number of literals it left.
333: */
334: public long cost() {
335: if (literals.contains(falseT) && literals.size() == 1)
336: return 0;
337: if (literals.contains(trueT))
338: return -1;
339: int cost = literals.size();
340: return cost;
341: }
342:
343: /** Refine this clause in two process, first try to refined by
344: * itself, @see selfRefine. Second refine this clause by assuming
345: * assertLiteras are true*/
346: public void firstRefine() {
347: // if (selfRefine(literals)) {
348: // literals = SetAsListOfTerm.EMPTY_SET.add(trueT);
349: // return;
350: // }
351: literals = this .refine(assertLiterals);
352: }
353:
354: /**
355: * Refine literals in this clause, but it does not change
356: * literlas, only return literals that can't be removed by
357: * refining
358: */
359: public SetOfTerm refine(SetOfTerm assertLits) {
360: SetOfTerm res = SetAsListOfTerm.EMPTY_SET;
361: IteratorOfTerm it = this .iterator();
362: while (it.hasNext()) {
363: Term lit = it.next();
364: Term temp = proveLiteral(lit, assertLits);
365: final Operator op = temp.op();
366: if (op == Op.TRUE) {
367: res = SetAsListOfTerm.EMPTY_SET.add(trueT);
368: break;
369: }
370: if (op == Op.FALSE) {
371: continue;
372: }
373: res = res.add(lit);
374: }
375: if (res.size() == 0)
376: res = res.add(falseT);
377: return res;
378: }
379:
380: /**This method is used for detect where a clause can be simply
381: * refined to to true. And it is implemented like this. Assume
382: * that the clause contains two literals Li and Lj. If (!Li->Lj)
383: * which is acturally (Li|Lj), is true, and the clasue is true.
384: * provedByAnthoer(Lj,!Li) is used to proved (!Li->Lj). Some
385: * examples are (!a|a) which is (!!a->a) and (a>=1|a<=0) which is
386: * !a>=1->a<=0
387: */
388: public boolean selfRefine(SetOfTerm lits) {
389: if (lits.size() <= 1)
390: return false;
391: Term[] terms = lits.toArray();
392: SetOfTerm next = lits.remove(terms[0]);
393: boolean opNot = terms[0].op() == Op.NOT;
394: Term axiom = opNot ? terms[0].sub(0) : tb.not(terms[0]);
395: for (int j = 1; j < terms.length; j++) {
396: Term pro = provedByAnother(terms[j], axiom);
397: final Operator op = pro.op();
398: if (op == Op.TRUE)
399: return true;
400: if (op == Op.FALSE && terms[0].equals(terms[j])) {
401: next = next.remove(terms[j]);
402: literals = literals.remove(terms[j]);
403: }
404: }
405: return selfRefine(next);
406: }
407:
408: public String toString() {
409: return literals.toString();
410: }
411: }
412:
413: }
|