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 java.util.Vector;
014:
015: import de.uka.ilkd.key.logic.Axiom;
016: import de.uka.ilkd.key.logic.Term;
017: import de.uka.ilkd.key.logic.ldt.ADT;
018: import de.uka.ilkd.key.logic.op.Op;
019: import de.uka.ilkd.key.logic.op.Operator;
020:
021: /**
022: * This class generates the clauses for the axioms. It contains
023: * the complete Axiom Transformation algorithm as described in
024: * Wolfgang Ahrendt's PHD-Thesis
025: * @author Sonja Pieper
026: * @version 0.1
027: */
028: public class AxiomCalculus extends SortCalculus {
029:
030: private ADT adt;
031: private Clauses axioms;
032:
033: /*#CExTerm lnkCExTerm;*/
034:
035: public AxiomCalculus(ADT a) {
036: super (a.getSorts());
037:
038: //@@@ visitor?variables
039: adt = a;
040: axioms = new Clauses();
041: axioms.add(this .axiomClauses());
042: this .all.add(axioms);
043:
044: }
045:
046: public Clauses getAxiomClauses() {
047: return axioms;
048: }
049:
050: /**
051: * This method runs the loop so every axiom can be transformed with
052: * <code>transAxiom(...)</code> and then added to the list of axiomclauses
053: * @return the list of clauses with the transformed axioms
054: */
055: public Clauses axiomClauses() {
056:
057: Clauses cs = new Clauses();
058:
059: Vector axiomlist = adt.getAxioms();
060: for (int axiomidx = 0; axiomidx < axiomlist.size(); axiomidx++) {
061: cs.add(this .transAxiom((Axiom) axiomlist
062: .elementAt(axiomidx)));
063: }
064: return cs;
065: }
066:
067: /**
068: * This is the start of the actual Transformation of the axioms.
069: * @return The completely transformed axiom in the calculus clause format
070: */
071: public Clause transAxiom(Axiom axiom) {
072:
073: String ante = new String();
074:
075: /* @@@ generate antecedent:
076: vars = axiom.freeVars();
077: while(vars.hasMoreElements()){
078: Term v = vars.next();
079: ante = ante + v.sort() + "("+ v.toString() +")";
080: }
081: */
082:
083: String cnsq = this .transDisj(axiom.getAxiomTerm());
084:
085: //Axiom zu den Klauseln hinzufuegen:
086: return new Clause(ante, cnsq);
087: }
088:
089: /**
090: * Since an Axiom is a disjunktion of equalities or unequalities
091: * one calls this funktion before being able to transform the equalities
092: * which is done in the transLit function. A literal in this case
093: * means an equality.
094: *
095: * @param term the first call gets the full axiom then it works down
096: * the disjunctions recursively.
097: * @returns An mgtp-formatted string containing a disjunction of
098: * transformed equalities or inequalities.
099: */
100: public String transDisj(Term term) {
101: Operator operator = term.op();
102:
103: if ((operator == Op.EQV) || (operator == Op.NOT)) {
104: return this .transLit(term);
105: } else if (operator == Op.OR) {
106: return this .transDisj(term.sub(0)) + ";"
107: + this .transDisj(term.sub(1));
108: }
109:
110: return "Error Wrong Top Level Operator";
111: }
112:
113: /**
114: * This method works with equalities mainly and calls on the
115: * transformation methods for the two sides of the equality.
116: *
117: * @param lit A literal meaning either an equality or inequality
118: * @return An mgtp formatted string which contains the transformed literal
119: */
120: public String transLit(Term lit) {
121:
122: boolean eq = true;
123: if (lit.op() == Op.NOT) {
124: lit = lit.sub(0);
125: eq = false;
126: }
127:
128: if (eq) {
129: CExTerm[] t = { new CExTerm(lit.sub(0)),
130: new CExTerm(lit.sub(1)) };
131:
132: if (CounterExample.config.optimize) {
133:
134: //this is the optimized version of the transformation for equalities:
135: if ((t[0].isVar() || t[0].isConstr())
136: && (t[1].isVar() || t[1].isConstr())) {
137: return "same(" + t[0].Rep() + "," + t[1].Rep()
138: + ")" + TransTermListe(t);
139: } else if (t[0].isVar() || t[0].isConstr()) {
140: return t[1].interpretWith(t[0])
141: + TransTermListe(t[1].getParams())
142: + TransTerm(t[0]);
143: } else {
144: return t[0].interpretWith(t[1])
145: + TransTermListe(t[0].getParams())
146: + TransTerm(t[1]);
147: }
148: } else {//Unoptimized version of the transformation which is not as efficient
149: return "same(" + t[0].Rep() + "," + t[1].Rep() + ")"
150: + TransTermListe(t);
151: }
152:
153: } else { //different:
154: CExTerm[] t = { new CExTerm(lit.sub(0)),
155: new CExTerm(lit.sub(1)) };
156: return "different(" + t[0].Rep() + "," + t[1].Rep() + ")"
157: + TransTermListe(t);
158: }
159:
160: }
161:
162: /**
163: * ruft auf jedem CExTerm des Arrays CExTerm auf und baut eine Konjunktion zusammen
164: * "," wird in der CExTerm eingefuegt!
165: */
166:
167: public String TransTermListe(CExTerm[] termliste) {
168: String conj = new String();
169: for (int i = 0; i < termliste.length; i++) {
170: conj = conj + TransTerm(termliste[i]);
171: }
172: return conj;
173: }
174:
175: /**
176: * Eigentliche Rekursion;
177: * nachbedingung: nach ausfuehrung fuer Transterm muss bekannt
178: * sein ob ein ffterm nun fft ist oder nicht!!!!
179: */
180: public String TransTerm(CExTerm term) {
181:
182: if (term.isFFT()) {
183: return "";
184: } else if (term.isConstr()) {
185: return ",\n\t\t" + term.isRep(term)
186: + TransTermListe(term.getParams());
187: } else {
188: return ",\n\t\t" + term.interpretWith(term) + ","
189: + term.searchTerm()
190: + TransTermListe(term.getParams());
191: }
192: }
193:
194: }
|