sbv 10.5 → 10.6

raw patch · 11 files changed

+332/−28 lines, 11 files

Files

• CHANGES.md +13/−2
• Data/SBV/Tools/BVOptimize.hs +123/−0
• Documentation/SBV/Examples/Puzzles/HexPuzzle.hs +1/−1
• README.md +173/−2
• SBVTestSuite/GoldFiles/allSat8.gold +1/−1
• SBVTestSuite/GoldFiles/nested1.gold +1/−1
• SBVTestSuite/GoldFiles/nested2.gold +1/−1
• SBVTestSuite/GoldFiles/nested3.gold +1/−1
• SBVTestSuite/GoldFiles/nested4.gold +1/−1
• SBVTestSuite/GoldFiles/query1.gold +14/−14
• sbv.cabal +3/−4

@@ -1,7 +1,18 @@ * Hackage: <http://hackage.haskell.org/package/sbv>-* GitHub:  <http://leventerkok.github.io/sbv/>+* GitHub:  <http://github.com/LeventErkok/sbv> -* Latest Hackage released version: 10.5, 2024-02-20+* Latest Hackage released version: 10.6, 2024-03-16++### Version 10.6, 2024-03-16++  * Added Data.SBV.Tools.BVOptimize module, which implements a custom optimizer for unsigned bit-vector+    values. See 'minBV' and 'maxBV' methods. These algorithms use the incremental solver instead of+    the optimizer engines, and they can be more performant in certain cases. (For instance, z3's+    optimization engine isn't incremental, which makes it perform poorly on certain BV-optimization+    problems.) These algorithms scan the bits from most to least significant bit, and individually+    set/unset them in an incremental fashion to optimize quickly.++  * SBV web-page is no longer maintained. The info is put into the README.md instead.  ### Version 10.5, 2024-02-20 

