File tree Expand file tree Collapse file tree 2 files changed +8
-4
lines changed
src/org/sosy_lab/java_smt/basicimpl Expand file tree Collapse file tree 2 files changed +8
-4
lines changed Original file line number Diff line number Diff line change @@ -281,7 +281,7 @@ private String sanitize(String formulaStr) {
281281 // Keep only declaration, definitions and assertion
282282 builder .append (token ).append ('\n' );
283283
284- } else if (Tokenizer .isUnsupportedToken (token )) {
284+ } else if (Tokenizer .isForbiddenToken (token )) {
285285 // Throw an exception if the script contains commands like (pop) or (reset) that change the
286286 // state of the assertion stack.
287287 // We could keep track of the state of the stack and only consider the formulas that remain
Original file line number Diff line number Diff line change @@ -219,9 +219,9 @@ public static boolean isExitToken(String token) {
219219 }
220220
221221 /**
222- * Check if this is an unsupported token.
222+ * Check if this is a forbidden token.
223223 *
224- * <p>The list of unsupported tokens contains:
224+ * <p>The list of forbidden tokens contains:
225225 *
226226 * <ul>
227227 * <li>push
@@ -230,9 +230,13 @@ public static boolean isExitToken(String token) {
230230 * <li>reset
231231 * </ul>
232232 *
233+ * <p>Forbidden tokens manipulate the stack and are not supported while parsing SMT-lIB2 string.
234+ * When a forbidden token is found parsing should be aborted by throwing an {@link
235+ * IllegalArgumentException} exception.
236+ *
233237 * <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
234238 */
235- public static boolean isUnsupportedToken (String token ) {
239+ public static boolean isForbiddenToken (String token ) {
236240 return isPushToken (token )
237241 | isPopToken (token )
238242 | isResetAssertionsToken (token )
You can’t perform that action at this time.
0 commit comments