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: //
009: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
011: // Universitaet Koblenz-Landau, Germany
012: // Chalmers University of Technology, Sweden
013: //
014: // The KeY system is protected by the GNU General Public License.
015: // See LICENSE.TXT for details.
016: package de.uka.ilkd.key.proof.decproc;
017:
018: import java.util.*;
019:
020: import org.apache.log4j.Logger;
021:
022: import de.uka.ilkd.key.java.Services;
023: import de.uka.ilkd.key.logic.Semisequent;
024: import de.uka.ilkd.key.logic.Sequent;
025: import de.uka.ilkd.key.logic.Term;
026: import de.uka.ilkd.key.logic.op.ArrayOfQuantifiableVariable;
027: import de.uka.ilkd.key.logic.op.SetOfMetavariable;
028:
029: /**
030: * Represents a try to remove code duplication.
031: */
032: public abstract class DecProcTranslation {
033: /**
034: * Just a constructor which starts the conversion to Simplify syntax. The
035: * result can be fetched with
036: *
037: * @see getText-
038: * @param sequent
039: * The sequent which shall be translated.
040: * @param cs
041: * The constraints which shall be incorporated.
042: * @param localmv
043: * The local metavariables, should be the ones introduced after
044: * the last branch.
045: */
046: public DecProcTranslation(Sequent sequent, ConstraintSet cs,
047: SetOfMetavariable localmv, Services services)
048: throws SimplifyException {
049: constraintSet = cs;
050: localMetavariables = localmv;
051: this .services = services;
052: }
053:
054: /**
055: * Returns the sequent given with the constructor in Simplify
056: * syntax (as far as possible)
057: * @returns The sequent given with the constructor in Simplify
058: * syntax (as far as possible)
059: */
060: public String getText() {
061: return text;
062: }
063:
064: /**
065: * Returns a unique HashCode for the object qv.
066: * Unique means unique for the goal given to the calling class.
067: * This function does not depend on .hashcode() to deliver unique
068: * hash codes like the memory address of the object. It uses a
069: * hashMap and compares every new Object in O(n) (n number of
070: * Objects with the same .hashCode()) to all others.
071: * @returns a unique hashcode for the variable gv.
072: * @param v the Object the hashcode should be returned.
073: */
074: public int getUniqueHashCode(Object qv) {
075: Integer number = (Integer) this .variableMap.get(qv);
076: if (number == null) {
077: number = new Integer(this .variableMap.size());
078: this .variableMap.put(qv, number);
079: }
080: return number.intValue();
081: }
082:
083: /**
084: * Returns a unique HashCode for the term qv.
085: * Unique means unique for the goal given to the calling class.
086: * This function does not depend on .hashcode() to deliver
087: * unique hash codes like the memory address of the object.
088: * It uses a hashMap and compares
089: * every new Object in O(n) (n number of Objects
090: * with the same .hashCode()) to all others.
091: * It compares with .equalsModRenaming().
092: * @returns a unique hashcode for the term gv.
093: * @param term the Term the hashcode should be returned.
094: */
095: public int getUniqueHashCodeForUninterpretedTerm(Term term) {
096: Integer number = (Integer) this .variableMap
097: .get(new UninterpretedTermWrapper(term));
098: if (number == null) {
099: number = new Integer(this .variableMap.size());
100: this .variableMap.put(new UninterpretedTermWrapper(term),
101: number);
102: }
103: return number.intValue();
104: }
105:
106: /**
107: * Replaces a modulo with a set of (in-)equalities. 'a mod b' becomes the c
108: * in 'a=k*b+c'. '(a = k*b+c) & (c >= 0) & (c < b)'. These constraints
109: * are added as global constraints. The same Term is never converted twice,
110: * the 'c' calculated before is taken. This way we ensure that constraints
111: * are added just once.
112: * As a guard '!(b=0)->' is added in front of these constraints.
113: *
114: * @param t
115: * The Term to be replaced
116: * @param quantifiedVars
117: * a Vector containing all variables that have been bound in
118: * super-terms. It is only used for the translation of modulo
119: * terms, but must be looped through until we get there.
120: * @return The 'c' of '(a = k*b+c)'
121: */
122: // protected Term translateModulo(Term t, Vector quantifiedVars) {
123: // if (moduloReplacements.containsKey(t)) {
124: // return (Term) moduloReplacements.get(t);
125: // }
126: // TermFactory tf = new TermFactory();
127: // final AbstractIntegerLDT integerLDT = services.getTypeConverter()
128: // .getIntegerLDT();
129: // final Sort intSort = integerLDT.targetSort();
130: // if (quantifiedVars.size() > 0) {
131: // return null;
132: // }
133: // // let the modulo term be "a mod b"
134: // // and the replacement c for which the following constraints hold:
135: // // (!(b=0))->
136: // // variable k,
137: // Term k = tf.createFunctionTerm(new LogicVariable(new Name("k"
138: // + moduloCounter), intSort));
139: // // b = 0
140: // Term be0 = tf.createEqualityTerm(t.sub(1), integerLDT
141: // .translateLiteral(new IntLiteral(0)));
142: // // !(b=0)
143: // Term nbe0 = tf.createJunctorTerm(Op.NOT, be0);
144: // // variable c
145: // Term c = tf.createFunctionTerm(new LogicVariable(new Name("c"
146: // + moduloCounter), intSort));
147: // // k * b
148: // Term mul = tf.createFunctionTerm(integerLDT.getFunctionFor(new Times(
149: // null, null)), k, t.sub(1));
150: // // (k*b)+c
151: // Term plus = tf.createFunctionTerm(integerLDT.getFunctionFor(new Plus(
152: // null, null)), mul, c);
153: // // a = (k*b)+c
154: // Term eq = tf.createEqualityTerm(t.sub(0), plus);
155: // // c >= 0
156: // Term ge = tf.createFunctionTerm(integerLDT
157: // .getFunctionFor(new GreaterOrEquals(new ExtList())), c,
158: // integerLDT.translateLiteral(new IntLiteral(0)));
159: // // TODO Java modulo semantic, c > -b
160: // // c < b
161: // Term lt = tf.createFunctionTerm(integerLDT.getFunctionFor(new LessThan(
162: // new ExtList())), c, t.sub(1));
163: // // !(b=0)-> a = (k*b)+c
164: // Term impeq = tf.createJunctorTerm(Op.IMP, nbe0, eq);
165: // // !(b=0)-> c >= 0
166: // Term impge = tf.createJunctorTerm(Op.IMP, nbe0, ge);
167: // // !(b=0)-> c < b
168: // Term implt = tf.createJunctorTerm(Op.IMP, nbe0, lt);
169: // moduloConstraints.add(impeq);
170: // moduloConstraints.add(impge);
171: // moduloConstraints.add(implt);
172: // usedLocalMv.add(c.op());
173: // usedLocalMv.add(k.op());
174: // if (nogger.isDebugEnabled()) {
175: // nogger.debug("c.op(): " + c.op().name());
176: // }
177: // moduloCounter++;
178: // moduloReplacements.put(t, c);
179: // return c;
180: // }
181: /**
182: * Takes all the modulo constraints already collected and conjoins them
183: * conjunctivly.
184: * @return the conjunctivly conjoined modulo constraints.
185: */
186: // protected Term moduloConjoin() {
187: // if (nogger.isDebugEnabled()) {
188: // nogger.debug("Entered ModuloConjoin, number is " + moduloConstraints.size());
189: // }
190: // TermFactory tf = new TermFactory();
191: // Term[] mc = new Term[moduloConstraints.size()];
192: // for (int i = 0; i < moduloConstraints.size(); i++) {
193: // mc[i] = (Term)moduloConstraints.get(i);
194: // }
195: // if (mc.length == 0) {
196: // return tf.createJunctorTerm(Op.TRUE);
197: // } else if (mc.length == 1) {
198: // return mc[0];
199: // }
200: // Term h = mc[0];
201: // int i = 1;
202: // do {
203: // h = tf.createJunctorTerm(Op.AND, h, mc[i]);
204: // } while (i++ < mc.length - 1);
205: // return h;
206: // }
207: /**
208: *
209: * Eliminates the modulo from all the modulo constraints . First, does a
210: * bogus translate to collect all first class modulos. Then goes through all
211: * modulo constraints, tries to convert them into the decision procedures
212: * input language, and, most important, while this happens, new modulo
213: * constraints may be found. These are added to moduloConstraints. Since
214: * modulo terms are never replaced in the term structure, just in the output
215: * for the decision procedure, this just ensures, that afterwards we have a
216: * list that really contains all modulo constraints.
217: *
218: * @throws SimplifyException
219: */
220: // protected void computeModuloConstraints(Sequent seq) throws SimplifyException {
221: // translate(seq.antecedent(), ANTECEDENT); //I just want the side effects
222: // translate(seq.succedent(), SUCCEDENT); //I just want the side effects
223: // // here moduloConstraints is a moving target,
224: // // as long as new constraints are added, the loop shall go on!
225: // for (int i = 0; i < moduloConstraints.size(); i ++) {
226: // translate((Term)moduloConstraints.get(i), ANTECEDENT, new Vector());
227: // }
228: // }
229: /**
230: * Just copies the quantified variables of term into quantifiedVars
231: * @param quantifiedVars
232: * @param term
233: */
234: protected void collectQuantifiedVars(Vector quantifiedVars,
235: Term term) {
236: ArrayOfQuantifiableVariable vars = term.varsBoundHere(0);
237: for (int i = 0; i < vars.size(); ++i) {
238: quantifiedVars.add(vars.getQuantifiableVariable(i));
239: }
240: }
241:
242: /** The translation result is stored in this variable. */
243: protected String text;
244: /** StringBuffer contains all declared predicate symbols. */
245: protected final StringBuffer predicate = new StringBuffer();
246: /** StringBuffer to store text which could be usefull for the user */
247: protected final StringBuffer notes = new StringBuffer();
248: /** remember all printed predicates */
249: protected final Set predicateSet = new HashSet();
250: /** The Constraint under which the sequent is to be proven */
251: protected final ConstraintSet constraintSet;
252: /**
253: * Some terms should need a unique HashCode (CVC doesn't handle quantors,
254: * ProgramVariables from different blocks could have the same name),
255: * functions and user named skolemfunctions can get the same name. The
256: * difference to variables is that the have quantified variables so they
257: * have to be compared moduloRenaming. Comparing terms without variables
258: * with .equals() instead of .equalsModRenaming() should give a speed
259: * improvement.
260: */
261: protected final HashMap variableMap = new HashMap();
262: /**
263: * To handle local metavariabls we have to quantify them existentially. We
264: * do not need to quantify already substituted metavariables.
265: */
266: protected final HashSet usedLocalMv = new HashSet();
267: protected final HashSet usedGlobalMv = new HashSet();
268: protected final SetOfMetavariable localMetavariables;
269: protected final HashMap moduloReplacements = new HashMap();
270: protected final List moduloConstraints = new ArrayList();
271: protected int moduloCounter = 0;
272: protected final Services services;
273: protected static final int ANTECEDENT = 0;
274: protected static final int SUCCEDENT = 1;
275: protected static final int YESNOT = 2;
276:
277: static Logger nogger = Logger.getLogger(DecProcTranslation.class
278: .getName());
279:
280: /**
281: * Translates the given term into the decision procedure's input syntax and
282: * and returns the resulting StringBuffer sb.
283: *
284: * @param term
285: * the Term which should be written in Simplify syntax
286: * @param skolemization
287: * Indicates whether the formula is in the ANTECEDENT, SUCCEDENT
288: * or with YESNOT if a "not" operation occurres above the term
289: * which will prevent skolemization ("not"s are not counted). For
290: * Simplify this parameter is ignored.
291: * @param quantifiedVars
292: * a Vector containing all variables that have been bound in
293: * super-terms. It is only used for the translation of modulo
294: * terms, but must be looped through until we get there.
295: */
296: protected abstract StringBuffer translate(Term term,
297: int skolemization, Vector quantifiedVars)
298: throws SimplifyException;
299:
300: /** Translates the given sequent into the decision procedure's input syntax
301: *
302: * @param s the Sequent which should be translated
303: * @return the translated version of s
304: */
305: protected abstract StringBuffer translate(Sequent sequent)
306: throws SimplifyException;
307:
308: /**
309: * Translates the given Semisequent into the decision procedure's input
310: * syntax and returns the resulting StringBuffer sb.
311: *
312: * @param ss
313: * the SemiSequent which should be written in the decision
314: * procedure's syntax
315: * @param skolemization
316: * Indicates whether the formula is in the ANTECEDENT, SUCCEDENT
317: * or with YESNOT if a "not" operation occurres above the term
318: * which will prevent skolemization for ICS ("not"s are not
319: * counted). For Simplify this parameter is ignored.
320: */
321: protected abstract StringBuffer translate(Semisequent ss,
322: int skolemization) throws SimplifyException;
323:
324: /* protected abstract StringBuffer translate(Semisequent ss,
325: int skolemization,
326: boolean lightWeight)
327: throws SimplifyException;*/
328: }
|