SolverFormulaIOTest: check declared function symbols, also for arrays.

Author: kfriedberger

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

@@ -14,11 +14,15 @@
 import static com.google.common.truth.TruthJUnit.assume;
 
 import com.google.common.base.Splitter;
-import com.google.common.collect.HashMultiset;
+import com.google.common.collect.HashMultimap;
+import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Iterables;
-import com.google.common.collect.Multiset;
+import com.google.common.collect.Multimap;
 import com.google.common.truth.TruthJUnit;
+import java.util.Collection;
 import java.util.function.Supplier;
+import java.util.regex.Pattern;
+import org.junit.AssumptionViolatedException;
 import org.junit.Test;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
@@ -105,6 +109,10 @@ public class SolverFormulaIOTest extends SolverBasedTest0.ParameterizedSolverBas
           + "(assert  (let (($x35 (and (xor q (= (+ a b) c)) (>= a b)))) (let (($x9 (= a b))) (and"
           + " (and (or $x35 u) q) (and $x9 $x35)))))";
 
+  private static final Collection<String> ABDE = ImmutableSet.of("a", "b", "d", "e");
+  private static final Collection<String> AQBCU = ImmutableSet.of("a", "q", "b", "c", "u");
+  private static final Collection<String> QBCU = ImmutableSet.of("q", "b", "c", "u");
+
   @Test
   public void logicsParseTest() throws SolverException, InterruptedException {
     requireParser();
@@ -278,83 +286,83 @@ public void funcsDumpTest() {
   @Test
   public void parseMathSatTestParseFirst1() throws SolverException, InterruptedException {
     requireParser();
-    compareParseWithOrgParseFirst(MATHSAT_DUMP1, this::genBoolExpr);
+    compareParseWithOrgParseFirst(MATHSAT_DUMP1, this::genBoolExpr, ABDE);
   }
 
   @Test
   public void parseMathSatTestExprFirst1() throws SolverException, InterruptedException {
     requireParser();
-    compareParseWithOrgExprFirst(MATHSAT_DUMP1, this::genBoolExpr);
+    compareParseWithOrgExprFirst(MATHSAT_DUMP1, this::genBoolExpr, ABDE);
   }
 
   @Test
   public void parseSmtinterpolTestParseFirst1() throws SolverException, InterruptedException {
     requireParser();
-    compareParseWithOrgParseFirst(SMTINTERPOL_DUMP1, this::genBoolExpr);
+    compareParseWithOrgParseFirst(SMTINTERPOL_DUMP1, this::genBoolExpr, ABDE);
   }
 
   @Test
   public void parseSmtinterpolTestExprFirst1() throws SolverException, InterruptedException {
     requireParser();
-    compareParseWithOrgExprFirst(SMTINTERPOL_DUMP1, this::genBoolExpr);
+    compareParseWithOrgExprFirst(SMTINTERPOL_DUMP1, this::genBoolExpr, ABDE);
   }
 
   @Test
   public void parseZ3TestParseFirst1() throws SolverException, InterruptedException {
     requireParser();
-    compareParseWithOrgParseFirst(Z3_DUMP1, this::genBoolExpr);
+    compareParseWithOrgParseFirst(Z3_DUMP1, this::genBoolExpr, ABDE);
   }
 
   @Test
   public void parseZ3TestExprFirst1() throws SolverException, InterruptedException {
     requireParser();
-    compareParseWithOrgExprFirst(Z3_DUMP1, this::genBoolExpr);
+    compareParseWithOrgExprFirst(Z3_DUMP1, this::genBoolExpr, ABDE);
   }
 
   @Test
   public void parseMathSatTestParseFirst2() throws SolverException, InterruptedException {
     requireParser();
     requireIntegers();
-    compareParseWithOrgParseFirst(MATHSAT_DUMP2, this::redundancyExprGen);
+    compareParseWithOrgParseFirst(MATHSAT_DUMP2, this::redundancyExprGen, AQBCU);
   }
 
   @Test
   public void parseMathSatTestExprFirst2() throws SolverException, InterruptedException {
     requireParser();
-    compareParseWithOrgExprFirst(MATHSAT_DUMP2, this::redundancyExprGen);
+    compareParseWithOrgExprFirst(MATHSAT_DUMP2, this::redundancyExprGen, AQBCU);
   }
 
   @Test
   public void parseSmtinterpolSatTestParseFirst2() throws SolverException, InterruptedException {
     requireParser();
     requireIntegers();
-    compareParseWithOrgParseFirst(SMTINTERPOL_DUMP2, this::redundancyExprGen);
+    compareParseWithOrgParseFirst(SMTINTERPOL_DUMP2, this::redundancyExprGen, QBCU);
   }
 
   @Test
   public void parseSmtinterpolSatTestExprFirst2() throws SolverException, InterruptedException {
     requireParser();
-    compareParseWithOrgExprFirst(SMTINTERPOL_DUMP2, this::redundancyExprGen);
+    compareParseWithOrgExprFirst(SMTINTERPOL_DUMP2, this::redundancyExprGen, QBCU);
   }
 
   @Test
   public void parseZ3SatTestParseFirst2() throws SolverException, InterruptedException {
     requireParser();
     requireIntegers();
-    compareParseWithOrgParseFirst(Z3_DUMP2, this::redundancyExprGen);
+    compareParseWithOrgParseFirst(Z3_DUMP2, this::redundancyExprGen, AQBCU);
   }
 
   @Test
   public void parseZ3SatTestExprFirst2() throws SolverException, InterruptedException {
     requireParser();
-    compareParseWithOrgExprFirst(Z3_DUMP2, this::redundancyExprGen);
+    compareParseWithOrgExprFirst(Z3_DUMP2, this::redundancyExprGen, AQBCU);
   }
 
   @Test
   public void parseMathSatTestExprFirst3() throws SolverException, InterruptedException {
     requireParser();
     requireIntegers();
-    compareParseWithOrgExprFirst(MATHSAT_DUMP3, this::functionExprGen);
+    compareParseWithOrgExprFirst(MATHSAT_DUMP3, this::functionExprGen, ImmutableSet.of("fun_b"));
   }
 
   @Test
@@ -399,7 +407,7 @@ public void funDeclareTest() {
     String formDump = mgr.dumpFormula(imgr.equal(calc, int1)).toString();
 
     // check if dumped formula fits our specification
-    checkThatFunOnlyDeclaredOnce(formDump);
+    checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("fun_a", "fun_b"));
     checkThatAssertIsInLastLine(formDump);
     checkThatDumpIsParseable(formDump);
   }
@@ -419,17 +427,41 @@ public void funDeclareTest2() {
     String formDump = mgr.dumpFormula(imgr.equal(calc, int1)).toString();
 
     // check if dumped formula fits our specification
-    checkThatFunOnlyDeclaredOnce(formDump);
+    checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("fun_a"));
+    checkThatAssertIsInLastLine(formDump);
+    checkThatDumpIsParseable(formDump);
+  }
+
+  @Test
+  public void funDeclareWithArrayTest() {
+    requireIntegers();
+    requireArrays();
+
+    IntegerFormula idx = imgr.makeVariable("idx");
+    IntegerFormula int1 = imgr.makeNumber(1);
+    IntegerFormula int2 = imgr.makeNumber(2);
+
+    // assert (((select (store arr idx 2) 1) 2)
+    var arr = amgr.makeArray("arr", FormulaType.IntegerType, FormulaType.IntegerType);
+    var store = amgr.store(arr, idx, int2);
+    var select = amgr.select(store, int1);
+    var query = imgr.equal(int2, select);
+
+    String formDump = mgr.dumpFormula(query).toString();
+
+    // check if dumped formula fits our specification
+    checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("idx", "arr"));
     checkThatAssertIsInLastLine(formDump);
     checkThatDumpIsParseable(formDump);
   }
 
