01: // This file is part of KeY - Integrated Deductive Software Design
02: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
03: // Universitaet Koblenz-Landau, Germany
04: // Chalmers University of Technology, Sweden
05: //
06: // The KeY system is protected by the GNU General Public License.
07: // See LICENSE.TXT for details.
08: //This file is part of KeY - Integrated Deductive Software Design
09: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
10: // Universitaet Koblenz-Landau, Germany
11: // Chalmers University of Technology, Sweden
12: //
13: //The KeY system is protected by the GNU General Public License.
14: //See LICENSE.TXT for details.
15: //
16: //
17:
18: package de.uka.ilkd.key.proof.decproc;
19:
20: import de.uka.ilkd.key.java.Services;
21: import de.uka.ilkd.key.proof.Goal;
22:
23: /** This class is just a dummy to enable translating a <tt>Sequent</tt> into a <tt>Benchmark</tt>
24: * and archiving it without calling an external decision procedure
25: *
26: * @author akuwertz
27: * @version 1.0, 07/26/2006
28: */
29:
30: public class DecisionProcedureDummyTranslation extends
31: DecisionProcedureSmtAuflia {
32:
33: /** A mere constructor.
34: *
35: * @param goal the <tt>Goal</tt> which should be checked for satisfiability
36: * @param dptf the <tt>DecisionProcedureTranslationFactory</tt> used to ranslate the the
37: * sequent of the goal
38: * @param services the <tt>Services</tt> used during the translation process
39: */
40: public DecisionProcedureDummyTranslation(Goal goal,
41: DecisionProcedureTranslationFactory dptf, Services services) {
42: super (goal, dptf, services);
43: }
44:
45: /* (non-Javadoc)
46: * @see de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAuflia#execDecProc()
47: */
48: protected DecisionProcedureResult execDecProc() {
49: // Do nothing, just a dummy!
50: return null;
51: }
52:
53: }
|