Implemented fp.rem in solvers, added tests

Author: leventeBajczi

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

@@ -280,6 +280,11 @@ protected Expr multiply(Expr pParam1, Expr pParam2, Expr pRoundingMode) {
     return exprManager.mkExpr(Kind.FLOATINGPOINT_MULT, pRoundingMode, pParam1, pParam2);
   }
 
+  @Override
+  protected Expr remainder(Expr pParam1, Expr pParam2) {
+    return exprManager.mkExpr(Kind.FLOATINGPOINT_REM, pParam1, pParam2);
+  }
+
   @Override
   protected Expr assignment(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.EQUAL, pParam1, pParam2);

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

@@ -317,6 +317,11 @@ protected Term multiply(Term pParam1, Term pParam2, Term pRoundingMode) {
     return solver.mkTerm(Kind.FLOATINGPOINT_MULT, pRoundingMode, pParam1, pParam2);
   }
 
+  @Override
+  protected Term remainder(Term pParam1, Term pParam2) {
+    return solver.mkTerm(Kind.FLOATINGPOINT_REM, pParam1, pParam2);
+  }
+
   @Override
   protected Term assignment(Term pParam1, Term pParam2) {
     return solver.mkTerm(Kind.EQUAL, pParam1, pParam2);

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java

@@ -248,6 +248,11 @@ protected Long multiply(Long pNumber1, Long pNumber2, Long pRoundingMode) {
     return msat_make_fp_times(mathsatEnv, pRoundingMode, pNumber1, pNumber2);
   }
 
+  @Override
+  protected Long remainder(Long pParam1, Long pParam2) {
+    throw new UnsupportedOperationException("MathSAT5 does not implement fp.rem");
+  }
+
   @Override
   protected Long divide(Long pNumber1, Long pNumber2, Long pRoundingMode) {
     return msat_make_fp_div(mathsatEnv, pRoundingMode, pNumber1, pNumber2);

src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java

@@ -216,6 +216,11 @@ protected Long multiply(Long pNumber1, Long pNumber2, Long pRoundingMode) {
     return Native.mkFpaMul(z3context, pRoundingMode, pNumber1, pNumber2);
   }
 
+  @Override
+  protected Long remainder(Long pParam1, Long pParam2) {
+    return Native.mkFpaRem(z3context, pParam1, pParam2);
+  }
+
   @Override
   protected Long divide(Long pNumber1, Long pNumber2, Long pRoundingMode) {
     return Native.mkFpaDiv(z3context, pRoundingMode, pNumber1, pNumber2);

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

@@ -197,6 +197,83 @@ public void sqrt() throws SolverException, InterruptedException {
     }
   }
 
+  @Test
+  public void fpremNormal() throws SolverException, InterruptedException {
+    assume()
+        .withMessage("MathSAT5 does not implement fp.rem")
+        .that(solver == Solvers.MATHSAT5)
+        .isFalse();
+
+    for (FloatingPointType prec : new FloatingPointType[]{singlePrecType, doublePrecType,
+        FormulaType.getFloatingPointType(5, 6)}) {
+
+      final FloatingPointFormula five = fpmgr.makeNumber(5, prec);
+      final FloatingPointFormula four = fpmgr.makeNumber(4, prec);
+      final FloatingPointFormula six = fpmgr.makeNumber(6, prec);
+
+      final FloatingPointFormula one = fpmgr.makeNumber(1, prec);
+      final FloatingPointFormula minusOne = fpmgr.makeNumber(-1, prec);
+
+      final FloatingPointFormula expr1 = fpmgr.remainder(five, four);
+      final FloatingPointFormula expr2 = fpmgr.remainder(five, six);
+
+      assertThatFormula(fpmgr.assignment(expr1, one)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr2, minusOne)).isTautological();
+    }
+  }
+
+  @Test
+  public void fpremSpecial() throws SolverException, InterruptedException {
+    assume()
+        .withMessage("MathSAT5 does not implement fp.rem")
+        .that(solver == Solvers.MATHSAT5)
+        .isFalse();
+
+    for (FloatingPointType prec : new FloatingPointType[]{singlePrecType, doublePrecType,
+        FormulaType.getFloatingPointType(5, 6)}) {
+
+      final FloatingPointFormula num = fpmgr.makeNumber(42, prec);
+
+      final FloatingPointFormula nan = fpmgr.makeNumber("NaN", prec);
+      final FloatingPointFormula zero = fpmgr.makeNumber("0", prec);
+      final FloatingPointFormula inf = fpmgr.makePlusInfinity(prec);
+
+      final FloatingPointFormula minusNan = fpmgr.makeNumber("-NaN", prec);
+      final FloatingPointFormula minusZero = fpmgr.makeNumber("0", prec);
+      final FloatingPointFormula minusInf = fpmgr.makeMinusInfinity(prec);
+
+
+      final FloatingPointFormula expr1 = fpmgr.remainder(nan, nan);
+      final FloatingPointFormula expr2 = fpmgr.remainder(zero, zero);
+      final FloatingPointFormula expr3 = fpmgr.remainder(inf, inf);
+
+      final FloatingPointFormula expr4 = fpmgr.remainder(minusNan, minusNan);
+      final FloatingPointFormula expr5 = fpmgr.remainder(minusZero, minusZero);
+      final FloatingPointFormula expr6 = fpmgr.remainder(minusInf, minusInf);
+
+      final FloatingPointFormula expr7 = fpmgr.remainder(num, nan);
+      final FloatingPointFormula expr8 = fpmgr.remainder(num, zero);
+      final FloatingPointFormula expr9 = fpmgr.remainder(num, inf);
+
+      final FloatingPointFormula expr10 = fpmgr.remainder(num, minusNan);
+      final FloatingPointFormula expr11 = fpmgr.remainder(num, minusZero);
+      final FloatingPointFormula expr12 = fpmgr.remainder(num, minusInf);
+
+      assertThatFormula(fpmgr.assignment(expr1, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr2, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr3, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr4, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr5, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr6, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr7, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr8, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr9, num)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr10, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr11, nan)).isTautological();
+      assertThatFormula(fpmgr.assignment(expr12, num)).isTautological();
+    }
+  }
+
   @Test
   public void specialValueFunctions() throws SolverException, InterruptedException {
     assertThatFormula(fpmgr.isInfinity(posInf)).isTautological();