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.proof.decproc;
012:
013: import java.io.BufferedReader;
014: import java.io.IOException;
015: import java.io.InputStream;
016: import java.io.InputStreamReader;
017: import java.util.Calendar;
018:
019: import de.uka.ilkd.key.java.Services;
020: import de.uka.ilkd.key.logic.Constraint;
021: import de.uka.ilkd.key.proof.Goal;
022: import de.uka.ilkd.key.proof.Node;
023:
024: /**
025: * Abstract base class for decision procedure wrappers.
026: * Provides common functionality for the ICS and Simplify wrappers.
027: */
028: public abstract class AbstractDecisionProcedure {
029:
030: protected final Goal goal;
031: protected final Constraint userConstraint;
032: protected final DecisionProcedureTranslationFactory dptf;
033: protected final Services services;
034: protected final Node node;
035:
036: public AbstractDecisionProcedure(Goal goal,
037: Constraint userConstraint,
038: DecisionProcedureTranslationFactory dptf, Services services) {
039: this .goal = goal;
040: this .node = goal.node();
041: this .userConstraint = userConstraint;
042: this .dptf = dptf;
043: this .services = services;
044: }
045:
046: public AbstractDecisionProcedure(Node node,
047: Constraint userConstraint,
048: DecisionProcedureTranslationFactory dptf, Services services) {
049: this .goal = null;
050: this .node = node;
051: this .userConstraint = userConstraint;
052: this .dptf = dptf;
053: this .services = services;
054: }
055:
056: /**
057: * the method responsible for making various calls to the underlying
058: * decision procedure with different Constraints
059: * @param lightWeight true iff only quantifier free formulas shall be
060: * considered.
061: */
062: public DecisionProcedureResult run(boolean lightWeight) {
063: ConstraintSet constraintSet = new ConstraintSet(node.sequent(),
064: userConstraint);
065: Constraint internalConstraint = constraintSet
066: .chooseConstraintSet();
067: DecisionProcedureResult res = runInternal(constraintSet,
068: lightWeight);
069: if (res.getResult()) {
070: return res;
071: } else {
072: if (constraintSet.addUserConstraint(userConstraint)) {
073: return runInternal(constraintSet, lightWeight);
074: } else {
075: return res;
076: }
077: }
078:
079: }
080:
081: /**
082: * the method responsible for making various calls to the underlying
083: * decision procedure with different Constraints
084: */
085: public DecisionProcedureResult run() {
086: return run(false);
087: }
088:
089: /**
090: * Invokes the actual decision procedure. This method is responsible for
091: * translating to the syntax of the external tool, as well as passing this
092: * as input to the tool and capturing its.
093: */
094: protected abstract DecisionProcedureResult runInternal(
095: ConstraintSet constraintSet, boolean lightWeight);
096:
097: private static String toStringLeadingZeros(int n, int width) {
098: String rv = "" + n;
099: while (rv.length() < width) {
100: rv = "0" + rv;
101: }
102: return rv;
103: }
104:
105: /**
106: * Constructs a date for use in log filenames.
107: */
108: protected static String getCurrentDateString() {
109: Calendar c = Calendar.getInstance();
110: StringBuffer sb = new StringBuffer();
111: String dateSeparator = "-";
112: String dateTimeSeparator = "_";
113: sb.append(toStringLeadingZeros(c.get(Calendar.YEAR), 4))
114: .append(dateSeparator).append(
115: toStringLeadingZeros(c.get(Calendar.MONTH) + 1,
116: 2)).append(dateSeparator).append(
117: toStringLeadingZeros(c.get(Calendar.DATE), 2))
118: .append(dateTimeSeparator).append(
119: toStringLeadingZeros(c
120: .get(Calendar.HOUR_OF_DAY), 2)
121: + "h").append(
122: toStringLeadingZeros(c.get(Calendar.MINUTE), 2)
123: + "m").append(
124: toStringLeadingZeros(c.get(Calendar.SECOND), 2)
125: + "s").append('.').append(
126: toStringLeadingZeros(c
127: .get(Calendar.MILLISECOND), 2));
128: return sb.toString();
129: }
130:
131: /** Read the input until end of file and return contents in a
132: * single string containing all line breaks. */
133: protected static String read(InputStream in) throws IOException {
134: String lineSeparator = System.getProperty("line.separator");
135: BufferedReader reader = new BufferedReader(
136: new InputStreamReader(in));
137: StringBuffer sb = new StringBuffer();
138: String line;
139: while ((line = reader.readLine()) != null) {
140: sb.append(line).append(lineSeparator);
141: }
142: return sb.toString();
143: }
144:
145: }
|