sbv 13.2 → 13.3
raw patch · 15 files changed
+117/−88 lines, 15 files
Files
- CHANGES.md +10/−1
- Data/SBV.hs +1/−1
- Data/SBV/Core/Model.hs +22/−4
- Data/SBV/Core/Symbolic.hs +8/−4
- Data/SBV/SMT/SMTLib2.hs +4/−3
- Documentation/SBV/Examples/Puzzles/HexPuzzle.hs +1/−1
- Documentation/SBV/Examples/TP/Primes.hs +14/−9
- README.md +1/−0
- SBVTestSuite/GoldFiles/array_caching_01.gold +10/−13
- SBVTestSuite/GoldFiles/array_caching_02.gold +11/−14
- SBVTestSuite/GoldFiles/freshVars.gold +31/−34
- SBVTestSuite/TestSuite/Arrays/Caching.hs +1/−1
- SBVTestSuite/TestSuite/Arrays/InitVals.hs +1/−1
- SBVTestSuite/TestSuite/Queries/FreshVars.hs +1/−1
- sbv.cabal +1/−1
CHANGES.md view
@@ -1,7 +1,16 @@ * Hackage: <http://hackage.haskell.org/package/sbv> * GitHub: <http://github.com/LeventErkok/sbv> -### Version 13.2, 2025-12-01+### Version 13.3, 2025-12-05++ * Added 'constArray', which allows creation of constant valued symbolic arrays. The definition+ is semantically equivalent to 'lambdaArray . const', but we generate simpler SMTLib code+ for it. For the general case of initializing an array with arbitrary functions, continue+ using 'lambdaArray'. Thanks to Robin Webbers for the patch.++ * Improved the infinite-number-of-primes theorem statement slightly.++### Version 13.2, 2025-12-02 * Improve support for SMTDefinable class, allowing support for on-the-fly generated functions. Thanks to Eddy Westbrook for the patch. This should have no impact on existing code or usage,
Data/SBV.hs view
@@ -249,7 +249,7 @@ -- ** Sets , RCSet(..), SSet -- * Arrays of symbolic values- , SArray, sArray, sArray_, sArrays, readArray, writeArray, lambdaArray, listArray, ArrayModel+ , SArray, sArray, sArray_, sArrays, readArray, writeArray, lambdaArray, constArray, listArray, ArrayModel -- * Creating symbolic values -- ** Single value
Data/SBV/Core/Model.hs view
@@ -57,7 +57,7 @@ , genLiteral, genFromCV, genMkSymVar , zeroExtend, signExtend , sbvQuickCheck- , readArray, writeArray, lambdaArray, listArray+ , readArray, writeArray, constArray, lambdaArray, listArray , FromSized, ToSized, FromSizedBV(..), ToSizedBV(..) , smtHOFunction, Closure(..) )@@ -982,7 +982,7 @@ r st = do let incr x table = ite (x `sElem` ignored) (0 :: SInteger) (1 + readArrayNoEq table x) initArray :: SArray a Integer- initArray = lambdaArray (const 0)+ initArray = constArray 0 finalArray = foldl (\table x -> writeArrayNoKnd table x (incr x table)) initArray es @@ -3251,13 +3251,31 @@ val <- sbvToSV st value newExpr st k (SBVApp WriteArray [arr, keyVal, val]) --- | Using a lambda as an array.+-- | Create a constant array. This is a special case of 'lambdaArray', but it creates a+-- simpler expression in the case of constants.+constArray :: forall key val. (SymVal key, SymVal val) => SBV val -> SArray key val+constArray v+ | Just v' <- unliteral v+ = literal $ ArrayModel [] v'+ | True+ = SBV . SVal k . Right $ cache g+ where ka = kindOf (Proxy @key)+ kb = kindOf (Proxy @val)+ k = KArray ka kb++ g st = do sv <- sbvToSV st v+ newExpr st k (SBVApp (ArrayInit (Left (ka, kb))) [sv])++-- | Using a lambda as an array. We can turn a function into an array, relating indexes+-- to their values. (That is, passing @f@ would create an array where entry @i@+-- is initialized to value @f i@.) For the special case of initializing with a constant+-- value, either pass @const val@, or use 'constArray'. lambdaArray :: forall a b. (SymVal a, HasKind b) => (SBV a -> SBV b) -> SArray a b lambdaArray f = SBV . SVal k . Right $ cache g where k = KArray (kindOf (Proxy @a)) (kindOf (Proxy @b)) g st = do def <- lambdaStr st TopLevel (kindOf (Proxy @b)) f- newExpr st k (SBVApp (ArrayLambda def) [])+ newExpr st k (SBVApp (ArrayInit (Right def)) []) -- | Turn a constant association-list and a default into a symbolic array. listArray :: (SymVal a, SymVal b) => [(a, b)] -> b -> SArray a b
Data/SBV/Core/Symbolic.hs view
@@ -246,9 +246,11 @@ | TupleAccess Int Int -- Access element i of an n-tuple; second argument is n | RationalConstructor -- Construct a rational. Note that there's no access to numerator or denumerator, since we cannot store rationals in canonical form | ADTOp ADTOp -- ADT access/construction/testing- | ArrayLambda SMTLambda -- An array value, created from a lambda- | ReadArray -- Reading an array value- | WriteArray -- Writing to an array++ -- Arrays+ | ArrayInit (Either (Kind, Kind) SMTLambda) -- An array value, created either from a lambda or a symbolic value. Kind is the+ | ReadArray -- Reading an array value+ | WriteArray -- Writing to an array deriving (Eq, Ord, Generic, G.Data, NFData) -- | ADT operations@@ -604,7 +606,9 @@ show (TupleAccess i n) = "proj_" ++ show i ++ "_SBVTuple" ++ show n show RationalConstructor = "SBV.Rational"- show (ArrayLambda s) = show s+ show (ArrayInit k) = case k of+ Left (a, b) -> "const-array[" ++ show a ++ " -> " ++ show b ++ "]"+ Right s -> show s show ReadArray = "select" show WriteArray = "store"
Data/SBV/SMT/SMTLib2.hs view
@@ -838,9 +838,10 @@ sh (SBVApp (KindCast f t) [a]) = handleKindCast f t (cvtSV a) - sh (SBVApp (ArrayLambda s) []) = show s- sh (SBVApp ReadArray [a, i]) = "(select " ++ cvtSV a ++ " " ++ cvtSV i ++ ")"- sh (SBVApp WriteArray [a, i, e]) = "(store " ++ cvtSV a ++ " " ++ cvtSV i ++ " " ++ cvtSV e ++ ")"+ sh (SBVApp (ArrayInit (Left (f, t))) [a]) = "((as const (Array " ++ smtType f ++ " " ++ smtType t ++ ")) " ++ cvtSV a ++ ")"+ sh (SBVApp (ArrayInit (Right s)) []) = show s+ sh (SBVApp ReadArray [a, i]) = "(select " ++ cvtSV a ++ " " ++ cvtSV i ++ ")"+ sh (SBVApp WriteArray [a, i, e]) = "(store " ++ cvtSV a ++ " " ++ cvtSV i ++ " " ++ cvtSV e ++ ")" sh (SBVApp (Uninterpreted nm) []) = nm sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm ++ " " ++ unwords (map cvtSV args) ++ ")"
Documentation/SBV/Examples/Puzzles/HexPuzzle.hs view
@@ -84,7 +84,7 @@ -- transform from the initial board position to a final board position. search :: [Color] -> [Color] -> IO () search initial final = runSMT $ do registerType (Proxy @SColor)- let emptyGrid = lambdaArray (const sBlack)+ let emptyGrid = constArray sBlack initGrid = foldr (\(i, c) a -> writeArray a (literal i) (literal c)) emptyGrid (zip [1..] initial) query $ loop (0 :: Int) initGrid []
Documentation/SBV/Examples/TP/Primes.hs view
@@ -468,20 +468,25 @@ -- === __Proof__ -- >>> runTP noLargestPrime -- Lemma: infinitudeOfPrimes Q.E.D.--- Lemma: noLargestPrime+-- Lemma: helper -- Step: 1 Q.E.D. -- Result: Q.E.D.--- [Proven] noLargestPrime :: Ɐn ∷ Integer → Bool-noLargestPrime :: TP (Proof (Forall "n" Integer -> SBool))+-- Lemma: noLargestPrime Q.E.D.+-- [Proven] noLargestPrime :: Ɐn ∷ Integer → ∃p ∷ Integer → Bool+noLargestPrime :: TP (Proof (Forall "n" Integer -> Exists "p" Integer -> SBool)) noLargestPrime = do iop <- recall "infinitudeOfPrimes" infinitudeOfPrimes - calc "noLargestPrime"- (\(Forall n) -> quantifiedBool (\(Exists p) -> isPrime p .&& p .> n)) $- \n -> [] |- quantifiedBool (\(Exists p) -> isPrime p .&& p .> n)- ?? iop `at` Inst @"n" n- =: sTrue- =: qed+ h <- calc "helper"+ (\(Forall @"n" n) -> quantifiedBool (\(Exists p) -> isPrime p .&& p .> n)) $+ \n -> [] |- quantifiedBool (\(Exists p) -> isPrime p .&& p .> n)+ ?? iop `at` Inst @"n" n+ =: sTrue+ =: qed++ lemmaWith cvc5 "noLargestPrime"+ (\(Forall n) (Exists p) -> isPrime p .&& p .> n)+ [proofOf h] {- HLint ignore module "Avoid lambda" -} {- HLint ignore module "Eta reduce" -}
README.md view
@@ -231,6 +231,7 @@ May Torrence, Daniel Wagner, Sean Weaver,+Robin Webbers, Eddy Westbrook, Nis Wegmann, Jared Ziegler,
SBVTestSuite/GoldFiles/array_caching_01.gold view
@@ -13,8 +13,8 @@ [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s1 () Int 0)-[GOOD] (define-fun s4 () Int 2)-[GOOD] (define-fun s6 () Int 1)+[GOOD] (define-fun s3 () (Array Int Int) (store ((as const (Array Int Int)) 0) 0 2))+[GOOD] (define-fun s4 () Int 1) [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "x" [GOOD] ; --- constant tables ---@@ -23,20 +23,17 @@ [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- [GOOD] (define-fun s2 () Bool (= s0 s1))-[GOOD] (define-fun s3 () (Array Int Int) (lambda ((l1_s0 Int))- 0))-[GOOD] (define-fun s5 () (Array Int Int) (store s3 s1 s4))-[GOOD] (define-fun s7 () Int (+ s0 s6))-[GOOD] (define-fun s8 () Int (select s5 s7))-[GOOD] (define-fun s9 () (Array Int Int) (store s5 s1 s8))+[GOOD] (define-fun s5 () Int (+ s0 s4))+[GOOD] (define-fun s6 () Int (select s3 s5))+[GOOD] (define-fun s7 () (Array Int Int) (store s3 s1 s6))+[GOOD] (define-fun s8 () Int (select s7 s1))+[GOOD] (define-fun s9 () (Array Int Int) (store s3 s5 s4)) [GOOD] (define-fun s10 () Int (select s9 s1))-[GOOD] (define-fun s11 () (Array Int Int) (store s5 s7 s6))-[GOOD] (define-fun s12 () Int (select s11 s1))-[GOOD] (define-fun s13 () Int (ite s2 s10 s12))-[GOOD] (define-fun s14 () Bool (= s6 s13))+[GOOD] (define-fun s11 () Int (ite s2 s8 s10))+[GOOD] (define-fun s12 () Bool (= s4 s11)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula ----[GOOD] (assert s14)+[GOOD] (assert s12) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))
SBVTestSuite/GoldFiles/array_caching_02.gold view
@@ -13,8 +13,8 @@ [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s1 () Int 0)-[GOOD] (define-fun s4 () Int 2)-[GOOD] (define-fun s6 () Int 1)+[GOOD] (define-fun s3 () (Array Int Int) (store ((as const (Array Int Int)) 0) 0 2))+[GOOD] (define-fun s4 () Int 1) [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () Int) ; tracks user variable "x" [GOOD] ; --- constant tables ---@@ -23,20 +23,17 @@ [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- [GOOD] (define-fun s2 () Bool (distinct s0 s1))-[GOOD] (define-fun s3 () (Array Int Int) (lambda ((l1_s0 Int))- 0))-[GOOD] (define-fun s5 () (Array Int Int) (store s3 s1 s4))-[GOOD] (define-fun s7 () Int (+ s0 s6))-[GOOD] (define-fun s8 () (Array Int Int) (store s5 s7 s6))-[GOOD] (define-fun s9 () Int (select s8 s1))-[GOOD] (define-fun s10 () Int (select s5 s7))-[GOOD] (define-fun s11 () (Array Int Int) (store s5 s1 s10))-[GOOD] (define-fun s12 () Int (select s11 s1))-[GOOD] (define-fun s13 () Int (ite s2 s9 s12))-[GOOD] (define-fun s14 () Bool (= s6 s13))+[GOOD] (define-fun s5 () Int (+ s0 s4))+[GOOD] (define-fun s6 () (Array Int Int) (store s3 s5 s4))+[GOOD] (define-fun s7 () Int (select s6 s1))+[GOOD] (define-fun s8 () Int (select s3 s5))+[GOOD] (define-fun s9 () (Array Int Int) (store s3 s1 s8))+[GOOD] (define-fun s10 () Int (select s9 s1))+[GOOD] (define-fun s11 () Int (ite s2 s7 s10))+[GOOD] (define-fun s12 () Bool (= s4 s11)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula ----[GOOD] (assert s14)+[GOOD] (assert s12) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))
SBVTestSuite/GoldFiles/freshVars.gold view
@@ -103,49 +103,46 @@ [GOOD] (define-fun s54 () Bool (= s52 s53)) [GOOD] (assert s54) [GOOD] (declare-fun s55 () Int)-[GOOD] (define-fun s57 () Int 96)-[GOOD] (define-fun s56 () (Array Int Int) (lambda ((l1_s0 Int))- 42))-[GOOD] (define-fun s58 () Int (select s56 s57))-[GOOD] (define-fun s59 () Bool (= s55 s58))+[GOOD] (define-fun s56 () Int 42)+[GOOD] (define-fun s57 () Bool (= s55 s56))+[GOOD] (assert s57)+[GOOD] (define-fun s58 () Int 1)+[GOOD] (define-fun s59 () Bool (= s50 s58)) [GOOD] (assert s59)-[GOOD] (define-fun s60 () Int 1)-[GOOD] (define-fun s61 () Bool (= s50 s60))-[GOOD] (assert s61)-[GOOD] (define-fun s62 () Bool (not s51))-[GOOD] (assert s62)-[GOOD] (declare-fun s63 () String)+[GOOD] (define-fun s60 () Bool (not s51))+[GOOD] (assert s60)+[GOOD] (declare-fun s61 () String) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true )-[GOOD] (declare-fun s64 () (Seq Int))+[GOOD] (declare-fun s62 () (Seq Int)) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true )-[GOOD] (declare-fun s65 () (Seq (Seq Int)))+[GOOD] (declare-fun s63 () (Seq (Seq Int))) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true )-[GOOD] (declare-fun s66 () (Seq (_ BitVec 8)))+[GOOD] (declare-fun s64 () (Seq (_ BitVec 8))) [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true )-[GOOD] (declare-fun s67 () (Seq (Seq (_ BitVec 16))))-[GOOD] (define-fun s68 () String "hello")-[GOOD] (define-fun s69 () Bool (= s63 s68))+[GOOD] (declare-fun s65 () (Seq (Seq (_ BitVec 16))))+[GOOD] (define-fun s66 () String "hello")+[GOOD] (define-fun s67 () Bool (= s61 s66))+[GOOD] (assert s67)+[GOOD] (define-fun s68 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4)))+[GOOD] (define-fun s69 () Bool (= s62 s68)) [GOOD] (assert s69)-[GOOD] (define-fun s70 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4)))-[GOOD] (define-fun s71 () Bool (= s64 s70))+[GOOD] (define-fun s70 () (Seq (Seq Int)) (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7)))))+[GOOD] (define-fun s71 () Bool (= s63 s70)) [GOOD] (assert s71)-[GOOD] (define-fun s72 () (Seq (Seq Int)) (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3))) (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7)))))-[GOOD] (define-fun s73 () Bool (= s65 s72))+[GOOD] (define-fun s72 () (Seq (_ BitVec 8)) (seq.++ (seq.unit #x01) (seq.unit #x02)))+[GOOD] (define-fun s73 () Bool (= s64 s72)) [GOOD] (assert s73)-[GOOD] (define-fun s74 () (Seq (_ BitVec 8)) (seq.++ (seq.unit #x01) (seq.unit #x02)))-[GOOD] (define-fun s75 () Bool (= s66 s74))+[GOOD] (define-fun s74 () (Seq (Seq (_ BitVec 16))) (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) (seq.unit (as seq.empty (Seq (_ BitVec 16)))) (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006)))))+[GOOD] (define-fun s75 () Bool (= s65 s74)) [GOOD] (assert s75)-[GOOD] (define-fun s76 () (Seq (Seq (_ BitVec 16))) (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) (seq.unit (as seq.empty (Seq (_ BitVec 16)))) (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006)))))-[GOOD] (define-fun s77 () Bool (= s67 s76))-[GOOD] (assert s77) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s0))@@ -191,17 +188,17 @@ [RECV] ((s51 false)) [SEND] (get-value (s55)) [RECV] ((s55 42))+[SEND] (get-value (s61))+[RECV] ((s61 "hello"))+[SEND] (get-value (s62))+[RECV] ((s62 (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4)))) [SEND] (get-value (s63))-[RECV] ((s63 "hello"))+[RECV] ((s63 (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))+ (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7)))))) [SEND] (get-value (s64))-[RECV] ((s64 (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4))))+[RECV] ((s64 (seq.++ (seq.unit #x01) (seq.unit #x02)))) [SEND] (get-value (s65))-[RECV] ((s65 (seq.++ (seq.unit (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3)))- (seq.unit (seq.++ (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7))))))-[SEND] (get-value (s66))-[RECV] ((s66 (seq.++ (seq.unit #x01) (seq.unit #x02))))-[SEND] (get-value (s67))-[RECV] ((s67 (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003)))+[RECV] ((s65 (seq.++ (seq.unit (seq.++ (seq.unit #x0001) (seq.unit #x0002) (seq.unit #x0003))) (seq.unit (as seq.empty (Seq (_ BitVec 16)))) (seq.unit (seq.++ (seq.unit #x0004) (seq.unit #x0005) (seq.unit #x0006)))))) [SEND] (get-value (s17))
SBVTestSuite/TestSuite/Arrays/Caching.hs view
@@ -29,7 +29,7 @@ test :: Bool -> Symbolic SBool test swap = do let arr :: SArray Integer Integer- arr = lambdaArray (const 0)+ arr = constArray 0 x <- sInteger "x"
SBVTestSuite/TestSuite/Arrays/InitVals.hs view
@@ -24,7 +24,7 @@ readDef = do c :: SInteger <- free "c" i :: SInteger <- free "i" j <- free "j"- let a = lambdaArray (const c)+ let a = constArray c let a' = writeArray a j 32
SBVTestSuite/TestSuite/Queries/FreshVars.hs view
@@ -88,7 +88,7 @@ constrain $ readArray vSArray vi1 .== 2 let viSArray :: SArray Integer Integer- viSArray = lambdaArray (const 42)+ viSArray = constArray 42 mustBe42 <- freshVar "mustBe42" constrain $ readArray viSArray 96 .== mustBe42
sbv.cabal view
@@ -1,7 +1,7 @@ Cabal-Version: 2.2 Name : sbv-Version : 13.2+Version : 13.3 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