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.proof.decproc.smtlib;
019:
020: import java.util.HashSet;
021: import java.util.Iterator;
022: import java.util.Set;
023: import java.util.Vector;
024:
025: /** Represents a benchmark as defined in the SMT-Lib specification.
026: * <p>
027: * A benchmark thereby represents a closed first order formula with additional information attached
028: * to it. To be exact, the formula is built over a sublogic of first order logic with equality,
029: * namely (QF_)AUFLIA in this case.
030: * <p>
031: * The <tt>String</tt> representation of a <tt>Benchmark</tt> can be given to any decision
032: * procedure supporting the SMT-LIB format and the (QF_)AUFLIA sublogic, to decide satisfiability
033: * of the represented formula.<br>
034: * To get a <tt>String</tt> representation appropriate for SMT-LIB satisfiability solvers for an
035: * arbitrary <tt>Formula</tt> (SMT-LIB), the <tt>setFormula</tt> method must be called on a
036: * <tt>Benchmark</tt> instance with that <tt>Formula</tt> as argument. Calling to <tt>toString</tt>
037: * method on this <tt>Benchmark</tt> will then generate an appropriate <tt>String</tt>
038: * representation
039: *
040: * @author akuwertz
041: * @version 1.3, 03/28/2006 (Minor fixes)
042: *
043: * @see <a href="http://combination.cs.uiowa.edu/smtlib/">SMT-LIB</a>
044: */
045:
046: public class Benchmark {
047:
048: /** The name of this <tt>Benchmark</tt> */
049: private final String bmName;
050: /** The ":logic" attribute of this <tt>Benchmark</tt> */
051: private String bmLogic;
052: /** The ":source" attribute of this <tt>Benchmark</tt>; empty by default */
053: private String source = "";
054: /** The ":formula" attribute of this <tt>Benchmark</tt>, representing its <tt>Formula</tt> */
055: private Formula formula;
056: /** The assumptions of this <tt>Benchmark</tt> */
057: private Formula[] assumptions;
058: /** The notes of this <tt>Benchmark</tt> */
059: private String notes = "";
060:
061: /* The follow String variables represent the immutable pieces of a Benchmark, for
062: * internal use only */
063: private static final String bmBegin = "(benchmark ";
064: private static final String bmDefaultName = "SmtAuflia_";
065: private static final String bmSource = "\n :source { Translated automatically from a KeY proof obligation.\n"
066: + " The KeY project - Integrated Deductive Software Design:\n"
067: + " Universitaet Karlsruhe, Germany\n"
068: + " Universitaet Koblenz-Landau, Germany\n"
069: + " Chalmers University of Technology, Sweden\n"
070: + " => Visit http://www.key-project.org for more information\n"
071: + " }\n\n";
072: private static final String bmStatus = " :status unknown\n";
073: private static final String bmLogicQF_AUFLIA = " :logic QF_AUFLIA\n";
074: private static final String bmLogicAUFLIA = " :logic AUFLIA\n";
075: private static final String bmExtraFun = " :extrafuns ";
076: private static final String bmExtraPred = " :extrapreds ";
077: private static final String bmExtraSort = " :extrasort ";
078: private static final String bmAssumption = " :assumption ";
079: private static final String bmFormula = " :formula ";
080: private static final String bmNotesStart = "\n\n :notes \"";
081: private static final String bmNotesEnd = " \"";
082: private static final String bmEnd = "\n)";
083:
084: /* String constants for error messages during Benchmark creation */
085: private static final String noFormulaSetError = "No formula has yet been set!";
086: private static final String noLogicSetError = "No logic has yet been specified!";
087:
088: /* Constructor */
089:
090: /** Just a constructor
091: *
092: * @param name the name of the <tt>Benchmark</tt> to be created. If the given <tt>String</tt>
093: * is <tt>null</tt>, the name is set to "SmtAuflia_Benchmark" by default
094: */
095: public Benchmark(String name) {
096: bmName = bmDefaultName + name;
097: assumptions = new Formula[0];
098: }
099:
100: /* Public method implementation */
101:
102: /** Sets the ":logic" attribute of this <tt>Formula</tt> by specifying if quantifiers should
103: * be supported or not
104: * @param useQuantifiers if true, quantifiers will be supported (AUFLIA); else QF_AUFLIA
105: * will be used as logic
106: */
107: public void setLogic(boolean useQuantifiers) {
108: bmLogic = bmLogicAUFLIA;
109: if (!useQuantifiers)
110: bmLogic = bmLogicQF_AUFLIA;
111: }
112:
113: /** Sets the <tt>Formula</tt> of this <tt>Benchmark</tt> to the specified <tt>Formula</tt>
114: *
115: * @param f the <tt>Formula</tt> this <tt>Benchmark</tt> should represent
116: */
117: public void setFormula(Formula f) {
118: formula = f;
119: }
120:
121: /** Returns the <tt>Formula</tt> of this <tt>Benchmark</tt>
122: *
123: * @return the <tt>Formula</tt> of this <tt>Benchmark</tt>
124: */
125: public Formula getFormula() {
126: return formula;
127: }
128:
129: /** Sets the assumptions of this Benchmark to the specified <tt>Formula</tt> array
130: * @param assumptions the <tt>Formula</tt> array of assumptions under which the
131: * <tt>Formula</tt> of this <tt>Benchmark</tt> should be checked
132: */
133: public void setAssumptions(Formula[] assumptions) {
134: this .assumptions = assumptions;
135: }
136:
137: /** Returns the assumptions of this <tt>Benchmark</tt>
138: *
139: * @return a <tt>Formula</tt> array containing the assumptions under which the <tt>Formula</tt>
140: * of this <tt>Benchmark</tt> should be checked
141: */
142: public Formula[] getAssuptions() {
143: return assumptions;
144: }
145:
146: /** Sets the notes of this Benchmark to the specified <tt>String</tt>
147: * @param notes the <tt>String</tt> representing to value of the ":notes" attribute for
148: * this <tt>Benchmark</tt>
149: */
150: public void setNotes(String notes) {
151: this .notes = bmNotesStart + notes + bmNotesEnd;
152: }
153:
154: /** Sets the ":source" attribute of this <tt>Benchmark</tt> to a predefined value.
155: * <p>
156: * Before this function is called on a <tt>Benchmark</tt> for the first time, it won't contain
157: * any ":source" attribute
158: */
159: public void setSource() {
160: source = bmSource;
161: }
162:
163: /** Returns a String representation of this <tt>Benchmark</tt>, including the String
164: * representations of its <tt>Formula</tt> and its extra uninterpreted functions.
165: * The returned representation satisfies the specifications of the SMT-Lib
166: * benchmark definition
167: *
168: * @return The String representation of this <tt>Benchmark</tt>
169: * @throws IllegalStateException if this method is called on a <tt>Benchmark</tt> whichout
170: * specifying its logic or setting its <tt>Formula</tt> first,
171: * or if its <tt>Formula</tt> is set to <tt>null</tt>
172: */
173: public String toString() {
174:
175: if (formula == null)
176: throw new IllegalStateException(noFormulaSetError);
177: if (bmLogic == null)
178: throw new IllegalStateException(noLogicSetError);
179:
180: // Assemble benchmark head
181: String representation = bmBegin + bmName + source + bmStatus
182: + bmLogic;
183:
184: // Assemble the ":extrafuns" , ":extrapreds" and ":extrasorts" attributes
185: UninterpretedFuncTerm[] extraFuns = (UninterpretedFuncTerm[]) formula
186: .getUIF().toArray(
187: new UninterpretedFuncTerm[formula.getUIF()
188: .size()]);
189: Vector uiPred = formula.getUIPredicates();
190: UninterpretedPredFormula[] extraPreds = (UninterpretedPredFormula[]) uiPred
191: .toArray(new UninterpretedPredFormula[uiPred.size()]);
192: Set freeSorts = new HashSet();
193: // First ":extrafuns"
194: String exFuncDefs = "";
195: for (int i = 0; i < extraFuns.length; i++) {
196: // Add uninterpreted sorts
197: freeSorts.addAll(extraFuns[i].getSignature().getUiSorts());
198: // Assemble ":extrafuns" attribute for each uninterpreted function
199: exFuncDefs += bmExtraFun + "(("
200: + extraFuns[i].getFunction() + " "
201: + extraFuns[i].getSignature().toString() + "))\n";
202: }
203: // Then ":extrapreds"
204: String exPredDefs = "";
205: for (int i = 0; i < extraPreds.length; i++) {
206: // Add uninterpreted sorts
207: freeSorts.addAll(extraPreds[i].getSignature().getUiSorts());
208: // Assemble ":extrapreds" attribute for each uninterpreted predicate
209: exPredDefs += bmExtraPred + "((" + extraPreds[i].getOp()
210: + " " + extraPreds[i].getSignature().toString()
211: + "))\n";
212: }
213: // At last assemble ":extrasort" attribute for each of the collected sort strings
214: String exSortDefs = "";
215: Iterator sortIterator = freeSorts.iterator();
216: while (sortIterator.hasNext())
217: exSortDefs += bmExtraSort + "(("
218: + (String) sortIterator.next() + "))\n";
219:
220: // Assemble the ":assumption" attributes
221: String allAssumptions = "";
222: for (int i = 0; i < assumptions.length; i++) {
223: allAssumptions += bmAssumption + assumptions[i].toString()
224: + "\n";
225: }
226:
227: // Assemble the ":formula" attribute
228: String formulaAttr = bmFormula + formula.toString();
229:
230: // Attach the assembled attributes to the header and return the result
231: representation += exSortDefs + exFuncDefs + exPredDefs
232: + allAssumptions + formulaAttr + notes;
233: return representation + bmEnd;
234: }
235: }
|