Match new z3 output

Data/SBV.hs

@@ -1295,15 +1295,15 @@ Q.E.D.
 Q.E.D.
 >>> prove $ roundTrip @Int32
 Falsifiable. Counter-example:
-  s0 = RoundNearestTiesToAway :: RoundingMode
-  s1 =             -740395022 :: Int32
+  s0 = RoundNearestTiesToEven :: RoundingMode
+  s1 =              -16891903 :: Int32
 
 Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float:
 
->>> toRational (-740395022 :: Float)
-(-740395008) % 1
+>>> toRational (-16891903 :: Float)
+(-16891904) % 1
 
-Note how the numerator is different, it is off by 14. This is hardly surprising, since floats become sparser as
+Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as
 the magnitude increases to be able to cover all the integer values representable.
 
 >>> :{
@@ -1325,16 +1325,16 @@ Q.E.D.
 Q.E.D.
 >>> prove $ roundTrip @Int64
 Falsifiable. Counter-example:
-  s0 = RoundTowardPositive :: RoundingMode
-  s1 = 1152921504606846896 :: Int64
+  s0 = RoundNearestTiesToEven :: RoundingMode
+  s1 =    -144678154135535600 :: Int64
 
 Just like in the `SFloat` case, once we reach 64-bits, we no longer can exactly represent the
 integer value for all possible values:
 
->>> toRational (fromIntegral (1152921504606846896 :: Int64) :: Double)
-1152921504606846848 % 1
+>>> toRational (fromIntegral (-144678154135535600 :: Int64) :: Double)
+(-144678154135535616) % 1
 
-In this case the numerator is off by 48.
+In this case the numerator is off by 16.
 -}
 
 -- | An implementation of rotate-left, using a barrel shifter like design. Only works when both

Documentation/SBV/Examples/Existentials/CRCPolynomial.hs

