SMTInperpol-FormulaCreator: change long ITE-cascade into switch-case.
@@ -258,20 +258,21 @@ class SmtInterpolFormulaCreator
return FunctionDeclarationKind.IMPLIES;
} else if (symbol == t.mXor) {
return FunctionDeclarationKind.XOR;
+ }
// Polymorphic function symbols are more difficult.
- } else if (symbol.getName().equals("=")) {
+ switch (symbol.getName()) {
+ case "=":
return FunctionDeclarationKind.EQ;
- } else if (symbol.getName().equals("distinct")) {
+ case "distinct":
return FunctionDeclarationKind.DISTINCT;
- } else if (symbol.getName().equals("ite")) {
+ case "ite":
return FunctionDeclarationKind.ITE;
- } else if (symbol.getName().equals("select")) {
+ case "select":
return FunctionDeclarationKind.SELECT;
- } else if (symbol.getName().equals("store")) {
+ case "store":
return FunctionDeclarationKind.STORE;
- } else {
-
+ default:
// TODO: other declaration kinds!
return FunctionDeclarationKind.OTHER;
}
