Changes to the FormulaManager.equal and FormulaManager.distinct API

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

@@ -8,10 +8,9 @@
 
 package org.sosy_lab.java_smt.api;
 
-import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
-import java.util.Collection;
+import java.util.Arrays;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
@@ -140,8 +139,8 @@ <T extends Formula> T makeApplication(
    * @param pArgs Arguments to be compared for equality, ordering does not matter.
    * @return Equality formula
    */
-  default BooleanFormula equal(Formula... pArgs) {
-    return equal(ImmutableList.copyOf(pArgs));
+  default BooleanFormula makeEqual(Formula... pArgs) {
+    return makeEqual(Arrays.asList(pArgs));
   }
 
   /**
@@ -151,7 +150,7 @@ default BooleanFormula equal(Formula... pArgs) {
    * @param pArgs Arguments to be compared for equality, ordering does not matter.
    * @return Equality formula
    */
-  BooleanFormula equal(Collection<Formula> pArgs);
+  BooleanFormula makeEqual(Iterable<Formula> pArgs);
 
   /**
    * Create a distinctness formula between the given arguments. We return "true" if all arguments
@@ -160,8 +159,8 @@ default BooleanFormula equal(Formula... pArgs) {
    * @param pArgs Arguments to be compared for distinctness, ordering does not matter.
    * @return Distinctness formula
    */
-  default BooleanFormula distinct(Formula... pArgs) {
-    return distinct(ImmutableList.copyOf(pArgs));
+  default BooleanFormula makeDistinct(Formula... pArgs) {
+    return makeDistinct(Arrays.asList(pArgs));
   }
 
   /**
@@ -171,7 +170,7 @@ default BooleanFormula distinct(Formula... pArgs) {
    * @param pArgs Arguments to be compared for distinctness, ordering does not matter.
    * @return Distinctness formula
    */
-  BooleanFormula distinct(Collection<Formula> pArgs);
+  BooleanFormula makeDistinct(Iterable<Formula> pArgs);
 
   /** Returns the type of the given Formula. */
   <T extends Formula> FormulaType<T> getFormulaType(T formula);

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

@@ -14,15 +14,14 @@
 import com.google.common.annotations.VisibleForTesting;
 import com.google.common.base.CharMatcher;
 import com.google.common.base.Preconditions;
-import com.google.common.collect.Collections2;
+import com.google.common.collect.FluentIterable;
 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.ArrayList;
-import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import org.checkerframework.checker.nullness.qual.Nullable;
@@ -268,28 +267,20 @@ public EnumerationFormulaManager getEnumerationFormulaManager() {
   }
 
   /** Override if the solver API only supports binary equality. */
+  @SuppressWarnings("unused")
   protected TFormulaInfo equalImpl(TFormulaInfo pArg1, TFormulaInfo pArgs) {
-    return equalImpl(ImmutableList.of(pArg1, pArgs));
+    throw new UnsupportedOperationException(
+        "equalImpl(x, y) must be implemented in a subclass, if required.");
   }
 
   @Override
-  public BooleanFormula equal(Collection<Formula> pArgs) {
-    if (pArgs.size() < 2) {
-      return booleanManager.makeTrue(); // trivially true
-    }
-    final Collection<FormulaType<Formula>> types =
-        Collections2.transform(pArgs, formulaCreator::getFormulaType);
-    Preconditions.checkArgument(
-        ImmutableSet.copyOf(types).size() == 1,
-        "All arguments to `equal` must have the same type, but found %s different types: %s",
-        types.size(),
-        types);
-    return formulaCreator.encapsulateBoolean(
-        equalImpl(Collections2.transform(pArgs, formulaCreator::extractInfo)));
+  public BooleanFormula makeEqual(Iterable<Formula> pArgs) {
+    FluentIterable<TFormulaInfo> args = getTFormulaInfosForComparison(pArgs);
+    return formulaCreator.encapsulateBoolean(equalImpl(args));
   }
 
   /** Override if the solver API supports equality with many arguments. */
-  protected TFormulaInfo equalImpl(Collection<TFormulaInfo> pArgs) {
+  protected TFormulaInfo equalImpl(Iterable<TFormulaInfo> pArgs) {
     List<TFormulaInfo> equalities = new ArrayList<>();
     for (TFormulaInfo[] pair : pairwise(pArgs)) {
       equalities.add(equalImpl(pair[0], pair[1]));
@@ -312,22 +303,36 @@ private <T> List<T[]> pairwise(Iterable<T> pArgs) {
   }
 
   @Override
-  public BooleanFormula distinct(Collection<Formula> pArgs) {
-    if (pArgs.size() < 2) {
-      return booleanManager.makeTrue(); // trivially true
-    }
-    final Collection<FormulaType<Formula>> types =
-        Collections2.transform(pArgs, formulaCreator::getFormulaType);
+  public BooleanFormula makeDistinct(Iterable<Formula> pArgs) {
+    FluentIterable<TFormulaInfo> args = getTFormulaInfosForComparison(pArgs);
+    return formulaCreator.encapsulateBoolean(distinctImpl(args));
+  }
+
+  @SuppressWarnings("unchecked")
+  private FluentIterable<TFormulaInfo> getTFormulaInfosForComparison(Iterable<Formula> pArgs) {
+    final ImmutableSet<FormulaType<Formula>> types =
+        FluentIterable.from(pArgs).transform(formulaCreator::getFormulaType).toSet();
     Preconditions.checkArgument(
-        ImmutableSet.copyOf(types).size() == 1,
-        "All arguments to `equal` must have the same type, but found %s different types: %s",
+        types.size() < 2
+            || ImmutableSet.of(FormulaType.IntegerType, FormulaType.RationalType).equals(types),
+        "All arguments for comparison must have the same type, but found %s different types: %s",
         types.size(),
         types);
-    return formulaCreator.encapsulateBoolean(distinctImpl(formulaCreator.extractInfo(pArgs)));
+    FluentIterable<TFormulaInfo> args =
+        FluentIterable.from(pArgs).transform(formulaCreator::extractInfo);
+    if (types.contains(FormulaType.IntegerType) && types.contains(FormulaType.RationalType)) {
+      // We can compare Integer and Rational terms, so we convert all terms to Rational
+      args =
+          args.transform(
+              ((AbstractNumeralFormulaManager<TFormulaInfo, ?, ?, ?, ?, ?>)
+                      getRationalFormulaManager())
+                  ::toType);
+    }
+    return args;
   }
 
   /** Override if the solver API supports <code>distinct</code>. */
-  protected TFormulaInfo distinctImpl(Collection<TFormulaInfo> pArgs) {
+  protected TFormulaInfo distinctImpl(Iterable<TFormulaInfo> pArgs) {
     List<TFormulaInfo> inequalities = new ArrayList<>();
     for (TFormulaInfo[] pair : allUniquePairs(pArgs)) {
       inequalities.add(booleanManager.not(equalImpl(pair[0], pair[1])));

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

@@ -13,7 +13,6 @@
 import com.google.common.collect.ImmutableMap;
 import java.io.IOException;
 import java.util.ArrayList;
-import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
@@ -150,19 +149,19 @@ public <T extends Formula> T makeApplication(
   }
 
   @Override
-  public BooleanFormula equal(Collection<Formula> pArgs) {
+  public BooleanFormula makeEqual(Iterable<Formula> pArgs) {
     debugging.assertThreadLocal();
     pArgs.forEach(debugging::assertFormulaInContext);
-    BooleanFormula result = delegate.equal(pArgs);
+    BooleanFormula result = delegate.makeEqual(pArgs);
     debugging.addFormulaTerm(result);
     return result;
   }
 
   @Override
-  public BooleanFormula distinct(Collection<Formula> pArgs) {
+  public BooleanFormula makeDistinct(Iterable<Formula> pArgs) {
     debugging.assertThreadLocal();
     pArgs.forEach(debugging::assertFormulaInContext);
-    BooleanFormula result = delegate.distinct(pArgs);
+    BooleanFormula result = delegate.makeDistinct(pArgs);
     debugging.addFormulaTerm(result);
     return result;
   }

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

@@ -12,7 +12,6 @@
 
 import com.google.common.collect.ImmutableMap;
 import java.io.IOException;
-import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
@@ -123,17 +122,17 @@ public <T extends Formula> T makeApplication(
   }
 
   @Override
-  public BooleanFormula equal(Collection<Formula> pArgs) {
+  public BooleanFormula makeEqual(Iterable<Formula> pArgs) {
     // can be more than one operation, however, we count only once
     stats.booleanOperations.getAndIncrement();
-    return delegate.equal(pArgs);
+    return delegate.makeEqual(pArgs);
   }
 
   @Override
-  public BooleanFormula distinct(Collection<Formula> pArgs) {
+  public BooleanFormula makeDistinct(Iterable<Formula> pArgs) {
     // can be more than one operation, however, we count only once
     stats.booleanOperations.getAndIncrement();
-    return delegate.distinct(pArgs);
+    return delegate.makeDistinct(pArgs);
   }
 
   @Override

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

@@ -12,7 +12,6 @@
 
 import com.google.common.collect.ImmutableMap;
 import java.io.IOException;
-import java.util.Collection;
 import java.util.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
@@ -153,16 +152,16 @@ public <T extends Formula> T makeApplication(
   }
 
   @Override
-  public BooleanFormula equal(Collection<Formula> pArgs) {
+  public BooleanFormula makeEqual(Iterable<Formula> pArgs) {
     synchronized (sync) {
-      return delegate.equal(pArgs);
+      return delegate.makeEqual(pArgs);
     }
   }
 
   @Override
-  public BooleanFormula distinct(Collection<Formula> pArgs) {
+  public BooleanFormula makeDistinct(Iterable<Formula> pArgs) {
     synchronized (sync) {
-      return delegate.distinct(pArgs);
+      return delegate.makeDistinct(pArgs);
     }
   }
 

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java

@@ -13,7 +13,6 @@
 import com.google.common.collect.Iterables;
 import com.google.common.collect.Table;
 import com.google.common.collect.Table.Cell;
-import java.util.Collection;
 import java.util.List;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
@@ -62,13 +61,23 @@ public final class BitwuzlaFormulaManager
   }
 
   @Override
-  public Term equalImpl(Collection<Term> pArgs) {
-    return creator.getEnv().mk_term(Kind.EQUAL, new Vector_Term(pArgs), new Vector_Int());
+  public Term equalImpl(Iterable<Term> pArgs) {
+    Vector_Term array = new Vector_Term(pArgs);
+    if (array.size() < 2) {
+      return creator.getEnv().mk_true();
+    } else {
+      return creator.getEnv().mk_term(Kind.EQUAL, array, new Vector_Int());
+    }
   }
 
   @Override
-  public Term distinctImpl(Collection<Term> pArgs) {
-    return creator.getEnv().mk_term(Kind.DISTINCT, new Vector_Term(pArgs), new Vector_Int());
+  public Term distinctImpl(Iterable<Term> pArgs) {
+    Vector_Term array = new Vector_Term(pArgs);
+    if (array.size() < 2) {
+      return creator.getEnv().mk_true();
+    } else {
+      return creator.getEnv().mk_term(Kind.DISTINCT, array, new Vector_Int());
+    }
   }
 
   @Override

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

@@ -18,7 +18,6 @@
 import edu.stanford.CVC4.vectorExpr;
 import java.io.IOException;
 import java.io.OutputStream;
-import java.util.Collection;
 import java.util.LinkedHashMap;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.Formula;
@@ -72,12 +71,16 @@ public Expr equalImpl(Expr pArg1, Expr pArgs) {
   }
 
   @Override
-  public Expr distinctImpl(Collection<Expr> pArgs) {
+  public Expr distinctImpl(Iterable<Expr> pArgs) {
     vectorExpr vec = new vectorExpr();
     for (Expr e : pArgs) {
       vec.add(e);
     }
-    return getEnvironment().mkExpr(Kind.DISTINCT, vec);
+    if (vec.size() < 2) {
+      return getEnvironment().mkConst(true);
+    } else {
+      return getEnvironment().mkExpr(Kind.DISTINCT, vec);
+    }
   }
 
   @Override

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

@@ -11,6 +11,7 @@
 import static com.google.common.base.Preconditions.checkArgument;
 
 import com.google.common.base.Joiner;
+import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.Iterables;
 import de.uni_freiburg.informatik.ultimate.logic.PrintTerm;
@@ -20,7 +21,6 @@
 import io.github.cvc5.Term;
 import io.github.cvc5.TermManager;
 import java.util.Arrays;
-import java.util.Collection;
 import java.util.LinkedHashMap;
 import java.util.Map;
 import java.util.Map.Entry;
@@ -71,13 +71,23 @@ static Term getCVC5Term(Formula pT) {
   }
 
   @Override
-  public Term equalImpl(Collection<Term> pArgs) {
-    return getEnvironment().mkTerm(Kind.EQUAL, pArgs.toArray(new Term[0]));
+  public Term equalImpl(Iterable<Term> pArgs) {
+    Term[] array = ImmutableList.copyOf(pArgs).toArray(new Term[0]);
+    if (array.length < 2) {
+      return getEnvironment().mkTrue();
+    } else {
+      return getEnvironment().mkTerm(Kind.EQUAL, array);
+    }
   }
 
   @Override
-  public Term distinctImpl(Collection<Term> pArgs) {
-    return getEnvironment().mkTerm(Kind.DISTINCT, pArgs.toArray(new Term[0]));
+  public Term distinctImpl(Iterable<Term> pArgs) {
+    Term[] array = ImmutableList.copyOf(pArgs).toArray(new Term[0]);
+    if (array.length < 2) {
+      return getEnvironment().mkTrue();
+    } else {
+      return getEnvironment().mkTerm(Kind.DISTINCT, array);
+    }
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaManager.java

@@ -10,7 +10,6 @@
 
 import com.google.common.base.Joiner;
 import com.google.common.collect.Lists;
-import java.util.Collection;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
@@ -51,13 +50,23 @@ class OpenSmtFormulaManager extends AbstractFormulaManager<PTRef, SRef, Logic, S
   }
 
   @Override
-  protected PTRef equalImpl(Collection<PTRef> pArgs) {
-    return getEnvironment().mkEq(new VectorPTRef(pArgs));
+  protected PTRef equalImpl(Iterable<PTRef> pArgs) {
+    VectorPTRef array = new VectorPTRef(pArgs);
+    if (array.size() < 2) {
+      return getEnvironment().getTerm_true();
+    } else {
+      return getEnvironment().mkEq(array);
+    }
   }
 
   @Override
-  public PTRef distinctImpl(Collection<PTRef> pArgs) {
-    return getEnvironment().mkDistinct(new VectorPTRef(pArgs));
+  public PTRef distinctImpl(Iterable<PTRef> pArgs) {
+    VectorPTRef array = new VectorPTRef(pArgs);
+    if (array.size() < 2) {
+      return getEnvironment().getTerm_true();
+    } else {
+      return getEnvironment().mkDistinct(array);
+    }
   }
 
   @Override