@@ -69,7 +69,7 @@ genPoly hd maxCnt = do res <- allSatWith defaultSMTCfg{allSatMaxModelCount = Jus
 -- We have:
 --
 -- >>> findHD4Polynomials 2
--- Polynomial #1. x^16 + x^3 + x^2 + 1
+-- Polynomial #1. x^16 + x^6 + x^3 + 1
 -- Polynomial #2. x^16 + x^2 + x + 1
 -- Found: 2 polynomial(s).
 --

Documentation/SBV/Examples/Misc/Floating.hs

@@ -66,19 +66,19 @@ assocPlus x y z = x + (y + z) .== (x + y) + z
 --
 -- >>> assocPlusRegular
 -- Falsifiable. Counter-example:
---   x =  2097149.9 :: Float
---   y =  13.999817 :: Float
---   z = -1.9998167 :: Float
+--   x = -1.1529219e18 :: Float
+--   y =  5.8411555e11 :: Float
+--   z = -3.5919253e19 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let x =  2097149.9 :: Float
--- >>> let y =  13.999817 :: Float
--- >>> let z = -1.9998167 :: Float
+-- >>> let x = -1.1529219e18 :: Float
+-- >>> let y =  5.8411555e11 :: Float
+-- >>> let z = -3.5919253e19 :: Float
 -- >>> x + (y + z)
--- 2097162.0
+-- -3.7072176e19
 -- >>> (x + y) + z
--- 2097161.8
+-- -3.707217e19
 --
 -- Note the difference in the results!
 assocPlusRegular :: IO ThmResult
@@ -100,13 +100,13 @@ assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"]
 --
 -- >>> nonZeroAddition
 -- Falsifiable. Counter-example:
---   a =   -7.441692e23 :: Float
---   b = -7.5039685e-27 :: Float
+--   a = 1.4495462e-36 :: Float
+--   b =       4.5e-44 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let a =   -7.441692e23 :: Float
--- >>> let b = -7.5039685e-27 :: Float
+-- >>> let a = 1.4495462e-36 :: Float
+-- >>> let b =       4.5e-44 :: Float
 -- >>> a + b == a
 -- True
 -- >>> b == 0
@@ -129,13 +129,13 @@ nonZeroAddition = prove $ do [a, b] <- sFloats ["a", "b"]
 --
 -- >>> multInverse
 -- Falsifiable. Counter-example:
---   a = -5.69379e-39 :: Float
+--   a = -1.7414917e38 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let a = -5.69379e-39 :: Float
+-- >>> let a = -1.7414917e38 :: Float
 -- >>> a * (1/a)
--- 0.99999994
+-- 0.9999999
 multInverse :: IO ThmResult
 multInverse = prove $ do a <- sFloat "a"
                          constrain $ fpIsPoint a
@@ -155,28 +155,28 @@ multInverse = prove $ do a <- sFloat "a"
 --
 -- >>> roundingAdd
 -- Satisfiable. Model:
---   rm = RoundTowardZero :: RoundingMode
---   x  =  -1.0579198e-37 :: Float
---   y  =   4.7017266e-38 :: Float
+--   rm = RoundTowardPositive :: RoundingMode
+--   x  =                -2.0 :: Float
+--   y  =       1.2621775e-29 :: Float
 --
 -- (Note that depending on your version of Z3, you might get a different result.)
 -- Unfortunately Haskell floats do not allow computation with arbitrary rounding modes, but SBV's
 -- 'SFloatingPoint' type does. We have:
 --
--- >>> fpAdd sRoundTowardZero (-1.0579198e-37) (4.7017266e-38) :: SFPSingle
--- -5.87747119e-38 :: SFloatingPoint 8 24
--- >>> fpAdd sRoundNearestTiesToEven (-1.0579198e-37) (4.7017266e-38) :: SFPSingle
--- -5.87747175e-38 :: SFloatingPoint 8 24
+-- >>> fpAdd sRoundTowardPositive (-2.0) (1.2621775e-29) :: SFPSingle
+-- -1.99999988 :: SFloatingPoint 8 24
+-- >>> fpAdd sRoundNearestTiesToEven (-2.0) (1.2621775e-29) :: SFPSingle
+-- -2.0 :: SFloatingPoint 8 24
 --
--- We can see why these two results are indeed different: The 'RoundTowardZero'
--- (which rounds towards zero) produces a larger result, closer to 0. Indeed, if we treat these numbers
+-- We can see why these two results are indeed different: The 'RoundTowardPositive'
+-- (which rounds towards positive infinity) produces a larger result, closer to 0. Indeed, if we treat these numbers
 -- as 'Double' values, we get:
 --
--- >>> (-1.0579198e-37) + (4.7017266e-38) :: Double
--- -5.8774714e-38
+-- >>> (-2.0) + 1.2621775e-29 :: Double
+-- -2.0
 --
--- we see that the "more precise" result is larger than what the 'Float' value is, justifying the
--- larger value with 'RoundTowardZero'. A more detailed study is beyond our current scope, so we'll
+-- we see that the "more precise" result is smaller than what the 'Float' value is, justifying the
+-- larger value with 'RoundTowardPositive'. A more detailed study is beyond our current scope, so we'll
 -- merely note that floating point representation and semantics is indeed a thorny
 -- subject, and point to <http://ece.uwaterloo.ca/~dwharder/NumericalAnalysis/02Numerics/Double/paper.pdf> as
 -- an excellent guide.

Documentation/SBV/Examples/Misc/Newtypes.hs

@@ -81,12 +81,12 @@ ceilingHighEnoughForHuman ceiling humanHeight = humanHeight' .< ceiling'
 --
 -- >>> sat problem
 -- Satisfiable. Model:
---   floorToCeiling =  16 :: Integer
---   humanheight    = 255 :: Word16
+--   floorToCeiling =   3 :: Integer
+--   humanheight    = 272 :: Word16
 problem :: Predicate
 problem = do
     ceiling     :: SMetres          <- free "floorToCeiling"
     humanHeight :: SHumanHeightInCm <- free "humanheight"
-    constrain $ humanHeight .<= tallestHumanEver
+    constrain $ humanHeight .== tallestHumanEver
 
     return $ ceilingHighEnoughForHuman ceiling humanHeight

Documentation/SBV/Examples/Misc/ProgramPaths.hs

@@ -48,36 +48,36 @@ d4 x y = d1 x y + d2 y + d3 x y
 --
 -- >>> paths
 -- Solution #1:
---   x =   7 :: Integer
+--   x =  -2 :: Integer
 --   y =   4 :: Integer
---   r = 217 :: Integer
+--   r = 112 :: Integer
 -- Solution #2:
---   x =   4 :: Integer
---   y =   0 :: Integer
---   r = 257 :: Integer
--- Solution #3:
---   x =   3 :: Integer
---   y =  -1 :: Integer
---   r = 157 :: Integer
--- Solution #4:
---   x =  -1 :: Integer
+--   x =   0 :: Integer
 --   y =   3 :: Integer
---   r = 152 :: Integer
--- Solution #5:
+--   r = 252 :: Integer
+-- Solution #3:
 --   x =  -1 :: Integer
 --   y =   4 :: Integer
 --   r = 212 :: Integer
+-- Solution #4:
+--   x =   3 :: Integer
+--   y =   0 :: Integer
+--   r = 257 :: Integer
+-- Solution #5:
+--   x =   2 :: Integer
+--   y =  -1 :: Integer
+--   r = 157 :: Integer
 -- Solution #6:
---   x =   0 :: Integer
---   y =   3 :: Integer
---   r = 252 :: Integer
--- Solution #7:
---   x =  -2 :: Integer
+--   x =   7 :: Integer
 --   y =   4 :: Integer
---   r = 112 :: Integer
+--   r = 217 :: Integer
+-- Solution #7:
+--   x =   0 :: Integer
+--   y =   0 :: Integer
+--   r = 152 :: Integer
 -- Found 7 different solutions.
 paths :: IO AllSatResult
 paths = allSat $ do
   x <- sInteger "x"
   y <- sInteger "y"
-  partition "r" $ d4 x y
+  partition "r" $ d4 x y

Documentation/SBV/Examples/Uninterpreted/Multiply.hs

@@ -47,12 +47,12 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo)
 -- >>> sat synthMul22
 -- Satisfiable. Model:
 --   mul22_hi :: Bool -> Bool -> Bool -> Bool -> Bool
