sbv 2.9 → 2.10
raw patch · 28 files changed
+1233/−705 lines, 28 files
Files
- CHANGES.md +527/−0
- Data/SBV.hs +8/−4
- Data/SBV/BitVectors/Data.hs +49/−27
- Data/SBV/BitVectors/Model.hs +40/−3
- Data/SBV/Bridge/Boolector.hs +105/−0
- Data/SBV/Bridge/CVC4.hs +2/−0
- Data/SBV/Bridge/Yices.hs +2/−0
- Data/SBV/Bridge/Z3.hs +2/−0
- Data/SBV/Examples/BitPrecise/PrefixSum.hs +12/−10
- Data/SBV/Examples/Uninterpreted/Shannon.hs +129/−0
- Data/SBV/Provers/Boolector.hs +83/−0
- Data/SBV/Provers/CVC4.hs +13/−4
- Data/SBV/Provers/Prover.hs +18/−12
- Data/SBV/Provers/SExpr.hs +2/−0
- Data/SBV/Provers/Yices.hs +10/−1
- Data/SBV/Provers/Z3.hs +15/−6
- Data/SBV/SMT/SMT.hs +9/−7
- Data/SBV/SMT/SMTLib.hs +21/−7
- Data/SBV/SMT/SMTLib1.hs +58/−50
- Data/SBV/SMT/SMTLib2.hs +53/−34
- README +0/−4
- README.md +4/−0
- RELEASENOTES +0/−524
- SBVUnitTest/SBVTestCollection.hs +6/−4
- SBVUnitTest/SBVUnitTest.hs +4/−3
- SBVUnitTest/SBVUnitTestBuildTime.hs +1/−1
- SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs +49/−0
- sbv.cabal +11/−4
+ CHANGES.md view
@@ -0,0 +1,527 @@+* Hackage: <http://hackage.haskell.org/package/sbv>+* GitHub: <http://leventerkok.github.com/sbv/>++* Latest Hackage released version: 2.10++### Version 2.10, 2013-03-22+ + * Add support for the Boolector SMT solver+ * See: http://fmv.jku.at/boolector/+ * Use `import Data.SBV.Bridge.Boolector` to use Boolector from SBV+ * Boolector supports QF_BV (with an without arrays). In the last+ SMT-Lib competition it won both bit-vector categories. It is definitely+ worth trying it out for bitvector problems.+ * Changes to the library:+ * Generalize types of `allDifferent` and `allEqual` to take+ arbitrary EqSymbolic values. (Previously was just over SBV values.)+ * Add `inRange` predicate, which checks if a value is bounded within+ two others.+ * Add `sElem` predicate, which checks for symbolic membership+ * Add `fullAdder`: Returns the carry-over as a separate boolean bit.+ * Add `fullMultiplier`: Returns both the lower and higher bits resulting+ from multiplication.+ * Use the SMT-Lib Bool sort to represent SBool, instead of bit-vectors of length 1.+ While this is an under-the-hood mechanism that should be user-transparent, it+ turns out that one can no longer write axioms that return booleans in a direct+ way due to this translation. This change makes it easier to write axioms that+ utilize booleans as there is now a 1-to-1 match. (Suggested by Thomas DuBuisson.)+ * Solvers changes:+ * Z3: Update to the new parameter naming schema of Z3. This implies that+ you need to have a really recent version of Z3 installed, something+ in the Z3-4.3 series.+ * Examples:+ * Add Examples/Uninterpreted/Shannon.hs: Demonstrating Shannon expansion,+ boolean derivatives, etc.+ * Bug-fixes:+ * Gracefully handle the case if the backend-SMT solver does not put anything+ in stdout. (Reported by Thomas DuBuisson.)+ * Handle uninterpreted sort values, if they happen to be only created via+ function calls, as opposed to being inputs. (Reported by Thomas DuBuisson.)++### Version 2.9, 2013-01-02++ - Add support for the CVC4 SMT solver from New York University and+ the University of Iowa. (http://cvc4.cs.nyu.edu/).+ NB. Z3 remains the default solver for SBV. To use CVC4, use the+ *With variants of the interface (i.e., proveWith, satWith, ..)+ by passing cvc4 as the solver argument. (Similarly, use 'yices'+ as the argument for the *With functions for invoking yices.)+ - Latest release of Yices calls the SMT-Lib based solver executable+ yices-smt. Updated the default value of the executable to have this+ name for ease of use.+ - Add an extra boolean flag to compileToSMTLib and generateSMTBenchmarks+ functions to control if the translation should keep the query as is+ (for SAT cases), or negate it (for PROVE cases). Previously, this value+ was hard-coded to do the PROVE case only.+ - Add bridge modules, to simplify use of different solvers. You can now say:++ import Data.SBV.Bridge.CVC4+ import Data.SBV.Bridge.Yices+ import Data.SBV.Bridge.Z3+ + to pick the appropriate default solver. if you simply 'import Data.SBV', then+ you will get the default SMT solver, which is currently Z3. The value+ 'defaultSMTSolver' refers to z3 (currently), and 'sbvCurrentSolver' refers+ to the chosen solver as determined by the imported module. (The latter is+ useful for modifying options to the SMT solver in an solver-agnostic way.)+ - Various improvements to Z3 model parsing routines.+ - New web page for SBV: http://leventerkok.github.com/sbv/ is now online.++### Version 2.8, 2012-11-29++ - Rename the SNum class to SIntegral, and make it index over regular+ types. This makes it much more useful, simplifying coding of+ polymorphic symbolic functions over integral types, which is+ the common case.+ - Add the functions:+ - sbvShiftLeft+ - sbvShiftRight+ which can accommodate unsigned symbolic shift amounts. Note that+ one cannot use Haskell's shiftL/shiftR from the Bits class since+ they are hard-wired to take 'Int' values as the shift amounts only.+ - Add a new function 'sbvArithShiftRight', which is the same as+ a shift-right, except it uses the MSB of the input as the bit to fill+ in (instead of always filling in with 0 bits). Note that this is+ the same as shiftRight for signed values, but differs from a shiftRight+ when the input is unsigned. (There is no Haskell analogue of this+ function, as Haskell's shiftR is always arithmetic for signed+ types and logical for unsigned ones.) This variant is designed for+ use cases when one uses the underlying unsigned SMT-Lib representation+ to implement custom signed operations, for instance.+ - Several typo fixes.++### Version 2.7, 2012-10-21++ - Add missing QuickCheck instance for SReal+ - When dealing with concrete SReal's, make sure to operate+ only on exact algebraic reals on the Haskell side, leaving+ true algebraic reals (i.e., those that are roots of polynomials+ that cannot be expressed as a rational) symbolic. This avoids+ issues with functions that we cannot implement directly on+ the Haskell side, like exact square-roots.+ - Documentation tweaks, typo fixes etc.+ - Rename BVDivisible class to SDivisible; since SInteger+ is also an instance of this class, and SDivisible is a+ more appropriate name to start with. Also add sQuot and sRem+ methods; along with sDivMod, sDiv, and sMod, with usual+ semantics. + - Improve test suite, adding many constant-folding tests+ and start using cabal based tests (--enable-tests option.)++Versions 2.4, 2.5, and 2.6: Around mid October 2012++ - Workaround issues related hackage compilation, in particular to the+ problem with the new containers package release, which does provide+ an NFData instance for sequences.+ - Add explicit Num requirements when necessary, as the Bits class+ no longer does this.+ - Remove dependency on the hackage package strict-concurrency, as+ hackage can no longer compile it due to some dependency mismatch.+ - Add forgotten Real class instance for the type 'AlgReal'+ - Stop putting bounds on hackage dependencies, as they cause+ more trouble then they actually help. (See the discussion+ here: http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html.)++### Version 2.3, 2012-07-20++ - Maintanence release, no new features.+ - Tweak cabal dependencies to avoid using packages that are newer+ than those that come with ghc-7.4.2. Apparently this is a no-no+ that breaks many things, see the discussion in this thread:+ http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html+ In particular, the use of containers >= 0.5 is *not* OK until we have+ a version of GHC that comes with that version.++### Version 2.2, 2012-07-17++ - Maintanence release, no new features.+ - Update cabal dependencies, in particular fix the+ regression with respect to latest version of the+ containers package.++### Version 2.1, 2012-05-24++ Library:+ - Add support for uninterpreted sorts, together with user defined+ domain axioms. See Data.SBV.Examples.Uninterpreted.Sort+ and Data.SBV.Examples.Uninterpreted.Deduce for basic examples of+ this feature.+ - Add support for C code-generation with SReals. The user picks+ one of 3 possible C types for the SReal type: CgFloat, CgDouble+ or CgLongDouble, using the function cgSRealType. Naturally, the+ resulting C program will suffer a loss of precision, as it will+ be subject to IEE-754 rounding as implied by the underlying type.+ - Add toSReal :: SInteger -> SReal, which can be used to promote+ symbolic integers to reals. Comes handy in mixed integer/real+ computations.+ Examples:+ - Recast the dog-cat-mouse example to use the solver over reals.+ - Add Data.SBV.Examples.Uninterpreted.Sort, and+ Data.SBV.Examples.Uninterpreted.Deduce+ for illustrating uninterpreted sorts and axioms.++### Version 2.0, 2012-05-10+ + This is a major release of SBV, adding support for symbolic algebraic reals: SReal.+ See http://en.wikipedia.org/wiki/Algebraic_number for details. In brief, algebraic+ reals are solutions to univariate polynomials with rational coefficients. The arithmetic+ on algebraic reals is precise, with no approximation errors. Note that algebraic reals+ are a proper subset of all reals, in particular transcendental numbers are not+ representable in this way. (For instance, "sqrt 2" is algebraic, but pi, e are not.)+ However, algebraic reals is a superset of rationals, so SBV now also supports symbolic+ rationals as well.+ + You *should* use Z3 v4.0 when working with real numbers. While the interface will+ work with older versions of Z3 (or other SMT solvers in general), it uses Z3's+ root-obj construct to retrieve and query algebraic reals.++ While SReal values have infinite precision, printing such values is not trivial since+ we might need an infinite number of digits if the result happens to be irrational. The+ user controls printing precision, by specifying how many digits after the decimal point+ should be printed. The default number of decimal digits to print is 10. (See the+ 'printRealPrec' field of SMT-solver configuration.)++ The acronym SBV used to stand for Symbolic Bit Vectors. However, SBV has grown beyond+ bit-vectors, especially with the addition of support for SInteger and SReal types and+ other code-generation utilities. Therefore, "SMT Based Verification" is now a better fit+ for the expansion of the acronym SBV.++ Other notable changes in the library:+ * Add functions s[TYPE] and s[TYPE]s for each symbolic type we support (i.e.,+ sBool, sBools, sWord8, sWord8s, etc.), to create symbolic variables of the+ right kind. Strictly speaking these are just synonyms for 'free'+ and 'mapM free' (plural versions), so they aren't adding any additional+ power. Except, they are specialized at their respective types, and might be+ easier to remember.+ * Add function solve, which is merely a synonym for (return . bAnd), but+ it simplifies expressing problems.+ * Add class SNum, which simplifies writing polymorphic code over symbolic values+ * Increase haddock coverage metrics+ * Major code refactoring around symbolic kinds+ * SMTLib2: Emit ":produce-models" call before setting the logic, as required+ by the SMT-Lib2 standard. [Patch provided by arrowdodger on github, thanks!]++ Bugs fixed:+ * [Performance] Use a much simpler default definition for "select": While the+ older version (based on binary search on the bits of the indexer) was correct,+ it created unnecessarily big expressions. Since SBV does not have a notion+ of concrete subwords, the binary-search trick was not bringing any advantage+ in any case. Instead, we now simply use a linear walk over the elements.++ Examples:+ * Change dog-cat-mouse example to use SInteger for the counts+ * Add merge-sort example: Data.SBV.Examples.BitPrecise.MergeSort+ * Add diophantine solver example: Data.SBV.Examples.Existentials.Diophantine++### Version 1.4, 2012-05-10++ * Interim release for test purposes++### Version 1.3, 2012-02-25++ * Workaround cabal/hackage issue, functionally the same as release+ 1.2 below++### Version 1.2, 2012-02-25++ Library:+ * Add a hook so users can add custom script segments for SMT solvers. The new+ "solverTweaks" field in the SMTConfig data-type can be used for this purpose.+ The need for this came about due to the need to workaround a Z3 v3.2 issue+ detalied below:+ http://stackoverflow.com/questions/9426420/soundness-issue-with-integer-bv-mixed-benchmarks+ As a consequence, mixed Integer/BV problems can cause soundness issues in Z3+ and does in SBV. Unfortunately, it's too severe for SBV to add the woraround+ option, as it slows down the solver as a side effect as well. Thus, we're+ making this optionally available if/when needed. (Note that the work-around+ should not be necessary with Z3 v3.3; which isn't released yet.)+ * Other minor clean-up++### Version 1.1, 2012-02-14++ Library:+ * Rename bitValue to sbvTestBit+ * Add sbvPopCount+ * Add a custom implementation of 'popCount' for the Bits class+ instance of SBV (GHC >= 7.4.1 only)+ * Add 'sbvCheckSolverInstallation', which can be used to check+ that the given solver is installed and good to go.+ * Add 'generateSMTBenchmarks', simplifying the generation of+ SMTLib benchmarks for offline sharing.++### Version 1.0, 2012-02-13++ Library:+ * Z3 is now the "default" SMT solver. Yices is still available, but+ has to be specifically selected. (Use satWith, allSatWith, proveWith, etc.)+ * Better handling of the pConstrain probability threshold for test+ case generation and quickCheck purposes.+ * Add 'renderTest', which accompanies 'genTest' to render test+ vectors as Haskell/C/Forte program segments.+ * Add 'expectedValue' which can compute the expected value of+ a symbolic value under the given constraints. Useful for statistical+ analysis and probability computations.+ * When saturating provable values, use forAll_ for proofs and forSome_+ for sat/allSat. (Previously we were allways using forAll_, which is+ not incorrect but less intuitive.)+ * add function:+ extractModels :: SatModel a => AllSatResult -> [a]+ which simplifies accessing allSat results greatly.+ Code-generation:+ * add "cgGenerateMakefile" which allows the user to choose if SBV+ should generate a Makefile. (default: True)+ Other+ * Changes to make it compile with GHC 7.4.1.++### Version 0.9.24, 2011-12-28++ Library:+ * Add "forSome," analogous to "forAll." (The name "exists" would've+ been better, but it's already taken.) This is not as useful as+ one might think as forAll and forSome do not nest, as an inner+ application of one pushes its argument to a Predicate, making+ the outer one useless, but it's nonetheless useful by itself.+ * Add a "Modelable" class, which simplifies model extraction.+ * Add support for quick-check at the "Symbolic SBool" level. Previously+ SBV only allowed functions returning SBool to be quick-checked, which+ forced a certain style of coding. In particular with the addition+ of quantifiers, the new coding style mostly puts the top-level+ expressions in the Symbolic monad, which were not quick-checkable+ before. With new support, the quickCheck, prove, sat, and allSat+ commands are all interchangeable with obvious meanings.+ * Add support for concrete test case generation, see the genTest function.+ * Improve optimize routines and add support for iterative optimization.+ * Add "constrain", simplifying conjunctive constraints, especially+ useful for adding constraints at variable generation time via+ forall/exists. Note that the interpretation of such constraints+ is different for genTest and quickCheck functions, where constraints+ will be used for appropriately filtering acceptable test values+ in those two cases.+ * Add "pConstrain", which probabilistically adds constraints. This+ is useful for quickCheck and genTest functions for filtering acceptable+ test values. (Calls to pConstrain will be rejected for sat/prove calls.)+ * Add "isVacuous" which can be used to check that the constraints added+ via constrain are satisfable. This is useful to prevent vacuous passes,+ i.e., when a proof is not just passing because the constraints imposed+ are inconsistent. (Also added accompanying isVacuousWith.)+ * Add "free" and "free_", analogous to "forall/forall_" and "exists/exists_"+ The difference is that free behaves universally in a proof context, while+ it behaves existentially in a sat context. This allows us to express+ properties more succinctly, since the intended semantics is usually this+ way depending on the context. (i.e., in a proof, we want our variables+ universal, in a sat call existential.) Of course, exists/forall are still+ available when mixed quantifiers are needed, or when the user wants to+ be explicit about the quantifiers.+ Examples+ * Add Data/SBV/Examples/Puzzles/Coins.hs. (Shows the usage of "constrain".)+ Dependencies+ * Bump up random package dependency to 1.0.1.1 (from 1.0.0.2)+ Internal+ * Major reorganization of files to and build infrastructure to+ decrease build times and better layout+ * Get rid of custom Setup.hs, just use simple build. The extra work+ was not worth the complexity.++### Version 0.9.23, 2011-12-05+ + Library:+ * Add support for SInteger, the type of signed unbounded integer+ values. SBV can now prove theorems about unbounded numbers,+ following the semantics of Haskell's Integer type. (Requires z3 to+ be used as the backend solver.)+ * Add functions 'optimize', 'maximize', and 'minimize' that can+ be used to find optimal solutions to given constraints with+ respect to a given cost function.+ * Add 'cgUninterpret', which simplifies code generation when we want+ to use an alternate definition in the target language (i.e., C). This+ is important for efficient code generation, when we want to+ take advantage of native libraries available in the target platform.+ Other:+ * Change getModel to return a tuple in the success case, where+ the first component is a boolean indicating whether the model+ is "potential." This is used to indicate that the solver+ actually returned "unknown" for the problem and the model+ might therefore be bogus. Note that we did not need this before+ since we only supported bounded bit-vectors, which has a decidable+ theory. With the addition of unbounded Integer's and quantifiers, the+ solvers can now return unknown. This should still be rare in practice,+ but can happen with the use of non-linear constructs. (i.e.,+ multiplication of two variables.)++### Version 0.9.22, 2011-11-13+ + The major change in this release is the support for quantifiers. The+ SBV library *no* longer assumes all variables are universals in a proof,+ (and correspondingly existential in a sat) call. Instead, the user+ marks free-variables appropriately using forall/exists functions, and the+ solver translates them accordingly. Note that this is a non-backwards+ compatible change in sat calls, as the semantics of formulas is essentially+ changing. While this is unfortunate, it's more uniform and simpler to understand+ in general.++ This release also adds support for the Z3 solver, which is the main+ SMT-solver used for solving formulas involving quantifiers. More formally,+ we use the new AUFBV/ABV/UFBV logics when quantifiers are involved. Also, + the communication with Z3 is now done via SMT-Lib2 format. Eventually+ the SMTLib1 connection will be severed.++ The other main change is the support for C code generation with+ uninterpreted functions enabling users to interface with external+ C functions defined elsewhere. See below for details.++ Other changes:+ Code:+ * Change getModel, so it returns an Either value to indicate+ something went wrong; instead of throwing an error+ * Add support for computing CRCs directly (without needing+ polynomial division).+ Code generation:+ * Add "cgGenerateDriver" function, which can be used to turn+ on/off driver program generation. Default is to generate+ a driver. (Issue "cgGenerateDriver False" to skip the driver.)+ For a library, a driver will be generated if any of the+ constituent parts has a driver. Otherwise it'll be skipped.+ * Fix a bug in C code generation where "Not" over booleans were+ incorrectly getting translated due to need for masking.+ * Add support for compilation with uninterpreted functions. Users+ can now specify the corresponding C code and SBV will simply+ call the "native" functions instead of generating it. This+ enables interfacing with other C programs. See the functions:+ cgAddPrototype, cgAddDecl, and cgAddLDFlags.+ Examples:+ * Add CRC polynomial generation example via existentials+ * Add USB CRC code generation example, both via polynomials and+ using the internal CRC functionality++### Version 0.9.21, 2011-08-05+ + Code generation:+ * Allow for inclusion of user makefiles+ * Allow for CCFLAGS to be set by the user+ * Other minor clean-up++### Version 0.9.20, 2011-06-05+ + Regression on 0.9.19; add missing file to cabal++### Version 0.9.19, 2011-06-05+ + Code:+ * Add SignCast class for conversion between signed/unsigned+ quantities for same-sized bit-vectors+ * Add full-binary trees that can be indexed symbolically (STree). The+ advantage of this type is that the reads and writes take+ logarithmic time. Suitable for implementing faster symbolic look-up.+ * Expose HasSignAndSize class through Data.SBV.Internals+ * Many minor improvements, file re-orgs+ Examples:+ * Add sentence-counting example+ * Add an implementation of RC4++### Version 0.9.18, 2011-04-07++ Code:+ * Re-engineer code-generation, and compilation to C.+ In particular, allow arrays of inputs to be specified,+ both as function arguments and output reference values.+ * Add support for generation of generation of C-libraries,+ allowing code generation for a set of functions that+ work together.+ Examples:+ * Update code-generation examples to use the new API.+ * Include a library-generation example for doing 128-bit+ AES encryption++### Version 0.9.17, 2011-03-29+ + Code:+ * Simplify and reorganize the test suite+ Examples:+ * Improve AES decryption example, by using+ table-lookups in InvMixColumns.+ +### Version 0.9.16, 2011-03-28++ Code:+ * Further optimizations on Bits instance of SBV+ Examples:+ * Add AES algorithm as an example, showing how+ encryption algorithms are particularly suitable+ for use with the code-generator++### Version 0.9.15, 2011-03-24+ + Bug fixes:+ * Fix rotateL/rotateR instances on concrete+ words. Previous versions was bogus since+ it relied on the Integer instance, which+ does the wrong thing after normalization.+ * Fix conversion of signed numbers from bits,+ previous version did not handle two's+ complement layout correctly+ Testing:+ * Add a sleuth of concrete test cases on+ arithmetic to catch bugs. (There are many+ of them, ~30K, but they run quickly.)++### Version 0.9.14, 2011-03-19+ + - Reimplement sharing using Stable names, inspired+ by the Data.Reify techniques. This avoids tricks+ with unsafe memory stashing, and hence is safe.+ Thus, issues with respect to CAFs are now resolved.++### Version 0.9.13, 2011-03-16+ + Bug fixes:+ * Make sure SBool short-cut evaluations are done+ as early as possible, as these help with coding+ recursion-depth based algorithms, when dealing+ with symbolic termination issues.+ Examples:+ * Add fibonacci code-generation example, original+ code by Lee Pike.+ * Add a GCD code-generation/verification example++### Version 0.9.12, 2011-03-10+ + New features:+ * Add support for compilation to C+ * Add a mechanism for offline saving of SMT-Lib files++ Bug fixes:+ * Output naming bug, reported by Josef Svenningsson+ * Specification bug in Legato's multipler example++### Version 0.9.11, 2011-02-16+ + * Make ghc-7.0 happy, minor re-org on the cabal file/Setup.hs++### Version 0.9.10, 2011-02-15++ * Integrate commits from Iavor: Generalize SBV's to keep+ track the integer directly without resorting to different+ leaf types+ * Remove the unnecessary CLC instruction from the Legato example+ * More tests++### Version 0.9.9, 2011-01-23++ * Support for user-defined SMT-Lib axioms to be+ specified for uninterpreted constants/functions+ * Move to using doctest style inline tests++### Version 0.9.8, 2011-01-22++ * Better support for uninterpreted-functions+ * Support counter-examples with SArray's+ * Ladner-Fischer scheme example+ * Documentation updates++### Version 0.9.7, 2011-01-18++ * First stable public hackage release++Versions 0.0.0 - 0.9.6, Mid 2010 through early 2011++ * Basic infrastructure, design exploration
Data/SBV.hs view
@@ -84,6 +84,8 @@ -- -- * CVC4 from New York University and University of Iowa: <http://cvc4.cs.nyu.edu/> --+-- * Boolector from Johannes Kepler University: <http://fmv.jku.at/boolector/>+-- -- Support for other compliant solvers can be added relatively easily, please -- get in touch if there is a solver you'd like to see included. ---------------------------------------------------------------------------------@@ -118,11 +120,13 @@ , SymArray(..), SArray, SFunArray, mkSFunArray -- *** Full binary trees , STree, readSTree, writeSTree, mkSTree- -- ** Operations on symbolic words+ -- ** Operations on symbolic values -- *** Word level , sbvTestBit, sbvPopCount, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight, setBitTo, oneIf, lsb, msb- -- *** List level- , allEqual, allDifferent+ -- *** Predicates+ , allEqual, allDifferent, inRange, sElem+ -- *** Addition and Multiplication with high-bits+ , fullAdder, fullMultiplier -- *** Blasting/Unblasting , blastBE, blastLE, FromBits(..) -- *** Splitting, joining, and extending@@ -191,7 +195,7 @@ , SatModel(..), Modelable(..), displayModels, extractModels -- * SMT Interface: Configurations and solvers- , SMTConfig(..), OptimizeOpts(..), SMTSolver(..), yices, z3, cvc4, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation+ , SMTConfig(..), OptimizeOpts(..), SMTSolver(..), boolector, cvc4, yices, z3, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation -- * Symbolic computations , Symbolic, output, SymWord(..)
Data/SBV/BitVectors/Data.hs view
@@ -35,6 +35,7 @@ , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom , Quantifier(..), needsExistentials , SMTLibPgm(..), SMTLibVersion(..)+ , SolverCapabilities(..) ) where import Control.DeepSeq (NFData(..))@@ -210,6 +211,7 @@ kindOf :: a -> Kind hasSign :: a -> Bool intSizeOf :: a -> Int+ isBoolean :: a -> Bool isBounded :: a -> Bool isReal :: a -> Bool isInteger :: a -> Bool@@ -226,6 +228,8 @@ KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)" KReal -> error "SBV.HasKind.intSizeOf((S)Real)" KUninterpreted s -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s+ isBoolean x | KBounded False 1 <- kindOf x = True+ | True = False isBounded x | KBounded{} <- kindOf x = True | True = False isReal x | KReal{} <- kindOf x = True@@ -594,19 +598,26 @@ when (isJust mbCode) $ modifyIORef (rCgMap st) (Map.insert nm (fromJust mbCode)) where validChar x = isAlphaNum x || x `elem` "_" +-- | Create a new SW+newSW :: State -> Kind -> IO (SW, String)+newSW st k = do ctr <- incCtr st+ let sw = SW k (NodeId ctr)+ () <- case k of+ KUnbounded -> modifyIORef (rUnBounded st) (\(_, y) -> (True, y))+ KReal -> modifyIORef (rUnBounded st) (\(x, _) -> (x, True))+ KUninterpreted sortName -> registerSort st sortName -- in case the result is produced via an uninterpreted function+ _ -> return ()+ return (sw, 's' : show ctr)+{-# INLINE newSW #-}+ -- | Create a new constant; hash-cons as necessary newConst :: State -> CW -> IO SW newConst st c = do constMap <- readIORef (rconstMap st) case c `Map.lookup` constMap of Just sw -> return sw- Nothing -> do ctr <- incCtr st- let k = kindOf c- sw = SW k (NodeId ctr)- () <- case kindOf c of- KUnbounded -> modifyIORef (rUnBounded st) (\(_, y) -> (True, y))- KReal -> modifyIORef (rUnBounded st) (\(x, _) -> (x, True))- _ -> return ()+ Nothing -> do let k = kindOf c+ (sw, _) <- newSW st k modifyIORef (rconstMap st) (Map.insert c sw) return sw {-# INLINE newConst #-}@@ -633,12 +644,7 @@ exprMap <- readIORef (rexprMap st) case e `Map.lookup` exprMap of Just sw -> return sw- Nothing -> do ctr <- incCtr st- let sw = SW k (NodeId ctr)- () <- case k of- KUnbounded -> modifyIORef (rUnBounded st) (\(_, y) -> (True, y))- KReal -> modifyIORef (rUnBounded st) (\(x, _) -> (x, True))- _ -> return ()+ Nothing -> do (sw, _) <- newSW st k modifyIORef (spgm st) (\(SBVPgm xs) -> SBVPgm (xs S.|> (sw, e))) modifyIORef (rexprMap st) (Map.insert e sw) return sw@@ -676,13 +682,8 @@ Concrete _ -> do v@(SBV _ (Left cw)) <- liftIO randomIO liftIO $ modifyIORef (rCInfo st) ((maybe "_" id mbNm, cw):) return v- _ -> do ctr <- liftIO $ incCtr st- let nm = maybe ('s':show ctr) id mbNm- sw = SW k (NodeId ctr)- () <- case k of- KUnbounded -> liftIO $ modifyIORef (rUnBounded st) (\(_, y) -> (True, y))- KReal -> liftIO $ modifyIORef (rUnBounded st) (\(x, _) -> (x, True))- _ -> return ()+ _ -> do (sw, internalName) <- liftIO $ newSW st k+ let nm = maybe internalName id mbNm liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):) return $ SBV k $ Right $ cache (const (return sw)) @@ -895,24 +896,33 @@ mkSymWord mbQ mbNm = do let sortName = tyconUQname . dataTypeName . dataTypeOf $ (undefined :: a) st <- ask- let -- TBD: Is this list comprehensive?- reserved = ["Int", "Real", "List", "Array", "Bool"]- when (sortName `elem` reserved) $ error $ "SBV.registerSort: " ++ show sortName ++ " is a reserved sort; please use a different name"- curSorts <- liftIO $ readIORef (rSorts st)- when (sortName `notElem` curSorts) $ liftIO $ modifyIORef (rSorts st) (sortName :)+ liftIO $ registerSort st sortName let k = KUninterpreted sortName q = case (mbQ, runMode st) of (Just x, _) -> x (Nothing, Proof True) -> EX (Nothing, Proof False) -> ALL- (Nothing, Concrete{}) -> error $ "SBV.registerSort: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode."- (Nothing, CodeGen) -> error $ "SBV.registerSort: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode."+ (Nothing, Concrete{}) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in concrete simulation mode."+ (Nothing, CodeGen) -> error $ "SBV: Uninterpreted sort " ++ sortName ++ " can not be used in code-generation mode." ctr <- liftIO $ incCtr st let sw = SW k (NodeId ctr) nm = maybe ('s':show ctr) id mbNm liftIO $ modifyIORef (rinps st) ((q, (sw, nm)):) return $ SBV k $ Right $ cache (const (return sw)) +-- | Register an uninterpreted sort with SBV+registerSort :: State -> String -> IO ()+registerSort st sortName = do+ let -- This list comes from http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r10.12.21.pdf+ -- Note that we only have to include those SMT-Lib reserved names that start with a capital+ -- letter, since all Haskell types start with a capital-letter and there's no possibility of+ -- conflict for lower-case ones!+ -- TODO: Make sure this list covers everything!+ reserved = ["Int", "Real", "List", "Array", "Bool", "NUMERAL", "DECIMAL", "STRING", "FP"]+ when (sortName `elem` reserved) $ error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name."+ curSorts <- readIORef (rSorts st)+ when (sortName `notElem` curSorts) $ liftIO $ modifyIORef (rSorts st) (sortName :)+ instance (Random a, SymWord a) => Random (SBV a) where randomR (l, h) g = case (unliteral l, unliteral h) of (Just lb, Just hb) -> let (v, g') = randomR (lb, hb) g in (literal (v :: a), g')@@ -1142,3 +1152,15 @@ instance NFData a => NFData (SBV a) where rnf (SBV x y) = rnf x `seq` rnf y `seq` () instance NFData SBVPgm++-- | Translation tricks needed for specific capabilities afforded by each solver+data SolverCapabilities = SolverCapabilities {+ capSolverName :: String -- ^ Name of the solver+ , mbDefaultLogic :: Maybe String -- ^ set-logic string to use in case not automatically determined (if any)+ , supportsMacros :: Bool -- ^ Does the solver understand SMT-Lib2 macros?+ , supportsProduceModels :: Bool -- ^ Does the solver understand produce-models option setting+ , supportsQuantifiers :: Bool -- ^ Does the solver understand SMT-Lib2 style quantifiers?+ , supportsUninterpretedSorts :: Bool -- ^ Does the solver understand SMT-Lib2 style uninterpreted-sorts+ , supportsUnboundedInts :: Bool -- ^ Does the solver support unbounded integers?+ , supportsReals :: Bool -- ^ Does the solver support reals?+ }
Data/SBV/BitVectors/Model.hs view
@@ -23,7 +23,7 @@ module Data.SBV.BitVectors.Model ( Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SIntegral , sbvTestBit, sbvPopCount, setBitTo, sbvShiftLeft, sbvShiftRight, sbvSignedShiftArithRight- , allEqual, allDifferent, oneIf, blastBE, blastLE+ , allEqual, allDifferent, inRange, sElem, oneIf, blastBE, blastLE, fullAdder, fullMultiplier , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_ , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32 , sWord32s, sWord64, sWord64s, sInt8, sInt8s, sInt16, sInt16s, sInt32, sInt32s, sInt64@@ -522,15 +522,23 @@ | True = Nothing -- | Returns (symbolic) true if all the elements of the given list are different.-allDifferent :: (Eq a, SymWord a) => [SBV a] -> SBool+allDifferent :: EqSymbolic a => [a] -> SBool allDifferent (x:xs@(_:_)) = bAll (x ./=) xs &&& allDifferent xs allDifferent _ = true -- | Returns (symbolic) true if all the elements of the given list are the same.-allEqual :: (Eq a, SymWord a) => [SBV a] -> SBool+allEqual :: EqSymbolic a => [a] -> SBool allEqual (x:xs@(_:_)) = bAll (x .==) xs allEqual _ = true +-- | Returns (symbolic) true if the argument is in range+inRange :: OrdSymbolic a => a -> (a, a) -> SBool+inRange x (y, z) = x .>= y &&& x .<= z++-- | Symbolic membership test+sElem :: EqSymbolic a => a -> [a] -> SBool+sElem x xs = bAny (.== x) xs+ -- | Returns 1 if the boolean is true, otherwise 0. oneIf :: (Num a, SymWord a) => SBool -> SBV a oneIf t = ite t 1 0@@ -705,6 +713,35 @@ | True = ite (msb x) (complement (sbvShiftRight (complement x) i)) (sbvShiftRight x i)++-- | Full adder. Returns the carry-out from the addition.+--+-- N.B. Only works for unsigned types. Signed arguments will be rejected.+fullAdder :: SIntegral a => SBV a -> SBV a -> (SBool, SBV a)+fullAdder a b+ | isSigned a = error "fullAdder: only works on unsigned numbers"+ | True = (a .> s ||| b .> s, s)+ where s = a + b++-- | Full multiplier: Returns both the high-order and the low-order bits in a tuple,+-- thus fully accounting for the overflow.+--+-- N.B. Only works for unsigned types. Signed arguments will be rejected.+--+-- N.B. The higher-order bits are determined using a simple shift-add multiplier,+-- thus involving bit-blasting. It'd be naive to expect SMT solvers to deal efficiently+-- with properties involving this function, at least with the current state of the art.+fullMultiplier :: SIntegral a => SBV a -> SBV a -> (SBV a, SBV a)+fullMultiplier a b+ | isSigned a = error "fullMultiplier: only works on unsigned numbers"+ | True = (go (bitSize a) 0 a, a*b)+ where go 0 p _ = p+ go n p x = let (c, p') = ite (lsb x) (fullAdder p b) (false, p)+ (o, p'') = shiftIn c p'+ (_, x') = shiftIn o x+ in go (n-1) p'' x'+ shiftIn k v = (lsb v, mask .|. (v `shiftR` 1))+ where mask = ite k (bit (bitSize v - 1)) 0 -- | Little-endian blasting of a word into its bits. Also see the 'FromBits' class. blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]
+ Data/SBV/Bridge/Boolector.hs view
@@ -0,0 +1,105 @@+---------------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Bridge.Boolector+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Interface to the Boolector SMT solver. Import this module if you want to use the+-- Boolector SMT prover as your backend solver. Also see:+--+-- - "Data.SBV.Bridge.Yices"+--+-- - "Data.SBV.Bridge.Z3"+--+-- - "Data.SBV.Bridge.CVC4"+---------------------------------------------------------------------------------++module Data.SBV.Bridge.Boolector (+ -- * CVC4 specific interface+ sbvCurrentSolver+ -- ** Proving and checking satisfiability+ , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable+ -- ** Optimization routines+ , optimize, minimize, maximize+ -- * Non-Boolector specific SBV interface+ -- $moduleExportIntro+ , module Data.SBV+ ) where++import Data.SBV hiding (prove, sat, allSat, isVacuous, isTheorem, isSatisfiable, optimize, minimize, maximize, sbvCurrentSolver)++-- | Current solver instance, pointing to cvc4.+sbvCurrentSolver :: SMTConfig+sbvCurrentSolver = boolector++-- | Prove theorems, using the CVC4 SMT solver+prove :: Provable a+ => a -- ^ Property to check+ -> IO ThmResult -- ^ Response from the SMT solver, containing the counter-example if found+prove = proveWith sbvCurrentSolver++-- | Find satisfying solutions, using the CVC4 SMT solver+sat :: Provable a+ => a -- ^ Property to check+ -> IO SatResult -- ^ Response of the SMT Solver, containing the model if found+sat = satWith sbvCurrentSolver++-- | Find all satisfying solutions, using the CVC4 SMT solver+allSat :: Provable a+ => a -- ^ Property to check+ -> IO AllSatResult -- ^ List of all satisfying models+allSat = allSatWith sbvCurrentSolver++-- | Check vacuity of the explicit constraints introduced by calls to the 'constrain' function, using the CVC4 SMT solver+isVacuous :: Provable a+ => a -- ^ Property to check+ -> IO Bool -- ^ True if the constraints are unsatisifiable+isVacuous = isVacuousWith sbvCurrentSolver++-- | Check if the statement is a theorem, with an optional time-out in seconds, using the CVC4 SMT solver+isTheorem :: Provable a+ => Maybe Int -- ^ Optional time-out, specify in seconds+ -> a -- ^ Property to check+ -> IO (Maybe Bool) -- ^ Returns Nothing if time-out expires+isTheorem = isTheoremWith sbvCurrentSolver++-- | Check if the statement is satisfiable, with an optional time-out in seconds, using the CVC4 SMT solver+isSatisfiable :: Provable a+ => Maybe Int -- ^ Optional time-out, specify in seconds+ -> a -- ^ Property to check+ -> IO (Maybe Bool) -- ^ Returns Nothing if time-out expiers+isSatisfiable = isSatisfiableWith sbvCurrentSolver++-- | Optimize cost functions, using the CVC4 SMT solver+optimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+ => OptimizeOpts -- ^ Parameters to optimization (Iterative, Quantified, etc.)+ -> (SBV c -> SBV c -> SBool) -- ^ Betterness check: This is the comparison predicate for optimization+ -> ([SBV a] -> SBV c) -- ^ Cost function+ -> Int -- ^ Number of inputs+ -> ([SBV a] -> SBool) -- ^ Validity function+ -> IO (Maybe [a]) -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+optimize = optimizeWith sbvCurrentSolver++-- | Minimize cost functions, using the CVC4 SMT solver+minimize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+ => OptimizeOpts -- ^ Parameters to optimization (Iterative, Quantified, etc.)+ -> ([SBV a] -> SBV c) -- ^ Cost function to minimize+ -> Int -- ^ Number of inputs+ -> ([SBV a] -> SBool) -- ^ Validity function+ -> IO (Maybe [a]) -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+minimize = minimizeWith sbvCurrentSolver++-- | Maximize cost functions, using the CVC4 SMT solver+maximize :: (SatModel a, SymWord a, Show a, SymWord c, Show c)+ => OptimizeOpts -- ^ Parameters to optimization (Iterative, Quantified, etc.)+ -> ([SBV a] -> SBV c) -- ^ Cost function to maximize+ -> Int -- ^ Number of inputs+ -> ([SBV a] -> SBool) -- ^ Validity function+ -> IO (Maybe [a]) -- ^ Returns Nothing if there is no valid solution, otherwise an optimal solution+maximize = maximizeWith sbvCurrentSolver++{- $moduleExportIntro+The remainder of the SBV library that is common to all back-end SMT solvers, directly coming from the "Data.SBV" module.+-}
Data/SBV/Bridge/CVC4.hs view
@@ -12,6 +12,8 @@ -- - "Data.SBV.Bridge.Yices" -- -- - "Data.SBV.Bridge.Z3"+--+-- - "Data.SBV.Bridge.Boolector" --------------------------------------------------------------------------------- module Data.SBV.Bridge.CVC4 (
Data/SBV/Bridge/Yices.hs view
@@ -9,6 +9,8 @@ -- Interface to the Yices SMT solver. Import this module if you want to use the -- Yices SMT prover as your backend solver. Also see: --+-- - "Data.SBV.Bridge.Boolector"+-- -- - "Data.SBV.Bridge.CVC4" -- -- - "Data.SBV.Bridge.Z3"
Data/SBV/Bridge/Z3.hs view
@@ -9,6 +9,8 @@ -- Interface to the Z3 SMT solver. Import this module if you want to use the -- Z3 SMT prover as your backend solver. Also see: --+-- - "Data.SBV.Bridge.Boolector"+-- -- - "Data.SBV.Bridge.CVC4" -- -- - "Data.SBV.Bridge.Yices"
Data/SBV/Examples/BitPrecise/PrefixSum.hs view
@@ -104,27 +104,29 @@ -- s1 = 0 :: SWord32 -- s2 = 0 :: SWord32 -- s3 = 0 :: SWord32--- s4 = 0 :: SWord32+-- s4 = 1073741824 :: SWord32 -- s5 = 0 :: SWord32 -- s6 = 0 :: SWord32--- s7 = 3221225472 :: SWord32+-- s7 = 0 :: SWord32 -- -- uninterpreted: u -- u = 0 -- -- uninterpreted: flOp--- flOp 0 3221225472 = 2147483648--- flOp 0 2147483648 = 3758096384--- flOp _ _ = 0+-- flOp 0 0 = 2147483648+-- flOp 0 1073741824 = 3221225472+-- flOp 2147483648 0 = 3221225472+-- flOp 2147483648 1073741824 = 1073741824+-- flOp _ _ = 0 ----- You can verify that the above function for @flOp@ is not associative:+-- You can verify that the function @flOp@ is indeed not associative: -- -- @--- ghci> flOp 3221225472 (flOp 2147483648 3221225472)+-- ghci> flOp 3221225472 (flOp 2147483648 1073741824) -- 0--- ghci> flOp (flOp 3221225472 2147483648) 3221225472--- 2147483648+-- ghci> flOp (flOp 3221225472 2147483648) 1073741824+-- 3221225472 -- @ ----- Also, the unit @0@ is clearly not a left-unit for @flOp@, as the third+-- Also, the unit @0@ is clearly not a left-unit for @flOp@, as the last -- equation for @flOp@ will simply map many elements to @0@. -- (NB. We need to use yices for this proof as the uninterpreted function -- examples are only supported through the yices interface currently.)
+ Data/SBV/Examples/Uninterpreted/Shannon.hs view
@@ -0,0 +1,129 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Examples.Uninterpreted.Shannon+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Proves (instances of) Shannon's expansion theorem and other relevant+-- facts. See: <http://en.wikipedia.org/wiki/Shannon's_expansion>+-----------------------------------------------------------------------------++module Data.SBV.Examples.Uninterpreted.Shannon where++import Data.SBV++-----------------------------------------------------------------------------+-- * Boolean functions+-----------------------------------------------------------------------------++-- | A ternary boolean function+type Ternary = SBool -> SBool -> SBool -> SBool++-- | A binary boolean function+type Binary = SBool -> SBool-> SBool++-----------------------------------------------------------------------------+-- * Shannon cofactors+-----------------------------------------------------------------------------++-- | Positive Shannon cofactor of a boolean function, with+-- respect to its first argument+pos :: (SBool -> a) -> a+pos f = f true++-- | Negative Shannon cofactor of a boolean function, with+-- respect to its first argument+neg :: (SBool -> a) -> a+neg f = f false++-----------------------------------------------------------------------------+-- * Shannon expansion theorem+-----------------------------------------------------------------------------++-- | Shannon's expansion over the first argument of a function. We have:+--+-- >>> shannon+-- Q.E.D.+shannon :: IO ThmResult+shannon = prove $ \x y z -> f x y z .== (x &&& pos f y z ||| bnot x &&& neg f y z)+ where f :: Ternary+ f = uninterpret "f"++-- | Alternative form of Shannon's expansion over the first argument of a function. We have:+--+-- >>> shannon2+-- Q.E.D.+shannon2 :: IO ThmResult+shannon2 = prove $ \x y z -> f x y z .== ((x ||| neg f y z) &&& (bnot x ||| pos f y z))+ where f :: Ternary+ f = uninterpret "f"++-----------------------------------------------------------------------------+-- * Derivatives+-----------------------------------------------------------------------------++-- | Computing the derivative of a boolean function (boolean difference).+-- Defined as exclusive-or of Shannon cofactors with respect to that+-- variable.+derivative :: Ternary -> Binary+derivative f y z = pos f y z <+> neg f y z++-- | The no-wiggle theorem: If the derivative of a function with respect to+-- a variable is constant False, then that variable does not "wiggle" the+-- function; i.e., any changes to it won't affect the result of the function.+-- In fact, we have an equivalence: The variable only changes the+-- result of the function iff the derivative with respect to it is not False:+--+-- >>> noWiggle+-- Q.E.D.+noWiggle :: IO ThmResult+noWiggle = prove $ \y z -> bnot (f' y z) <=> pos f y z .== neg f y z+ where f :: Ternary+ f = uninterpret "f"+ f' = derivative f++-----------------------------------------------------------------------------+-- * Universal quantification+-----------------------------------------------------------------------------++-- | Universal quantification of a boolean function with respect to a variable.+-- Simply defined as the conjunction of the Shannon cofactors.+universal :: Ternary -> Binary+universal f y z = pos f y z &&& neg f y z++-- | Show that universal quantification is really meaningful: That is, if the universal+-- quantification with respect to a variable is True, then both cofactors are true for+-- those arguments. Of course, this is a trivial theorem if you think about it for a+-- moment, or you can just let SBV prove it for you:+--+-- >>> univOK+-- Q.E.D.+univOK :: IO ThmResult+univOK = prove $ \y z -> f' y z ==> pos f y z &&& neg f y z+ where f :: Ternary+ f = uninterpret "f"+ f' = universal f++-----------------------------------------------------------------------------+-- * Existential quantification+-----------------------------------------------------------------------------++-- | Existential quantification of a boolean function with respect to a variable.+-- Simply defined as the conjunction of the Shannon cofactors.+existential :: Ternary -> Binary+existential f y z = pos f y z ||| neg f y z++-- | Show that existential quantification is really meaningful: That is, if the existential+-- quantification with respect to a variable is True, then one of the cofactors must be true for+-- those arguments. Again, this is a trivial theorem if you think about it for a moment, but+-- we will just let SBV prove it:+--+-- >>> existsOK+-- Q.E.D.+existsOK :: IO ThmResult+existsOK = prove $ \y z -> f' y z ==> pos f y z ||| neg f y z+ where f :: Ternary+ f = uninterpret "f"+ f' = existential f
+ Data/SBV/Provers/Boolector.hs view
@@ -0,0 +1,83 @@+-----------------------------------------------------------------------------+-- |+-- Module : Data.SBV.Provers.Boolector+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- The connection to the Boolector SMT solver+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}++module Data.SBV.Provers.Boolector(boolector) where++import qualified Control.Exception as C++import Data.Function (on)+import Data.List (sortBy)+import System.Environment (getEnv)+import System.Exit (ExitCode(..))++import Data.SBV.BitVectors.Data+import Data.SBV.SMT.SMT+import Data.SBV.SMT.SMTLib++-- | The description of the Boolector SMT solver+-- The default executable is @\"boolector\"@, which must be in your path. You can use the @SBV_BOOLECTOR@ environment variable to point to the executable on your system.+-- The default options are @\"--lang smt\"@. You can use the @SBV_BOOLECTOR_OPTIONS@ environment variable to override the options.+boolector :: SMTSolver+boolector = SMTSolver {+ name = "boolector"+ , executable = "boolector"+ , options = ["-m", "--smt2"]+ , engine = \cfg _isSat qinps modelMap _skolemMap pgm -> do+ execName <- getEnv "SBV_BOOLECTOR" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg)))+ execOpts <- (words `fmap` getEnv "SBV_BOOLECTOR_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg)))+ let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts}+ , satCmd = satCmd cfg ++ "\n(exit)" -- boolector requires a final exit line+ }+ tweaks = case solverTweaks cfg' of+ [] -> ""+ ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"]+ -- boolector complains if we don't have "exit" at the end+ script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Nothing}+ standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap (map snd qinps) modelMap))+ , xformExitCode = boolectorExitCode+ , capabilities = SolverCapabilities {+ capSolverName = "Boolector"+ , mbDefaultLogic = Nothing+ , supportsMacros = False+ , supportsProduceModels = False+ , supportsQuantifiers = False+ , supportsUninterpretedSorts = False+ , supportsUnboundedInts = False+ , supportsReals = False+ }+ }+ where addTimeOut Nothing o = o+ addTimeOut (Just i) o+ | i < 0 = error $ "Boolector: Timeout value must be non-negative, received: " ++ show i+ | True = o ++ ["-t=" ++ show i]++-- | Similar to CVC4, Boolector uses different exit codes to indicate its status.+boolectorExitCode :: ExitCode -> ExitCode+boolectorExitCode (ExitFailure n) | n `elem` [10, 20, 0] = ExitSuccess+boolectorExitCode ec = ec++extractMap :: [NamedSymVar] -> [(String, UnintKind)] -> [String] -> SMTModel+extractMap inps _modelMap solverLines =+ SMTModel { modelAssocs = map snd $ sortByNodeId $ concatMap (interpretSolverModelLine inps . cvt) solverLines+ , modelUninterps = []+ , modelArrays = []+ }+ where sortByNodeId :: [(Int, a)] -> [(Int, a)]+ sortByNodeId = sortBy (compare `on` fst)+ -- Boolector outputs in a non-parenthesized way; and also puts x's for don't care bits:+ cvt :: String -> String+ cvt s = case words s of+ [var, val] -> "((" ++ var ++ " #b" ++ map tr val ++ "))"+ _ -> s -- good-luck..+ where tr 'x' = '0'+ tr x = x
Data/SBV/Provers/CVC4.hs view
@@ -43,7 +43,16 @@ script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Just (cont skolemMap)} standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap)) , xformExitCode = cvc4ExitCode- , defaultLogic = Just "ALL_SUPPORTED" -- CVC4 is not happy if we don't set the logic, so fall-back to this if necessary+ , capabilities = SolverCapabilities {+ capSolverName = "CVC4"+ , mbDefaultLogic = Just "ALL_SUPPORTED" -- CVC4 is not happy if we don't set the logic, so fall-back to this if necessary+ , supportsMacros = True+ , supportsProduceModels = True+ , supportsQuantifiers = True+ , supportsUninterpretedSorts = True+ , supportsUnboundedInts = True+ , supportsReals = True -- Not quite the same capability as Z3; but works more or less..+ } } where zero :: Kind -> String zero (KBounded False 1) = "#b0"@@ -77,9 +86,9 @@ sortByNodeId = sortBy (compare `on` fst) inps -- for "sat", display the prefix existentials. For completeness, we will drop -- only the trailing foralls. Exception: Don't drop anything if it's all a sequence of foralls- | isSat = if all (== ALL) (map fst qinps)- then map snd qinps- else map snd $ reverse $ dropWhile ((== ALL) . fst) $ reverse qinps+ | isSat = map snd $ if all (== ALL) (map fst qinps)+ then qinps+ else reverse $ dropWhile ((== ALL) . fst) $ reverse qinps -- for "proof", just display the prefix universals | True = map snd $ takeWhile ((== ALL) . fst) qinps -- CVC4 puts quotes around echo's, go figure. strip them here
Data/SBV/Provers/Prover.hs view
@@ -25,7 +25,7 @@ , isVacuous, isVacuousWith , solve , SatModel(..), Modelable(..), displayModels, extractModels- , yices, z3, cvc4, defaultSMTCfg+ , boolector, cvc4, yices, z3, defaultSMTCfg , compileToSMTLib, generateSMTBenchmarks , sbvCheckSolverInstallation ) where@@ -43,14 +43,15 @@ import Data.SBV.BitVectors.Model import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib-import qualified Data.SBV.Provers.CVC4 as CVC4-import qualified Data.SBV.Provers.Yices as Yices-import qualified Data.SBV.Provers.Z3 as Z3+import qualified Data.SBV.Provers.Boolector as Boolector+import qualified Data.SBV.Provers.CVC4 as CVC4+import qualified Data.SBV.Provers.Yices as Yices+import qualified Data.SBV.Provers.Z3 as Z3 import Data.SBV.Utils.TDiff import Data.SBV.Utils.Boolean mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig-mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False+mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False , timing = False , timeOut = Nothing , printBase = 10@@ -62,16 +63,21 @@ , satCmd = "(check-sat)" } +-- | Default configuration for the Boolector SMT solver+boolector :: SMTConfig+boolector = mkConfig Boolector.boolector True []+ -- | Default configuration for the CVC4 SMT Solver. cvc4 :: SMTConfig cvc4 = mkConfig CVC4.cvc4 True []+ -- | Default configuration for the Yices SMT Solver. yices :: SMTConfig yices = mkConfig Yices.yices False [] -- | Default configuration for the Z3 SMT solver z3 :: SMTConfig-z3 = mkConfig Z3.z3 True ["(set-option :mbqi true) ; use model based quantifier instantiation"]+z3 = mkConfig Z3.z3 True ["(set-option :smt.mbqi true) ; use model based quantifier instantiation"] -- | The default solver used by SBV. This is currently set to z3. defaultSMTCfg :: SMTConfig@@ -329,9 +335,9 @@ cvt = if smtLib2 then toSMTLib2 else toSMTLib1 (_, _, _, _, smtLibPgm) <- simulate cvt defaultSMTCfg isSat comments a let out = show smtLibPgm- if smtLib2 -- append check-sat in case of smtLib2- then return $ out ++ "\n(check-sat)\n"- else return $ out ++ "\n"+ return $ out ++ if smtLib2 -- append check-sat in case of smtLib2+ then "\n(check-sat)\n"+ else "\n" -- | Create both SMT-Lib1 and SMT-Lib2 benchmarks. The first argument is the basename of the file, -- SMT-Lib1 version will be written with suffix ".smt1" and SMT-Lib2 version will be written with@@ -448,8 +454,8 @@ runProofOn :: SMTLibConverter -> SMTConfig -> Bool -> [String] -> Result -> IO SMTProblem runProofOn converter config isSat comments res =- let isTiming = timing config- defLogic = defaultLogic (solver config)+ let isTiming = timing config+ solverCaps = capabilities (solver config) in case res of Result boundInfo usorts _qcInfo _codeSegs is consts tbls arrs uis axs pgm cstrs [o@(SW (KBounded False 1) _)] -> timeIf isTiming "translation" $ let uiMap = mapMaybe arrayUIKind arrs ++ map unintFnUIKind uis@@ -461,7 +467,7 @@ where go [] (_, sofar) = reverse sofar go ((ALL, (v, _)):rest) (us, sofar) = go rest (v:us, Left v : sofar) go ((EX, (v, _)):rest) (us, sofar) = go rest (us, Right (v, reverse us) : sofar)- in return (is, uiMap, skolemMap, usorts, converter boundInfo defLogic isSat comments usorts is skolemMap consts tbls arrs uis axs pgm cstrs o)+ in return (is, uiMap, skolemMap, usorts, converter solverCaps boundInfo isSat comments usorts is skolemMap consts tbls arrs uis axs pgm cstrs o) Result _boundInfo _us _qcInfo _codeSegs _is _consts _tbls _arrs _uis _axs _pgm _cstrs os -> case length os of 0 -> error $ "Impossible happened, unexpected non-outputting result\n" ++ show res 1 -> error $ "Impossible happened, non-boolean output in " ++ show os
Data/SBV/Provers/SExpr.hs view
@@ -53,6 +53,8 @@ parseApp r (f : sofar) parseApp (tok:toks) sofar = do t <- pTok tok parseApp toks (t : sofar)+ pTok "false" = return $ SNum 0+ pTok "true" = return $ SNum 1 pTok ('0':'b':r) = mkNum $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r pTok ('b':'v':r) = mkNum $ readDec (takeWhile (/= '[') r) pTok ('#':'b':r) = mkNum $ readInt 2 (`elem` "01") (\c -> ord c - ord '0') r
Data/SBV/Provers/Yices.hs view
@@ -42,7 +42,16 @@ script = SMTScript {scriptBody = unlines (solverTweaks cfg') ++ pgm, scriptModel = Nothing} standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap (map snd qinps) modelMap)) , xformExitCode = id- , defaultLogic = Nothing+ , capabilities = SolverCapabilities {+ capSolverName = "Yices"+ , mbDefaultLogic = Nothing+ , supportsMacros = False+ , supportsProduceModels = False+ , supportsQuantifiers = False+ , supportsUninterpretedSorts = False+ , supportsUnboundedInts = False+ , supportsReals = False+ } } where addTimeOut Nothing o = o addTimeOut (Just i) o
Data/SBV/Provers/Z3.hs view
@@ -49,13 +49,22 @@ [] -> "" ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"] dlim = printRealPrec cfg'- ppDecLim = "(set-option :pp-decimal-precision " ++ show dlim ++ ")\n"+ ppDecLim = "(set-option :pp.decimal_precision " ++ show dlim ++ ")\n" script = SMTScript {scriptBody = tweaks ++ ppDecLim ++ pgm, scriptModel = Just (cont skolemMap)} if dlim < 1 then error $ "SBV.Z3: printRealPrec value should be at least 1, invalid value received: " ++ show dlim else standardSolver cfg' script cleanErrs (ProofError cfg') (interpretSolverOutput cfg' (extractMap isSat qinps modelMap)) , xformExitCode = id- , defaultLogic = Nothing+ , capabilities = SolverCapabilities {+ capSolverName = "Z3"+ , mbDefaultLogic = Nothing+ , supportsMacros = True+ , supportsProduceModels = True+ , supportsQuantifiers = True+ , supportsUninterpretedSorts = True+ , supportsUnboundedInts = True+ , supportsReals = True+ } } where -- Get rid of the following when z3_4.0 is out cleanErrs = intercalate "\n" . filter (not . junk) . lines@@ -76,7 +85,7 @@ extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"] extract (Right (s, [])) = let g = "(get-value (" ++ show s ++ "))" in getVal (kindOf s) g extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ ")))" in getVal (kindOf s) g- getVal KReal g = ["(set-option :pp-decimal false)", g, "(set-option :pp-decimal true)", g]+ getVal KReal g = ["(set-option :pp.decimal false)", g, "(set-option :pp.decimal true)", g] getVal _ g = [g] addTimeOut Nothing o = o addTimeOut (Just i) o@@ -93,9 +102,9 @@ sortByNodeId = sortBy (compare `on` fst) inps -- for "sat", display the prefix existentials. For completeness, we will drop -- only the trailing foralls. Exception: Don't drop anything if it's all a sequence of foralls- | isSat = if all (== ALL) (map fst qinps)- then map snd qinps- else map snd $ reverse $ dropWhile ((== ALL) . fst) $ reverse qinps+ | isSat = map snd $ if all (== ALL) (map fst qinps)+ then qinps+ else reverse $ dropWhile ((== ALL) . fst) $ reverse qinps -- for "proof", just display the prefix universals | True = map snd $ takeWhile ((== ALL) . fst) qinps squashReals :: [(Int, (String, CW))] -> [(Int, (String, CW))]
Data/SBV/SMT/SMT.hs view
@@ -33,7 +33,7 @@ import Data.SBV.BitVectors.PrettyNum import Data.SBV.Utils.TDiff --- | Solver configuration. See also 'z3', 'yices', and 'cvc4', which are instantiations of this type for those solvers, with+-- | Solver configuration. See also 'z3', 'yices', 'cvc4', and 'boolector, which are instantiations of this type for those solvers, with -- reasonable defaults. In particular, custom configuration can be created by varying those values. (Such as @z3{verbose=True}@.) -- -- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does@@ -68,8 +68,8 @@ , executable :: String -- ^ The path to its executable , options :: [String] -- ^ Options to provide to the solver , engine :: SMTEngine -- ^ The solver engine, responsible for interpreting solver output- , defaultLogic :: Maybe String -- ^ Default logic to set, if any , xformExitCode :: ExitCode -> ExitCode -- ^ Should we re-interpret exit codes. Most solvers behave rationally, i.e., id will do. Some (like CVC4) don't.+ , capabilities :: SolverCapabilities -- ^ Various capabilities of the solver } -- | A model, as returned by a solver@@ -409,12 +409,14 @@ runSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String) runSolver cfg execPath opts script | isNothing $ scriptModel script- = readProcessWithExitCode execPath opts (scriptBody script)+ = let checkCmd | useSMTLib2 cfg = '\n' : satCmd cfg+ | True = ""+ in readProcessWithExitCode execPath opts (scriptBody script ++ checkCmd) | True = do (send, ask, cleanUp) <- do (inh, outh, errh, pid) <- runInteractiveProcess execPath opts Nothing Nothing let send l = hPutStr inh (l ++ "\n") >> hFlush inh- recv = hGetLine outh+ recv = hGetLine outh `C.catch` (\(_ :: C.SomeException) -> return "") ask l = send l >> recv cleanUp r = do outMVar <- newEmptyMVar out <- hGetContents outh@@ -429,9 +431,9 @@ ex <- waitForProcess pid -- if the status is unknown, prepare for the possibility of not having a model -- TBD: This is rather crude and potentially Z3 specific- if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err)- then return (ExitSuccess, r , "")- else return (ex, r ++ "\n" ++ out, err)+ return $ if "unknown" `isPrefixOf` r && "error" `isInfixOf` (out ++ err)+ then (ExitSuccess, r , "")+ else (ex, r ++ "\n" ++ out, err) return (send, ask, cleanUp) mapM_ send (lines (scriptBody script)) r <- ask $ satCmd cfg
Data/SBV/SMT/SMTLib.hs view
@@ -19,10 +19,9 @@ import qualified Data.SBV.SMT.SMTLib1 as SMT1 import qualified Data.SBV.SMT.SMTLib2 as SMT2 --- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for--- newer versions in the future.)-type SMTLibConverter = (Bool, Bool) -- ^ has unbounded integers/reals- -> Maybe String -- ^ set-logic string to use in case not automatically determined (if any)+-- | An instance of SMT-Lib converter; instantiated for SMT-Lib v1 and v2. (And potentially for newer versions in the future.)+type SMTLibConverter = SolverCapabilities -- ^ Capabilities of the backend solver targeted+ -> (Bool, Bool) -- ^ has unbounded integers/reals -> Bool -- ^ is this a sat problem? -> [String] -- ^ extra comments to place on top -> [String] -- ^ uninterpreted sorts@@ -44,10 +43,25 @@ -- | Convert to SMTLib-2 format toSMTLib2 :: SMTLibConverter (toSMTLib1, toSMTLib2) = (cvt SMTLib1, cvt SMTLib2)- where cvt v mbDefaultLogic boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out = SMTLibPgm v (aliasTable, pre, post)- where aliasTable = map (\(_, (x, y)) -> (y, x)) qinps+ where cvt v solverCaps boundedInfo@(needsIntegers, needsReals) isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out+ | needsIntegers && not (supportsUnboundedInts solverCaps)+ = unsupported "unbounded integers"+ | needsReals && not (supportsReals solverCaps)+ = unsupported "algebraic reals"+ | needsQuantifiers && not (supportsQuantifiers solverCaps)+ = unsupported "quantifiers"+ | not (null sorts) && not (supportsUninterpretedSorts solverCaps)+ = unsupported "uninterpreted sorts"+ | True+ = SMTLibPgm v (aliasTable, pre, post)+ where unsupported w = error $ "SBV: Given problem needs " ++ w ++ ", which is not supported by SBV for the chosen solver: " ++ capSolverName solverCaps+ aliasTable = map (\(_, (x, y)) -> (y, x)) qinps converter = if v == SMTLib1 then SMT1.cvt else SMT2.cvt- (pre, post) = converter mbDefaultLogic boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out+ (pre, post) = converter solverCaps boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out+ needsQuantifiers+ | isSat = ALL `elem` quantifiers+ | True = EX `elem` quantifiers+ where quantifiers = map fst qinps -- | Add constraints generated from older models, used for querying new models addNonEqConstraints :: [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String
Data/SBV/SMT/SMTLib1.hs view
@@ -40,8 +40,8 @@ nonEq (s, c) = "(not (= " ++ s ++ " " ++ cvtCW c ++ "))" -- | Translate a problem into an SMTLib1 script-cvt :: (Bool, Bool) -- ^ has infinite precision integers/reals- -> Maybe String -- ^ Not used in the SMTLib1 converter+cvt :: SolverCapabilities -- ^ capabilities of the current solver+ -> (Bool, Bool) -- ^ has infinite precision integers/reals -> Bool -- ^ is this a sat problem? -> [String] -- ^ extra comments to place on top -> [String] -- ^ uninterpreted sorts@@ -56,21 +56,8 @@ -> [SW] -- ^ extra constraints -> SW -- ^ output variable -> ([String], [String])-cvt (hasIntegers, hasReals) _mbDefaultLogic isSat comments sorts qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out- | hasIntegers- = error "SBV: Unbounded integers are not supported in the SMTLib1/yices interface."- | hasReals- = error "SBV: The real value domain is not supported in the SMTLib1/yices interface."- | not ((isSat && allExistential) || (not isSat && allUniversal))- = error "SBV: The chosen solver does not support quantified variables."- | not (null sorts)- = error "SBV: The chosen solver does not support unintepreted sorts."- | True- = (pre, post)- where quantifiers = map fst qinps- allExistential = all (== EX) quantifiers- allUniversal = all (== ALL) quantifiers- logic+cvt _solverCaps _boundInfo isSat comments _sorts qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out = (pre, post)+ where logic | null tbls && null arrs && null uis = "QF_BV" | True = "QF_AUFBV" inps = map (fst . snd) qinps@@ -103,7 +90,7 @@ ++ [mkFormula isSat out] ++ [")"] asgns = F.toList (pgmAssignments asgnsSeq)- mkCstr s = " :assumption (= " ++ show s ++ " bv1[1])"+ mkCstr s = " :assumption " ++ show s -- TODO: Does this work for SMT-Lib when the index/element types are signed? -- Currently we ignore the signedness of the arguments, as there appears to be no way@@ -133,9 +120,9 @@ ArrayFree (Just sw) -> declA sw ArrayReset _ sw -> declA sw ArrayMutate j a b -> [" :assumption (= " ++ nm ++ " (store array_" ++ show j ++ " " ++ show a ++ " " ++ show b ++ "))"]- ArrayMerge t j k -> [" :assumption (= " ++ nm ++ " (ite (= bv1[1] " ++ show t ++ ") array_" ++ show j ++ " array_" ++ show k ++ "))"]+ ArrayMerge t j k -> [" :assumption (= " ++ nm ++ " (ite " ++ show t ++ " array_" ++ show j ++ " array_" ++ show k ++ "))"] declA sw = let iv = nm ++ "_freeInitializer"- in [ " :extrafuns ((" ++ iv ++ " BitVec[" ++ show at ++ "]))"+ in [ " :extrafuns ((" ++ iv ++ " " ++ kindType ak ++ "))" , " :assumption (= (select " ++ nm ++ " " ++ iv ++ ") " ++ show sw ++ ")" ] @@ -147,12 +134,14 @@ mkFormula :: Bool -> SW -> String mkFormula isSat s- | isSat = " :formula (= " ++ show s ++ " bv1[1])"- | True = " :formula (= " ++ show s ++ " bv0[1])"+ | isSat = " :formula " ++ show s+ | True = " :formula (not " ++ show s ++ ")" -- SMTLib represents signed/unsigned quantities with the same type decl :: SW -> String-decl s = " :extrafuns ((" ++ show s ++ " BitVec[" ++ show (intSizeOf s) ++ "]))"+decl s+ | isBoolean s = " :extrapreds ((" ++ show s ++ "))"+ | True = " :extrafuns ((" ++ show s ++ " " ++ kindType (kindOf s) ++ "))" cvtAsgn :: (SW, SBVExpr) -> String cvtAsgn (s, e) = " :assumption (= " ++ show s ++ " " ++ cvtExp e ++ ")"@@ -162,6 +151,7 @@ -- no need to worry about Int/Real here as we don't support them with the SMTLib1 interface.. cvtCW :: CW -> String+cvtCW (CW (KBounded False 1) (CWInteger v)) = if v == 0 then "false" else "true" cvtCW x@(CW _ (CWInteger v)) | not (hasSign x) = "bv" ++ show v ++ "[" ++ show (intSizeOf x) ++ "]" -- signed numbers (with 2's complement representation) is problematic -- since there's no way to put a bvneg over a positive number to get minBound..@@ -191,7 +181,7 @@ o = if s then oS else oW cvtExp :: SBVExpr -> String-cvtExp (SBVApp Ite [a, b, c]) = "(ite (= bv1[1] " ++ show a ++ ") " ++ show b ++ " " ++ show c ++ ")"+cvtExp (SBVApp Ite [a, b, c]) = "(ite " ++ show a ++ " " ++ show b ++ " " ++ show c ++ ")" cvtExp (SBVApp (Rol i) [a]) = rot "rotate_left" i a cvtExp (SBVApp (Ror i) [a]) = rot "rotate_right" i a cvtExp (SBVApp (Shl i) [a]) = shft "bvshl" "bvshl" i a@@ -212,48 +202,66 @@ le0 = "(" ++ less ++ " " ++ show i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ show i ++ ")" cvtExp (SBVApp (Extract i j) [a]) = "(extract[" ++ show i ++ ":" ++ show j ++ "] " ++ show a ++ ")"-cvtExp (SBVApp (ArrEq i j) []) = "(ite (= array_" ++ show i ++ " array_" ++ show j ++") bv1[1] bv0[1])"+cvtExp (SBVApp (ArrEq i j) []) = "(= array_" ++ show i ++ " array_" ++ show j ++")" cvtExp (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ show a ++ ")" cvtExp (SBVApp (Uninterpreted nm) []) = "uninterpreted_" ++ nm cvtExp (SBVApp (Uninterpreted nm) args) = "(uninterpreted_" ++ nm ++ " " ++ unwords (map show args) ++ ")" cvtExp inp@(SBVApp op args) | Just f <- lookup op smtOpTable- = f (any hasSign args) (map show args)+ = f (any hasSign args) (all isBoolean args) (map show args) | True = error $ "SBV.SMT.SMTLib1.cvtExp: impossible happened; can't translate: " ++ show inp- where lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")"- lift2 o _ sbvs = error $ "SBV.SMTLib1.cvtExp.lift2: Unexpected arguments: " ++ show (o, sbvs)- lift2B oU oS sgn sbvs = "(ite " ++ lift2S oU oS sgn sbvs ++ " bv1[1] bv0[1])"- lift2S oU oS sgn sbvs+ where lift2 o _ _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")"+ lift2 o _ _ sbvs = error $ "SBV.SMTLib1.cvtExp.lift2: Unexpected arguments: " ++ show (o, sbvs)+ lift2S oU oS sgn isB sbvs | sgn- = lift2 oS sgn sbvs+ = lift2 oS sgn isB sbvs | True- = lift2 oU sgn sbvs- lift2N o sgn sbvs = "(bvnot " ++ lift2 o sgn sbvs ++ ")"- lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")"- lift1 o _ sbvs = error $ "SBV.SMT.SMTLib1.cvtExp.lift1: Unexpected arguments: " ++ show (o, sbvs)+ = lift2 oU sgn isB sbvs+ lift1 o _ _ [x] = "(" ++ o ++ " " ++ x ++ ")"+ lift1 o _ _ sbvs = error $ "SBV.SMT.SMTLib1.cvtExp.lift1: Unexpected arguments: " ++ show (o, sbvs)+ -- ops that distinguish 1-bit bitvectors (boolean) from others+ lift2B bOp vOp sgn isB sbvs+ | isB+ = lift2 bOp sgn isB sbvs+ | True+ = lift2 vOp sgn isB sbvs+ lift1B bOp vOp sgn isB sbvs+ | isB+ = lift1 bOp sgn isB sbvs+ | True+ = lift1 vOp sgn isB sbvs+ eq sgn isB sbvs+ | isB+ = lift2 "=" sgn isB sbvs+ | True+ = "(= " ++ lift2 "bvcomp" sgn isB sbvs ++ " bv1[1])"+ neq sgn isB sbvs = "(not " ++ eq sgn isB sbvs ++ ")" smtOpTable = [ (Plus, lift2 "bvadd") , (Minus, lift2 "bvsub") , (Times, lift2 "bvmul") , (Quot, lift2S "bvudiv" "bvsdiv") , (Rem, lift2S "bvurem" "bvsrem")- , (Equal, lift2 "bvcomp")- , (NotEqual, lift2N "bvcomp")- , (LessThan, lift2B "bvult" "bvslt")- , (GreaterThan, lift2B "bvugt" "bvsgt")- , (LessEq, lift2B "bvule" "bvsle")- , (GreaterEq, lift2B "bvuge" "bvsge")- , (And, lift2 "bvand")- , (Or, lift2 "bvor")- , (XOr, lift2 "bvxor")- , (Not, lift1 "bvnot")+ , (Equal, eq)+ , (NotEqual, neq)+ , (LessThan, lift2S "bvult" "bvslt")+ , (GreaterThan, lift2S "bvugt" "bvsgt")+ , (LessEq, lift2S "bvule" "bvsle")+ , (GreaterEq, lift2S "bvuge" "bvsge")+ , (And, lift2B "and" "bvand")+ , (Or, lift2B "or" "bvor")+ , (Not, lift1B "not" "bvnot")+ , (XOr, lift2B "xor" "bvxor") , (Join, lift2 "concat") ] cvtType :: SBVType -> String cvtType (SBVType []) = error "SBV.SMT.SMTLib1.cvtType: internal: received an empty type!"-cvtType (SBVType xs) = unwords $ map sh xs- where sh (KBounded _ s) = "BitVec[" ++ show s ++ "]"- sh KUnbounded = die "unbounded Integer"- sh KReal = die "real value"- sh (KUninterpreted s) = die $ "uninterpreted sort: " ++ s+cvtType (SBVType xs) = unwords $ map kindType xs++kindType :: Kind -> String+kindType (KBounded False 1) = "Bool"+kindType (KBounded _ s) = "BitVec[" ++ show s ++ "]"+kindType KUnbounded = die "unbounded Integer"+kindType KReal = die "real value"+kindType (KUninterpreted s) = die $ "uninterpreted sort: " ++ s
Data/SBV/SMT/SMTLib2.hs view
@@ -57,8 +57,8 @@ tbd e = error $ "SBV.SMTLib2: Not-yet-supported: " ++ e -- | Translate a problem into an SMTLib2 script-cvt :: (Bool, Bool) -- ^ has infinite precision values- -> Maybe String -- ^ set-logic string to use in case not automatically determined (if any)+cvt :: SolverCapabilities -- ^ capabilities of the current solver+ -> (Bool, Bool) -- ^ bounded info -> Bool -- ^ is this a sat problem? -> [String] -- ^ extra comments to place on top -> [String] -- ^ uninterpreted sorts@@ -73,11 +73,11 @@ -> [SW] -- ^ extra constraints -> SW -- ^ output variable -> ([String], [String])-cvt (hasInteger, hasReal) mbDefaultLogic isSat comments sorts _inps skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, [])+cvt solverCaps (hasInteger, hasReal) isSat comments sorts _inps skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, []) where -- the logic is an over-approaximation logic | hasInteger || hasReal || not (null sorts)- = case mbDefaultLogic of+ = case mbDefaultLogic solverCaps of Nothing -> ["; Has unbounded values (Int/Real) or sorts; no logic specified."] -- combination, let the solver pick Just l -> ["(set-logic " ++ l ++ ")"] | True@@ -88,15 +88,17 @@ | True = "A" ufs | null uis && null tbls = "" -- we represent tables as UFs | True = "UF"+ getModels+ | supportsProduceModels solverCaps = ["(set-option :produce-models true)"]+ | True = [] pre = ["; Automatically generated by SBV. Do not edit."] ++ map ("; " ++) comments- ++ [ "(set-option :produce-models true)"- ]+ ++ getModels ++ logic ++ [ "; --- uninterpreted sorts ---" ] ++ map declSort sorts ++ [ "; --- literal constants ---" ]- ++ map declConst consts+ ++ concatMap (declConst (supportsMacros solverCaps)) consts ++ [ "; --- skolem constants ---" ] ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType ss s ++ ")" | Right (s, ss) <- skolemInps] ++ [ "; --- constant tables ---" ]@@ -136,7 +138,7 @@ assertOut | null cstrs = o | True = "(and " ++ unwords (map mkConj cstrs ++ [o]) ++ ")"- where mkConj x = "(= " ++ cvtSW skolemMap x ++ " #b1)"+ where mkConj = cvtSW skolemMap o | isSat = mkConj out | True = "(not " ++ mkConj out ++ ")" skolemMap = M.fromList [(s, ss) | Right (s, ss) <- skolemInps, not (null ss)]@@ -145,7 +147,12 @@ mkSkTable (((t, _, _), _), _) = (t, "table" ++ show t ++ forallArgs) asgns = F.toList asgnsSeq mkLet (s, e) = "(let ((" ++ show s ++ " " ++ cvtExp skolemMap tableMap e ++ "))"- declConst (s, c) = "(define-fun " ++ show s ++ " " ++ swFunType [] s ++ " " ++ cvtCW c ++ ")"+ declConst useDefFun (s, c)+ | useDefFun = ["(define-fun " ++ varT ++ " " ++ cvtCW c ++ ")"]+ | True = [ "(declare-fun " ++ varT ++ ")"+ , "(assert (= " ++ show s ++ " " ++ cvtCW c ++ "))"+ ]+ where varT = show s ++ " " ++ swFunType [] s declSort s = "(declare-sort " ++ s ++ " 0)" declUI :: (String, SBVType) -> [String]@@ -200,15 +207,15 @@ = cvtSW skolemMap sw | True = tbd "Non-constant array initializer in a quantified context"- adecl = "(declare-fun " ++ nm ++ "() (Array " ++ smtType aKnd ++ " " ++ smtType bKnd ++ "))"+ adecl = "(declare-fun " ++ nm ++ " () (Array " ++ smtType aKnd ++ " " ++ smtType bKnd ++ "))" ctxInfo = case ctx of ArrayFree Nothing -> [] ArrayFree (Just sw) -> declA sw ArrayReset _ sw -> declA sw ArrayMutate j a b -> [(all (`elem` consts) [a, b], "(= " ++ nm ++ " (store array_" ++ show j ++ " " ++ ssw a ++ " " ++ ssw b ++ "))")]- ArrayMerge t j k -> [(t `elem` consts, "(= " ++ nm ++ " (ite (= #b1 " ++ ssw t ++ ") array_" ++ show j ++ " array_" ++ show k ++ "))")]+ ArrayMerge t j k -> [(t `elem` consts, "(= " ++ nm ++ " (ite " ++ ssw t ++ " array_" ++ show j ++ " array_" ++ show k ++ "))")] declA sw = let iv = nm ++ "_freeInitializer"- in [ (True, "(declare-fun " ++ iv ++ "() " ++ smtType aKnd ++ ")")+ in [ (True, "(declare-fun " ++ iv ++ " () " ++ smtType aKnd ++ ")") , (sw `elem` consts, "(= (select " ++ nm ++ " " ++ iv ++ ") " ++ ssw sw ++ ")") ] wrap (False, s) = s@@ -221,6 +228,7 @@ swFunType ss s = "(" ++ unwords (map swType ss) ++ ") " ++ swType s smtType :: Kind -> String+smtType (KBounded False 1) = "Bool" smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")" smtType KUnbounded = "Int" smtType KReal = "Real"@@ -248,6 +256,8 @@ where pad n s = replicate (n - length s) '0' ++ s cvtCW :: CW -> String+cvtCW x | isBoolean x = if w == 0 then "false" else "true"+ where CWInteger w = cwVal x cvtCW x | isUninterpreted x = s where CWUninterpreted s = cwVal x cvtCW x | isReal x = algRealToSMTLib2 w@@ -284,17 +294,26 @@ bvOp = all isBounded arguments intOp = any isInteger arguments realOp = any isReal arguments+ boolOp = all isBoolean arguments bad | intOp = error $ "SBV.SMTLib2: Unsupported operation on unbounded integers: " ++ show expr | True = error $ "SBV.SMTLib2: Unsupported operation on real values: " ++ show expr ensureBV = bvOp || bad lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs)- lift2B oU oS sgn sbvs = "(ite " ++ lift2S oU oS sgn sbvs ++ " #b1 #b0)"+ lift2B bOp vOp+ | boolOp = lift2 bOp+ | True = lift2 vOp+ lift1B bOp vOp+ | boolOp = lift1 bOp+ | True = lift1 vOp+ eq sgn sbvs+ | boolOp = lift2 "=" sgn sbvs+ | True = "(= " ++ lift2 "bvcomp" sgn sbvs ++ " #b1)"+ neq sgn sbvs = "(not " ++ eq sgn sbvs ++ ")" lift2S oU oS sgn = lift2 (if sgn then oS else oU) sgn- lift2N o sgn sbvs = "(bvnot " ++ lift2 o sgn sbvs ++ ")" lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")" lift1 o _ sbvs = error $ "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs)- sh (SBVApp Ite [a, b, c]) = "(ite (= #b1 " ++ ssw a ++ ") " ++ ssw b ++ " " ++ ssw c ++ ")"+ sh (SBVApp Ite [a, b, c]) = "(ite " ++ ssw a ++ " " ++ ssw b ++ " " ++ ssw c ++ ")" sh (SBVApp (LkUp (t, aKnd, _, l) i e) []) | needsCheck = "(ite " ++ cond ++ ssw e ++ " " ++ lkUp ++ ")" | True = lkUp@@ -315,7 +334,7 @@ mkCnst = cvtCW . mkConstCW (kindOf i) le0 = "(" ++ less ++ " " ++ ssw i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ ssw i ++ ")"- sh (SBVApp (ArrEq i j) []) = "(ite (= array_" ++ show i ++ " array_" ++ show j ++") #b1 #b0)"+ sh (SBVApp (ArrEq i j) []) = "(= array_" ++ show i ++ " array_" ++ show j ++")" sh (SBVApp (ArrRead i) [a]) = "(select array_" ++ show i ++ " " ++ ssw a ++ ")" sh (SBVApp (Uninterpreted nm) []) = nm sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm ++ " " ++ unwords (map ssw args) ++ ")"@@ -347,10 +366,10 @@ where -- The first 4 operators below do make sense for Integer's in Haskell, but there's -- no obvious counterpart for them in the SMTLib translation. -- TODO: provide support for these.- smtBVOpTable = [ (And, lift2 "bvand")- , (Or, lift2 "bvor")- , (XOr, lift2 "bvxor")- , (Not, lift1 "bvnot")+ smtBVOpTable = [ (And, lift2B "and" "bvand")+ , (Or, lift2B "or" "bvor")+ , (XOr, lift2B "xor" "bvxor")+ , (Not, lift1B "not" "bvnot") , (Join, lift2 "concat") ] sh inp@(SBVApp op args)@@ -369,12 +388,12 @@ , (Times, lift2 "bvmul") , (Quot, lift2S "bvudiv" "bvsdiv") , (Rem, lift2S "bvurem" "bvsrem")- , (Equal, lift2 "bvcomp")- , (NotEqual, lift2N "bvcomp")- , (LessThan, lift2B "bvult" "bvslt")- , (GreaterThan, lift2B "bvugt" "bvsgt")- , (LessEq, lift2B "bvule" "bvsle")- , (GreaterEq, lift2B "bvuge" "bvsge")+ , (Equal, eq)+ , (NotEqual, neq)+ , (LessThan, lift2S "bvult" "bvslt")+ , (GreaterThan, lift2S "bvugt" "bvsgt")+ , (LessEq, lift2S "bvule" "bvsle")+ , (GreaterEq, lift2S "bvuge" "bvsge") ] smtOpRealTable = smtIntRealShared ++ [ (Quot, lift2 "/")@@ -386,16 +405,16 @@ smtIntRealShared = [ (Plus, lift2 "+") , (Minus, lift2 "-") , (Times, lift2 "*")- , (Equal, lift2B "=" "=")- , (NotEqual, lift2B "distinct" "distinct")- , (LessThan, lift2B "<" "<")- , (GreaterThan, lift2B ">" ">")- , (LessEq, lift2B "<=" "<=")- , (GreaterEq, lift2B ">=" ">=")+ , (Equal, lift2S "=" "=")+ , (NotEqual, lift2S "distinct" "distinct")+ , (LessThan, lift2S "<" "<")+ , (GreaterThan, lift2S ">" ">")+ , (LessEq, lift2S "<=" "<=")+ , (GreaterEq, lift2S ">=" ">=") ] -- equality is the only thing that works on uninterpreted sorts- uninterpretedTable = [ (Equal, lift2B "=" "=" True)- , (NotEqual, lift2B "distinct" "distinct" True)+ uninterpretedTable = [ (Equal, lift2S "=" "=" True)+ , (NotEqual, lift2S "distinct" "distinct" True) ] rot :: (SW -> String) -> String -> Int -> SW -> String
− README
@@ -1,4 +0,0 @@-SBV: SMT Based Verification in Haskell-======================================--Please see: http://leventerkok.github.com/sbv/
+ README.md view
@@ -0,0 +1,4 @@+SBV: SMT Based Verification in Haskell+======================================++Please see: http://leventerkok.github.com/sbv/
− RELEASENOTES
@@ -1,524 +0,0 @@-Hackage: <http://hackage.haskell.org/package/sbv>-GitHub: <http://leventerkok.github.com/sbv/>--Latest Hackage released version: 2.9--======================================================================-Version 2.9, 2013-01-02-- - Add support for the CVC4 SMT solver from New York University and- the University of Iowa. (http://cvc4.cs.nyu.edu/).- NB. Z3 remains the default solver for SBV. To use CVC4, use the- *With variants of the interface (i.e., proveWith, satWith, ..)- by passing cvc4 as the solver argument. (Similarly, use 'yices'- as the argument for the *With functions for invoking yices.)- - Latest release of Yices calls the SMT-Lib based solver executable- yices-smt. Updated the default value of the executable to have this- name for ease of use.- - Add an extra boolean flag to compileToSMTLib and generateSMTBenchmarks- functions to control if the translation should keep the query as is- (for SAT cases), or negate it (for PROVE cases). Previously, this value- was hard-coded to do the PROVE case only.- - Add bridge modules, to simplify use of different solvers. You can now say:-- import Data.SBV.Bridge.CVC4- import Data.SBV.Bridge.Yices- import Data.SBV.Bridge.Z3- - to pick the appropriate default solver. if you simply 'import Data.SBV', then- you will get the default SMT solver, which is currently Z3. The value- 'defaultSMTSolver' refers to z3 (currently), and 'sbvCurrentSolver' refers- to the chosen solver as determined by the imported module. (The latter is- useful for modifying options to the SMT solver in an solver-agnostic way.)- - Various improvements to Z3 model parsing routines.- - New web page for SBV: http://leventerkok.github.com/sbv/ is now online.--======================================================================-Version 2.8, 2012-11-29-- - Rename the SNum class to SIntegral, and make it index over regular- types. This makes it much more useful, simplifying coding of- polymorphic symbolic functions over integral types, which is- the common case.- - Add the functions:- - sbvShiftLeft- - sbvShiftRight- which can accommodate unsigned symbolic shift amounts. Note that- one cannot use Haskell's shiftL/shiftR from the Bits class since- they are hard-wired to take 'Int' values as the shift amounts only.- - Add a new function 'sbvArithShiftRight', which is the same as- a shift-right, except it uses the MSB of the input as the bit to fill- in (instead of always filling in with 0 bits). Note that this is- the same as shiftRight for signed values, but differs from a shiftRight- when the input is unsigned. (There is no Haskell analogue of this- function, as Haskell's shiftR is always arithmetic for signed- types and logical for unsigned ones.) This variant is designed for- use cases when one uses the underlying unsigned SMT-Lib representation- to implement custom signed operations, for instance.- - Several typo fixes.--======================================================================-Version 2.7, 2012-10-21-- - Add missing QuickCheck instance for SReal- - When dealing with concrete SReal's, make sure to operate- only on exact algebraic reals on the Haskell side, leaving- true algebraic reals (i.e., those that are roots of polynomials- that cannot be expressed as a rational) symbolic. This avoids- issues with functions that we cannot implement directly on- the Haskell side, like exact square-roots.- - Documentation tweaks, typo fixes etc.- - Rename BVDivisible class to SDivisible; since SInteger- is also an instance of this class, and SDivisible is a- more appropriate name to start with. Also add sQuot and sRem- methods; along with sDivMod, sDiv, and sMod, with usual- semantics. - - Improve test suite, adding many constant-folding tests- and start using cabal based tests (--enable-tests option.)--======================================================================-Versions 2.4, 2.5, and 2.6: Around mid October 2012-- - Workaround issues related hackage compilation, in particular to the- problem with the new containers package release, which does provide- an NFData instance for sequences.- - Add explicit Num requirements when necessary, as the Bits class- no longer does this.- - Remove dependency on the hackage package strict-concurrency, as- hackage can no longer compile it due to some dependency mismatch.- - Add forgotten Real class instance for the type 'AlgReal'- - Stop putting bounds on hackage dependencies, as they cause- more trouble then they actually help. (See the discussion- here: http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html.)--======================================================================-Version 2.3, 2012-07-20-- - Maintanence release, no new features.- - Tweak cabal dependencies to avoid using packages that are newer- than those that come with ghc-7.4.2. Apparently this is a no-no- that breaks many things, see the discussion in this thread:- http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html- In particular, the use of containers >= 0.5 is *not* OK until we have- a version of GHC that comes with that version.--======================================================================-Version 2.2, 2012-07-17-- - Maintanence release, no new features.- - Update cabal dependencies, in particular fix the- regression with respect to latest version of the- containers package.--======================================================================-Version 2.1, 2012-05-24-- Library:- - Add support for uninterpreted sorts, together with user defined- domain axioms. See Data.SBV.Examples.Uninterpreted.Sort- and Data.SBV.Examples.Uninterpreted.Deduce for basic examples of- this feature.- - Add support for C code-generation with SReals. The user picks- one of 3 possible C types for the SReal type: CgFloat, CgDouble- or CgLongDouble, using the function cgSRealType. Naturally, the- resulting C program will suffer a loss of precision, as it will- be subject to IEE-754 rounding as implied by the underlying type.- - Add toSReal :: SInteger -> SReal, which can be used to promote- symbolic integers to reals. Comes handy in mixed integer/real- computations.- Examples:- - Recast the dog-cat-mouse example to use the solver over reals.- - Add Data.SBV.Examples.Uninterpreted.Sort, and- Data.SBV.Examples.Uninterpreted.Deduce- for illustrating uninterpreted sorts and axioms.--======================================================================-Version 2.0, 2012-05-10- - This is a major release of SBV, adding support for symbolic algebraic reals: SReal.- See http://en.wikipedia.org/wiki/Algebraic_number for details. In brief, algebraic- reals are solutions to univariate polynomials with rational coefficients. The arithmetic- on algebraic reals is precise, with no approximation errors. Note that algebraic reals- are a proper subset of all reals, in particular transcendental numbers are not- representable in this way. (For instance, "sqrt 2" is algebraic, but pi, e are not.)- However, algebraic reals is a superset of rationals, so SBV now also supports symbolic- rationals as well.- - You *should* use Z3 v4.0 when working with real numbers. While the interface will- work with older versions of Z3 (or other SMT solvers in general), it uses Z3's- root-obj construct to retrieve and query algebraic reals.-- While SReal values have infinite precision, printing such values is not trivial since- we might need an infinite number of digits if the result happens to be irrational. The- user controls printing precision, by specifying how many digits after the decimal point- should be printed. The default number of decimal digits to print is 10. (See the- 'printRealPrec' field of SMT-solver configuration.)-- The acronym SBV used to stand for Symbolic Bit Vectors. However, SBV has grown beyond- bit-vectors, especially with the addition of support for SInteger and SReal types and- other code-generation utilities. Therefore, "SMT Based Verification" is now a better fit- for the expansion of the acronym SBV.-- Other notable changes in the library:- * Add functions s[TYPE] and s[TYPE]s for each symbolic type we support (i.e.,- sBool, sBools, sWord8, sWord8s, etc.), to create symbolic variables of the- right kind. Strictly speaking these are just synonyms for 'free'- and 'mapM free' (plural versions), so they aren't adding any additional- power. Except, they are specialized at their respective types, and might be- easier to remember.- * Add function solve, which is merely a synonym for (return . bAnd), but- it simplifies expressing problems.- * Add class SNum, which simplifies writing polymorphic code over symbolic values- * Increase haddock coverage metrics- * Major code refactoring around symbolic kinds- * SMTLib2: Emit ":produce-models" call before setting the logic, as required- by the SMT-Lib2 standard. [Patch provided by arrowdodger on github, thanks!]-- Bugs fixed:- * [Performance] Use a much simpler default definition for "select": While the- older version (based on binary search on the bits of the indexer) was correct,- it created unnecessarily big expressions. Since SBV does not have a notion- of concrete subwords, the binary-search trick was not bringing any advantage- in any case. Instead, we now simply use a linear walk over the elements.-- Examples:- * Change dog-cat-mouse example to use SInteger for the counts- * Add merge-sort example: Data.SBV.Examples.BitPrecise.MergeSort- * Add diophantine solver example: Data.SBV.Examples.Existentials.Diophantine--======================================================================-Version 1.4, 2012-05-10-- * Interim release for test purposes--======================================================================-Version 1.3, 2012-02-25-- * Workaround cabal/hackage issue, functionally the same as release- 1.2 below--======================================================================-Version 1.2, 2012-02-25-- Library:- * Add a hook so users can add custom script segments for SMT solvers. The new- "solverTweaks" field in the SMTConfig data-type can be used for this purpose.- The need for this came about due to the need to workaround a Z3 v3.2 issue- detalied below:- http://stackoverflow.com/questions/9426420/soundness-issue-with-integer-bv-mixed-benchmarks- As a consequence, mixed Integer/BV problems can cause soundness issues in Z3- and does in SBV. Unfortunately, it's too severe for SBV to add the woraround- option, as it slows down the solver as a side effect as well. Thus, we're- making this optionally available if/when needed. (Note that the work-around- should not be necessary with Z3 v3.3; which isn't released yet.)- * Other minor clean-up--======================================================================-Version 1.1, 2012-02-14-- Library:- * Rename bitValue to sbvTestBit- * Add sbvPopCount- * Add a custom implementation of 'popCount' for the Bits class- instance of SBV (GHC >= 7.4.1 only)- * Add 'sbvCheckSolverInstallation', which can be used to check- that the given solver is installed and good to go.- * Add 'generateSMTBenchmarks', simplifying the generation of- SMTLib benchmarks for offline sharing.--======================================================================-Version 1.0, 2012-02-13-- Library:- * Z3 is now the "default" SMT solver. Yices is still available, but- has to be specifically selected. (Use satWith, allSatWith, proveWith, etc.)- * Better handling of the pConstrain probability threshold for test- case generation and quickCheck purposes.- * Add 'renderTest', which accompanies 'genTest' to render test- vectors as Haskell/C/Forte program segments.- * Add 'expectedValue' which can compute the expected value of- a symbolic value under the given constraints. Useful for statistical- analysis and probability computations.- * When saturating provable values, use forAll_ for proofs and forSome_- for sat/allSat. (Previously we were allways using forAll_, which is- not incorrect but less intuitive.)- * add function:- extractModels :: SatModel a => AllSatResult -> [a]- which simplifies accessing allSat results greatly.- Code-generation:- * add "cgGenerateMakefile" which allows the user to choose if SBV- should generate a Makefile. (default: True)- Other- * Changes to make it compile with GHC 7.4.1.--======================================================================-Version 0.9.24, 2011-12-28-- Library:- * Add "forSome," analogous to "forAll." (The name "exists" would've- been better, but it's already taken.) This is not as useful as- one might think as forAll and forSome do not nest, as an inner- application of one pushes its argument to a Predicate, making- the outer one useless, but it's nonetheless useful by itself.- * Add a "Modelable" class, which simplifies model extraction.- * Add support for quick-check at the "Symbolic SBool" level. Previously- SBV only allowed functions returning SBool to be quick-checked, which- forced a certain style of coding. In particular with the addition- of quantifiers, the new coding style mostly puts the top-level- expressions in the Symbolic monad, which were not quick-checkable- before. With new support, the quickCheck, prove, sat, and allSat- commands are all interchangeable with obvious meanings.- * Add support for concrete test case generation, see the genTest function.- * Improve optimize routines and add support for iterative optimization.- * Add "constrain", simplifying conjunctive constraints, especially- useful for adding constraints at variable generation time via- forall/exists. Note that the interpretation of such constraints- is different for genTest and quickCheck functions, where constraints- will be used for appropriately filtering acceptable test values- in those two cases.- * Add "pConstrain", which probabilistically adds constraints. This- is useful for quickCheck and genTest functions for filtering acceptable- test values. (Calls to pConstrain will be rejected for sat/prove calls.)- * Add "isVacuous" which can be used to check that the constraints added- via constrain are satisfable. This is useful to prevent vacuous passes,- i.e., when a proof is not just passing because the constraints imposed- are inconsistent. (Also added accompanying isVacuousWith.)- * Add "free" and "free_", analogous to "forall/forall_" and "exists/exists_"- The difference is that free behaves universally in a proof context, while- it behaves existentially in a sat context. This allows us to express- properties more succinctly, since the intended semantics is usually this- way depending on the context. (i.e., in a proof, we want our variables- universal, in a sat call existential.) Of course, exists/forall are still- available when mixed quantifiers are needed, or when the user wants to- be explicit about the quantifiers.- Examples- * Add Data/SBV/Examples/Puzzles/Coins.hs. (Shows the usage of "constrain".)- Dependencies- * Bump up random package dependency to 1.0.1.1 (from 1.0.0.2)- Internal- * Major reorganization of files to and build infrastructure to- decrease build times and better layout- * Get rid of custom Setup.hs, just use simple build. The extra work- was not worth the complexity.--======================================================================-Version 0.9.23, 2011-12-05- - Library:- * Add support for SInteger, the type of signed unbounded integer- values. SBV can now prove theorems about unbounded numbers,- following the semantics of Haskell's Integer type. (Requires z3 to- be used as the backend solver.)- * Add functions 'optimize', 'maximize', and 'minimize' that can- be used to find optimal solutions to given constraints with- respect to a given cost function.- * Add 'cgUninterpret', which simplifies code generation when we want- to use an alternate definition in the target language (i.e., C). This- is important for efficient code generation, when we want to- take advantage of native libraries available in the target platform.- Other:- * Change getModel to return a tuple in the success case, where- the first component is a boolean indicating whether the model- is "potential." This is used to indicate that the solver- actually returned "unknown" for the problem and the model- might therefore be bogus. Note that we did not need this before- since we only supported bounded bit-vectors, which has a decidable- theory. With the addition of unbounded Integer's and quantifiers, the- solvers can now return unknown. This should still be rare in practice,- but can happen with the use of non-linear constructs. (i.e.,- multiplication of two variables.)--======================================================================-Version 0.9.22, 2011-11-13- - The major change in this release is the support for quantifiers. The- SBV library *no* longer assumes all variables are universals in a proof,- (and correspondingly existential in a sat) call. Instead, the user- marks free-variables appropriately using forall/exists functions, and the- solver translates them accordingly. Note that this is a non-backwards- compatible change in sat calls, as the semantics of formulas is essentially- changing. While this is unfortunate, it's more uniform and simpler to understand- in general.-- This release also adds support for the Z3 solver, which is the main- SMT-solver used for solving formulas involving quantifiers. More formally,- we use the new AUFBV/ABV/UFBV logics when quantifiers are involved. Also, - the communication with Z3 is now done via SMT-Lib2 format. Eventually- the SMTLib1 connection will be severed.-- The other main change is the support for C code generation with- uninterpreted functions enabling users to interface with external- C functions defined elsewhere. See below for details.-- Other changes:- Code:- * Change getModel, so it returns an Either value to indicate- something went wrong; instead of throwing an error- * Add support for computing CRCs directly (without needing- polynomial division).- Code generation:- * Add "cgGenerateDriver" function, which can be used to turn- on/off driver program generation. Default is to generate- a driver. (Issue "cgGenerateDriver False" to skip the driver.)- For a library, a driver will be generated if any of the- constituent parts has a driver. Otherwise it'll be skipped.- * Fix a bug in C code generation where "Not" over booleans were- incorrectly getting translated due to need for masking.- * Add support for compilation with uninterpreted functions. Users- can now specify the corresponding C code and SBV will simply- call the "native" functions instead of generating it. This- enables interfacing with other C programs. See the functions:- cgAddPrototype, cgAddDecl, and cgAddLDFlags.- Examples:- * Add CRC polynomial generation example via existentials- * Add USB CRC code generation example, both via polynomials and- using the internal CRC functionality--======================================================================-Version 0.9.21, 2011-08-05- - Code generation:- * Allow for inclusion of user makefiles- * Allow for CCFLAGS to be set by the user- * Other minor clean-up--======================================================================-Version 0.9.20, 2011-06-05- - * Regression on 0.9.19; add missing file to cabal--======================================================================-Version 0.9.19, 2011-06-05- - Code:- * Add SignCast class for conversion between signed/unsigned- quantities for same-sized bit-vectors- * Add full-binary trees that can be indexed symbolically (STree). The- advantage of this type is that the reads and writes take- logarithmic time. Suitable for implementing faster symbolic look-up.- * Expose HasSignAndSize class through Data.SBV.Internals- * Many minor improvements, file re-orgs- Examples:- * Add sentence-counting example- * Add an implementation of RC4--======================================================================-Version 0.9.18, 2011-04-07-- Code:- * Re-engineer code-generation, and compilation to C.- In particular, allow arrays of inputs to be specified,- both as function arguments and output reference values.- * Add support for generation of generation of C-libraries,- allowing code generation for a set of functions that- work together.- Examples:- * Update code-generation examples to use the new API.- * Include a library-generation example for doing 128-bit- AES encryption--======================================================================-Version 0.9.17, 2011-03-29- - Code:- * Simplify and reorganize the test suite- Examples:- * Improve AES decryption example, by using- table-lookups in InvMixColumns.- -======================================================================-Version 0.9.16, 2011-03-28-- Code:- * Further optimizations on Bits instance of SBV- Examples:- * Add AES algorithm as an example, showing how- encryption algorithms are particularly suitable- for use with the code-generator--======================================================================-Version 0.9.15, 2011-03-24- - Bug fixes:- * Fix rotateL/rotateR instances on concrete- words. Previous versions was bogus since- it relied on the Integer instance, which- does the wrong thing after normalization.- * Fix conversion of signed numbers from bits,- previous version did not handle two's- complement layout correctly- Testing:- * Add a sleuth of concrete test cases on- arithmetic to catch bugs. (There are many- of them, ~30K, but they run quickly.)--======================================================================-Version 0.9.14, 2011-03-19- - - Reimplement sharing using Stable names, inspired- by the Data.Reify techniques. This avoids tricks- with unsafe memory stashing, and hence is safe.- Thus, issues with respect to CAFs are now resolved.--======================================================================-Version 0.9.13, 2011-03-16- - Bug fixes:- * Make sure SBool short-cut evaluations are done- as early as possible, as these help with coding- recursion-depth based algorithms, when dealing- with symbolic termination issues.- Examples:- * Add fibonacci code-generation example, original- code by Lee Pike.- * Add a GCD code-generation/verification example--======================================================================-Version 0.9.12, 2011-03-10- - New features:- * Add support for compilation to C- * Add a mechanism for offline saving of SMT-Lib files-- Bug fixes:- * Output naming bug, reported by Josef Svenningsson- * Specification bug in Legato's multipler example--======================================================================-Version 0.9.11, 2011-02-16- - * Make ghc-7.0 happy, minor re-org on the cabal file/Setup.hs--======================================================================-Version 0.9.10, 2011-02-15-- * Integrate commits from Iavor: Generalize SBV's to keep- track the integer directly without resorting to different- leaf types- * Remove the unnecessary CLC instruction from the Legato example- * More tests--======================================================================-Version 0.9.9, 2011-01-23-- * Support for user-defined SMT-Lib axioms to be- specified for uninterpreted constants/functions- * Move to using doctest style inline tests--======================================================================-Version 0.9.8, 2011-01-22-- * Better support for uninterpreted-functions- * Support counter-examples with SArray's- * Ladner-Fischer scheme example- * Documentation updates--======================================================================-Version 0.9.7, 2011-01-18-- * First stable public hackage release--======================================================================-Versions 0.0.0 - 0.9.6, Mid 2010 through early 2011-- * Basic infrastructure, design exploration
SBVUnitTest/SBVTestCollection.hs view
@@ -53,8 +53,9 @@ import qualified TestSuite.Puzzles.Temperature as T09_09(testSuite) import qualified TestSuite.Puzzles.U2Bridge as T09_10(testSuite) import qualified TestSuite.Uninterpreted.AUF as T10_01(testSuite)-import qualified TestSuite.Uninterpreted.Function as T10_02(testSuite)-import qualified TestSuite.Uninterpreted.Uninterpreted as T10_03(testSuite)+import qualified TestSuite.Uninterpreted.Axioms as T10_02(testSuite)+import qualified TestSuite.Uninterpreted.Function as T10_03(testSuite)+import qualified TestSuite.Uninterpreted.Uninterpreted as T10_04(testSuite) -- Bool says whether we need a real SMT solver to run this test -- Note that it's ok to say True even if an SMT solver is *not*@@ -101,6 +102,7 @@ , ("temperature", True, T09_09.testSuite) , ("u2bridge", True, T09_10.testSuite) , ("auf1", True, T10_01.testSuite)- , ("auf2", True, T10_02.testSuite)- , ("unint", True, T10_03.testSuite)+ , ("unint-axms", True, T10_02.testSuite)+ , ("auf2", True, T10_03.testSuite)+ , ("unint", True, T10_04.testSuite) ]
SBVUnitTest/SBVUnitTest.hs view
@@ -77,8 +77,9 @@ when (e /= 0) $ putStrLn $ "*** " ++ show e ++ " (of " ++ show c ++ ") test cases in error." when (f /= 0) $ putStrLn $ "*** " ++ show f ++ " (of " ++ show c ++ ") test cases failed." if c == t && e == 0 && f == 0- then do if shouldCreate- then putStrLn $ "All " ++ show c ++ " test cases executed in gold-file generation mode."- else putStrLn $ "All " ++ show c ++ " test cases successfully passed."+ then do putStrLn $ "All " ++ show c ++ " test cases "+ ++ (if shouldCreate+ then " executed in gold-file generation mode."+ else " successfully passed.") exitSuccess else exitWith $ ExitFailure 2
SBVUnitTest/SBVUnitTestBuildTime.hs view
@@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String-buildTime = "Tue Jan 1 22:35:55 PST 2013"+buildTime = "Thu Mar 21 21:14:54 PDT 2013"
+ SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs view
@@ -0,0 +1,49 @@+-----------------------------------------------------------------------------+-- |+-- Module : TestSuite.Uninterpreted.Axioms+-- Copyright : (c) Levent Erkok+-- License : BSD3+-- Maintainer : erkokl@gmail.com+-- Stability : experimental+--+-- Test suite for basic axioms and uninterpreted functions+-----------------------------------------------------------------------------++{-# LANGUAGE DeriveDataTypeable #-}+module TestSuite.Uninterpreted.Axioms(testSuite) where++import Data.SBV+import SBVTest+import Data.Generics++-- Test suite+testSuite :: SBVTestSuite+testSuite = mkTestSuite $ \_ -> test [+ "unint-axioms" ~: assert =<< isThm p0+ ]++-- Example provided by Thomas DuBuisson:+data Bitstring = Bitstring deriving (Eq, Ord, Data, Typeable)+instance SymWord Bitstring+instance HasKind Bitstring+type SBitstring = SBV Bitstring++a :: SBitstring -> SBool+a = uninterpret "a"++e :: SBitstring -> SBitstring -> SBitstring+e = uninterpret "e"++axE :: [String]+axE = [ "(assert (forall ((p Bitstring) (k Bitstring))"+ , " (=> (and (a k) (a p)) (a (e k p)))))"+ ]++p0 :: Symbolic SBool+p0 = do+ p <- free "p" :: Symbolic SBitstring+ k <- free "k" :: Symbolic SBitstring+ addAxiom "axE" axE+ constrain $ a p+ constrain $ a k+ return $ a (e k p)
sbv.cabal view
@@ -1,5 +1,5 @@ Name: sbv-Version: 2.9+Version: 2.10 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@@ -30,6 +30,9 @@ [@import "Data.SBV.Bridge.CVC4"@] Picks CVC4 from New York University and the University of Iowa (<http://cvc4.cs.nyu.edu>) .+ [@import "Data.SBV.Bridge.Boolector"@]+ Picks Boolector from Johannes Kepler University at (<http://fmv.jku.at/boolector/>).+ . SBV introduces the following types and concepts: . * 'SBool': Symbolic Booleans (bits)@@ -100,7 +103,7 @@ Build-Type: Simple Cabal-Version: >= 1.14 Data-Files: SBVUnitTest/GoldFiles/*.gold-Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES+Extra-Source-Files: INSTALL, README.md, COPYRIGHT, CHANGES.md source-repository head type: git@@ -132,6 +135,7 @@ , array, containers, deepseq, directory, filepath, old-time , pretty, process, mtl, QuickCheck, random, syb Exposed-modules : Data.SBV+ , Data.SBV.Bridge.Boolector , Data.SBV.Bridge.CVC4 , Data.SBV.Bridge.Yices , Data.SBV.Bridge.Z3@@ -162,6 +166,7 @@ , Data.SBV.Examples.Uninterpreted.AUF , Data.SBV.Examples.Uninterpreted.Deduce , Data.SBV.Examples.Uninterpreted.Function+ , Data.SBV.Examples.Uninterpreted.Shannon , Data.SBV.Examples.Uninterpreted.Sort Other-modules : Data.SBV.BitVectors.AlgReals , Data.SBV.BitVectors.Data@@ -178,6 +183,7 @@ , Data.SBV.SMT.SMTLib2 , Data.SBV.Provers.Prover , Data.SBV.Provers.SExpr+ , Data.SBV.Provers.Boolector , Data.SBV.Provers.CVC4 , Data.SBV.Provers.Yices , Data.SBV.Provers.Z3@@ -197,7 +203,7 @@ ScopedTypeVariables TupleSections Build-depends : base >= 4 && < 5- , HUnit, directory, filepath, process, sbv+ , HUnit, directory, filepath, process, syb, sbv Hs-Source-Dirs : SBVUnitTest main-is : SBVUnitTest.hs Other-modules : SBVUnitTestBuildTime@@ -258,13 +264,14 @@ , TestSuite.Uninterpreted.AUF , TestSuite.Uninterpreted.Function , TestSuite.Uninterpreted.Uninterpreted+ , TestSuite.Uninterpreted.Axioms Test-Suite SBVBasicTests type : exitcode-stdio-1.0 default-language: Haskell2010 ghc-options : -Wall Build-depends : base >= 4 && < 5- , HUnit, directory, filepath, sbv+ , HUnit, directory, filepath, syb, sbv Hs-Source-Dirs : SBVUnitTest main-is : SBVBasicTests.hs Other-modules : SBVBasicTests