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: * Implementors will know whether to create a DecProcTranslation object for Java
24: * or for ASM. This is necessary since the Translation classes are not visible
25: * to callers of the DecisionProcedure classes.
26: *
27: * @author daniels
28: */
29: public interface DecisionProcedureTranslationFactory {
30: SimplifyTranslation createSimplifyTranslation(Sequent sequent,
31: ConstraintSet cs, SetOfMetavariable localmv,
32: Services services, boolean lightWeight)
33: throws SimplifyException;
34:
35: ICSTranslation createICSTranslation(Sequent sequent,
36: ConstraintSet cs, SetOfMetavariable localmv,
37: Services services) throws SimplifyException;
38:
39: SmtAufliaTranslation createSmtAufliaTranslation(Sequent sequent,
40: Services services, boolean useQuantifiers);
41: }
|