Print error messages for unsupported SMTLIB commands during parsing

Author: daniel-raffler

src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java

@@ -287,7 +287,21 @@ private String sanitize(String formulaStr) {
         // We could keep track of the state of the stack and only consider the formulas that remain
         // on the stack at the end of the script. However, this does not seem worth it at the
         // moment. If needed, this feature can still be added later.
-        throw new IllegalArgumentException();
+        String message;
+        if (Tokenizer.isPushToken(token)) {
+          message = "(push ...)";
+        } else if (Tokenizer.isPopToken(token)) {
+          message = "(pop ...)";
+        } else if (Tokenizer.isResetAssertionsToken(token)) {
+          message = "(reset-assertions)";
+        } else if (Tokenizer.isResetToken(token)) {
+          message = "(reset)";
+        } else {
+          // Should be unreachable
+          throw new UnsupportedOperationException();
+        }
+        throw new IllegalArgumentException(
+            String.format("SMTLIB command '%s' is not supported when parsing formulas.", message));
 
       } else {
         // Remove everything else

src/org/sosy_lab/java_smt/basicimpl/Tokenizer.java

@@ -137,6 +137,15 @@ private static boolean matchesOneOf(String token, String... regexp) {
     return token.matches("\\(\\s*(" + String.join("|", regexp) + ")[\\S\\s]*");
   }
 
+  /**
+   * Check if the token is <code>(set-logic ..)</code>.
+   *
+   * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
+   */
+  public static boolean isSetLogicToken(String token) {
+    return matchesOneOf(token, "set-logic");
+  }
+
   /**
    * Check if the token is a function or variable declaration.
    *
@@ -165,16 +174,43 @@ public static boolean isAssertToken(String token) {
   }
 
   /**
-   * Check if the token is <code>(set-logic ..)</code>.
+   * Check if the token is an <code>(push ...)</code>.
    *
    * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
    */
-  public static boolean isSetLogicToken(String token) {
-    return matchesOneOf(token, "set-logic");
+  public static boolean isPushToken(String token) {
+    return matchesOneOf(token, "push");
+  }
+
+  /**
+   * Check if the token is an <code>(pop ...)</code>.
+   *
+   * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
+   */
+  public static boolean isPopToken(String token) {
+    return matchesOneOf(token, "pop");
+  }
+
+  /**
+   * Check if the token is an <code>(reset-assertions ...)</code>.
+   *
+   * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
+   */
+  public static boolean isResetAssertionsToken(String token) {
+    return matchesOneOf(token, "reset-assertions");
+  }
+
+  /**
+   * Check if the token is an <code>(reset)</code>.
+   *
+   * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
+   */
+  public static boolean isResetToken(String token) {
+    return matchesOneOf(token, "reset");
   }
 
   /**
-   * Check if the token is <code>(exit ...)</code>.
+   * Check if the token is <code>(exit)</code>.
    *
    * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
    */
@@ -197,6 +233,9 @@ public static boolean isExitToken(String token) {
    * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
    */
   public static boolean isUnsupportedToken(String token) {
-    return matchesOneOf(token, "push", "pop", "reset-assertions", "reset");
+    return isPushToken(token)
+        | isPopToken(token)
+        | isResetAssertionsToken(token)
+        | isResetToken(token);
   }
 }