sbv 14.6 → 14.7
raw patch · 20 files changed
+186/−17 lines, 20 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- CHANGES.md +7/−0
- Data/SBV.hs +1/−1
- Data/SBV/Client.hs +8/−0
- Data/SBV/Control/Utils.hs +7/−1
- Documentation/SBV/Examples/Lists/CountOutAndTransfer.hs +1/−1
- Documentation/SBV/Examples/Puzzles/Newspaper.hs +1/−1
- README.md +2/−1
- SBVTestSuite/GoldFiles/adt00.gold +1/−0
- SBVTestSuite/GoldFiles/adt01.gold +1/−0
- SBVTestSuite/GoldFiles/adt02.gold +1/−0
- SBVTestSuite/GoldFiles/adt03.gold +1/−0
- SBVTestSuite/GoldFiles/adt04.gold +1/−0
- SBVTestSuite/GoldFiles/adt05.gold +1/−0
- SBVTestSuite/GoldFiles/adt06.gold +3/−2
- SBVTestSuite/GoldFiles/adt07.gold +44/−0
- SBVTestSuite/GoldFiles/adt08.gold +55/−0
- SBVTestSuite/TestSuite/ADT/ADT.hs +46/−5
- SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr +2/−2
- SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr +2/−2
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,6 +1,13 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> +### Version 14.7, 2026-08-31++ * Fix https://github.com/LeventErkok/sbv/issues/813. Thanks to David van Balen for reporting.++ * Add support for sets and arrays as ADT fields: A type declared via `mkSymbolic` can now+ have `RCSet` and `ArrayModel` valued constructor arguments.+ ### Version 14.6, 2026-08-18 * New TP example: Binary trees (`Documentation.SBV.Examples.TP.Tree`). Proves that mirroring
Data/SBV.hs view
@@ -125,7 +125,7 @@ -- The SBV library is designed to work with any SMT-Lib compliant SMT-solver. -- Currently, we support the following SMT-Solvers out-of-the box: ----- * ABC from University of Berkeley: <http://www.eecs.berkeley.edu/~alanmi/abc/>+-- * ABC from University of Berkeley: <https://github.com/berkeley-abc/abc> -- -- * CVC4, and CVC5 from Stanford University and the University of Iowa. <https://cvc4.github.io/> and <https://cvc5.github.io> --
Data/SBV/Client.hs view
@@ -624,6 +624,14 @@ | nm == ''Ratio && i == ''Integer = pure KRational + -- sets+ go (TH.AppT (TH.ConT nm) t)+ | nm == ''RCSet = KSet <$> go t++ -- arrays+ go (TH.AppT (TH.AppT (TH.ConT nm) t1) t2)+ | nm == ''ArrayModel = KArray <$> go t1 <*> go t2+ -- deal with base types go t@(TH.ConT constr) | Just base <- getBase constr
Data/SBV/Control/Utils.hs view
@@ -1125,9 +1125,15 @@ EApp (ECon c : cs) -> (c, cs) _ -> bad ["Unexpected expression value; does not start with a constructor."] + -- Drop the "as" annotation off the constructor, if we have one. Note that we+ -- only strip in the head position: The fields are recovered by a recursive+ -- call to 'recoverKindedValue', which deals with their own annotations. (Do+ -- not be tempted to recurse into the fields here: That would corrupt values+ -- whose annotation is load bearing, e.g., sets and arrays, which are printed+ -- using the ((as const (Array A B)) v) form.) removeAS :: SExpr -> SExpr removeAS (EApp [ECon "as", i, _]) = removeAS i- removeAS (EApp xs) = EApp $ map removeAS xs+ removeAS (EApp (f@EApp{} : as)) = EApp (removeAS f : as) removeAS ae = ae bad :: [String] -> a
Documentation/SBV/Examples/Lists/CountOutAndTransfer.hs view
@@ -7,7 +7,7 @@ -- Stability : experimental -- -- Shows that COAT (Count-out-and-transfer) trick preserves order of cards.--- From pg. 35 of <http://graphics8.nytimes.com/packages/pdf/crossword/Mulcahy_Mathematical_Card_Magic-Sample2.pdf>:+-- Quoting Colm Mulcahy's /Mathematical Card Magic: Fifty-Two New Effects/ (CRC Press, 2013): -- -- /Given a packet of n cards, COATing k cards refers to counting out that many from the top into a pile, thus reversing their order, and transferring those as a unit to the bottom./ --
Documentation/SBV/Examples/Puzzles/Newspaper.hs view
@@ -6,7 +6,7 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental ----- Solution to the following puzzle (found at <http://hugopeters.me/posts/15>)+-- Solution to the following puzzle (found at <https://hugopeters.me/posts/15>) -- which contains 10 questions: -- -- @
README.md view
@@ -155,7 +155,7 @@ | Solver | From | | Solver | From | |--------|------|-|--------|------|-| [ABC](http://www.eecs.berkeley.edu/~alanmi/abc) | Berkeley | | [DReal](http://dreal.github.io/) | CMU |+| [ABC](https://github.com/berkeley-abc/abc) | Berkeley | | [DReal](http://dreal.github.io/) | CMU | | [Bitwuzla](http://bitwuzla.github.io/) | Stanford | | [MathSAT](http://mathsat.fbk.eu/) | FBK / Trento | | [Boolector](http://boolector.github.io/) | JKU | | [OpenSMT](http://verify.inf.usi.ch/opensmt) | USI | | [CVC4](http://cvc4.github.io/) | Stanford / Iowa | | [Yices](http://github.com/SRI-CSL/yices2) | SRI |@@ -206,6 +206,7 @@ Ara Adkins, Andrew Anderson, Kanishka Azimi,+David van Balen, Markus Barenhoff, Reid Barton, Ben Blaxill,
SBVTestSuite/GoldFiles/adt00.gold view
@@ -70,6 +70,7 @@ (APair (getAPair_1 ADT) (getAPair_2 ADT)) (KChar (getKChar_1 String)) (KRational (getKRational_1 SBVRational))+ (KArray (getKArray_1 (Array Int Bool))) )) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs ---
SBVTestSuite/GoldFiles/adt01.gold view
@@ -70,6 +70,7 @@ (APair (getAPair_1 ADT) (getAPair_2 ADT)) (KChar (getKChar_1 String)) (KRational (getKRational_1 SBVRational))+ (KArray (getKArray_1 (Array Int Bool))) )) [GOOD] ; --- literal constants --- [GOOD] (define-fun s1 () ADT ((as APair ADT) ((as AInt64 ADT) #x0000000000000004) ((as AMaybe ADT) ((as Just (Maybe (SBVTuple3 Real (_ FloatingPoint 8 24) (SBVTuple2 (Either Int (_ FloatingPoint 8 24)) (Seq Bool))))) (mkSBVTuple3 0.0 (fp #b0 #b10000010 #b10000000000000000000000) (mkSBVTuple2 ((as Left (Either Int (_ FloatingPoint 8 24))) 3) (seq.++ (seq.unit false) (seq.unit true))))))))
SBVTestSuite/GoldFiles/adt02.gold view
@@ -70,6 +70,7 @@ (APair (getAPair_1 ADT) (getAPair_2 ADT)) (KChar (getKChar_1 String)) (KRational (getKRational_1 SBVRational))+ (KArray (getKArray_1 (Array Int Bool))) )) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs ---
SBVTestSuite/GoldFiles/adt03.gold view
@@ -70,6 +70,7 @@ (APair (getAPair_1 ADT) (getAPair_2 ADT)) (KChar (getKChar_1 String)) (KRational (getKRational_1 SBVRational))+ (KArray (getKArray_1 (Array Int Bool))) )) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs ---
SBVTestSuite/GoldFiles/adt04.gold view
@@ -70,6 +70,7 @@ (APair (getAPair_1 ADT) (getAPair_2 ADT)) (KChar (getKChar_1 String)) (KRational (getKRational_1 SBVRational))+ (KArray (getKArray_1 (Array Int Bool))) )) [GOOD] ; --- literal constants --- [GOOD] (define-fun s3 () Int 0)
SBVTestSuite/GoldFiles/adt05.gold view
@@ -66,6 +66,7 @@ (APair (getAPair_1 ADT) (getAPair_2 ADT)) (KChar (getKChar_1 String)) (KRational (getKRational_1 SBVRational))+ (KArray (getKArray_1 (Array Int Bool))) )) [GOOD] ; --- literal constants --- [GOOD] (define-fun s4 () (_ FloatingPoint 8 24) (fp #b0 #b10000001 #b00000000000000000000000))
SBVTestSuite/GoldFiles/adt06.gold view
@@ -70,6 +70,7 @@ (APair (getAPair_1 ADT) (getAPair_2 ADT)) (KChar (getKChar_1 String)) (KRational (getKRational_1 SBVRational))+ (KArray (getKArray_1 (Array Int Bool))) )) [GOOD] ; --- literal constants --- [GOOD] ; --- top level inputs ---@@ -95,9 +96,9 @@ [RECV] ((s0 (AMaybe (Just (mkSBVTuple3 2.0 (fp #b0 #x00 #b00000000000000000000001) (mkSBVTuple2 (Right (fp #b0 #x00 #b00000000000000000100000))- (seq.unit true)))))))+ (seq.unit false))))))) -getValue: AMaybe (Just (2.0,1.0e-45,(Right 4.5e-44,[True])))+getValue: AMaybe (Just (2.0,1.0e-45,(Right 4.5e-44,[False]))) DONE *** Solver : Z3 *** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/adt07.gold view
@@ -0,0 +1,44 @@+** 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] ; --- ADTs --- +[GOOD] ; User defined ADT: Either+[GOOD] (declare-datatype Either (par (a b) (+ (Left (getLeft_1 a))+ (Right (getRight_1 b))+ )))+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s1 () (Either Int (SBVTuple2 Int (Array Int Bool))) ((as Right (Either Int (SBVTuple2 Int (Array Int Bool)))) (mkSBVTuple2 4 (store ((as const (Array Int Bool)) false) 2 true))))+[GOOD] ; --- top level inputs ---+[GOOD] (declare-fun s0 () (Either Int (SBVTuple2 Int (Array Int Bool)))) ; tracks user variable "a"+[GOOD] ; --- constant tables ---+[GOOD] ; --- non-constant tables ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user defined functions ---+[GOOD] ; --- assignments ---+[GOOD] (define-fun s2 () Bool (= s0 s1))+[GOOD] ; --- delayedEqualities ---+[GOOD] ; --- formula ---+[GOOD] (assert s2)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (Right (mkSBVTuple2 4 (store ((as const (Array Int Bool)) false) 2 true)))))++getValue: Right (4,{2})+DONE+*** Solver : Z3+*** Exit code: ExitSuccess
+ SBVTestSuite/GoldFiles/adt08.gold view
@@ -0,0 +1,55 @@+** 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] ; --- sums ---+[GOOD] ; --- ADTs --- +[GOOD] ; User defined ADT: Probe+[GOOD] (declare-datatype Probe (+ (PSet (getPSet_1 (Array Int Bool)))+ (PArr (getPArr_1 (Array Int Bool)))+ (PInt (getPInt_1 Int))+ ))+[GOOD] ; --- literal constants ---+[GOOD] (define-fun s4 () (Array Int Bool) (store ((as const (Array Int Bool)) false) 2 true))+[GOOD] (define-fun s9 () Int 3)+[GOOD] ; --- top level inputs ---+[GOOD] (declare-fun s0 () Probe) ; tracks user variable "a"+[GOOD] (declare-fun s1 () Probe) ; tracks user variable "b"+[GOOD] ; --- constant tables ---+[GOOD] ; --- non-constant tables ---+[GOOD] ; --- uninterpreted constants ---+[GOOD] ; --- user defined functions ---+[GOOD] ; --- assignments ---+[GOOD] (define-fun s2 () Bool ((as is-PSet Bool) s0))+[GOOD] (define-fun s3 () (Array Int Bool) (getPSet_1 s0))+[GOOD] (define-fun s5 () Bool (= s3 s4))+[GOOD] (define-fun s6 () Bool (and s2 s5))+[GOOD] (define-fun s7 () Bool ((as is-PArr Bool) s1))+[GOOD] (define-fun s8 () (Array Int Bool) (getPArr_1 s1))+[GOOD] (define-fun s10 () Bool (select s8 s9))+[GOOD] (define-fun s11 () Bool (and s7 s10))+[GOOD] ; --- delayedEqualities ---+[GOOD] ; --- formula ---+[GOOD] (assert s6)+[GOOD] (assert s11)+[SEND] (check-sat)+[RECV] sat+[SEND] (get-value (s0))+[RECV] ((s0 (PSet (store ((as const (Array Int Bool)) false) 2 true))))+[SEND] (get-value (s1))+[RECV] ((s1 (PArr ((as const (Array Int Bool)) true))))++getValue a: PSet {2}+getValue b: PArr (ArrayModel [] True)+DONE+*** Solver : Z3+*** Exit code: ExitSuccess
SBVTestSuite/TestSuite/ADT/ADT.hs view
@@ -22,6 +22,9 @@ import Utils.SBVTestFramework import Data.SBV.Control import Data.SBV.Maybe+import Data.SBV.Either (sRight)+import Data.SBV.Set (insert, empty)+import Data.SBV.Tuple (tuple) data ADT = AEmpty | ABool Bool@@ -52,15 +55,22 @@ | APair ADT ADT | KChar Char | KRational Rational- {-- | KADT String (Maybe [(String, [Kind])])- | KSet Kind- | KArray Kind Kind- -}+ | KArray (ArrayModel Integer Bool)+ -- NB. KADT is covered by the APair constructor above. KSet is deliberately+ -- absent: t05 has to run on cvc5 (z3 is buggy on it), and cvc5 doesn't+ -- support sets; a single set field here would make every test over this+ -- type require set support. Sets in ADT fields are covered by t08 instead. deriving Show mkSymbolic [''ADT] +data Probe = PSet (RCSet Integer)+ | PArr (ArrayModel Integer Bool)+ | PInt Integer+ deriving Show++mkSymbolic [''Probe]+ tests :: TestTree tests = testGroup "ADT" [@@ -71,6 +81,8 @@ , goldenCapturedIO "adt04" t04 , goldenCapturedIO "adt05" t05 , goldenCapturedIO "adt06" t06+ , goldenCapturedIO "adt07" t07+ , goldenCapturedIO "adt08" t08 ] checkWith :: Symbolic () -> FilePath -> IO ()@@ -127,5 +139,34 @@ case cs of Sat{} -> do v <- getValue a io $ do appendFile rf $ "\ngetValue: " ++ show v+ appendFile rf "\nDONE\n"+ _ -> error ("BAD RESULT: " ++ show cs)++-- Sets (and arrays) nested inside an ADT field: The model parser used to strip the+-- (as const (Array Int Bool)) annotation off the field while looking for the constructor,+-- which made the set unparseable. See interpretADT/removeAS in Data.SBV.Control.Utils.+t07 :: FilePath -> IO ()+t07 rf = runSMTWith z3{verbose=True, redirectVerbose = Just rf} $ do+ a :: SEither Integer (Integer, RCSet Integer) <- free "a"+ constrain $ a .== sRight (tuple (4, insert 2 empty))+ query $ do cs <- checkSat+ case cs of+ Sat{} -> do v <- getValue a+ io $ do appendFile rf $ "\ngetValue: " ++ show v+ appendFile rf "\nDONE\n"+ _ -> error ("BAD RESULT: " ++ show cs)++t08 :: FilePath -> IO ()+t08 rf = runSMTWith z3{verbose=True, redirectVerbose = Just rf} $ do+ a :: SProbe <- free "a"+ b :: SProbe <- free "b"+ constrain $ isPSet a .&& getPSet_1 a .== insert 2 empty+ constrain $ isPArr b .&& readArray (getPArr_1 b) 3 .== sTrue+ query $ do cs <- checkSat+ case cs of+ Sat{} -> do va <- getValue a+ vb <- getValue b+ io $ do appendFile rf $ "\ngetValue a: " ++ show va+ appendFile rf $ "\ngetValue b: " ++ show vb appendFile rf "\nDONE\n" _ -> error ("BAD RESULT: " ++ show cs)
SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr view
@@ -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.6:Data.SBV.TP.TP.TPProofGen- (SBV Bool) [sbv-14.6:Data.SBV.TP.TP.Helper] ()+ with actual type: sbv-14.7:Data.SBV.TP.TP.TPProofGen+ (SBV Bool) [sbv-14.7:Data.SBV.TP.TP.Helper] () " In the expression: cases [(isZero e ==> (e .== e =: qed)), (isNum e ==> (e .== e =: qed)),
SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr view
@@ -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.6:Data.SBV.TP.TP.TPProofGen- a0 [sbv-14.6:Data.SBV.TP.TP.Helper] ()+ with actual type: sbv-14.7:Data.SBV.TP.TP.TPProofGen+ a0 [sbv-14.7:Data.SBV.TP.TP.Helper] () " In the expression: cases [(isZero e ==> undefined), (isNum e ==> undefined),
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 14.6+Version : 14.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