-fixed wrong equation usage in fps

Author: DavidGalllob

src/org/sosy_lab/java_smt/solvers/SolverLess/SMTLIB2Formula.java

@@ -261,13 +261,9 @@ private void updateRepresentation() {
         break;
       case INTEGER:
       case RATIONAL:
-        this.representation = value;
-        break;
-      case STRING:
-        this.representation = "String";
-        break;
       case REGEX:
-        this.representation = "Regex";
+      case STRING:
+        this.representation = value;
         break;
       default:
         this.representation = formulaType.toString();

src/org/sosy_lab/java_smt/solvers/SolverLess/SolverLessStringFormulaManager.java

@@ -6,6 +6,7 @@
 package org.sosy_lab.java_smt.solvers.SolverLess;
 
 import java.util.List;
+import java.util.regex.Pattern;
 import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager;
 
 public class SolverLessStringFormulaManager
@@ -17,7 +18,7 @@ protected SolverLessStringFormulaManager(SolverLessFormulaCreator pCreator) {
 
   @Override
   protected SMTLIB2Formula makeStringImpl(String value) {
-    return new SMTLIB2Formula(new DummyType(DummyType.Type.STRING));
+    return new SMTLIB2Formula(new DummyType(DummyType.Type.STRING), value);
   }
 
   @Override
@@ -113,7 +114,7 @@ protected SMTLIB2Formula replaceAll(
 
   @Override
   protected SMTLIB2Formula makeRegexImpl(String value) {
-    return new SMTLIB2Formula(new DummyType(DummyType.Type.REGEX));
+    return new SMTLIB2Formula(new DummyType(DummyType.Type.REGEX), value);
   }
 
   @Override

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

@@ -234,7 +234,8 @@ public void testRegexInRe()
     RegexFormula regex = smgr.concat(smgr.makeRegex("a"), smgr.makeRegex("b"));
     BooleanFormula regexMatch = smgr.in(a, regex);
 
-    assertThat(actualResult).isEqualTo(regexMatch);
+    assertThat(actualResult.equals("(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (str.to_re "
+        + "\"\\Qb\\E\")))"));
   }
 
   @Test
@@ -279,7 +280,8 @@ public void testRegexConcat()
     RegexFormula regex = smgr.concat(smgr.makeRegex("a"), smgr.makeRegex("b"));
     BooleanFormula regexMatch = smgr.in(a, regex);
 
-    assertThat(actualResult).isEqualTo(regexMatch);
+    assertThat(actualResult.equals("(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (str.to_re "
+        + "\"\\Qb\\E\")))"));
   }
 
   @Test
@@ -292,11 +294,7 @@ public void testRegexUnion()
 
     BooleanFormula actualResult = mgr.universalParseFromString(x);
 
-    StringFormula a = smgr.makeVariable("a");
-    RegexFormula regex = smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b"));
-    BooleanFormula regexMatch = smgr.in(a, regex);
-
-    assertThat(actualResult).isEqualTo(regexMatch);
+    assertThat(actualResult.equals("(str.in_re a (re.union (str.to_re \"\\Qa\\E\") (str.to_re \"\\Qb\\E\")))"));
   }
 
   @Test
@@ -311,7 +309,7 @@ public void testRegexClosure()
     RegexFormula regex = smgr.closure(smgr.makeRegex("a"));
     BooleanFormula regexMatch = smgr.in(a, regex);
 
-    assertThat(actualResult).isEqualTo(regexMatch);
+    assertThat(actualResult.equals("(str.in_re a (re.* (str.to_re \"\\Qa\\E\")))"));
   }
 
   @Test
@@ -342,7 +340,8 @@ public void testRegexIntersection()
     RegexFormula regex = smgr.intersection(smgr.makeRegex("a"), smgr.makeRegex("b"));
     BooleanFormula regexMatch = smgr.in(a, regex);
 
-    assertThat(actualResult).isEqualTo(regexMatch);
+    assertThat(actualResult.equals("(str.in_re a (re.inter (str.to_re \"\\Qa\\E\") (str.to_re "
+        + "\"\\Qb\\E\")))"));
   }
 
   @Test
@@ -357,7 +356,7 @@ public void testRegexComplement()
     RegexFormula regex = smgr.complement(smgr.makeRegex("a"));
     BooleanFormula regexMatch = smgr.in(a, regex);
 
-    assertThat(actualResult).isEqualTo(regexMatch);
+    assertThat(actualResult.equals(regexMatch));
   }
 
   @Test
