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: //
010:
011: package de.uka.ilkd.key.counterexample;
012:
013: import de.uka.ilkd.key.logic.Term;
014: import de.uka.ilkd.key.logic.op.ConstructorFunction;
015: import de.uka.ilkd.key.logic.op.LogicVariable;
016:
017: /**
018: * Diese Klasse soll als Wrapper dienen fuer ibijas Termklassen.
019: * es soll gleichzeitig darin gespeichert werden, ob der entsprechende
020: * Term funktionsfrei ist.
021: * @author Sonja Pieper
022: * @version 1
023: * @see AxiomCalculus
024: */
025:
026: class CExTerm {
027:
028: Term term;
029: String opname, sorte;
030: CExTerm[] params;
031:
032: private boolean fft;
033:
034: /*#AxiomCalculus lnkAxiomCalculus;*/
035:
036: CExTerm(Term t) {
037: term = t;
038: sorte = (term.sort()).toString();
039: opname = (term.op()).toString();
040:
041: //the following builds the CExTerm structure recursivly
042: //calculating the fft-property as a side effect.
043:
044: if (term.arity() > 0) {
045:
046: //if a term is headed by a constructor and
047: //all subterms are function-free the term is function-free:
048:
049: params = new CExTerm[term.arity()];
050: boolean subs = true;
051: for (int i = 0; i < params.length; i++) {
052: params[i] = new CExTerm(term.sub(i));
053: subs = subs && params[i].isFFT();
054: }
055: fft = subs && this .isConstr();
056: } else {
057:
058: //if the term is a constructor or a variable it is function-free:
059:
060: fft = this .isConstr() || this .isVar();
061: }
062: }
063:
064: /**
065: * Generiere eine Liste der Parameter mit Reps fuer die nicht fft
066: */
067: public String paramsRep() {
068:
069: String paramsrep = new String("");
070: if (params.length > 0) {
071: paramsrep = params[0].Rep();
072: for (int i = 1; i < params.length; i++) {
073: paramsrep = paramsrep + "," + params[i].Rep();
074: }
075: }
076: return paramsrep;
077: }
078:
079: /**
080: * wird bisher nur auf sich selbst aufgerufen als mit sich selbst als param
081: */
082: public String isRep(CExTerm res) {
083: return "is(" + this .Rep() + "," + res.opname + "("
084: + res.paramsRep() + "))";
085: }
086:
087: /**
088: * Nur fuer die optimierte Version der Ausgabe wichtig:
089: * Daher getrennte von der eigentlichen Ausgabe.
090: */
091: public String interpretWith(CExTerm res) {
092: return "intpr("
093: + opname
094: + ",tup"
095: + params.length
096: + (params.length > 0 ? "(" + this .paramsRep() + ")"
097: : "") /* keine klammer 0 params */
098: + "," + res.Rep() + ")";
099: }
100:
101: /**
102: * suchTerm fuer den platzhalter des termes
103: */
104: public String searchTerm() {
105: return "search_" + sorte + "(" + this .Rep() + ")";
106: }
107:
108: /**
109: * Soll zurueckgeben ob fft oder nicht
110: */
111: public boolean isFFT() {
112: return fft;
113: }
114:
115: public boolean isConstr() {
116: return (term.op() instanceof ConstructorFunction); //@@@
117: }
118:
119: public boolean isVar() {
120: return (term.op() instanceof LogicVariable); //@@@
121: }
122:
123: /**
124: * Erstellung von Platzhaltern zu bestimmten Termen
125: * ueberprueft ob ueberhaupt einer benoetigt wird anhand
126: * der boolschen Variablen fft welche besagt ob
127: * es sich bei dem term um einen funktionsfreien Term handelt:
128: */
129: public String Rep() {
130: if (fft) {
131: return this .toString();
132: }
133: return "val(" + this .toString() + ")";
134: }
135:
136: public String toString() {
137:
138: if (params.length == 0) {
139: return opname;
140: }
141:
142: String s = new String();
143: for (int i = 0; i < params.length; i++) {
144: s = s + (i > 0 ? "," : "") + params[i].toString();
145: }
146: s = opname + "(" + s + ")";
147: return s;
148: }
149:
150: /**
151: * Hat ein FunctionTerm (z.B. ein konstruktor) keine Parameter
152: * wird an dieser stelle ein array der laenge 0 zurueckgegeben.
153: */
154: public CExTerm[] getParams() {
155:
156: if (params.length == 0) {
157: System.out
158: .println("Error: cannot getParams of non-FunctionTerm!");
159: return new CExTerm[0];
160: }
161: return params;
162: }
163:
164: }
|