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: package de.uka.ilkd.key.rule;
09:
10: import de.uka.ilkd.key.java.Services;
11: import de.uka.ilkd.key.logic.Constraint;
12: import de.uka.ilkd.key.logic.Name;
13: import de.uka.ilkd.key.proof.Goal;
14: import de.uka.ilkd.key.proof.decproc.AbstractDecisionProcedure;
15: import de.uka.ilkd.key.proof.decproc.DecisionProcedureCVC3;
16: import de.uka.ilkd.key.proof.decproc.DecisionProcedureTranslationFactory;
17:
18: /**
19: * CVC3 is as its predecessor CVC3 an SMT prover. This rule allows its invocation
20: * from within KeY using the SMT-LIb interface.
21: * @see AbstractIntegerRule
22: */
23: public class CVC3IntegerRule extends AbstractIntegerRule {
24:
25: /** A mere constructor.
26: *
27: * @param resultWindow a <tt>boolean</tt> indicating if the results of this <tt>Rule</tt>
28: * should be presented in a separate window
29: * @param dptf the <tt>DecisionProcedureTranslationFactory</tt> to be used
30: */
31: public CVC3IntegerRule(boolean resultWindow,
32: DecisionProcedureTranslationFactory dptf) {
33: super (new Name("Decision procedure CVC3"), resultWindow, dptf);
34: }
35:
36: /** A mere constructor for convenience. Creates an <tt>CVC3IntegerRule</tt> with
37: * <tt>resultWindow</tt> set to <tt>true</tt>
38: *
39: * @param dptf the <tt>DecisionProcedureTranslationFactory</tt> to be used
40: */
41: public CVC3IntegerRule(DecisionProcedureTranslationFactory dptf) {
42: this (true, dptf);
43: }
44:
45: /* (non-Javadoc)
46: * @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)
47: */
48: protected AbstractDecisionProcedure getDecisionProcedure(Goal goal,
49: Constraint userConstraint, Services services) {
50: return new DecisionProcedureCVC3(goal, dptf, services);
51: }
52:
53: public AbstractIntegerRule clone(
54: DecisionProcedureTranslationFactory dptf) {
55: return new CVC3IntegerRule(showResults, dptf);
56: }
57:
58: }
|