@@ -0,0 +1,123 @@+-----------------------------------------------------------------------------+-- |+-- Module    : Data.SBV.Tools.BVOptimize+-- Copyright : (c) Levent Erkok+-- License   : BSD3+-- Maintainer: erkokl@gmail.com+-- Stability : experimental+--+-- Bit-vector optimization based on linear scan of the bits. The optimization+-- engines are usually not incremental, and they perform poorly for optimizing+-- bit-vector values in the presence of complicated constraints. We implement+-- a simple optimizer by scanning the bits from top-to-bottom to minimize/maximize+-- unsigned bit vector quantities, using the regular (i.e., incremental) solver.+-- This can lead to better performance for this class of problems.+--+-- This implementation is based on an idea by Nikolaj Bjorner, see <https://github.com/Z3Prover/z3/issues/7156>.+-----------------------------------------------------------------------------++{-# OPTIONS_GHC -Wall -Werror #-}++module Data.SBV.Tools.BVOptimize (+            -- ** Maximizing bit-vectors+            -- $maxBVEx+              maxBV, maxBVWith+            -- ** Minimizing bit-vectors+            -- $minBVEx+            , minBV, minBVWith+          ) where++import Control.Monad++import Data.SBV+import Data.SBV.Control++-- $setup+-- >>> -- For doctest purposes only:+-- >>> :set -XDataKinds+-- >>> import Data.SBV++{- $maxBVEx++Here is a simple example of maximizing a bit-vector value:++>>> :{+runSMT $ do x :: SWord 32 <- free "x"+            constrain $ x .> 5+            constrain $ x .< 27+            maxBV False x+:}+Satisfiable. Model:+  x = 26 :: Word32+-}++-- | Maximize the value of an unsigned bit-vector value, using the default solver.+maxBV :: SFiniteBits a+      => Bool                -- ^ Do we want unsat-cores if unsatisfiable?+      -> SBV a               -- ^ Value to maximize+      -> Symbolic SatResult+maxBV = maxBVWith defaultSMTCfg++-- | Maximize the value of an unsigned bit-vector value, using the given solver.+maxBVWith :: SFiniteBits a => SMTConfig -> Bool-> SBV a -> Symbolic SatResult+maxBVWith = minMaxBV True++{- $minBVEx++Here is a simple example of minimizing a bit-vector value:++>>> :{+runSMT $ do x :: SWord 32 <- free "x"+            constrain $ x .> 5+            constrain $ x .< 27+            minBV False x+:}+Satisfiable. Model:+  x = 6 :: Word32+-}++-- | Minimize the value of an unsigned bit-vector value, using the default solver.+minBV :: SFiniteBits a+      => Bool                -- ^ Do we want unsat-cores if unsatisfiable?+      -> SBV a               -- ^ Value to minimize+      -> Symbolic SatResult+minBV = minBVWith defaultSMTCfg++-- | Minimize the value of an unsigned bit-vector value, using the given solver.+minBVWith :: SFiniteBits a => SMTConfig -> Bool-> SBV a -> Symbolic SatResult+minBVWith = minMaxBV False++-- | min/max a given unsigned bit-vector. We walk down the bits in an incremental+-- fashion. If we are maximizing, we try to make the bits set as we go down, otherwise+-- we try to unset them. We keep adding the constraints so long as they are satisfiable,+-- and at the end, get the optimal value produced.+minMaxBV :: SFiniteBits a => Bool -> SMTConfig -> Bool -> SBV a -> Symbolic SatResult+minMaxBV isMax cfg getUC v+ | hasSign v+ = error $ "minMaxBV works on unsigned bitvectors, received: " ++ show (kindOf v)+ | True+ = do when getUC $ setOption $ ProduceUnsatCores True +      query $ go (blastBE v)+ where uc | getUC = Just <$> getUnsatCore+          | True  = pure Nothing++       rSat   = SatResult . Satisfiable   cfg <$> getModel+       rUnk   = SatResult . Unknown       cfg <$> getUnknownReason+       rUnsat = SatResult . Unsatisfiable cfg <$> uc++       go :: [SBool] -> Query SatResult+       go []     = do r <- checkSat+                      case r of+                        Sat     -> rSat+                        Unsat   -> rUnsat+                        Unk     -> rUnk+                        DSat {} -> error "minMaxBV: Unexpected DSat result"+       go (b:bs) = do push 1+                      if isMax then constrain b+                               else constrain $ sNot b+                      r <- checkSat+                      case r of+                        Sat    -> go bs >>= \res -> pop 1 >> return res+                        Unsat  ->                   pop 1 >> go bs+                        Unk    ->                   pop 1 >> rUnk+                        DSat{} -> error "minMaxBV: Unexpected DSat result"

@@ -130,8 +130,8 @@ -- Searching at depth: 4 -- Searching at depth: 5 -- Searching at depth: 6--- Found: [10,10,9,11,14,6] -- Found: [10,10,11,9,14,6]+-- Found: [10,10,9,11,14,6] -- There are no more solutions. example :: IO () example = search initBoard finalBoard

