Cleaned up ParserSymbolsEscapedTest an reduced the number of test inputs

Author: daniel-raffler

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

@@ -783,7 +783,8 @@ public Object convertValue(
   }
 
   /** Variable names (symbols) can be wrapped with "|". This function removes those chars. */
-  protected static String dequote(String s) {
+  @VisibleForTesting
+  public static String dequote(String s) {
     int l = s.length();
     if (l >= 2 && s.charAt(0) == '|' && s.charAt(l - 1) == '|') {
       return s.substring(1, l - 1);

src/org/sosy_lab/java_smt/test/ParserSymbolsEscapedTest.java

@@ -13,21 +13,23 @@
 import static com.google.common.truth.Truth.assertThat;
 import static com.google.common.truth.TruthJUnit.assume;
 import static org.junit.Assert.assertThrows;
-import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.RESERVED;
+import static org.sosy_lab.java_smt.basicimpl.FormulaCreator.dequote;
 
 import com.google.common.collect.FluentIterable;
-import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
 import java.util.Collection;
 import org.junit.Before;
 import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
 import org.junit.runners.Parameterized.Parameter;
 import org.junit.runners.Parameterized.Parameters;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
 
-public class ParserSymbolsEscapedTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
+@RunWith(Parameterized.class)
+public class ParserSymbolsEscapedTest extends SolverBasedTest0 {
 
   public static ImmutableSet<String> TEST_SYMBOLS =
       ImmutableSet.of(
@@ -46,110 +48,43 @@ public class ParserSymbolsEscapedTest extends SolverBasedTest0.ParameterizedSolv
           ".8",
           "+34",
           "-32",
+
           // Quoted symbols from the standard:
           "this is a quoted symbol",
           "so is\nthis one",
           "\" can occur too",
           "af klj ^*0 asfe2 (&*)&(#^ $ > > >?\" ’]]984",
+
           // Some more edge cases
           "",
           " ",
+          ",",
+          "'",
           "\n",
           "ꯍ",
           "#b101011",
           "#b2",
           "1",
+          ",1",
           "01",
           "1.0",
           "01.0",
           "#xA04",
           "#xR04",
-          "#o70");
-
-  private static final ImmutableList<String> reserved =
-      ImmutableList.of(
-          // Reserved
+          "#o70",
           "_",
-          "!",
-          "as",
-          "let",
-          "exists",
           "forall",
-          "match",
-          "par",
-
-          // Commands
           "assert",
-          "check-sat",
-          "check-sat-assuming",
-          "declare-const",
-          "declare-datatype",
-          "declare-datatypes",
-          "declare-fun",
-          "declare-sort",
-          "define-fun",
           "define-fun-rec",
-          "define-funs-rec",
-          "define-sort",
-          "echo",
-          "exit",
-          "get-assertions",
-          "get-assignment",
-          "get-info",
-          "get-model",
-          "get-option",
-          "get-proof",
-          "get-unsat-assumptions",
-          "get-unsat-core",
-          "get-value",
-          "pop",
-          "push",
-          "reset",
-          "reset-assertions",
-          "set-info",
-          "set-logic",
-          "set-option",
-
-          // Predefined symbols
-          // Array
-          "select",
           "store",
-          // Bitvector
           "concat",
-          "extract",
-          "bvnot",
-          "bvneg",
-          "bvand",
-          "bvor",
-          "bvadd",
-          "bvmul",
-          "bvudiv",
-          "bvurem",
-          "bvshl",
-          "bvlshr",
-          "true",
-          "false",
-          "not",
-          "=>",
-          "and",
-          "or",
-          "xor",
-          "=",
-          "distinct",
-          "ite"
-          // TODO: Add more theories
-          );
+          "=");
 
   @Parameters(name = "{0},{1}")
   public static Collection<Object[]> data() {
     ImmutableSet.Builder<Object[]> builder = ImmutableSet.builder();
     for (Solvers solver : Solvers.values()) {
-      for (String symbol :
-          FluentIterable.concat(
-              RESERVED,
-              TEST_SYMBOLS,
-              VariableNamesTest.NAMES,
-              VariableNamesTest.UNSUPPORTED_NAMES)) {
+      for (String symbol : FluentIterable.concat(TEST_SYMBOLS)) {
         for (String variant :
             ImmutableSet.of(
                 symbol,
@@ -179,45 +114,21 @@ public void init() {
     requireParser();
   }
 
-  /** Is this <code>True</code> if the symbol is a reserved keyword in the SMTLIB standard. */
-  private static boolean isReserved(String pSymbol) {
-    return RESERVED.contains(pSymbol);
-  }
-
-  /** <code>True</code> if the symbol is a simple symbol according to the SMTLIB standard. */
-  private static boolean isSimple(String pSymbol) {
-    return pSymbol.matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$")
-        && !Character.isDigit(pSymbol.charAt(0))
-        && !isReserved(pSymbol);
-  }
-
   /**
    * <code>True</code> if the symbol is a valid symbol according to the SMTLIB standard.
    *
-   * <p>Valid symbols can be either <code>simple</code> symbols or <code>quoted</code> symbols.
+   * <p>This function is stricter than {@link FormulaCreator#isValidName(String)} and won't allow
+   * names such as <code>"a \nb"</code> without any SMTLIB quotes.
    */
   private static boolean isValid(String pSymbol) {
     if (pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|")) {
-      return FormulaCreator.isValidName(removeQuotes(pSymbol));
+      return FormulaCreator.isValidName(dequote(pSymbol));
     } else {
       return pSymbol.matches("^[~!@$%^&*_\\-+=<>.?\\/0-9a-zA-Z]+$")
           && FormulaCreator.isValidName(pSymbol);
     }
   }
 
-  /**
-   * Remove quotes from the symbol.
-   *
-   * <p>If the symbol is not quoted, return it unchanged.
-   */
-  private static String removeQuotes(String pSymbol) {
-    if (pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|")) {
-      return pSymbol.substring(1, pSymbol.length() - 1);
-    } else {
-      return pSymbol;
-    }
-  }
-
   /**
    * Add quotes to the symbol
    *
@@ -227,22 +138,16 @@ private static String addQuotes(String pSymbol) {
     return "|" + pSymbol + "|";
   }
 
+  /** Returns <code>True</code> if the symbol is quoted */
   private static boolean hasQuotes(String pSymbol) {
     return pSymbol.length() >= 2 && pSymbol.startsWith("|") && pSymbol.endsWith("|");
   }
 
   /**
-   * Return the canonical representation of the symbol.
+   * Parse a variable definition in the SMTLIB format and return the term.
    *
-   * <p>The symbol will have quotes if and only if the same symbol without quotes would not be legal
-   * in SMTLIB.
+   * <p>Returns a variable or a UF depending on the value of <code>asUfSymbol</code>
    */
-  private static String canonical(String pSymbol) {
-    String noquotes = removeQuotes(pSymbol);
-    return isSimple(noquotes) ? noquotes : addQuotes(noquotes);
-  }
-
-  /** Parse a variable definition in the SMTLIB format and return the term. */
   private BooleanFormula parseSymbol(String pSymbol, boolean asUfSymbol) {
     String sort = solver == Solvers.BITWUZLA ? "(_ BitVec 8)" : "Int";
     String query =
@@ -254,10 +159,12 @@ private BooleanFormula parseSymbol(String pSymbol, boolean asUfSymbol) {
     return mgr.parse(query);
   }
 
+  /* Only consider valid SMTLIB symbols for this test */
   private void forValidSymbols(String pSymbol) {
     assume().that(isValid(pSymbol)).isTrue();
   }
 
+  /* Only consider invalid symbols. */
   private void forInvalidSymbols(String pSymbol) {
     assume().that(isValid(pSymbol)).isFalse();
   }