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: //
09: //
10:
11: package de.uka.ilkd.key.rule;
12:
13: import de.uka.ilkd.key.java.Services;
14: import de.uka.ilkd.key.logic.Constraint;
15: import de.uka.ilkd.key.logic.Name;
16: import de.uka.ilkd.key.proof.Goal;
17: import de.uka.ilkd.key.proof.decproc.AbstractDecisionProcedure;
18: import de.uka.ilkd.key.proof.decproc.DecisionProcedureDummyTranslation;
19: import de.uka.ilkd.key.proof.decproc.DecisionProcedureTranslationFactory;
20:
21: /** This class represents the <tt>Rule</tt> for a mere translation of the current sequent into an
22: * SMT <tt>Benchmark</tt>
23: *
24: * @author akuwertz
25: * @version 1.0, 07/26/2006
26: */
27:
28: public class SmtTranslationIntegerRule extends AbstractIntegerRule {
29:
30: /** A mere constructor.
31: *
32: * @param resultWindow a <tt>boolean</tt> indicating if the results of this <tt>Rule</tt>
33: * should be presented in a separate window
34: * @param dptf the <tt>DecisionProcedureTranslationFactory</tt> to be used
35: */
36: public SmtTranslationIntegerRule(boolean resultWindow,
37: DecisionProcedureTranslationFactory dptf) {
38: super (new Name(
39: "Decision Procedure Dummy for mere SMT Translation"),
40: resultWindow, dptf);
41: }
42:
43: /** A mere constructor for convenience. Creates an <tt>SmtTranslationIntegerRule</tt> instance with
44: * <tt>resultWindow</tt> set to <tt>true</tt>
45: *
46: * @param dptf the <tt>DecisionProcedureTranslationFactory</tt> to be used
47: */
48: public SmtTranslationIntegerRule(
49: DecisionProcedureTranslationFactory dptf) {
50: this (true, dptf);
51: }
52:
53: /* (non-Javadoc)
54: * @see de.uka.ilkd.key.rule.AbstractIntegerRule#getDecisionProcedure(de.uka.ilkd.key.proof.Goal, de.uka.ilkd.key.logic.Constraint, de.uka.ilkd.key.java.Services)
55: */
56: protected AbstractDecisionProcedure getDecisionProcedure(Goal goal,
57: Constraint userConstraint, Services services) {
58: return new DecisionProcedureDummyTranslation(goal, dptf,
59: services);
60: }
61:
62: public AbstractIntegerRule clone(
63: DecisionProcedureTranslationFactory dptf) {
64: return new SmtTranslationIntegerRule(showResults, dptf);
65: }
66:
67: }
|