@@ -1,7 +1,178 @@-## SBV: SMT Based Verification in Haskell+# SBV: SMT Based Verification in Haskell  [![Build Status](https://github.com/LeventErkok/sbv/actions/workflows/haskell-ci.yml/badge.svg)](https://github.com/LeventErkok/sbv/actions/workflows/haskell-ci.yml)  On Hackage: http://hackage.haskell.org/package/sbv -Please see: http://leventerkok.github.io/sbv/+Express properties about Haskell programs and automatically prove them using SMT solvers.++```haskell+$ ghci+ghci> :m Data.SBV+ghci> prove $ \x -> x `shiftL` 2 .== 4 * (x::SWord8)+Q.E.D.+ghci> prove $ \x -> x `shiftL` 2 .== 2 * (x::SWord8)+Falsifiable. Counter-example:+  s0 = 32 :: Word8+```++The function `prove` establishes theorem-hood, while `sat` finds a satisfying model if it exists.+All satisfying models can be computed using `allSat`. +SBV can also perform static assertion checks, such as absence of division-by-0, and other user given properties. +Furthermore, SBV can perform optimization, minimizing/maximizing arithmetic goals for their optimal values.++SBV also allows for an incremental mode: Users are given a handle to the SMT solver as their programs execute, and they can issue SMTLib commands programmatically, query values, and direct the interaction using a high-level typed API. The incremental mode also allows for creation of constraints based on the current model, and access to internals of SMT solvers for advanced users. See the `runSMT` and `query` commands for details.++## 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).+   +SBV library provides support for dealing with symbolic values in Haskell. It introduces the types:++ - `SBool`: Symbolic Booleans (bits).+ - `SWord8`, `SWord16`, `SWord32`, `SWord64`: Symbolic Words (unsigned).+ - `SInt8`, `SInt16`, `SInt32`, `SInt64`: Symbolic Ints (signed).+ - `SWord N`, `SInt N`, for `N > 0`: Arbitrary sized unsigned/signed bit-vectors, parameterized by the bitsize. (Using DataKinds extension.)+ - `SInteger`: Symbolic unbounded integers (signed).+ - `SReal`: Symbolic infinite precision algebraic reals (signed).+ - `SRational`: Symbolic rationals, ratio of two symbolic integers. (`Rational`.)+ - `SFloat`: IEEE-754 single precision floating point number. (`Float`.)+ - `SDouble`: IEEE-754 double precision floating point number. (`Double`.)+ - `SFloatingPoint`: IEEE-754 floating point number with user specified exponent and significand sizes. (`FloatingPoint`)+ - `SChar`: Symbolic characters, supporting unicode.+ - `SString`: Symbolic strings.+ - `SList`: Symbolic lists. (Which can be nested, i.e., lists of lists.)+ - `STuple`: Symbolic tuples (upto 8-tuples, can be nested)+ - `SEither`: Symbolic sums+ - `SMaybe`: Symbolic optional values+ - `SSet`: Symbolic sets+ - Arrays of symbolic values.+ - Symbolic enumerations, for arbitrary user-defined enumerated types.+ - Symbolic polynomials over GF(2^n ), polynomial arithmetic, and CRCs.+ - Uninterpreted constants and functions over symbolic values, with user defined axioms.+ - Uninterpreted sorts, and proofs over such sorts, potentially with axioms.+ - Ability to define SMTLib functions, generated directly from Haskell versions, including support for recursive and mutually recursive functions.+ - Reasoning with universal and existential quantifiers, including alternating quantifiers.+  +The user can construct ordinary Haskell programs using these types, which behave like ordinary Haskell values when used concretely. However, when used with symbolic arguments, functions built out of these types can also be:++ - proven correct via an external SMT solver (the `prove` function),+ - checked for satisfiability (the `sat`, and `allSat` functions),+ - checked for assertion violations (the `safe` function with `sAssert` calls),+ - checked for delta-satisfiability (the `dsat` and `dprove` functions),+ - used in synthesis (the `sat`function with existentials),+ - checked for machine-arithmetic overflow/underflow conditions,+ - optimized with respect to cost functions (the `optimize`, `maximize`, and `minimize` functions),+ - quick-checked,+ - used for generating Haskell and C test vectors (the `genTest` function),+ - compiled down to C, rendered as straight-line programs or libraries (`compileToC` and `compileToCLib` functions).+   +## Picking the SMT solver to use++The SBV library uses third-party SMT solvers via the standard SMT-Lib interface. The following solvers are supported:++ - [ABC](http://www.eecs.berkeley.edu/~alanmi/abc) from University of Berkeley+ - [Boolector](https://boolector.github.io/) from Johannes Kepler University+ - [Bitwuzla](https://bitwuzla.github.io/) from Stanford University+ - [CVC4](http://cvc4.github.io/) and [CVC5](http://cvc5.github.io/) from Stanford University and the University of Iowa+ - [DReal](https://dreal.github.io/) from CMU+ - [MathSAT](http://mathsat.fbk.eu/) from FBK and DISI-University of Trento+ - [OpenSMT](https://verify.inf.usi.ch/opensmt) from Università della Svizzera italiana+ - [Yices](http://yices.csl.sri.com/) from SRI+ - [Z3](http://github.com/Z3Prover/z3/wiki) from Microsoft+   +Most functions have two variants: For instance `prove`/`proveWith`. The former uses the default solver, which is currently Z3. The latter expects you to pass it a configuration that picks the solver.+The valid values are `abc`, `boolector`, `bitwuzla`, `cvc4`, `cvc5`, `dReal`, `mathSAT`, `openSMT`, `yices`, and `z3`.++See [versions](http://github.com/LeventErkok/sbv/blob/master/SMTSolverVersions.md) for a listing of the versions of these tools SBV has been tested with. Please report if you see any discrepancies!++Other SMT solvers can be used with SBV as well, with a relatively easy hook-up mechanism. Please do get in touch if you plan to use SBV with any other solver.++## Using multiple solvers, simultaneously++SBV also allows for running multiple solvers at the same time, either picking the result of the first to complete, or getting results from all. +See `proveWithAny`/`proveWithAll` and `satWithAny`/`satWithAll` functions. The function `sbvAvailableSolvers` can be used to query the available solvers at run-time.++## Copyright, License++The SBV library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for details.+The [LICENSE](http://github.com/LeventErkok/sbv/tree/master/LICENSE) file contains the [BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.++## Thanks++The following people made major contributions to SBV, by developing new features and contributing to the design in significant ways: Joel Burget, Brian Huffman, Brian Schroeder, and Jeffrey Young.++The following people reported bugs, provided comments/feedback, or contributed to the development of SBV in various ways:+Ara Adkins,+Kanishka Azimi,+Markus Barenhoff,+Reid Barton,+Ben Blaxill,+Ian Blumenfeld,+Guillaume Bouchard,+Martin Brain,+Ian Calvert,+Oliver Charles,+Christian Conkle,+Matthew Danish,+Iavor Diatchki,+Alex Dixon,+Robert Dockins, +Thomas DuBuisson,+Trevor Elliott,+Gergő Érdi,+John Erickson,+Richard Fergie,+Adam Foltzer,+Joshua Gancher,+Remy Goldschmidt,+Brad Hardy,+Tom Hawkins,+Greg Horn,+Jan Hrcek,+Georges-Axel Jaloyan,+Anders Kaseorg,+Tom Sydney Kerckhove,+Lars Kuhtz,+Piërre van de Laar,+Pablo Lamela,+Ken Friis Larsen,+Andrew Lelechenko,+Joe Leslie-Hurd,+Nick Lewchenko,+Brett Letner,+Sirui Lu,+Georgy Lukyanov,+Martin Lundfall,+John Matthews,+Curran McConnell,+Philipp Meyer,+Joshua Moerman,+Matt Parker,+Jan Path,+Matt Peddie,+Lucas Peña,+Matthew Pickering,+Lee Pike,+Gleb Popov,+Rohit Ramesh,+Geoffrey Ramseyer,+Jaro Reinders,+Stephan Renatus,+Dan Rosén,+Ryan Scott,+Eric Seidel,+Austin Seipp,+Andrés Sicard-Ramírez,+Don Stewart,+Greg Sullivan,+Josef Svenningsson,+George Thomas,+May Torrence,+Daniel Wagner,+Sean Weaver,+Nis Wegmann,+and Jared Ziegler.++Thanks!

