Merge pull request #363 from leventeBajczi/fp.rem

Add fp.rem operation to FloatingPointFormulaManager

Author: kfriedberger

src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java

@@ -201,6 +201,13 @@ FloatingPointFormula multiply(
       FloatingPointFormula number2,
       FloatingPointRoundingMode pFloatingPointRoundingMode);
 
+  /**
+   * remainder: x - y * n, where n in Z is nearest to x/y. The result can be negative even for two
+   * positive arguments, e.g. "rem(5, 4) == 1" and "rem(5, 6) == -1", as opposed to integer modulo
+   * operators.
+   */
+  FloatingPointFormula remainder(FloatingPointFormula dividend, FloatingPointFormula divisor);
+
   // ----------------- Numeric relations, return type BooleanFormula -----------------
 
   /**

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

@@ -374,6 +374,14 @@ public FloatingPointFormula multiply(
   protected abstract TFormulaInfo multiply(
       TFormulaInfo pParam1, TFormulaInfo pParam2, TFormulaInfo pFloatingPointRoundingMode);
 
+  @Override
+  public FloatingPointFormula remainder(
+      FloatingPointFormula number1, FloatingPointFormula number2) {
+    return wrap(remainder(extractInfo(number1), extractInfo(number2)));
+  }
+
+  protected abstract TFormulaInfo remainder(TFormulaInfo pParam1, TFormulaInfo pParam2);
+
   @Override
   public BooleanFormula assignment(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2) {
     TFormulaInfo param1 = extractInfo(pNumber1);

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsFloatingPointFormulaManager.java

@@ -263,6 +263,13 @@ public FloatingPointFormula multiply(
     return delegate.multiply(pNumber1, pNumber2, pFloatingPointRoundingMode);
   }
 
+  @Override
+  public FloatingPointFormula remainder(
+      FloatingPointFormula number1, FloatingPointFormula number2) {
+    stats.fpOperations.getAndIncrement();
+    return delegate.remainder(number1, number2);
+  }
+
   @Override
   public BooleanFormula assignment(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2) {
     stats.fpOperations.getAndIncrement();

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedFloatingPointFormulaManager.java

@@ -297,6 +297,14 @@ public FloatingPointFormula multiply(
     }
   }
 
+  @Override
+  public FloatingPointFormula remainder(
+      FloatingPointFormula number1, FloatingPointFormula number2) {
+    synchronized (sync) {
+      return delegate.remainder(number1, number2);
+    }
+  }
+
   @Override
   public BooleanFormula assignment(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2) {
     synchronized (sync) {

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

@@ -281,6 +281,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);