---   mul22_hi True  False False True  = True
---   mul22_hi True  True  False True  = True
 --   mul22_hi False True  True  True  = True
---   mul22_hi True  False True  True  = True
+--   mul22_hi True  True  False True  = True
+--   mul22_hi True  False False True  = True
 --   mul22_hi False True  True  False = True
 --   mul22_hi True  True  True  False = True
+--   mul22_hi True  False True  True  = True
 --   mul22_hi _     _     _     _     = False
 -- <BLANKLINE>
 --   mul22_lo :: Bool -> Bool -> Bool
@@ -67,12 +67,12 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo)
 --
 -- >>> :{
 -- mul22_hi :: (SBool, SBool, SBool, SBool) -> SBool
--- mul22_hi params = params `sElem` [ (sTrue,  sFalse, sFalse, sTrue)
+-- mul22_hi params = params `sElem` [ (sFalse, sTrue,  sTrue,  sTrue)
 --                                  , (sTrue,  sTrue,  sFalse, sTrue)
---                                  , (sFalse, sTrue,  sTrue,  sTrue)
---                                  , (sTrue,  sFalse, sTrue,  sTrue)
+--                                  , (sTrue,  sFalse, sFalse, sTrue)
 --                                  , (sFalse, sTrue,  sTrue,  sFalse)
 --                                  , (sTrue,  sTrue,  sTrue,  sFalse)
+--                                  , (sTrue,  sFalse, sTrue,  sTrue)
 --                                  ]
 -- :}
 --

SBVTestSuite/GoldFiles/charConstr08.gold

@@ -36,8 +36,7 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (lambda ((x!1 String))
-         (and (not (and (not (= x!1 "A")) (not (= x!1 "B")))) (not (= x!1 "B"))))))
+[RECV] ((s0 (lambda ((x!1 String)) (= x!1 "A"))))
 
 MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",{'A'} :: {Char})], modelUIFuns = []}
 DONE.*** Solver   : Z3

SBVTestSuite/GoldFiles/query_uisatex1.gold

@@ -117,12 +117,12 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (- 1)))
+[RECV] ((s0 0))
 [GOOD] (set-option :pp.max_depth      4294967295)
 [GOOD] (set-option :pp.min_alias_size 4294967295)
 [GOOD] (set-option :model.inline_def  true      )
 [SEND] (get-value (q1))
-[RECV] ((q1 (store (store (store ((as const (Array Int Int)) 12) 3 75) (- 3) 9) (- 1) 0)))
+[RECV] ((q1 (store (store (store ((as const (Array Int Int)) 12) 3 75) (- 3) 9) 0 1)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store (store ((as const (Array Bool Int Int)) 5) false 7 6) false 12 3)))
 [SEND] (get-value (q3))
@@ -164,10 +164,10 @@
 
  FINAL:
 Satisfiable. Model:
-  s0 = -1 :: Integer
+  s0 = 0 :: Integer
 
   q1 :: Integer -> Integer
-  q1 (-1) = 0 
+  q1 0    = 1 
   q1 (-3) = 9 
   q1 3    = 75
   q1 _    = 12

