sbv 10.6 → 10.7
raw patch · 10 files changed
+167/−15 lines, 10 files
Files
- CHANGES.md +3/−2
- Data/SBV/Core/Model.hs +5/−5
- README.md +2/−2
- SBVTestSuite/GoldFiles/allSat8.gold +1/−1
- SBVTestSuite/GoldFiles/nested1.gold +1/−1
- SBVTestSuite/GoldFiles/nested2.gold +1/−1
- SBVTestSuite/GoldFiles/nested3.gold +1/−1
- SBVTestSuite/GoldFiles/nested4.gold +1/−1
- SBVTestSuite/TestSuite/Uninterpreted/Function.hs +151/−0
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,8 +1,10 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> -* Latest Hackage released version: 10.6, 2024-03-16+### Version 10.7, 2024-03-23 + * Fix SMTDefinable instances for functions of arity 8-12. Thanks to Nick Lewchenko for the patch.+ ### Version 10.6, 2024-03-16 * Added Data.SBV.Tools.BVOptimize module, which implements a custom optimizer for unsigned bit-vector@@ -2378,7 +2380,6 @@ to the chosen solver as determined by the imported module. (The latter is useful for modifying options to the SMT solver in an solver-agnostic way.) * Various improvements to Z3 model parsing routines.- * New web page for SBV: http://leventerkok.github.io/sbv/ is now online. ### Version 2.8, 2012-11-29
Data/SBV/Core/Model.hs view
@@ -2611,7 +2611,7 @@ result st = do isSMT <- inSMTMode st case (isSMT, uiKind) of (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7)- _ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki]) =<< retrieveUICode nm st ka uiKind+ _ -> do newUninterpreted st (nm, mbArgs) (SBVType [ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind sw0 <- sbvToSV st arg0 sw1 <- sbvToSV st arg1 sw2 <- sbvToSV st arg2@@ -2647,7 +2647,7 @@ result st = do isSMT <- inSMTMode st case (isSMT, uiKind) of (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8)- _ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj]) =<< retrieveUICode nm st ka uiKind+ _ -> do newUninterpreted st (nm, mbArgs) (SBVType [kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind sw0 <- sbvToSV st arg0 sw1 <- sbvToSV st arg1 sw2 <- sbvToSV st arg2@@ -2685,7 +2685,7 @@ result st = do isSMT <- inSMTMode st case (isSMT, uiKind) of (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9)- _ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj, kk]) =<< retrieveUICode nm st ka uiKind+ _ -> do newUninterpreted st (nm, mbArgs) (SBVType [kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind sw0 <- sbvToSV st arg0 sw1 <- sbvToSV st arg1 sw2 <- sbvToSV st arg2@@ -2725,7 +2725,7 @@ result st = do isSMT <- inSMTMode st case (isSMT, uiKind) of (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10)- _ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj, kk, kl]) =<< retrieveUICode nm st ka uiKind+ _ -> do newUninterpreted st (nm, mbArgs) (SBVType [kl, kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind sw0 <- sbvToSV st arg0 sw1 <- sbvToSV st arg1 sw2 <- sbvToSV st arg2@@ -2767,7 +2767,7 @@ result st = do isSMT <- inSMTMode st case (isSMT, uiKind) of (True, UICodeC (v, _)) -> sbvToSV st (v arg0 arg1 arg2 arg3 arg4 arg5 arg6 arg7 arg8 arg9 arg10 arg11)- _ -> do newUninterpreted st (nm, mbArgs) (SBVType [kh, kg, kf, ke, kd, kc, kb, ka, ki, kj, kk, kl, km]) =<< retrieveUICode nm st ka uiKind+ _ -> do newUninterpreted st (nm, mbArgs) (SBVType [km, kl, kk, kj, ki, kh, kg, kf, ke, kd, kc, kb, ka]) =<< retrieveUICode nm st ka uiKind sw0 <- sbvToSV st arg0 sw1 <- sbvToSV st arg1 sw2 <- sbvToSV st arg2
README.md view
@@ -25,8 +25,8 @@ ## Overview - - [Hackage](http://hackage.haskell.org/package/sbv) (Version 10.5. Released: Feb 20th, 2024.)- - [Release Notes](http://github.com/LeventErkok/sbv/tree/master/CHANGES.md).+ - [Hackage](http://hackage.haskell.org/package/sbv)+ - [Release Notes](http://github.com/LeventErkok/sbv/tree/master/CHANGES.md) SBV library provides support for dealing with symbolic values in Haskell. It introduces the types:
SBVTestSuite/GoldFiles/allSat8.gold view
@@ -61,4 +61,4 @@ *** NB. If this is a use case you'd like SBV to support, please get in touch! CallStack (from HasCallStack):- error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.6-inplace:Data.SBV.Control.Utils+ error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.7-inplace:Data.SBV.Control.Utils
SBVTestSuite/GoldFiles/nested1.gold view
@@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack):- error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.6-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/nested2.gold view
@@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack):- error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.6-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/nested3.gold view
@@ -37,4 +37,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack):- error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.6-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/GoldFiles/nested4.gold view
@@ -11,4 +11,4 @@ *** See https://github.com/LeventErkok/sbv/issues/71 for several examples. CallStack (from HasCallStack):- error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.6-inplace:Data.SBV.Core.Symbolic+ error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.7-inplace:Data.SBV.Core.Symbolic
SBVTestSuite/TestSuite/Uninterpreted/Function.hs view
@@ -9,6 +9,12 @@ -- Testsuite for Documentation.SBV.Examples.Uninterpreted.Function ----------------------------------------------------------------------------- +{-# LANGUAGE DeriveAnyClass #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TemplateHaskell #-}+ {-# OPTIONS_GHC -Wall -Werror #-} module TestSuite.Uninterpreted.Function(tests) where@@ -17,8 +23,153 @@ import Utils.SBVTestFramework +data A1+mkUninterpretedSort ''A1++data A2+mkUninterpretedSort ''A2++data A3+mkUninterpretedSort ''A3++data A4+mkUninterpretedSort ''A4++data A5+mkUninterpretedSort ''A5++data A6+mkUninterpretedSort ''A6++data A7+mkUninterpretedSort ''A7++data A8+mkUninterpretedSort ''A8++data A9+mkUninterpretedSort ''A9++data A10+mkUninterpretedSort ''A10++data A11+mkUninterpretedSort ''A11++data A12+mkUninterpretedSort ''A12+++f1 :: SA1 -> SBool+f1 = uninterpret "f1"++f2 :: SA1 -> SA2 -> SBool+f2 = uninterpret "f2"++f3 :: SA1 -> SA2 -> SA3 -> SBool+f3 = uninterpret "f3"++f4 :: SA1 -> SA2 -> SA3 -> SA4 -> SBool+f4 = uninterpret "f4"++f5 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SBool+f5 = uninterpret "f5"++f6 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SBool+f6 = uninterpret "f6"++f7 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SBool+f7 = uninterpret "f7"++f8 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SBool+f8 = uninterpret "f8"++f9 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SBool+f9 = uninterpret "f9"++f10 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SBool+f10 = uninterpret "f10"++f11 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SBool+f11 = uninterpret "f11"++f12 :: SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SA12 -> SBool+f12 = uninterpret "f12"++thm1 :: SA1 -> SA1 -> SBool+thm1 x a1 =+ x .== a1+ .=> f1 x .== f1 a1++thm2 :: SA1 -> SA1 -> SA2 -> SBool+thm2 x a1 a2 =+ x .== a1+ .=> f2 x a2 .== f2 a1 a2++thm3 :: SA1 -> SA1 -> SA2 -> SA3 -> SBool+thm3 x a1 a2 a3 =+ x .== a1+ .=> f3 x a2 a3 .== f3 a1 a2 a3++thm4 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SBool+thm4 x a1 a2 a3 a4 =+ x .== a1+ .=> f4 x a2 a3 a4 .== f4 a1 a2 a3 a4++thm5 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SBool+thm5 x a1 a2 a3 a4 a5 =+ x .== a1+ .=> f5 x a2 a3 a4 a5 .== f5 a1 a2 a3 a4 a5++thm6 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SBool+thm6 x a1 a2 a3 a4 a5 a6 =+ x .== a1+ .=> f6 x a2 a3 a4 a5 a6 .== f6 a1 a2 a3 a4 a5 a6++thm7 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SBool+thm7 x a1 a2 a3 a4 a5 a6 a7 =+ x .== a1+ .=> f7 x a2 a3 a4 a5 a6 a7 .== f7 a1 a2 a3 a4 a5 a6 a7++thm8 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SBool+thm8 x a1 a2 a3 a4 a5 a6 a7 a8 =+ x .== a1+ .=> f8 x a2 a3 a4 a5 a6 a7 a8 .== f8 a1 a2 a3 a4 a5 a6 a7 a8++thm9 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SBool+thm9 x a1 a2 a3 a4 a5 a6 a7 a8 a9 =+ x .== a1+ .=> f9 x a2 a3 a4 a5 a6 a7 a8 a9 .== f9 a1 a2 a3 a4 a5 a6 a7 a8 a9++thm10 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SBool+thm10 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 =+ x .== a1+ .=> f10 x a2 a3 a4 a5 a6 a7 a8 a9 a10 .== f10 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10++thm11 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SBool+thm11 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 =+ x .== a1+ .=> f11 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 .== f11 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11++thm12 :: SA1 -> SA1 -> SA2 -> SA3 -> SA4 -> SA5 -> SA6 -> SA7 -> SA8 -> SA9 -> SA10 -> SA11 -> SA12 -> SBool+thm12 x a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 =+ x .== a1+ .=> f12 x a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 .== f12 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12+ tests :: TestTree tests = testGroup "Uninterpreted.Function" [ testCase "aufunc-0" (assertIsThm thmGood)+ , testCase "aufunc-1" (assertIsThm thm1)+ , testCase "aufunc-2" (assertIsThm thm2)+ , testCase "aufunc-3" (assertIsThm thm3)+ , testCase "aufunc-4" (assertIsThm thm4)+ , testCase "aufunc-5" (assertIsThm thm5)+ , testCase "aufunc-6" (assertIsThm thm6)+ , testCase "aufunc-7" (assertIsThm thm7)+ , testCase "aufunc-8" (assertIsThm thm8)+ , testCase "aufunc-9" (assertIsThm thm9)+ , testCase "aufunc-10" (assertIsThm thm10)+ , testCase "aufunc-11" (assertIsThm thm11)+ , testCase "aufunc-12" (assertIsThm thm12) ]
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 10.6+Version : 10.7 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