Add support for const array literals

lib/ivy.xml

@@ -147,9 +147,9 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-1242-g5c50fb6d" conf="runtime-smtinterpol->master; contrib->sources"/>
 
         <!-- Princess for our Maven release -->
-        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2023-06-19" conf="runtime-princess-with-javacup->default; contrib->sources"/>
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-01-12" conf="runtime-princess-with-javacup->default; contrib->sources"/>
         <!-- Princess for our Ivy release-->
-        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2023-06-19" conf="runtime-princess->default; contrib->sources">
+        <dependency org="io.github.uuverifiers" name="princess_2.13" rev="2024-01-12" conf="runtime-princess->default; contrib->sources">
           <!-- Exclude dependency on java-cup and replace it with java-cup-runtime, which is enough.
                We use the JAR that is published by us instead of the one from net.sf.squirrel-sql.thirdparty-non-maven
                because the latter does not provide a separate JAR for java-cup-runtime. -->

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

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -48,18 +48,43 @@ <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> store(
    *
    * @param pIndexType The type of the array index
    * @param pElementType The type of the array elements
-   * @return Formula that represents the array
    */
   <TI extends Formula, TE extends Formula, FTI extends FormulaType<TI>, FTE extends FormulaType<TE>>
       ArrayFormula<TI, TE> makeArray(String pName, FTI pIndexType, FTE pElementType);
 
   /**
-   * Declare a new array.
+   * Declare a new array 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.
+   *
+   * @param type The type of the array, consisting of index type and element type
+   */
+  default <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
+      String pName, ArrayFormulaType<TI, TE> type) {
+    return makeArray(pName, type.getIndexType(), type.getElementType());
+  }
+
+  /**
+   * Create a new array constant with values initialized to elseElem.
+   *
+   * @param elseElem The default value of all entries in the array.
+   */
+  <TI extends Formula, TE extends Formula, FTI extends FormulaType<TI>, FTE extends FormulaType<TE>>
+      ArrayFormula<TI, TE> makeArray(FTI pIndexType, FTE pElementType, TE elseElem);
+
+  /**
+   * Create a new array constant with values initialized to elseElem.
    *
-   * @param pName The name of the array variable
+   * @param elseElem The default value of all entries in the array.
    */
