Add tests for #461

Author: daniel-raffler

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

@@ -9,23 +9,135 @@
 package org.sosy_lab.java_smt.test;
 
 import static com.google.common.truth.Truth.assertThat;
+import static com.google.common.truth.TruthJUnit.assume;
 import static org.junit.Assert.assertThrows;
 
 import com.google.common.collect.ImmutableList;
 import java.util.ArrayList;
 import java.util.List;
+import java.util.function.BiFunction;
+import java.util.function.Function;
 import org.junit.Test;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
 import org.sosy_lab.java_smt.api.BooleanFormula;
 import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FunctionDeclaration;
+import org.sosy_lab.java_smt.api.NumeralFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
 import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
 import org.sosy_lab.java_smt.api.SolverException;
 import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor;
 
 public class NumeralFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
 
+  /** Require that the solver supports mixed integer-real arithmetics */
+  private void requireMixedArithmetics() {
+    requireIntegers();
+    requireRationals();
+    assume().that(solver).isNotEqualTo(Solvers.OPENSMT); // OpenSMT does not support mixed terms
+  }
+
+  /** Check if this unary operation returns the expected value. */
+  private void testOperation(
+      Function<NumeralFormula, NumeralFormula> f, NumeralFormula arg, NumeralFormula expected)
+      throws SolverException, InterruptedException {
+    assertThatFormula(rmgr.equal(f.apply(arg), expected)).isSatisfiable();
+    assertThat(mgr.getFormulaType(f.apply(arg)).isRationalType()).isTrue();
+  }
+
+  /** Same as unary testOperation(), but we expect the result to be an integer term. */
+  private void testIntegerOperation(
+      Function<NumeralFormula, IntegerFormula> f, NumeralFormula arg, IntegerFormula expected)
+      throws SolverException, InterruptedException {
+    assertThatFormula(imgr.equal(f.apply(arg), expected)).isSatisfiable();
+    assertThat(mgr.getFormulaType(f.apply(arg)).isIntegerType()).isTrue();
+  }
+
+  /** Check if this binary operation returns the expected value. */
+  private void testOperation(
+      BiFunction<NumeralFormula, NumeralFormula, NumeralFormula> f,
+      NumeralFormula arg1,
+      NumeralFormula arg2,
+      NumeralFormula expected)
+      throws SolverException, InterruptedException {
+    assertThatFormula(rmgr.equal(f.apply(arg1, arg2), expected)).isSatisfiable();
+    assertThat(mgr.getFormulaType(f.apply(arg1, arg2)).isRationalType()).isTrue();
+  }
+
+  @Test
+  public void mixedNegationTest() throws SolverException, InterruptedException {
+    requireMixedArithmetics();
+    testOperation(rmgr::negate, imgr.makeNumber(1.5), rmgr.makeNumber(-1.0));
+    testOperation(rmgr::negate, rmgr.makeNumber(1.5), rmgr.makeNumber(-1.5));
+  }
+
+  @Test
+  public void mixedFloorTest() throws SolverException, InterruptedException {
+    requireRationalFloor();
+    requireMixedArithmetics();
+    testIntegerOperation(rmgr::floor, imgr.makeNumber(1.0), imgr.makeNumber(1.0));
+    testIntegerOperation(rmgr::floor, rmgr.makeNumber(1.5), imgr.makeNumber(1.0));
+  }
+
+  @Test
+  public void mixedAdditionTest() throws SolverException, InterruptedException {
+    requireMixedArithmetics();
+    testOperation(rmgr::add, imgr.makeNumber(2), imgr.makeNumber(1), rmgr.makeNumber(3.0));
+    testOperation(rmgr::add, imgr.makeNumber(2), rmgr.makeNumber(1.5), rmgr.makeNumber(3.5));
+    testOperation(rmgr::add, rmgr.makeNumber(1.5), imgr.makeNumber(2), rmgr.makeNumber(3.5));
+    testOperation(rmgr::add, rmgr.makeNumber(1.5), rmgr.makeNumber(2.5), rmgr.makeNumber(4.0));
+  }
+
+  @Test
+  public void mixedSubtractionTest() throws SolverException, InterruptedException {
+    requireMixedArithmetics();
+    testOperation(rmgr::subtract, imgr.makeNumber(2), imgr.makeNumber(1), rmgr.makeNumber(1.0));
+    testOperation(rmgr::subtract, imgr.makeNumber(2), rmgr.makeNumber(1.5), rmgr.makeNumber(0.5));
+    testOperation(rmgr::subtract, rmgr.makeNumber(1.5), imgr.makeNumber(2), rmgr.makeNumber(-0.5));
+    testOperation(rmgr::subtract, rmgr.makeNumber(1.5), rmgr.makeNumber(0.5), rmgr.makeNumber(1.0));
+  }
+
+  @Test
+  public void mixedDivisionTest() throws SolverException, InterruptedException {
+    requireMixedArithmetics();
+    testOperation(rmgr::divide, imgr.makeNumber(1), imgr.makeNumber(2), rmgr.makeNumber(0.5));
+    testOperation(rmgr::divide, imgr.makeNumber(1), rmgr.makeNumber(2.0), rmgr.makeNumber(0.5));
+    testOperation(rmgr::divide, rmgr.makeNumber(1.0), imgr.makeNumber(2), rmgr.makeNumber(0.5));
+    testOperation(rmgr::divide, rmgr.makeNumber(1.0), rmgr.makeNumber(0.5), rmgr.makeNumber(2.0));
+  }
+
+  @Test
+  public void mixedMultiplicationTest() throws SolverException, InterruptedException {
+    requireMixedArithmetics();
+    testOperation(rmgr::multiply, imgr.makeNumber(2), imgr.makeNumber(3), rmgr.makeNumber(6.0));
+    testOperation(rmgr::multiply, imgr.makeNumber(2), rmgr.makeNumber(1.25), rmgr.makeNumber(2.5));
+    testOperation(rmgr::multiply, rmgr.makeNumber(1.25), imgr.makeNumber(2), rmgr.makeNumber(2.5));
+    testOperation(
+        rmgr::multiply, rmgr.makeNumber(1.5), rmgr.makeNumber(2.5), rmgr.makeNumber(3.75));
+  }
+
+  @Test
+  public void mixedEqualityTest() throws SolverException, InterruptedException {
+    requireMixedArithmetics();
+    assertThatFormula(rmgr.equal(imgr.makeNumber(1.5), rmgr.makeNumber(1.0))).isSatisfiable();
+    assertThatFormula(rmgr.equal(rmgr.makeNumber(1.0), imgr.makeNumber(1.5))).isSatisfiable();
+  }
+
+  @Test
+  public void mixedGreaterThanTest() throws SolverException, InterruptedException {
+    requireMixedArithmetics();
+    assertThatFormula(rmgr.greaterThan(imgr.makeNumber(1.5), rmgr.makeNumber(0.5))).isSatisfiable();
+    assertThatFormula(rmgr.greaterThan(rmgr.makeNumber(1.5), imgr.makeNumber(1.5))).isSatisfiable();
+  }
+
+  @Test
+  public void mixedLessThanTest() throws SolverException, InterruptedException {
+    requireMixedArithmetics();
+    assertThatFormula(rmgr.lessThan(imgr.makeNumber(1.5), rmgr.makeNumber(1.5))).isSatisfiable();
+    assertThatFormula(rmgr.lessThan(rmgr.makeNumber(0.5), imgr.makeNumber(1.5))).isSatisfiable();
+  }
+
   @Test
   public void distinctTest() throws SolverException, InterruptedException {
     requireIntegers();