String formulae

lib/ivy.xml

@@ -143,7 +143,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="com.puppycrawl.tools" name="checkstyle" rev="8.43" conf="checkstyle->default"/>
 
         <!-- SmtInterpol -->
-        <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-732-gd208e931" conf="runtime-smtinterpol->master; contrib->sources"/>
+        <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-842-gfcd46532" conf="runtime-smtinterpol->master; contrib->sources"/>
 
         <!-- Princess for our Maven release -->
         <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2021-08-12" conf="runtime-princess-with-javacup->default; contrib->sources"/>

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

@@ -78,6 +78,13 @@ public interface FormulaManager {
    */
   QuantifiedFormulaManager getQuantifiedFormulaManager();
 
+  /**
+   * Returns the String Theory.
+   *
+   * @throws UnsupportedOperationException If the theory is not supported by the solver.
+   */
+  StringFormulaManager getStringFormulaManager();
+
   /**
    * Create variable of the type equal to {@code formulaType}.
    *

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

@@ -62,6 +62,10 @@ public boolean isSLType() {
     return false;
   }
 
+  public boolean isStringType() {
+    return false;
+  }
+
   @Override
   public abstract String toString();
 
@@ -344,6 +348,25 @@ public String toSMTLIBString() {
     }
   }
 
+  public static final FormulaType<BooleanFormula> StringType =
+      new FormulaType<>() {
+
+        @Override
+        public boolean isStringType() {
+          return true;
+        }
+
+        @Override
+        public String toString() {
+          return "String";
+        }
+
+        @Override
+        public String toSMTLIBString() {
+          return "String";
+        }
+      };
+
   /**
    * Parse a string and return the corresponding type. This method is the counterpart of {@link
    * #toString()}.
@@ -355,6 +378,8 @@ public static FormulaType<?> fromString(String t) {
       return IntegerType;
     } else if (RationalType.toString().equals(t)) {
       return RationalType;
+    } else if (StringType.toString().equals(t)) {
+      return StringType;
     } else if (FloatingPointRoundingModeType.toString().equals(t)) {
       return FloatingPointRoundingModeType;
     } else if (t.startsWith("FloatingPoint<")) {

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

@@ -90,6 +90,14 @@ public interface Model extends Iterable<ValueAssignment>, AutoCloseable {
   @Nullable
   BigInteger evaluate(BitvectorFormula f);
 
+  /**
+   * Type-safe evaluation for string formulas.
+   *
+   * <p>The formula does not need to be a variable, we also allow complex expression.
+   */
+  @Nullable
+  String evaluate(StringFormula f);
+
   /**
    * Iterate over all values present in the model. Note that iterating multiple times may be
    * inefficient for some solvers, it is recommended to use {@link

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

@@ -0,0 +1,15 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2021 Alejandro Serrano Mena
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.api;
+
+import com.google.errorprone.annotations.Immutable;
+
+/** A formula of the string sort. */
+@Immutable
+public interface StringFormula extends Formula {}

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

@@ -0,0 +1,34 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2021 Alejandro Serrano Mena
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.api;
+
+/** Manager for dealing with string formulas. */
+public interface StringFormulaManager {
+
+  /**
+   * Returns a {@link StringFormula} representing the given constant.
+   *
+   * @param value the boolean value the returned <code>Formula</code> should represent
+   * @return a Formula representing the given value
+   */
+  StringFormula makeString(String value);
+
+  /**
+   * Creates a variable with exactly the given name.
+   *
+   * <p>Please make sure that the given name is valid in SMT-LIB2. Take a look at {@link
+   * FormulaManager#isValidName} for further information.
+   *
+   * <p>This method does not quote or unquote the given name, but uses the plain name "AS IS".
+   * {@link Formula#toString} can return a different String than the given one.
+   */
+  StringFormula makeVariable(String pVar);
+
+  BooleanFormula equal(StringFormula str1, StringFormula str2);
+}

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

@@ -21,6 +21,7 @@
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+import org.sosy_lab.java_smt.api.StringFormula;
 
 /**
  * A Formula represented as a TFormulaInfo object.
@@ -132,4 +133,12 @@ static final class RationalFormulaImpl<TFormulaInfo> extends AbstractFormula<TFo
       super(pTerm);
     }
   }
+
+  /** Simple StringFormula implementation. */
+  static final class StringFormulaImpl<TFormulaInfo> extends AbstractFormula<TFormulaInfo>
+      implements StringFormula {
+    StringFormulaImpl(TFormulaInfo pT) {
+      super(pT);
+    }
+  }
 }

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

