Add realTrunc and realRoundEven operations to fill out the

standard rounding modes.

Add test cases that prove the rounding operations satisfy their specifications.

Fixes #46

what4-abc/src/What4/Solver/ABC.hs

@@ -540,6 +540,7 @@ bitblastExpr h ae = do
     SBVToInteger{} -> intFail
 
     RoundReal{} -> realFail
+    RoundEvenReal{} -> realFail
     FloorReal{} -> realFail
     CeilReal{}  -> realFail
     RealToInteger{} -> intFail

what4/src/What4/Expr/AppTheory.hs

@@ -208,6 +208,7 @@ appTheory a0 =
     SBVToInteger{}  -> LinearArithTheory
 
     RoundReal{} -> LinearArithTheory
+    RoundEvenReal{} -> LinearArithTheory
     FloorReal{} -> LinearArithTheory
     CeilReal{}  -> LinearArithTheory
     RealToInteger{} -> LinearArithTheory

what4/src/What4/Expr/Builder.hs

@@ -823,6 +823,7 @@ data App (e :: BaseType -> Type) (tp :: BaseType) where
   IntegerToBV  :: (1 <= w) => !(e BaseIntegerType) -> NatRepr w -> App e (BaseBVType w)
 
   RoundReal :: !(e BaseRealType) -> App e BaseIntegerType
+  RoundEvenReal :: !(e BaseRealType) -> App e BaseIntegerType
   FloorReal :: !(e BaseRealType) -> App e BaseIntegerType
   CeilReal  :: !(e BaseRealType) -> App e BaseIntegerType
 
@@ -1244,6 +1245,7 @@ appType a =
     RealSqrt{} -> knownRepr
 
     RoundReal{} -> knownRepr
+    RoundEvenReal{} -> knownRepr
     FloorReal{} -> knownRepr
     CeilReal{}  -> knownRepr
 
@@ -1657,6 +1659,7 @@ abstractEval f a0 = do
     SBVToInteger x -> valueRange (Inclusive lx) (Inclusive ux)
       where (lx, ux) = BVD.sbounds (bvWidth x) (f x)
     RoundReal x -> mapRange roundAway (ravRange (f x))
+    RoundEvenReal x -> mapRange round (ravRange (f x))
     FloorReal x -> mapRange floor (ravRange (f x))
     CeilReal x  -> mapRange ceiling (ravRange (f x))
     IntegerToNat x -> intRangeToNatRange (f x)
@@ -1987,6 +1990,7 @@ ppApp' a0 = do
     SBVToInteger x  -> ppSExpr "sbvToInteger" [x]
 
     RoundReal x -> ppSExpr "round" [x]
+    RoundEvenReal x -> ppSExpr "roundEven" [x]
     FloorReal x -> ppSExpr "floor" [x]
     CeilReal  x -> ppSExpr "ceil"  [x]
 
@@ -3289,6 +3293,7 @@ reduceApp sym a0 = do
     IntegerToBV x w -> integerToBV sym x w
 
     RoundReal x -> realRound sym x
+    RoundEvenReal x -> realRoundEven sym x
     FloorReal x -> realFloor sym x
     CeilReal  x -> realCeil sym x
 
@@ -5527,6 +5532,17 @@ instance IsExprBuilder (ExprBuilder t st fs) where
       -- Unsimplified case
     | otherwise = sbMakeExpr sym (RoundReal x)
 
+  realRoundEven sym x
+      -- Ground case
+    | SemiRingLiteral SR.SemiRingRealRepr r l <- x = return $ SemiRingLiteral SR.SemiRingIntegerRepr (round r) l
+      -- Match integerToReal
+    | Just (IntegerToReal xi) <- asApp x = return xi
+      -- Static case
+    | Just True <- ravIsInteger (exprAbsValue x) =
+      sbMakeExpr sym (RealToInteger x)
+      -- Unsimplified case
+    | otherwise = sbMakeExpr sym (RoundEvenReal x)
+
   realFloor sym x
       -- Ground case
     | SemiRingLiteral SR.SemiRingRealRepr r l <- x = return $ SemiRingLiteral SR.SemiRingIntegerRepr (floor r) l

what4/src/What4/Expr/GroundEval.hs

@@ -497,6 +497,7 @@ evalGroundApp f0 a0 = do
     SBVToInteger x -> BV.asSigned (bvWidth x) <$> f x
 
     RoundReal x -> roundAway <$> f x
+    RoundEvenReal x -> round <$> f x
     FloorReal x -> floor <$> f x
     CeilReal  x -> ceiling <$> f x
 

what4/src/What4/Interface.hs

@@ -1345,16 +1345,29 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
 
   -- | Round a real number to an integer.
   --
-  -- Numbers are rounded to the nearest representable number, with rounding away from
+  -- Numbers are rounded to the nearest integer, with rounding away from
   -- zero when two integers are equi-distant (e.g., 1.5 rounds to 2).
   realRound :: sym -> SymReal sym -> IO (SymInteger sym)
 
+  -- | Round a real number to an integer.
+  --
+  -- Numbers are rounded to the neareset integer, with rounding toward
+  -- even values when two integers are equi-distant (e.g., 2.5 rounds to 2).
+  realRoundEven :: sym -> SymReal sym -> IO (SymInteger sym)
+
   -- | Round down to the nearest integer that is at most this value.
   realFloor :: sym -> SymReal sym -> IO (SymInteger sym)
 
   -- | Round up to the nearest integer that is at least this value.
   realCeil :: sym -> SymReal sym -> IO (SymInteger sym)
 