-  private void compareParseWithOrgExprFirst(String textToParse, Supplier<BooleanFormula> fun)
+  private void compareParseWithOrgExprFirst(
+      String textToParse, Supplier<BooleanFormula> fun, Collection<String> expectedDeclarations)
       throws SolverException, InterruptedException {
     // Boolector will fail this anyway since bools are bitvecs for btor
     TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR);
     // check if input is correct
-    checkThatFunOnlyDeclaredOnce(textToParse);
+    checkThatFunOnlyDeclaredOnce(textToParse, expectedDeclarations);
     checkThatAssertIsInLastLine(textToParse);
 
     // actual test
@@ -438,12 +470,13 @@ private void compareParseWithOrgExprFirst(String textToParse, Supplier<BooleanFo
     assertThatFormula(parsedForm).isEquivalentTo(expr);
   }
 
-  private void compareParseWithOrgParseFirst(String textToParse, Supplier<BooleanFormula> fun)
+  private void compareParseWithOrgParseFirst(
+      String textToParse, Supplier<BooleanFormula> fun, Collection<String> expectedDeclarations)
       throws SolverException, InterruptedException {
     // Boolector will fail this anyway since bools are bitvecs for btor
     TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR);
     // check if input is correct
-    checkThatFunOnlyDeclaredOnce(textToParse);
+    checkThatFunOnlyDeclaredOnce(textToParse, expectedDeclarations);
     checkThatAssertIsInLastLine(textToParse);
 
     // actual test
@@ -452,19 +485,25 @@ private void compareParseWithOrgParseFirst(String textToParse, Supplier<BooleanF
     assertThatFormula(parsedForm).isEquivalentTo(expr);
   }
 
-  private void checkThatFunOnlyDeclaredOnce(String formDump) {
+  private void checkThatFunOnlyDeclaredOnce(
+      String formDump, Collection<String> expectedDeclarations) {
     // Boolector will fail this anyway since bools are bitvecs for btor
     TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR);
-    Multiset<String> funDeclares = HashMultiset.create();
+    Multimap<String, String> funDeclares = HashMultimap.create();
 
+    final Pattern declareFunRegex = Pattern.compile("\\(declare-fun\\s+(?<name>\\S+)\\s*");
     for (String line : Splitter.on('\n').split(formDump)) {
       if (line.startsWith("(declare-fun ")) {
-        funDeclares.add(line.replaceAll("\\s+", ""));
+        var matcher = declareFunRegex.matcher(line);
+        var name = matcher.find() ? matcher.group(1) : line.replaceAll("\\s+", "");
+        funDeclares.put(name, line.replaceAll("\\s+", ""));
       }
     }
 
+    assertThat(funDeclares.keySet()).containsExactlyElementsIn(expectedDeclarations);
+
     // remove non-duplicates
-    funDeclares.entrySet().removeIf(pStringEntry -> pStringEntry.getCount() <= 1);
+    funDeclares.keySet().removeIf(pStringEntry -> funDeclares.get(pStringEntry).size() <= 1);
     assertWithMessage("duplicate function declarations").that(funDeclares).isEmpty();
   }
 
@@ -487,8 +526,13 @@ private void checkThatAssertIsInLastLine(String dump) {
 
   @SuppressWarnings("CheckReturnValue")
   private void checkThatDumpIsParseable(String dump) {
-    requireParser();
-    mgr.parse(dump);
+    try {
+      requireParser();
+      mgr.parse(dump);
+    } catch (AssumptionViolatedException ave) {
+      // ignore, i.e., do not report test-case as skipped.
+    }
+    ;
   }
 
   private BooleanFormula genBoolExpr() {