| java.lang.Object
 de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAufliaOp
| DecisionProcedureSmtAufliaOp | | abstract public class DecisionProcedureSmtAufliaOp (Code) | | This abstract class provides the operators defined in the SMT-Lib for
the sublogics AUFLIA and QF_AUFLIA
author:
akuwertz
version:
1.3, 09/29/2006 (Added quantifier support;
version:
all operators for logic AUFLIA are now implemented)
See Also: AUFLIA
See Also: QF_AUFLIA |
| Method Summary | |
| final public static String[] | getAllSmtOperators()
Returns an array containing all interpreted symbols in AUFLIA, which could be used to
check if a function, predicate or variable name or any arbitrary identifier equals one of
those interpreted symbols. |
| AND | | final public static String AND(Code) | | the usual 'and' operator '/\' (be A, B formulae then 'A /\ B'
is true if and only if A is true and B is true (interpreted connective)
|
| ARRAY | | final public static String ARRAY(Code) | | the usual functional array (interpreted sort)
|
| DISTINCT | | final public static String DISTINCT(Code) | | a pairwise different predicate for convenience (interpreted)
|
| EQUALS | | final public static String EQUALS(Code) | | the usual 'equality' operator '=' (interpreted predicate)
|
| EQV | | final public static String EQV(Code) | | the usual 'equivalence' operator '<->' (be A, B formulae then
'A <-> B' is true if and only if A and B have the same truth
value (interpreted connective)
|
| EXISTS | | final public static String EXISTS(Code) | | the usual 'exists' quantifier
|
| FALSE | | final public static String FALSE(Code) | | the false constant
|
| FLET | | final public static String FLET(Code) | | the flet construct for formulae (Be f1, f0 formulae and e a (formula) variable
then 'flet e=f0 in f1' is semantically equivalent to the formula obtained from f1 by
simultaneously replacing every occurrence of e in f1 by f0
|
| FORALL | | final public static String FORALL(Code) | | the usual 'all' quantifier
|
| GEQ | | final public static String GEQ(Code) | | the usual 'greater than or equal' operator '>=' (interpreted predicate)
|
| GT | | final public static String GT(Code) | | the usual 'greater than' operator '>' (interpreted predicate)
|
| IFTHENELSE | | final public static String IFTHENELSE(Code) | | the if-then-else construct for formulae, can be seen as Shannon Operator for
formulae (be A, B and C formulae then 'if A then B else C' is true if and only
if either A is true and B is true or A is false and C is true
|
| IMP | | final public static String IMP(Code) | | the usual 'implication' operator '->' (be A, B formulae then
'A -> B' is true if and only if A is false or B is true (interpreted connective)
|
| INT | | final public static String INT(Code) | | the usual set of integer numbers (interpreted sort)
|
| ITE | | final public static String ITE(Code) | | the if-then-else construct for terms, which is very similiar to the
'?' operator in java (Be f a formula, t1 and t2 terms then 'ite (f, t1, t2)'
evaluates to the value of t1 in every interpretation that makes f true,
and to the value of t2 in every interpretation that makes f false
|
| LEQ | | final public static String LEQ(Code) | | the usual 'less than or equal' operator '<=' (interpreted predicate)
|
| LET | | final public static String LET(Code) | | the let construct for terms (Be t a term, f a formula and x a (term) variable
then 'let x=t in f' is semantically equivalent to the formula obtained from f
by simultaneously replacing every occurrence of x in f by t
|
| LT | | final public static String LT(Code) | | the usual 'less than' operator '<' (interpreted predicate)
|
| MINUS | | final public static String MINUS(Code) | | the usual arithmetic 'minus' operater (interpreted function)
|
| MULT | | final public static String MULT(Code) | | the usual arithmetic 'multiply' operater (interpreted function)
|
| NOT | | final public static String NOT(Code) | | the usual 'negation' operator '-' (interpreted connective)
|
| OR | | final public static String OR(Code) | | the usual 'or' operator '\/' (be A, B formulae then 'A \/ B'
is true if and only if A is true or B is true (interpreted connective)
|
| PLUS | | final public static String PLUS(Code) | | the usual arithmetic 'plus' operater (interpreted function)
|
| SELECT | | final public static String SELECT(Code) | | Array access operation for selecting an array element (interpreted function)
|
| STORE | | final public static String STORE(Code) | | Array access operation for storing an element (interpreted function)
|
| UMINUS | | final public static String UMINUS(Code) | | the unary minus, denoting the additive inverse of a number (interpreted function)
|
| XOR | | final public static String XOR(Code) | | the usual 'xor' or 'antivalence' operator 'xor' (be A, B formulae
then 'A xor B' is true if and only if A and B have different truth
values (interpreted connective)
|
| getAllSmtOperators | | final public static String[] getAllSmtOperators()(Code) | | Returns an array containing all interpreted symbols in AUFLIA, which could be used to
check if a function, predicate or variable name or any arbitrary identifier equals one of
those interpreted symbols.
an array of Strings containing all interpreted symbols in AUFLIA |
|
|