SBVTestSuite/GoldFiles/query_uisatex2.gold

@@ -119,7 +119,7 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store (store (store ((as const (Array Int Int)) 12) 3 75) (- 3) 9) (- 1) 0)))
+[RECV] ((q1 (store (store (store ((as const (Array Int Int)) 12) 3 75) (- 3) 9) 0 1)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store (store ((as const (Array Bool Int Int)) 5) false 7 6) false 12 3)))
 [SEND] (get-value (q3))
@@ -162,5 +162,5 @@
 *** Exit code: ExitSuccess
 
  FINAL:
-(Right ([(-1,0),(-3,9),(3,75)],12),Right ([((False,12),3),((False,7),6)],5),Right ([((9.6,False,8),Infinity),((9.6,True,121),-0.0)],8.6),Right ([(('r',"foo"),3.5),(('c',"tey"),92.0)],78.0),Right ([(([5],[8.2,0.0]),210),(([9,5],[8.2,9.0]),21)],7),Right ([],False))
+(Right ([(0,1),(-3,9),(3,75)],12),Right ([((False,12),3),((False,7),6)],5),Right ([((9.6,False,8),Infinity),((9.6,True,121),-0.0)],8.6),Right ([(('r',"foo"),3.5),(('c',"tey"),92.0)],78.0),Right ([(([5],[8.2,0.0]),210),(([9,5],[8.2,9.0]),21)],7),Right ([],False))
 DONE!

SBVTestSuite/GoldFiles/set_tupleSet.gold

@@ -34,12 +34,11 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (mkSBVTuple2 ((as const (Array Bool Bool)) true)
-                    (store ((as const (Array Bool Bool)) false) false true))))
+[RECV] ((s0 (mkSBVTuple2 ((as const (Array Bool Bool)) true) (lambda ((x!1 Bool)) x!1))))
 *** Solver   : Z3
 *** Exit code: ExitSuccess
 
 FINAL:
 Satisfiable. Model:
-  s0 = (U,{False}) :: ({Bool}, {Bool})
+  s0 = (U,{True}) :: ({Bool}, {Bool})
 DONE!

SBVTestSuite/GoldFiles/set_uninterp1.gold

@@ -104,7 +104,7 @@ Fast allSat, Looking for solution 8
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) C true)))
+[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) B true)))
 [GOOD] (push 1)
 [GOOD] (define-fun s22 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) B true))
 [GOOD] (define-fun s23 () Bool (= s0 s22))

SBVTestSuite/GoldFiles/sumBimapPlus.gold

@@ -48,8 +48,8 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (left_SBVEither (- 1))))
+[RECV] ((s0 (left_SBVEither 0)))
 
-MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Left -1 :: Either Integer Integer)], modelUIFuns = []}
+MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Left 0 :: Either Integer Integer)], modelUIFuns = []}
 DONE.*** Solver   : Z3
 *** Exit code: ExitSuccess

SBVTestSuite/GoldFiles/sumMaybe.gold

@@ -54,8 +54,8 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (just_SBVMaybe (- 1))))
+[RECV] ((s0 (just_SBVMaybe 0)))
 
-MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Just -1 :: Maybe Integer)], modelUIFuns = []}
+MODEL: SMTModel {modelObjectives = [], modelBindings = Nothing, modelAssocs = [("x",Just 0 :: Maybe Integer)], modelUIFuns = []}
 DONE.*** Solver   : Z3
 *** Exit code: ExitSuccess

SBVTestSuite/GoldFiles/validate_1.gold

@@ -29,11 +29,11 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (fp #b1 #xfe #b11111111111111111111111)))
+[RECV] ((s0 (_ -zero 8 24)))
 *** Solver   : Z3
 *** Exit code: ExitSuccess
 [VALIDATE] Validating the model. Assignment:
-[VALIDATE]       x = -3.4028235e38 :: Float
+[VALIDATE]       x = -0.0 :: Float
 [VALIDATE] There are no constraints to check.
 [VALIDATE] Validating outputs.
 
@@ -42,7 +42,7 @@ FINAL OUTPUT:
 *** 
 *** Assignment:
 *** 
-***       x = -3.4028235e38 :: Float
+***       x = -0.0 :: Float
 *** 
 *** Not all floating point operations are supported concretely.
 *** 
@@ -52,4 +52,4 @@ FINAL OUTPUT:
 *** Alleged model:
 ***
 *** Satisfiable. Model:
-***   x = -3.4028235e38 :: Float
+***   x = -0.0 :: Float