Add tests for division by zero

Author: daniel-raffler

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

@@ -9,12 +9,14 @@
 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 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;
@@ -26,6 +28,78 @@
 
 public class NumeralFormulaManagerTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
 
+  @Test
+  public void divZeroTest() throws SolverException, InterruptedException {
+    requireIntegers();
+    assume().that(solver).isNoneOf(Solvers.OPENSMT, Solvers.YICES2); // No division by zero
+
+    IntegerFormula zero = imgr.makeNumber(0);
+    IntegerFormula three = imgr.makeNumber(3);
+    IntegerFormula seven = imgr.makeNumber(7);
+
+    // Show that 3/0=0 and 3/0=7 can hold separately
+    IntegerFormula f1 = imgr.divide(three, zero);
+    assertThatFormula(imgr.equal(f1, zero)).isSatisfiable();
+    assertThatFormula(imgr.equal(f1, seven)).isSatisfiable();
+
+    // But if 3/0=0 in the model, it can't also be another value
+    IntegerFormula var = imgr.makeVariable("var");
+    IntegerFormula f2 = imgr.divide(var, zero);
+    IntegerFormula res = imgr.makeVariable("res");
+    assertThatFormula(
+            bmgr.and(
+                imgr.equal(f1, zero),
+                imgr.equal(var, three),
+                imgr.equal(f2, res),
+                bmgr.not(imgr.equal(res, zero))))
+        .isUnsatisfiable();
+
+    // Show that a=b => a/0=b/0
+    IntegerFormula var1 = imgr.makeVariable("arg1");
+    IntegerFormula var2 = imgr.makeVariable("arg2");
+    assertThatFormula(
+            bmgr.implication(
+                imgr.equal(var1, var2),
+                imgr.equal(imgr.divide(var1, zero), imgr.divide(var2, zero))))
+        .isTautological();
+  }
+
+  @Test
+  public void modZeroTest() throws SolverException, InterruptedException {
+    requireIntegers();
+    assume().that(solver).isNoneOf(Solvers.OPENSMT, Solvers.YICES2); // No division by zero
+
+    IntegerFormula zero = imgr.makeNumber(0);
+    IntegerFormula three = imgr.makeNumber(3);
+    IntegerFormula seven = imgr.makeNumber(7);
+
+    // Show that 3%0=0 and 3%0=7 can hold separately
+    IntegerFormula f1 = imgr.modulo(three, zero);
+    assertThatFormula(imgr.equal(f1, zero)).isSatisfiable();
+    assertThatFormula(imgr.equal(f1, seven)).isSatisfiable();
+
+    // But if 3%0=0 in the model, it can't also be another value
+    IntegerFormula var = imgr.makeVariable("var");
+    IntegerFormula f2 = imgr.modulo(var, zero);
+    IntegerFormula res = imgr.makeVariable("res");
+    assertThatFormula(
+            bmgr.and(
+                imgr.equal(f1, zero),
+                imgr.equal(var, three),
+                imgr.equal(f2, res),
+                bmgr.not(imgr.equal(res, zero))))
+        .isUnsatisfiable();
+
+    // Show that a=b => a%0=b%0
+    IntegerFormula var1 = imgr.makeVariable("arg1");
+    IntegerFormula var2 = imgr.makeVariable("arg2");
+    assertThatFormula(
+            bmgr.implication(
+                imgr.equal(var1, var2),
+                imgr.equal(imgr.modulo(var1, zero), imgr.modulo(var2, zero))))
+        .isTautological();
+  }
+
   @Test
   public void distinctTest() throws SolverException, InterruptedException {
     requireIntegers();