diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,16 @@ * Hackage: * GitHub: -### 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, diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -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 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 @@ -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 diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs --- a/Data/SBV/Core/Symbolic.hs +++ b/Data/SBV/Core/Symbolic.hs @@ -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" diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -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) ++ ")" diff --git a/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs --- a/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs +++ b/Documentation/SBV/Examples/Puzzles/HexPuzzle.hs @@ -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 [] diff --git a/Documentation/SBV/Examples/TP/Primes.hs b/Documentation/SBV/Examples/TP/Primes.hs --- a/Documentation/SBV/Examples/TP/Primes.hs +++ b/Documentation/SBV/Examples/TP/Primes.hs @@ -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" -} diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -231,6 +231,7 @@ May Torrence, Daniel Wagner, Sean Weaver, +Robin Webbers, Eddy Westbrook, Nis Wegmann, Jared Ziegler, diff --git a/SBVTestSuite/GoldFiles/array_caching_01.gold b/SBVTestSuite/GoldFiles/array_caching_01.gold --- a/SBVTestSuite/GoldFiles/array_caching_01.gold +++ b/SBVTestSuite/GoldFiles/array_caching_01.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/array_caching_02.gold b/SBVTestSuite/GoldFiles/array_caching_02.gold --- a/SBVTestSuite/GoldFiles/array_caching_02.gold +++ b/SBVTestSuite/GoldFiles/array_caching_02.gold @@ -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)) diff --git a/SBVTestSuite/GoldFiles/freshVars.gold b/SBVTestSuite/GoldFiles/freshVars.gold --- a/SBVTestSuite/GoldFiles/freshVars.gold +++ b/SBVTestSuite/GoldFiles/freshVars.gold @@ -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)) diff --git a/SBVTestSuite/TestSuite/Arrays/Caching.hs b/SBVTestSuite/TestSuite/Arrays/Caching.hs --- a/SBVTestSuite/TestSuite/Arrays/Caching.hs +++ b/SBVTestSuite/TestSuite/Arrays/Caching.hs @@ -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" diff --git a/SBVTestSuite/TestSuite/Arrays/InitVals.hs b/SBVTestSuite/TestSuite/Arrays/InitVals.hs --- a/SBVTestSuite/TestSuite/Arrays/InitVals.hs +++ b/SBVTestSuite/TestSuite/Arrays/InitVals.hs @@ -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 diff --git a/SBVTestSuite/TestSuite/Queries/FreshVars.hs b/SBVTestSuite/TestSuite/Queries/FreshVars.hs --- a/SBVTestSuite/TestSuite/Queries/FreshVars.hs +++ b/SBVTestSuite/TestSuite/Queries/FreshVars.hs @@ -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 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 : 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