diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,6 +1,13 @@ * Hackage: * GitHub: +### 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 diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -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: +-- * ABC from University of Berkeley: -- -- * CVC4, and CVC5 from Stanford University and the University of Iowa. and -- diff --git a/Data/SBV/Client.hs b/Data/SBV/Client.hs --- a/Data/SBV/Client.hs +++ b/Data/SBV/Client.hs @@ -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 diff --git a/Data/SBV/Control/Utils.hs b/Data/SBV/Control/Utils.hs --- a/Data/SBV/Control/Utils.hs +++ b/Data/SBV/Control/Utils.hs @@ -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 diff --git a/Documentation/SBV/Examples/Lists/CountOutAndTransfer.hs b/Documentation/SBV/Examples/Lists/CountOutAndTransfer.hs --- a/Documentation/SBV/Examples/Lists/CountOutAndTransfer.hs +++ b/Documentation/SBV/Examples/Lists/CountOutAndTransfer.hs @@ -7,7 +7,7 @@ -- Stability : experimental -- -- Shows that COAT (Count-out-and-transfer) trick preserves order of cards. --- From pg. 35 of : +-- 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./ -- diff --git a/Documentation/SBV/Examples/Puzzles/Newspaper.hs b/Documentation/SBV/Examples/Puzzles/Newspaper.hs --- a/Documentation/SBV/Examples/Puzzles/Newspaper.hs +++ b/Documentation/SBV/Examples/Puzzles/Newspaper.hs @@ -6,7 +6,7 @@ -- Maintainer: erkokl@gmail.com -- Stability : experimental -- --- Solution to the following puzzle (found at ) +-- Solution to the following puzzle (found at ) -- which contains 10 questions: -- -- @ diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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, diff --git a/SBVTestSuite/GoldFiles/adt00.gold b/SBVTestSuite/GoldFiles/adt00.gold --- a/SBVTestSuite/GoldFiles/adt00.gold +++ b/SBVTestSuite/GoldFiles/adt00.gold @@ -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 --- diff --git a/SBVTestSuite/GoldFiles/adt01.gold b/SBVTestSuite/GoldFiles/adt01.gold --- a/SBVTestSuite/GoldFiles/adt01.gold +++ b/SBVTestSuite/GoldFiles/adt01.gold @@ -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)))))))) diff --git a/SBVTestSuite/GoldFiles/adt02.gold b/SBVTestSuite/GoldFiles/adt02.gold --- a/SBVTestSuite/GoldFiles/adt02.gold +++ b/SBVTestSuite/GoldFiles/adt02.gold @@ -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 --- diff --git a/SBVTestSuite/GoldFiles/adt03.gold b/SBVTestSuite/GoldFiles/adt03.gold --- a/SBVTestSuite/GoldFiles/adt03.gold +++ b/SBVTestSuite/GoldFiles/adt03.gold @@ -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 --- diff --git a/SBVTestSuite/GoldFiles/adt04.gold b/SBVTestSuite/GoldFiles/adt04.gold --- a/SBVTestSuite/GoldFiles/adt04.gold +++ b/SBVTestSuite/GoldFiles/adt04.gold @@ -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) diff --git a/SBVTestSuite/GoldFiles/adt05.gold b/SBVTestSuite/GoldFiles/adt05.gold --- a/SBVTestSuite/GoldFiles/adt05.gold +++ b/SBVTestSuite/GoldFiles/adt05.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/adt06.gold b/SBVTestSuite/GoldFiles/adt06.gold --- a/SBVTestSuite/GoldFiles/adt06.gold +++ b/SBVTestSuite/GoldFiles/adt06.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/adt07.gold b/SBVTestSuite/GoldFiles/adt07.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/adt07.gold @@ -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 diff --git a/SBVTestSuite/GoldFiles/adt08.gold b/SBVTestSuite/GoldFiles/adt08.gold new file mode 100644 --- /dev/null +++ b/SBVTestSuite/GoldFiles/adt08.gold @@ -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 diff --git a/SBVTestSuite/TestSuite/ADT/ADT.hs b/SBVTestSuite/TestSuite/ADT/ADT.hs --- a/SBVTestSuite/TestSuite/ADT/ADT.hs +++ b/SBVTestSuite/TestSuite/ADT/ADT.hs @@ -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) 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.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)), 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.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), 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.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