diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,8 +1,10 @@ * Hackage: * GitHub: -* 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 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 @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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: diff --git a/SBVTestSuite/GoldFiles/allSat8.gold b/SBVTestSuite/GoldFiles/allSat8.gold --- a/SBVTestSuite/GoldFiles/allSat8.gold +++ b/SBVTestSuite/GoldFiles/allSat8.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/nested1.gold b/SBVTestSuite/GoldFiles/nested1.gold --- a/SBVTestSuite/GoldFiles/nested1.gold +++ b/SBVTestSuite/GoldFiles/nested1.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/nested2.gold b/SBVTestSuite/GoldFiles/nested2.gold --- a/SBVTestSuite/GoldFiles/nested2.gold +++ b/SBVTestSuite/GoldFiles/nested2.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/nested3.gold b/SBVTestSuite/GoldFiles/nested3.gold --- a/SBVTestSuite/GoldFiles/nested3.gold +++ b/SBVTestSuite/GoldFiles/nested3.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/nested4.gold b/SBVTestSuite/GoldFiles/nested4.gold --- a/SBVTestSuite/GoldFiles/nested4.gold +++ b/SBVTestSuite/GoldFiles/nested4.gold @@ -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 diff --git a/SBVTestSuite/TestSuite/Uninterpreted/Function.hs b/SBVTestSuite/TestSuite/Uninterpreted/Function.hs --- a/SBVTestSuite/TestSuite/Uninterpreted/Function.hs +++ b/SBVTestSuite/TestSuite/Uninterpreted/Function.hs @@ -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) ] 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 : 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