@@ -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.5-inplace:Data.SBV.Control.Utils+  error, called at ./Data/SBV/Control/Utils.hs:1660:57 in sbv-10.6-inplace:Data.SBV.Control.Utils

@@ -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.5-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.6-inplace:Data.SBV.Core.Symbolic

@@ -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.5-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.6-inplace:Data.SBV.Core.Symbolic

@@ -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.5-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.6-inplace:Data.SBV.Core.Symbolic

@@ -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.5-inplace:Data.SBV.Core.Symbolic+  error, called at ./Data/SBV/Core/Symbolic.hs:1937:48 in sbv-10.6-inplace:Data.SBV.Core.Symbolic

@@ -77,7 +77,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "state of the most recent check-sat command is not known") [SEND] (get-info :version)-[RECV] (:version "4.12.6")+[RECV] (:version "4.13.0") [SEND] (get-info :status) [RECV] (:status sat) [GOOD] (define-fun s16 () Int 4)@@ -108,7 +108,7 @@ [SEND] (get-info :reason-unknown) [RECV] (:reason-unknown "unknown") [SEND] (get-info :version)-[RECV] (:version "4.12.6")+[RECV] (:version "4.13.0") [SEND] (get-info :memory) [RECV] unsupported [SEND] (get-info :time)@@ -152,18 +152,18 @@ [RECV] ((set-logic ALL)        (proof        (let (($x268 (<= s0 6)))-        (let (($x269 (not $x268)))-        (let (($x276 (or (not bey) $x269)))-        (let ((@x274 (monotonicity (rewrite (= (> s0 6) $x269)) (= (=> bey (> s0 6)) (=> bey $x269)))))-        (let ((@x280 (trans @x274 (rewrite (= (=> bey $x269) $x276)) (= (=> bey (> s0 6)) $x276))))-        (let ((@x281 (mp (asserted (=> bey (> s0 6))) @x280 $x276)))-        (let (($x293 (>= s0 6)))-        (let (($x292 (not $x293)))-        (let (($x300 (or (not hey) $x292)))-        (let ((@x291 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) (rewrite (= (not (<= 6 s0)) $x292)) (= (< s0 6) $x292))))-        (let ((@x304 (trans (monotonicity @x291 (= (=> hey (< s0 6)) (=> hey $x292))) (rewrite (= (=> hey $x292) $x300)) (= (=> hey (< s0 6)) $x300))))-        (let ((@x305 (mp (asserted (=> hey (< s0 6))) @x304 $x300)))-        (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x293 $x268)) (unit-resolution @x305 (asserted hey) $x292) (unit-resolution @x281 (asserted bey) $x269) false)))))))))))))))+       (let (($x269 (not $x268)))+       (let (($x276 (or (not bey) $x269)))+       (let ((@x274 (monotonicity (rewrite (= (> s0 6) $x269)) (= (=> bey (> s0 6)) (=> bey $x269)))))+       (let ((@x280 (trans @x274 (rewrite (= (=> bey $x269) $x276)) (= (=> bey (> s0 6)) $x276))))+       (let ((@x281 (mp (asserted (=> bey (> s0 6))) @x280 $x276)))+       (let (($x293 (>= s0 6)))+       (let (($x292 (not $x293)))+       (let (($x300 (or (not hey) $x292)))+       (let ((@x291 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) (rewrite (= (not (<= 6 s0)) $x292)) (= (< s0 6) $x292))))+       (let ((@x304 (trans (monotonicity @x291 (= (=> hey (< s0 6)) (=> hey $x292))) (rewrite (= (=> hey $x292) $x300)) (= (=> hey (< s0 6)) $x300))))+       (let ((@x305 (mp (asserted (=> hey (< s0 6))) @x304 $x300)))+       (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x293 $x268)) (unit-resolution @x305 (asserted hey) $x292) (unit-resolution @x281 (asserted bey) $x269) false))))))))))))))) [SEND, TimeOut: 90000ms] (get-assertions)  [RECV] ((! s7 :named |a > 0|)

@@ -1,20 +1,18 @@ Cabal-Version: 2.2  Name        : sbv-Version     : 10.5+Version     : 10.6 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                (Satisfiability Modulo Theories) solvers.-               .-               For details, please see: <http://leventerkok.github.io/sbv/>  Copyright          : Levent Erkok, 2010-2024 License            : BSD-3-Clause License-file       : LICENSE Stability          : Experimental Author             : Levent Erkok-Homepage           : http://leventerkok.github.io/sbv/+Homepage           : http://github.com/LeventErkok/sbv Bug-reports        : http://github.com/LeventErkok/sbv/issues Maintainer         : Levent Erkok (erkokl@gmail.com) Build-Type         : Simple@@ -116,6 +114,7 @@                   , Data.SBV.RegExp                   , Data.SBV.Tools.BMC                   , Data.SBV.Tools.BoundedList+                  , Data.SBV.Tools.BVOptimize                   , Data.SBV.Tools.Induction                   , Data.SBV.Tools.BoundedFix                   , Data.SBV.Tools.CodeGen