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.proof.decproc.translation;
12:
13: import de.uka.ilkd.key.logic.op.Operator;
14:
15: /** This interface represents a rule for translating KeY <tt>Term</tt>s into SMT-LIB
16: * <tt>Term</tt>s and <tt>Formula</tt>e.
17: * <p>
18: * A rule offers two methods: One for checking if this rule is applicable on a given
19: * <tt>Operator</tt> of a <tt>Term</tt> and one that actually performs the translation
20: *
21: * @author akuwertz
22: * @version <pre>
23: * 1.0,
24: * 1.1, 01/28/2006 (Added comments)</pre>
25: */
26: public interface IOperatorTranslation {
27:
28: /** Returns <tt>true</tt> if this translation rule can be applied to the given
29: * <tt>Operator</tt>
30: *
31: * @param op the <tt>Operator</tt> to be checked for applicability
32: * @return true iff the specified <tt>Operator</tt> can be translated by this rule
33: */
34: public boolean isApplicable(Operator op);
35:
36: /** Returns an SMT-LIB <tt>Term</tt> or <tt>Formula</tt> as translation result of the
37: * specified <tt>Operator</tt>
38: *
39: * @param op the <tt>Operator</tt> to be translated
40: * @param ttVisitor the <tt>TermTranslationVisitor</tt> on which the translation is performed
41: * @return an SMT-LIB <tt>Term</tt> or <tt>Formula</tt> representing the translation of
42: * the specified <tt>Operator</tt>
43: *
44: * @throws IllegalArgumentException if one of the arguments of the specified <tt>Operator</tt>
45: * on the stack of <tt>ttVisitor</tt> has an illegal type
46: * @throws UnsupportedOperationException if the specified <tt>Operator</tt> can not be
47: * translated
48: */
49: public Object translate(Operator op,
50: TermTranslationVisitor ttVisitor);
51:
52: }
|