@@ -36,6 +36,7 @@
 import org.sosy_lab.java_smt.api.IntegerFormulaManager;
 import org.sosy_lab.java_smt.api.RationalFormulaManager;
 import org.sosy_lab.java_smt.api.SLFormulaManager;
+import org.sosy_lab.java_smt.api.StringFormulaManager;
 import org.sosy_lab.java_smt.api.Tactic;
 import org.sosy_lab.java_smt.api.visitors.FormulaTransformationVisitor;
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
@@ -117,6 +118,8 @@ public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDec
 
   private final @Nullable AbstractSLFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> slManager;
 
+  private final @Nullable StringFormulaManager strManager;
+
   private final FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> formulaCreator;
 
   /** Builds a solver from the given theory implementations. */
@@ -135,7 +138,8 @@ protected AbstractFormulaManager(
       @Nullable
           AbstractQuantifiedFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> quantifiedManager,
       @Nullable AbstractArrayFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> arrayManager,
-      @Nullable AbstractSLFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> slManager) {
+      @Nullable AbstractSLFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl> slManager,
+      @Nullable StringFormulaManager strManager) {
 
     this.arrayManager = arrayManager;
     this.quantifiedManager = quantifiedManager;
@@ -146,6 +150,7 @@ protected AbstractFormulaManager(
     this.bitvectorManager = bitvectorManager;
     this.floatingPointManager = floatingPointManager;
     this.slManager = slManager;
+    this.strManager = strManager;
     this.formulaCreator = pFormulaCreator;
 
     checkArgument(
@@ -230,6 +235,14 @@ public ArrayFormulaManager getArrayFormulaManager() {
     return arrayManager;
   }
 
+  @Override
+  public StringFormulaManager getStringFormulaManager() {
+    if (strManager == null) {
+      throw new UnsupportedOperationException("Solver does not support string theory");
+    }
+    return strManager;
+  }
+
   public abstract Appender dumpFormula(TFormulaInfo t);
 
   @Override
@@ -391,6 +404,9 @@ public <T extends Formula> T makeVariable(FormulaType<T> formulaType, String nam
     } else if (formulaType.isRationalType()) {
       assert rationalManager != null;
       t = rationalManager.makeVariable(name);
+    } else if (formulaType.isStringType()) {
+      assert strManager != null;
+      t = strManager.makeVariable(name);
     } else if (formulaType.isBitvectorType()) {
       assert bitvectorManager != null;
       t = bitvectorManager.makeVariable((BitvectorType) formulaType, name);

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

@@ -21,6 +21,7 @@
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
+import org.sosy_lab.java_smt.api.StringFormula;
 
 @SuppressWarnings("ClassTypeParameterName")
 public abstract class AbstractModel<TFormulaInfo, TType, TEnv> implements Model {
@@ -56,6 +57,12 @@ public Boolean evaluate(BooleanFormula f) {
     return (Boolean) evaluateImpl(creator.extractInfo(f));
   }
 
+  @Nullable
+  @Override
+  public String evaluate(StringFormula f) {
+    return (String) evaluateImpl(creator.extractInfo(f));
+  }
+
   @Nullable
   @Override
   public BigInteger evaluate(BitvectorFormula f) {

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

@@ -0,0 +1,55 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2021 Alejandro SerranoMena
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.basicimpl;
+
+import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName;
+
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.StringFormula;
+import org.sosy_lab.java_smt.api.StringFormulaManager;
+
+@SuppressWarnings("ClassTypeParameterName")
+public abstract class AbstractStringFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
+    extends AbstractBaseFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
+    implements StringFormulaManager {
+
+  protected AbstractStringFormulaManager(
+      FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> pCreator) {
+    super(pCreator);
+  }
+
+  private StringFormula wrap(TFormulaInfo formulaInfo) {
+    return getFormulaCreator().encapsulateString(formulaInfo);
+  }
+
+  @Override
+  public StringFormula makeString(String value) {
+    return wrap(makeStringImpl(value));
+  }
+
+  protected abstract TFormulaInfo makeStringImpl(String value);
+
+  @Override
+  public StringFormula makeVariable(String pVar) {
+    checkVariableName(pVar);
+    return wrap(makeVariableImpl(pVar));
+  }
+
+  protected abstract TFormulaInfo makeVariableImpl(String pVar);
+
+  @Override
+  public BooleanFormula equal(StringFormula str1, StringFormula str2) {
+    TFormulaInfo param1 = extractInfo(str1);
+    TFormulaInfo param2 = extractInfo(str2);
+
+    return wrapBool(equal(param1, param2));
+  }
+
+  protected abstract TFormulaInfo equal(TFormulaInfo pParam1, TFormulaInfo pParam2);
+}

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

@@ -39,6 +39,7 @@
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier;
+import org.sosy_lab.java_smt.api.StringFormula;
 import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor;
 import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
 import org.sosy_lab.java_smt.api.visitors.TraversalProcess;
@@ -49,6 +50,7 @@
 import org.sosy_lab.java_smt.basicimpl.AbstractFormula.FloatingPointRoundingModeFormulaImpl;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormula.IntegerFormulaImpl;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormula.RationalFormulaImpl;
+import org.sosy_lab.java_smt.basicimpl.AbstractFormula.StringFormulaImpl;
 
 /**
  * This is a helper class with several methods that are commonly used throughout the basicimpl
@@ -66,14 +68,20 @@ public abstract class FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> {
   private final TType boolType;
   private final @Nullable TType integerType;
   private final @Nullable TType rationalType;
+  private final @Nullable TType stringType;
   protected final TEnv environment;
 
   protected FormulaCreator(
-      TEnv env, TType boolType, @Nullable TType pIntegerType, @Nullable TType pRationalType) {
+      TEnv env,
+      TType boolType,
+      @Nullable TType pIntegerType,
+      @Nullable TType pRationalType,
+      @Nullable TType stringType) {
     this.environment = env;
     this.boolType = boolType;
     this.integerType = pIntegerType;
     this.rationalType = pRationalType;
+    this.stringType = stringType;
   }
 
   public final TEnv getEnv() {
@@ -104,6 +112,13 @@ public final TType getRationalType() {
 
   public abstract TType getArrayType(TType indexType, TType elementType);
 
+  public final TType getStringType() {
+    if (stringType == null) {
+      throw new UnsupportedOperationException("String theory is not supported by this solver.");
+    }
+    return stringType;
+  }
+
   public abstract TFormulaInfo makeVariable(TType type, String varName);
 
   public BooleanFormula encapsulateBoolean(TFormulaInfo pTerm) {
@@ -132,6 +147,11 @@ assert getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElemen
     return new ArrayFormulaImpl<>(pTerm, pIndexType, pElementType);
   }
 
+  public StringFormula encapsulateString(TFormulaInfo pTerm) {
+    assert getFormulaType(pTerm).isStringType();
+    return new StringFormulaImpl<>(pTerm);
+  }
+
   public Formula encapsulateWithTypeOf(TFormulaInfo pTerm) {
     return encapsulate(getFormulaType(pTerm), pTerm);
   }
@@ -148,6 +168,8 @@ public <T extends Formula> T encapsulate(FormulaType<T> pType, TFormulaInfo pTer
       return (T) new IntegerFormulaImpl<>(pTerm);
     } else if (pType.isRationalType()) {
       return (T) new RationalFormulaImpl<>(pTerm);
+    } else if (pType.isStringType()) {
+      return (T) new StringFormulaImpl<>(pTerm);
     } else if (pType.isBitvectorType()) {
       return (T) new BitvectorFormulaImpl<>(pTerm);
     } else if (pType.isFloatingPointType()) {
@@ -194,6 +216,8 @@ protected <T extends Formula> FormulaType<T> getFormulaType(T formula) {
       t = FormulaType.IntegerType;
     } else if (formula instanceof RationalFormula) {
       t = FormulaType.RationalType;
+    } else if (formula instanceof StringFormula) {
+      t = FormulaType.StringType;
     } else if (formula instanceof FloatingPointRoundingModeFormula) {
       t = FormulaType.FloatingPointRoundingModeType;
     } else if (formula instanceof ArrayFormula) {

src/org/sosy_lab/java_smt/delegate/statistics/SolverStatistics.java

@@ -36,6 +36,7 @@ public class SolverStatistics {
   final AtomicInteger bvOperations = new AtomicInteger();
   final AtomicInteger fpOperations = new AtomicInteger();
   final AtomicInteger typeOperations = new AtomicInteger();
+  final AtomicInteger stringOperations = new AtomicInteger();
 
   // model operations
   final AtomicInteger modelEvaluations = new AtomicInteger();
@@ -140,6 +141,10 @@ public int getNumberOfFPOperations() {
     return fpOperations.get();
   }
 
+  public int getNumberOfStringOperations() {
+    return stringOperations.get();
+  }
+
   public int getNumberOfModelEvaluationQueries() {
     return modelEvaluations.get();
   }