+  -- | Round toward zero.  This is @floor(x)@ when x is positive
+  --   and @celing(x)@ when @x@ is negative.
+  realTrunc :: sym -> SymReal sym -> IO (SymInteger sym)
+  realTrunc sym x =
+    do pneg <- realLt sym x =<< realLit sym 0
+       iteM intIte sym pneg (realCeil sym x) (realFloor sym x)
+
   -- | Convert an integer to a bitvector.  The result is the unique bitvector
   --   whose value (signed or unsigned) is congruent to the input integer, modulo @2^w@.
   --

what4/src/What4/Protocol/SMTWriter.hs

@@ -2630,6 +2630,19 @@ appSMTExpr ae = do
       addSideCondition "round" $ x .>= 0 .|| negExpr
       return nm
 
+    RoundEvenReal xe -> do
+      checkIntegerSupport i
+      x <- mkBaseExpr xe
+      nm <- asBase <$> freshConstant "roundEven" IntegerTypeMap
+      r <- asBase <$> freshBoundTerm RealTypeMap (termIntegerToReal nm)
+      -- Assert that `x` is in the interval `[r, r+1]`
+      addSideCondition "roundEven" $ (r .<= x) .&& (x .<= r+1)
+      diff <- asBase <$> freshBoundTerm RealTypeMap (x - r)
+      freshBoundTerm IntegerTypeMap $
+        ite (diff .< rationalTerm 0.5) nm $
+          ite (diff .> rationalTerm 0.5) (nm+1) $
+            ite (intDivisible nm 2) nm (nm+1)
+
     FloorReal xe -> do
       checkIntegerSupport i
       x <- mkBaseExpr xe

what4/test/ExprBuilderSMTLib2.hs

@@ -477,6 +477,74 @@ testBoundVarAsFree = testCase "boundvarasfree" $ withOnlineZ3 $ \sym s -> do
   expectFailure $ checkSatisfiable s "test" px
   expectFailure $ checkSatisfiable s "test" py
 
+
+roundingTest ::
+  OnlineSolver t solver =>
+  SimpleExprBuilder t fs ->
+  SolverProcess t solver ->
+  IO ()
+roundingTest sym solver =
+  do r <- freshConstant sym (userSymbol' "r") BaseRealRepr
+
+     let runErrTest nm op errOp =
+           do diff <- realAbs sym =<< realSub sym r =<< integerToReal sym =<< op sym r
+              p'   <- notPred sym =<< errOp diff
+              res  <- checkSatisfiable solver nm p'
+              isUnsat res @? nm
+
+     runErrTest "floor"   realFloor (\diff -> realLt sym diff =<< realLit sym 1)
+     runErrTest "ceiling" realCeil  (\diff -> realLt sym diff =<< realLit sym 1)
+     runErrTest "trunc"   realTrunc (\diff -> realLt sym diff =<< realLit sym 1)
+     runErrTest "rna"     realRound (\diff -> realLe sym diff =<< realLit sym 0.5)
+     runErrTest "rne"     realRoundEven (\diff -> realLe sym diff =<< realLit sym 0.5)
+
+     -- floor test
+     do ri <- integerToReal sym =<< realFloor sym r
+        p  <- realLe sym ri r
+
+        res <- checkSatisfiable solver "floorTest" =<< notPred sym p
+        isUnsat res @? "floorTest"
+
+     -- ceiling test
+     do ri <- integerToReal sym =<< realCeil sym r
+        p  <- realLe sym r ri
+
+        res <- checkSatisfiable solver "ceilingTest" =<< notPred sym p
+        isUnsat res @? "ceilingTest"
+
+     -- truncate test
+     do ri <- integerToReal sym =<< realTrunc sym r
+        rabs  <- realAbs sym r
+        riabs <- realAbs sym ri
+        p  <- realLe sym riabs rabs
+
+        res <- checkSatisfiable solver "truncateTest" =<< notPred sym p
+        isUnsat res @? "truncateTest"
+
+     -- round away test
+     do ri <- integerToReal sym =<< realRound sym r
+        diff <- realAbs sym =<< realSub sym r ri
+        ptie <- realEq sym diff =<< realLit sym 0.5
+        rabs <- realAbs sym r
+        iabs <- realAbs sym ri
+        plarge <- realGt sym iabs rabs
+
+        res <- checkSatisfiable solver "rnaTest" =<<
+                  andPred sym ptie =<< notPred sym plarge
+        isUnsat res @? "rnaTest"
+
+     -- round-to-even test
+     do i <- realRoundEven sym r
+        ri <- integerToReal sym i
+        diff <- realAbs sym =<< realSub sym r ri
+        ptie <- realEq sym diff =<< realLit sym 0.5
+        ieven <- intDivisible sym i 2
+
+        res <- checkSatisfiable solver "rneTest" =<<
+                 andPred sym ptie =<< notPred sym ieven
+        isUnsat res @? "rneTest"
+
+
 zeroTupleTest ::
   OnlineSolver t solver =>
   SimpleExprBuilder t fs ->
@@ -886,4 +954,8 @@ main = defaultMain $ testGroup "Tests"
 
   , testCase "CVC4 binder tuple1" $ withCVC4 binderTupleTest1
   , testCase "CVC4 binder tuple2" $ withCVC4 binderTupleTest2
+
+  , testCase "Z3 rounding" $ withOnlineZ3 roundingTest
+  , testCase "Yices rounding" $ withYices roundingTest
+  , testCase "CVC4 rounding" $ withCVC4 roundingTest
   ]