Merge branch 'master' into use_solver_native_bv_to_ieee-fp_CVC4_CVC5

Author: BaierD

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

@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.api;
 
+import com.google.common.collect.ImmutableList;
 import java.math.BigInteger;
 import java.util.List;
 import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
@@ -415,6 +416,6 @@ default BitvectorFormula extract(BitvectorFormula number, int msb, int lsb, bool
   BooleanFormula distinct(List<BitvectorFormula> pBits);
 
   default BooleanFormula distinct(BitvectorFormula... pBits) {
-    return distinct(List.of(pBits));
+    return distinct(ImmutableList.copyOf(pBits));
   }
 }

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

@@ -8,9 +8,9 @@
 
 package org.sosy_lab.java_smt.api;
 
+import com.google.common.collect.ImmutableList;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import java.util.Collection;
-import java.util.List;
 import java.util.Set;
 import java.util.stream.Collector;
 import org.sosy_lab.java_smt.api.visitors.BooleanFormulaTransformationVisitor;
@@ -113,7 +113,7 @@ default BooleanFormula makeBoolean(boolean value) {
    * @see #and(BooleanFormula, BooleanFormula)
    */
   default BooleanFormula and(BooleanFormula... bits) {
-    return and(List.of(bits));
+    return and(ImmutableList.copyOf(bits));
   }
 
   /** Return a stream {@link Collector} that creates a conjunction of all elements in the stream. */
@@ -137,7 +137,7 @@ default BooleanFormula and(BooleanFormula... bits) {
    * @see #or(BooleanFormula, BooleanFormula)
    */
   default BooleanFormula or(BooleanFormula... bits) {
-    return or(List.of(bits));
+    return or(ImmutableList.copyOf(bits));
   }
 
   /** Return a stream {@link Collector} that creates a disjunction of all elements in the stream. */

src/org/sosy_lab/java_smt/api/SLFormulaManager.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: 2025 Dirk Beyer <https://www.sosy-lab.org>
 //
 // SPDX-License-Identifier: Apache-2.0
 
@@ -15,18 +15,73 @@
  * all formulae for one heap need to use matching types (sorts) for the AdressFormulae and
  * ValueFormulae. The user has to take care of this, otherwise the {@link ProverEnvironment}
  * complains at runtime!
+ *
+ * @see <a href="https://en.wikipedia.org/wiki/Separation_logic">Separation Logic</a>
+ * @see <a href="https://cacm.acm.org/research/separation-logic/">Separation Logic</a>
+ * @see <a
+ *     href="https://www.cs.cmu.edu/afs/cs.cmu.edu/project/fox-19/member/jcr/www15818As2011/cs818A3-11.html">15-818A3
+ *     Introduction to Separation Logic (6 units) Spring 2011</a>
+ * @see <a href="https://www.philipzucker.com/executable-seperation">Modeling Separation Logic with
+ *     Python Dicts and Z3</a>
  */
 @SuppressWarnings("MethodTypeParameterName")
 public interface SLFormulaManager {
 
+  /**
+   * Creates a formula representing the "separating conjunction" (*) of two Boolean formulas. In
+   * separation logic, the separating conjunction asserts that the two formulas describe disjoint
+   * parts of the heap. It is similar to the logical AND operator, but with the additional
+   * constraint that the memory regions described by the two formulas do not overlap.
+   *
+   * @return a Boolean formula representing the separating conjunction of {@code f1} and {@code f2}.
+   */
   BooleanFormula makeStar(BooleanFormula f1, BooleanFormula f2);
 
+  /**
+   * Creates a formula representing a "points-to" relation in the heap. The "points-to" relation
+   * asserts that a pointer points to a specific value in memory.
+   *
+   * @param <AF> the type of the address formula.
+   * @param <VF> the type of the value formula.
+   * @param ptr the pointer formula.
+   * @param to the value formula.
+   * @return a Boolean formula representing the "points-to" relation.
+   */
   <AF extends Formula, VF extends Formula> BooleanFormula makePointsTo(AF ptr, VF to);
 
+  /**
+   * Creates a formula representing the "magic wand" (-*) operator in separation logic. The "magic
+   * wand" operator asserts that if the first formula holds, then the second formula can be added to
+   * the heap without conflict. It is a form of implication (=&gt;) that takes into account the
+   * disjointness of memory regions.
+   *
+   * @return a Boolean formula representing the "magic wand" of {@code f1} and {@code f2}.
+   */
   BooleanFormula makeMagicWand(BooleanFormula f1, BooleanFormula f2);
 
+  /**
+   * Creates a formula representing an empty heap. The empty heap formula asserts that no memory is
+   * allocated for the given address and value types.
+   *
+   * @param <AF> the type of the address formula.
+   * @param <VF> the type of the value formula.
+   * @param <AT> the type of the address formula type.
+   * @param <VT> the type of the value formula type.
+   * @param pAddressType the type of the address formula.
+   * @param pValueType the type of the value formula.
+   * @return a Boolean formula representing an empty heap.
+   */
   <AF extends Formula, VF extends Formula, AT extends FormulaType<AF>, VT extends FormulaType<VF>>
-      BooleanFormula makeEmptyHeap(AT pAdressType, VT pValueType);
+      BooleanFormula makeEmptyHeap(AT pAddressType, VT pValueType);
 
+  /**
+   * Creates a formula representing the "nil" element for a given address type. The "nil" element is
+   * used to represent a null pointer or an unallocated memory address.
+   *
+   * @param <AF> the type of the address formula.
+   * @param <AT> the type of the address formula type.
+   * @param pAdressType the type of the address formula.
+   * @return a formula representing the "nil" element for the given address type.
+   */
   <AF extends Formula, AT extends FormulaType<AF>> AF makeNilElement(AT pAdressType);
 }

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

@@ -8,7 +8,7 @@
 
 package org.sosy_lab.java_smt.api;
 
-import java.util.Arrays;
+import com.google.common.collect.ImmutableList;
 import java.util.List;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager;
@@ -104,7 +104,7 @@ public interface StringFormulaManager {
   IntegerFormula length(StringFormula str);
 
   default StringFormula concat(StringFormula... parts) {
-    return concat(Arrays.asList(parts));
+    return concat(ImmutableList.copyOf(parts));
   }
 
   StringFormula concat(List<StringFormula> parts);
@@ -165,7 +165,7 @@ default RegexFormula range(char start, char end) {
    * @return formula denoting the concatenation
    */
   default RegexFormula concat(RegexFormula... parts) {
-    return concatRegex(Arrays.asList(parts));
+    return concatRegex(ImmutableList.copyOf(parts));
   }
 
   /**

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

@@ -8,6 +8,7 @@
 
 package org.sosy_lab.java_smt.api;
 
+import com.google.common.collect.ImmutableList;
 import java.util.List;
 
 /** Manager for dealing with uninterpreted functions (UFs). */
@@ -20,7 +21,7 @@ <T extends Formula> FunctionDeclaration<T> declareUF(
   /** Declare an uninterpreted function. */
   default <T extends Formula> FunctionDeclaration<T> declareUF(
       String name, FormulaType<T> returnType, FormulaType<?>... args) {
-    return declareUF(name, returnType, List.of(args));
+    return declareUF(name, returnType, ImmutableList.copyOf(args));
   }
 
   /**
@@ -38,7 +39,7 @@ default <T extends Formula> FunctionDeclaration<T> declareUF(
    * @see #callUF(FunctionDeclaration, List)
    */
   default <T extends Formula> T callUF(FunctionDeclaration<T> funcType, Formula... args) {
-    return callUF(funcType, List.of(args));
+    return callUF(funcType, ImmutableList.copyOf(args));
   }
 
   /**
@@ -58,6 +59,6 @@ <T extends Formula> T declareAndCallUF(
    */
   default <T extends Formula> T declareAndCallUF(
       String name, FormulaType<T> pReturnType, Formula... pArgs) {
-    return declareAndCallUF(name, pReturnType, List.of(pArgs));
+    return declareAndCallUF(name, pReturnType, ImmutableList.copyOf(pArgs));
   }
 }

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

@@ -15,11 +15,11 @@
 import com.google.common.base.CharMatcher;
 import com.google.common.base.Preconditions;
 import com.google.common.collect.ImmutableBiMap;
+import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Iterables;
 import java.io.IOException;
-import java.util.Arrays;
 import java.util.List;
 import java.util.Map;
 import org.checkerframework.checker.nullness.qual.Nullable;
@@ -542,7 +542,7 @@ public <T extends Formula> T makeApplication(
   @Override
   public <T extends Formula> T makeApplication(
       FunctionDeclaration<T> declaration, Formula... args) {
-    return makeApplication(declaration, Arrays.asList(args));
+    return makeApplication(declaration, ImmutableList.copyOf(args));
   }
 
   @Override

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

@@ -29,7 +29,7 @@
 
 public abstract class AbstractProver<T> implements BasicProverEnvironment<T> {
 
-  private final boolean generateModels;
+  protected final boolean generateModels;
   private final boolean generateAllSat;
   protected final boolean generateUnsatCores;
   private final boolean generateUnsatCoresOverAssumptions;

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

@@ -10,8 +10,8 @@
 
 import static org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager.checkVariableName;
 
+import com.google.common.collect.ImmutableList;
 import com.google.common.collect.Lists;
-import java.util.Arrays;
 import java.util.List;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
@@ -68,6 +68,6 @@ public <T extends Formula> T declareAndCallUF(
   public <T extends Formula> T declareAndCallUF(
       String name, FormulaType<T> pReturnType, Formula... pArgs) {
     checkVariableName(name);
-    return declareAndCallUF(name, pReturnType, Arrays.asList(pArgs));
+    return declareAndCallUF(name, pReturnType, ImmutableList.copyOf(pArgs));
   }
 }

src/org/sosy_lab/java_smt/delegate/debugging/DebuggingAssertions.java

@@ -9,7 +9,7 @@
 package org.sosy_lab.java_smt.delegate.debugging;
 
 import com.google.common.base.Preconditions;
-import java.util.List;
+import com.google.common.collect.ImmutableList;
 import org.sosy_lab.common.configuration.Configuration;
 import org.sosy_lab.common.configuration.InvalidConfigurationException;
 import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
@@ -54,7 +54,7 @@ public void addFunctionDeclaration(FunctionDeclaration<?> pFunctionDeclaration)
 
   /** Assert that the function declaration belongs to this context. */
   public void assertDeclarationInContext(FunctionDeclaration<?> pFunctionDeclaration) {
-    if (List.of(FunctionDeclarationKind.VAR, FunctionDeclarationKind.UF)
+    if (ImmutableList.of(FunctionDeclarationKind.VAR, FunctionDeclarationKind.UF)
         .contains(pFunctionDeclaration.getKind())) {
       Preconditions.checkArgument(
           debugInfo.getDeclaredFunctions().contains(pFunctionDeclaration),

src/org/sosy_lab/java_smt/example/Binoxxo.java

@@ -9,6 +9,7 @@
 package org.sosy_lab.java_smt.example;
 
 import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
 import java.io.IOException;
 import java.math.BigInteger;
 import java.nio.charset.Charset;
@@ -95,7 +96,7 @@ public static void main(String... args)
           SolverContextFactory.createSolverContext(config, logger, notifier, solver)) {
 
         for (BinoxxoSolver<?> binoxxo :
-            List.of(
+            ImmutableList.of(
                 new IntegerBasedBinoxxoSolver(context), new BooleanBasedBinoxxoSolver(context))) {
           long start = System.currentTimeMillis();
 
@@ -300,7 +301,7 @@ List<BooleanFormula> getRules(IntegerFormula[][] symbols) {
       for (int row = 0; row < size; row++) {
         for (int col = 0; col < size - 2; col++) {
           List<IntegerFormula> lst =
-              List.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]);
+              ImmutableList.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]);
           IntegerFormula sum = imgr.sum(lst);
           rules.add(bmgr.or(imgr.equal(one, sum), imgr.equal(two, sum)));
         }
@@ -310,7 +311,7 @@ List<BooleanFormula> getRules(IntegerFormula[][] symbols) {
       for (int col = 0; col < size; col++) {
         for (int row = 0; row < size - 2; row++) {
           List<IntegerFormula> lst =
-              List.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]);
+              ImmutableList.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]);
           IntegerFormula sum = imgr.sum(lst);
           rules.add(bmgr.or(imgr.equal(one, sum), imgr.equal(two, sum)));
         }
@@ -398,7 +399,7 @@ List<BooleanFormula> getRules(BooleanFormula[][] symbols) {
       for (int row = 0; row < size; row++) {
         for (int col = 0; col < size - 2; col++) {
           List<BooleanFormula> lst =
-              List.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]);
+              ImmutableList.of(symbols[row][col], symbols[row][col + 1], symbols[row][col + 2]);
           rules.add(bmgr.not(bmgr.and(lst)));
           rules.add(bmgr.or(lst));
         }
@@ -408,7 +409,7 @@ List<BooleanFormula> getRules(BooleanFormula[][] symbols) {
       for (int col = 0; col < size; col++) {
         for (int row = 0; row < size - 2; row++) {
           List<BooleanFormula> lst =
-              List.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]);
+              ImmutableList.of(symbols[row][col], symbols[row + 1][col], symbols[row + 2][col]);
           rules.add(bmgr.not(bmgr.and(lst)));
           rules.add(bmgr.or(lst));
         }