-  <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
-      String pName, ArrayFormulaType<TI, TE> type);
+  default <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
+      ArrayFormulaType<TI, TE> type, TE elseElem) {
+    return makeArray(type.getIndexType(), type.getElementType(), elseElem);
+  }
 
   /** Make a {@link BooleanFormula} that represents the equality of two {@link ArrayFormula}. */
   <TI extends Formula, TE extends Formula> BooleanFormula equivalence(

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

@@ -33,9 +33,10 @@ public enum FunctionDeclarationKind {
   /** Distinct operator for a set of numeric formulas. */
   DISTINCT,
 
-  /** Store and select on arrays. */
+  /** Store and select on arrays, and constant initialization. */
   STORE,
   SELECT,
+  CONST,
 
   // Simple arithmetic,
   // they work across integers and rationals.

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

@@ -15,7 +15,6 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
-import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
 
 @SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"})
 public abstract class AbstractArrayFormulaManager<TFormulaInfo, TType, TEnv, TFuncDecl>
@@ -59,12 +58,6 @@ public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> store(
   protected abstract TFormulaInfo store(
       TFormulaInfo pArray, TFormulaInfo pIndex, TFormulaInfo pValue);
 
-  @Override
-  public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
-      String pName, ArrayFormulaType<TI, TE> type) {
-    return makeArray(pName, type.getIndexType(), type.getElementType());
-  }
-
   @Override
   public <
           TI extends Formula,
@@ -77,9 +70,24 @@ ArrayFormula<TI, TE> makeArray(String pName, FTI pIndexType, FTE pElementType) {
     return getFormulaCreator().encapsulateArray(namedArrayFormula, pIndexType, pElementType);
   }
 
+  @Override
+  public <
+          TI extends Formula,
+          TE extends Formula,
+          FTI extends FormulaType<TI>,
+          FTE extends FormulaType<TE>>
+      ArrayFormula<TI, TE> makeArray(FTI pIndexType, FTE pElementType, TE elseElem) {
+    final TFormulaInfo arrayConst =
+        internalMakeArray(pIndexType, pElementType, extractInfo(elseElem));
+    return getFormulaCreator().encapsulateArray(arrayConst, pIndexType, pElementType);
+  }
+
   protected abstract <TI extends Formula, TE extends Formula> TFormulaInfo internalMakeArray(
       String pName, FormulaType<TI> pIndexType, FormulaType<TE> pElementType);
 
+  protected abstract <TI extends Formula, TE extends Formula> TFormulaInfo internalMakeArray(
+      FormulaType<TI> pIndexType, FormulaType<TE> pElementType, TFormulaInfo elseElem);
+
   @Override
   public <TI extends Formula> FormulaType<TI> getIndexType(ArrayFormula<TI, ?> pArray) {
     return getFormulaCreator().getArrayFormulaIndexType(pArray);

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

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -17,6 +17,7 @@
 import com.google.common.collect.ImmutableBiMap;
 import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.ImmutableSet;
+import com.google.common.collect.Iterables;
 import java.util.Arrays;
 import java.util.List;
 import java.util.Map;
@@ -33,6 +34,7 @@
 import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
 import org.sosy_lab.java_smt.api.FunctionDeclaration;
+import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
 import org.sosy_lab.java_smt.api.IntegerFormulaManager;
 import org.sosy_lab.java_smt.api.RationalFormulaManager;
 import org.sosy_lab.java_smt.api.SLFormulaManager;
@@ -445,6 +447,15 @@ public <T extends Formula> T makeVariable(FormulaType<T> formulaType, String nam
   @SuppressWarnings("unchecked")
   public <T extends Formula> T makeApplication(
       FunctionDeclaration<T> declaration, List<? extends Formula> args) {
+
+    if (declaration.getKind() == FunctionDeclarationKind.CONST) {
+      ArrayFormulaType<?, ?> arrayType = (ArrayFormulaType<?, ?>) declaration.getType();
+      Formula elseElem = Iterables.getOnlyElement(args);
+      return (T)
+          arrayManager.makeArray(
+              arrayType.getIndexType(), getFormulaType(elseElem), Iterables.getOnlyElement(args));
+    }
+
     return formulaCreator.callFunction(declaration, args);
   }
 

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

@@ -15,7 +15,6 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
-import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
 
 @SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"})
 class StatisticsArrayFormulaManager implements ArrayFormulaManager {
@@ -54,10 +53,14 @@ ArrayFormula<TI, TE> makeArray(String pName, FTI pIndexType, FTE pElementType) {
   }
 
   @Override
-  public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
-      String pName, ArrayFormulaType<TI, TE> pType) {
+  public <
+          TI extends Formula,
+          TE extends Formula,
+          FTI extends FormulaType<TI>,
+          FTE extends FormulaType<TE>>
+      ArrayFormula<TI, TE> makeArray(FTI pIndexType, FTE pElementType, TE elseElem) {
     stats.arrayOperations.getAndIncrement();
-    return delegate.makeArray(pName, pType);
+    return delegate.makeArray(pIndexType, pElementType, elseElem);
   }
 
   @Override

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java

@@ -15,7 +15,6 @@
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
-import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
 import org.sosy_lab.java_smt.api.SolverContext;
 
 @SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"})
@@ -58,10 +57,14 @@ ArrayFormula<TI, TE> makeArray(String pName, FTI pIndexType, FTE pElementType) {
   }
 
   @Override
-  public <TI extends Formula, TE extends Formula> ArrayFormula<TI, TE> makeArray(
-      String pName, ArrayFormulaType<TI, TE> pType) {
+  public <
+          TI extends Formula,
+          TE extends Formula,
+          FTI extends FormulaType<TI>,
+          FTE extends FormulaType<TE>>
+      ArrayFormula<TI, TE> makeArray(FTI pIndexType, FTE pElementType, TE elseElem) {
     synchronized (sync) {
-      return delegate.makeArray(pName, pType);
+      return delegate.makeArray(pIndexType, pElementType, elseElem);
     }
   }
 

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorArrayFormulaManager.java

@@ -16,6 +16,7 @@
 import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
 import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager;
 
+@SuppressWarnings("MethodTypeParameterName")
 public class BoolectorArrayFormulaManager
     extends AbstractArrayFormulaManager<Long, Long, Long, Long> {
 
@@ -64,6 +65,12 @@ protected <TI extends Formula, TE extends Formula> Long internalMakeArray(
     return array;
   }
 
+  @Override
+  protected <TI extends Formula, TE extends Formula> Long internalMakeArray(
+      FormulaType<TI> pIndexType, FormulaType<TE> pElementType, Long elseElem) {
+    throw new UnsupportedOperationException();
+  }
+
   @Override
   protected Long equivalence(Long pArray1, Long pArray2) {
     return BtorJNI.boolector_eq(btor, pArray1, pArray2);

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

@@ -8,15 +8,17 @@
 
 package org.sosy_lab.java_smt.solvers.cvc4;
 
+import edu.stanford.CVC4.ArrayStoreAll;
+import edu.stanford.CVC4.ArrayType;
 import edu.stanford.CVC4.Expr;
 import edu.stanford.CVC4.ExprManager;
 import edu.stanford.CVC4.Kind;
 import edu.stanford.CVC4.Type;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
-import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
 import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager;
 
+@SuppressWarnings("MethodTypeParameterName")
 public class CVC4ArrayFormulaManager
     extends AbstractArrayFormulaManager<Expr, Type, ExprManager, Expr> {
 
@@ -41,12 +43,17 @@ protected Expr store(Expr pArray, Expr pIndex, Expr pValue) {
   @SuppressWarnings("MethodTypeParameterName")
   protected <TI extends Formula, TE extends Formula> Expr internalMakeArray(
       String pName, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
-    final ArrayFormulaType<TI, TE> arrayFormulaType =
-        FormulaType.getArrayType(pIndexType, pElementType);
-    final Type cvc4ArrayType = toSolverType(arrayFormulaType);
+    final Type cvc4ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType));
     return getFormulaCreator().makeVariable(cvc4ArrayType, pName);
   }
 
+  @Override
+  protected <TI extends Formula, TE extends Formula> Expr internalMakeArray(
+      FormulaType<TI> pIndexType, FormulaType<TE> pElementType, Expr elseElem) {
+    final Type cvc4ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType));
+    return exprManager.mkConst(new ArrayStoreAll((ArrayType) cvc4ArrayType, elseElem));
+  }
+
   @Override
   protected Expr equivalence(Expr pArray1, Expr pArray2) {
     return exprManager.mkExpr(Kind.EQUAL, pArray1, pArray2);

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

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -16,6 +16,7 @@
 import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.Iterables;
 import com.google.common.primitives.Ints;
+import edu.stanford.CVC4.ArrayStoreAll;
 import edu.stanford.CVC4.ArrayType;
 import edu.stanford.CVC4.BitVectorType;
 import edu.stanford.CVC4.Expr;
@@ -323,6 +324,18 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Expr f) {
         return visitor.visitConstant(formula, f.getConstRoundingMode());
       } else if (type.isString()) {
         return visitor.visitConstant(formula, f.getConstString());
+      } else if (type.isArray()) {
+        ArrayStoreAll storeAll = f.getConstArrayStoreAll();
+        Expr constant = storeAll.getExpr();
+        return visitor.visitFunction(
+            formula,
+            ImmutableList.of(encapsulate(constant)),
+            FunctionDeclarationImpl.of(
+                getName(f),
+                getDeclarationKind(f),
+                ImmutableList.of(getFormulaTypeFromTermType(constant.getType())),
+                getFormulaType(f),
+                f.getKind()));
       } else {
         throw new UnsupportedOperationException("Unhandled constant " + f + " with type " + type);
       }
@@ -506,6 +519,9 @@ private Expr normalize(Expr operator) {
           .put(Kind.REGEXP_INTER, FunctionDeclarationKind.RE_INTERSECT)
           .put(Kind.REGEXP_COMPLEMENT, FunctionDeclarationKind.RE_COMPLEMENT)
           .put(Kind.REGEXP_DIFF, FunctionDeclarationKind.RE_DIFFERENCE)
+          .put(Kind.SELECT, FunctionDeclarationKind.SELECT)
+          .put(Kind.STORE, FunctionDeclarationKind.STORE)
+          .put(Kind.STORE_ALL, FunctionDeclarationKind.CONST)
           .buildOrThrow();
 
   private FunctionDeclarationKind getDeclarationKind(Expr f) {

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

@@ -14,9 +14,9 @@
 import io.github.cvc5.Term;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
-import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType;
 import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager;
 
+@SuppressWarnings("MethodTypeParameterName")
 public class CVC5ArrayFormulaManager extends AbstractArrayFormulaManager<Term, Sort, Solver, Term> {
 
   private final Solver solver;
@@ -40,12 +40,17 @@ protected Term store(Term pArray, Term pIndex, Term pValue) {
   @SuppressWarnings("MethodTypeParameterName")
   protected <TI extends Formula, TE extends Formula> Term internalMakeArray(
       String pName, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
-    final ArrayFormulaType<TI, TE> arrayFormulaType =
-        FormulaType.getArrayType(pIndexType, pElementType);
-    final Sort cvc5ArrayType = toSolverType(arrayFormulaType);
+    final Sort cvc5ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType));
     return getFormulaCreator().makeVariable(cvc5ArrayType, pName);
   }
 
+  @Override
+  protected <TI extends Formula, TE extends Formula> Term internalMakeArray(
+      FormulaType<TI> pIndexType, FormulaType<TE> pElementType, Term elseElem) {
+    final Sort cvc5ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType));
+    return solver.mkConstArray(cvc5ArrayType, elseElem);
+  }
+
   @Override
   protected Term equivalence(Term pArray1, Term pArray2) {
     return solver.mkTerm(Kind.EQUAL, pArray1, pArray2);

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

@@ -2,7 +2,7 @@
 // an API wrapper for a collection of SMT solvers:
 // https://github.com/sosy-lab/java-smt
 //
-// SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
+// SPDX-FileCopyrightText: 2024 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -408,6 +408,18 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
       } else if (f.isRoundingModeValue()) {
         return visitor.visitConstant(formula, f.getRoundingModeValue());
 
+      } else if (f.isConstArray()) {
+        Term constant = f.getConstArrayBase();
+        return visitor.visitFunction(
+            formula,
+            ImmutableList.of(encapsulate(constant)),
+            FunctionDeclarationImpl.of(
+                getName(f),
+                getDeclarationKind(f),
+                ImmutableList.of(getFormulaTypeFromTermType(constant.getSort())),
+                getFormulaType(f),
+                f.getKind()));
+
       } else if (f.getKind() == Kind.VARIABLE) {
         // BOUND vars are used for all vars that are bound to a quantifier in CVC5.
         // We resubstitute them back to the original free.
@@ -623,6 +635,9 @@ private Term normalize(Term operator) {
           .put(Kind.REGEXP_INTER, FunctionDeclarationKind.RE_INTERSECT)
           .put(Kind.REGEXP_COMPLEMENT, FunctionDeclarationKind.RE_COMPLEMENT)
           .put(Kind.REGEXP_DIFF, FunctionDeclarationKind.RE_DIFFERENCE)
+          .put(Kind.SELECT, FunctionDeclarationKind.SELECT)
+          .put(Kind.STORE, FunctionDeclarationKind.STORE)
+          .put(Kind.CONST_ARRAY, FunctionDeclarationKind.CONST)
           .build();
 
   private FunctionDeclarationKind getDeclarationKind(Term f) {