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