String theory: extend API with support for code points.

Author: kfriedberger

src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java

@@ -300,6 +300,8 @@ public enum FunctionDeclarationKind {
   STR_IN_RE,
   STR_TO_INT,
   INT_TO_STR,
+  STR_FROM_CODE,
+  STR_TO_CODE,
   STR_LT,
   STR_LE,
   RE_PLUS,

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

@@ -511,6 +511,8 @@ private Expr normalize(Expr operator) {
           .put(Kind.STRING_IN_REGEXP, FunctionDeclarationKind.STR_IN_RE)
           .put(Kind.STRING_STOI, FunctionDeclarationKind.STR_TO_INT)
           .put(Kind.STRING_ITOS, FunctionDeclarationKind.INT_TO_STR)
+          .put(Kind.STRING_TO_CODE, FunctionDeclarationKind.STR_TO_CODE)
+          .put(Kind.STRING_FROM_CODE, FunctionDeclarationKind.STR_FROM_CODE)
           .put(Kind.STRING_LT, FunctionDeclarationKind.STR_LT)
           .put(Kind.STRING_LEQ, FunctionDeclarationKind.STR_LE)
           .put(Kind.REGEXP_PLUS, FunctionDeclarationKind.RE_PLUS)

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

@@ -626,6 +626,8 @@ private Term normalize(Term operator) {
           .put(Kind.STRING_IN_REGEXP, FunctionDeclarationKind.STR_IN_RE)
           .put(Kind.STRING_FROM_INT, FunctionDeclarationKind.INT_TO_STR)
           .put(Kind.STRING_TO_INT, FunctionDeclarationKind.STR_TO_INT)
+          .put(Kind.STRING_TO_CODE, FunctionDeclarationKind.STR_TO_CODE)
+          .put(Kind.STRING_FROM_CODE, FunctionDeclarationKind.STR_FROM_CODE)
           .put(Kind.STRING_LT, FunctionDeclarationKind.STR_LT)
           .put(Kind.STRING_LEQ, FunctionDeclarationKind.STR_LE)
           .put(Kind.REGEXP_PLUS, FunctionDeclarationKind.RE_PLUS)

src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java

@@ -135,6 +135,10 @@ class PrincessFormulaCreator
         PrincessEnvironment.stringTheory.str_to_re(), FunctionDeclarationKind.STR_TO_RE);
     theoryFunctionKind.put(
         PrincessEnvironment.stringTheory.str_to_int(), FunctionDeclarationKind.STR_TO_INT);
+    theoryFunctionKind.put(
+        PrincessEnvironment.stringTheory.str_to_code(), FunctionDeclarationKind.STR_TO_CODE);
+    theoryFunctionKind.put(
+        PrincessEnvironment.stringTheory.str_from_code(), FunctionDeclarationKind.STR_FROM_CODE);
     theoryFunctionKind.put(
         PrincessEnvironment.stringTheory.re_range(), FunctionDeclarationKind.RE_RANGE);
     theoryFunctionKind.put(

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -818,6 +818,10 @@ private FunctionDeclarationKind getDeclarationKind(long f) {
         return FunctionDeclarationKind.STR_IN_RE;
       case Z3_OP_STR_TO_INT:
         return FunctionDeclarationKind.STR_TO_INT;
+      case Z3_OP_STR_TO_CODE:
+        return FunctionDeclarationKind.STR_TO_CODE;
+      case Z3_OP_STR_FROM_CODE:
+        return FunctionDeclarationKind.STR_FROM_CODE;
       case Z3_OP_INT_TO_STR:
         return FunctionDeclarationKind.INT_TO_STR;
       case Z3_OP_STRING_LT:

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

@@ -736,6 +736,7 @@ public void stringInStringFormulaVisit() throws SolverException, InterruptedExce
     StringFormula z = smgr.makeString("zAsString");
     IntegerFormula offset = imgr.makeVariable("offset");
     IntegerFormula len = imgr.makeVariable("len");
+    IntegerFormula cp = imgr.makeVariable("cp");
 
     ImmutableList.Builder<StringFormula> formulas =
         ImmutableList.<StringFormula>builder()
@@ -744,6 +745,9 @@ public void stringInStringFormulaVisit() throws SolverException, InterruptedExce
             .add(smgr.charAt(x, offset))
             .add(smgr.toStringFormula(offset))
             .add(smgr.concat(x, y, z));
+    if (solverToUse() != Solvers.PRINCESS) {
+      formulas.add(smgr.fromCodePoint(cp));
+    }
     if (solverToUse() != Solvers.Z3) {
       formulas.add(smgr.replaceAll(x, y, z)); // unsupported in Z3
     }