-added a test and changed Generator to use Set-logic all. THIS MUST BE CHANGED SOON!

-added new test

Author: DavidGalllob

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

@@ -255,7 +255,9 @@ public static String getSMTLIB2String() {
     String endSMTLIB2 = "(check-sat)\n(get-model)\n(exit)";
     // FIXME Should we really add this to lines?
     lines.append(endSMTLIB2);
-    return "(set-logic AUFLIRA)\n" + lines;
+    // TODO GENERATOR URGENTLY NEEDS TO DETECT USED THEORIES AND DECLARE IT HERE
+    // TODO NOT ALL SOLVER SUPPORT SET-LOGIC ALL!
+    return "(set-logic ALL)\n" + lines;
   }
 
   public static void resetGenerator() {

src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Visitor.java

@@ -56,6 +56,7 @@
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_assertContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_declareConstContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_declareFunContext;
+import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_defineSortContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_popContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_pushContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Decl_sortContext;
@@ -456,7 +457,7 @@ public FormulaType<?> visitSort_id(Sort_idContext ctx) {
       case "String":
         return FormulaType.StringType;
       default:
-        throw new ParserException(type + " is not a known Array sort. ");
+        throw new ParserException(type + " is not a known sort.");
     }
   }
 
@@ -2317,6 +2318,11 @@ public Object visitDecl_sort(Decl_sortContext ctx) {
     throw new UnsupportedOperationException("JavaSMT does not support \"declare-sort\"");
   }
 
+  @Override
+  public Object visitCmd_defineSort(Cmd_defineSortContext ctx) {
+    throw new UnsupportedOperationException("JavaSMT does not support \"define-sort\"");
+  }
+
   @Override
   public Object visitResp_get_model(Resp_get_modelContext ctx) {
     isModel = true;

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

@@ -15,10 +15,13 @@
 import org.sosy_lab.common.configuration.ConfigurationBuilder;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.FormulaType;
+import org.sosy_lab.java_smt.api.FunctionDeclaration;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.RegexFormula;
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.StringFormula;
+import org.sosy_lab.java_smt.basicimpl.Generator;
 
 @SuppressWarnings({"CheckReturnValue", "ReturnValueIgnored"})
 public class SMTLIB2StringTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
@@ -417,4 +420,60 @@ public void testRegexRange()
 
     assertThat(actualResult).isEqualTo(regexMatch);
   }
+
+  @Test
+  public void testDeclareUFString()
+      throws IOException, SolverException, InterruptedException, InvalidConfigurationException {
+    String x =
+        "(set-info :license \"https://creativecommons.org/licenses/by/4.0/\")\n"
+            + "(set-info :category \"random\")\n"
+            + "(set-info :status sat)\n"
+            + "\n"
+            + "(declare-fun I () String)\n"
+            + "(declare-fun B () String)\n"
+            + "(declare-fun G () String)\n"
+            + "(declare-fun F () String)\n"
+            + "(assert (= (str.++  \"cefcdf\" B \"bgcdfedb\" G \"fgafb\" G \"gefdgcbadf\")  (str.++"
+            + "  G \"ef\" I \"dcbbf\" G \"f\" G \"bbg\" F \"gefdg\" G \"badf\") ))\n"
+            + "(check-sat)\n"
+            + "\n"
+            + "(exit)";
+
+    BooleanFormula actualResult = mgr.universalParseFromString(x);
+    FunctionDeclaration<StringFormula> I =
+        mgr.getUFManager().declareUF("I", FormulaType.StringType);
+    FunctionDeclaration<StringFormula> B =
+        mgr.getUFManager().declareUF("B", FormulaType.StringType);
+    FunctionDeclaration<StringFormula> G =
+        mgr.getUFManager().declareUF("G", FormulaType.StringType);
+    FunctionDeclaration<StringFormula> F =
+        mgr.getUFManager().declareUF("F", FormulaType.StringType);
+    BooleanFormula constraint =
+        smgr.equal(
+            smgr.concat(
+                smgr.makeString("cefcdf"),
+                fmgr.callUF(B),
+                smgr.makeString("bgcdfedb"),
+                fmgr.callUF(G),
+                smgr.makeString("fgafb"),
+                fmgr.callUF(G),
+                smgr.makeString("gefdgcbadf")),
+            smgr.concat(
+                fmgr.callUF(G),
+                smgr.makeString("ef"),
+                fmgr.callUF(I),
+                smgr.makeString("dcbbf"),
+                fmgr.callUF(G),
+                smgr.makeString("f"),
+                fmgr.callUF(G),
+                smgr.makeString("bbg"),
+                fmgr.callUF(F),
+                smgr.makeString("gefdg"),
+                fmgr.callUF(G),
+                smgr.makeString("badf")));
+
+    Generator.assembleConstraint(actualResult);
+    System.out.println(Generator.getSMTLIB2String());
+    assertThat(actualResult).isEqualTo(constraint);
+  }
 }