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 de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.logic.Term;
021: import de.uka.ilkd.key.logic.TermBuilder;
022: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
023: import de.uka.ilkd.key.logic.op.Function;
024: import de.uka.ilkd.key.logic.op.Op;
025: import de.uka.ilkd.key.logic.op.Operator;
026: import de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial;
027:
028: /**
029: * This class is used to prove some simple arithmetic problem which are
030: * a==b, a>=b, a<=b; Besides it can be used to prove that a>=b or a<=b by
031: * knowing that c>=d or c<=d;
032: *
033: */
034: class HandleArith {
035:
036: private final static TermBuilder tb = TermBuilder.DF;
037: private final static Term trueT = tb.tt(), falseT = tb.ff();
038:
039: private HandleArith() {
040: }
041:
042: /**
043: * try to prove atom by using polynomial
044: *
045: * @param problem
046: * @return <code>trueT</code> if if formu is proved to true,
047: * <code>falseT</code> if false, and <code>problem</code> if it
048: * cann't be proved.
049: */
050: public static Term provedByArith(Term problem, Services services) {
051: Term arithTerm = formatArithTerm(problem, services);
052: if (arithTerm.equals(falseT))
053: return provedArithEqual(problem, services);
054: Polynomial poly1 = Polynomial
055: .create(arithTerm.sub(0), services);
056: Polynomial poly2 = Polynomial
057: .create(arithTerm.sub(1), services);
058: if (poly2.valueLeq(poly1)) {
059: return trueT;
060: }
061: if (poly1.valueLess(poly2)) {
062: return falseT;
063: }
064: return problem;
065: }
066:
067: /**
068: * @param problem
069: * @return true if atom.sub(0) is euqual to atom.sub(1), false if not
070: * equal, else return atom
071: */
072: public static Term provedArithEqual(Term problem, Services services) {
073: boolean temp = true;
074: Term pro = problem;
075: Operator op = pro.op();
076: // may be here we should check wehre sub0 and sub1 is integer.
077: while (op == Op.NOT) {
078: pro = pro.sub(0);
079: op = pro.op();
080: temp = !temp;
081: }
082: if (op == Op.EQUALS) {
083: Term sub0 = problem.sub(0);
084: Term sub1 = problem.sub(1);
085: Polynomial poly1 = Polynomial.create(sub0, services);
086: Polynomial poly2 = Polynomial.create(sub1, services);
087: boolean gt = poly2.valueLeq(poly1);
088: boolean lt = poly1.valueLeq(poly2);
089: if (gt && lt)
090: return temp ? trueT : falseT;
091: if (gt || lt)
092: return temp ? falseT : trueT;
093: }
094: return problem;
095: }
096:
097: /**
098: * Try to prove problem by know that axiom is true. The idea is that we
099: * know a>=b(axiom),we want to prove c>=d(problem). It is enough to
100: * prove that c+b>=a+d which means c>=d is true. or we prove that
101: * !(c>=d) which is d>=c+1 is true. This means c>= d is false;
102: *
103: * @param problem
104: * @param axiom
105: * @return trueT if true, falseT if false, and atom if can't be prove;
106: */
107: public static Term provedByArith(Term problem, Term axiom,
108: Services services) {
109: Term cd = formatArithTerm(problem, services);
110: Term ab = formatArithTerm(axiom, services);
111: if (cd.op() == Op.FALSE || ab.op() == Op.FALSE)
112: return problem;
113: Function addfun = services.getTypeConverter().getIntegerLDT()
114: .getArithAddition();
115: Term arithTerm = tb.geq(tb.func(addfun, cd.sub(0), ab.sub(1)),
116: tb.func(addfun, ab.sub(0), cd.sub(1)), services);
117: Term res = provedByArith(arithTerm, services);
118: if (res.op() == Op.TRUE)
119: return trueT;
120: Term t0 = formatArithTerm(tb.not(problem), services);
121: arithTerm = tb.geq(tb.func(addfun, t0.sub(0), ab.sub(1)), tb
122: .func(addfun, ab.sub(0), t0.sub(1)), services);
123: res = provedByArith(arithTerm, services);
124: if (res.op() == Op.TRUE)
125: return falseT;
126: return problem;
127: }
128:
129: /**
130: * Format literal to a form of "geq",linke a>=b;For example, a <=b to
131: * b>=a;a>b to a>=b+1;!(a>=b) to b>=a+1..
132: *
133: * @param term
134: * @return falseT if <code>term</code>'s operator is not >= or <=
135: */
136: private static Term formatArithTerm(Term problem, Services services) {
137: Term pro = problem;
138: Operator op = pro.op();
139: boolean opNot = false;
140: while (op == Op.NOT) {
141: opNot = !opNot;
142: pro = pro.sub(0);
143: op = pro.op();
144: }
145: IntegerLDT ig = services.getTypeConverter().getIntegerLDT();
146: Function geq = ig.getGreaterOrEquals();
147: Function leq = ig.getLessOrEquals();
148: if (op == geq) {
149: if (opNot)
150: pro = tb.geq(pro.sub(1), tb.func(ig.getArithAddition(),
151: pro.sub(0), tb.zTerm(services, "1")), services);
152: } else {
153: if (op == leq) {
154: if (opNot)
155: pro = tb.geq(pro.sub(0), tb.func(ig
156: .getArithAddition(), pro.sub(1), tb.zTerm(
157: services, "1")), services);
158: else
159: pro = tb.geq(pro.sub(1), pro.sub(0), services);
160: } else
161: pro = falseT;
162: }
163: return pro;
164: }
165:
166: }
|