Adds an ability to specify a floating point rounding mode.

Either using an option, or explicitly.
Closes #63.

Author: cheshire

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -35,6 +35,7 @@
 import org.sosy_lab.common.configuration.Options;
 import org.sosy_lab.common.io.PathCounterTemplate;
 import org.sosy_lab.common.log.LogManager;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.logging.LoggingSolverContext;
 import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5SolverContext;
@@ -86,9 +87,13 @@ public enum Solvers {
   @Option(secure = true, description = "Which SMT solver to use.")
   private Solvers solver = Solvers.SMTINTERPOL;
 
-  @Option(secure = true, name = "useLogger", description = "Log solver actions, this may be slow!")
+  @Option(secure = true, description = "Log solver actions, this may be slow!")
   private boolean useLogger = false;
 
+  @Option(secure = true, description = "Default rounding mode for floating point operations.")
+  private FloatingPointRoundingMode floatingPointRoundingMode =
+      FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN;
+
   private final LogManager logger;
   private final ShutdownNotifier shutdownNotifier;
   private final Configuration config;
@@ -147,17 +152,20 @@ private SolverContext generateContext0(Solvers solverToCreate)
         // Loading SmtInterpol is difficult as it requires its own class
         // loader for fiddling with Java_CUP versions.
         return getFactoryForSolver(createSmtInterpolClassLoader(logger), SMTINTERPOL_FACTORY_CLASS)
-            .create(config, logger, shutdownNotifier, logfile, randomSeed);
+            .create(
+                config, logger, shutdownNotifier, logfile, randomSeed, floatingPointRoundingMode);
 
       case MATHSAT5:
-        return Mathsat5SolverContext.create(logger, config, shutdownNotifier, logfile, randomSeed);
+        return Mathsat5SolverContext.create(
+            logger, config, shutdownNotifier, logfile, randomSeed, floatingPointRoundingMode);
 
       case Z3:
 
         // Z3 requires its own custom class loader to perform trickery with the
         // java.library.path without affecting the main class loader.
         return getFactoryForSolver(z3ClassLoader, Z3_FACTORY_CLASS)
-            .create(config, logger, shutdownNotifier, logfile, randomSeed);
+            .create(
+                config, logger, shutdownNotifier, logfile, randomSeed, floatingPointRoundingMode);
 
       case PRINCESS:
         // TODO: pass randomSeed to Princess
@@ -225,13 +233,20 @@ public SolverContext create(
         LogManager logger,
         ShutdownNotifier pShutdownNotifier,
         @Nullable PathCounterTemplate solverLogfile,
-        long randomSeed)
+        long randomSeed,
+        FloatingPointRoundingMode pFloatingPointRoundingMode)
         throws InvalidConfigurationException {
       final Thread currentThread = Thread.currentThread();
       final ClassLoader contextClassLoader = currentThread.getContextClassLoader();
       try {
         currentThread.setContextClassLoader(this.getClass().getClassLoader());
-        return generateSolverContext(config, logger, pShutdownNotifier, solverLogfile, randomSeed);
+        return generateSolverContext(
+            config,
+            logger,
+            pShutdownNotifier,
+            solverLogfile,
+            randomSeed,
+            pFloatingPointRoundingMode);
       } finally {
         currentThread.setContextClassLoader(contextClassLoader);
       }
@@ -242,7 +257,8 @@ protected abstract SolverContext generateSolverContext(
         LogManager logger,
         ShutdownNotifier pShutdownNotifier,
         @Nullable PathCounterTemplate solverLogfile,
-        long randomSeed)
+        long randomSeed,
+        FloatingPointRoundingMode pFloatingPointRoundingMode)
         throws InvalidConfigurationException;
   }
 

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

@@ -20,43 +20,94 @@
 package org.sosy_lab.java_smt.api;
 
 import org.sosy_lab.common.rationals.Rational;
+import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
 
 import java.math.BigDecimal;
 