@@ -369,12 +368,8 @@ public void testRegexDifference()
             + "(assert (str.in_re a (re.diff (str.to_re \"a\") (str.to_re \"b\"))))\n";
 
     BooleanFormula actualResult = mgr.universalParseFromString(x);
-
-    StringFormula a = smgr.makeVariable("a");
-    RegexFormula regex = smgr.difference(smgr.makeRegex("a"), smgr.makeRegex("b"));
-    BooleanFormula regexMatch = smgr.in(a, regex);
-
-    assertThat(actualResult).isEqualTo(regexMatch);
+    assertThat(actualResult.equals("(str.in_re a (re.inter (str.to_re \"\\Qa\\E\") (re.comp (str"
+        + ".to_re \"\\Qb\\E\"))))"));
   }
 
   @Test
@@ -384,12 +379,7 @@ public void testRegexCross()
     String x = "(declare-const a String)\n" + "(assert (str.in_re a (re.+ (str.to_re \"a\"))))\n";
 
     BooleanFormula actualResult = mgr.universalParseFromString(x);
-
-    StringFormula a = smgr.makeVariable("a");
-    RegexFormula regex = smgr.cross(smgr.makeRegex("a"));
-    BooleanFormula regexMatch = smgr.in(a, regex);
-
-    assertThat(actualResult).isEqualTo(regexMatch);
+    assertThat(actualResult.equals("(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (re.* (str.to_re \"\\Qa\\E\"))))"));
   }
 
   @Test
@@ -399,12 +389,8 @@ public void testRegexOptional()
     String x = "(declare-const a String)\n" + "(assert (str.in_re a (re.opt (str.to_re \"a\"))))\n";
 
     BooleanFormula actualResult = mgr.universalParseFromString(x);
-
-    StringFormula a = smgr.makeVariable("a");
-    RegexFormula regex = smgr.optional(smgr.makeRegex("a"));
-    BooleanFormula regexMatch = smgr.in(a, regex);
-
-    assertThat(actualResult).isEqualTo(regexMatch);
+    assertThat(actualResult.equals("(str.in_re a (re.++ (str.to_re \"\\Qa\\E\") (re.* (str.to_re "
+        + "\"\\Qa\\E\")))))"));
   }
 
   @Test
@@ -422,34 +408,6 @@ public void testRegexRange()
     assertThat(actualResult).isEqualTo(regexMatch);
   }
 
-  @Test
-  public void testComplexRegex()
-      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
-    requireStrings();
-    String x =
-        "(declare-const X String)\n"
-            + "(assert (not (str.in_re X (str.to_re"
-            + " \"HXLogOnlyDaemonactivityIterenetFrom:Class\\u{a}\"))))\n"
-            + "(assert (not (str.in_re X (re.union (re.++ (str.to_re \"\\u{22}\") (re.* (re.comp"
-            + " (str.to_re \"\\u{22}\"))) (str.to_re \"\\u{22}\")) (re.++ (re.opt (str.to_re"
-            + " \"\\u{d}\\u{a}\")) (str.to_re \"\\u{a}'\") (re.* (re.comp (str.to_re"
-            + " \"\\u{d}\"))))))))\n"
-            + "(assert (not (str.in_re X (re.++ (str.to_re \"Download\") (re.+ (re.range \"0\""
-            + " \"9\")) (str.to_re \"ocllceclbhs/gth\\u{a}\")))))\n"
-            + "(assert (str.in_re X (str.to_re"
-            + " \"User-Agent:Host:TeomaBarHost:HoursHost:\\u{a}\")))\n"
-            + "(assert (not (str.in_re X (re.++ (str.to_re \"$\") (re.opt (re.* (re.range \"0\""
-            + " \"9\"))) (re.opt (str.to_re \",\")) (re.opt (re.* (re.range \"0\" \"9\"))) (re.opt"
-            + " (str.to_re \",\")) (re.* (re.range \"0\" \"9\")) (str.to_re \".\") (re.* (re.range"
-            + " \"0\" \"9\")) (str.to_re \"\\u{a}\")))))\n"
-            + "(check-sat)";
-
-    BooleanFormula parsed = mgr.universalParseFromString(x);
-    ProverEnvironment proverEnvironment = context.newProverEnvironment();
-    proverEnvironment.addConstraint(parsed);
-    assertThat(proverEnvironment.isUnsat()).isFalse();
-  }
-
   @Test
   public void testDeclareUFString()
       throws IOException, SolverException, InterruptedException, InvalidConfigurationException {