Formatted using ant format-source

Author: leventeBajczi

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

@@ -8,7 +8,6 @@
 
 package org.sosy_lab.java_smt.api;
 
-import com.microsoft.z3.Native;
 import java.math.BigDecimal;
 import org.sosy_lab.common.rationals.Rational;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
@@ -203,11 +202,10 @@ FloatingPointFormula multiply(
       FloatingPointRoundingMode pFloatingPointRoundingMode);
 
   /**
-   * remainder: x - y * n, where n in Z is nearest to x/y
+   * remainder: x - y * n, where n in Z is nearest to x/y. Can be negative even or two positive
+   * arguments (as opposed to integer modulo operators)
    */
-  FloatingPointFormula remainder(
-      FloatingPointFormula number1,
-      FloatingPointFormula number2);
+  FloatingPointFormula remainder(FloatingPointFormula number1, FloatingPointFormula number2);
 
   // ----------------- Numeric relations, return type BooleanFormula -----------------
 

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

@@ -376,8 +376,7 @@ protected abstract TFormulaInfo multiply(
 
   @Override
   public FloatingPointFormula remainder(
-      FloatingPointFormula number1,
-      FloatingPointFormula number2) {
+      FloatingPointFormula number1, FloatingPointFormula number2) {
     return wrap(remainder(extractInfo(number1), extractInfo(number2)));
   }
 

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

@@ -265,8 +265,7 @@ public FloatingPointFormula multiply(
 
   @Override
   public FloatingPointFormula remainder(
-      FloatingPointFormula number1,
-      FloatingPointFormula number2) {
+      FloatingPointFormula number1, FloatingPointFormula number2) {
     stats.fpOperations.getAndIncrement();
     return delegate.remainder(number1, number2);
   }

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

@@ -299,8 +299,7 @@ public FloatingPointFormula multiply(
 
   @Override
   public FloatingPointFormula remainder(
-      FloatingPointFormula number1,
-      FloatingPointFormula number2) {
+      FloatingPointFormula number1, FloatingPointFormula number2) {
     synchronized (sync) {
       return delegate.remainder(number1, number2);
     }

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

@@ -204,8 +204,10 @@ public void fpremNormal() throws SolverException, InterruptedException {
         .that(solver == Solvers.MATHSAT5)
         .isFalse();
 
-    for (FloatingPointType prec : new FloatingPointType[]{singlePrecType, doublePrecType,
-        FormulaType.getFloatingPointType(5, 6)}) {
+    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);
@@ -229,8 +231,10 @@ public void fpremSpecial() throws SolverException, InterruptedException {
         .that(solver == Solvers.MATHSAT5)
         .isFalse();
 
-    for (FloatingPointType prec : new FloatingPointType[]{singlePrecType, doublePrecType,
-        FormulaType.getFloatingPointType(5, 6)}) {
+    for (FloatingPointType prec :
+        new FloatingPointType[] {
+          singlePrecType, doublePrecType, FormulaType.getFloatingPointType(5, 6)
+        }) {
 
       final FloatingPointFormula num = fpmgr.makeNumber(42, prec);
 
@@ -242,7 +246,6 @@ public void fpremSpecial() throws SolverException, InterruptedException {
       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);