+/**
+ * Floating point operations.
+ *
+ * Most operations are overloaded: there is an option of either using the default
+ * rounding mode (set via the option {@code solver.floatingPointRoundingMode}),
+ * or providing the rounding mode explicitly.
+ */
 public interface FloatingPointFormulaManager {
-  FloatingPointFormula makeNumber(double n, FormulaType.FloatingPointType type);
 
-  FloatingPointFormula makeNumber(BigDecimal n, FormulaType.FloatingPointType type);
+  FloatingPointFormula makeNumber(double n, FloatingPointType type);
+
+  FloatingPointFormula makeNumber(
+      double n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
+
+  FloatingPointFormula makeNumber(BigDecimal n, FloatingPointType type);
+
+  FloatingPointFormula makeNumber(
+      BigDecimal n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
+
+  FloatingPointFormula makeNumber(String n, FloatingPointType type);
+
+  FloatingPointFormula makeNumber(
+      String n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
 
-  FloatingPointFormula makeNumber(String n, FormulaType.FloatingPointType type);
+  FloatingPointFormula makeNumber(Rational n, FloatingPointType type);
 
-  FloatingPointFormula makeNumber(Rational n, FormulaType.FloatingPointType type);
+  FloatingPointFormula makeNumber(
+      Rational n, FloatingPointType type, FloatingPointRoundingMode pFloatingPointRoundingMode);
 
-  FloatingPointFormula makeVariable(String pVar, FormulaType.FloatingPointType type);
+  FloatingPointFormula makeVariable(String pVar, FloatingPointType type);
 
-  FloatingPointFormula makePlusInfinity(FormulaType.FloatingPointType type);
+  FloatingPointFormula makePlusInfinity(FloatingPointType type);
 
-  FloatingPointFormula makeMinusInfinity(FormulaType.FloatingPointType type);
+  FloatingPointFormula makeMinusInfinity(FloatingPointType type);
 
-  FloatingPointFormula makeNaN(FormulaType.FloatingPointType type);
+  FloatingPointFormula makeNaN(FloatingPointType type);
 
   <T extends Formula> T castTo(FloatingPointFormula number, FormulaType<T> targetType);
 
+  <T extends Formula> T castTo(
+      FloatingPointFormula number,
+      FormulaType<T> targetType,
+      FloatingPointRoundingMode pFloatingPointRoundingMode);
+
+  FloatingPointFormula castFrom(Formula number, boolean signed, FloatingPointType targetType);
+
   FloatingPointFormula castFrom(
-      Formula number, boolean signed, FormulaType.FloatingPointType targetType);
+      Formula number,
+      boolean signed,
+      FloatingPointType targetType,
+      FloatingPointRoundingMode pFloatingPointRoundingMode);
 
   // ----------------- Arithmetic relations, return type NumeralFormula -----------------
 
   FloatingPointFormula negate(FloatingPointFormula number);
 
   FloatingPointFormula add(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  FloatingPointFormula add(
+      FloatingPointFormula number1,
+      FloatingPointFormula number2,
+      FloatingPointRoundingMode pFloatingPointRoundingMode);
+
   FloatingPointFormula subtract(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  FloatingPointFormula subtract(
+      FloatingPointFormula number1,
+      FloatingPointFormula number2,
+      FloatingPointRoundingMode pFloatingPointRoundingMode);
+
   FloatingPointFormula divide(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  FloatingPointFormula divide(
+      FloatingPointFormula number1,
+      FloatingPointFormula number2,
+      FloatingPointRoundingMode pFloatingPointRoundingMode);
+
   FloatingPointFormula multiply(FloatingPointFormula number1, FloatingPointFormula number2);
 
+  FloatingPointFormula multiply(
+      FloatingPointFormula number1,
+      FloatingPointFormula number2,
+      FloatingPointRoundingMode pFloatingPointRoundingMode);
+
   // ----------------- Numeric relations, return type BooleanFormula -----------------
 
   /**