Add generic equality and distinct to the API

daniel-raffler · daniel-raffler · commit fcf5910ce78d · 2025-12-20T08:52:57.000+01:00
diff --git a/src/org/sosy_lab/java_smt/api/FormulaManager.java b/src/org/sosy_lab/java_smt/api/FormulaManager.java
@@ -8,6 +8,7 @@
 
 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.List;
@@ -131,6 +132,18 @@ <T extends Formula> T makeApplication(
    */
   <T extends Formula> T makeApplication(FunctionDeclaration<T> declaration, Formula... args);
 
+  default BooleanFormula equal(Formula... pArgs) {
+    return equal(ImmutableList.copyOf(pArgs));
+  }
+
+  BooleanFormula equal(List<Formula> pArgs);
+
+  default BooleanFormula distinct(Formula... pArgs) {
+    return distinct(ImmutableList.copyOf(pArgs));
+  }
+
+  BooleanFormula distinct(List<Formula> pArgs);
+
   /** Returns the type of the given Formula. */
   <T extends Formula> FormulaType<T> getFormulaType(T formula);
 
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java
@@ -19,6 +19,7 @@
 import com.google.common.collect.ImmutableMap;
 import com.google.common.collect.ImmutableSet;
 import com.google.common.collect.Iterables;
+import com.google.common.collect.Lists;
 import java.io.IOException;
 import java.util.List;
 import java.util.Map;
@@ -264,6 +265,58 @@ 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 if the solver API supports equality with many arguments. */
+  protected TFormulaInfo equalImpl(List<TFormulaInfo> pArgs) {
+    ImmutableList.Builder<TFormulaInfo> builder = ImmutableList.builder();
+    for (int i = 1; i < pArgs.size(); i++) {
+      builder.add(equalImpl(pArgs.get(i - 1), pArgs.get(i)));
+    }
+    return booleanManager.andImpl(builder.build());
+  }
+
+  @Override
+  public BooleanFormula equal(List<Formula> pArgs) {
+    Preconditions.checkArgument(
+        pArgs.size() > 1,
+        "Called `equal` with %s arguments, but at least two are needed",
+        pArgs.size());
+    Preconditions.checkArgument(
+        ImmutableSet.copyOf(Lists.transform(pArgs, formulaCreator::getFormulaType)).size() == 1,
+        "All arguments to `equal` must have the same type, but found %s different types",
+        Lists.transform(pArgs, formulaCreator::getFormulaType).size());
+    return formulaCreator.encapsulateBoolean(
+        equalImpl(Lists.transform(pArgs, formulaCreator::extractInfo)));
+  }
+
+  /** Override if the solver API supports <code>distinct</code>. */
+  protected TFormulaInfo distinctImpl(List<TFormulaInfo> pArgs) {
+    ImmutableList.Builder<TFormulaInfo> builder = ImmutableList.builder();
+    for (int i = 0; i < pArgs.size(); i++) {
+      for (int j = i + 1; j < pArgs.size(); j++) {
+        builder.add(booleanManager.not(equalImpl(pArgs.get(i), pArgs.get(j))));
+      }
+    }
+    return booleanManager.andImpl(builder.build());
+  }
+
+  @Override
+  public BooleanFormula distinct(List<Formula> pArgs) {
+    Preconditions.checkArgument(
+        pArgs.size() > 1,
+        "Called `distinct` with %s arguments, but at least two are needed",
+        pArgs.size());
+    Preconditions.checkArgument(
+        ImmutableSet.copyOf(Lists.transform(pArgs, formulaCreator::getFormulaType)).size() == 1,
+        "All arguments to `distinct` must have the same type, but found %s different types",
+        Lists.transform(pArgs, formulaCreator::getFormulaType).size());
+    return formulaCreator.encapsulateBoolean(distinctImpl(formulaCreator.extractInfo(pArgs)));
+  }
+
   protected abstract TFormulaInfo parseImpl(String formulaStr) throws IllegalArgumentException;
 
   /**
diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingFormulaManager.java
@@ -148,6 +148,28 @@ public <T extends Formula> T makeApplication(
     return result;
   }
 
+  @Override
+  public BooleanFormula equal(List<Formula> pArgs) {
+    debugging.assertThreadLocal();
+    for (Formula f : pArgs) {
+      debugging.assertFormulaInContext(f);
+    }
+    BooleanFormula result = delegate.equal(pArgs);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
+
+  @Override
+  public BooleanFormula distinct(List<Formula> pArgs) {
+    debugging.assertThreadLocal();
+    for (Formula f : pArgs) {
+      debugging.assertFormulaInContext(f);
+    }
+    BooleanFormula result = delegate.distinct(pArgs);
+    debugging.addFormulaTerm(result);
+    return result;
+  }
+
   @Override
   public <T extends Formula> FormulaType<T> getFormulaType(T formula) {
     debugging.assertThreadLocal();
diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFormulaManager.java
@@ -121,6 +121,18 @@ public <T extends Formula> T makeApplication(
     return delegate.makeApplication(pDeclaration, pArgs);
   }
 
+  @Override
+  public BooleanFormula equal(List<Formula> pArgs) {
+    stats.booleanOperations.getAndIncrement(); // TODO Check the formula type?
+    return delegate.equal(pArgs);
+  }
+
+  @Override
+  public BooleanFormula distinct(List<Formula> pArgs) {
+    stats.booleanOperations.getAndIncrement(); // TODO Check the formula type?
+    throw new UnsupportedOperationException();
+  }
+
   @Override
   public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
     return delegate.getFormulaType(pFormula);
diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFormulaManager.java
@@ -151,6 +151,20 @@ public <T extends Formula> T makeApplication(
     }
   }
 
+  @Override
+  public BooleanFormula equal(List<Formula> pArgs) {
+    synchronized (sync) {
+      return delegate.equal(pArgs);
+    }
+  }
+
+  @Override
+  public BooleanFormula distinct(List<Formula> pArgs) {
+    synchronized (sync) {
+      return delegate.distinct(pArgs);
+    }
+  }
+
   @Override
   public <T extends Formula> FormulaType<T> getFormulaType(T pFormula) {
     synchronized (sync) {
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java
@@ -18,11 +18,13 @@
 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 +59,18 @@ public final class BitwuzlaFormulaManager
     bitwuzlaOption = pBitwuzlaOptions;
   }
 
+  @Override
+  public Term equalImpl(List<Term> pArgs) {
+    return creator.getTermManager().mk_term(Kind.EQUAL, new Vector_Term(pArgs), new Vector_Int());
+  }
+
+  @Override
+  public Term distinctImpl(List<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
diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaManager.java b/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.");
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaManager.java
@@ -13,10 +13,13 @@
 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.LinkedHashMap;
+import java.util.List;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
@@ -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(List<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();
diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaManager.java
@@ -17,6 +17,7 @@
 import io.github.cvc5.Term;
 import io.github.cvc5.TermManager;
 import java.util.LinkedHashMap;
+import java.util.List;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
@@ -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(List<Term> pArgs) {
+    return getEnvironment().mkTerm(Kind.EQUAL, pArgs.toArray(new Term[0]));
+  }
+
+  @Override
+  public Term distinctImpl(List<Term> pArgs) {
+    return getEnvironment().mkTerm(Kind.DISTINCT, pArgs.toArray(new Term[0]));
+  }
+
   @Override
   public Term parseImpl(String formulaStr) throws IllegalArgumentException {
     throw new UnsupportedOperationException();
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaManager.java
@@ -11,6 +11,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_apply_substitution;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_from_smtlib2;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_copy_from;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_eq;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_simplify;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_to_smtlib2_ext;
@@ -68,6 +69,11 @@ static long[] getMsatTerm(Collection<? extends Formula> pFormulas) {
     return Longs.toArray(Collections2.transform(pFormulas, Mathsat5FormulaManager::getMsatTerm));
   }
 
+  @Override
+  protected Long equalImpl(Long pArg1, Long pArgs) {
+    return msat_make_eq(getEnvironment(), pArg1, pArgs);
+  }
+
   @Override
   public Long parseImpl(String pS) throws IllegalArgumentException {
     return msat_from_smtlib2(getEnvironment(), pS);
diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaManager.java
@@ -10,6 +10,7 @@
 
 import com.google.common.base.Joiner;
 import com.google.common.collect.Lists;
+import java.util.List;
 import java.util.Map;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
@@ -18,6 +19,7 @@
 import org.sosy_lab.java_smt.solvers.opensmt.api.SRef;
 import org.sosy_lab.java_smt.solvers.opensmt.api.SymRef;
 import org.sosy_lab.java_smt.solvers.opensmt.api.Symbol;
+import org.sosy_lab.java_smt.solvers.opensmt.api.VectorPTRef;
 
 class OpenSmtFormulaManager extends AbstractFormulaManager<PTRef, SRef, Logic, SymRef> {
   private final OpenSmtFormulaCreator creator;
@@ -48,6 +50,16 @@ class OpenSmtFormulaManager extends AbstractFormulaManager<PTRef, SRef, Logic, S
     osmtLogic = pFormulaCreator.getEnv();
   }
 
+  @Override
+  protected PTRef equalImpl(List<PTRef> pArgs) {
+    return getEnvironment().mkEq(new VectorPTRef(pArgs));
+  }
+
+  @Override
+  public PTRef distinctImpl(List<PTRef> pArgs) {
+    return getEnvironment().mkDistinct(new VectorPTRef(pArgs));
+  }
+
   @Override
   public PTRef parseImpl(String pS) throws IllegalArgumentException {
     return osmtLogic.parseFormula(pS);
diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaManager.java
@@ -8,8 +8,11 @@
 
 package org.sosy_lab.java_smt.solvers.princess;
 
+import ap.parser.IBinFormula;
+import ap.parser.IBinJunctor;
 import ap.parser.IExpression;
 import ap.parser.IFormula;
+import ap.parser.ITerm;
 import ap.types.Sort;
 import com.google.common.base.Preconditions;
 import java.io.IOException;
@@ -55,6 +58,15 @@ BooleanFormula encapsulateBooleanFormula(IExpression t) {
     return getFormulaCreator().encapsulateBoolean(t);
   }
 
+  @Override
+  protected IExpression equalImpl(IExpression pArg1, IExpression pArgs) {
+    if (pArg1 instanceof IFormula) {
+      return new IBinFormula(IBinJunctor.Eqv(), (IFormula) pArg1, (IFormula) pArgs);
+    } else {
+      return ((ITerm) pArg1).$eq$eq$eq((ITerm) pArgs);
+    }
+  }
+
   @Override
   public IExpression parseImpl(String pS) throws IllegalArgumentException {
     List<? extends IExpression> formulas = getEnvironment().parseStringToTerms(pS, creator);
diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaManager.java
@@ -29,6 +29,7 @@
 import java.util.Collections;
 import java.util.Deque;
 import java.util.HashSet;
+import java.util.List;
 import java.util.Set;
 import org.sosy_lab.common.log.LogManager;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -68,6 +69,16 @@ BooleanFormula encapsulateBooleanFormula(Term t) {
     return getFormulaCreator().encapsulateBoolean(t);
   }
 
+  @Override
+  protected Term equalImpl(List<Term> pArgs) {
+    return getEnvironment().getTheory().equals(pArgs.toArray(new Term[0]));
+  }
+
+  @Override
+  protected Term distinctImpl(List<Term> pArgs) {
+    return getEnvironment().getTheory().distinct(pArgs.toArray(new Term[0]));
+  }
+
   @Override
   public Term parseImpl(String pS) throws IllegalArgumentException {
     FormulaCollectionScript parseScript =
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java
diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaManager.java
diff --git a/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FormulaManagerTest.java
