Add generic equality and distinct to the API

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

@@ -8,8 +8,10 @@
 
 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.List;
 import java.util.Map;
 import org.sosy_lab.common.Appender;
@@ -131,6 +133,46 @@ <T extends Formula> T makeApplication(
    */
   <T extends Formula> T makeApplication(FunctionDeclaration<T> declaration, Formula... args);
 
+  /**
+   * Create an equality formula between the given arguments. We return "true" if all arguments are
+   * equal, even if there are less than two arguments.
+   *
+   * @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));
+  }
+
+  /**
+   * Create an equality formula between the given arguments. We return "true" if all arguments are
+   * equal, even if there are less than two arguments.
+   *
+   * @param pArgs Arguments to be compared for equality, ordering does not matter.
+   * @return Equality formula
+   */
+  BooleanFormula equal(Collection<Formula> pArgs);
+
+  /**
+   * Create a distinctness formula between the given arguments. We return "true" if all arguments
+   * are pairwise distinct, even if there are less than two arguments.
+   *
+   * @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));
+  }
+
+  /**
+   * Create a distinctness formula between the given arguments. We return "true" if all arguments
+   * are pairwise distinct, even if there are less than two arguments.
+   *
+   * @param pArgs Arguments to be compared for distinctness, ordering does not matter.
+   * @return Distinctness formula
+   */
+  BooleanFormula distinct(Collection<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,12 +14,15 @@
 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.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;
@@ -264,6 +267,88 @@ public EnumerationFormulaManager getEnumerationFormulaManager() {
     return enumManager;
   }
 
+  /** Override if the solver API only supports binary equality. */
+  protected TFormulaInfo equalImpl(TFormulaInfo pArg1, TFormulaInfo pArgs) {
+    return equalImpl(ImmutableList.of(pArg1, pArgs));
+  }
+
+  @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)));
+  }
+
+  /** Override if the solver API supports equality with many arguments. */
+  protected TFormulaInfo equalImpl(Collection<TFormulaInfo> pArgs) {
+    List<TFormulaInfo> equalities = new ArrayList<>();
+    for (TFormulaInfo[] pair : pairwise(pArgs)) {
+      equalities.add(equalImpl(pair[0], pair[1]));
+    }
+    return booleanManager.andImpl(equalities);
+  }
+
+  /** for an Iterable [1, 2, 3, 4, 5], collect pairs [(1,2), (2,3), (3,4), (4,5)]. */
+  @SuppressWarnings("unchecked")
+  private <T> List<T[]> pairwise(Iterable<T> pArgs) {
+    final List<T[]> result = new ArrayList<>();
+    T prev = null;
+    for (T arg : pArgs) {
+      if (prev != null) {
+        result.add((T[]) new Object[] {prev, arg});
+      }
+      prev = arg;
+    }
+    return result;
+  }
+
+  @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);
+    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(distinctImpl(formulaCreator.extractInfo(pArgs)));
+  }
+
+  /** Override if the solver API supports <code>distinct</code>. */
+  protected TFormulaInfo distinctImpl(Collection<TFormulaInfo> pArgs) {
+    List<TFormulaInfo> inequalities = new ArrayList<>();
+    for (TFormulaInfo[] pair : allUniquePairs(pArgs)) {
+      inequalities.add(booleanManager.not(equalImpl(pair[0], pair[1])));
+    }
+    return booleanManager.andImpl(inequalities);
+  }
+
+  /** for an Iterable [1, 2, 3, 4], collect all pairs [(1,2), (1,3), (1,4), (2,3), (2,4), (3,4)]. */
+  @SuppressWarnings("unchecked")
+  private <T> List<T[]> allUniquePairs(Iterable<T> pArgs) {
+    final List<T[]> result = new ArrayList<>();
+    final List<T> seenSoFar = new ArrayList<>(); // local cache for visited elements
+    for (T current : pArgs) {
+      for (T previous : seenSoFar) {
+        result.add((T[]) new Object[] {previous, current});
+      }
+      seenSoFar.add(current);
+    }
+    return result;
+  }
+
   protected abstract TFormulaInfo parseImpl(String formulaStr) throws IllegalArgumentException;
 
   /**

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

@@ -16,6 +16,7 @@
 import com.google.common.collect.Sets;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import java.util.ArrayDeque;
+import java.util.Collection;
 import java.util.Deque;
 import java.util.HashMap;
 import java.util.LinkedHashMap;
@@ -25,6 +26,7 @@
 import java.util.Set;
 import java.util.function.BiConsumer;
 import java.util.function.Predicate;
+import java.util.stream.Collectors;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.sosy_lab.java_smt.api.ArrayFormula;
 import org.sosy_lab.java_smt.api.BitvectorFormula;
@@ -320,8 +322,8 @@ public <R> R visit(Formula input, FormulaVisitor<R> visitor) {
    */
   public abstract <R> R visit(FormulaVisitor<R> visitor, Formula formula, TFormulaInfo f);
 
