RoundingMode: Add a test for visitors on rounding mode formulas

Author: daniel-raffler

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

@@ -32,15 +32,21 @@
 import org.sosy_lab.java_smt.api.FloatingPointNumber;
 import org.sosy_lab.java_smt.api.FloatingPointNumber.Sign;
 import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingModeFormula;
+import org.sosy_lab.java_smt.api.Formula;
 import org.sosy_lab.java_smt.api.FormulaType;
 import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.api.FunctionDeclaration;
+import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
 import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
 import org.sosy_lab.java_smt.api.Model;
 import org.sosy_lab.java_smt.api.Model.ValueAssignment;
 import org.sosy_lab.java_smt.api.NumeralFormula;
 import org.sosy_lab.java_smt.api.ProverEnvironment;
+import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
 
 public class FloatingPointFormulaManagerTest
     extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
@@ -87,6 +93,66 @@ public void floatingPointType() {
         .isEqualTo(type.getMantissaSize());
   }
 
+  @Test
+  public void roundingModeVisitor() {
+    FloatingPointFormula var =
+        fpmgr.makeVariable("a", FloatingPointType.getSinglePrecisionFloatingPointType());
+    FloatingPointFormula f = fpmgr.sqrt(var, FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN);
+
+    for (FloatingPointRoundingMode rm : FloatingPointRoundingMode.values()) {
+      if (solver == Solvers.MATHSAT5 && rm == FloatingPointRoundingMode.NEAREST_TIES_AWAY) {
+        // SKIP MathSAT does not support rounding mode "nearest-ties-away"
+        continue;
+      }
+      // Build a term with a different rounding mode, then replace it in the visitor
+      FloatingPointFormula g =
+          (FloatingPointFormula)
+              mgr.visit(
+                  fpmgr.sqrt(var, rm),
+                  new FormulaVisitor<Formula>() {
+                    @Override
+                    public Formula visitFreeVariable(Formula f, String name) {
+                      return f;
+                    }
+
+                    @Override
+                    public Formula visitConstant(Formula f, Object value) {
+                      assertThat(f).isInstanceOf(FloatingPointRoundingModeFormula.class);
+                      assertThat(value).isInstanceOf(FloatingPointRoundingMode.class);
+                      assertThat(value).isEqualTo(rm);
+
+                      // Return the default rounding mode
+                      return fpmgr.makeRoundingMode(FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN);
+                    }
+
+                    @Override
+                    public Formula visitFunction(
+                        Formula f, List<Formula> args, FunctionDeclaration<?> functionDeclaration) {
+                      assertThat(functionDeclaration.getKind())
+                          .isEqualTo(FunctionDeclarationKind.FP_SQRT);
+                      assertThat(args.size()).isEqualTo(2);
+                      return mgr.makeApplication(
+                          functionDeclaration,
+                          mgr.visit(args.get(0), this),
+                          mgr.visit(args.get(1), this));
+                    }
+
+                    @Override
+                    public Formula visitQuantifier(
+                        BooleanFormula f,
+                        Quantifier quantifier,
+                        List<Formula> boundVariables,
+                        BooleanFormula body) {
+                      throw new IllegalArgumentException(
+                          String.format("Unexpected quantifier %s", quantifier));
+                    }
+                  });
+
+      // Check that after the substitution the rounding mode is the default again
+      assertThat(f).isEqualTo(g);
+    }
+  }
+
   @Test
   public void negative() throws SolverException, InterruptedException {
     for (double d : new double[] {-1, -2, -0.0, Double.NEGATIVE_INFINITY}) {