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: // This file is part of KeY - Integrated Deductive Software Design
10: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
11: // Universitaet Koblenz-Landau, Germany
12: // Chalmers University of Technology, Sweden
13: //
14: // The KeY system is protected by the GNU General Public License.
15: // See LICENSE.TXT for details.
16: package de.uka.ilkd.key.proof.decproc;
17:
18: import de.uka.ilkd.key.java.Services;
19: import de.uka.ilkd.key.logic.Sequent;
20: import de.uka.ilkd.key.logic.op.SetOfMetavariable;
21:
22: /**
23: * Returns the Translation classes for Java.
24: * @author daniels
25: */
26: public class JavaDecisionProcedureTranslationFactory implements
27: DecisionProcedureTranslationFactory {
28:
29: /* (non-Javadoc)
30: * @see de.uka.ilkd.key.proof.decproc.DecisionProcedureTranslationFactory#createSimplifyTranslation(de.uka.ilkd.key.logic.Sequent, de.uka.ilkd.key.proof.decproc.ConstraintSet, de.uka.ilkd.key.logic.op.SetOfMetavariable)
31: */
32: public SimplifyTranslation createSimplifyTranslation(
33: Sequent sequent, ConstraintSet cs,
34: SetOfMetavariable localmv, Services services,
35: boolean lightWeight) throws SimplifyException {
36: return new SimplifyTranslation(sequent, cs, localmv, services,
37: lightWeight);
38: }
39:
40: /* (non-Javadoc)
41: * @see de.uka.ilkd.key.proof.decproc.DecisionProcedureTranslationFactory#createICSTranslation(de.uka.ilkd.key.logic.Sequent, de.uka.ilkd.key.proof.decproc.ConstraintSet, de.uka.ilkd.key.logic.op.SetOfMetavariable)
42: */
43: public ICSTranslation createICSTranslation(Sequent sequent,
44: ConstraintSet cs, SetOfMetavariable localmv,
45: Services services) throws SimplifyException {
46: return new ICSTranslation(sequent, cs, localmv, services);
47: }
48:
49: /* (non-Javadoc)
50: * @see de.uka.ilkd.key.proof.decproc.DecisionProcedureTranslationFactory#createSmtTranslation(de.uka.ilkd.key.logic.Sequent, de.uka.ilkd.key.proof.decproc.ConstraintSet, de.uka.ilkd.key.logic.op.SetOfMetavariable)
51: */
52: public SmtAufliaTranslation createSmtAufliaTranslation(
53: Sequent sequent, Services services, boolean useQuantifiers) {
54: return new SmtAufliaTranslation(sequent, services,
55: useQuantifiers);
56: }
57: }
|