Merge branch 'trivial-distinct' into 'master'

Author: kfriedberger

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

@@ -178,8 +178,12 @@ protected Expr lessOrEquals(Expr pParam1, Expr pParam2) {
 
   @Override
   protected Expr distinctImpl(List<Expr> pParam) {
-    vectorExpr param = new vectorExpr();
-    pParam.forEach(param::add);
-    return exprManager.mkExpr(Kind.DISTINCT, param);
+    if (pParam.size() < 2) {
+      return exprManager.mkConst(true);
+    } else {
+      vectorExpr param = new vectorExpr();
+      pParam.forEach(param::add);
+      return exprManager.mkExpr(Kind.DISTINCT, param);
+    }
   }
 }

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

@@ -188,6 +188,10 @@ protected Term lessOrEquals(Term pParam1, Term pParam2) {
 
   @Override
   protected Term distinctImpl(List<Term> pParam) {
-    return solver.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0]));
+    if (pParam.size() < 2) {
+      return solver.mkTrue();
+    } else {
+      return solver.mkTerm(Kind.DISTINCT, pParam.toArray(new Term[0]));
+    }
   }
 }

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolNumeralFormulaManager.java

@@ -148,7 +148,11 @@ public Term equal(Term pNumber1, Term pNumber2) {
 
   @Override
   public Term distinctImpl(List<Term> pNumbers) {
-    return env.term("distinct", pNumbers.toArray(new Term[0]));
+    if (pNumbers.size() < 2) {
+      return env.getTheory().mTrue;
+    } else {
+      return env.term("distinct", pNumbers.toArray(new Term[0]));
+    }
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/yices2/Yices2NumeralFormulaManager.java

@@ -24,6 +24,7 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_rational;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_sub;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_constructor;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_true;
 
 import com.google.common.primitives.Ints;
 import java.math.BigInteger;
@@ -104,8 +105,11 @@ public Integer equal(Integer pParam1, Integer pParam2) {
 
   @Override
   public Integer distinctImpl(List<Integer> pNumbers) {
-    int[] numberTerms = Ints.toArray(pNumbers);
-    return yices_distinct(numberTerms.length, numberTerms);
+    if (pNumbers.size() < 2) {
+      return yices_true();
+    } else {
+      return yices_distinct(pNumbers.size(), Ints.toArray(pNumbers));
+    }
   }
 
   @Override

src/org/sosy_lab/java_smt/test/NumeralFormulaManagerTest.java

@@ -69,6 +69,13 @@ public void distinctTest3() throws SolverException, InterruptedException {
     assertThatFormula(bmgr.and(imgr.distinct(symbols), bmgr.and(constraints))).isUnsatisfiable();
   }
 
+  @Test
+  public void trivialDistinctTest() throws SolverException, InterruptedException {
+    requireIntegers();
+    assertThatFormula(imgr.distinct(ImmutableList.of())).isTautological();
+    assertThatFormula(imgr.distinct(ImmutableList.of(imgr.makeVariable("a")))).isTautological();
+  }
+
   @Test
   public void trivialSumTest() throws SolverException, InterruptedException {
     requireIntegers();