diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,32 @@ * Hackage: * GitHub: +### Version 14.6, 2026-08-18 + + * New TP example: Binary trees (`Documentation.SBV.Examples.TP.Tree`). Proves that mirroring + a tree is an involution, that it preserves the tree's size, and that the in-order traversal + of a mirrored tree is the reverse of the original's. + + * `Data.SBV.TP` now exports `atProxy`, which annotates a proof name with the type it is being + run at: `atProxy (Proxy @a) "myLemma"` gives `myLemma @Integer` when `a` is `Integer`. Handy + for polymorphic lemmas that get used at several types within a single proof, so each instance + shows up under its own name in the transcript. + + * Add `(.**)`, integer exponentiation following SMT-LIB's `**` operator over the `Int` theory. + Unlike `(.^)` (which mirrors Haskell's `^` and requires a non-negative, non-symbolic exponent), + `(.**)` is total and places no restriction on the exponent: it may be negative or symbolic. When + both arguments are concrete and the exponent is non-negative, the result is computed directly; + otherwise the application is emitted as SMT-LIB's `**` for the solver to interpret. Note that no + current solver supports `**`, so symbolic (or negative) exponentiation will typically come back + as `unknown` (or be rejected) until backend support arrives. Thanks to Ryan Scott for the pointer. + + * [DEVELOPERS ONLY] SBV used to rely on latest z3 compiled from github master. While this was + important as tools matured, it also created extra-work to keep track of daily z3 changes. Starting + with this release, we'll track only officially released latest version of z3, which should bring + more stability to both the build process and end users who most likely download binaries of z3. + This is also true for other solvers we support, i.e., we'll track only the officially released + versions, instead of their latest source code. + ### Version 14.5, 2026-07-26 * Add `sRationalToSReal` and `sRealToSRational`, converting between symbolic rationals and @@ -3185,18 +3211,13 @@ hackage can no longer compile it due to some dependency mismatch. * Add forgotten Real class instance for the type 'AlgReal' * Stop putting bounds on hackage dependencies, as they cause - more trouble then they actually help. (See the discussion - here: .) + more trouble then they actually help. ### Version 2.3, 2012-07-20 * Maintenance release, no new features. * Tweak cabal dependencies to avoid using packages that are newer - than those that come with ghc-7.4.2. Apparently this is a no-no - that breaks many things, see the discussion in this thread: - http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html - In particular, the use of containers >= 0.5 is *not* OK until we have - a version of GHC that comes with that version. + than those that come with ghc-7.4.2. ### Version 2.2, 2012-07-17 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -331,7 +331,7 @@ -- ** Splitting, joining, and extending bit-vectors , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake, ByteConverter(..) -- ** Exponentiation - , (.^) + , (.^), (.**) -- * IEEE-floating point numbers , IEEEFloating(..), RoundingMode(..), SRoundingMode, nan, infinity, sNaN, sInfinity -- ** Rounding modes @@ -1374,15 +1374,15 @@ Q.E.D. >>> prove $ roundTrip @Int32 Falsifiable. Counter-example: - s0 = RoundNearestTiesToAway :: RoundingMode - s1 = 22049281 :: Int32 + s0 = RoundNearestTiesToEven :: RoundingMode + s1 = -892327435 :: Int32 Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float: ->>> toRational (22049281 :: Float) -22049280 % 1 +>>> toRational (-892327435 :: Float) +(-892327424) % 1 -Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as +Note how the numerator is different, it is off by 11. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable. >>> :{ @@ -1404,16 +1404,16 @@ Q.E.D. >>> prove $ roundTrip @Int64 Falsifiable. Counter-example: - s0 = RoundNearestTiesToEven :: RoundingMode - s1 = 2305843026393563113 :: Int64 + s0 = RoundTowardPositive :: RoundingMode + s1 = -2370765003978487132 :: 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 (2305843026393563113 :: Int64) :: Double) -2305843026393563136 % 1 +>>> toRational (fromIntegral (-2370765003978487132 :: Int64) :: Double) +(-2370765003978487296) % 1 -In this case the numerator is off by 23. +In this case the numerator is off by 164. -} -- | An implementation of rotate-left, using a barrel shifter like design. Only works when both diff --git a/Data/SBV/Core/Model.hs b/Data/SBV/Core/Model.hs --- a/Data/SBV/Core/Model.hs +++ b/Data/SBV/Core/Model.hs @@ -37,7 +37,7 @@ , checkMutualGroup , SDivisible(..), SMTDefinable(..), QSaturate, qSaturateSavingObservables , Metric(..), minimize, maximize, assertWithPenalty, SIntegral, SFiniteBits(..) - , ite, iteLazy, sFromIntegral, sShiftLeft, sShiftRight, sRotateLeft, sBarrelRotateLeft, sRotateRight, sBarrelRotateRight, sSignedShiftArithRight, (.^) + , ite, iteLazy, sFromIntegral, sShiftLeft, sShiftRight, sRotateLeft, sBarrelRotateLeft, sRotateRight, sBarrelRotateRight, sSignedShiftArithRight, (.^), (.**) , some , oneIf, genVar, genVar_ , pbAtMost, pbAtLeast, pbExactly, pbLe, pbGe, pbEq, pbMutexed, pbStronglyMutexed @@ -2922,6 +2922,47 @@ blasted (iterate (\x -> x*x) b) infixr 8 .^ + +-- | Integer exponentiation, emitted as SMT-LIB's @**@ over the @Int@ theory. Unlike '.^' (which +-- mirrors Haskell's @^@), @.**@ places no restriction on the exponent: it may be negative or +-- symbolic. +-- +-- If both arguments are concrete and the exponent is non-negative, the result is computed and +-- returned as a literal. Otherwise the application is emitted as SMT-LIB's @**@, whose @Int@-theory +-- semantics are: for @n >= 0@, ordinary exponentiation (with @0 .** 0 == 1@); for @n < 0@, @0@ when +-- @m == 0@ or @abs m > 1@, and @m .** abs n@ when @abs m == 1@. +-- +-- N.B. Symbolic (or negative) integer exponentiation via @**@ is not supported by all solvers, so +-- such a query may come back as @unknown@ (or the solver may reject it outright). +-- +-- Concrete, non-negative exponents fold directly: +-- +-- >>> 2 .** 3 +-- 8 :: SInteger +-- >>> (-2) .** 3 +-- -8 :: SInteger +-- >>> 0 .** 0 +-- 1 :: SInteger +-- +-- Symbolic and negative exponents are handed to the solver, so they need a backend that +-- implements SMT-LIB's @**@. No solver supports it yet (as of July 2026), so the following +-- are illustrative only: +-- +-- @ +-- prove $ \\x -> x .** 2 .== x * x -- Q.E.D. +-- prove $ 2 .** (-3) .== 0 -- Q.E.D. +-- prove $ (-1) .** (-3) .== -1 -- Q.E.D. +-- @ +(.**) :: SInteger -> SInteger -> SInteger +m .** n + | Just b <- unliteral m, Just e <- unliteral n, e >= 0 + = literal (b ^ e) + | True + = SBV $ SVal KUnbounded $ Right $ cache r + where r st = do sm <- sbvToSV st m + sn <- sbvToSV st n + newExpr st KUnbounded (SBVApp (NonLinear NR_IntPow) [sm, sn]) +infixr 8 .** instance (Ord a, Num (SBV a), SymVal a, Fractional a) => Fractional (SBV a) where fromRational = literal . fromRational diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -336,25 +336,27 @@ | NR_Exp | NR_Log | NR_Pow + | NR_IntPow deriving (Eq, Ord, G.Data, NFData, Generic) -- | Show a non-linear op. Unfortunately this can't be generically done since different -- solvers use different names for some of these ops. showNROp :: Solver -> NROp -> String showNROp slvr = sh - where sh NR_Sin = "sin" - sh NR_Cos = "cos" - sh NR_Tan = "tan" - sh NR_ASin = arc ++ "sin" - sh NR_ACos = arc ++ "cos" - sh NR_ATan = arc ++ "tan" - sh NR_Sinh = "sinh" - sh NR_Cosh = "cosh" - sh NR_Tanh = "tanh" - sh NR_Sqrt = "sqrt" - sh NR_Exp = "exp" - sh NR_Log = "log" - sh NR_Pow = "pow" + where sh NR_Sin = "sin" + sh NR_Cos = "cos" + sh NR_Tan = "tan" + sh NR_ASin = arc ++ "sin" + sh NR_ACos = arc ++ "cos" + sh NR_ATan = arc ++ "tan" + sh NR_Sinh = "sinh" + sh NR_Cosh = "cosh" + sh NR_Tanh = "tanh" + sh NR_Sqrt = "sqrt" + sh NR_Exp = "exp" + sh NR_Log = "log" + sh NR_Pow = "pow" + sh NR_IntPow = "**" -- SMT-LIB Int-theory exponentiation -- DReal uses asin/acos etc. CVC5 uses arcsin. Other solvers probably -- don't even support these. But this isn't the right place to bail-out diff --git a/Data/SBV/RegExp.hs b/Data/SBV/RegExp.hs --- a/Data/SBV/RegExp.hs +++ b/Data/SBV/RegExp.hs @@ -88,7 +88,7 @@ -- >>> let phone = pre * "-" * post -- >>> sat $ \(s :: SString) -> s `match` phone -- Satisfiable. Model: --- s0 = "422-2222" :: String +-- s0 = "100-1000" :: String class RegExpMatchable a where -- | @`match` s r@ checks whether @s@ is in the language generated by @r@. match :: a -> RegExp -> SBool diff --git a/Data/SBV/TP.hs b/Data/SBV/TP.hs --- a/Data/SBV/TP.hs +++ b/Data/SBV/TP.hs @@ -44,6 +44,9 @@ -- * Creating instances of proofs , at, Inst(..) + -- * Naming proofs at specific types + , atProxy + -- * Faking proofs , sorry @@ -82,3 +85,4 @@ ) where import Data.SBV.TP.TP +import Data.SBV.Utils.Lib (atProxy) diff --git a/Data/SBV/Trans.hs b/Data/SBV/Trans.hs --- a/Data/SBV/Trans.hs +++ b/Data/SBV/Trans.hs @@ -69,7 +69,7 @@ -- ** Splitting, joining, and extending bit-vectors , bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake -- ** Exponentiation - , (.^) + , (.^), (.**) -- * IEEE-floating point numbers , IEEEFloating(..), RoundingMode(..), SRoundingMode, nan, infinity, sNaN, sInfinity -- ** Rounding modes diff --git a/Data/SBV/Utils/Numeric.hs b/Data/SBV/Utils/Numeric.hs --- a/Data/SBV/Utils/Numeric.hs +++ b/Data/SBV/Utils/Numeric.hs @@ -31,9 +31,7 @@ import Test.QuickCheck (Arbitrary(..), elements) -- | The SMT-Lib (in particular Z3) implementation for min/max for floats does not agree with --- Haskell's; and also it does not agree with what the hardware does. Sigh.. See: --- --- +-- Haskell's; and also it does not agree with what the hardware does. Sigh.. -- So, we codify here what the Z3 (SMTLib) is implementing for fpMax. -- The discrepancy with Haskell is that the NaN propagation doesn't work in Haskell -- The discrepancy with x86 is that given +0/-0, x86 returns the second argument; SMTLib is non-deterministic diff --git a/Documentation/SBV/Examples/ADT/Expr.hs b/Documentation/SBV/Examples/ADT/Expr.hs --- a/Documentation/SBV/Examples/ADT/Expr.hs +++ b/Documentation/SBV/Examples/ADT/Expr.hs @@ -110,9 +110,9 @@ -- -- >>> evalSat -- Satisfiable. Model: --- e = Let "h" (Val 1) (Var "h") :: Expr --- a = 9 :: Integer --- b = 10 :: Integer +-- e = Let "a" (Val 1313) (Add (Val (-1312)) (Var "a")) :: Expr +-- a = 9 :: Integer +-- b = 10 :: Integer evalSat :: IO SatResult evalSat = sat $ do e :: SExpr <- free "e" constrain $ isValid e @@ -129,8 +129,8 @@ -- -- >>> genE -- Satisfiable. Model: --- e1 = Let "k" (Mul (Val 1) (Mul (Val (-3)) (Val (-1)))) (Var "k") :: Expr --- e2 = Val (-2) :: Expr +-- e1 = Let "t" (Val 5) (Val 3) :: Expr +-- e2 = Val (-2) :: Expr genE :: IO SatResult genE = sat $ do e1 :: SExpr <- free "e1" e2 :: SExpr <- free "e2" @@ -146,7 +146,7 @@ -- | Query mode example. -- -- >>> queryE --- e1: (let k = (1 * (-3 * -1)) in k) +-- e1: (let t = 5 in 3) -- e2: -2 queryE :: IO () queryE = runSMT $ do diff --git a/Documentation/SBV/Examples/ADT/Param.hs b/Documentation/SBV/Examples/ADT/Param.hs --- a/Documentation/SBV/Examples/ADT/Param.hs +++ b/Documentation/SBV/Examples/ADT/Param.hs @@ -119,9 +119,9 @@ -- -- >>> evalSat -- Satisfiable. Model: --- e = Let "h" (Val 1) (Var "h") :: Expr String Integer --- a = 9 :: Integer --- b = 10 :: Integer +-- e = Let "a" (Val 1313) (Add (Val (-1312)) (Var "a")) :: Expr String Integer +-- a = 9 :: Integer +-- b = 10 :: Integer evalSat :: IO SatResult evalSat = sat $ do e :: SExpr String Integer <- free "e" constrain $ isValid isId e @@ -138,7 +138,7 @@ -- -- >>> genE -- Satisfiable. Model: --- e1 = Let "h" (Val 5) (Val 3) :: Expr String Integer +-- e1 = Let "s" (Val 5) (Val 3) :: Expr String Integer -- e2 = Val (-2) :: Expr String Integer genE :: IO SatResult genE = sat $ do e1 :: SExpr String Integer <- free "e1" @@ -155,9 +155,9 @@ -- | Query mode example. -- -- >>> queryE --- e1: (let a = ((let x = 20 in 4) * -5) in (-1 * -3)) +-- e1: (let a = (-1 * -3) in (a * 1)) -- e2: -2 --- e3: (let h = 79 % 80 in h) +-- e3: (let h = 77 % 78 in h) queryE :: IO () queryE = runSMT $ do e1 :: SExpr String Integer <- free "e1" diff --git a/Documentation/SBV/Examples/Existentials/Diophantine.hs b/Documentation/SBV/Examples/Existentials/Diophantine.hs --- a/Documentation/SBV/Examples/Existentials/Diophantine.hs +++ b/Documentation/SBV/Examples/Existentials/Diophantine.hs @@ -110,8 +110,8 @@ -- We have: -- -- >>> test --- (1+k, k', 2k+k') -- (k, 2+k', 2k+k') +-- (1+k, k', 2k+k') -- -- That is, for arbitrary @k@ and @k'@, we have two different solutions. (An infinite family.) -- You can verify these solutions by substituting the values for @x@, @y@ and @z@ in the above, for each choice. diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs --- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs @@ -127,26 +127,25 @@ >>> prove $ (qe (\(Forall x) -> p x) .|| qe (\(Forall x) -> q x)) .<=> qe (\(Forall x) -> p x .|| q x) Falsifiable. Counter-example: P :: U -> Bool + P U_1 = False P U_2 = True - P U_0 = True - P _ = False + P _ = True Q :: U -> Bool + Q U_1 = True Q U_2 = False - Q U_0 = False Q _ = True The solver found us a falsifying instance: Pick a domain with at least three elements. We'll call -the first element @U_2@, and the second element @U_0@, without naming the others. (Unfortunately the solver picks nonintuitive names, but you can substitute better names if you like. They're just names of two distinct -objects that belong to the domain \(U\) with no other meaning.) +the first element @U_1@, and the second element @U_2@, without naming the others. -Arrange so that \(P\) is true on @U_2@ and @U_0@, but false for everything else. -Also arrange so that \(Q\) is false on these two elements, but true for everything else. +Arrange so that \(P\) is false on @U_1@ true everywhere else. +Also arrange so that \(Q\) is false for @U_2@ but true for everything else. With this assignment, the right hand side of our conjecture is true no matter which element you pick, because either \(P\) or \(Q\) is true on any -given element. (Actually, only one will be true on any element, but that is tangential.) +given element, or both. But left-hand-side is not a tautology: Clearly neither \(P\) nor \(Q\) are true for all elements, and hence both disjuncts are false. Thus, the alleged conjecture is not an equivalence in first order logic. -} @@ -202,18 +201,18 @@ -- b _ = 0 -- -- d :: Word8 -> Word8 -> Word8 --- d a c = a + 255 * c +-- d a c = 255 * c + a -- -- Let's see what the solver said. It suggested we should use the value of @0@ for @b@, regardless of the -- choice of @a@. (Note how @b@ is a function of one variable, i.e., of @a@) --- And it suggested using @a + (255 * c)@ for @d@, +-- And it suggested using @255 * c + a@ for @d@, -- for whatever we choose for @a@ and @c@. Why does this work? Well, given -- arbitrary @a@ and @c@, we end up with: -- -- @ -- a + b >= c + d --- --> substitute b = 0 and d = a + 255c as suggested by the solver --- a + 0 >= c + a + 255c +-- --> substitute b = 0 and d = 255c + a as suggested by the solver +-- a + 0 >= c + 255c + a -- a >= 256c + a -- a >= a -- @ diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs --- a/Documentation/SBV/Examples/Misc/Floating.hs +++ b/Documentation/SBV/Examples/Misc/Floating.hs @@ -68,21 +68,21 @@ -- -- >>> assocPlusRegular -- Falsifiable. Counter-example: --- x = 2.5291315e20 :: Float --- y = -2.9558926e20 :: Float --- z = 1.1256507e20 :: Float +-- x = -0.3383789 :: Float +-- y = -27907.219 :: Float +-- z = -515389.94 :: Float -- -- Indeed, we have: -- --- >>> let x = 2.5291315e20 :: Float --- >>> let y = -2.9558926e20 :: Float --- >>> let z = 1.1256507e20 :: Float +-- >>> let x = -0.3383789 :: Float +-- >>> let y = -27907.219 :: Float +-- >>> let z = -515389.94 :: Float -- >>> x + (y + z) --- 6.988897e19 +-- -543297.44 -- >>> (x + y) + z --- 6.988896e19 +-- -543297.5 -- --- Note the significant difference in the results! +-- Note the precision difference in the results! assocPlusRegular :: IO ThmResult assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"] let lhs = x+(y+z) @@ -102,13 +102,13 @@ -- -- >>> nonZeroAddition -- Falsifiable. Counter-example: --- a = 2.9670994e34 :: Float --- b = -7.208359e-5 :: Float +-- a = -3.6509563e26 :: Float +-- b = 1.6777216e7 :: Float -- -- Indeed, we have: -- --- >>> let a = 2.9670994e34 :: Float --- >>> let b = -7.208359e-5 :: Float +-- >>> let a = -3.6509563e26 :: Float +-- >>> let b = 1.6777216e7 :: Float -- >>> a + b == a -- True -- >>> b == 0 @@ -131,11 +131,11 @@ -- -- >>> multInverse -- Falsifiable. Counter-example: --- a = -2.372672e38 :: Float +-- a = 5.2268255e-34 :: Float -- -- Indeed, we have: -- --- >>> let a = -2.372672e38 :: Float +-- >>> let a = 5.2268255e-34 :: Float -- >>> a * (1/a) -- 0.99999994 multInverse :: IO ThmResult @@ -158,24 +158,25 @@ -- >>> roundingAdd -- Satisfiable. Model: -- rm = RoundTowardPositive :: RoundingMode --- x = -4.0039067 :: Float --- y = 131076.0 :: Float +-- x = -2.341805e-38 :: Float +-- y = -1.83671e-40 :: 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: -- --- >>> sat $ \x -> x .== (fpAdd sRoundTowardPositive (-4.0039067) 131076.0 :: SFloat) +-- >>> sat $ \x -> x .== (fpAdd sRoundTowardPositive (-2.341805e-38) (-1.83671e-40) :: SFloat) -- Satisfiable. Model: --- s0 = 131072.0 :: Float --- >>> (-4.0039067) + 131076.0 :: Float --- 131071.99 +-- s0 = -2.360172e-38 :: Float +-- >>> (-2.360172e-38) + (-1.83671e-40 :: Float) +-- -2.378539e-38 -- -- We can see why these two results are indeed different: The 'RoundTowardPositive --- (which rounds towards positive infinity) produces a larger result. +-- (which rounds towards positive infinity) produces a larger result. If we do the computation +-- using double precision, we get: -- --- >>> (-4.0039067) + 131076.0 :: Double --- 131071.9960933 +-- >>> (-2.360172e-38) + (-1.83671e-40 :: Double) +-- -2.3785390999999997e-38 -- -- we see that the "more precise" result is larger than what the 'Float' value is, justifying the -- larger value with 'RoundTowardPositive. A more detailed study is beyond our current scope, so we'll diff --git a/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs --- a/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs +++ b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs @@ -131,8 +131,8 @@ -- Searching at depth: 4 -- Searching at depth: 5 -- Searching at depth: 6 --- Found: [10,10,9,11,14,6] -- Found: [10,10,11,9,14,6] +-- Found: [10,10,9,11,14,6] -- There are no more solutions. example :: IO () example = search initBoard finalBoard diff --git a/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs b/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs --- a/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs +++ b/Documentation/SBV/Examples/Puzzles/SquareBirthday.hs @@ -6,9 +6,6 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental -- --- As of January 2026, to access the careers link at , you need to solve the following --- puzzle: --- -- @ -- Suppose that today is June 1, 2025. We call a date "square" if all of its components (day, month, and year) are -- perfect squares. I was born in the last millennium, and my next birthday (relative to that date) will be the last diff --git a/Documentation/SBV/Examples/Strings/RegexCrossword.hs b/Documentation/SBV/Examples/Strings/RegexCrossword.hs --- a/Documentation/SBV/Examples/Strings/RegexCrossword.hs +++ b/Documentation/SBV/Examples/Strings/RegexCrossword.hs @@ -26,7 +26,7 @@ -- | Solve a given crossword, returning the corresponding rows solveCrossword :: [R.RegExp] -> [R.RegExp] -> IO [String] -solveCrossword rowRegExps colRegExps = runSMT $ do +solveCrossword rowRegExps colRegExps = runSMTWith cvc5 $ do let numRows = genericLength rowRegExps numCols = genericLength colRegExps diff --git a/Documentation/SBV/Examples/TP/Basics.hs b/Documentation/SBV/Examples/TP/Basics.hs --- a/Documentation/SBV/Examples/TP/Basics.hs +++ b/Documentation/SBV/Examples/TP/Basics.hs @@ -368,7 +368,7 @@ -- Lemma: badRevLen -- *** Failed to prove badRevLen. -- Falsifiable. Counter-example: --- xs = [17,17,17] :: [Integer] +-- xs = [20,20,20] :: [Integer] badRevLen :: IO () badRevLen = runTP $ void $ lemma "badRevLen" @@ -384,7 +384,7 @@ -- Lemma: badLengthProof -- *** Failed to prove badLengthProof. -- Falsifiable. Counter-example: --- xs = [12,15,19,25,32,42] :: [Integer] +-- xs = [13,16,19,24,34,42] :: [Integer] -- imp = 42 :: Integer -- spec = 6 :: Integer badLengthProof :: IO () diff --git a/Documentation/SBV/Examples/TP/GCD.hs b/Documentation/SBV/Examples/TP/GCD.hs --- a/Documentation/SBV/Examples/TP/GCD.hs +++ b/Documentation/SBV/Examples/TP/GCD.hs @@ -202,6 +202,7 @@ -- -- ==== __Proof__ -- >>> runTP dvdMul +-- Lemma: mulMod0 Q.E.D. -- Lemma: dvdMul -- Step: 1 (2 way case split) -- Step: 1.1 Q.E.D. @@ -211,22 +212,33 @@ -- Result: Q.E.D. -- [Proven] dvdMul :: Ɐd ∷ Integer → Ɐa ∷ Integer → Ɐk ∷ Integer → Bool dvdMul :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> Forall "k" Integer -> SBool)) -dvdMul = calc "dvdMul" - (\(Forall d) (Forall a) (Forall k) -> d `dvd` a .=> d `dvd` (k*a)) $ - \d a k -> [d `dvd` a] - |- cases [ d .== 0 ==> d `dvd` (k*a) - ?? a .== 0 - =: sTrue - =: qed - , d ./= 0 ==> d `dvd` (k*a) - =: (k*a) `sEMod` d .== 0 - ?? a .== d * a `sEDiv` d - ?? k * a .== d * (k * a `sEDiv` d) - ?? (d * (k * a `sEDiv` d)) `sEMod` d .== 0 - =: sTrue - =: qed - ] +dvdMul = do + -- The only genuinely nonlinear fact we need: any multiple of a nonzero @d@ leaves no + -- remainder modulo @d@. We prove it once, in isolation, so z3 sees the smallest possible + -- nonlinear goal. With this in hand, the divisibility argument below is pure substitution. + mulMod0 <- lemma "mulMod0" + (\(Forall @"d" d) (Forall @"y" y) -> d ./= 0 .=> (d * y) `sEMod` d .== 0) + [] + calc "dvdMul" + (\(Forall d) (Forall a) (Forall k) -> d `dvd` a .=> d `dvd` (k*a)) $ + \d a k -> [d `dvd` a] + |- cases [ d .== 0 ==> d `dvd` (k*a) + ?? a .== 0 + =: sTrue + =: qed + , d ./= 0 ==> let q = a `sEDiv` d + in d `dvd` (k*a) + =: (k*a) `sEMod` d .== 0 + -- @d@ divides @a@ exactly, so @a = d*q@, hence @k*a = d*(k*q)@ + ?? a .== d * q + ?? k * a .== d * (k * q) + -- and @d*(k*q)@ is a multiple of @d@, so its remainder is @0@ + ?? mulMod0 `at` (Inst @"d" d, Inst @"y" (k * q)) + =: sTrue + =: qed + ] + -- | \(a \mid |b| \iff a \mid b\) -- -- A number divides another exactly when it also divides its absolute value. This follows @@ -307,50 +319,76 @@ -- -- ==== __Proof__ -- >>> runTP dvdEvenWhenOdd +-- Lemma: dvdMul Q.E.D. +-- Lemma: dvdSelf +-- Step: 1 (2 way case split) +-- Step: 1.1 Q.E.D. +-- Step: 1.2.1 Q.E.D. +-- Step: 1.2.2 Q.E.D. +-- Step: 1.Completeness Q.E.D. +-- Result: Q.E.D. -- Lemma: dvdEvenWhenOdd --- Step: 1 Q.E.D. --- Step: 2 Q.E.D. --- Step: 3 Q.E.D. --- Step: 4 Q.E.D. --- Step: 5 Q.E.D. --- Step: 6 Q.E.D. --- Step: 7 Q.E.D. --- Result: Q.E.D. +-- Step: 1 Q.E.D. +-- Step: 2 Q.E.D. +-- Step: 3 Q.E.D. +-- Step: 4 Q.E.D. +-- Step: 5 Q.E.D. +-- Step: 6 Q.E.D. +-- Step: 7 Q.E.D. +-- Result: Q.E.D. -- [Proven] dvdEvenWhenOdd :: Ɐd ∷ Integer → Ɐa ∷ Integer → Bool dvdEvenWhenOdd :: TP (Proof (Forall "d" Integer -> Forall "a" Integer -> SBool)) -dvdEvenWhenOdd = calc "dvdEvenWhenOdd" - (\(Forall d) (Forall a) -> isOdd d .&& d `dvd` (2*a) .=> d `dvd` a) $ - \d a -> [isOdd d, d `dvd` (2*a)] - |- let t = (d - 1) `sEDiv` 2 - m = (2*a) `sEDiv` d - in sTrue +dvdEvenWhenOdd = do + dMul <- recall dvdMul - -- Observe that d = 2t+1 and 2a = dm - =: d .== 2*t + 1 .&& 2*a .== d*m + -- Every number divides itself. We could hand this to z3 directly, but as a raw fact it + -- forces it to reason about @d `sEMod` d@ with a symbolic divisor, which it is fickle at. + -- Spelling out the reduction keeps it robust. + dSelf <- calc "dvdSelf" + (\(Forall @"d" d) -> d `dvd` d) $ + \d -> [] |- cases [ d .== 0 ==> trivial + , d ./= 0 ==> d `dvd` d + =: d `sEMod` d .== 0 + =: sTrue + =: qed + ] - -- So, 2a == (2t+1)m holds - =: 2*a .== (2*t+1) * m + calc "dvdEvenWhenOdd" + (\(Forall d) (Forall a) -> isOdd d .&& d `dvd` (2*a) .=> d `dvd` a) $ + \d a -> [isOdd d, d `dvd` (2*a)] + |- let t = (d - 1) `sEDiv` 2 + m = (2*a) `sEDiv` d + in sTrue - -- Arithmetic gives us - =: 2*a .== 2*t*m + m .&& 2*(a-t*m) .== m + -- Observe that d = 2t+1 and 2a = dm + =: d .== 2*t + 1 .&& 2*a .== d*m - -- So m = 2*(a-t*m), i.e., m is even - =: m .== 2 * (a - t*m) + -- So, 2a == (2t+1)m holds + =: 2*a .== (2*t+1) * m - -- Let n = a - t*m, so m = 2n. It follows that 2a = d(2n) = 2(dn) - =: let n = a - t*m - in 2*a .== d * (2 * n) .&& 2 * a .== 2 * (d * n) + -- Arithmetic gives us + =: 2*a .== 2*t*m + m .&& 2*(a-t*m) .== m - -- From which we can conclude a = dn - =: a .== d * n + -- So m = 2*(a-t*m), i.e., m is even + =: m .== 2 * (a - t*m) - -- Thus we can deduce d must divide a - ?? d `dvd` (d * n) - =: d `dvd` a + -- Let n = a - t*m, so m = 2n. It follows that 2a = d(2n) = 2(dn) + =: let n = a - t*m + in 2*a .== d * (2 * n) .&& 2 * a .== 2 * (d * n) - -- Done! - =: qed + -- From which we can conclude a = dn + =: a .== d * n + -- Since d divides d (dSelf), it also divides any multiple of itself, in + -- particular d*n (dMul). As a == d*n, d divides a. We hand z3 these as + -- proven facts, so it doesn't have to rediscover the divisibility itself. + ?? dSelf `at` Inst @"d" d + ?? dMul `at` (Inst @"d" d, Inst @"a" d, Inst @"k" n) + =: d `dvd` a + + -- Done! + =: qed + -- | \(d \mid a \land d \mid b \implies d \mid (a + b)\) -- -- ==== __Proof__ @@ -868,6 +906,9 @@ -- >>> runTP gcdSubEquiv -- Lemma: commutative Q.E.D. -- Lemma: gcdAdd Q.E.D. +-- Lemma: gcdNonNeg +-- Step: 1 Q.E.D. +-- Result: Q.E.D. -- Inductive lemma (strong): nGCDSubEquiv -- Step: Measure is non-negative Q.E.D. -- Step: 1 (5 way case split) @@ -898,6 +939,20 @@ comm <- recall commutative addG <- recall gcdAdd + -- Bridge from the general @gcd@ (used by @comm@/@addG@) to @nGCD@ on non-negative inputs. + -- Since @gcd x y = nGCD (abs x) (abs y)@, this is just @abs@ elimination -- but proving it + -- here, in isolation, lets z3 close it by congruence (equal args => equal @nGCD@) instead of + -- unfolding the recursive @nGCD@. Handed to the induction below as an opaque equality, it + -- keeps z3 from diverging when relating @gcd@-facts to @nGCD@. + nnB <- calc "gcdNonNeg" + (\(Forall @"x" x) (Forall @"y" y) -> x .>= 0 .&& y .>= 0 .=> gcd x y .== nGCD x y) $ + \x y -> [x .>= 0, y .>= 0] + |- gcd x y + ?? abs x .== x + ?? abs y .== y + =: nGCD x y + =: qed + -- First prove over the non-negative numbers: nEq <- sInduct "nGCDSubEquiv" (\(Forall @"a" a) (Forall @"b" b) -> a .>= 0 .&& b .>= 0 .=> nGCDSub a b .== nGCD a b) @@ -911,16 +966,28 @@ ?? ih =: nGCD (a - b) b ?? addG `at` (Inst @"a" (a - b), Inst @"b" b) + ?? nnB `at` (Inst @"x" (a - b), Inst @"y" b) + ?? nnB `at` (Inst @"x" a, Inst @"y" b) =: nGCD a b =: qed , a .< b .&& a ./= 0 ==> nGCDSub a (b - a) ?? ih =: nGCD a (b - a) ?? comm + ?? nnB `at` (Inst @"x" a, Inst @"y" (b - a)) + ?? nnB `at` (Inst @"x" (b - a), Inst @"y" a) =: nGCD (b - a) a + -- @addG@ is stated over @gcd@; hand z3 the + -- @gcd = nGCD@ bridge (via @nnB@) as proven + -- equalities so it closes this by chaining + -- rather than unfolding the recursive @nGCD@. ?? addG `at` (Inst @"a" (b - a), Inst @"b" a) + ?? nnB `at` (Inst @"x" (b - a), Inst @"y" a) + ?? nnB `at` (Inst @"x" b, Inst @"y" a) =: nGCD b a ?? comm + ?? nnB `at` (Inst @"x" b, Inst @"y" a) + ?? nnB `at` (Inst @"x" a, Inst @"y" b) =: nGCD a b =: qed ] diff --git a/Documentation/SBV/Examples/TP/Lists.hs b/Documentation/SBV/Examples/TP/Lists.hs --- a/Documentation/SBV/Examples/TP/Lists.hs +++ b/Documentation/SBV/Examples/TP/Lists.hs @@ -78,6 +78,8 @@ import Prelude (Integer, Bool, Eq, ($), Num(..), id, (.), flip) +import Data.Proxy (Proxy(..)) + import Data.SBV import Data.SBV.List import Data.SBV.Tuple @@ -130,21 +132,41 @@ -- | @length (inits xs) == 1 + length xs@ -- -- >>> runTP $ initsLength @Integer +-- Lemma: initLength Q.E.D. -- Inductive lemma (strong): initsLength -- Step: Measure is non-negative Q.E.D. --- Step: 1 Q.E.D. +-- Step: 1 (2 way case split) +-- Step: 1.1 Q.E.D. +-- Step: 1.2.1 Q.E.D. +-- Step: 1.2.2 Q.E.D. +-- Step: 1.2.3 Q.E.D. +-- Step: 1.2.4 Q.E.D. +-- Step: 1.Completeness Q.E.D. -- Result: Q.E.D. -- Functions proven terminating: sbv.inits -- [Proven] initsLength :: Ɐxs ∷ [Integer] → Bool initsLength :: forall a. SymVal a => TP (Proof (Forall "xs" [a] -> SBool)) -initsLength = +initsLength = do + + initLength <- lemma "initLength" + (\(Forall @"xs" (xs :: SList a)) -> sNot (null xs) .=> length (init xs) .== length xs - 1) + [] + sInduct "initsLength" (\(Forall xs) -> length (inits xs) .== 1 + length xs) (length @a, []) $ - \ih xs -> [] |- length (inits xs) - ?? ih - =: 1 + length xs - =: qed + \ih xs -> [] |- length (inits xs) .== 1 + length xs + =: [pCase| xs of + [] -> trivial + whole@(_ : _) -> + length (inits whole) .== 1 + length whole + =: length (inits (init whole) ++ [whole]) .== 1 + length whole + =: 1 + length (inits (init whole)) .== 1 + length whole + ?? ih `at` Inst @"xs" (init whole) + ?? initLength `at` Inst @"xs" whole + =: sTrue + =: qed + |] -- | @length (tails xs) == 1 + length xs@ -- @@ -1513,19 +1535,23 @@ -- | @n .> 0 ==> drop n (x .: xs) == drop (n - 1) xs@ -- +-- Note that we name the lemma with the type it is proven at, using 'atProxy'. This way, a +-- proof that needs this lemma at several different types (as 'drop_map' does) gets a distinct +-- name for each instance. +-- -- >>> runTP $ drop_cons @Integer --- Lemma: drop_cons Q.E.D. --- [Proven] drop_cons :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool +-- Lemma: drop_cons @Integer Q.E.D. +-- [Proven] drop_cons @Integer :: Ɐn ∷ Integer → Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool drop_cons :: forall a. SymVal a => TP (Proof (Forall "n" Integer -> Forall "x" a -> Forall "xs" [a] -> SBool)) -drop_cons = lemma "drop_cons" +drop_cons = lemma (atProxy (Proxy @a) "drop_cons") (\(Forall n) (Forall x) (Forall xs) -> n .> 0 .=> drop n (x .: xs) .== drop (n - 1) xs) [] -- | @drop n (map f xs) == map f (drop n xs)@ -- -- >>> runTP $ drop_map @Integer @String (uninterpret "f") --- Lemma: drop_cons Q.E.D. --- Lemma: drop_cons Q.E.D. +-- Lemma: drop_cons @Integer Q.E.D. +-- Lemma: drop_cons @[Char] Q.E.D. -- Lemma: drop_map.n <= 0 Q.E.D. -- Inductive lemma: drop_map.n > 0 -- Step: Base Q.E.D. @@ -1545,7 +1571,13 @@ drop_map :: forall a b. (SymVal a, SymVal b) => (SBV a -> SBV b) -> TP (Proof (Forall "n" Integer -> Forall "xs" [a] -> SBool)) drop_map f = do dcA <- drop_cons @a - dcB <- drop_cons @b + + -- We need 'drop_cons' at the result type as well. We can't simply use @drop_cons \@b@ here: if @b@ is + -- itself a sequence (as it is in the doctest above, where it is 'String'), then z3 gives up on the + -- resulting nested-sequence goal with an incompleteness report. So, we prove this instance with cvc5. + dcB <- lemmaWith cvc5 (atProxy (Proxy @b) "drop_cons") + (\(Forall @"n" n) (Forall @"x" (x :: SBV b)) (Forall @"xs" xs) -> n .> 0 .=> drop n (x .: xs) .== drop (n - 1) xs) + [] h1 <- lemma "drop_map.n <= 0" (\(Forall @"xs" xs) (Forall @"n" n) -> n .<= 0 .=> drop n (map f xs) .== map f (drop n xs)) diff --git a/Documentation/SBV/Examples/TP/Primes.hs b/Documentation/SBV/Examples/TP/Primes.hs --- a/Documentation/SBV/Examples/TP/Primes.hs +++ b/Documentation/SBV/Examples/TP/Primes.hs @@ -317,6 +317,9 @@ -- === __Proof__ -- >>> runTP dividesFact -- Lemma: dividesProduct Q.E.D. +-- Lemma: factUnfold Q.E.D. +-- Lemma: dvdCong Q.E.D. +-- Lemma: dvdRefl Q.E.D. -- Inductive lemma: dividesFact -- Step: Base Q.E.D. -- Step: 1 Q.E.D. @@ -325,6 +328,7 @@ -- Step: 2.1.2 Q.E.D. -- Step: 2.2.1 Q.E.D. -- Step: 2.2.2 Q.E.D. +-- Step: 2.2.3 Q.E.D. -- Step: 2.Completeness Q.E.D. -- Result: Q.E.D. -- Functions proven terminating: fact @@ -333,21 +337,44 @@ dividesFact = do dvp <- recall dividesProduct - induct "dividesFact" - (\(Forall n) (Forall k) -> 1 .<= k .&& k .<= n .=> k `dvd` fact n) $ - \ih n k -> [1 .<= k, k .<= n + 1] - |- k `dvd` fact (n + 1) - =: k `dvd` ((n + 1) * fact n) - =: cases [ k .== n + 1 ==> k `dvd` ((n + 1) * fact n) - ?? dvp `at` (Inst @"x" k, Inst @"y" (n+1), Inst @"z" (fact n)) - =: sTrue - =: qed - , k ./= n + 1 ==> k `dvd` ((n + 1) * fact n) - ?? ih - ?? dvp `at` (Inst @"x" k, Inst @"y" (fact n), Inst @"z" (n+1)) - =: sTrue - =: qed - ] + -- Unfolding 'fact' underneath the mod that 'dvd' introduces is something no solver comes back + -- from. So, we split that step into two obligations, neither of which mentions both: 'factUnfold' + -- is the defining equation of 'fact' (no mod in sight), and 'dvdCong' is congruence of 'dvd' + -- over equal arguments (no recursion in sight). The step itself is then propositional. + -- + -- Note that we phrase 'factUnfold' at @n+1@, matching the shape it is used at below exactly. + fu <- lemmaWith cvc5 "factUnfold" + (\(Forall @"n" n) -> n .>= 0 .=> fact (n+1) .== (n+1) * fact n) + [] + + dc <- lemma "dvdCong" + (\(Forall @"k" k) (Forall @"x" x) (Forall @"y" y) -> x .== y .=> (k `dvd` x .== k `dvd` y)) + [] + + -- Every number divides itself. Isolated like this it is a one-liner for z3; buried inside the + -- case below (where 'fact' is also in scope) it is not. + dr <- lemma "dvdRefl" (\(Forall @"x" x) -> x `dvd` x) [] + + inductWith cvc5 "dividesFact" + (\(Forall n) (Forall k) -> 1 .<= k .&& k .<= n .=> k `dvd` fact n) $ + \ih n k -> [1 .<= k, k .<= n + 1] + |- k `dvd` fact (n + 1) + ?? fu `at` Inst @"n" n + ?? dc `at` (Inst @"k" k, Inst @"x" (fact (n+1)), Inst @"y" ((n + 1) * fact n)) + =: k `dvd` ((n + 1) * fact n) + =: cases [ k .== n + 1 ==> k `dvd` ((n + 1) * fact n) + ?? dr `at` Inst @"x" k + ?? dvp `at` (Inst @"x" k, Inst @"y" (n+1), Inst @"z" (fact n)) + =: sTrue + =: qed + , k ./= n + 1 ==> k `dvd` ((n + 1) * fact n) + ?? dc `at` (Inst @"k" k, Inst @"x" ((n + 1) * fact n), Inst @"y" (fact n * (n + 1))) + =: k `dvd` (fact n * (n + 1)) + ?? ih `at` Inst @"k" k + ?? dvp `at` (Inst @"x" k, Inst @"y" (fact n), Inst @"z" (n+1)) + =: sTrue + =: qed + ] -- | \(1 \leq k \land k \leq n \implies \neg (k \mid n! + 1)\) -- diff --git a/Documentation/SBV/Examples/TP/Tree.hs b/Documentation/SBV/Examples/TP/Tree.hs new file mode 100644 --- /dev/null +++ b/Documentation/SBV/Examples/TP/Tree.hs @@ -0,0 +1,283 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Documentation.SBV.Examples.TP.Tree +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer: erkokl@gmail.com +-- Stability : experimental +-- +-- Proofs about binary tree mirroring, in-order traversal (flattening), and +-- tree sizes. +----------------------------------------------------------------------------- + +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedLists #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeApplications #-} + +{-# OPTIONS_GHC -Wall -Werror #-} + +module Documentation.SBV.Examples.TP.Tree where + +import Prelude hiding (length, head, tail, null, reverse, (++)) + +import Data.SBV +import Data.SBV.List +import Data.SBV.TP + +import qualified Documentation.SBV.Examples.TP.Lists as TP + +import Data.Proxy (Proxy(..)) + +#ifdef DOCTEST +-- $setup +-- >>> :set -XTypeApplications +-- >>> import Data.SBV +-- >>> import Data.SBV.TP +#endif + +-- * Binary tree definition + +-- | A classic parametric binary tree data type. +data Tree a = Leaf + | Node (Tree a) a (Tree a) + deriving (Show, Eq) + +-- | Generate symbolic counterpart 'STree'. +mkSymbolic [''Tree] + +-- * Tree operations + +-- | Mirror a tree by recursively swapping its left and right subtrees. +-- +-- >>> mirror $ literal $ Node (Node Leaf (1::Integer) Leaf) 2 Leaf +-- Node Leaf 2 (Node Leaf 1 Leaf) :: Tree Integer +mirror :: SymVal a => STree a -> STree a +mirror = smtFunction "mirror" + $ \t -> [sCase| t of + Leaf -> sLeaf + Node l x r -> sNode (mirror r) x (mirror l) + |] + +-- | Flatten a tree into a list via in-order traversal. +-- +-- >>> flatten (sNode (sNode sLeaf (1 :: SInteger) sLeaf) 2 (sNode sLeaf 3 sLeaf)) +-- [1,2,3] :: [SInteger] +flatten :: SymVal a => STree a -> SList a +flatten = smtFunction "flatten" + $ \t -> [sCase| t of + Leaf -> [] + Node l x r -> flatten l ++ [x] ++ flatten r + |] + +-- | Calculate the number of internal nodes in a tree. +-- +-- >>> treeSize (sNode (sNode sLeaf (1 :: SInteger) sLeaf) 2 sLeaf) +-- 2 :: SInteger +treeSize :: SymVal a => STree a -> SInteger +treeSize = smtFunction "treeSize" + $ \t -> [sCase| t of + Leaf -> 0 + Node l _ r -> 1 + treeSize l + treeSize r + |] + +-- | The size is always non-negative. +-- +-- >>> runTP $ treeSizePos @Integer +-- Lemma: treeSizePos @Integer Q.E.D. +-- Functions proven terminating: treeSize +-- [Proven] treeSizePos @Integer :: Ɐt ∷ (Tree Integer) → Bool +treeSizePos :: forall a. SymVal a => TP (Proof (Forall "t" (Tree a) -> SBool)) +treeSizePos = inductiveLemma (atProxy (Proxy @a) "treeSizePos") (\(Forall t) -> treeSize t .>= 0) [] + +-- | Both subtrees of a node are strictly smaller than the node itself. This is the +-- lemma that lets us discharge the guard on the induction hypothesis in the strong +-- induction proofs below. +-- +-- @treeSize l < treeSize (Node l x r) && treeSize r < treeSize (Node l x r)@ +-- +-- >>> runTP $ treeSizeSmaller @Integer +-- Lemma: treeSizePos @Integer Q.E.D. +-- Lemma: treeSizeSmaller @Integer +-- Step: 1 Q.E.D. +-- Result: Q.E.D. +-- Functions proven terminating: treeSize +-- [Proven] treeSizeSmaller @Integer :: Ɐl ∷ (Tree Integer) → Ɐx ∷ Integer → Ɐr ∷ (Tree Integer) → Bool +treeSizeSmaller :: forall a. SymVal a => TP (Proof (Forall "l" (Tree a) -> Forall "x" a -> Forall "r" (Tree a) -> SBool)) +treeSizeSmaller = do + tsp <- recall $ treeSizePos @a + + calc (atProxy (Proxy @a) "treeSizeSmaller") + (\(Forall l) (Forall x) (Forall r) -> + let n = treeSize (sNode l x r) + in treeSize l .< n .&& treeSize r .< n) $ + \l x r -> let n = treeSize (sNode l x r) + in [] |- treeSize l .< n .&& treeSize r .< n + ?? tsp `at` Inst @"t" l + ?? tsp `at` Inst @"t" r + =: sTrue + =: qed + +-- * Correctness proofs + +-- | Proves that mirroring a tree twice yields the original tree: +-- +-- @mirror (mirror t) == t@ +-- +-- >>> runTP $ mirrorInvolution @Integer +-- Lemma: treeSizePos @Integer Q.E.D. +-- Lemma: treeSizeSmaller @Integer Q.E.D. +-- Inductive lemma (strong): mirrorInvolution @Integer +-- Step: Measure is non-negative Q.E.D. +-- Step: 1 (2 way case split) +-- Step: 1.1.1 Q.E.D. +-- Step: 1.1.2 Q.E.D. +-- Step: 1.2.1 Q.E.D. +-- Step: 1.2.2 Q.E.D. +-- Step: 1.2.3 Q.E.D. +-- Step: 1.2.4 Q.E.D. +-- Step: 1.Completeness Q.E.D. +-- Result: Q.E.D. +-- Functions proven terminating: mirror, treeSize +-- [Proven] mirrorInvolution @Integer :: Ɐt ∷ (Tree Integer) → Bool +mirrorInvolution :: forall a. SymVal a => TP (Proof (Forall "t" (Tree a) -> SBool)) +mirrorInvolution = do + tsp <- recall $ treeSizePos @a + tss <- recall $ treeSizeSmaller @a + + sInduct (atProxy (Proxy @a) "mirrorInvolution") + (\(Forall @"t" t) -> mirror (mirror t) .== t) + (treeSize, [proofOf tsp]) $ + \ih t -> [] |- [pCase| t of + Leaf -> mirror (mirror sLeaf) + =: mirror sLeaf + =: sLeaf + =: qed + Node l x r -> mirror (mirror (sNode l x r)) + =: mirror (sNode (mirror r) x (mirror l)) + =: sNode (mirror (mirror l)) x (mirror (mirror r)) + ?? tss `at` (Inst @"l" l, Inst @"x" x, Inst @"r" r) + ?? ih `at` Inst @"t" l + =: sNode l x (mirror (mirror r)) + ?? tss `at` (Inst @"l" l, Inst @"x" x, Inst @"r" r) + ?? ih `at` Inst @"t" r + =: sNode l x r + =: qed + |] + +-- | Proves that mirroring a tree preserves its size: +-- +-- @treeSize (mirror t) == treeSize t@ +-- +-- >>> runTP $ sizeMirror @Integer +-- Lemma: treeSizePos @Integer Q.E.D. +-- Lemma: treeSizeSmaller @Integer Q.E.D. +-- Inductive lemma (strong): sizeMirror @Integer +-- Step: Measure is non-negative Q.E.D. +-- Step: 1 (2 way case split) +-- Step: 1.1 Q.E.D. +-- Step: 1.2.1 Q.E.D. +-- Step: 1.2.2 Q.E.D. +-- Step: 1.2.3 Q.E.D. +-- Step: 1.2.4 Q.E.D. +-- Step: 1.2.5 Q.E.D. +-- Step: 1.Completeness Q.E.D. +-- Result: Q.E.D. +-- Functions proven terminating: mirror, treeSize +-- [Proven] sizeMirror @Integer :: Ɐt ∷ (Tree Integer) → Bool +sizeMirror :: forall a. SymVal a => TP (Proof (Forall "t" (Tree a) -> SBool)) +sizeMirror = do + tsp <- recall $ treeSizePos @a + tss <- recall $ treeSizeSmaller @a + + sInduct (atProxy (Proxy @a) "sizeMirror") + (\(Forall @"t" t) -> treeSize (mirror t) .== treeSize t) + (treeSize, [proofOf tsp]) $ + \ih t -> [] |- [pCase| t of + Leaf -> treeSize (mirror (sLeaf :: STree a)) + =: treeSize (sLeaf :: STree a) + =: qed + Node l x r -> treeSize (mirror (sNode l x r)) + =: treeSize (sNode (mirror r) x (mirror l)) + =: 1 + treeSize (mirror r) + treeSize (mirror l) + ?? tss `at` (Inst @"l" l, Inst @"x" x, Inst @"r" r) + ?? ih `at` Inst @"t" r + =: 1 + treeSize r + treeSize (mirror l) + ?? tss `at` (Inst @"l" l, Inst @"x" x, Inst @"r" r) + ?? ih `at` Inst @"t" l + =: 1 + treeSize r + treeSize l + =: treeSize (sNode l x r) + =: qed + |] + +-- | Proves that in-order traversal of a mirrored tree is equal to the reverse +-- of the in-order traversal of the original tree: +-- +-- @flatten (mirror t) == reverse (flatten t)@ +-- +-- >>> runTP $ flattenMirror @Integer +-- Lemma: treeSizePos @Integer Q.E.D. +-- Lemma: treeSizeSmaller @Integer Q.E.D. +-- Lemma: revApp Q.E.D. +-- Lemma: appendAssoc Q.E.D. +-- Inductive lemma (strong): flattenMirror @Integer +-- Step: Measure is non-negative Q.E.D. +-- Step: 1 (2 way case split) +-- Step: 1.1.1 Q.E.D. +-- Step: 1.1.2 Q.E.D. +-- Step: 1.1.3 Q.E.D. +-- Step: 1.1.4 Q.E.D. +-- Step: 1.2.1 Q.E.D. +-- Step: 1.2.2 Q.E.D. +-- Step: 1.2.3 Q.E.D. +-- Step: 1.2.4 Q.E.D. +-- Step: 1.2.5 Q.E.D. +-- Step: 1.2.6 Q.E.D. +-- Step: 1.2.7 Q.E.D. +-- Step: 1.2.8 Q.E.D. +-- Step: 1.Completeness Q.E.D. +-- Result: Q.E.D. +-- Functions proven terminating: flatten, mirror, sbv.reverse, treeSize +-- [Proven] flattenMirror @Integer :: Ɐt ∷ (Tree Integer) → Bool +flattenMirror :: forall a. SymVal a => TP (Proof (Forall "t" (Tree a) -> SBool)) +flattenMirror = do + tsp <- recall $ treeSizePos @a + tss <- recall $ treeSizeSmaller @a + + -- Quietly import a couple of list helpers from "Documentation.SBV.Examples.TP.Lists" + revApp <- recall $ TP.revApp @a + aAssoc <- recall $ TP.appendAssoc @a + + sInduct (atProxy (Proxy @a) "flattenMirror") + (\(Forall @"t" t) -> flatten (mirror t) .== reverse (flatten t)) + (treeSize, [proofOf tsp]) $ + \ih t -> [] |- [pCase| t of + Leaf -> flatten (mirror sLeaf) + =: flatten sLeaf + =: ([] :: SList a) + =: reverse [] + =: reverse (flatten sLeaf) + =: qed + Node l x r -> flatten (mirror (sNode l x r)) + =: flatten (sNode (mirror r) x (mirror l)) + =: flatten (mirror r) ++ [x] ++ flatten (mirror l) + ?? tss `at` (Inst @"l" l, Inst @"x" x, Inst @"r" r) + ?? ih `at` Inst @"t" r + =: reverse (flatten r) ++ [x] ++ flatten (mirror l) + ?? tss `at` (Inst @"l" l, Inst @"x" x, Inst @"r" r) + ?? ih `at` Inst @"t" l + =: reverse (flatten r) ++ [x] ++ reverse (flatten l) + ?? aAssoc `at` (Inst @"xs" (reverse (flatten r)), Inst @"ys" [x], Inst @"zs" (reverse (flatten l))) + =: (reverse (flatten r) ++ [x]) ++ reverse (flatten l) + ?? revApp `at` (Inst @"xs" [x], Inst @"ys" (flatten r)) + =: reverse ([x] ++ flatten r) ++ reverse (flatten l) + ?? revApp `at` (Inst @"xs" (flatten l), Inst @"ys" ([x] ++ flatten r)) + =: reverse (flatten l ++ [x] ++ flatten r) + =: reverse (flatten (sNode l x r)) + =: qed + |] diff --git a/Documentation/SBV/Examples/Uninterpreted/EUFLogic.hs b/Documentation/SBV/Examples/Uninterpreted/EUFLogic.hs --- a/Documentation/SBV/Examples/Uninterpreted/EUFLogic.hs +++ b/Documentation/SBV/Examples/Uninterpreted/EUFLogic.hs @@ -311,8 +311,8 @@ -- -- f :: Word32 -> Word32 -- f 0 = 4188219399 --- f 1445036292 = 285239361 -- f 3298461113 = 4054018119 +-- f 1445036292 = 285239361 -- f 996506182 = 4054018119 -- f _ = 0 -- diff --git a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs --- a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs +++ b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs @@ -49,8 +49,8 @@ -- >>> sat synthMul22 -- Satisfiable. Model: -- mul22_hi :: Bool -> Bool -> Bool -> Bool -> Bool --- mul22_hi False True True 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 False False True = True -- mul22_hi False True True False = True diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs --- a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs +++ b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs @@ -207,8 +207,8 @@ Following proof obligation failed: ================================== Invariant for loop "i < n" is not maintained by the body: - Before: SumS {n = 3, i = 1, s = 1} - After : SumS {n = 3, i = 2, s = 3} + Before: SumS {n = 2, i = 1, s = 1} + After : SumS {n = 2, i = 2, s = 3} Here, we posed the extra incorrect invariant that @s <= i@ must be maintained, and SBV found us a reachable state that violates the invariant. The /before/ state indeed satisfies @s <= i@, but the /after/ state does not. Note that the proof fails in this case not because the program @@ -224,8 +224,8 @@ Following proof obligation failed: ================================== Measure for loop "i < n" is negative: - State : SumS {n = 7, i = 6, s = 21} - Measure: -5 + State : SumS {n = 3, i = 2, s = 3} + Measure: -1 The failure is pretty obvious in this case: Measure produces a negative value. @@ -239,10 +239,10 @@ Following proof obligation failed: ================================== Measure for loop "i < n" does not decrease: - Before : SumS {n = 1, i = -1, s = 0} - Measure: 0 - After : SumS {n = 1, i = 0, s = 0} + Before : SumS {n = 1, i = 0, s = 0} Measure: 1 + After : SumS {n = 1, i = 1, s = 1} + Measure: 2 Clearly, as @i@ increases, so does our bogus measure @n+i@. (Note that in this case the counterexample might have @i@ and @n@ as negative values, as the SMT solver finds a counter-example to induction, not necessarily a reachable state. Obviously, all such failures need to be addressed for the full proof.) diff --git a/SBVTestSuite/GoldFiles/adt_gen00.gold b/SBVTestSuite/GoldFiles/adt_gen00.gold --- a/SBVTestSuite/GoldFiles/adt_gen00.gold +++ b/SBVTestSuite/GoldFiles/adt_gen00.gold @@ -267,11 +267,12 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (Let "l" - (Val 6) - (Let "a" (Val 0) (Add (Mul (Val 3) (Let "p" (Val 4) (Var "p"))) (Var "a")))))) +[RECV] ((s0 (Let "p" + (Add (Mul (Val 4) (Mul (Val (- 5)) (Val (- 3)))) + (Let "d" (Val (- 58)) (Var "d"))) + (Let "d" (Add (Val 8) (Val 1)) (Add (Var "d") (Val 3)))))) -Got: (let l = 6 in (let a = 0 in ((3 * (let p = 4 in p)) + a))) +Got: (let p = ((4 * (-5 * -3)) + (let d = -58 in d)) in (let d = (8 + 1) in (d + 3))) DONE *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/adt_pgen00.gold b/SBVTestSuite/GoldFiles/adt_pgen00.gold --- a/SBVTestSuite/GoldFiles/adt_pgen00.gold +++ b/SBVTestSuite/GoldFiles/adt_pgen00.gold @@ -267,11 +267,18 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (Let "t" - (Val 4) - (Let "l" (Val 7) (Add (Val (- 28281)) (Let "x" (Val 28293) (Var "x"))))))) +[RECV] ((s0 (Let "a" + (Let "t" (Val (- 3)) (Var "t")) + (Let "k" + (Mul (Val 7) (Var "a")) + (Add (Val 12) + (Mul (Mul (Val 4) (Val 3)) + (Mul (Var "k") + (Mul (Val 5) + (Add (Add (Val 6) (Var "k")) + (Let "l" (Var "k") (Val 15))))))))))) -Got: (let t = 4 in (let l = 7 in (-28281 + (let x = 28293 in x)))) +Got: (let a = (let t = -3 in t) in (let k = (7 * a) in (12 + ((4 * 3) * (k * (5 * ((6 + k) + (let l = k in 15)))))))) DONE *** Solver : Z3 *** Exit code: ExitSuccess diff --git a/SBVTestSuite/GoldFiles/array_misc_2.gold b/SBVTestSuite/GoldFiles/array_misc_2.gold --- a/SBVTestSuite/GoldFiles/array_misc_2.gold +++ b/SBVTestSuite/GoldFiles/array_misc_2.gold @@ -39,7 +39,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store (store ((as const (Array Int Int)) 4) 6 12) 3 5))) +[RECV] ((s0 (store (store ((as const (Array Int Int)) 5) 2 4) 6 12))) [SEND] (get-value (s1)) [RECV] ((s1 2)) [SEND] (get-value (s2)) @@ -51,7 +51,7 @@ FINAL OUTPUT: Satisfiable. Model: - s0 = ([(3,5),(6,12)], 4) :: Array Integer Integer + s0 = ([(6,12),(2,4)], 5) :: Array Integer Integer s1 = 2 :: Integer s2 = 3 :: Integer s3 = 6 :: Integer diff --git a/SBVTestSuite/GoldFiles/doctest_sanity.gold b/SBVTestSuite/GoldFiles/doctest_sanity.gold --- a/SBVTestSuite/GoldFiles/doctest_sanity.gold +++ b/SBVTestSuite/GoldFiles/doctest_sanity.gold @@ -1,3 +1,3 @@ -Total: 1238; Tried: 1238; Skipped: 0; Success: 1238; Errors: 0; Failures 0 -Examples: 1086; Tried: 1086; Skipped: 0; Success: 1086; Errors: 0; Failures 0 -Setup: 152; Tried: 152; Skipped: 0; Success: 152; Errors: 0; Failures 0 +Total: 1248; Tried: 1248; Skipped: 0; Success: 1248; Errors: 0; Failures 0 +Examples: 1093; Tried: 1093; Skipped: 0; Success: 1093; Errors: 0; Failures 0 +Setup: 155; Tried: 155; Skipped: 0; Success: 155; Errors: 0; Failures 0 diff --git a/SBVTestSuite/GoldFiles/exceptionLocal1.gold b/SBVTestSuite/GoldFiles/exceptionLocal1.gold --- a/SBVTestSuite/GoldFiles/exceptionLocal1.gold +++ b/SBVTestSuite/GoldFiles/exceptionLocal1.gold @@ -54,5 +54,5 @@ *** Sent : (define-fun s34 () (_ BitVec 32) (bvmul s33 s33)) *** *** Stderr : at line 40, column 35: in bvmul: maximal polynomial degree exceeded -*** Executable: /usr/local/bin/yices-smt2 +*** Executable: /Users/lerkok/Projects/Solvers/bin/yices-smt2 *** Options : --incremental diff --git a/SBVTestSuite/GoldFiles/exceptionLocal2.gold b/SBVTestSuite/GoldFiles/exceptionLocal2.gold --- a/SBVTestSuite/GoldFiles/exceptionLocal2.gold +++ b/SBVTestSuite/GoldFiles/exceptionLocal2.gold @@ -17,5 +17,5 @@ *** Sent : (declare-fun s0 () Real) ; tracks user variable "x" *** *** Stderr : line 8 column 23: logic does not support reals -*** Executable: /usr/local/bin/z3 +*** Executable: /Users/lerkok/Projects/Solvers/bin/z3 *** Options : -nw -in -smt2 diff --git a/SBVTestSuite/GoldFiles/lambda07.gold b/SBVTestSuite/GoldFiles/lambda07.gold --- a/SBVTestSuite/GoldFiles/lambda07.gold +++ b/SBVTestSuite/GoldFiles/lambda07.gold @@ -215,13 +215,13 @@ [SEND] (get-value (s16)) [RECV] ((s16 0)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 2)))) +[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 4)))) [SEND] (get-value (s11)) [RECV] ((s11 0)) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): abs arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = (0,[2]) :: (Integer, [Integer]) + arg = (0,[4]) :: (Integer, [Integer]) before = 0 :: Integer then = 0 :: Integer [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): trying next candidate.. diff --git a/SBVTestSuite/GoldFiles/lambda15.gold b/SBVTestSuite/GoldFiles/lambda15.gold --- a/SBVTestSuite/GoldFiles/lambda15.gold +++ b/SBVTestSuite/GoldFiles/lambda15.gold @@ -101,19 +101,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s14)) -[RECV] ((s14 0)) +[RECV] ((s14 8946)) [SEND] (get-value (s16)) -[RECV] ((s16 0)) +[RECV] ((s16 8946)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 0)))) +[RECV] ((s0 (mkSBVTuple2 8946 (seq.unit 0)))) [SEND] (get-value (s12)) [RECV] ((s12 0)) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.foldl @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): abs arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = (0,[0]) :: (Integer, [Integer]) - before = 0 :: Integer - then = 0 :: Integer + arg = (8946,[0]) :: (Integer, [Integer]) + before = 8946 :: Integer + then = 8946 :: Integer [MEASURE] sbv.foldl @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): trying next candidate.. [MEASURE] sbv.foldl @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): trying length arg1._2 [MEASURE] replayDAG {sbv.foldl @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer)}: replaying 11 node(s) diff --git a/SBVTestSuite/GoldFiles/lambda16.gold b/SBVTestSuite/GoldFiles/lambda16.gold --- a/SBVTestSuite/GoldFiles/lambda16.gold +++ b/SBVTestSuite/GoldFiles/lambda16.gold @@ -105,15 +105,15 @@ [SEND] (get-value (s16)) [RECV] ((s16 1)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 1 (seq.unit 1)))) +[RECV] ((s0 (mkSBVTuple2 1 (seq.unit (- 1))))) [SEND] (get-value (s12)) [RECV] ((s12 0)) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.foldl @(SBV (Integer,Integer) -> SBV Integer)_dd270bb7de @(SBV (Integer,[Integer]) -> SBV Integer): abs arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = (1,[1]) :: (Integer, [Integer]) - before = 1 :: Integer - then = 1 :: Integer + arg = (1,[-1]) :: (Integer, [Integer]) + before = 1 :: Integer + then = 1 :: Integer [MEASURE] sbv.foldl @(SBV (Integer,Integer) -> SBV Integer)_dd270bb7de @(SBV (Integer,[Integer]) -> SBV Integer): trying next candidate.. [MEASURE] sbv.foldl @(SBV (Integer,Integer) -> SBV Integer)_dd270bb7de @(SBV (Integer,[Integer]) -> SBV Integer): trying length arg1._2 [MEASURE] replayDAG {sbv.foldl @(SBV (Integer,Integer) -> SBV Integer)_dd270bb7de @(SBV (Integer,[Integer]) -> SBV Integer)}: replaying 11 node(s) diff --git a/SBVTestSuite/GoldFiles/lambda17.gold b/SBVTestSuite/GoldFiles/lambda17.gold --- a/SBVTestSuite/GoldFiles/lambda17.gold +++ b/SBVTestSuite/GoldFiles/lambda17.gold @@ -107,13 +107,13 @@ [SEND] (get-value (s17)) [RECV] ((s17 1)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 (as seq.empty (Seq Int)) (seq.unit 2)))) +[RECV] ((s0 (mkSBVTuple2 (as seq.empty (Seq Int)) (seq.unit 4)))) [SEND] (get-value (s13)) [RECV] ((s13 (as seq.empty (Seq Int)))) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.foldl @(SBV ([Integer],Integer) -> SBV [Integer])_2d6951daf1 @(SBV ([Integer],[Integer]) -> SBV [Integer]): length arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = ([],[2]) :: ([Integer], [Integer]) + arg = ([],[4]) :: ([Integer], [Integer]) before = 0 :: Integer then = 1 :: Integer [MEASURE] sbv.foldl @(SBV ([Integer],Integer) -> SBV [Integer])_2d6951daf1 @(SBV ([Integer],[Integer]) -> SBV [Integer]): trying next candidate.. diff --git a/SBVTestSuite/GoldFiles/lambda19.gold b/SBVTestSuite/GoldFiles/lambda19.gold --- a/SBVTestSuite/GoldFiles/lambda19.gold +++ b/SBVTestSuite/GoldFiles/lambda19.gold @@ -105,13 +105,13 @@ [SEND] (get-value (s16)) [RECV] ((s16 0)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 2)))) +[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 4)))) [SEND] (get-value (s11)) [RECV] ((s11 0)) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): abs arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = (0,[2]) :: (Integer, [Integer]) + arg = (0,[4]) :: (Integer, [Integer]) before = 0 :: Integer then = 0 :: Integer [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): trying next candidate.. diff --git a/SBVTestSuite/GoldFiles/lambda20.gold b/SBVTestSuite/GoldFiles/lambda20.gold --- a/SBVTestSuite/GoldFiles/lambda20.gold +++ b/SBVTestSuite/GoldFiles/lambda20.gold @@ -105,13 +105,13 @@ [SEND] (get-value (s16)) [RECV] ((s16 0)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 2)))) +[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 4)))) [SEND] (get-value (s11)) [RECV] ((s11 0)) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_dd270bb7de @(SBV (Integer,[Integer]) -> SBV Integer): abs arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = (0,[2]) :: (Integer, [Integer]) + arg = (0,[4]) :: (Integer, [Integer]) before = 0 :: Integer then = 0 :: Integer [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_dd270bb7de @(SBV (Integer,[Integer]) -> SBV Integer): trying next candidate.. diff --git a/SBVTestSuite/GoldFiles/lambda21.gold b/SBVTestSuite/GoldFiles/lambda21.gold --- a/SBVTestSuite/GoldFiles/lambda21.gold +++ b/SBVTestSuite/GoldFiles/lambda21.gold @@ -107,13 +107,13 @@ [SEND] (get-value (s17)) [RECV] ((s17 0)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 (as seq.empty (Seq Int)) (seq.unit 2)))) +[RECV] ((s0 (mkSBVTuple2 (as seq.empty (Seq Int)) (seq.unit 4)))) [SEND] (get-value (s10)) [RECV] ((s10 (as seq.empty (Seq Int)))) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.foldr @(SBV (Integer,[Integer]) -> SBV [Integer])_5c3e05abf3 @(SBV ([Integer],[Integer]) -> SBV [Integer]): length arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = ([],[2]) :: ([Integer], [Integer]) + arg = ([],[4]) :: ([Integer], [Integer]) before = 0 :: Integer then = 0 :: Integer [MEASURE] sbv.foldr @(SBV (Integer,[Integer]) -> SBV [Integer])_5c3e05abf3 @(SBV ([Integer],[Integer]) -> SBV [Integer]): trying next candidate.. diff --git a/SBVTestSuite/GoldFiles/lambda23.gold b/SBVTestSuite/GoldFiles/lambda23.gold --- a/SBVTestSuite/GoldFiles/lambda23.gold +++ b/SBVTestSuite/GoldFiles/lambda23.gold @@ -329,13 +329,13 @@ [SEND] (get-value (s16)) [RECV] ((s16 0)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 2)))) +[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 4)))) [SEND] (get-value (s11)) [RECV] ((s11 0)) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): abs arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = (0,[2]) :: (Integer, [Integer]) + arg = (0,[4]) :: (Integer, [Integer]) before = 0 :: Integer then = 0 :: Integer [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): trying next candidate.. diff --git a/SBVTestSuite/GoldFiles/lambda25.gold b/SBVTestSuite/GoldFiles/lambda25.gold --- a/SBVTestSuite/GoldFiles/lambda25.gold +++ b/SBVTestSuite/GoldFiles/lambda25.gold @@ -228,13 +228,13 @@ [SEND] (get-value (s16)) [RECV] ((s16 0)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 2)))) +[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 4)))) [SEND] (get-value (s11)) [RECV] ((s11 0)) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): abs arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = (0,[2]) :: (Integer, [Integer]) + arg = (0,[4]) :: (Integer, [Integer]) before = 0 :: Integer then = 0 :: Integer [MEASURE] sbv.foldr @(SBV (Integer,Integer) -> SBV Integer)_1fd06f7602 @(SBV (Integer,[Integer]) -> SBV Integer): trying next candidate.. diff --git a/SBVTestSuite/GoldFiles/lambda26.gold b/SBVTestSuite/GoldFiles/lambda26.gold --- a/SBVTestSuite/GoldFiles/lambda26.gold +++ b/SBVTestSuite/GoldFiles/lambda26.gold @@ -1,3 +1,219 @@ +[MEASURE] Verifying termination measures for: sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]) +[MEASURE] Checking: sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]) +[MEASURE] sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]): barified = "|sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])|" +[MEASURE] sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]): Uninterpreted ops in DAG: [("|sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])|",1)] +[MEASURE] sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]): recursive calls found = 1 +[MEASURE] sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]): trying length arg1._1 +[MEASURE] replayDAG {sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])}: replaying 11 node(s) +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-option :model.inline_def true ) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- tuples --- +[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) + ((mkSBVTuple2 (proj_1_SBVTuple2 T1) + (proj_2_SBVTuple2 T2)))))) +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s1 () Int 0) +[GOOD] (define-fun s2 () Int 1) +[GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () (SBVTuple2 (Seq Int) (Seq (Seq Int)))) ; tracks user variable "arg" +[GOOD] (declare-fun s11 () (Seq Int)) ; tracks user variable "__internal_sbv_s11" +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] (define-fun s3 () (Seq (Seq Int)) (proj_2_SBVTuple2 s0)) +[GOOD] (define-fun s4 () Int (seq.len s3)) +[GOOD] (define-fun s5 () Bool (= s1 s4)) +[GOOD] (define-fun s6 () (Seq Int) (proj_1_SBVTuple2 s0)) +[GOOD] (define-fun s7 () (Seq Int) (seq.nth s3 s1)) +[GOOD] (define-fun s8 () Int (- s4 s2)) +[GOOD] (define-fun s9 () (Seq (Seq Int)) (seq.extract s3 s2 s8)) +[GOOD] (define-fun s10 () (SBVTuple2 (Seq Int) (Seq (Seq Int))) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) s6 s9)) +[GOOD] (define-fun s12 () (Seq Int) (seq.++ s7 s11)) +[GOOD] (define-fun s13 () (Seq Int) (ite s5 s6 s12)) +[GOOD] (define-fun s14 () Int (seq.len s6)) +[GOOD] (define-fun s15 () Bool (>= s14 s1)) +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert (not s15)) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess +[MEASURE] replayDAG {sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])}: replaying 11 node(s) +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-option :model.inline_def true ) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- tuples --- +[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) + ((mkSBVTuple2 (proj_1_SBVTuple2 T1) + (proj_2_SBVTuple2 T2)))))) +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s1 () Int 0) +[GOOD] (define-fun s2 () Int 1) +[GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () (SBVTuple2 (Seq Int) (Seq (Seq Int)))) ; tracks user variable "arg" +[GOOD] (declare-fun s11 () (Seq Int)) ; tracks user variable "__internal_sbv_s11" +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] (define-fun s3 () (Seq (Seq Int)) (proj_2_SBVTuple2 s0)) +[GOOD] (define-fun s4 () Int (seq.len s3)) +[GOOD] (define-fun s5 () Bool (= s1 s4)) +[GOOD] (define-fun s6 () (Seq Int) (proj_1_SBVTuple2 s0)) +[GOOD] (define-fun s7 () (Seq Int) (seq.nth s3 s1)) +[GOOD] (define-fun s8 () Int (- s4 s2)) +[GOOD] (define-fun s9 () (Seq (Seq Int)) (seq.extract s3 s2 s8)) +[GOOD] (define-fun s10 () (SBVTuple2 (Seq Int) (Seq (Seq Int))) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) s6 s9)) +[GOOD] (define-fun s12 () (Seq Int) (seq.++ s7 s11)) +[GOOD] (define-fun s13 () (Seq Int) (ite s5 s6 s12)) +[GOOD] (define-fun s14 () Int (seq.len s6)) +[GOOD] (define-fun s15 () (Seq Int) (proj_1_SBVTuple2 s10)) +[GOOD] (define-fun s16 () Int (seq.len s15)) +[GOOD] (define-fun s17 () Bool (not s5)) +[GOOD] (define-fun s18 () Bool (> s14 s16)) +[GOOD] (define-fun s19 () Bool (=> s17 s18)) +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert (not s19)) +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s14)) +[RECV] ((s14 0)) +[SEND] (get-value (s16)) +[RECV] ((s16 0)) +[SEND] (get-value (s0)) +[RECV] ((s0 (mkSBVTuple2 (as seq.empty (Seq Int)) (seq.unit (seq.unit 2))))) +[SEND] (get-value (s11)) +[RECV] ((s11 (as seq.empty (Seq Int)))) +*** Solver : Z3 +*** Exit code: ExitSuccess +[MEASURE] sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]): length arg1._1 failed strict decrease: Falsifiable. Counter-example: + arg = ([],[[2]]) :: ([Integer], [[Integer]]) + before = 0 :: Integer + then = 0 :: Integer +[MEASURE] sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]): trying next candidate.. +[MEASURE] sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]): trying length arg1._2 +[MEASURE] replayDAG {sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])}: replaying 11 node(s) +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-option :model.inline_def true ) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- tuples --- +[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) + ((mkSBVTuple2 (proj_1_SBVTuple2 T1) + (proj_2_SBVTuple2 T2)))))) +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s1 () Int 0) +[GOOD] (define-fun s2 () Int 1) +[GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () (SBVTuple2 (Seq Int) (Seq (Seq Int)))) ; tracks user variable "arg" +[GOOD] (declare-fun s11 () (Seq Int)) ; tracks user variable "__internal_sbv_s11" +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] (define-fun s3 () (Seq (Seq Int)) (proj_2_SBVTuple2 s0)) +[GOOD] (define-fun s4 () Int (seq.len s3)) +[GOOD] (define-fun s5 () Bool (= s1 s4)) +[GOOD] (define-fun s6 () (Seq Int) (proj_1_SBVTuple2 s0)) +[GOOD] (define-fun s7 () (Seq Int) (seq.nth s3 s1)) +[GOOD] (define-fun s8 () Int (- s4 s2)) +[GOOD] (define-fun s9 () (Seq (Seq Int)) (seq.extract s3 s2 s8)) +[GOOD] (define-fun s10 () (SBVTuple2 (Seq Int) (Seq (Seq Int))) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) s6 s9)) +[GOOD] (define-fun s12 () (Seq Int) (seq.++ s7 s11)) +[GOOD] (define-fun s13 () (Seq Int) (ite s5 s6 s12)) +[GOOD] (define-fun s14 () Bool (>= s4 s1)) +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert (not s14)) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess +[MEASURE] replayDAG {sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer])}: replaying 11 node(s) +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-option :model.inline_def true ) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- tuples --- +[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) + ((mkSBVTuple2 (proj_1_SBVTuple2 T1) + (proj_2_SBVTuple2 T2)))))) +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s1 () Int 0) +[GOOD] (define-fun s2 () Int 1) +[GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () (SBVTuple2 (Seq Int) (Seq (Seq Int)))) ; tracks user variable "arg" +[GOOD] (declare-fun s11 () (Seq Int)) ; tracks user variable "__internal_sbv_s11" +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] (define-fun s3 () (Seq (Seq Int)) (proj_2_SBVTuple2 s0)) +[GOOD] (define-fun s4 () Int (seq.len s3)) +[GOOD] (define-fun s5 () Bool (= s1 s4)) +[GOOD] (define-fun s6 () (Seq Int) (proj_1_SBVTuple2 s0)) +[GOOD] (define-fun s7 () (Seq Int) (seq.nth s3 s1)) +[GOOD] (define-fun s8 () Int (- s4 s2)) +[GOOD] (define-fun s9 () (Seq (Seq Int)) (seq.extract s3 s2 s8)) +[GOOD] (define-fun s10 () (SBVTuple2 (Seq Int) (Seq (Seq Int))) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) s6 s9)) +[GOOD] (define-fun s12 () (Seq Int) (seq.++ s7 s11)) +[GOOD] (define-fun s13 () (Seq Int) (ite s5 s6 s12)) +[GOOD] (define-fun s14 () (Seq (Seq Int)) (proj_2_SBVTuple2 s10)) +[GOOD] (define-fun s15 () Int (seq.len s14)) +[GOOD] (define-fun s16 () Bool (not s5)) +[GOOD] (define-fun s17 () Bool (> s4 s15)) +[GOOD] (define-fun s18 () Bool (=> s16 s17)) +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert (not s18)) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess +[MEASURE] sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]): length arg1._2 -> OK +[MEASURE] Passed (terminating): sbv.foldr @(SBV ([Integer],[Integer]) -> SBV [Integer])_44d71053fc @(SBV ([Integer],[[Integer]]) -> SBV [Integer]) ** Calling: z3 -nw -in -smt2 [GOOD] ; Automatically generated by SBV. Do not edit. [GOOD] (set-option :print-success true) diff --git a/SBVTestSuite/GoldFiles/lambda69.gold b/SBVTestSuite/GoldFiles/lambda69.gold --- a/SBVTestSuite/GoldFiles/lambda69.gold +++ b/SBVTestSuite/GoldFiles/lambda69.gold @@ -34,11 +34,11 @@ [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) [SEND] (get-value (F)) -[RECV] ((F (lambda ((x!1 Int) (x!2 Int)) (+ 3 (* 2 x!1) (* (- 1) x!2))))) +[RECV] ((F (lambda ((x!1 Int) (x!2 Int)) (+ 3 (* (- 1) x!2) (* 2 x!1))))) *** Solver : Z3 *** Exit code: ExitSuccess RESULT: Satisfiable. Model: F :: Integer -> Integer -> Integer - F x y = 3 + 2 * x + (-y) + F x y = 3 + (-y) + 2 * x diff --git a/SBVTestSuite/GoldFiles/lambda87.gold b/SBVTestSuite/GoldFiles/lambda87.gold --- a/SBVTestSuite/GoldFiles/lambda87.gold +++ b/SBVTestSuite/GoldFiles/lambda87.gold @@ -223,13 +223,13 @@ [SEND] (get-value (s19)) [RECV] ((s19 0)) [SEND] (get-value (s0)) -[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 2)))) +[RECV] ((s0 (mkSBVTuple2 0 (seq.unit 4)))) [SEND] (get-value (s14)) [RECV] ((s14 (as seq.empty (Seq Int)))) *** Solver : Z3 *** Exit code: ExitSuccess [MEASURE] sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_d8dc9e6fbd @(SBV (Integer,[Integer]) -> SBV [Integer]): abs arg1._1 failed strict decrease: Falsifiable. Counter-example: - arg = (0,[2]) :: (Integer, [Integer]) + arg = (0,[4]) :: (Integer, [Integer]) before = 0 :: Integer then = 0 :: Integer [MEASURE] sbv.closureMap @(SBV Integer -> SBV Integer -> SBV Integer)_d8dc9e6fbd @(SBV (Integer,[Integer]) -> SBV [Integer]): trying next candidate.. diff --git a/SBVTestSuite/GoldFiles/lambda88.gold b/SBVTestSuite/GoldFiles/lambda88.gold --- a/SBVTestSuite/GoldFiles/lambda88.gold +++ b/SBVTestSuite/GoldFiles/lambda88.gold @@ -1,3 +1,231 @@ +[MEASURE] Verifying termination measures for: sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]) +[MEASURE] Checking: sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]) +[MEASURE] sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]): barified = "|sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]])|" +[MEASURE] sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]): Uninterpreted ops in DAG: [("|sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]])|",1)] +[MEASURE] sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]): recursive calls found = 1 +[MEASURE] sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]): trying length arg1._1 +[MEASURE] replayDAG {sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]])}: replaying 13 node(s) +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-option :model.inline_def true ) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- tuples --- +[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) + ((mkSBVTuple2 (proj_1_SBVTuple2 T1) + (proj_2_SBVTuple2 T2)))))) +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s1 () Int 0) +[GOOD] (define-fun s2 () Int 1) +[GOOD] (define-fun s3 () (Seq (Seq Int)) (as seq.empty (Seq (Seq Int)))) +[GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () (SBVTuple2 (Seq Int) (Seq (Seq Int)))) ; tracks user variable "arg" +[GOOD] (declare-fun s14 () (Seq (Seq Int))) ; tracks user variable "__internal_sbv_s14" +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] (define-fun s4 () (Seq (Seq Int)) (proj_2_SBVTuple2 s0)) +[GOOD] (define-fun s5 () Int (seq.len s4)) +[GOOD] (define-fun s6 () Bool (= s1 s5)) +[GOOD] (define-fun s7 () (Seq Int) (seq.nth s4 s1)) +[GOOD] (define-fun s8 () (Seq Int) (proj_1_SBVTuple2 s0)) +[GOOD] (define-fun s9 () (Seq Int) (seq.++ s7 s8)) +[GOOD] (define-fun s10 () (Seq (Seq Int)) (seq.unit s9)) +[GOOD] (define-fun s11 () Int (- s5 s2)) +[GOOD] (define-fun s12 () (Seq (Seq Int)) (seq.extract s4 s2 s11)) +[GOOD] (define-fun s13 () (SBVTuple2 (Seq Int) (Seq (Seq Int))) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) s8 s12)) +[GOOD] (define-fun s15 () (Seq (Seq Int)) (seq.++ s10 s14)) +[GOOD] (define-fun s16 () (Seq (Seq Int)) (ite s6 s3 s15)) +[GOOD] (define-fun s17 () Int (seq.len s8)) +[GOOD] (define-fun s18 () Bool (>= s17 s1)) +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert (not s18)) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess +[MEASURE] replayDAG {sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]])}: replaying 13 node(s) +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-option :model.inline_def true ) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- tuples --- +[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) + ((mkSBVTuple2 (proj_1_SBVTuple2 T1) + (proj_2_SBVTuple2 T2)))))) +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s1 () Int 0) +[GOOD] (define-fun s2 () Int 1) +[GOOD] (define-fun s3 () (Seq (Seq Int)) (as seq.empty (Seq (Seq Int)))) +[GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () (SBVTuple2 (Seq Int) (Seq (Seq Int)))) ; tracks user variable "arg" +[GOOD] (declare-fun s14 () (Seq (Seq Int))) ; tracks user variable "__internal_sbv_s14" +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] (define-fun s4 () (Seq (Seq Int)) (proj_2_SBVTuple2 s0)) +[GOOD] (define-fun s5 () Int (seq.len s4)) +[GOOD] (define-fun s6 () Bool (= s1 s5)) +[GOOD] (define-fun s7 () (Seq Int) (seq.nth s4 s1)) +[GOOD] (define-fun s8 () (Seq Int) (proj_1_SBVTuple2 s0)) +[GOOD] (define-fun s9 () (Seq Int) (seq.++ s7 s8)) +[GOOD] (define-fun s10 () (Seq (Seq Int)) (seq.unit s9)) +[GOOD] (define-fun s11 () Int (- s5 s2)) +[GOOD] (define-fun s12 () (Seq (Seq Int)) (seq.extract s4 s2 s11)) +[GOOD] (define-fun s13 () (SBVTuple2 (Seq Int) (Seq (Seq Int))) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) s8 s12)) +[GOOD] (define-fun s15 () (Seq (Seq Int)) (seq.++ s10 s14)) +[GOOD] (define-fun s16 () (Seq (Seq Int)) (ite s6 s3 s15)) +[GOOD] (define-fun s17 () Int (seq.len s8)) +[GOOD] (define-fun s18 () (Seq Int) (proj_1_SBVTuple2 s13)) +[GOOD] (define-fun s19 () Int (seq.len s18)) +[GOOD] (define-fun s20 () Bool (not s6)) +[GOOD] (define-fun s21 () Bool (> s17 s19)) +[GOOD] (define-fun s22 () Bool (=> s20 s21)) +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert (not s22)) +[SEND] (check-sat) +[RECV] sat +[SEND] (get-value (s17)) +[RECV] ((s17 0)) +[SEND] (get-value (s19)) +[RECV] ((s19 0)) +[SEND] (get-value (s0)) +[RECV] ((s0 (mkSBVTuple2 (as seq.empty (Seq Int)) (seq.unit (seq.unit 2))))) +[SEND] (get-value (s14)) +[RECV] ((s14 (as seq.empty (Seq (Seq Int))))) +*** Solver : Z3 +*** Exit code: ExitSuccess +[MEASURE] sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]): length arg1._1 failed strict decrease: Falsifiable. Counter-example: + arg = ([],[[2]]) :: ([Integer], [[Integer]]) + before = 0 :: Integer + then = 0 :: Integer +[MEASURE] sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]): trying next candidate.. +[MEASURE] sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]): trying length arg1._2 +[MEASURE] replayDAG {sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]])}: replaying 13 node(s) +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-option :model.inline_def true ) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- tuples --- +[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) + ((mkSBVTuple2 (proj_1_SBVTuple2 T1) + (proj_2_SBVTuple2 T2)))))) +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s1 () Int 0) +[GOOD] (define-fun s2 () Int 1) +[GOOD] (define-fun s3 () (Seq (Seq Int)) (as seq.empty (Seq (Seq Int)))) +[GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () (SBVTuple2 (Seq Int) (Seq (Seq Int)))) ; tracks user variable "arg" +[GOOD] (declare-fun s14 () (Seq (Seq Int))) ; tracks user variable "__internal_sbv_s14" +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] (define-fun s4 () (Seq (Seq Int)) (proj_2_SBVTuple2 s0)) +[GOOD] (define-fun s5 () Int (seq.len s4)) +[GOOD] (define-fun s6 () Bool (= s1 s5)) +[GOOD] (define-fun s7 () (Seq Int) (seq.nth s4 s1)) +[GOOD] (define-fun s8 () (Seq Int) (proj_1_SBVTuple2 s0)) +[GOOD] (define-fun s9 () (Seq Int) (seq.++ s7 s8)) +[GOOD] (define-fun s10 () (Seq (Seq Int)) (seq.unit s9)) +[GOOD] (define-fun s11 () Int (- s5 s2)) +[GOOD] (define-fun s12 () (Seq (Seq Int)) (seq.extract s4 s2 s11)) +[GOOD] (define-fun s13 () (SBVTuple2 (Seq Int) (Seq (Seq Int))) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) s8 s12)) +[GOOD] (define-fun s15 () (Seq (Seq Int)) (seq.++ s10 s14)) +[GOOD] (define-fun s16 () (Seq (Seq Int)) (ite s6 s3 s15)) +[GOOD] (define-fun s17 () Bool (>= s5 s1)) +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert (not s17)) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess +[MEASURE] replayDAG {sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]])}: replaying 13 node(s) +** Calling: z3 -nw -in -smt2 +[GOOD] ; Automatically generated by SBV. Do not edit. +[GOOD] (set-option :print-success true) +[GOOD] (set-option :global-declarations true) +[GOOD] (set-option :smtlib2_compliant true) +[GOOD] (set-option :diagnostic-output-channel "stdout") +[GOOD] (set-option :produce-models true) +[GOOD] (set-option :pp.max_depth 4294967295) +[GOOD] (set-option :pp.min_alias_size 4294967295) +[GOOD] (set-option :model.inline_def true ) +[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] ; --- tuples --- +[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2) + ((mkSBVTuple2 (proj_1_SBVTuple2 T1) + (proj_2_SBVTuple2 T2)))))) +[GOOD] ; --- sums --- +[GOOD] ; --- literal constants --- +[GOOD] (define-fun s1 () Int 0) +[GOOD] (define-fun s2 () Int 1) +[GOOD] (define-fun s3 () (Seq (Seq Int)) (as seq.empty (Seq (Seq Int)))) +[GOOD] ; --- top level inputs --- +[GOOD] (declare-fun s0 () (SBVTuple2 (Seq Int) (Seq (Seq Int)))) ; tracks user variable "arg" +[GOOD] (declare-fun s14 () (Seq (Seq Int))) ; tracks user variable "__internal_sbv_s14" +[GOOD] ; --- constant tables --- +[GOOD] ; --- non-constant tables --- +[GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- user defined functions --- +[GOOD] ; --- assignments --- +[GOOD] (define-fun s4 () (Seq (Seq Int)) (proj_2_SBVTuple2 s0)) +[GOOD] (define-fun s5 () Int (seq.len s4)) +[GOOD] (define-fun s6 () Bool (= s1 s5)) +[GOOD] (define-fun s7 () (Seq Int) (seq.nth s4 s1)) +[GOOD] (define-fun s8 () (Seq Int) (proj_1_SBVTuple2 s0)) +[GOOD] (define-fun s9 () (Seq Int) (seq.++ s7 s8)) +[GOOD] (define-fun s10 () (Seq (Seq Int)) (seq.unit s9)) +[GOOD] (define-fun s11 () Int (- s5 s2)) +[GOOD] (define-fun s12 () (Seq (Seq Int)) (seq.extract s4 s2 s11)) +[GOOD] (define-fun s13 () (SBVTuple2 (Seq Int) (Seq (Seq Int))) ((as mkSBVTuple2 (SBVTuple2 (Seq Int) (Seq (Seq Int)))) s8 s12)) +[GOOD] (define-fun s15 () (Seq (Seq Int)) (seq.++ s10 s14)) +[GOOD] (define-fun s16 () (Seq (Seq Int)) (ite s6 s3 s15)) +[GOOD] (define-fun s17 () (Seq (Seq Int)) (proj_2_SBVTuple2 s13)) +[GOOD] (define-fun s18 () Int (seq.len s17)) +[GOOD] (define-fun s19 () Bool (not s6)) +[GOOD] (define-fun s20 () Bool (> s5 s18)) +[GOOD] (define-fun s21 () Bool (=> s19 s20)) +[GOOD] ; --- delayedEqualities --- +[GOOD] ; --- formula --- +[GOOD] (assert (not s21)) +[SEND] (check-sat) +[RECV] unsat +*** Solver : Z3 +*** Exit code: ExitSuccess +[MEASURE] sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]): length arg1._2 -> OK +[MEASURE] Passed (terminating): sbv.closureMap @(SBV [Integer] -> SBV [Integer] -> SBV [Integer])_24b5487d7f @(SBV ([Integer],[[Integer]]) -> SBV [[Integer]]) ** Calling: z3 -nw -in -smt2 [GOOD] ; Automatically generated by SBV. Do not edit. [GOOD] (set-option :print-success true) diff --git a/SBVTestSuite/GoldFiles/pareto1.gold b/SBVTestSuite/GoldFiles/pareto1.gold --- a/SBVTestSuite/GoldFiles/pareto1.gold +++ b/SBVTestSuite/GoldFiles/pareto1.gold @@ -5,89 +5,89 @@ max_x_plus_y = 2 :: Integer min_y = 1 :: Integer Pareto front #2: Optimal model: - x = 2 :: Integer - y = 2 :: Integer - min_x = 2 :: Integer - max_x_plus_y = 4 :: Integer - min_y = 2 :: Integer -Pareto front #3: Optimal model: - x = 3 :: Integer + x = 0 :: Integer y = 3 :: Integer - min_x = 3 :: Integer - max_x_plus_y = 6 :: Integer + min_x = 0 :: Integer + max_x_plus_y = 3 :: Integer min_y = 3 :: Integer +Pareto front #3: Optimal model: + x = 0 :: Integer + y = 4 :: Integer + min_x = 0 :: Integer + max_x_plus_y = 4 :: Integer + min_y = 4 :: Integer Pareto front #4: Optimal model: - x = 4 :: Integer - y = 1 :: Integer - min_x = 4 :: Integer - max_x_plus_y = 5 :: Integer - min_y = 1 :: Integer -Pareto front #5: Optimal model: x = 3 :: Integer y = 2 :: Integer min_x = 3 :: Integer max_x_plus_y = 5 :: Integer min_y = 2 :: Integer +Pareto front #5: Optimal model: + x = 2 :: Integer + y = 1 :: Integer + min_x = 2 :: Integer + max_x_plus_y = 3 :: Integer + min_y = 1 :: Integer Pareto front #6: Optimal model: - x = 5 :: Integer + x = 3 :: Integer y = 1 :: Integer - min_x = 5 :: Integer - max_x_plus_y = 6 :: Integer + min_x = 3 :: Integer + max_x_plus_y = 4 :: Integer min_y = 1 :: Integer Pareto front #7: Optimal model: - x = 5 :: Integer + x = 4 :: Integer y = 0 :: Integer - min_x = 5 :: Integer - max_x_plus_y = 5 :: Integer + min_x = 4 :: Integer + max_x_plus_y = 4 :: Integer min_y = 0 :: Integer Pareto front #8: Optimal model: x = 2 :: Integer - y = 4 :: Integer + y = 2 :: Integer min_x = 2 :: Integer - max_x_plus_y = 6 :: Integer - min_y = 4 :: Integer + max_x_plus_y = 4 :: Integer + min_y = 2 :: Integer Pareto front #9: Optimal model: - x = 4 :: Integer + x = 1 :: Integer y = 3 :: Integer - min_x = 4 :: Integer - max_x_plus_y = 7 :: Integer + min_x = 1 :: Integer + max_x_plus_y = 4 :: Integer min_y = 3 :: Integer Pareto front #10: Optimal model: - x = 5 :: Integer - y = 2 :: Integer - min_x = 5 :: Integer - max_x_plus_y = 7 :: Integer - min_y = 2 :: Integer + x = 0 :: Integer + y = 0 :: Integer + min_x = 0 :: Integer + max_x_plus_y = 0 :: Integer + min_y = 0 :: Integer Pareto front #11: Optimal model: - x = 5 :: Integer - y = 3 :: Integer - min_x = 5 :: Integer - max_x_plus_y = 8 :: Integer - min_y = 3 :: Integer + x = 0 :: Integer + y = 1 :: Integer + min_x = 0 :: Integer + max_x_plus_y = 1 :: Integer + min_y = 1 :: Integer Pareto front #12: Optimal model: - x = 3 :: Integer - y = 4 :: Integer - min_x = 3 :: Integer - max_x_plus_y = 7 :: Integer - min_y = 4 :: Integer + x = 2 :: Integer + y = 0 :: Integer + min_x = 2 :: Integer + max_x_plus_y = 2 :: Integer + min_y = 0 :: Integer Pareto front #13: Optimal model: - x = 4 :: Integer + x = 0 :: Integer y = 2 :: Integer - min_x = 4 :: Integer - max_x_plus_y = 6 :: Integer + min_x = 0 :: Integer + max_x_plus_y = 2 :: Integer min_y = 2 :: Integer Pareto front #14: Optimal model: - x = 4 :: Integer - y = 4 :: Integer - min_x = 4 :: Integer - max_x_plus_y = 8 :: Integer - min_y = 4 :: Integer + x = 3 :: Integer + y = 0 :: Integer + min_x = 3 :: Integer + max_x_plus_y = 3 :: Integer + min_y = 0 :: Integer Pareto front #15: Optimal model: - x = 5 :: Integer - y = 4 :: Integer - min_x = 5 :: Integer - max_x_plus_y = 9 :: Integer - min_y = 4 :: Integer + x = 1 :: Integer + y = 2 :: Integer + min_x = 1 :: Integer + max_x_plus_y = 3 :: Integer + min_y = 2 :: Integer Pareto front #16: Optimal model: x = 1 :: Integer y = 0 :: Integer @@ -95,86 +95,86 @@ max_x_plus_y = 1 :: Integer min_y = 0 :: Integer Pareto front #17: Optimal model: - x = 0 :: Integer + x = 5 :: Integer y = 0 :: Integer - min_x = 0 :: Integer - max_x_plus_y = 0 :: Integer + min_x = 5 :: Integer + max_x_plus_y = 5 :: Integer min_y = 0 :: Integer Pareto front #18: Optimal model: - x = 2 :: Integer - y = 0 :: Integer - min_x = 2 :: Integer - max_x_plus_y = 2 :: Integer - min_y = 0 :: Integer -Pareto front #19: Optimal model: - x = 0 :: Integer + x = 4 :: Integer y = 1 :: Integer - min_x = 0 :: Integer - max_x_plus_y = 1 :: Integer + min_x = 4 :: Integer + max_x_plus_y = 5 :: Integer min_y = 1 :: Integer -Pareto front #20: Optimal model: - x = 2 :: Integer +Pareto front #19: Optimal model: + x = 5 :: Integer y = 1 :: Integer - min_x = 2 :: Integer - max_x_plus_y = 3 :: Integer + min_x = 5 :: Integer + max_x_plus_y = 6 :: Integer min_y = 1 :: Integer -Pareto front #21: Optimal model: +Pareto front #20: Optimal model: x = 1 :: Integer - y = 2 :: Integer + y = 4 :: Integer min_x = 1 :: Integer - max_x_plus_y = 3 :: Integer + max_x_plus_y = 5 :: Integer + min_y = 4 :: Integer +Pareto front #21: Optimal model: + x = 4 :: Integer + y = 2 :: Integer + min_x = 4 :: Integer + max_x_plus_y = 6 :: Integer min_y = 2 :: Integer Pareto front #22: Optimal model: - x = 0 :: Integer + x = 4 :: Integer + y = 3 :: Integer + min_x = 4 :: Integer + max_x_plus_y = 7 :: Integer + min_y = 3 :: Integer +Pareto front #23: Optimal model: + x = 3 :: Integer + y = 4 :: Integer + min_x = 3 :: Integer + max_x_plus_y = 7 :: Integer + min_y = 4 :: Integer +Pareto front #24: Optimal model: + x = 5 :: Integer y = 2 :: Integer - min_x = 0 :: Integer - max_x_plus_y = 2 :: Integer + min_x = 5 :: Integer + max_x_plus_y = 7 :: Integer min_y = 2 :: Integer -Pareto front #23: Optimal model: - x = 0 :: Integer +Pareto front #25: Optimal model: + x = 3 :: Integer y = 3 :: Integer - min_x = 0 :: Integer - max_x_plus_y = 3 :: Integer + min_x = 3 :: Integer + max_x_plus_y = 6 :: Integer min_y = 3 :: Integer -Pareto front #24: Optimal model: - x = 1 :: Integer +Pareto front #26: Optimal model: + x = 5 :: Integer y = 3 :: Integer - min_x = 1 :: Integer - max_x_plus_y = 4 :: Integer + min_x = 5 :: Integer + max_x_plus_y = 8 :: Integer min_y = 3 :: Integer -Pareto front #25: Optimal model: - x = 0 :: Integer +Pareto front #27: Optimal model: + x = 4 :: Integer y = 4 :: Integer - min_x = 0 :: Integer - max_x_plus_y = 4 :: Integer + min_x = 4 :: Integer + max_x_plus_y = 8 :: Integer min_y = 4 :: Integer -Pareto front #26: Optimal model: - x = 1 :: Integer +Pareto front #28: Optimal model: + x = 2 :: Integer y = 4 :: Integer - min_x = 1 :: Integer - max_x_plus_y = 5 :: Integer + min_x = 2 :: Integer + max_x_plus_y = 6 :: Integer min_y = 4 :: Integer -Pareto front #27: Optimal model: +Pareto front #29: Optimal model: + x = 5 :: Integer + y = 4 :: Integer + min_x = 5 :: Integer + max_x_plus_y = 9 :: Integer + min_y = 4 :: Integer +Pareto front #30: Optimal model: x = 2 :: Integer y = 3 :: Integer min_x = 2 :: Integer max_x_plus_y = 5 :: Integer min_y = 3 :: Integer -Pareto front #28: Optimal model: - x = 3 :: Integer - y = 0 :: Integer - min_x = 3 :: Integer - max_x_plus_y = 3 :: Integer - min_y = 0 :: Integer -Pareto front #29: Optimal model: - x = 4 :: Integer - y = 0 :: Integer - min_x = 4 :: Integer - max_x_plus_y = 4 :: Integer - min_y = 0 :: Integer -Pareto front #30: Optimal model: - x = 3 :: Integer - y = 1 :: Integer - min_x = 3 :: Integer - max_x_plus_y = 4 :: Integer - min_y = 1 :: Integer diff --git a/SBVTestSuite/GoldFiles/pareto2.gold b/SBVTestSuite/GoldFiles/pareto2.gold --- a/SBVTestSuite/GoldFiles/pareto2.gold +++ b/SBVTestSuite/GoldFiles/pareto2.gold @@ -24,159 +24,159 @@ max_x_plus_y = 5 :: Integer Pareto front #5: Optimal model: x = 0 :: Integer - y = 6 :: Integer - min_x = 0 :: Integer - max_y = 6 :: Integer - max_x_plus_y = 6 :: Integer -Pareto front #6: Optimal model: - x = 0 :: Integer y = 7 :: Integer min_x = 0 :: Integer max_y = 7 :: Integer max_x_plus_y = 7 :: Integer -Pareto front #7: Optimal model: +Pareto front #6: Optimal model: x = 0 :: Integer - y = 9 :: Integer + y = 6 :: Integer min_x = 0 :: Integer - max_y = 9 :: Integer - max_x_plus_y = 9 :: Integer -Pareto front #8: Optimal model: + max_y = 6 :: Integer + max_x_plus_y = 6 :: Integer +Pareto front #7: Optimal model: x = 0 :: Integer - y = 8 :: Integer + y = 0 :: Integer min_x = 0 :: Integer - max_y = 8 :: Integer - max_x_plus_y = 8 :: Integer + max_y = 0 :: Integer + max_x_plus_y = 0 :: Integer +Pareto front #8: Optimal model: + x = 0 :: Integer + y = -2 :: Integer + min_x = 0 :: Integer + max_y = -2 :: Integer + max_x_plus_y = -2 :: Integer Pareto front #9: Optimal model: x = 0 :: Integer - y = 11 :: Integer + y = -4 :: Integer min_x = 0 :: Integer - max_y = 11 :: Integer - max_x_plus_y = 11 :: Integer + max_y = -4 :: Integer + max_x_plus_y = -4 :: Integer Pareto front #10: Optimal model: x = 0 :: Integer - y = 13 :: Integer + y = -5 :: Integer min_x = 0 :: Integer - max_y = 13 :: Integer - max_x_plus_y = 13 :: Integer + max_y = -5 :: Integer + max_x_plus_y = -5 :: Integer Pareto front #11: Optimal model: x = 0 :: Integer - y = 14 :: Integer + y = -6 :: Integer min_x = 0 :: Integer - max_y = 14 :: Integer - max_x_plus_y = 14 :: Integer + max_y = -6 :: Integer + max_x_plus_y = -6 :: Integer Pareto front #12: Optimal model: x = 0 :: Integer - y = 15 :: Integer + y = -8 :: Integer min_x = 0 :: Integer - max_y = 15 :: Integer - max_x_plus_y = 15 :: Integer + max_y = -8 :: Integer + max_x_plus_y = -8 :: Integer Pareto front #13: Optimal model: x = 0 :: Integer - y = 17 :: Integer + y = -9 :: Integer min_x = 0 :: Integer - max_y = 17 :: Integer - max_x_plus_y = 17 :: Integer + max_y = -9 :: Integer + max_x_plus_y = -9 :: Integer Pareto front #14: Optimal model: - x = 0 :: Integer - y = 19 :: Integer - min_x = 0 :: Integer - max_y = 19 :: Integer - max_x_plus_y = 19 :: Integer + x = 0 :: Integer + y = -11 :: Integer + min_x = 0 :: Integer + max_y = -11 :: Integer + max_x_plus_y = -11 :: Integer Pareto front #15: Optimal model: - x = 0 :: Integer - y = 21 :: Integer - min_x = 0 :: Integer - max_y = 21 :: Integer - max_x_plus_y = 21 :: Integer + x = 0 :: Integer + y = -13 :: Integer + min_x = 0 :: Integer + max_y = -13 :: Integer + max_x_plus_y = -13 :: Integer Pareto front #16: Optimal model: - x = 0 :: Integer - y = 22 :: Integer - min_x = 0 :: Integer - max_y = 22 :: Integer - max_x_plus_y = 22 :: Integer + x = 0 :: Integer + y = -15 :: Integer + min_x = 0 :: Integer + max_y = -15 :: Integer + max_x_plus_y = -15 :: Integer Pareto front #17: Optimal model: - x = 0 :: Integer - y = 23 :: Integer - min_x = 0 :: Integer - max_y = 23 :: Integer - max_x_plus_y = 23 :: Integer + x = 0 :: Integer + y = -16 :: Integer + min_x = 0 :: Integer + max_y = -16 :: Integer + max_x_plus_y = -16 :: Integer Pareto front #18: Optimal model: - x = 0 :: Integer - y = 25 :: Integer - min_x = 0 :: Integer - max_y = 25 :: Integer - max_x_plus_y = 25 :: Integer + x = 0 :: Integer + y = -18 :: Integer + min_x = 0 :: Integer + max_y = -18 :: Integer + max_x_plus_y = -18 :: Integer Pareto front #19: Optimal model: - x = 0 :: Integer - y = 26 :: Integer - min_x = 0 :: Integer - max_y = 26 :: Integer - max_x_plus_y = 26 :: Integer + x = 0 :: Integer + y = -19 :: Integer + min_x = 0 :: Integer + max_y = -19 :: Integer + max_x_plus_y = -19 :: Integer Pareto front #20: Optimal model: - x = 0 :: Integer - y = 28 :: Integer - min_x = 0 :: Integer - max_y = 28 :: Integer - max_x_plus_y = 28 :: Integer + x = 0 :: Integer + y = -20 :: Integer + min_x = 0 :: Integer + max_y = -20 :: Integer + max_x_plus_y = -20 :: Integer Pareto front #21: Optimal model: - x = 0 :: Integer - y = 30 :: Integer - min_x = 0 :: Integer - max_y = 30 :: Integer - max_x_plus_y = 30 :: Integer + x = 0 :: Integer + y = -22 :: Integer + min_x = 0 :: Integer + max_y = -22 :: Integer + max_x_plus_y = -22 :: Integer Pareto front #22: Optimal model: - x = 0 :: Integer - y = 32 :: Integer - min_x = 0 :: Integer - max_y = 32 :: Integer - max_x_plus_y = 32 :: Integer + x = 0 :: Integer + y = -24 :: Integer + min_x = 0 :: Integer + max_y = -24 :: Integer + max_x_plus_y = -24 :: Integer Pareto front #23: Optimal model: - x = 0 :: Integer - y = 34 :: Integer - min_x = 0 :: Integer - max_y = 34 :: Integer - max_x_plus_y = 34 :: Integer + x = 0 :: Integer + y = -25 :: Integer + min_x = 0 :: Integer + max_y = -25 :: Integer + max_x_plus_y = -25 :: Integer Pareto front #24: Optimal model: - x = 0 :: Integer - y = 36 :: Integer - min_x = 0 :: Integer - max_y = 36 :: Integer - max_x_plus_y = 36 :: Integer + x = 0 :: Integer + y = -27 :: Integer + min_x = 0 :: Integer + max_y = -27 :: Integer + max_x_plus_y = -27 :: Integer Pareto front #25: Optimal model: - x = 0 :: Integer - y = 37 :: Integer - min_x = 0 :: Integer - max_y = 37 :: Integer - max_x_plus_y = 37 :: Integer + x = 0 :: Integer + y = -28 :: Integer + min_x = 0 :: Integer + max_y = -28 :: Integer + max_x_plus_y = -28 :: Integer Pareto front #26: Optimal model: - x = 0 :: Integer - y = 39 :: Integer - min_x = 0 :: Integer - max_y = 39 :: Integer - max_x_plus_y = 39 :: Integer + x = 0 :: Integer + y = -30 :: Integer + min_x = 0 :: Integer + max_y = -30 :: Integer + max_x_plus_y = -30 :: Integer Pareto front #27: Optimal model: - x = 0 :: Integer - y = 40 :: Integer - min_x = 0 :: Integer - max_y = 40 :: Integer - max_x_plus_y = 40 :: Integer + x = 0 :: Integer + y = -32 :: Integer + min_x = 0 :: Integer + max_y = -32 :: Integer + max_x_plus_y = -32 :: Integer Pareto front #28: Optimal model: - x = 0 :: Integer - y = 41 :: Integer - min_x = 0 :: Integer - max_y = 41 :: Integer - max_x_plus_y = 41 :: Integer + x = 0 :: Integer + y = -33 :: Integer + min_x = 0 :: Integer + max_y = -33 :: Integer + max_x_plus_y = -33 :: Integer Pareto front #29: Optimal model: - x = 0 :: Integer - y = 43 :: Integer - min_x = 0 :: Integer - max_y = 43 :: Integer - max_x_plus_y = 43 :: Integer + x = 0 :: Integer + y = -35 :: Integer + min_x = 0 :: Integer + max_y = -35 :: Integer + max_x_plus_y = -35 :: Integer Pareto front #30: Optimal model: - x = 0 :: Integer - y = 44 :: Integer - min_x = 0 :: Integer - max_y = 44 :: Integer - max_x_plus_y = 44 :: Integer + x = 0 :: Integer + y = -37 :: Integer + min_x = 0 :: Integer + max_y = -37 :: Integer + max_x_plus_y = -37 :: Integer *** Note: Pareto-front extraction was terminated as requested by the user. *** There might be many other results! diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold --- a/SBVTestSuite/GoldFiles/query1.gold +++ b/SBVTestSuite/GoldFiles/query1.gold @@ -72,7 +72,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version) -[RECV] (:version "4.17.0") +[RECV] (:version "5.1.0") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4) @@ -103,7 +103,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version) -[RECV] (:version "4.17.0") +[RECV] (:version "5.1.0") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time) diff --git a/SBVTestSuite/GoldFiles/query_Interpolant4.gold b/SBVTestSuite/GoldFiles/query_Interpolant4.gold --- a/SBVTestSuite/GoldFiles/query_Interpolant4.gold +++ b/SBVTestSuite/GoldFiles/query_Interpolant4.gold @@ -36,10 +36,10 @@ [SEND] (get-interpolant s8 s13) [RECV] (or (and (= s1 s2) (= s1 s3)) (<= (+ (* (- 1) s1) s0) (- 1)) - (<= (+ s1 (* (- 1) s0)) (- 1)) + (<= (+ (* (- 1) s0) s1) (- 1)) (= s2 s3)) *** Solver : Z3 *** Exit code: ExitSuccess FINAL OUTPUT: -"(or (and (= s1 s2) (= s1 s3)) (<= (+ (* (- 1) s1) s0) (- 1)) (<= (+ s1 (* (- 1) s0)) (- 1)) (= s2 s3))" +"(or (and (= s1 s2) (= s1 s3)) (<= (+ (* (- 1) s1) s0) (- 1)) (<= (+ (* (- 1) s0) s1) (- 1)) (= s2 s3))" diff --git a/SBVTestSuite/GoldFiles/query_abc.gold b/SBVTestSuite/GoldFiles/query_abc.gold --- a/SBVTestSuite/GoldFiles/query_abc.gold +++ b/SBVTestSuite/GoldFiles/query_abc.gold @@ -46,4 +46,3 @@ [RECV] ((s1 #x1)) *** Solver : ABC *** Exit code: ExitSuccess -*** Std-err : Cmd warning: redefining '%graft' diff --git a/SBVTestSuite/GoldFiles/query_badOption.gold b/SBVTestSuite/GoldFiles/query_badOption.gold --- a/SBVTestSuite/GoldFiles/query_badOption.gold +++ b/SBVTestSuite/GoldFiles/query_badOption.gold @@ -29,6 +29,7 @@ *** rlimit (unsigned int) (default: 0) *** smtlib2_compliant (bool) (default: false) *** stats (bool) (default: false) +*** suppress_platform_verbose (bool) (default: false) *** timeout (unsigned int) (default: 4294967295) *** trace (bool) (default: false) *** trace_file_name (string) (default: z3.log) @@ -39,7 +40,7 @@ *** well_sorted_check (bool) (default: false)") *** *** Exit code : ExitFailure (-15) -*** Executable: /usr/local/bin/z3 +*** Executable: /Users/lerkok/Projects/Solvers/bin/z3 *** Options : -nw -in -smt2 *** *** Reason : Backend solver reports it does not support this option. diff --git a/SBVTestSuite/GoldFiles/set_uninterp1.gold b/SBVTestSuite/GoldFiles/set_uninterp1.gold --- a/SBVTestSuite/GoldFiles/set_uninterp1.gold +++ b/SBVTestSuite/GoldFiles/set_uninterp1.gold @@ -60,7 +60,7 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) A true))) +[RECV] ((s0 (store (store ((as const (Array E Bool)) false) A true) B true))) [GOOD] (push 1) [GOOD] (define-fun s7 () (Array E Bool) (store (store ((as const (Array E Bool)) false) (as B E) true) (as A E) true)) [GOOD] (define-fun s8 () Bool (distinct s0 s7)) @@ -69,36 +69,36 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store (store ((as const (Array E Bool)) true) C false) A false))) +[RECV] ((s0 (store ((as const (Array E Bool)) false) B true))) [GOOD] (push 1) -[GOOD] (define-fun s9 () (Array E Bool) (store (store ((as const (Array E Bool)) true) (as C E) false) (as A E) false)) +[GOOD] (define-fun s9 () (Array E Bool) (store ((as const (Array E Bool)) false) (as B E) true)) [GOOD] (define-fun s10 () Bool (distinct s0 s9)) [GOOD] (assert s10) Fast allSat, Looking for solution 6 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store ((as const (Array E Bool)) true) B false))) +[RECV] ((s0 (store ((as const (Array E Bool)) true) A false))) [GOOD] (push 1) -[GOOD] (define-fun s11 () (Array E Bool) (store ((as const (Array E Bool)) true) (as B E) false)) +[GOOD] (define-fun s11 () (Array E Bool) (store ((as const (Array E Bool)) true) (as A E) false)) [GOOD] (define-fun s12 () Bool (distinct s0 s11)) [GOOD] (assert s12) Fast allSat, Looking for solution 7 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) B true))) +[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) A true))) [GOOD] (push 1) -[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) false) (as C E) true) (as B E) true)) +[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) false) (as C E) true) (as A E) true)) [GOOD] (define-fun s14 () Bool (distinct s0 s13)) [GOOD] (assert s14) Fast allSat, Looking for solution 8 [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 ((as const (Array E Bool)) true))) +[RECV] ((s0 (store (store (store ((as const (Array E Bool)) false) C true) A true) B true))) [GOOD] (push 1) -[GOOD] (define-fun s15 () (Array E Bool) ((as const (Array E Bool)) true)) +[GOOD] (define-fun s15 () (Array E Bool) (store (store (store ((as const (Array E Bool)) false) (as C E) true) (as B E) true) (as A E) true)) [GOOD] (define-fun s16 () Bool (distinct s0 s15)) [GOOD] (assert s16) Fast allSat, Looking for solution 9 @@ -117,13 +117,13 @@ FINAL: Solution #1: - s0 = U :: {E} + s0 = {A,B,C} :: {E} Solution #2: - s0 = {B,C} :: {E} + s0 = {A,C} :: {E} Solution #3: - s0 = U - {B} :: {E} + s0 = U - {A} :: {E} Solution #4: - s0 = U - {A,C} :: {E} + s0 = {B} :: {E} Solution #5: s0 = {A,B} :: {E} Solution #6: diff --git a/SBVTestSuite/GoldFiles/uiSat_test3.gold b/SBVTestSuite/GoldFiles/uiSat_test3.gold --- a/SBVTestSuite/GoldFiles/uiSat_test3.gold +++ b/SBVTestSuite/GoldFiles/uiSat_test3.gold @@ -941,10 +941,7 @@ [SEND] (get-value (q1)) [RECV] ((q1 ((as const (Array Bool Bool)) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true) - false - true - true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true))) [GOOD] (define-fun q1_model33 ((x!0 Bool)) Bool true ) @@ -953,9 +950,8 @@ (distinct (q1 x!0) (q1_model33 x!0)))) [GOOD] (define-fun q2_model33 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) true - (ite (and (= x!0 true) (= x!1 false)) true - false)) + (ite (and (= x!0 true) (= x!1 true)) true + false) ) [GOOD] (define-fun q2_model33_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -970,19 +966,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) true))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true))) [GOOD] (define-fun q1_model34 ((x!0 Bool)) Bool - true + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model34_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model34 x!0)))) [GOOD] (define-fun q2_model34 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) false - true) + (ite (and (= x!0 true) (= x!1 true)) true + false) ) [GOOD] (define-fun q2_model34_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -997,14 +994,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) true))) +[RECV] ((q1 ((as const (Array Bool Bool)) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true) - true - true - true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true))) [GOOD] (define-fun q1_model35 ((x!0 Bool)) Bool - true + false ) [GOOD] (define-fun q1_model35_reject () Bool (exists ((x!0 Bool)) @@ -1012,8 +1006,7 @@ (q1_model35 x!0)))) [GOOD] (define-fun q2_model35 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 true) (= x!1 true)) true - (ite (and (= x!0 false) (= x!1 true)) true - false)) + false) ) [GOOD] (define-fun q2_model35_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1028,18 +1021,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) true))) +[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true))) [GOOD] (define-fun q1_model36 ((x!0 Bool)) Bool - true + (ite (and (= x!0 false)) true + false) ) [GOOD] (define-fun q1_model36_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model36 x!0)))) [GOOD] (define-fun q2_model36 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) true + (ite (and (= x!0 true) (= x!1 true)) true false) ) [GOOD] (define-fun q2_model36_reject () Bool @@ -1055,24 +1049,24 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false))) +[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true) - true +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false) true - true))) + false + false))) [GOOD] (define-fun q1_model37 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + (ite (and (= x!0 false)) true + false) ) [GOOD] (define-fun q1_model37_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model37 x!0)))) [GOOD] (define-fun q2_model37 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) true - (ite (and (= x!0 false) (= x!1 true)) true - false)) + (ite (and (= x!0 true) (= x!1 false)) false + (ite (and (= x!0 false) (= x!1 false)) false + true)) ) [GOOD] (define-fun q2_model37_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1087,20 +1081,23 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false))) +[RECV] ((q1 ((as const (Array Bool Bool)) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false))) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false) + true + false + false))) [GOOD] (define-fun q1_model38 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + true ) [GOOD] (define-fun q1_model38_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model38 x!0)))) [GOOD] (define-fun q2_model38 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) false - true) + (ite (and (= x!0 true) (= x!1 false)) false + (ite (and (= x!0 false) (= x!1 false)) false + true)) ) [GOOD] (define-fun q2_model38_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1115,18 +1112,18 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) false))) +[RECV] ((q1 ((as const (Array Bool Bool)) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false))) [GOOD] (define-fun q1_model39 ((x!0 Bool)) Bool - false + true ) [GOOD] (define-fun q1_model39_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model39 x!0)))) [GOOD] (define-fun q2_model39 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) false + (ite (and (= x!0 false) (= x!1 false)) false true) ) [GOOD] (define-fun q2_model39_reject () Bool @@ -1142,22 +1139,22 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) false))) +[RECV] ((q1 ((as const (Array Bool Bool)) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false) - false +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false) true + true false))) [GOOD] (define-fun q1_model40 ((x!0 Bool)) Bool - false + true ) [GOOD] (define-fun q1_model40_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model40 x!0)))) [GOOD] (define-fun q2_model40 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) false (ite (and (= x!0 true) (= x!1 true)) false + (ite (and (= x!0 false) (= x!1 false)) false true)) ) [GOOD] (define-fun q2_model40_reject () Bool @@ -1173,23 +1170,24 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) true))) +[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false) - false +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true) true - false))) + false + true))) [GOOD] (define-fun q1_model41 ((x!0 Bool)) Bool - true + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model41_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model41 x!0)))) [GOOD] (define-fun q2_model41 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) false - (ite (and (= x!0 true) (= x!1 true)) false - true)) + (ite (and (= x!0 true) (= x!1 false)) true + (ite (and (= x!0 false) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model41_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1204,19 +1202,20 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) false))) +[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false))) [GOOD] (define-fun q1_model42 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) false + true) ) [GOOD] (define-fun q1_model42_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model42 x!0)))) [GOOD] (define-fun q2_model42 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) true - false) + (ite (and (= x!0 true) (= x!1 true)) false + true) ) [GOOD] (define-fun q2_model42_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1233,7 +1232,7 @@ [SEND] (get-value (q1)) [RECV] ((q1 ((as const (Array Bool Bool)) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false))) [GOOD] (define-fun q1_model43 ((x!0 Bool)) Bool false ) @@ -1242,8 +1241,8 @@ (distinct (q1 x!0) (q1_model43 x!0)))) [GOOD] (define-fun q2_model43 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 false)) true - false) + (ite (and (= x!0 true) (= x!1 true)) false + true) ) [GOOD] (define-fun q2_model43_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1285,19 +1284,18 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 ((as const (Array Bool Bool)) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true))) [GOOD] (define-fun q1_model45 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + false ) [GOOD] (define-fun q1_model45_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model45 x!0)))) [GOOD] (define-fun q2_model45 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) true + (ite (and (= x!0 true) (= x!1 false)) true false) ) [GOOD] (define-fun q2_model45_reject () Bool @@ -1313,12 +1311,14 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 ((as const (Array Bool Bool)) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true))) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true) + true + true + true))) [GOOD] (define-fun q1_model46 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + false ) [GOOD] (define-fun q1_model46_reject () Bool (exists ((x!0 Bool)) @@ -1326,7 +1326,8 @@ (q1_model46 x!0)))) [GOOD] (define-fun q2_model46 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 true) (= x!1 true)) true - false) + (ite (and (= x!0 true) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model46_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1343,10 +1344,7 @@ [SEND] (get-value (q1)) [RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true true true) - false - true - true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true))) [GOOD] (define-fun q1_model47 ((x!0 Bool)) Bool (ite (and (= x!0 true)) true false) @@ -1357,8 +1355,7 @@ (q1_model47 x!0)))) [GOOD] (define-fun q2_model47 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 true)) true - (ite (and (= x!0 true) (= x!1 true)) true - false)) + false) ) [GOOD] (define-fun q2_model47_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1373,23 +1370,24 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) false))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true true true) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false) false true - true))) + false))) [GOOD] (define-fun q1_model48 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model48_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model48 x!0)))) [GOOD] (define-fun q2_model48 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) true - (ite (and (= x!0 true) (= x!1 true)) true - false)) + (ite (and (= x!0 false) (= x!1 true)) false + (ite (and (= x!0 false) (= x!1 false)) false + true)) ) [GOOD] (define-fun q2_model48_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1406,10 +1404,10 @@ [SEND] (get-value (q1)) [RECV] ((q1 ((as const (Array Bool Bool)) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true) false true - false))) + true))) [GOOD] (define-fun q1_model49 ((x!0 Bool)) Bool false ) @@ -1418,9 +1416,9 @@ (distinct (q1 x!0) (q1_model49 x!0)))) [GOOD] (define-fun q2_model49 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) false - (ite (and (= x!0 false) (= x!1 false)) false - true)) + (ite (and (= x!0 false) (= x!1 true)) true + (ite (and (= x!0 true) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model49_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1524,7 +1522,7 @@ [SEND] (get-value (q1)) [RECV] ((q1 ((as const (Array Bool Bool)) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false true false) true true false))) @@ -1537,7 +1535,7 @@ (q1_model53 x!0)))) [GOOD] (define-fun q2_model53 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 true) (= x!1 true)) false - (ite (and (= x!0 false) (= x!1 false)) false + (ite (and (= x!0 false) (= x!1 true)) false true)) ) [GOOD] (define-fun q2_model53_reject () Bool @@ -1553,24 +1551,23 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 ((as const (Array Bool Bool)) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true) false - true - false))) + false + true))) [GOOD] (define-fun q1_model54 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + true ) [GOOD] (define-fun q1_model54_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model54 x!0)))) [GOOD] (define-fun q2_model54 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 true)) false - (ite (and (= x!0 false) (= x!1 false)) false - true)) + (ite (and (= x!0 false) (= x!1 false)) true + (ite (and (= x!0 true) (= x!1 false)) true + false)) ) [GOOD] (define-fun q2_model54_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1585,20 +1582,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true))) +[RECV] ((q1 ((as const (Array Bool Bool)) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false))) [GOOD] (define-fun q1_model55 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + true ) [GOOD] (define-fun q1_model55_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model55 x!0)))) [GOOD] (define-fun q2_model55 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) true - false) + (ite (and (= x!0 true) (= x!1 true)) false + true) ) [GOOD] (define-fun q2_model55_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1613,19 +1609,23 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) true))) +[RECV] ((q1 ((as const (Array Bool Bool)) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false))) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true) + false + false + true))) [GOOD] (define-fun q1_model56 ((x!0 Bool)) Bool - true + false ) [GOOD] (define-fun q1_model56_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model56 x!0)))) [GOOD] (define-fun q2_model56 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) false - true) + (ite (and (= x!0 false) (= x!1 false)) true + (ite (and (= x!0 false) (= x!1 true)) true + false)) ) [GOOD] (define-fun q2_model56_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1640,24 +1640,24 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false))) +[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true) - false +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false) + true false - true))) + false))) [GOOD] (define-fun q1_model57 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + (ite (and (= x!0 false)) true + false) ) [GOOD] (define-fun q1_model57_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model57 x!0)))) [GOOD] (define-fun q2_model57 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) true - (ite (and (= x!0 true) (= x!1 false)) true - false)) + (ite (and (= x!0 true) (= x!1 false)) false + (ite (and (= x!0 true) (= x!1 true)) false + true)) ) [GOOD] (define-fun q2_model57_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1672,20 +1672,23 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false))) +[RECV] ((q1 ((as const (Array Bool Bool)) false))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true))) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false) + true + false + false))) [GOOD] (define-fun q1_model58 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) false - true) + false ) [GOOD] (define-fun q1_model58_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model58 x!0)))) [GOOD] (define-fun q2_model58 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) true - false) + (ite (and (= x!0 true) (= x!1 false)) false + (ite (and (= x!0 false) (= x!1 false)) false + true)) ) [GOOD] (define-fun q2_model58_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1700,14 +1703,15 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) false))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false) true false false))) [GOOD] (define-fun q1_model59 ((x!0 Bool)) Bool - false + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model59_reject () Bool (exists ((x!0 Bool)) @@ -1715,7 +1719,7 @@ (q1_model59 x!0)))) [GOOD] (define-fun q2_model59 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 true) (= x!1 false)) false - (ite (and (= x!0 true) (= x!1 true)) false + (ite (and (= x!0 false) (= x!1 false)) false true)) ) [GOOD] (define-fun q2_model59_reject () Bool @@ -1731,24 +1735,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) +[RECV] ((q1 ((as const (Array Bool Bool)) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false) - true - false - false))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true))) [GOOD] (define-fun q1_model60 ((x!0 Bool)) Bool - (ite (and (= x!0 true)) true - false) + true ) [GOOD] (define-fun q1_model60_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model60 x!0)))) [GOOD] (define-fun q2_model60 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 false)) false - (ite (and (= x!0 true) (= x!1 true)) false - true)) + (ite (and (= x!0 false) (= x!1 true)) true + false) ) [GOOD] (define-fun q2_model60_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1763,23 +1762,24 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) true))) +[RECV] ((q1 (lambda ((x!1 Bool)) x!1))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true) - false +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false) + true false - true))) + false))) [GOOD] (define-fun q1_model61 ((x!0 Bool)) Bool - true + (ite (and (= x!0 true)) true + false) ) [GOOD] (define-fun q1_model61_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model61 x!0)))) [GOOD] (define-fun q2_model61 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) true - (ite (and (= x!0 false) (= x!1 true)) true - false)) + (ite (and (= x!0 true) (= x!1 false)) false + (ite (and (= x!0 true) (= x!1 true)) false + true)) ) [GOOD] (define-fun q2_model61_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1796,7 +1796,10 @@ [SEND] (get-value (q1)) [RECV] ((q1 ((as const (Array Bool Bool)) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true))) +[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false) + true + false + false))) [GOOD] (define-fun q1_model62 ((x!0 Bool)) Bool true ) @@ -1805,8 +1808,9 @@ (distinct (q1 x!0) (q1_model62 x!0)))) [GOOD] (define-fun q2_model62 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 false) (= x!1 false)) true - false) + (ite (and (= x!0 true) (= x!1 false)) false + (ite (and (= x!0 true) (= x!1 true)) false + true)) ) [GOOD] (define-fun q2_model62_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1821,18 +1825,19 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 ((as const (Array Bool Bool)) true))) +[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true))) [GOOD] (define-fun q1_model63 ((x!0 Bool)) Bool - true + (ite (and (= x!0 false)) true + false) ) [GOOD] (define-fun q1_model63_reject () Bool (exists ((x!0 Bool)) (distinct (q1 x!0) (q1_model63 x!0)))) [GOOD] (define-fun q2_model63 ((x!0 Bool) (x!1 Bool)) Bool - (ite (and (= x!0 true) (= x!1 true)) true + (ite (and (= x!0 false) (= x!1 false)) true false) ) [GOOD] (define-fun q2_model63_reject () Bool @@ -1848,15 +1853,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (q1)) -[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true))) +[RECV] ((q1 ((as const (Array Bool Bool)) true))) [SEND] (get-value (q2)) -[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true) - false - false - true))) +[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true))) [GOOD] (define-fun q1_model64 ((x!0 Bool)) Bool - (ite (and (= x!0 false)) true - false) + true ) [GOOD] (define-fun q1_model64_reject () Bool (exists ((x!0 Bool)) @@ -1864,8 +1865,7 @@ (q1_model64 x!0)))) [GOOD] (define-fun q2_model64 ((x!0 Bool) (x!1 Bool)) Bool (ite (and (= x!0 false) (= x!1 false)) true - (ite (and (= x!0 false) (= x!1 true)) true - false)) + false) ) [GOOD] (define-fun q2_model64_reject () Bool (exists ((x!0 Bool) (x!1 Bool)) @@ -1884,36 +1884,28 @@ RESULT: Solution #1: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool q2 False False = True - q2 False True = True q2 _ _ = False Solution #2: q1 :: Bool -> Bool - q1 _ = True - - q2 :: Bool -> Bool -> Bool - q2 True True = True - q2 _ _ = False -Solution #3: - q1 :: Bool -> Bool - q1 _ = True + q1 False = True + q1 _ = False q2 :: Bool -> Bool -> Bool q2 False False = True q2 _ _ = False -Solution #4: +Solution #3: q1 :: Bool -> Bool q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False False = True - q2 False True = True - q2 _ _ = False -Solution #5: + q2 True False = False + q2 True True = False + q2 _ _ = True +Solution #4: q1 :: Bool -> Bool q1 True = True q1 _ = False @@ -1922,63 +1914,70 @@ q2 True False = False q2 True True = False q2 _ _ = True +Solution #5: + q1 :: Bool -> Bool + q1 _ = True + + q2 :: Bool -> Bool -> Bool + q2 False True = True + q2 _ _ = False Solution #6: q1 :: Bool -> Bool - q1 _ = False + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True False = False - q2 True True = False - q2 _ _ = True + q2 True False = False + q2 False False = False + q2 _ _ = True Solution #7: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False False = True - q2 _ _ = False + q2 True False = False + q2 False False = False + q2 _ _ = True Solution #8: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 False = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False False = True - q2 True False = True - q2 _ _ = False + q2 True False = False + q2 True True = False + q2 _ _ = True Solution #9: q1 :: Bool -> Bool - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 _ _ = True + q2 False False = True + q2 False True = True + q2 _ _ = False Solution #10: q1 :: Bool -> Bool - q1 False = True - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True True = True - q2 _ _ = False + q2 True True = False + q2 _ _ = True Solution #11: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = False - q2 False False = False - q2 _ _ = True + q2 False False = True + q2 True False = True + q2 _ _ = False Solution #12: q1 :: Bool -> Bool q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 False False = False - q2 _ _ = True + q2 True True = False + q2 False True = False + q2 _ _ = True Solution #13: q1 :: Bool -> Bool q1 True = True @@ -2008,17 +2007,18 @@ q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False True = False - q2 False False = False - q2 _ _ = True + q2 False True = True + q2 True False = True + q2 _ _ = False Solution #17: q1 :: Bool -> Bool - q1 _ = False + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 True True = True - q2 _ _ = False + q2 False True = False + q2 False False = False + q2 _ _ = True Solution #18: q1 :: Bool -> Bool q1 True = True @@ -2026,24 +2026,22 @@ q2 :: Bool -> Bool -> Bool q2 False True = True - q2 True True = True q2 _ _ = False Solution #19: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = True - q2 _ _ = False + q2 True True = True + q2 True False = True + q2 _ _ = False Solution #20: q1 :: Bool -> Bool - q1 True = True - q1 _ = False + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 _ _ = False + q2 True False = True + q2 _ _ = False Solution #21: q1 :: Bool -> Bool q1 _ = False @@ -2056,85 +2054,87 @@ q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True False = True - q2 _ _ = False + q2 True True = False + q2 _ _ = True Solution #23: q1 :: Bool -> Bool - q1 _ = False + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True True = True - q2 _ _ = False + q2 True True = False + q2 _ _ = True Solution #24: q1 :: Bool -> Bool - q1 _ = True + q1 True = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = False - q2 True True = False - q2 _ _ = True + q2 True False = True + q2 False False = True + q2 _ _ = False Solution #25: q1 :: Bool -> Bool - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = False - q2 True True = False - q2 _ _ = True + q2 True True = False + q2 False False = False + q2 _ _ = True Solution #26: q1 :: Bool -> Bool - q1 _ = False + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 _ _ = True + q2 False False = False + q2 _ _ = True Solution #27: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 _ = True q2 :: Bool -> Bool -> Bool - q2 True True = False - q2 _ _ = True + q2 True False = False + q2 False False = False + q2 _ _ = True Solution #28: q1 :: Bool -> Bool - q1 True = False - q1 _ = True + q1 False = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = True - q2 False True = True - q2 _ _ = False + q2 True False = False + q2 False False = False + q2 _ _ = True Solution #29: q1 :: Bool -> Bool - q1 _ = True + q1 False = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 _ _ = False + q2 True True = True + q2 _ _ = False Solution #30: q1 :: Bool -> Bool - q1 _ = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 True True = True - q2 False True = True - q2 _ _ = False + q2 True True = True + q2 _ _ = False Solution #31: q1 :: Bool -> Bool - q1 _ = True + q1 True = True + q1 _ = False q2 :: Bool -> Bool -> Bool - q2 False False = False - q2 _ _ = True + q2 True True = True + q2 _ _ = False Solution #32: q1 :: Bool -> Bool q1 _ = True q2 :: Bool -> Bool -> Bool - q2 False True = True - q2 True False = True - q2 _ _ = False + q2 True True = True + q2 _ _ = False Solution #33: q1 :: Bool -> Bool q1 _ = True diff --git a/SBVTestSuite/GoldFiles/validate_0.gold b/SBVTestSuite/GoldFiles/validate_0.gold --- a/SBVTestSuite/GoldFiles/validate_0.gold +++ b/SBVTestSuite/GoldFiles/validate_0.gold @@ -27,7 +27,6 @@ [RECV] ((s0 #x0)) *** Solver : ABC *** Exit code: ExitSuccess -*** Std-err : Cmd warning: redefining '%graft' [VALIDATE] Validating the model. Assignment: [VALIDATE] x = 0 :: Word8 [VALIDATE] There are no constraints to check. diff --git a/SBVTestSuite/GoldFiles/validate_2.gold b/SBVTestSuite/GoldFiles/validate_2.gold --- a/SBVTestSuite/GoldFiles/validate_2.gold +++ b/SBVTestSuite/GoldFiles/validate_2.gold @@ -25,11 +25,11 @@ [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0)) -[RECV] ((s0 (fp #b0 #x00 #b00000000000000011001101))) +[RECV] ((s0 (fp #b0 #x00 #b00000000101010111000111))) *** Solver : Z3 *** Exit code: ExitSuccess [VALIDATE] Validating the model. Assignment: -[VALIDATE] x = 2.87e-43 :: Float +[VALIDATE] x = 3.0771e-41 :: Float [VALIDATE] There are no constraints to check. [VALIDATE] Validating outputs. @@ -38,7 +38,7 @@ *** *** Assignment: *** -*** x = 2.87e-43 :: Float +*** x = 3.0771e-41 :: Float *** *** Floating point FMA operation is not supported concretely. *** @@ -48,4 +48,4 @@ *** Alleged model: *** *** Satisfiable. Model: -*** x = 2.87e-43 :: Float +*** x = 3.0771e-41 :: Float diff --git a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs --- a/SBVTestSuite/TestSuite/Basics/ArithSolver.hs +++ b/SBVTestSuite/TestSuite/Basics/ArithSolver.hs @@ -919,8 +919,7 @@ misc :: [TestTree] misc = [ testCase "misc-t1" $ assertIsSat t1 ] - where -- https://stackoverflow.com/questions/69033969/trivial-rationals-problems-without-variables-in-sbv-solver-in-haskell - t1 = do _xs <- sRationals [] + where t1 = do _xs <- sRationals [] constrain $ (5.%1:: SRational) .<= (5.%1:: SRational) realRatConvs :: [TestTree] @@ -944,9 +943,8 @@ , testCase "ratConv8" $ assertIsThm ratRneTieEven , testCase "ratConv9" $ assertIsThm ratRnaTieAway - -- z3 struggles with this in the compliant mode so we turn compliance off for these two - , testCase "ratRealRoundTrip1" $ assert $ isTheoremWith z3{smtLib2Compliant = False} ratToRealToRat - , testCase "ratRealRoundTrip2" $ assert $ isTheoremWith z3{smtLib2Compliant = False} realToRatToReal + , testCase "ratRealRoundTrip1" $ assert $ isTheorem ratToRealToRat + , testCase "ratRealRoundTrip2" $ assert $ isTheorem realToRatToReal , testCase "convertCov1" $ assertIsSat (\x y -> sFromIntegral @Word8 @Integer x .== y) , testCase "convertCov2" $ assertIsSat (\x y -> sFromIntegral @Integer @Word8 x .== y) diff --git a/SBVTestSuite/TestSuite/Basics/Lambda.hs b/SBVTestSuite/TestSuite/Basics/Lambda.hs --- a/SBVTestSuite/TestSuite/Basics/Lambda.hs +++ b/SBVTestSuite/TestSuite/Basics/Lambda.hs @@ -110,8 +110,7 @@ , \a b -> P.foldr (+) 0 (P.zipWith (+) a b) ) - -- Disabled due to z3 bug: https://github.com/LeventErkok/sbv/issues/773 - -- , goldenCapturedIO "lambda26" $ eval1 ([[1..5], [1..10], [1..20]] :: [[Integer]]) (concat, P.concat) + , goldenCapturedIO "lambda26" $ eval1 ([[1..5], [1..10], [1..20]] :: [[Integer]]) (concat, P.concat) , goldenCapturedIO "lambda27" $ eval1 [2, 4, 6, 8, 10 :: Integer] (all (\x -> x `sMod` 2 .== 0), P.all (\x -> x `mod` 2 == 0)) , goldenCapturedIO "lambda28" $ eval1 [2, 4, 6, 1, 8, 10 :: Integer] (all (\x -> x `sMod` 2 .== 0), P.all (\x -> x `mod` 2 == 0)) @@ -281,7 +280,6 @@ , \xs ys -> P.map (\x -> P.map (\y -> x + y) xs) ys ) - {- Disabled due to z3 bug: https://github.com/LeventErkok/sbv/issues/773 , let cls :: SList Integer -> Closure (SList Integer) (SList Integer -> SList Integer) cls ys = Closure { closureEnv = ys , closureFun = \env xs -> xs ++ env @@ -290,7 +288,6 @@ ( \xss ys -> map (cls ys) xss , \xss ys -> P.map (P.++ ys) xss ) - -} ] P.++ qc1 "lambdaQC1" P.sum (foldr ((+) @SInteger) (0::SInteger)) P.++ qc2 "lambdaQC2" (+) (smtFunction "sadd" ((+) :: SInteger -> SInteger -> SInteger)) diff --git a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr --- a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr @@ -15,8 +15,8 @@ (isLet e ==> (e .== e =: qed))] PCase17.hs:18:14: error: [GHC-83865] " Couldn't match expected type: Proof SBool - with actual type: sbv-14.5:Data.SBV.TP.TP.TPProofGen - (SBV Bool) [sbv-14.5:Data.SBV.TP.TP.Helper] () + with actual type: sbv-14.6:Data.SBV.TP.TP.TPProofGen + (SBV Bool) [sbv-14.6:Data.SBV.TP.TP.Helper] () " In the expression: cases [(isZero e ==> (e .== e =: qed)), (isNum e ==> (e .== e =: qed)), diff --git a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr --- a/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr @@ -15,8 +15,8 @@ (isLet e ==> undefined)] PCase38.hs:12:14: error: [GHC-83865] " Couldn't match expected type: Proof SBool - with actual type: sbv-14.5:Data.SBV.TP.TP.TPProofGen - a0 [sbv-14.5:Data.SBV.TP.TP.Helper] () + with actual type: sbv-14.6:Data.SBV.TP.TP.TPProofGen + a0 [sbv-14.6:Data.SBV.TP.TP.Helper] () " In the expression: cases [(isZero e ==> undefined), (isNum e ==> undefined), diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr @@ -28,4 +28,4 @@ ((\ _ -> 1) (Data.SBV.Maybe.getJust_1 m)) (ite (Data.SBV.Maybe.isNothing m) 0 - (symWithKind "unmatched_sCase_Maybe_6989586621679035040"))) + (symWithKind "unmatched_sCase_Maybe_6989586621679035057"))) diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr @@ -24,4 +24,4 @@ ((\ _ -> Data.SBV.Either.isRight (Data.SBV.Maybe.getJust_1 m)) (Data.SBV.Maybe.getJust_1 m))) ((\ _ -> 1) (Data.SBV.Maybe.getJust_1 m)) - (symWithKind "unmatched_sCase_Maybe_6989586621679035040"))) + (symWithKind "unmatched_sCase_Maybe_6989586621679035057"))) diff --git a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr --- a/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr +++ b/SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr @@ -30,4 +30,4 @@ (ite (Data.SBV.Either.isRight e) ((\ _ -> 1) (Data.SBV.Either.getRight_1 e)) - (symWithKind "unmatched_sCase_Either_6989586621679035002"))) + (symWithKind "unmatched_sCase_Either_6989586621679035019"))) diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv -Version : 14.5 +Version : 14.6 Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description : Express properties about Haskell programs and automatically prove them using SMT @@ -283,6 +283,7 @@ , Documentation.SBV.Examples.TP.SumReverse , Documentation.SBV.Examples.TP.Tao , Documentation.SBV.Examples.TP.TautologyChecker + , Documentation.SBV.Examples.TP.Tree , Documentation.SBV.Examples.TP.UpDown , Documentation.SBV.Examples.TP.VM , Documentation.SBV.Examples.Transformers.SymbolicEval