Princess: Disable all tests that require use operations with only non…

…-singleton strings as their arguments. Ostrich does not support such operations yet, although the feature will likely be added later. See uuverifiers/ostrich#88 for some details.

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

@@ -96,6 +96,17 @@ private void assertDistinct(StringFormula str1, StringFormula str2)
     assertThatFormula(smgr.equal(str1, str2)).isUnsatisfiable();
   }
 
+  private void requireVariableStringLiterals() {
+    // FIXME: Remove once support for operations on non-singleton Strings has been added
+    // See https://github.com/uuverifiers/ostrich/issues/88
+    assume()
+        .withMessage(
+            "Princess currently requires at least one of the arguments to be a "
+                + "singleton string")
+        .that(solverToUse())
+        .isNotEqualTo(Solvers.PRINCESS);
+  }
+
   // Tests
 
   @Test
@@ -114,6 +125,8 @@ public void testRegexAll3() throws SolverException, InterruptedException {
 
   @Test
   public void testRegexAllChar() throws SolverException, InterruptedException {
+    requireVariableStringLiterals();
+
     RegexFormula regexAllChar = smgr.allChar();
 
     assertThatFormula(smgr.in(smgr.makeString("a"), regexAllChar)).isSatisfiable();
@@ -130,6 +143,8 @@ public void testRegexAllChar() throws SolverException, InterruptedException {
 
   @Test
   public void testRegexAllCharUnicode() throws SolverException, InterruptedException {
+    requireVariableStringLiterals();
+
     RegexFormula regexAllChar = smgr.allChar();
 
     // Single characters.
@@ -161,6 +176,8 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti
 
   @Test
   public void testStringRegex2() throws SolverException, InterruptedException {
+    requireVariableStringLiterals();
+
     RegexFormula regex = smgr.concat(smgr.closure(a2z), smgr.makeRegex("ll"), smgr.closure(a2z));
     assertThatFormula(smgr.in(hello, regex)).isSatisfiable();
   }
@@ -248,6 +265,8 @@ public void testStringPrefixSuffixConcat() throws SolverException, InterruptedEx
 
   @Test
   public void testStringPrefixSuffix() throws SolverException, InterruptedException {
+    requireVariableStringLiterals();
+
     // check whether "prefix == suffix iff equal length"
     StringFormula prefix = smgr.makeVariable("prefix");
     StringFormula suffix = smgr.makeVariable("suffix");
@@ -390,6 +409,8 @@ public void testStringCompare() throws SolverException, InterruptedException {
     // TODO regression:
     // - CVC5 was able to solve this in v1.0.2, but no longer in v1.0.5
 
+    requireVariableStringLiterals();
+
     StringFormula var1 = smgr.makeVariable("0");
     StringFormula var2 = smgr.makeVariable("1");
     assertThatFormula(bmgr.and(smgr.lessOrEquals(var1, var2), smgr.greaterOrEquals(var1, var2)))
@@ -957,6 +978,8 @@ public void testConstStringContains() throws SolverException, InterruptedExcepti
 
   @Test
   public void testStringVariableContains() throws SolverException, InterruptedException {
+    requireVariableStringLiterals();
+
     StringFormula var1 = smgr.makeVariable("var1");
     StringFormula var2 = smgr.makeVariable("var2");
 
@@ -1005,6 +1028,8 @@ public void testStringContainsOtherVariable() throws SolverException, Interrupte
         .that(solverToUse())
         .isNotEqualTo(Solvers.Z3);
 
+    requireVariableStringLiterals();
+
     StringFormula var1 = smgr.makeVariable("var1");
     StringFormula var2 = smgr.makeVariable("var2");
 
@@ -1068,6 +1093,8 @@ public void testConstStringIndexOf() throws SolverException, InterruptedExceptio
 
   @Test
   public void testStringVariableIndexOf() throws SolverException, InterruptedException {
+    requireVariableStringLiterals();
+
     StringFormula var1 = smgr.makeVariable("var1");
     StringFormula var2 = smgr.makeVariable("var2");
     IntegerFormula intVar = imgr.makeVariable("intVar");
@@ -1152,6 +1179,8 @@ public void testStringPrefixImpliesPrefixIndexOf() throws SolverException, Inter
         .that(solverToUse())
         .isNoneOf(Solvers.Z3, Solvers.CVC4);
 
+    requireVariableStringLiterals();
+
     StringFormula var1 = smgr.makeVariable("var1");
     StringFormula var2 = smgr.makeVariable("var2");
 
@@ -1320,6 +1349,8 @@ public void testStringVariableReplacePrefix() throws SolverException, Interrupte
 
   @Test
   public void testStringVariableReplaceSubstring() throws SolverException, InterruptedException {
+    requireVariableStringLiterals();
+
     // I couldn't find stronger constraints in the implication that don't run endlessly.....
     StringFormula original = smgr.makeVariable("original");
     StringFormula prefix = smgr.makeVariable("prefix");
@@ -1422,6 +1453,8 @@ public void testStringVariableReplaceMiddle() throws SolverException, Interrupte
         .that(solverToUse())
         .isNoneOf(Solvers.CVC4, Solvers.Z3);
 
+    requireVariableStringLiterals();
+
     StringFormula original = smgr.makeVariable("original");
     StringFormula replacement = smgr.makeVariable("replacement");
     StringFormula replaced = smgr.makeVariable("replaced");
@@ -1473,6 +1506,8 @@ public void testStringVariableReplaceFront() throws SolverException, Interrupted
         .that(solverToUse())
         .isNoneOf(Solvers.Z3, Solvers.CVC5);
 
+    requireVariableStringLiterals();
+
     StringFormula var1 = smgr.makeVariable("var1");
     StringFormula var2 = smgr.makeVariable("var2");
     StringFormula var3 = smgr.makeVariable("var3");
@@ -1534,6 +1569,8 @@ public void testStringVariableReplaceAllConcatedString()
         .that(solverToUse())
         .isNotEqualTo(Solvers.Z3);
 
+    requireVariableStringLiterals();
+
     // 2 concats is the max number CVC4 supports without running endlessly
     for (int numOfConcats = 0; numOfConcats < 3; numOfConcats++) {
 
@@ -1568,6 +1605,8 @@ public void testStringVariableReplaceAllSubstring() throws SolverException, Inte
         .that(solverToUse())
         .isNotEqualTo(Solvers.Z3);
 
+    requireVariableStringLiterals();
+
     // I couldn't find stronger constraints in the implication that don't run endlessly.....
     StringFormula original = smgr.makeVariable("original");
     StringFormula prefix = smgr.makeVariable("prefix");