-  protected List<TFormulaInfo> extractInfo(List<? extends Formula> input) {
-    return Lists.transform(input, this::extractInfo);
+  protected List<TFormulaInfo> extractInfo(Collection<? extends Formula> input) {
+    return input.stream().map(this::extractInfo).collect(Collectors.toList());
   }
 
   /**

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

@@ -13,6 +13,7 @@
 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;
@@ -148,6 +149,24 @@ public <T extends Formula> T makeApplication(
     return result;
   }
 
+  @Override
+  public BooleanFormula equal(Collection<Formula> pArgs) {
+    debugging.assertThreadLocal();
+    pArgs.forEach(debugging::assertFormulaInContext);
+    BooleanFormula result = delegate.equal(pArgs);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
+
+  @Override
+  public BooleanFormula distinct(Collection<Formula> pArgs) {
+    debugging.assertThreadLocal();
+    pArgs.forEach(debugging::assertFormulaInContext);
+    BooleanFormula result = delegate.distinct(pArgs);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
+
   @Override
   public <T extends Formula> FormulaType<T> getFormulaType(T formula) {
     debugging.assertThreadLocal();

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

@@ -12,6 +12,7 @@
 
 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;
@@ -121,6 +122,20 @@ public <T extends Formula> T makeApplication(
     return delegate.makeApplication(pDeclaration, pArgs);
   }
 
+  @Override
+  public BooleanFormula equal(Collection<Formula> pArgs) {
+    // can be more than one operation, however, we count only once
+    stats.booleanOperations.getAndIncrement();
+    return delegate.equal(pArgs);
+  }
+
+  @Override
+  public BooleanFormula distinct(Collection<Formula> pArgs) {
+    // can be more than one operation, however, we count only once
+    stats.booleanOperations.getAndIncrement();
+    return delegate.distinct(pArgs);
+  }
+
   @Override
   public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
     return delegate.getFormulaType(pFormula);

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

@@ -12,6 +12,7 @@
 
 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;
@@ -151,6 +152,20 @@ public <T extends Formula> T makeApplication(
     }
   }
 
+  @Override
+  public BooleanFormula equal(Collection<Formula> pArgs) {
+    synchronized (sync) {
+      return delegate.equal(pArgs);
+    }
+  }
+
+  @Override
+  public BooleanFormula distinct(Collection<Formula> pArgs) {
+    synchronized (sync) {
+      return delegate.distinct(pArgs);
+    }
+  }
+
   @Override
   public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
     synchronized (sync) {

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

@@ -13,16 +13,19 @@
 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;
 import org.sosy_lab.java_smt.basicimpl.Tokenizer;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Bitwuzla;
+import org.sosy_lab.java_smt.solvers.bitwuzla.api.Kind;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Map_TermTerm;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Options;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Parser;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Sort;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Term;
+import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Int;
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Term;
 
 public final class BitwuzlaFormulaManager
@@ -57,6 +60,18 @@ public final class BitwuzlaFormulaManager
     bitwuzlaOption = pBitwuzlaOptions;
   }
 
+  @Override
+  public Term equalImpl(Collection<Term> pArgs) {
+    return creator.getTermManager().mk_term(Kind.EQUAL, new Vector_Term(pArgs), new Vector_Int());
+  }
+
+  @Override
+  public Term distinctImpl(Collection<Term> pArgs) {
+    return creator
+        .getTermManager()
+        .mk_term(Kind.DISTINCT, new Vector_Term(pArgs), new Vector_Int());
+  }
+
   @Override
   public Term parseImpl(String formulaStr) throws IllegalArgumentException {
     // Split the input string into a list of SMT-LIB2 commands

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

@@ -34,6 +34,11 @@ final class BoolectorFormulaManager extends AbstractFormulaManager<Long, Long, L
         null);
   }
 
+  @Override
+  protected Long equalImpl(Long pArg1, Long pArgs) {
+    return BtorJNI.boolector_eq(getEnvironment(), pArg1, pArgs);
+  }
+
   @Override
   public Long parseImpl(String pS) throws IllegalArgumentException {
     throw new UnsupportedOperationException("Boolector can not parse single formulas.");

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

@@ -13,9 +13,12 @@
 import de.uni_freiburg.informatik.ultimate.logic.PrintTerm;
 import edu.stanford.CVC4.Expr;
 import edu.stanford.CVC4.ExprManager;
+import edu.stanford.CVC4.Kind;
 import edu.stanford.CVC4.Type;
+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;
@@ -63,6 +66,20 @@ static Expr getCVC4Expr(Formula pT) {
         "Cannot get the formula info of type " + pT.getClass().getSimpleName() + " in the Solver!");
   }
 
+  @Override
+  public Expr equalImpl(Expr pArg1, Expr pArgs) {
+    return getEnvironment().mkExpr(Kind.EQUAL, pArg1, pArgs);
+  }
+
+  @Override
+  public Expr distinctImpl(Collection<Expr> pArgs) {
+    vectorExpr vec = new vectorExpr();
+    for (Expr e : pArgs) {
+      vec.add(e);
+    }
+    return getEnvironment().mkExpr(Kind.DISTINCT, vec);
+  }
+
   @Override
   public Expr parseImpl(String formulaStr) throws IllegalArgumentException {
     throw new UnsupportedOperationException();

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

@@ -16,6 +16,7 @@
 import io.github.cvc5.Sort;
 import io.github.cvc5.Term;
 import io.github.cvc5.TermManager;
+import java.util.Collection;
 import java.util.LinkedHashMap;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.Formula;
@@ -64,6 +65,16 @@ static Term getCVC5Term(Formula pT) {
         "Cannot get the formula info of type " + pT.getClass().getSimpleName() + " in the Solver!");
   }
 
+  @Override
+  public Term equalImpl(Collection<Term> pArgs) {
+    return getEnvironment().mkTerm(Kind.EQUAL, pArgs.toArray(new Term[0]));
+  }
+
+  @Override
+  public Term distinctImpl(Collection<Term> pArgs) {
+    return getEnvironment().mkTerm(Kind.DISTINCT, pArgs.toArray(new Term[0]));
+  }
+
   @Override
   public Term parseImpl(String formulaStr) throws IllegalArgumentException {
     throw new UnsupportedOperationException();