001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //This file is part of KeY - Integrated Deductive Software Design
009: //Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: //The KeY system is protected by the GNU General Public License.
014: //See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof.decproc;
019:
020: /**
021: * This abstract class provides the operators defined in the SMT-Lib for
022: * the sublogics AUFLIA and QF_AUFLIA
023: *
024: * @author akuwertz
025: * @version 1.3, 09/29/2006 (Added quantifier support;
026: * all operators for logic AUFLIA are now implemented)
027: *
028: * @see <a href="http://goedel.cs.uiowa.edu/smtlib/logics/AUFLIA.smt">AUFLIA</a>
029: * @see <a href="http://goedel.cs.uiowa.edu/smtlib/logics/QF_AUFLIA.smt">QF_AUFLIA</a>
030: */
031: public abstract class DecisionProcedureSmtAufliaOp {
032:
033: /* OPERATORS in the AUFLIA-logic */
034:
035: // Logical connectives in formulae
036: /** the usual 'negation' operator '-' (interpreted connective) */
037: public static final String NOT = "not";
038: /** the usual 'and' operator '/\' (be A, B formulae then 'A /\ B'
039: * is true if and only if A is true and B is true (interpreted connective) */
040: public static final String AND = "and";
041: /** the usual 'or' operator '\/' (be A, B formulae then 'A \/ B'
042: * is true if and only if A is true or B is true (interpreted connective) */
043: public static final String OR = "or";
044: /** the usual 'equivalence' operator '<->' (be A, B formulae then
045: * 'A <-> B' is true if and only if A and B have the same truth
046: * value (interpreted connective) */
047: public static final String EQV = "iff";
048: /** the usual 'xor' or 'antivalence' operator 'xor' (be A, B formulae
049: * then 'A xor B' is true if and only if A and B have different truth
050: * values (interpreted connective) */
051: public static final String XOR = "xor";
052: /** the usual 'implication' operator '->' (be A, B formulae then
053: * 'A -> B' is true if and only if A is false or B is true (interpreted connective) */
054: public static final String IMP = "implies";
055:
056: // Interpreted predicate symbols
057: /** the usual 'equality' operator '=' (interpreted predicate) */
058: public static final String EQUALS = "=";
059: /** the usual 'less than or equal' operator '<=' (interpreted predicate) */
060: public static final String LEQ = "<=";
061: /** the usual 'less than' operator '<' (interpreted predicate) */
062: public static final String LT = "<";
063: /** the usual 'greater than or equal' operator '>=' (interpreted predicate) */
064: public static final String GEQ = ">=";
065: /** the usual 'greater than' operator '>' (interpreted predicate) */
066: public static final String GT = ">";
067: /** the true constant */
068: public static final String TRUE = "true";
069: /** the false constant */
070: public static final String FALSE = "false";
071: /** a pairwise different predicate for convenience (interpreted) */
072: public static final String DISTINCT = "distinct";
073:
074: // Quantifier symbols
075: /** the usual 'all' quantifier */
076: public static final String FORALL = "forall";
077: /** the usual 'exists' quantifier */
078: public static final String EXISTS = "exists";
079:
080: // Interpreted function symbols
081: /** the usual arithmetic 'plus' operater (interpreted function) */
082: public static final String PLUS = "+";
083: /** the usual arithmetic 'minus' operater (interpreted function) */
084: public static final String MINUS = "-";
085: /** the usual arithmetic 'multiply' operater (interpreted function) */
086: public static final String MULT = "*";
087: /** the unary minus, denoting the additive inverse of a number (interpreted function) */
088: public static final String UMINUS = "~";
089:
090: /** Array access operation for selecting an array element (interpreted function) */
091: public static final String SELECT = "select";
092: /** Array access operation for storing an element (interpreted function) */
093: public static final String STORE = "store";
094:
095: // Constructs for convenience
096: /** the let construct for terms (Be t a term, f a formula and x a (term) variable
097: * then 'let x=t in f' is semantically equivalent to the formula obtained from f
098: * by simultaneously replacing every occurrence of x in f by t */
099: public static final String LET = "let";
100:
101: /** the flet construct for formulae (Be f1, f0 formulae and e a (formula) variable
102: * then 'flet e=f0 in f1' is semantically equivalent to the formula obtained from f1 by
103: * simultaneously replacing every occurrence of e in f1 by f0 */
104: public static final String FLET = "flet";
105:
106: /** the if-then-else construct for terms, which is very similiar to the
107: * '?' operator in java (Be f a formula, t1 and t2 terms then 'ite (f, t1, t2)'
108: * evaluates to the value of t1 in every interpretation that makes f true,
109: * and to the value of t2 in every interpretation that makes f false */
110: public static final String ITE = "ite";
111:
112: /** the if-then-else construct for formulae, can be seen as Shannon Operator for
113: * formulae (be A, B and C formulae then 'if A then B else C' is true if and only
114: * if either A is true and B is true or A is false and C is true */
115: public static final String IFTHENELSE = "if_then_else";
116:
117: // Interpreted sort symbols
118: /** the usual set of integer numbers (interpreted sort) */
119: public static final String INT = "Int";
120: /** the usual functional array (interpreted sort) */
121: public static final String ARRAY = "Array";
122:
123: /** An array of <tt>String</tt>s containing all interpreted symbols in AUFLIA.
124: * <p>
125: /* It is used to ensure that the operator name of newly created uninterpreted symbols doesn't
126: * match an interpreted symbol. Therefore this array has to be updated on adding or removing
127: * operators */
128: private static final String[] allSmtOperators = { NOT, AND, OR,
129: EQV, XOR, IMP, EQUALS, GT, GEQ, LT, LEQ, TRUE, FALSE,
130: DISTINCT, PLUS, MINUS, MULT, UMINUS, SELECT, STORE, LET,
131: FLET, ITE, IFTHENELSE, INT, ARRAY };
132:
133: /** Returns an array containing all interpreted symbols in AUFLIA, which could be used to
134: * check if a function, predicate or variable name or any arbitrary identifier equals one of
135: * those interpreted symbols.
136: *
137: * @return an array of <tt>String</tt>s containing all interpreted symbols in AUFLIA
138: */
139: public static final String[] getAllSmtOperators() {
140: return (String[]) allSmtOperators.clone();
141: }
142:
143: //*ToDo* Is this needed for SMT AUFLIA?
144: // Will be added if needed
145: // /** some facts about byte_MAX and friends */
146: // public static final String LIMIT_FACTS =
147: // "(and "
148: // + "(< (long_MIN) (int_MIN))"
149: // + "(< (int_MIN) (short_MIN))"
150: // + "(< (short_MIN) (byte_MIN))"
151: // + "(< (byte_MIN) 0)"
152: // + "(< 0 (byte_MAX))"
153: // + "(< (byte_MAX) (short_MAX))"
154: // + "(< (short_MAX) (int_MAX))"
155: // + "(< (int_MAX) (long_MAX))"
156: // + "(EQ (byte_HALFRANGE) (+ (byte_MAX) 1))"
157: // + "(EQ (short_HALFRANGE) (+ (short_MAX) 1))"
158: // + "(EQ (int_HALFRANGE) (+ (int_MAX) 1))"
159: // + "(EQ (long_HALFRANGE) (+ (long_MAX) 1))"
160: // + "(EQ (byte_MIN) (- 0 (byte_HALFRANGE)))"
161: // + "(EQ (short_MIN) (- 0 (short_HALFRANGE)))"
162: // + "(EQ (int_MIN) (- 0 (int_HALFRANGE)))"
163: // + "(EQ (long_MIN) (- 0 (long_HALFRANGE)))"
164: // + "(EQ (byte_RANGE) (* 2 (byte_HALFRANGE)))"
165: // + "(EQ (short_RANGE) (* 2 (short_HALFRANGE)))"
166: // + "(EQ (int_RANGE) (* 2 (int_HALFRANGE)))"
167: // + "(EQ (long_RANGE) (* 2 (long_HALFRANGE)))"
168: // + "(EQ (byte_MAX) 127)"
169: // + "(EQ (short_MAX) 32767)"
170: // + ")\n";
171: }
|