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.DecisionProcedureCVCLite;
19: import de.uka.ilkd.key.proof.decproc.DecisionProcedureTranslationFactory;
20:
21: /** This class represents the <tt>Rule</tt> for the simplification of a <tt>Goal</tt> by the
22: * decicion procedure CVCLite
23: *
24: * @author akuwertz
25: * @version 1.0, 04/07/2006
26: */
27:
28: public class CVCLiteIntegerRule 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 CVCLiteIntegerRule(boolean resultWindow,
37: DecisionProcedureTranslationFactory dptf) {
38: super (new Name("Decision procedure CVCLite"), resultWindow,
39: dptf);
40: }
41:
42: /** A mere constructor for convenience. Creates an <tt>CVCLiteIntegerRule</tt> with
43: * <tt>resultWindow</tt> set to <tt>true</tt>
44: *
45: * @param dptf the <tt>DecisionProcedureTranslationFactory</tt> to be used
46: */
47: public CVCLiteIntegerRule(DecisionProcedureTranslationFactory dptf) {
48: this (true, dptf);
49: }
50:
51: /* (non-Javadoc)
52: * @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)
53: */
54: protected AbstractDecisionProcedure getDecisionProcedure(Goal goal,
55: Constraint userConstraint, Services services) {
56: return new DecisionProcedureCVCLite(goal, dptf, services);
57: }
58:
59: public AbstractIntegerRule clone(
60: DecisionProcedureTranslationFactory dptf) {
61: return new CVCLiteIntegerRule(showResults, dptf);
62: }
63:
64: }
|