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:
018: package de.uka.ilkd.key.parser.ocl;
019:
020: import de.uka.ilkd.key.java.Services;
021: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
022: import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
023: import de.uka.ilkd.key.logic.*;
024: import de.uka.ilkd.key.logic.op.ListOfLogicVariable;
025: import de.uka.ilkd.key.logic.op.LogicVariable;
026: import de.uka.ilkd.key.logic.op.SLListOfLogicVariable;
027: import de.uka.ilkd.key.logic.sort.Sort;
028:
029: /**
030: * Converts between formulas and boolean terms.
031: */
032: class FormulaBoolConverter {
033: private static final String VARNAME_PREFIX = "_oclFBC";
034: private static final TermBuilder tb = TermBuilder.DF;
035:
036: private final NamespaceSet nss;
037: private final Term trueLitTerm;
038: private final Sort boolSort;
039:
040: private int varCounter = 0;
041: private ListOfTerm termsToAdd = SLListOfTerm.EMPTY_LIST;
042: private ListOfLogicVariable introducedVars = SLListOfLogicVariable.EMPTY_LIST;
043:
044: /**
045: * @param serv used for adding the created variables to the
046: * appropriate namespace
047: *
048: */
049: public FormulaBoolConverter(Services serv, NamespaceSet nss) {
050: this .nss = nss;
051: trueLitTerm = serv.getTypeConverter().convertToLogicElement(
052: BooleanLiteral.TRUE);
053: boolSort = serv.getJavaInfo().getKeYJavaType(
054: PrimitiveType.JAVA_BOOLEAN).getSort();
055: }
056:
057: /**
058: * Sets the counter which is used for naming the introduced variables.
059: */
060: public void setVariableCounter(int value) {
061: varCounter = value;
062: }
063:
064: /**
065: * Returns the current value of the counter which is used for naming the
066: * introduced variables.
067: */
068: public int getVariableCounter() {
069: return varCounter;
070: }
071:
072: /**
073: * Adds axiomatisations for all variables which have been introduced so far
074: * to a term.
075: *
076: */
077: public Term addAxioms(Term term) {
078: Term result = term;
079:
080: Term termToAdd = null;
081: if (termsToAdd.size() == 1) {
082: termToAdd = termsToAdd.head();
083: } else if (termsToAdd.size() > 1) {
084: termToAdd = tb.and(termsToAdd.toArray());
085: }
086:
087: if (termToAdd != null) {
088: Term impTerm = tb.imp(termToAdd, result);
089: result = tb.all(introducedVars.toArray(), impTerm);
090: }
091:
092: return result;
093: }
094:
095: /**
096: * Converts a term to a formula, if it is boolean; otherwise, just returns
097: * the term unchanged.
098: */
099: public Term convertBoolToFormula(Term term) {
100: Term result = term;
101:
102: if (term != null && term.sort() == boolSort) {
103: result = tb.equals(term, trueLitTerm);
104: }
105:
106: return result;
107: }
108:
109: /**
110: * Converts a term to a boolean term, if it is a formula; otherwise, just
111: * returns the term unchanged. For the conversion, a logic variable is
112: * introduced, which must later be axiomatised by calling addAxioms().
113: */
114: public Term convertFormulaToBool(Term term) {
115: Term result = term;
116:
117: if (term != null && term.sort() == Sort.FORMULA) {
118: Name name = new Name(VARNAME_PREFIX + varCounter++);
119: LogicVariable var = new LogicVariable(name, boolSort);
120:
121: nss.variables().add(var);
122: introducedVars = introducedVars.prepend(var);
123:
124: Term varTerm = tb.var(var);
125: Term varTrueTerm = tb.equals(varTerm, trueLitTerm);
126: Term termToAdd = tb.equiv(term, varTrueTerm);
127:
128: termsToAdd = termsToAdd.append(termToAdd);
129:
130: result = varTerm;
131: }
132:
133: return result;
134: }
135:
136: /**
137: * Converts those terms in a list which are formulas to boolean
138: * terms, and leaves the others unchanged.
139: */
140: public ListOfTerm convertFormulasToBool(ListOfTerm list) {
141: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
142:
143: IteratorOfTerm it = list.iterator();
144: while (it.hasNext()) {
145: result = result.append(convertFormulaToBool(it.next()));
146: }
147:
148: return result;
149: }
150:
151: /**
152: * Converts those terms in a list of OCLEntities which are formulas
153: * to boolean terms, and leaves the others unchanged.
154: */
155: public ListOfTerm convertFormulasToBool(ListOfOCLEntity list) {
156: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
157:
158: IteratorOfOCLEntity it = list.iterator();
159: while (it.hasNext()) {
160: result = result.append(it.next().getTerm());
161: }
162:
163: return convertFormulasToBool(result);
164: }
165:
166: }
|