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;
12:
13: public abstract class DecisionProcedureSimplifyOp {
14:
15: // OPERATORS
16: /** the ususal 'negation' operator '-' */
17: public static final String NOT = "NOT";
18: /** the ususal 'and' operator '/\' (be A, B formulae then 'A /\ B'
19: * is true if and only if A is true and B is true */
20: public static final String AND = "AND";
21: /** the ususal 'or' operator '\/' (be A, B formulae then 'A \/ B'
22: * is true if and only if A is true or B is true */
23: public static final String OR = "OR";
24: /** the ususal 'implication' operator '->' (be A, B formulae then
25: * 'A -> B' is true if and only if A is false or B is true */
26: public static final String IMP = "IMPLIES";
27: /** the ususal 'equivalence' operator '<->' (be A, B formulae then
28: * 'A <-> B' is true if and only if A and B have the same truth
29: * value */
30: public static final String EQV = "IFF";
31:
32: /** the usual arithmetic operations: */
33: public static final String PLUS = "+";
34: public static final String MINUS = "-";
35: public static final String MULT = "*";
36:
37: /** the ususal 'equality' operator '=' */
38: public static final String EQUALS = "EQ";
39: /** the ususal 'less than' operator '<' */
40: public static final String LT = "<";
41: /** the ususal 'greater than' operator '>' */
42: public static final String GT = ">";
43: /** the ususal 'less than or equal' operator '<=' */
44: public static final String LEQ = "<=";
45: /** the ususal 'greater than or equal' operator '>=' */
46: public static final String GEQ = ">=";
47:
48: /** the ususal 'forall' operator 'all' (be A a formula then
49: * 'all x.A' is true if and only if for all elements d of the
50: * universe A{x<-d} (x substitued with d) is true */
51: public static final String ALL = "FORALL";
52: /** the ususal 'exists' operator 'ex' (be A a formula then
53: * 'ex x.A' is true if and only if there is at least one elements
54: * d of the universe such that A{x<-d} (x substitued with d) is true */
55: public static final String EX = "EXISTS";
56: /** the true constant */
57: public static final String TRUE = "TRUE";
58: /** the false constant */
59: public static final String FALSE = "FALSE";
60:
61: /** some facts about byte_MAX and friends */
62: public static final String LIMIT_FACTS = "(AND "
63: + "(< (long_MIN) (int_MIN))" + "(< (int_MIN) (short_MIN))"
64: + "(< (short_MIN) (byte_MIN))" + "(< (byte_MIN) 0)"
65: + "(< 0 (byte_MAX))" + "(< (byte_MAX) (short_MAX))"
66: + "(< (short_MAX) (int_MAX))" + "(< (int_MAX) (long_MAX))"
67: + "(EQ (byte_HALFRANGE) (+ (byte_MAX) 1))"
68: + "(EQ (short_HALFRANGE) (+ (short_MAX) 1))"
69: + "(EQ (int_HALFRANGE) (+ (int_MAX) 1))"
70: + "(EQ (long_HALFRANGE) (+ (long_MAX) 1))"
71: + "(EQ (byte_MIN) (- 0 (byte_HALFRANGE)))"
72: + "(EQ (short_MIN) (- 0 (short_HALFRANGE)))"
73: + "(EQ (int_MIN) (- 0 (int_HALFRANGE)))"
74: + "(EQ (long_MIN) (- 0 (long_HALFRANGE)))"
75: + "(EQ (byte_RANGE) (* 2 (byte_HALFRANGE)))"
76: + "(EQ (short_RANGE) (* 2 (short_HALFRANGE)))"
77: + "(EQ (int_RANGE) (* 2 (int_HALFRANGE)))"
78: + "(EQ (long_RANGE) (* 2 (long_HALFRANGE)))"
79: + "(EQ (byte_MAX) 127)" + "(EQ (short_MAX) 32767)" + ")\n";
80: }
|