diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,8 +1,56 @@ * Hackage: * GitHub: -* Latest Hackage released version: 2.10 +* Latest Hackage released version: 3.0 +### Version 3.0, 2014-02-16 + + * Support for floating-point numbers: + * Preliminary support for IEEE-floating point arithmetic, introducing + the types `SFloat` and `SDouble`. The support is still quite new, + and Z3 is the only solver that currently features a solver for + this logic. Likely to have bugs, both at the SBV level, and at the + Z3 level; so any bug reports are welcome! + * New backend solvers: + * SBV now supports MathSAT from Fondazione Bruno Kessler and + DISI-University of Trento. See: http://mathsat.fbk.eu/ + * Support all-sat calls in the presence of uninterpreted sorts: + * Implement better support for `allSat` in the presence of uninterpreted + sorts. Previously, SBV simply rejected running `allSat` queries + in the presence of uninterpreted sorts, since it was not possible + to generate a refuting model. The model returned by the SMT solver + is simply not usable, since it names constants that is not visible + in a subsequent run. Eric Seidel came up with the idea that we can + actually compute equivalence classes based on a produced model, and + assert the constraint that the new model should disallow the previously + found equivalence classes instead. The idea seems to work well + in practice, and there is also an example program demonstrating + the functionality: Examples/Uninterpreted/UISortAllSat.hs + * Programmable model extraction improvements: + * Add functions `getModelDictionary` and `getModelDictionaries`, which + provide low-level access to models returned from SMT solvers. Former + for `sat` and `prove` calls, latter for `allSat` calls. Together with + the exported utils from the `Data.SBV.Internals` module, this should + allow for expert users to dissect the models returned and do fancier + programming on top of SBV. + * Add `getModelValue`, `getModelValues`, `getModelUninterpretedValue`, and + `getModelUninterpretedValues`; which further aid in model value + extraction. + * Other: + * Allow users to specify the SMT-Lib logic to use, if necessary. SBV will + still pick the logic automatically, but users can now override that choice. + Comes in handy when playing with custom logics. + * Bug fixes: + * Address allsat-laziness issue (#78 in github issue tracker). Essentially, + simplify how all-sat is called so we can avoid calling the solver for + solutions that are not needed. Thanks to Eric Seidel for reporting. + * Examples: + * Add Data/SBV/Examples/Misc/ModelExtract.hs as a simple example for + programmable model extraction and usage. + * Add Data/SBV/Examples/Misc/Floating.hs for some FP examples. + * Use the AUFLIA logic in Examples.Existentials.Diophantine which helps + z3 complete the proof quickly. (The BV logics take too long for this problem.) + ### Version 2.10, 2013-03-22 * Add support for the Boolector SMT solver @@ -108,7 +156,7 @@ - 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 +### 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 @@ -141,24 +189,24 @@ ### 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. + * 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 @@ -187,28 +235,31 @@ 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!] + * 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. + * [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 @@ -225,6 +276,7 @@ ### 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 @@ -240,6 +292,7 @@ ### Version 1.1, 2012-02-14 Library: + * Rename bitValue to sbvTestBit * Add sbvPopCount * Add a custom implementation of 'popCount' for the Bits class @@ -252,6 +305,7 @@ ### 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 @@ -267,15 +321,20 @@ * 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 @@ -312,11 +371,17 @@ 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 @@ -325,6 +390,7 @@ ### 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 @@ -336,7 +402,9 @@ 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 @@ -370,100 +438,120 @@ 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 + 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 + 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 + + * 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 +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. +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 +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.) +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 @@ -473,26 +561,31 @@ ### 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 +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 +New features: - Bug fixes: - * Output naming bug, reported by Josef Svenningsson - * Specification bug in Legato's multipler example + * 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 @@ -522,6 +615,6 @@ * First stable public hackage release -Versions 0.0.0 - 0.9.6, Mid 2010 through early 2011 +### Versions 0.0.0 - 0.9.6, Mid 2010 through early 2011 * Basic infrastructure, design exploration diff --git a/COPYRIGHT b/COPYRIGHT --- a/COPYRIGHT +++ b/COPYRIGHT @@ -1,4 +1,4 @@ -Copyright (c) 2010-2013, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2010-2014, Levent Erkok (erkokl@gmail.com) All rights reserved. The sbv library is distributed with the BSD3 license. See the LICENSE file diff --git a/Data/SBV.hs b/Data/SBV.hs --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -40,6 +40,14 @@ -- -- * 'SInt8', 'SInt16', 'SInt32', 'SInt64': Symbolic Ints (signed). -- +-- * 'SInteger': Unbounded signed integers. +-- +-- * 'SReal': Algebraic-real numbers +-- +-- * 'SFloat': IEEE-754 single-precision floating point values +-- +-- * 'SDouble': IEEE-754 double-precision floating point values +-- -- * 'SArray', 'SFunArray': Flat arrays of symbolic values. -- -- * Symbolic polynomials over GF(2^n), polynomial arithmetic, and CRCs. @@ -86,6 +94,8 @@ -- -- * Boolector from Johannes Kepler University: -- +-- * MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: +-- -- 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. --------------------------------------------------------------------------------- @@ -105,15 +115,18 @@ -- *** Signed unbounded integers -- $unboundedLimitations , SInteger + -- *** IEEE-floating point numbers + -- $floatingPoints + , SFloat, SDouble, RoundingMode(..), nan, infinity, sNaN, sInfinity, fusedMA, isFPPoint -- *** Signed algebraic reals -- $algReals - , SReal, AlgReal + , SReal, AlgReal, toSReal -- ** Creating a symbolic variable -- $createSym - , sBool, sWord8, sWord16, sWord32, sWord64, sInt8, sInt16, sInt32, sInt64, sInteger + , sBool, sWord8, sWord16, sWord32, sWord64, sInt8, sInt16, sInt32, sInt64, sInteger, sReal, sFloat, sDouble -- ** Creating a list of symbolic variables -- $createSyms - , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sInt8s, sInt16s, sInt32s, sInt64s, sIntegers, sReal, sReals, toSReal + , sBools, sWord8s, sWord16s, sWord32s, sWord64s, sInt8s, sInt16s, sInt32s, sInt64s, sIntegers, sReals, sFloats, sDoubles -- *** Abstract SBV type , SBV -- *** Arrays of symbolic values @@ -193,9 +206,10 @@ -- ** Programmable model extraction -- $programmableExtraction , SatModel(..), Modelable(..), displayModels, extractModels + , getModelDictionaries, getModelValues, getModelUninterpretedValues -- * SMT Interface: Configurations and solvers - , SMTConfig(..), OptimizeOpts(..), SMTSolver(..), boolector, cvc4, yices, z3, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation + , SMTConfig(..), SMTLibLogic(..), Logic(..), OptimizeOpts(..), SMTSolver(..), boolector, cvc4, yices, z3, mathSAT, sbvCurrentSolver, defaultSMTCfg, sbvCheckSolverInstallation -- * Symbolic computations , Symbolic, output, SymWord(..) @@ -268,6 +282,13 @@ sbvCurrentSolver :: SMTConfig sbvCurrentSolver = z3 +-- | We call a FP number FPPoint if it is neither NaN, nor +/- infinity. +-- Note that we cannot use == to test for this, as NaN does not compare equal to itself. +isFPPoint :: (Floating a, SymWord a) => SBV a -> SBool +isFPPoint x = x .== x -- gets rid of NaN's + &&& x .< sInfinity -- gets rid of +inf + &&& x .> -sInfinity -- gets rid of -inf + -- Haddock section documentation {- $progIntro The SBV library is really two things: @@ -420,6 +441,12 @@ .) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.) +-} + +{- $floatingPoints +Floating point numbers are defined by the IEEE-754 standard; and correspond to Haskell's +'Float' and 'Double' types. For SMT support with floating-point numbers, see the paper +by Rummer and Wahl: . -} {- $constrainIntro diff --git a/Data/SBV/BitVectors/AlgReals.hs b/Data/SBV/BitVectors/AlgReals.hs --- a/Data/SBV/BitVectors/AlgReals.hs +++ b/Data/SBV/BitVectors/AlgReals.hs @@ -49,7 +49,7 @@ mkPolyReal (Right (k, coeffs)) = AlgPolyRoot (k, Polynomial (normalize coeffs)) Nothing where normalize :: [(Integer, Integer)] -> [(Integer, Integer)] - normalize = merge . reverse . sortBy (compare `on` snd) + normalize = merge . sortBy (flip compare `on` snd) merge [] = [] merge [x] = [x] merge ((a, b):r@((c, d):xs)) diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs --- a/Data/SBV/BitVectors/Data.hs +++ b/Data/SBV/BitVectors/Data.hs @@ -20,17 +20,19 @@ module Data.SBV.BitVectors.Data ( SBool, SWord8, SWord16, SWord32, SWord64 - , SInt8, SInt16, SInt32, SInt64, SInteger, SReal + , SInt8, SInt16, SInt32, SInt64, SInteger, SReal, SFloat, SDouble + , nan, infinity, sNaN, sInfinity, RoundingMode(..), smtLibSquareRoot, smtLibFusedMA , SymWord(..) - , CW(..), CWVal(..), cwSameType, cwIsBit, cwToBool + , CW(..), CWVal(..), AlgReal(..), cwSameType, cwIsBit, cwToBool , mkConstCW ,liftCW2, mapCW, mapCW2 - , SW(..), trueSW, falseSW, trueCW, falseCW + , SW(..), trueSW, falseSW, trueCW, falseCW, normCW , SBV(..), NodeId(..), mkSymSBV , ArrayContext(..), ArrayInfo, SymArray(..), SFunArray(..), mkSFunArray, SArray(..), arrayUIKind , sbvToSW, sbvToSymSW , SBVExpr(..), newExpr , cache, Cached, uncache, uncacheAI, HasKind(..) , Op(..), NamedSymVar, UnintKind(..), getTableIndex, SBVPgm(..), Symbolic, runSymbolic, runSymbolic', State, inProofMode, SBVRunMode(..), Kind(..), Outputtable(..), Result(..) + , Logic(..), SMTLibLogic(..) , getTraceInfo, getConstraints, addConstraint , SBVType(..), newUninterpreted, unintFnUIKind, addAxiom , Quantifier(..), needsExistentials @@ -52,6 +54,7 @@ import qualified Data.IntMap as IMap (IntMap, empty, size, toAscList, lookup, insert, insertWith) import qualified Data.Map as Map (Map, empty, toList, size, insert, lookup) +import qualified Data.Set as Set (Set, empty, toList, insert) import qualified Data.Foldable as F (toList) import qualified Data.Sequence as S (Seq, empty, (|>)) @@ -64,6 +67,8 @@ -- | A constant value data CWVal = CWAlgReal AlgReal -- ^ algebraic real | CWInteger Integer -- ^ bit-vector/unbounded integer + | CWFloat Float -- ^ float + | CWDouble Double -- ^ double | CWUninterpreted String -- ^ value of an uninterpreted kind -- We cannot simply derive Eq/Ord for CWVal, since CWAlgReal doesn't have proper @@ -73,19 +78,39 @@ CWAlgReal a == CWAlgReal b = a `algRealStructuralEqual` b CWInteger a == CWInteger b = a == b CWUninterpreted a == CWUninterpreted b = a == b + CWFloat a == CWFloat b = a == b + CWDouble a == CWDouble b = a == b _ == _ = False instance Ord CWVal where CWAlgReal a `compare` CWAlgReal b = a `algRealStructuralCompare` b CWAlgReal _ `compare` CWInteger _ = LT + CWAlgReal _ `compare` CWFloat _ = LT + CWAlgReal _ `compare` CWDouble _ = LT CWAlgReal _ `compare` CWUninterpreted _ = LT CWInteger _ `compare` CWAlgReal _ = GT CWInteger a `compare` CWInteger b = a `compare` b + CWInteger _ `compare` CWFloat _ = LT + CWInteger _ `compare` CWDouble _ = LT CWInteger _ `compare` CWUninterpreted _ = LT + CWFloat _ `compare` CWAlgReal _ = GT + CWFloat _ `compare` CWInteger _ = GT + CWFloat a `compare` CWFloat b = a `compare` b + CWFloat _ `compare` CWDouble _ = LT + CWFloat _ `compare` CWUninterpreted _ = LT + + CWDouble _ `compare` CWAlgReal _ = GT + CWDouble _ `compare` CWInteger _ = GT + CWDouble _ `compare` CWFloat _ = GT + CWDouble a `compare` CWDouble b = a `compare` b + CWDouble _ `compare` CWUninterpreted _ = LT + CWUninterpreted _ `compare` CWAlgReal _ = GT CWUninterpreted _ `compare` CWInteger _ = GT + CWUninterpreted _ `compare` CWFloat _ = GT + CWUninterpreted _ `compare` CWDouble _ = GT CWUninterpreted a `compare` CWUninterpreted b = a `compare` b -- | 'CW' represents a concrete word of a fixed size: @@ -129,6 +154,8 @@ | KUnbounded | KReal | KUninterpreted String + | KFloat + | KDouble deriving (Eq, Ord) instance Show Kind where @@ -138,6 +165,8 @@ show KUnbounded = "SInteger" show KReal = "SReal" show (KUninterpreted s) = s + show KFloat = "SFloat" + show KDouble = "SDouble" -- | A symbolic node id newtype NodeId = NodeId Int deriving (Eq, Ord) @@ -199,6 +228,19 @@ | Uninterpreted String deriving (Eq, Ord) +-- | SMT-Lib's square-root over floats/doubles. We piggy back on to the uninterpreted function mechanism +-- to implement these; which is not a terrible idea; although the use of the constructor 'Uninterpreted' +-- might be confusing. This function will *not* be uninterpreted in reality, as QF_FPA will define it. It's +-- a bit of a shame, but much easier to implement it this way. +smtLibSquareRoot :: Op +smtLibSquareRoot = Uninterpreted "squareRoot" + +-- | SMT-Lib's fusedMA over floats/doubles. Similar to the 'smtLibSquareRoot'. Note that we cannot implement +-- this function in Haskell as precision loss would be inevitable. Maybe Haskell will eventually add this op +-- to the Num class. +smtLibFusedMA :: Op +smtLibFusedMA = Uninterpreted "fusedMA" + -- | A symbolic expression data SBVExpr = SBVApp !Op ![SW] deriving (Eq, Ord) @@ -214,6 +256,8 @@ isBoolean :: a -> Bool isBounded :: a -> Bool isReal :: a -> Bool + isFloat :: a -> Bool + isDouble :: a -> Bool isInteger :: a -> Bool isUninterpreted :: a -> Bool showType :: a -> String @@ -222,11 +266,15 @@ KBounded b _ -> b KUnbounded -> True KReal -> True + KFloat -> True + KDouble -> True KUninterpreted{} -> False intSizeOf x = case kindOf x of KBounded _ s -> s KUnbounded -> error "SBV.HasKind.intSizeOf((S)Integer)" KReal -> error "SBV.HasKind.intSizeOf((S)Real)" + KFloat -> error "SBV.HasKind.intSizeOf((S)Float)" + KDouble -> error "SBV.HasKind.intSizeOf((S)Double)" KUninterpreted s -> error $ "SBV.HasKind.intSizeOf: Uninterpreted sort: " ++ s isBoolean x | KBounded False 1 <- kindOf x = True | True = False @@ -234,6 +282,10 @@ | True = False isReal x | KReal{} <- kindOf x = True | True = False + isFloat x | KFloat{} <- kindOf x = True + | True = False + isDouble x | KDouble{} <- kindOf x = True + | True = False isInteger x | KUnbounded{} <- kindOf x = True | True = False isUninterpreted x | KUninterpreted{} <- kindOf x = True @@ -255,35 +307,45 @@ instance HasKind Word64 where kindOf _ = KBounded False 64 instance HasKind Integer where kindOf _ = KUnbounded instance HasKind AlgReal where kindOf _ = KReal +instance HasKind Float where kindOf _ = KFloat +instance HasKind Double where kindOf _ = KDouble -- | Lift a unary function thruough a CW -liftCW :: (AlgReal -> b) -> (Integer -> b) -> (String -> b) -> CW -> b -liftCW f _ _ (CW _ (CWAlgReal v)) = f v -liftCW _ g _ (CW _ (CWInteger v)) = g v -liftCW _ _ h (CW _ (CWUninterpreted v)) = h v +liftCW :: (AlgReal -> b) -> (Integer -> b) -> (Float -> b) -> (Double -> b) -> (String -> b) -> CW -> b +liftCW f _ _ _ _ (CW _ (CWAlgReal v)) = f v +liftCW _ f _ _ _ (CW _ (CWInteger v)) = f v +liftCW _ _ f _ _ (CW _ (CWFloat v)) = f v +liftCW _ _ _ f _ (CW _ (CWDouble v)) = f v +liftCW _ _ _ _ f (CW _ (CWUninterpreted v)) = f v -- | Lift a binary function through a CW -liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (String -> String -> b) -> CW -> CW -> b -liftCW2 f g h x y = case (cwVal x, cwVal y) of - (CWAlgReal a, CWAlgReal b) -> f a b - (CWInteger a, CWInteger b) -> g a b - (CWUninterpreted a, CWUninterpreted b) -> h a b - _ -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y) +liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> (String -> String -> b) -> CW -> CW -> b +liftCW2 r i f d u x y = case (cwVal x, cwVal y) of + (CWAlgReal a, CWAlgReal b) -> r a b + (CWInteger a, CWInteger b) -> i a b + (CWFloat a, CWFloat b) -> f a b + (CWDouble a, CWDouble b) -> d a b + (CWUninterpreted a, CWUninterpreted b) -> u a b + _ -> error $ "SBV.liftCW2: impossible, incompatible args received: " ++ show (x, y) -- | Map a unary function through a CW -mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (String -> String) -> CW -> CW -mapCW f g h x = normCW $ CW (cwKind x) $ case cwVal x of - CWAlgReal a -> CWAlgReal (f a) - CWInteger a -> CWInteger (g a) - CWUninterpreted a -> CWUninterpreted (h a) +mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> (String -> String) -> CW -> CW +mapCW r i f d u x = normCW $ CW (cwKind x) $ case cwVal x of + CWAlgReal a -> CWAlgReal (r a) + CWInteger a -> CWInteger (i a) + CWFloat a -> CWFloat (f a) + CWDouble a -> CWDouble (d a) + CWUninterpreted a -> CWUninterpreted (u a) -- | Map a binary function through a CW -mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (String -> String -> String) -> CW -> CW -> CW -mapCW2 f g h x y = case (cwSameType x y, cwVal x, cwVal y) of - (True, CWAlgReal a, CWAlgReal b) -> normCW $ CW (cwKind x) (CWAlgReal (f a b)) - (True, CWInteger a, CWInteger b) -> normCW $ CW (cwKind x) (CWInteger (g a b)) - (True, CWUninterpreted a, CWUninterpreted b) -> normCW $ CW (cwKind x) (CWUninterpreted (h a b)) - _ -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y) +mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> (String -> String -> String) -> CW -> CW -> CW +mapCW2 r i f d u x y = case (cwSameType x y, cwVal x, cwVal y) of + (True, CWAlgReal a, CWAlgReal b) -> normCW $ CW (cwKind x) (CWAlgReal (r a b)) + (True, CWInteger a, CWInteger b) -> normCW $ CW (cwKind x) (CWInteger (i a b)) + (True, CWFloat a, CWFloat b) -> normCW $ CW (cwKind x) (CWFloat (f a b)) + (True, CWDouble a, CWDouble b) -> normCW $ CW (cwKind x) (CWDouble (d a b)) + (True, CWUninterpreted a, CWUninterpreted b) -> normCW $ CW (cwKind x) (CWUninterpreted (u a b)) + _ -> error $ "SBV.mapCW2: impossible, incompatible args received: " ++ show (x, y) instance HasKind CW where kindOf = cwKind @@ -293,7 +355,7 @@ instance Show CW where show w | cwIsBit w = show (cwToBool w) - show w = liftCW show show id w ++ " :: " ++ showType w + show w = liftCW show show show show id w ++ " :: " ++ showType w instance Show SW where show (SW _ (NodeId n)) @@ -355,8 +417,7 @@ deriving Show -- | Result of running a symbolic computation -data Result = Result (Bool, Bool) -- contains unbounded integers/reals - [String] -- uninterpreted sorts +data Result = Result (Set.Set Kind) -- kinds used in the program [(String, CW)] -- quick-check counter-example information (if any) [(String, [String])] -- uninterpeted code segments [(Quantifier, NamedSymVar)] -- inputs (possibly existential) @@ -371,18 +432,18 @@ -- | Extract the constraints from a result getConstraints :: Result -> [SW] -getConstraints (Result _ _ _ _ _ _ _ _ _ _ _ cstrs _) = cstrs +getConstraints (Result _ _ _ _ _ _ _ _ _ _ cstrs _) = cstrs -- | Extract the traced-values from a result (quick-check) getTraceInfo :: Result -> [(String, CW)] -getTraceInfo (Result _ _ tvals _ _ _ _ _ _ _ _ _ _) = tvals +getTraceInfo (Result _ tvals _ _ _ _ _ _ _ _ _ _) = tvals instance Show Result where - show (Result _ _ _ _ _ cs _ _ [] [] _ [] [r]) + show (Result _ _ _ _ cs _ _ [] [] _ [] [r]) | Just c <- r `lookup` cs = show c - show (Result _ sorts _ cgs is cs ts as uis axs xs cstrs os) = intercalate "\n" $ - (if null sorts then [] else "SORTS" : map (" " ++) sorts) + show (Result kinds _ cgs is cs ts as uis axs xs cstrs os) = intercalate "\n" $ + (if null usorts then [] else "SORTS" : map (" " ++) usorts) ++ ["INPUTS"] ++ map shn is ++ ["CONSTANTS"] @@ -403,7 +464,8 @@ ++ map ((" " ++) . show) cstrs ++ ["OUTPUTS"] ++ map ((" " ++) . show) os - where shs sw = show sw ++ " :: " ++ showType sw + where usorts = [s | KUninterpreted s <- Set.toList kinds] + shs sw = show sw ++ " :: " ++ showType sw sht ((i, at, rt), es) = " Table " ++ show i ++ " : " ++ show at ++ "->" ++ show rt ++ " = " ++ show es shc (sw, cw) = " " ++ show sw ++ " = " ++ show cw shcg (s, ss) = ("Variable: " ++ s) : map (" " ++) ss @@ -440,6 +502,9 @@ -- | Constants are stored in a map, for hash-consing type CnstMap = Map.Map CW SW +-- | Kinds used in the program; used for determining the final SMT-Lib logic to pick +type KindSet = Set.Set Kind + -- | Tables generated during a symbolic run type TableMap = Map.Map [SW] (Int, Kind, Kind) @@ -488,7 +553,7 @@ , rStdGen :: IORef StdGen , rCInfo :: IORef [(String, CW)] , rctr :: IORef Int - , rUnBounded :: IORef (Bool, Bool) -- SInteger, SReal + , rUsedKinds :: IORef KindSet , rinps :: IORef [(Quantifier, NamedSymVar)] , rConstraints :: IORef [SW] , routs :: IORef [SW] @@ -502,7 +567,6 @@ , raxioms :: IORef [(String, [String])] , rSWCache :: IORef (Cache SW) , rAICache :: IORef (Cache Int) - , rSorts :: IORef [String] } -- | Are we running in proof mode? @@ -551,6 +615,46 @@ -- | Infinite precision symbolic algebraic real value type SReal = SBV AlgReal +-- | IEEE-754 single-precision floating point numbers +type SFloat = SBV Float + +-- | IEEE-754 double-precision floating point numbers +type SDouble = SBV Double + +-- | Not-A-Number for 'Double' and 'Float'. Surprisingly, Haskell +-- Prelude doesn't have this value defined, so we provide it here. +nan :: Floating a => a +nan = 0/0 + +-- | Infinity for 'Double' and 'Float'. Surprisingly, Haskell +-- Prelude doesn't have this value defined, so we provide it here. +infinity :: Floating a => a +infinity = 1/0 + +-- | Symbolic variant of Not-A-Number. This value will inhabit both +-- 'SDouble' and 'SFloat'. +sNaN :: (Floating a, SymWord a) => SBV a +sNaN = literal nan + +-- | Symbolic variant of infinity. This value will inhabit both +-- 'SDouble' and 'SFloat'. +sInfinity :: (Floating a, SymWord a) => SBV a +sInfinity = literal infinity + +-- | Rounding mode to be used for the IEEE floating-point operations. +-- Note that Haskell's default is 'RoundNearestTiesToEven'. If you use +-- a different rounding mode, then the counter-examples you get may not +-- match what you observe in Haskell. +data RoundingMode = RoundNearestTiesToEven -- ^ Round to nearest representable floating point value. + -- If precisely at half-way, pick the even number. + -- (In this context, /even/ means the lowest-order bit is zero.) + | RoundNearestTiesToAway -- ^ Round to nearest representable floating point value. + -- If precisely at half-way, pick the number further away from 0. + -- (That is, for positive values, pick the greater; for negative values, pick the smaller.) + | RoundTowardPositive -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.) + | RoundTowardNegative -- ^ Round towards negative infinity. (Also known as rounding-down or floor.) + | RoundTowardZero -- ^ Round towards zero. (Also known as truncation.) + -- Not particularly "desirable", but will do if needed instance Show (SBV a) where show (SBV _ (Left c)) = show c @@ -602,14 +706,18 @@ 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 () + registerKind st k return (sw, 's' : show ctr) {-# INLINE newSW #-} +registerKind :: State -> Kind -> IO () +registerKind st k + | KUninterpreted sortName <- k, sortName `elem` reserved + = error $ "SBV: " ++ show sortName ++ " is a reserved sort; please use a different name." + | True + = modifyIORef (rUsedKinds st) (Set.insert k) + where reserved = ["Int", "Real", "List", "Array", "Bool", "NUMERAL", "DECIMAL", "STRING", "FP"] -- Reserved by SMT-Lib + -- | Create a new constant; hash-cons as necessary newConst :: State -> CW -> IO SW newConst st c = do @@ -632,10 +740,14 @@ modifyIORef (rtblMap st) (Map.insert elts (i, at, rt)) return i --- | Create a constant word +-- | Create a constant word from an integral mkConstCW :: Integral a => Kind -> a -> CW -mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a))) -mkConstCW k a = normCW $ CW k (CWInteger (toInteger a)) +mkConstCW k@(KBounded{}) a = normCW $ CW k (CWInteger (toInteger a)) +mkConstCW KUnbounded a = normCW $ CW KUnbounded (CWInteger (toInteger a)) +mkConstCW KReal a = normCW $ CW KReal (CWAlgReal (fromInteger (toInteger a))) +mkConstCW KFloat a = normCW $ CW KFloat (CWFloat (fromInteger (toInteger a))) +mkConstCW KDouble a = normCW $ CW KDouble (CWDouble (fromInteger (toInteger a))) +mkConstCW (KUninterpreted s) a = error $ "Unexpected call to mkConstCW with uninterpreted kind: " ++ s ++ " with value: " ++ show (toInteger a) -- | Create a new expression; hash-cons as necessary newExpr :: State -> Kind -> SBVExpr -> IO SW @@ -770,9 +882,8 @@ axioms <- newIORef [] swCache <- newIORef IMap.empty aiCache <- newIORef IMap.empty - unbounded <- newIORef (False, False) + usedKinds <- newIORef Set.empty cstrs <- newIORef [] - sorts <- newIORef [] rGen <- case currentRunMode of Concrete g -> newIORef g _ -> newStdGen >>= newIORef @@ -780,7 +891,7 @@ , rStdGen = rGen , rCInfo = cInfo , rctr = ctr - , rUnBounded = unbounded + , rUsedKinds = usedKinds , rinps = inps , routs = outs , rtblMap = tables @@ -794,7 +905,6 @@ , rSWCache = swCache , rAICache = aiCache , rConstraints = cstrs - , rSorts = sorts } _ <- newConst st (mkConstCW (KBounded False 1) (0::Integer)) -- s(-2) == falseSW _ <- newConst st (mkConstCW (KBounded False 1) (1::Integer)) -- s(-1) == trueSW @@ -809,12 +919,11 @@ arrs <- IMap.toAscList `fmap` readIORef arrays unint <- Map.toList `fmap` readIORef uis axs <- reverse `fmap` readIORef axioms - boundInfo <- readIORef unbounded + knds <- readIORef usedKinds cgMap <- Map.toList `fmap` readIORef cgs traceVals <- reverse `fmap` readIORef cInfo extraCstrs <- reverse `fmap` readIORef cstrs - usorts <- reverse `fmap` readIORef sorts - return $ (r, Result boundInfo usorts traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO) + return $ (r, Result knds traceVals cgMap inpsO cnsts tbls arrs unint axs (SBVPgm rpgm) extraCstrs outsO) ------------------------------------------------------------------------------- -- * Symbolic Words @@ -896,9 +1005,9 @@ mkSymWord mbQ mbNm = do let sortName = tyconUQname . dataTypeName . dataTypeOf $ (undefined :: a) st <- ask - liftIO $ registerSort st sortName let k = KUninterpreted sortName - q = case (mbQ, runMode st) of + liftIO $ registerKind st k + let q = case (mbQ, runMode st) of (Just x, _) -> x (Nothing, Proof True) -> EX (Nothing, Proof False) -> ALL @@ -910,19 +1019,6 @@ 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') @@ -1134,12 +1230,11 @@ rnf (CW x y) = x `seq` y `seq` () instance NFData Result where - rnf (Result isInf sorts qcInfo cgs inps consts tbls arrs uis axs pgm cstr outs) - = rnf isInf `seq` rnf sorts `seq` rnf qcInfo `seq` rnf cgs - `seq` rnf inps `seq` rnf consts `seq` rnf tbls - `seq` rnf arrs `seq` rnf uis `seq` rnf axs - `seq` rnf pgm `seq` rnf cstr `seq` rnf outs - + rnf (Result kindInfo qcInfo cgs inps consts tbls arrs uis axs pgm cstr outs) + = rnf kindInfo `seq` rnf qcInfo `seq` rnf cgs `seq` rnf inps + `seq` rnf consts `seq` rnf tbls `seq` rnf arrs + `seq` rnf uis `seq` rnf axs `seq` rnf pgm + `seq` rnf cstr `seq` rnf outs instance NFData Kind instance NFData ArrayContext instance NFData SW @@ -1153,6 +1248,45 @@ rnf (SBV x y) = rnf x `seq` rnf y `seq` () instance NFData SBVPgm +-- | SMT-Lib logics. If left unspecified SBV will pick the logic based on what it determines is needed. However, the +-- user can override this choice using the 'useLogic' parameter to the configuration. This is especially handy if +-- one is experimenting with custom logics that might be supported on new solvers. +data SMTLibLogic + = AUFLIA -- ^ Formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values + | AUFLIRA -- ^ Linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value + | AUFNIRA -- ^ Formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value + | LRA -- ^ Linear formulas in linear real arithmetic + | UFLRA -- ^ Linear real arithmetic with uninterpreted sort and function symbols. + | UFNIA -- ^ Non-linear integer arithmetic with uninterpreted sort and function symbols. + | QF_ABV -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays + | QF_AUFBV -- ^ Quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols + | QF_AUFLIA -- ^ Quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols + | QF_AX -- ^ Quantifier-free formulas over the theory of arrays with extensionality + | QF_BV -- ^ Quantifier-free formulas over the theory of fixed-size bitvectors + | QF_IDL -- ^ Difference Logic over the integers. Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant + | QF_LIA -- ^ Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables + | QF_LRA -- ^ Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables. + | QF_NIA -- ^ Quantifier-free integer arithmetic. + | QF_NRA -- ^ Quantifier-free real arithmetic. + | QF_RDL -- ^ Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant. + | QF_UF -- ^ Unquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols. + | QF_UFBV -- ^ Unquantified formulas over bitvectors with uninterpreted sort function and symbols. + | QF_UFIDL -- ^ Difference Logic over the integers (in essence) but with uninterpreted sort and function symbols. + | QF_UFLIA -- ^ Unquantified linear integer arithmetic with uninterpreted sort and function symbols. + | QF_UFLRA -- ^ Unquantified linear real arithmetic with uninterpreted sort and function symbols. + | QF_UFNRA -- ^ Unquantified non-linear real arithmetic with uninterpreted sort and function symbols. + | QF_FPABV -- ^ Quantifier-free formulas over the theory of floating point numbers, arrays, and bit-vectors + | QF_FPA -- ^ Quantifier-free formulas over the theory of floating point numbers + deriving Show + +-- | Chosen logic for the solver +data Logic = PredefinedLogic SMTLibLogic -- ^ Use one of the logics as defined by the standard + | CustomLogic String -- ^ Use this name for the logic + +instance Show Logic where + show (PredefinedLogic l) = show l + show (CustomLogic s) = s + -- | Translation tricks needed for specific capabilities afforded by each solver data SolverCapabilities = SolverCapabilities { capSolverName :: String -- ^ Name of the solver @@ -1163,4 +1297,6 @@ , 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? + , supportsFloats :: Bool -- ^ Does the solver support single-precision floating point numbers? + , supportsDoubles :: Bool -- ^ Does the solver support double-precision floating point numbers? } diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs --- a/Data/SBV/BitVectors/Model.hs +++ b/Data/SBV/BitVectors/Model.hs @@ -27,7 +27,8 @@ , 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 - , sInt64s, sInteger, sIntegers, sReal, sReals, toSReal, slet + , sInt64s, sInteger, sIntegers, sReal, sReals, toSReal, sFloat, sFloats, sDouble, sDoubles, slet + , fusedMA ) where @@ -55,9 +56,9 @@ noUnint2 :: String -> String -> a noUnint2 x y = error $ "Unexpected binary operation called on uninterpreted values: " ++ show (x, y) -liftSym1 :: (State -> Kind -> SW -> IO SW) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> SBV b -> SBV b -liftSym1 _ opCR opCI (SBV k (Left a)) = SBV k $ Left $ mapCW opCR opCI noUnint a -liftSym1 opS _ _ a@(SBV k _) = SBV k $ Right $ cache c +liftSym1 :: (State -> Kind -> SW -> IO SW) -> (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> SBV b -> SBV b +liftSym1 _ opCR opCI opCF opCD (SBV k (Left a)) = SBV k $ Left $ mapCW opCR opCI opCF opCD noUnint a +liftSym1 opS _ _ _ _ a@(SBV k _) = SBV k $ Right $ cache c where c st = do swa <- sbvToSW st a opS st k swa @@ -67,13 +68,13 @@ sw2 <- sbvToSW st b opS st k sw1 sw2 -liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b -liftSym2 _ okCW opCR opCI (SBV k (Left a)) (SBV _ (Left b)) | okCW a b = SBV k $ Left $ mapCW2 opCR opCI noUnint2 a b -liftSym2 opS _ _ _ a@(SBV k _) b = SBV k $ Right $ liftSW2 opS k a b +liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> SBV b -> SBV b -> SBV b +liftSym2 _ okCW opCR opCI opCF opCD (SBV k (Left a)) (SBV _ (Left b)) | okCW a b = SBV k $ Left $ mapCW2 opCR opCI opCF opCD noUnint2 a b +liftSym2 opS _ _ _ _ _ a@(SBV k _) b = SBV k $ Right $ liftSW2 opS k a b -liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> SBV b -> SBV b -> SBool -liftSym2B _ okCW opCR opCI (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI noUnint2 a b) -liftSym2B opS _ _ _ a b = SBV (KBounded False 1) $ Right $ liftSW2 opS (KBounded False 1) a b +liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> (Float -> Float -> Bool) -> (Double -> Double -> Bool) -> SBV b -> SBV b -> SBool +liftSym2B _ okCW opCR opCI opCF opCD (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI opCF opCD noUnint2 a b) +liftSym2B opS _ _ _ _ _ a b = SBV (KBounded False 1) $ Right $ liftSW2 opS (KBounded False 1) a b liftSym1Bool :: (State -> Kind -> SW -> IO SW) -> (Bool -> Bool) -> SBool -> SBool liftSym1Bool _ opC (SBV _ (Left a)) = literal $ opC $ cwToBool a @@ -207,6 +208,30 @@ mbMaxBound = Nothing mbMinBound = Nothing +instance SymWord Float where + mkSymWord = genMkSymVar KFloat + literal = SBV KFloat . Left . CW KFloat . CWFloat + fromCW (CW _ (CWFloat a)) = a + fromCW c = error $ "SymWord.Float: Unexpected non-float value: " ++ show c + -- For Float, we conservatively return 'False' for isConcretely. The reason is that + -- this function is used for optimizations when only one of the argument is concrete, + -- and in the presence of NaN's it would be incorrect to do any optimization + isConcretely _ _ = False + mbMaxBound = Nothing + mbMinBound = Nothing + +instance SymWord Double where + mkSymWord = genMkSymVar KDouble + literal = SBV KDouble . Left . CW KDouble . CWDouble + fromCW (CW _ (CWDouble a)) = a + fromCW c = error $ "SymWord.Double: Unexpected non-double value: " ++ show c + -- For Double, we conservatively return 'False' for isConcretely. The reason is that + -- this function is used for optimizations when only one of the argument is concrete, + -- and in the presence of NaN's it would be incorrect to do any optimization + isConcretely _ _ = False + mbMaxBound = Nothing + mbMinBound = Nothing + ------------------------------------------------------------------------------------ -- * Smart constructors for creating symbolic values. These are not strictly -- necessary, as they are mere aliases for 'symbolic' and 'symbolics', but @@ -300,6 +325,22 @@ sReals :: [String] -> Symbolic [SReal] sReals = symbolics +-- | Declare an 'SFloat' +sFloat :: String -> Symbolic SFloat +sFloat = symbolic + +-- | Declare a list of 'SFloat's +sFloats :: [String] -> Symbolic [SFloat] +sFloats = symbolics + +-- | Declare an 'SDouble' +sDouble :: String -> Symbolic SDouble +sDouble = symbolic + +-- | Declare a list of 'SDouble's +sDoubles :: [String] -> Symbolic [SDouble] +sDoubles = symbolics + -- | Promote an SInteger to an SReal toSReal :: SInteger -> SReal toSReal x @@ -348,29 +389,36 @@ -} instance EqSymbolic (SBV a) where - (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW) Equal) rationalCheck (==) (==) - (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) rationalCheck (/=) (/=) + (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW) Equal) rationalCheck (==) (==) (==) (==) + (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) rationalCheck (/=) (/=) (/=) (/=) +-- | eqOpt says the references are to the same SW, thus we can optimize. Note that +-- we explicitly disallow KFloat/KDouble here. Why? Because it's *NOT* true that +-- NaN == NaN, NaN >= NaN, and so-forth. So, we have to make sure we don't optimize +-- floats and doubles, in case the argument turns out to be NaN. eqOpt :: SW -> SW -> SW -> Maybe SW -eqOpt w x y = if x == y then Just w else Nothing +eqOpt w x y = case kindOf x of + KFloat -> Nothing + KDouble -> Nothing + _ -> if x == y then Just w else Nothing instance SymWord a => OrdSymbolic (SBV a) where x .< y | Just mb <- mbMaxBound, x `isConcretely` (== mb) = false | Just mb <- mbMinBound, y `isConcretely` (== mb) = false - | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) rationalCheck (<) (<) x y + | True = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan) rationalCheck (<) (<) (<) (<) x y x .<= y | Just mb <- mbMinBound, x `isConcretely` (== mb) = true | Just mb <- mbMaxBound, y `isConcretely` (== mb) = true - | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) rationalCheck (<=) (<=) x y + | True = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq) rationalCheck (<=) (<=) (<=) (<=) x y x .> y | Just mb <- mbMinBound, x `isConcretely` (== mb) = false | Just mb <- mbMaxBound, y `isConcretely` (== mb) = false - | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) rationalCheck (>) (>) x y + | True = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) rationalCheck (>) (>) (>) (>) x y x .>= y | Just mb <- mbMaxBound, x `isConcretely` (== mb) = true | Just mb <- mbMinBound, y `isConcretely` (== mb) = true - | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) rationalCheck (>=) (>=) x y + | True = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq) rationalCheck (>=) (>=) (>=) (>=) x y -- Bool instance EqSymbolic Bool where @@ -549,16 +597,16 @@ x + y | x `isConcretely` (== 0) = y | y `isConcretely` (== 0) = x - | True = liftSym2 (mkSymOp Plus) rationalCheck (+) (+) x y + | True = liftSym2 (mkSymOp Plus) rationalCheck (+) (+) (+) (+) x y x * y | x `isConcretely` (== 0) = 0 | y `isConcretely` (== 0) = 0 | x `isConcretely` (== 1) = y | y `isConcretely` (== 1) = x - | True = liftSym2 (mkSymOp Times) rationalCheck (*) (*) x y + | True = liftSym2 (mkSymOp Times) rationalCheck (*) (*) (*) (*) x y x - y | y `isConcretely` (== 0) = x - | True = liftSym2 (mkSymOp Minus) rationalCheck (-) (-) x y + | True = liftSym2 (mkSymOp Minus) rationalCheck (-) (-) (-) (-) x y abs a | hasSign a = ite (a .< 0) (-a) a | True = a @@ -566,12 +614,71 @@ | hasSign a = ite (a .< 0) (-1) (ite (a .== 0) 0 1) | True = oneIf (a ./= 0) -instance Fractional SReal where +instance (SymWord a, Fractional a) => Fractional (SBV a) where fromRational = literal . fromRational - x / y = liftSym2 (mkSymOp Quot) rationalCheck (/) die x y + x / y = liftSym2 (mkSymOp Quot) rationalCheck (/) die (/) (/) x y where -- should never happen - die = error $ "impossible: non-real value found in Fractional.SReal " ++ show (x, y) + die = error "impossible: integer valued data found in Fractional instance" +-- | Define Floating instance on SBV's; only for base types that are already floating; i.e., SFloat and SDouble +-- Note that most of the fields are "undefined" for symbolic values, we add methods as they are supported by SMTLib. +-- Currently, the only symbolicly available function in this class is sqrt. +instance (SymWord a, Fractional a, Floating a) => Floating (SBV a) where + pi = literal pi + exp = lift1FNS "exp" exp + log = lift1FNS "log" log + sqrt = lift1F sqrt smtLibSquareRoot + sin = lift1FNS "sin" sin + cos = lift1FNS "cos" cos + tan = lift1FNS "tan" tan + asin = lift1FNS "asin" asin + acos = lift1FNS "acos" acos + atan = lift1FNS "atan" atan + sinh = lift1FNS "sinh" sinh + cosh = lift1FNS "cosh" cosh + tanh = lift1FNS "tanh" tanh + asinh = lift1FNS "asinh" asinh + acosh = lift1FNS "acosh" acosh + atanh = lift1FNS "atanh" atanh + (**) = lift2FNS "**" (**) + logBase = lift2FNS "logBase" logBase + +-- | Fused-multiply add. @fusedMA a b c = a * b + c@, for double and floating point values. +-- Note that a 'fusedMA' call will *never* be concrete, even if all the arguments are constants; since +-- we cannot guarantee the precision requirements, which is the whole reason why 'fusedMA' exists in the +-- first place. (NB. 'fusedMA' only rounds once, even though it does two operations, and hence the extra +-- precision.) +fusedMA :: (SymWord a, Floating a) => SBV a -> SBV a -> SBV a -> SBV a +fusedMA a b c = SBV k $ Right $ cache r + where k = kindOf a + r st = do swa <- sbvToSW st a + swb <- sbvToSW st b + swc <- sbvToSW st c + newExpr st k (SBVApp smtLibFusedMA [swa, swb, swc]) + +-- | Lift a float/double unary function, using a corresponding function in SMT-lib. We piggy-back on the uninterpreted +-- function mechanism here, as it essentially is the same as introducing this as a new function. +lift1F :: (SymWord a, Floating a) => (a -> a) -> Op -> SBV a -> SBV a +lift1F f smtOp sv + | Just v <- unliteral sv = literal $ f v + | True = SBV k $ Right $ cache c + where k = kindOf sv + c st = do swa <- sbvToSW st sv + newExpr st k (SBVApp smtOp [swa]) + +-- | Lift a float/double unary function, only over constants +lift1FNS :: (SymWord a, Floating a) => String -> (a -> a) -> SBV a -> SBV a +lift1FNS nm f sv + | Just v <- unliteral sv = literal $ f v + | True = error $ "SBV." ++ nm ++ ": not supported for symbolic values of type " ++ show (kindOf sv) + +-- | Lift a float/double binary function, only over constants +lift2FNS :: (SymWord a, Floating a) => String -> (a -> a -> a) -> SBV a -> SBV a -> SBV a +lift2FNS nm f sv1 sv2 + | Just v1 <- unliteral sv1 + , Just v2 <- unliteral sv2 = literal $ f v1 v2 + | True = error $ "SBV." ++ nm ++ ": not supported for symbolic values of type " ++ show (kindOf sv1) + -- Most operations on concrete rationals require a compatibility check rationalCheck :: CW -> CW -> Bool rationalCheck a b = case (cwVal a, cwVal b) of @@ -587,9 +694,21 @@ noReal :: String -> AlgReal -> AlgReal -> AlgReal noReal o a b = error $ "SBV.AlgReal." ++ o ++ ": Unexpected arguments: " ++ show (a, b) +noFloat :: String -> Float -> Float -> Float +noFloat o a b = error $ "SBV.Float." ++ o ++ ": Unexpected arguments: " ++ show (a, b) + +noDouble :: String -> Double -> Double -> Double +noDouble o a b = error $ "SBV.Double." ++ o ++ ": Unexpected arguments: " ++ show (a, b) + noRealUnary :: String -> AlgReal -> AlgReal noRealUnary o a = error $ "SBV.AlgReal." ++ o ++ ": Unexpected argument: " ++ show a +noFloatUnary :: String -> Float -> Float +noFloatUnary o a = error $ "SBV.Float." ++ o ++ ": Unexpected argument: " ++ show a + +noDoubleUnary :: String -> Double -> Double +noDoubleUnary o a = error $ "SBV.Double." ++ o ++ ": Unexpected argument: " ++ show a + -- NB. In the optimizations below, use of -1 is valid as -- -1 has all bits set to True for both signed and unsigned values instance (Num a, Bits a, SymWord a) => Bits (SBV a) where @@ -598,38 +717,38 @@ | x `isConcretely` (== -1) = y | y `isConcretely` (== 0) = 0 | y `isConcretely` (== -1) = x - | True = liftSym2 (mkSymOp And) (const (const True)) (noReal ".&.") (.&.) x y + | True = liftSym2 (mkSymOp And) (const (const True)) (noReal ".&.") (.&.) (noFloat ".&.") (noDouble ".&.") x y x .|. y | x `isConcretely` (== 0) = y | x `isConcretely` (== -1) = -1 | y `isConcretely` (== 0) = x | y `isConcretely` (== -1) = -1 - | True = liftSym2 (mkSymOp Or) (const (const True)) (noReal ".|.") (.|.) x y + | True = liftSym2 (mkSymOp Or) (const (const True)) (noReal ".|.") (.|.) (noFloat ".|.") (noDouble ".|.") x y x `xor` y | x `isConcretely` (== 0) = y | y `isConcretely` (== 0) = x - | True = liftSym2 (mkSymOp XOr) (const (const True)) (noReal "xor") xor x y - complement = liftSym1 (mkSymOp1 Not) (noRealUnary "Not") complement + | True = liftSym2 (mkSymOp XOr) (const (const True)) (noReal "xor") xor (noFloat "xor") (noDouble "xor") x y + complement = liftSym1 (mkSymOp1 Not) (noRealUnary "complement") complement (noFloatUnary "complement") (noDoubleUnary "complement") bitSize _ = intSizeOf (undefined :: a) isSigned _ = hasSign (undefined :: a) bit i = 1 `shiftL` i shiftL x y | y < 0 = shiftR x (-y) | y == 0 = x - | True = liftSym1 (mkSymOp1 (Shl y)) (noRealUnary "shiftL") (`shiftL` y) x + | True = liftSym1 (mkSymOp1 (Shl y)) (noRealUnary "shiftL") (`shiftL` y) (noFloatUnary "shiftL") (noDoubleUnary "shiftL") x shiftR x y | y < 0 = shiftL x (-y) | y == 0 = x - | True = liftSym1 (mkSymOp1 (Shr y)) (noRealUnary "shiftR") (`shiftR` y) x + | True = liftSym1 (mkSymOp1 (Shr y)) (noRealUnary "shiftR") (`shiftR` y) (noFloatUnary "shiftR") (noDoubleUnary "shiftR") x rotateL x y | y < 0 = rotateR x (-y) | y == 0 = x - | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) x + | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Rol (y `mod` sz))) (noRealUnary "rotateL") (rot True sz y) (noFloatUnary "rotateL") (noDoubleUnary "rotateL") x | True = shiftL x y -- for unbounded Integers, rotateL is the same as shiftL in Haskell rotateR x y | y < 0 = rotateL x (-y) | y == 0 = x - | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) x + | isBounded x = let sz = bitSize x in liftSym1 (mkSymOp1 (Ror (y `mod` sz))) (noRealUnary "rotateR") (rot False sz y) (noFloatUnary "rotateR") (noDoubleUnary "rotateR") x | True = shiftR x y -- for unbounded integers, rotateR is the same as shiftR in Haskell -- NB. testBit is *not* implementable on non-concrete symbolic words x `testBit` i @@ -903,11 +1022,11 @@ instance SDivisible CW where sQuotRem a b | CWInteger x <- cwVal a, CWInteger y <- cwVal b - = let (r1, r2) = sQuotRem x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 }) + = let (r1, r2) = sQuotRem x y in (normCW a{ cwVal = CWInteger r1 }, normCW b{ cwVal = CWInteger r2 }) sQuotRem a b = error $ "SBV.sQuotRem: impossible, unexpected args received: " ++ show (a, b) sDivMod a b | CWInteger x <- cwVal a, CWInteger y <- cwVal b - = let (r1, r2) = sDivMod x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 }) + = let (r1, r2) = sDivMod x y in (normCW a { cwVal = CWInteger r1 }, normCW b { cwVal = CWInteger r2 }) sDivMod a b = error $ "SBV.sDivMod: impossible, unexpected args received: " ++ show (a, b) instance SDivisible SWord64 where @@ -980,9 +1099,15 @@ instance (SymWord a, Arbitrary a) => Arbitrary (SBV a) where arbitrary = liftM literal arbitrary --- | Symbolic choice operator, parameterized via a class --- 'select' is a total-indexing function, with the default. +-- | Symbolic conditionals are modeled by the 'Mergeable' class, describing +-- how to merge the results of an if-then-else call with a symbolic test. SBV +-- provides all basic types as instances of this class, so users only need +-- to declare instances for custom data-types of their programs as needed. -- +-- The function 'select' is a total-indexing function out of a list of choices +-- with a default value, simulating array/list indexing. It's an n-way generalization +-- of the 'ite' function. +-- -- Minimal complete definition: 'symbolicMerge' class Mergeable a where -- | Merge two values based on the condition. This is intended @@ -1495,7 +1620,7 @@ instance Testable (Symbolic SBool) where property m = QC.whenFail (putStrLn msg) $ QC.monadicIO test - where runOnce g = do (r, Result _ _ tvals _ _ cs _ _ _ _ _ cstrs _) <- runSymbolic' (Concrete g) m + where runOnce g = do (r, Result _ tvals _ _ cs _ _ _ _ _ cstrs _) <- runSymbolic' (Concrete g) m let cval = fromMaybe (error "Cannot quick-check in the presence of uninterpeted constants!") . (`lookup` cs) cond = all (cwToBool . cval) cstrs when (isSymbolic r) $ error $ "Cannot quick-check in the presence of uninterpreted constants! (" ++ show r ++ ")" diff --git a/Data/SBV/BitVectors/PrettyNum.hs b/Data/SBV/BitVectors/PrettyNum.hs --- a/Data/SBV/BitVectors/PrettyNum.hs +++ b/Data/SBV/BitVectors/PrettyNum.hs @@ -12,12 +12,17 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeSynonymInstances #-} -module Data.SBV.BitVectors.PrettyNum (PrettyNum(..), readBin, shex, shexI, sbin, sbinI) where +module Data.SBV.BitVectors.PrettyNum ( + PrettyNum(..), readBin, shex, shexI, sbin, sbinI + , showCFloat, showCDouble, showHFloat, showHDouble + , showSMTFloat, showSMTDouble, smtRoundingMode + ) where import Data.Char (ord) import Data.Int (Int8, Int16, Int32, Int64) import Data.List (isPrefixOf) import Data.Maybe (fromJust) +import Data.Ratio (numerator, denominator) import Data.Word (Word8, Word16, Word32, Word64) import Numeric (showIntAtBase, showHex, readInt) @@ -166,3 +171,73 @@ isDigit = (`elem` "01") s' | "0b" `isPrefixOf` s = drop 2 s | True = s + +-- | A version of show for floats that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included. +showCFloat :: Float -> String +showCFloat f + | isNaN f = "((float) NAN)" + | isInfinite f, f < 0 = "((float) (-INFINITY))" + | isInfinite f = "((float) INFINITY)" + | True = show f ++ "F" + +-- | A version of show for doubles that generates correct C literals for nan/infinite. NB. Requires "math.h" to be included. +showCDouble :: Double -> String +showCDouble f + | isNaN f = "((double) NAN)" + | isInfinite f, f < 0 = "((double) (-INFINITY))" + | isInfinite f = "((double) INFINITY)" + | True = show f + +-- | A version of show for floats that generates correct Haskell literals for nan/infinite +showHFloat :: Float -> String +showHFloat f + | isNaN f = "((0/0) :: Float)" + | isInfinite f, f < 0 = "((-1/0) :: Float)" + | isInfinite f = "((1/0) :: Float)" + | True = show f + +-- | A version of show for doubles that generates correct Haskell literals for nan/infinite +showHDouble :: Double -> String +showHDouble d + | isNaN d = "((0/0) :: Double)" + | isInfinite d, d < 0 = "((-1/0) :: Double)" + | isInfinite d = "((1/0) :: Double)" + | True = show d + +-- | A version of show for floats that generates correct SMTLib literals using the rounding mode +showSMTFloat :: RoundingMode -> Float -> String +showSMTFloat rm f + | isNaN f = as "NaN" + | isInfinite f, f < 0 = as "minusInfinity" + | isInfinite f = as "plusInfinity" + | isNegativeZero f = "(- ((_ asFloat 8 24) " ++ smtRoundingMode rm ++ " (/ 0 1)))" + | True = "((_ asFloat 8 24) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational f) ++ ")" + where as s = "(as " ++ s ++ " (_ FP 8 24))" + +-- | A version of show for doubles that generates correct SMTLib literals using the rounding mode +showSMTDouble :: RoundingMode -> Double -> String +showSMTDouble rm d + | isNaN d = as "NaN" + | isInfinite d, d < 0 = as "minusInfinity" + | isInfinite d = as "plusInfinity" + | isNegativeZero d = "(- ((_ asFloat 11 53) " ++ smtRoundingMode rm ++ " (/ 0 1)))" + | True = "((_ asFloat 11 53) " ++ smtRoundingMode rm ++ " " ++ toSMTLibRational (toRational d) ++ ")" + where as s = "(as " ++ s ++ " (_ FP 11 53))" + +-- | Show a rational in SMTLib format +toSMTLibRational :: Rational -> String +toSMTLibRational r + | n < 0 + = "(- (/ " ++ show (abs n) ++ " " ++ show d ++ "))" + | True + = "(/ " ++ show n ++ " " ++ show d ++ ")" + where n = numerator r + d = denominator r + +-- | Convert a rounding mode to the format SMT-Lib2 understands. +smtRoundingMode :: RoundingMode -> String +smtRoundingMode RoundNearestTiesToEven = "roundNearestTiesToEven" +smtRoundingMode RoundNearestTiesToAway = "roundNearestTiesToAway" +smtRoundingMode RoundTowardPositive = "roundTowardPositive" +smtRoundingMode RoundTowardNegative = "roundTowardNegative" +smtRoundingMode RoundTowardZero = "roundTowardZero" diff --git a/Data/SBV/BitVectors/SignCast.hs b/Data/SBV/BitVectors/SignCast.hs --- a/Data/SBV/BitVectors/SignCast.hs +++ b/Data/SBV/BitVectors/SignCast.hs @@ -85,6 +85,8 @@ KBounded True _ -> error "Data.SBV.SignCast.genericSign: Called on signed value" KUnbounded -> error "Data.SBV.SignCast.genericSign: Called on unbounded value" KReal -> error "Data.SBV.SignCast.genericSign: Called on real value" + KFloat -> error "Data.SBV.SignCast.genericSign: Called on float value" + KDouble -> error "Data.SBV.SignCast.genericSign: Called on double value" KUninterpreted s -> error $ "Data.SBV.SignCast.genericSign: Called on unintepreted sort " ++ s y st = do xsw <- sbvToSW st x newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw]) @@ -99,6 +101,8 @@ KBounded False _ -> error "Data.SBV.SignCast.genericUnSign: Called on unsigned value" KUnbounded -> error "Data.SBV.SignCast.genericUnSign: Called on unbounded value" KReal -> error "Data.SBV.SignCast.genericUnSign: Called on real value" + KFloat -> error "Data.SBV.SignCast.genericUnSign: Called on float value" + KDouble -> error "Data.SBV.SignCast.genericUnSign: Called on double value" KUninterpreted s -> error $ "Data.SBV.SignCast.genericUnSign: Called on unintepreted sort " ++ s y st = do xsw <- sbvToSW st x newExpr st k (SBVApp (Extract (intSizeOf x-1) 0) [xsw]) diff --git a/Data/SBV/Bridge/Boolector.hs b/Data/SBV/Bridge/Boolector.hs --- a/Data/SBV/Bridge/Boolector.hs +++ b/Data/SBV/Bridge/Boolector.hs @@ -14,10 +14,12 @@ -- - "Data.SBV.Bridge.Z3" -- -- - "Data.SBV.Bridge.CVC4" +-- +-- - "Data.SBV.Bridge.MathSAT" --------------------------------------------------------------------------------- module Data.SBV.Bridge.Boolector ( - -- * CVC4 specific interface + -- * Boolector specific interface sbvCurrentSolver -- ** Proving and checking satisfiability , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable diff --git a/Data/SBV/Bridge/CVC4.hs b/Data/SBV/Bridge/CVC4.hs --- a/Data/SBV/Bridge/CVC4.hs +++ b/Data/SBV/Bridge/CVC4.hs @@ -14,6 +14,8 @@ -- - "Data.SBV.Bridge.Z3" -- -- - "Data.SBV.Bridge.Boolector" +-- +-- - "Data.SBV.Bridge.MathSAT" --------------------------------------------------------------------------------- module Data.SBV.Bridge.CVC4 ( diff --git a/Data/SBV/Bridge/MathSAT.hs b/Data/SBV/Bridge/MathSAT.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Bridge/MathSAT.hs @@ -0,0 +1,107 @@ +--------------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Bridge.MathSAT +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Interface to the MathSAT SMT solver. Import this module if you want to use the +-- MathSAT SMT prover as your backend solver. Also see: +-- +-- - "Data.SBV.Bridge.Yices" +-- +-- - "Data.SBV.Bridge.Z3" +-- +-- - "Data.SBV.Bridge.CVC4" +-- +-- - "Data.SBV.Bridge.Boolector" +--------------------------------------------------------------------------------- + +module Data.SBV.Bridge.MathSAT ( + -- * MathSAT specific interface + sbvCurrentSolver + -- ** Proving and checking satisfiability + , prove, sat, allSat, isVacuous, isTheorem, isSatisfiable + -- ** Optimization routines + , optimize, minimize, maximize + -- * Non-MathSAT 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 = mathSAT + +-- | 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. +-} diff --git a/Data/SBV/Bridge/Yices.hs b/Data/SBV/Bridge/Yices.hs --- a/Data/SBV/Bridge/Yices.hs +++ b/Data/SBV/Bridge/Yices.hs @@ -14,6 +14,8 @@ -- - "Data.SBV.Bridge.CVC4" -- -- - "Data.SBV.Bridge.Z3" +-- +-- - "Data.SBV.Bridge.MathSAT" --------------------------------------------------------------------------------- module Data.SBV.Bridge.Yices ( diff --git a/Data/SBV/Bridge/Z3.hs b/Data/SBV/Bridge/Z3.hs --- a/Data/SBV/Bridge/Z3.hs +++ b/Data/SBV/Bridge/Z3.hs @@ -14,6 +14,8 @@ -- - "Data.SBV.Bridge.CVC4" -- -- - "Data.SBV.Bridge.Yices" +-- +-- - "Data.SBV.Bridge.MathSAT" --------------------------------------------------------------------------------- module Data.SBV.Bridge.Z3 ( diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs --- a/Data/SBV/Compilers/C.hs +++ b/Data/SBV/Compilers/C.hs @@ -13,18 +13,18 @@ module Data.SBV.Compilers.C(compileToC, compileToCLib, compileToC', compileToCLib') where -import Control.DeepSeq (rnf) -import Data.Char (isSpace) -import Data.List (nub, intercalate) -import Data.Maybe (isJust, isNothing, fromJust) -import qualified Data.Foldable as F (toList) -import System.FilePath (takeBaseName, replaceExtension) +import Control.DeepSeq (rnf) +import Data.Char (isSpace) +import Data.List (nub, intercalate) +import Data.Maybe (isJust, isNothing, fromJust) +import qualified Data.Foldable as F (toList) +import qualified Data.Set as Set (member, toList) +import System.FilePath (takeBaseName, replaceExtension) import System.Random import Text.PrettyPrint.HughesPJ import Data.SBV.BitVectors.Data -import Data.SBV.BitVectors.AlgReals -import Data.SBV.BitVectors.PrettyNum (shex) +import Data.SBV.BitVectors.PrettyNum (shex, showCFloat, showCDouble) import Data.SBV.Compilers.CodeGen --------------------------------------------------------------------------- @@ -164,6 +164,8 @@ KBounded b i -> spec (b, i) KUnbounded -> spec (True, fromJust (cgInteger cfg)) KReal -> specF (fromJust (cgReal cfg)) + KFloat -> specF CgFloat + KDouble -> specF CgDouble KUninterpreted s -> die $ "uninterpreted sort: " ++ s where spec :: (Bool, Int) -> Doc spec (False, 1) = text "%d" @@ -193,6 +195,8 @@ sRealSuffix CgLongDouble = text "L" mkConst cfg (CW KUnbounded (CWInteger i)) = showSizedConst i (True, fromJust (cgInteger cfg)) mkConst _ (CW (KBounded sg sz) (CWInteger i)) = showSizedConst i (sg, sz) +mkConst _ (CW KFloat (CWFloat f)) = text $ showCFloat f +mkConst _ (CW KDouble (CWDouble d)) = text $ showCDouble d mkConst _ cw = die $ "mkConst: " ++ show cw showSizedConst :: Integer -> (Bool, Int) -> Doc @@ -260,10 +264,17 @@ $$ text "#include " $$ text "#include " $$ text "#include " + $$ text "#include " $$ text "" $$ text "/* The boolean type */" $$ text "typedef bool SBool;" $$ text "" + $$ text "/* The float type */" + $$ text "typedef float SFloat;" + $$ text "" + $$ text "/* The double type */" + $$ text "typedef double SDouble;" + $$ text "" $$ text "/* Unsigned bit-vectors */" $$ text "typedef uint8_t SWord8 ;" $$ text "typedef uint16_t SWord16;" @@ -312,6 +323,7 @@ $$ text "#include " $$ text "#include " $$ text "#include " + $$ text "#include " $$ text "#include " header = text "#include" <+> doubleQuotes (nm <> text ".h") $$ text "" @@ -381,11 +393,11 @@ -- | Generate the C program genCProg :: CgConfig -> String -> Doc -> Result -> [(String, CgVal)] -> [(String, CgVal)] -> Maybe SW -> Doc -> [Doc] -genCProg cfg fn proto (Result (hasIntegers, hasReals) usorts _tvals cgs ins preConsts tbls arrs _ _ (SBVPgm asgns) cstrs _) inVars outVars mbRet extDecls - | isNothing (cgInteger cfg) && hasIntegers +genCProg cfg fn proto (Result kindInfo _tvals cgs ins preConsts tbls arrs _ _ (SBVPgm asgns) cstrs _) inVars outVars mbRet extDecls + | isNothing (cgInteger cfg) && KUnbounded `Set.member` kindInfo = error $ "SBV->C: Unbounded integers are not supported by the C compiler." ++ "\nUse 'cgIntegerSize' to specify a fixed size for SInteger representation." - | isNothing (cgReal cfg) && hasReals + | isNothing (cgReal cfg) && KReal `Set.member` kindInfo = error $ "SBV->C: SReal values are not supported by the C compiler." ++ "\nUse 'cgSRealType' to specify a custom type for SReal representation." | not (null usorts) @@ -398,11 +410,13 @@ = error "SBV->C: Cannot compile functions with existentially quantified variables." | True = [pre, header, post] - where pre = text "/* File:" <+> doubleQuotes (nm <> text ".c") <> text ". Automatically generated by SBV. Do not edit! */" + where usorts = [s | KUninterpreted s <- Set.toList kindInfo] + pre = text "/* File:" <+> doubleQuotes (nm <> text ".c") <> text ". Automatically generated by SBV. Do not edit! */" $$ text "" $$ text "#include " $$ text "#include " $$ text "#include " + $$ text "#include " header = text "#include" <+> doubleQuotes (nm <> text ".h") post = text "" $$ vcat (map codeSeg cgs) @@ -425,6 +439,8 @@ $$ text "" typeWidth = getMax 0 [len (kindOf s) | (s, _) <- assignments] where len (KReal{}) = 5 + len (KFloat{}) = 6 -- SFloat + len (KDouble{}) = 7 -- SDouble len (KUnbounded{}) = 8 len (KBounded False 1) = 5 -- SBool len (KBounded False n) = 5 + length (show n) -- SWordN @@ -502,6 +518,8 @@ (needsCheckL, needsCheckR) = case k of KBounded sg sz -> (sg, canOverflow sg sz) KReal -> die "array index with real value" + KFloat -> die "array index with float value" + KDouble -> die "array index with double value" KUnbounded -> case cgInteger cfg of Nothing -> (True, True) -- won't matter, it'll be rejected later Just i -> (True, canOverflow True i) @@ -661,6 +679,7 @@ $$ text "#include " $$ text "#include " $$ text "#include " + $$ text "#include " $$ text "#include " $$ inc mkDFun (f, [_pre, _header, body, _post]) = [header, body, post] diff --git a/Data/SBV/Examples/CodeGeneration/AddSub.hs b/Data/SBV/Examples/CodeGeneration/AddSub.hs --- a/Data/SBV/Examples/CodeGeneration/AddSub.hs +++ b/Data/SBV/Examples/CodeGeneration/AddSub.hs @@ -55,10 +55,17 @@ -- #include -- #include -- #include +-- #include -- -- /* The boolean type */ -- typedef bool SBool; -- +-- /* The float type */ +-- typedef float SFloat; +-- +-- /* The double type */ +-- typedef double SDouble; +-- -- /* Unsigned bit-vectors */ -- typedef uint8_t SWord8 ; -- typedef uint16_t SWord16; @@ -84,6 +91,7 @@ -- #include -- #include -- #include +-- #include -- #include -- #include "addSub.h" -- @@ -107,6 +115,7 @@ -- #include -- #include -- #include +-- #include -- #include "addSub.h" -- -- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum, diff --git a/Data/SBV/Examples/CodeGeneration/PopulationCount.hs b/Data/SBV/Examples/CodeGeneration/PopulationCount.hs --- a/Data/SBV/Examples/CodeGeneration/PopulationCount.hs +++ b/Data/SBV/Examples/CodeGeneration/PopulationCount.hs @@ -117,10 +117,17 @@ -- #include -- #include -- #include +-- #include -- -- /* The boolean type */ -- typedef bool SBool; -- +-- /* The float type */ +-- typedef float SFloat; +-- +-- /* The double type */ +-- typedef double SDouble; +-- -- /* Unsigned bit-vectors */ -- typedef uint8_t SWord8 ; -- typedef uint16_t SWord16; @@ -145,6 +152,7 @@ -- #include -- #include -- #include +-- #include -- #include -- #include "popCount.h" -- @@ -163,6 +171,7 @@ -- #include -- #include -- #include +-- #include -- #include "popCount.h" -- -- SWord8 popCount(const SWord64 x) diff --git a/Data/SBV/Examples/Existentials/Diophantine.hs b/Data/SBV/Examples/Existentials/Diophantine.hs --- a/Data/SBV/Examples/Existentials/Diophantine.hs +++ b/Data/SBV/Examples/Existentials/Diophantine.hs @@ -44,9 +44,11 @@ -- | Find the basis solution. By definition, the basis has all non-trivial (i.e., non-0) solutions -- that cannot be written as the sum of two other solutions. We use the mathematically equivalent -- statement that a solution is in the basis if it's least according to the lexicographic --- order using the ordinary less-than relation. +-- order using the ordinary less-than relation. (NB. We explicitly tell z3 to use the logic +-- AUFLIA for this problem, as the BV solver that is chosen automatically has a performance +-- issue. See: https://z3.codeplex.com/workitem/88.) basis :: [[SInteger]] -> IO [[Integer]] -basis m = extractModels `fmap` allSat cond +basis m = extractModels `fmap` allSatWith z3{useLogic = Just (PredefinedLogic AUFLIA)} cond where cond = do as <- mkExistVars n bs <- mkForallVars n return $ ok as &&& (ok bs ==> as .== bs ||| bnot (bs `less` as)) @@ -65,15 +67,15 @@ -- We have: -- -- >>> test --- NonHomogeneous [[0,2,0],[1,0,0]] [[0,1,1],[1,0,2]] +-- NonHomogeneous [[0,2,0],[1,0,0]] [[1,0,2],[0,1,1]] -- -- which means that the solutions are of the form: -- --- @(0, 2, 0) + k (0, 1, 1) + k' (1, 0, 2) = (k', 2+k, k+2k')@ +-- @(1, 0, 0) + k (0, 1, 1) + k' (1, 0, 2) = (1+k', k, k+2k')@ -- -- OR -- --- @(1, 0, 0) + k (0, 1, 1) + k' (1, 0, 2) = (1+k', k, k+2k')@ +-- @(0, 2, 0) + k (0, 1, 1) + k' (1, 0, 2) = (k', 2+k, k+2k')@ -- -- for arbitrary @k@, @k'@. It's easy to see that these are really solutions -- to the equation given. It's harder to see that they cover all possibilities, @@ -99,7 +101,7 @@ -- 4 x_5 = 5 x_6 + 1 -- @ -- --- We need to find to solve for x_0, over the naturals. We have: +-- We need to solve for x_0, over the naturals. We have: -- -- >>> sailors -- [15621,3124,2499,1999,1599,1279,1023] diff --git a/Data/SBV/Examples/Misc/Floating.hs b/Data/SBV/Examples/Misc/Floating.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Misc/Floating.hs @@ -0,0 +1,130 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Misc.Floating +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Several examples involving IEEE-754 floating point numbers, i.e., single +-- precision 'Float' ('SFloat') and double precision 'Double' ('SDouble') types. +-- +-- Note that arithmetic with floating point is full of surprises; due to precision +-- issues associativity of arithmetic operations typically do not hold. Also, +-- the presence of @NaN@ is always something to look out for. +----------------------------------------------------------------------------- + +module Data.SBV.Examples.Misc.Floating where + +import Data.SBV + +----------------------------------------------------------------------------- +-- * FP addition is not associative +----------------------------------------------------------------------------- + +-- | Prove that floating point addition is not associative. We have: +-- +-- >>> prove assocPlus +-- Falsifiable. Counter-example: +-- s0 = -Infinity :: SFloat +-- s1 = Infinity :: SFloat +-- s2 = -9.403955e-38 :: SFloat +-- +-- Indeed: +-- +-- >>> let i = 1/0 :: Float +-- >>> ((-i) + i) + (-9.403955e-38) :: Float +-- NaN +-- >>> (-i) + (i + (-9.403955e-38)) :: Float +-- NaN +-- +-- But keep in mind that @NaN@ does not equal itself in the floating point world! We have: +-- +-- >>> let nan = 0/0 :: Float in nan == nan +-- False +assocPlus :: SFloat -> SFloat -> SFloat -> SBool +assocPlus x y z = x + (y + z) .== (x + y) + z + +-- | Prove that addition is not associative, even if we ignore @NaN@/@Infinity@ values. +-- To do this, we use the predicate 'isFPPoint', which is true of a floating point +-- number ('SFloat' or 'SDouble') if it is neither @NaN@ nor @Infinity@. (That is, it's a +-- representable point in the real-number line.) +-- +-- We have: +-- +-- >>> assocPlusRegular +-- Falsifiable. Counter-example: +-- x = 1.5775295e-30 :: SFloat +-- y = 1.92593e-34 :: SFloat +-- z = -2.1521e-41 :: SFloat +-- +-- Indeed, we have: +-- +-- >>> (1.5775295e-30 + 1.92593e-34) + (-2.1521e-41) :: Float +-- 1.5777222e-30 +-- >>> 1.5775295e-30 + (1.92593e-34 + (-2.1521e-41)) :: Float +-- 1.577722e-30 +-- +-- Note the loss of precision in the second expression. +assocPlusRegular :: IO ThmResult +assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"] + let lhs = x+(y+z) + rhs = (x+y)+z + -- make sure we do not overflow at the intermediate points + constrain $ isFPPoint lhs + constrain $ isFPPoint rhs + return $ lhs .== rhs + +----------------------------------------------------------------------------- +-- * FP addition by non-zero can result in no change +----------------------------------------------------------------------------- + +-- | Demonstrate that @a+b = a@ does not necessarily mean @b@ is @0@ in the floating point world, +-- even when we disallow the obvious solution when @a@ and @b@ are @Infinity.@ +-- We have: +-- +-- >>> nonZeroAddition +-- Falsifiable. Counter-example: +-- a = -4.0 :: SFloat +-- b = 4.5918e-41 :: SFloat +-- +-- Indeed, we have: +-- +-- >>> -4.0 + 4.5918e-41 == (-4.0 :: Float) +-- True +-- +-- But: +-- +-- >>> 4.5918e-41 == (0 :: Float) +-- False +-- +nonZeroAddition :: IO ThmResult +nonZeroAddition = prove $ do [a, b] <- sFloats ["a", "b"] + constrain $ isFPPoint a + constrain $ isFPPoint b + constrain $ a + b .== a + return $ b .== 0 + +----------------------------------------------------------------------------- +-- * FP multiplicative inverses may not exist +----------------------------------------------------------------------------- + +-- | The last example illustrates that @a * (1/a)@ does not necessarily equal @1@. Again, +-- we protect against division by @0@ and @NaN@/@Infinity@. +-- +-- We have: +-- +-- >>> multInverse +-- Falsifiable. Counter-example: +-- a = 1.3999060872492817e-308 :: SDouble +-- +-- Indeed, we have: +-- +-- >>> let a = 1.3999060872492817e-308 :: Double +-- >>> a * (1/a) +-- 0.9999999999999999 +multInverse :: IO ThmResult +multInverse = prove $ do a <- sDouble "a" + constrain $ isFPPoint a + constrain $ isFPPoint (1/a) + return $ a * (1/a) .== 1 diff --git a/Data/SBV/Examples/Misc/ModelExtract.hs b/Data/SBV/Examples/Misc/ModelExtract.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Misc/ModelExtract.hs @@ -0,0 +1,46 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Misc.ModelExtract +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Demonstrates use of programmatic model extraction. When programming with +-- SBV, we typically use `sat`/`allSat` calls to compute models automatically. +-- In more advanced uses, however, the user might want to use programmable +-- extraction features to do fancier programming. We demonstrate some of +-- these utilities here. +----------------------------------------------------------------------------- + +module Data.SBV.Examples.Misc.ModelExtract where + +import Data.SBV + +-- | A simple function to generate a new integer value, that is not in the +-- given set of values. We also require the value to be non-negative +outside :: [Integer] -> IO SatResult +outside disallow = sat $ do x <- sInteger "x" + let notEq i = constrain $ x ./= literal i + mapM_ notEq disallow + return $ x .>= 0 + +-- | We now use "outside" repeatedly to generate 10 integers, such that we not only disallow +-- previously generated elements, but also any value that differs from previous solutions +-- by less than 5. Here, we use the `getModelValue` function. We could have also extracted the dictionary +-- via `getModelDictionary` and did fancier programming as well, as necessary. We have: +-- +-- >>> genVals +-- [45,40,35,30,25,20,15,10,5,0] +genVals :: IO [Integer] +genVals = go [] [] + where go _ model + | length model >= 10 = return model + go disallow model + = do res <- outside disallow + -- Look up the value of "x" in the generated model + -- Note that we simply get an integer here; but any + -- SBV known type would be OK as well. + case "x" `getModelValue` res of + Just c -> go [c-4 .. c+4] (c : model) + _ -> return model diff --git a/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Examples/Uninterpreted/UISortAllSat.hs @@ -0,0 +1,73 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Examples.Uninterpreted.UISortAllSat +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Demonstrates uninterpreted sorts and how all-sat behaves for them. +-- Thanks to Eric Seidel for the idea. +----------------------------------------------------------------------------- + +{-# LANGUAGE DeriveDataTypeable #-} + +module Data.SBV.Examples.Uninterpreted.UISortAllSat where + +import Data.Generics +import Data.SBV + +-- | A "list-like" data type, but one we plan to uninterpret at the SMT level. +-- The actual shape is really immaterial for us, but could be used as a proxy +-- to generate test cases or explore data-space in some other part of a program. +-- Note that we neither rely on the shape of this data, nor need the actual +-- constructors. +data L = Nil + | Cons Int L + deriving (Eq, Ord, Data, Typeable) + +-- | Declare instances to make 'L' a usable uninterpreted sort. Note that default +-- definitions suffice in each case. +instance SymWord L +instance HasKind L + +-- | An uninterpreted "classify" function. Really, we only care about +-- the fact that such a function exists, not what it does. +classify :: SBV L -> SInteger +classify = uninterpret "classify" + +-- | Formulate a query that essentially asserts a cardinality constraint on +-- the uninterpreted sort 'L'. The goal is to say there are precisely 3 +-- such things, as it might be the case. We manage this by declaring four +-- elements, and asserting that for a free variable of this sort, the +-- shape of the data matches one of these three instances. That is, we +-- assert that all the instances of the data 'L' can be classified into +-- 3 equivalence classes. Then, allSat returns all the possible instances, +-- which of course are all uninterpreted. +-- +-- As expected, we have: +-- +-- >>> genLs +-- Solution #1: +-- l = L!val!0 :: L +-- l0 = L!val!0 :: L +-- l1 = L!val!1 :: L +-- l2 = L!val!2 :: L +-- Solution #2: +-- l = L!val!2 :: L +-- l0 = L!val!0 :: L +-- l1 = L!val!1 :: L +-- l2 = L!val!2 :: L +-- Solution #3: +-- l = L!val!1 :: L +-- l0 = L!val!0 :: L +-- l1 = L!val!1 :: L +-- l2 = L!val!2 :: L +-- Found 3 different solutions. +genLs :: IO AllSatResult +genLs = allSatWith z3 + $ do [l, l0, l1, l2] <- symbolics ["l", "l0", "l1", "l2"] + constrain $ classify l0 .== 0 + constrain $ classify l1 .== 1 + constrain $ classify l2 .== 2 + return $ l .== l0 ||| l .== l1 ||| l .== l2 diff --git a/Data/SBV/Internals.hs b/Data/SBV/Internals.hs --- a/Data/SBV/Internals.hs +++ b/Data/SBV/Internals.hs @@ -15,12 +15,12 @@ -- * Running symbolic programs /manually/ Result, SBVRunMode(..), runSymbolic, runSymbolic' -- * Other internal structures useful for low-level programming - , SBV(..), slet, CW, mkConstCW, genVar, genVar_ + , SBV(..), slet, CW(..), Kind(..), CWVal(..), AlgReal(..), mkConstCW, genVar, genVar_ -- * Compilation to C , compileToC', compileToCLib', CgPgmBundle(..), CgPgmKind(..) ) where -import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW, mkConstCW) +import Data.SBV.BitVectors.Data (Result, SBVRunMode(..), runSymbolic, runSymbolic', SBV(..), CW(..), Kind(..), CWVal(..), AlgReal(..), mkConstCW) import Data.SBV.BitVectors.Model (genVar, genVar_, slet) import Data.SBV.Compilers.C (compileToC', compileToCLib') import Data.SBV.Compilers.CodeGen (CgPgmBundle(..), CgPgmKind(..)) diff --git a/Data/SBV/Provers/Boolector.hs b/Data/SBV/Provers/Boolector.hs --- a/Data/SBV/Provers/Boolector.hs +++ b/Data/SBV/Provers/Boolector.hs @@ -26,7 +26,7 @@ -- | 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. +-- The default options are @\"-m --smt2\"@. You can use the @SBV_BOOLECTOR_OPTIONS@ environment variable to override the options. boolector :: SMTSolver boolector = SMTSolver { name = "boolector" @@ -54,6 +54,8 @@ , supportsUninterpretedSorts = False , supportsUnboundedInts = False , supportsReals = False + , supportsFloats = False + , supportsDoubles = False } } where addTimeOut Nothing o = o diff --git a/Data/SBV/Provers/CVC4.hs b/Data/SBV/Provers/CVC4.hs --- a/Data/SBV/Provers/CVC4.hs +++ b/Data/SBV/Provers/CVC4.hs @@ -52,6 +52,8 @@ , supportsUninterpretedSorts = True , supportsUnboundedInts = True , supportsReals = True -- Not quite the same capability as Z3; but works more or less.. + , supportsFloats = False + , supportsDoubles = False } } where zero :: Kind -> String @@ -59,6 +61,8 @@ zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' zero KUnbounded = "0" zero KReal = "0.0" + zero KFloat = error "SBV.CVC4.zero: Unexpected float value" + zero KDouble = error "SBV.CVC4.zero: Unexpected double value" zero (KUninterpreted s) = error $ "SBV.CVC4.zero: Unexpected uninterpreted sort: " ++ s cont skolemMap = intercalate "\n" $ map extract skolemMap where extract (Left s) = "(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")" diff --git a/Data/SBV/Provers/MathSAT.hs b/Data/SBV/Provers/MathSAT.hs new file mode 100644 --- /dev/null +++ b/Data/SBV/Provers/MathSAT.hs @@ -0,0 +1,92 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Data.SBV.Provers.MathSAT +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- The connection to the MathSAT SMT solver +----------------------------------------------------------------------------- + +{-# LANGUAGE ScopedTypeVariables #-} + +module Data.SBV.Provers.MathSAT(mathSAT) where + +import qualified Control.Exception as C + +import Data.Function (on) +import Data.List (sortBy, intercalate) +import System.Environment (getEnv) + +import Data.SBV.BitVectors.Data +import Data.SBV.SMT.SMT +import Data.SBV.SMT.SMTLib + +-- | The description of the MathSAT SMT solver +-- The default executable is @\"mathsat\"@, which must be in your path. You can use the @SBV_MATHSAT@ environment variable to point to the executable on your system. +-- The default options are @\"-input=smt2\"@. You can use the @SBV_MATHSAT_OPTIONS@ environment variable to override the options. +mathSAT :: SMTSolver +mathSAT = SMTSolver { + name = "MathSAT" + , executable = "mathsat" + , options = ["-input=smt2"] + , engine = \cfg _isSat qinps modelMap skolemMap pgm -> do + execName <- getEnv "SBV_MATHSAT" `C.catch` (\(_ :: C.SomeException) -> return (executable (solver cfg))) + execOpts <- (words `fmap` getEnv "SBV_MATHSAT_OPTIONS") `C.catch` (\(_ :: C.SomeException) -> return (options (solver cfg))) + let cfg' = cfg { solver = (solver cfg) {executable = execName, options = addTimeOut (timeOut cfg) execOpts} + } + tweaks = case solverTweaks cfg' of + [] -> "" + ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"] + script = SMTScript {scriptBody = tweaks ++ pgm, scriptModel = Just (cont skolemMap)} + standardSolver cfg' script id (ProofError cfg') (interpretSolverOutput cfg' (extractMap (map snd qinps) modelMap)) + , xformExitCode = id + , capabilities = SolverCapabilities { + capSolverName = "MathSAT" + , mbDefaultLogic = Nothing + , supportsMacros = False + , supportsProduceModels = True + , supportsQuantifiers = True + , supportsUninterpretedSorts = True + , supportsUnboundedInts = True + , supportsReals = True + , supportsFloats = False + , supportsDoubles = False + } + } + where zero :: Kind -> String + zero (KBounded False 1) = "#b0" + zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' + zero KUnbounded = "0" + zero KReal = "0.0" + zero KFloat = error "SBV.MathSAT.zero: Unexpected sort SFloat" + zero KDouble = error "SBV.MathSAT.zero: Unexpected sort SDouble" + zero (KUninterpreted s) = error $ "SBV.MathSAT.zero: Unexpected uninterpreted sort: " ++ s + cont skolemMap = intercalate "\n" $ concatMap extract skolemMap + where -- In the skolemMap: + -- * Left's are universals: i.e., the model should be true for + -- any of these. So, we simply "echo 0" for these values. + -- * Right's are existentials. If there are no dependencies (empty list), then we can + -- simply use get-value to extract it's value. Otherwise, we have to apply it to + -- an appropriate number of 0's to get the final value. + extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"] + extract (Right (s, [])) = ["(get-value (" ++ show s ++ "))"] + extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero (kindOf a) | a <- ss] ++ ")))" in [g] + addTimeOut Nothing o = o + addTimeOut (Just _) _ = error "MathSAT: Timeout values are not supported by MathSat" + +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) + 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 diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs --- a/Data/SBV/Provers/Prover.hs +++ b/Data/SBV/Provers/Prover.hs @@ -25,20 +25,21 @@ , isVacuous, isVacuousWith , solve , SatModel(..), Modelable(..), displayModels, extractModels - , boolector, cvc4, yices, z3, defaultSMTCfg + , getModelDictionaries, getModelValues, getModelUninterpretedValues + , boolector, cvc4, yices, z3, mathSAT, defaultSMTCfg , compileToSMTLib, generateSMTBenchmarks , sbvCheckSolverInstallation ) where -import qualified Control.Exception as E - -import Control.Concurrent (forkIO, newChan, writeChan, getChanContents) -import Control.Monad (when, unless, void) +import Control.Monad (when, unless) import Data.List (intercalate) -import Data.Maybe (fromJust, isJust, mapMaybe) -import System.FilePath (addExtension) +import Data.Maybe (mapMaybe) +import System.FilePath (addExtension, splitExtension) import System.Time (getClockTime) +import System.IO.Unsafe (unsafeInterleaveIO) +import qualified Data.Set as Set (Set, toList) + import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.Model import Data.SBV.SMT.SMT @@ -47,6 +48,7 @@ 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.MathSAT as MathSAT import Data.SBV.Utils.TDiff import Data.SBV.Utils.Boolean @@ -61,6 +63,8 @@ , solverTweaks = tweaks , useSMTLib2 = isSMTLib2 , satCmd = "(check-sat)" + , roundingMode = RoundNearestTiesToEven + , useLogic = Nothing } -- | Default configuration for the Boolector SMT solver @@ -79,6 +83,10 @@ z3 :: SMTConfig z3 = mkConfig Z3.z3 True ["(set-option :smt.mbqi true) ; use model based quantifier instantiation"] +-- | Default configuration for the MathSAT SMT solver +mathSAT :: SMTConfig +mathSAT = mkConfig MathSAT.mathSAT True [] + -- | The default solver used by SBV. This is currently set to z3. defaultSMTCfg :: SMTConfig defaultSMTCfg = z3 @@ -365,11 +373,11 @@ -- | Determine if the constraints are vacuous using the given SMT-solver isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool isVacuousWith config a = do - Result ub us tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic True $ forAll_ a >>= output + Result ki tr uic is cs ts as uis ax asgn cstr _ <- runSymbolic True $ forAll_ a >>= output case cstr of [] -> return False -- no constraints, no need to check _ -> do let is' = [(EX, i) | (_, i) <- is] -- map all quantifiers to "exists" for the constraint check - res' = Result ub us tr uic is' cs ts as uis ax asgn cstr [trueSW] + res' = Result ki tr uic is' cs ts as uis ax asgn cstr [trueSW] cvt = if useSMTLib2 config then toSMTLib2 else toSMTLib1 SatResult result <- runProofOn cvt config True [] res' >>= callSolver True "Checking Satisfiability.." SatResult config case result of @@ -384,51 +392,47 @@ allSatWith config p = do let converter = if useSMTLib2 config then toSMTLib2 else toSMTLib1 msg "Checking Satisfiability, all solutions.." - sbvPgm@(qinps, _, _, usorts, _) <- simulate converter config True [] p - unless (null usorts) $ error $ "SBV.allSat: All-sat calls are not supported in the presence of uninterpreted sorts: " ++ unwords usorts - ++ "\n Only 'sat' and 'prove' calls are available when uninterpreted sorts are used." - resChan <- newChan - let add = writeChan resChan . Just - stop = writeChan resChan Nothing - final r = add r >> stop - die m = final (ProofError config [m]) - -- only fork if non-verbose.. otherwise stdout gets garbled - fork io = if verbose config then io else void (forkIO io) - fork $ E.catch (go sbvPgm add stop final (1::Int) []) - (\e -> die (show (e::E.SomeException))) - results <- getChanContents resChan + sbvPgm@(qinps, _, _, ki, _) <- simulate converter config True [] p + let usorts = [s | KUninterpreted s <- Set.toList ki] + unless (null usorts) $ msg $ "SBV.allSat: Uninterpreted sorts present: " ++ unwords usorts + ++ "\n SBV will use equivalence classes to generate all-satisfying instances." + results <- unsafeInterleaveIO $ go sbvPgm (1::Int) [] -- See if there are any existentials below any universals -- If such is the case, then the solutions are unique upto prefix existentials let w = ALL `elem` map fst qinps - return $ AllSatResult (w, map fromJust (takeWhile isJust results)) + return $ AllSatResult (w, results) where msg = when (verbose config) . putStrLn . ("** " ++) - go sbvPgm add stop final = loop + go sbvPgm = loop where loop !n nonEqConsts = do curResult <- invoke nonEqConsts n sbvPgm case curResult of - Nothing -> stop - Just (SatResult r) -> case r of - Satisfiable _ (SMTModel [] _ _) -> final r - Unknown _ (SMTModel [] _ _) -> final r - ProofError _ _ -> final r - TimeOut _ -> stop - Unsatisfiable _ -> stop - Satisfiable _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts) - Unknown _ model -> add r >> loop (n+1) (modelAssocs model : nonEqConsts) + Nothing -> return [] + Just (SatResult r) -> let cont model = do rest <- unsafeInterleaveIO $ loop (n+1) (modelAssocs model : nonEqConsts) + return (r : rest) + in case r of + Satisfiable _ (SMTModel [] _ _) -> return [r] + Unknown _ (SMTModel [] _ _) -> return [r] + ProofError _ _ -> return [r] + TimeOut _ -> return [] + Unsatisfiable _ -> return [] + Satisfiable _ model -> cont model + Unknown _ model -> cont model invoke nonEqConsts n (qinps, modelMap, skolemMap, _, smtLibPgm) = do msg $ "Looking for solution " ++ show n - case addNonEqConstraints qinps nonEqConsts smtLibPgm of + case addNonEqConstraints (roundingMode config) qinps nonEqConsts smtLibPgm of Nothing -> -- no new constraints added, stop return Nothing Just finalPgm -> do msg $ "Generated SMTLib program:\n" ++ finalPgm - smtAnswer <- engine (solver config) config True qinps modelMap skolemMap finalPgm + smtAnswer <- engine (solver config) (updateName (n-1) config) True qinps modelMap skolemMap finalPgm msg "Done.." return $ Just $ SatResult smtAnswer + updateName i cfg = cfg{smtFile = upd `fmap` smtFile cfg} + where upd nm = let (b, e) = splitExtension nm in b ++ "_allSat_" ++ show i ++ e type SMTProblem = ( [(Quantifier, NamedSymVar)] -- inputs , [(String, UnintKind)] -- model-map , [Either SW (SW, [SW])] -- skolem-map - , [String] -- uninterpreted sorts + , Set.Set Kind -- kinds used , SMTLibPgm -- SMTLib representation ) @@ -457,18 +461,19 @@ 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 - skolemMap = skolemize (if isSat then is else map flipQ is) - where flipQ (ALL, x) = (EX, x) - flipQ (EX, x) = (ALL, x) - skolemize :: [(Quantifier, NamedSymVar)] -> [Either SW (SW, [SW])] - skolemize qinps = go qinps ([], []) - 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 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 + Result ki _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 + skolemMap = skolemize (if isSat then is else map flipQ is) + where flipQ (ALL, x) = (EX, x) + flipQ (EX, x) = (ALL, x) + skolemize :: [(Quantifier, NamedSymVar)] -> [Either SW (SW, [SW])] + skolemize qinps = go qinps ([], []) + 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, ki, converter (roundingMode config) (useLogic config) solverCaps ki isSat comments is skolemMap consts tbls arrs uis axs pgm cstrs o) + Result _kindInfo _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 ++ "\nDetected while generating the trace:\n" ++ show res diff --git a/Data/SBV/Provers/SExpr.hs b/Data/SBV/Provers/SExpr.hs --- a/Data/SBV/Provers/SExpr.hs +++ b/Data/SBV/Provers/SExpr.hs @@ -14,15 +14,18 @@ import Control.Monad.Error () -- for Monad (Either String) instance import Data.Char (isDigit, ord) import Data.List (isPrefixOf) -import Numeric (readInt, readDec, readHex) +import Numeric (readInt, readDec, readHex, fromRat) import Data.SBV.BitVectors.AlgReals +import Data.SBV.BitVectors.Data (nan, infinity) -- | ADT S-Expression format, suitable for representing get-model output of SMT-Lib -data SExpr = SCon String - | SNum Integer - | SReal AlgReal - | SApp [SExpr] +data SExpr = ECon String + | ENum Integer + | EReal AlgReal + | EFloat Float + | EDouble Double + | EApp [SExpr] deriving Show -- | Parse a string into an SExpr, potentially failing with an error message @@ -41,7 +44,7 @@ ++ "\n*** Input : <" ++ inp ++ ">" parse [] = die "ran out of tokens" parse ("(":toks) = do (f, r) <- parseApp toks [] - f' <- cvt (SApp f) + f' <- cvt (EApp f) return (f', r) parse (")":_) = die "extra tokens after close paren" parse [tok] = do t <- pTok tok @@ -53,8 +56,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 "false" = return $ ENum 0 + pTok "true" = return $ ENum 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 @@ -63,28 +66,57 @@ | not (null n) && isDigit (head n) = if '.' `elem` n then getReal n else mkNum $ readDec n - pTok n = return $ SCon n - mkNum [(n, "")] = return $ SNum n + pTok n = return $ ECon n + mkNum [(n, "")] = return $ ENum n mkNum _ = die "cannot read number" - getReal n = return $ SReal $ mkPolyReal (Left (exact, n')) + getReal n = return $ EReal $ mkPolyReal (Left (exact, n')) where exact = not ("?" `isPrefixOf` reverse n) n' | exact = n | True = init n -- simplify numbers and root-obj values - cvt (SApp [SCon "/", SReal a, SReal b]) = return $ SReal (a / b) - cvt (SApp [SCon "/", SReal a, SNum b]) = return $ SReal (a / fromInteger b) - cvt (SApp [SCon "/", SNum a, SReal b]) = return $ SReal (fromInteger a / b) - cvt (SApp [SCon "/", SNum a, SNum b]) = return $ SReal (fromInteger a / fromInteger b) - cvt (SApp [SCon "-", SReal a]) = return $ SReal (-a) - cvt (SApp [SCon "-", SNum a]) = return $ SNum (-a) + cvt (EApp [ECon "/", EReal a, EReal b]) = return $ EReal (a / b) + cvt (EApp [ECon "/", EReal a, ENum b]) = return $ EReal (a / fromInteger b) + cvt (EApp [ECon "/", ENum a, EReal b]) = return $ EReal (fromInteger a / b) + cvt (EApp [ECon "/", ENum a, ENum b]) = return $ EReal (fromInteger a / fromInteger b) + cvt (EApp [ECon "-", EReal a]) = return $ EReal (-a) + cvt (EApp [ECon "-", ENum a]) = return $ ENum (-a) -- bit-vector value as CVC4 prints: (_ bv0 16) for instance - cvt (SApp [SCon "_", SNum a, SNum _b]) = return $ SNum a - cvt (SApp [SCon "root-obj", SApp (SCon "+":trms), SNum k]) = do ts <- mapM getCoeff trms - return $ SReal $ mkPolyReal (Right (k, ts)) + cvt (EApp [ECon "_", ENum a, ENum _b]) = return $ ENum a + cvt (EApp [ECon "root-obj", EApp (ECon "+":trms), ENum k]) = do ts <- mapM getCoeff trms + return $ EReal $ mkPolyReal (Right (k, ts)) + cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FP", ENum 11, ENum 53]]) = getDouble n + cvt (EApp [ECon "as", n, EApp [ECon "_", ECon "FP", ENum 8, ENum 24]]) = getFloat n cvt x = return x - getCoeff (SApp [SCon "*", SNum k, SApp [SCon "^", SCon "x", SNum p]]) = return (k, p) -- kx^p - getCoeff (SApp [SCon "*", SNum k, SCon "x" ] ) = return (k, 1) -- kx - getCoeff ( SApp [SCon "^", SCon "x", SNum p] ) = return (1, p) -- x^p - getCoeff ( SCon "x" ) = return (1, 1) -- x - getCoeff ( SNum k ) = return (k, 0) -- k + getCoeff (EApp [ECon "*", ENum k, EApp [ECon "^", ECon "x", ENum p]]) = return (k, p) -- kx^p + getCoeff (EApp [ECon "*", ENum k, ECon "x" ] ) = return (k, 1) -- kx + getCoeff ( EApp [ECon "^", ECon "x", ENum p] ) = return (1, p) -- x^p + getCoeff ( ECon "x" ) = return (1, 1) -- x + getCoeff ( ENum k ) = return (k, 0) -- k getCoeff x = die $ "Cannot parse a root-obj,\nProcessing term: " ++ show x + getDouble (ECon s) = case (s, rdFP (dropWhile (== '+') s)) of + ("plusInfinity", _ ) -> return $ EDouble infinity + ("minusInfinity", _ ) -> return $ EDouble (-infinity) + ("NaN", _ ) -> return $ EDouble nan + (_, Just v) -> return $ EDouble v + _ -> die $ "Cannot parse a double value from: " ++ s + getDouble (EReal r) = return $ EDouble $ fromRat $ toRational r + getDouble x = die $ "Cannot parse a double value from: " ++ show x + getFloat (ECon s) = case (s, rdFP (dropWhile (== '+') s)) of + ("plusInfinity", _ ) -> return $ EFloat infinity + ("minusInfinity", _ ) -> return $ EFloat (-infinity) + ("NaN", _ ) -> return $ EFloat nan + (_, Just v) -> return $ EFloat v + _ -> die $ "Cannot parse a float value from: " ++ s + getFloat (EReal r) = return $ EFloat $ fromRat $ toRational r + getFloat x = die $ "Cannot parse a float value from: " ++ show x + +-- | Parses the Z3 floating point formatted numbers like so: 1.321p5/1.2123e9 etc. +rdFP :: (Read a, RealFloat a) => String -> Maybe a +rdFP s = case break (`elem` "pe") s of + (m, 'p':e) -> rd m >>= \m' -> rd e >>= \e' -> return $ m' * ( 2 ** e') + (m, 'e':e) -> rd m >>= \m' -> rd e >>= \e' -> return $ m' * (10 ** e') + (m, "") -> rd m + _ -> Nothing + where rd v = case reads v of + [(n, "")] -> Just n + _ -> Nothing diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs --- a/Data/SBV/Provers/Yices.hs +++ b/Data/SBV/Provers/Yices.hs @@ -51,6 +51,8 @@ , supportsUninterpretedSorts = False , supportsUnboundedInts = False , supportsReals = False + , supportsFloats = False + , supportsDoubles = False } } where addTimeOut Nothing o = o @@ -90,9 +92,9 @@ matches -> error $ "SBV.Yices: Cannot uniquely identify value for " ++ 's':v ++ " in " ++ show matches isInput _ = Nothing - extract (SApp [SCon "=", SCon v, SNum i]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))] - extract (SApp [SCon "=", SNum i, SCon v]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))] - extract _ = [] + extract (EApp [ECon "=", ECon v, ENum i]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))] + extract (EApp [ECon "=", ENum i, ECon v]) | Just (n, s, nm) <- isInput v = [(n, (nm, mkConstCW (kindOf s) i))] + extract _ = [] extractUnints :: [(String, UnintKind)] -> [String] -> [(UnintKind, [String])] extractUnints modelMap = mapMaybe (extractUnint modelMap) . chunks @@ -122,21 +124,21 @@ = getDefaultVal knd (dropWhile (/= ' ') s) | True = case parseSExpr s of - Right (SApp [SCon "=", SApp (SCon _ : args), SNum i]) -> getCallVal knd args i - Right (SApp [SCon "=", SCon _, SNum i]) -> getCallVal knd [] i + Right (EApp [ECon "=", EApp (ECon _ : args), ENum i]) -> getCallVal knd args i + Right (EApp [ECon "=", ECon _, ENum i]) -> getCallVal knd [] i _ -> Nothing getDefaultVal :: UnintKind -> String -> Maybe (String, [String], String) getDefaultVal knd n = case parseSExpr n of - Right (SNum i) -> Just $ showDefault knd (show i) + Right (ENum i) -> Just $ showDefault knd (show i) _ -> Nothing getCallVal :: UnintKind -> [SExpr] -> Integer -> Maybe (String, [String], String) getCallVal knd args res = mapM getArg args >>= \as -> return (showCall knd as (show res)) getArg :: SExpr -> Maybe String -getArg (SNum i) = Just (show i) -getArg _ = Nothing +getArg (ENum i) = Just (show i) +getArg _ = Nothing showDefault :: UnintKind -> String -> (String, [String], String) showDefault (UFun cnt f) res = (f, replicate cnt "_", res) diff --git a/Data/SBV/Provers/Z3.hs b/Data/SBV/Provers/Z3.hs --- a/Data/SBV/Provers/Z3.hs +++ b/Data/SBV/Provers/Z3.hs @@ -23,6 +23,7 @@ import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data +import Data.SBV.BitVectors.PrettyNum import Data.SBV.SMT.SMT import Data.SBV.SMT.SMTLib @@ -50,7 +51,7 @@ ts -> unlines $ "; --- user given solver tweaks ---" : ts ++ ["; --- end of user given tweaks ---"] dlim = printRealPrec cfg' ppDecLim = "(set-option :pp.decimal_precision " ++ show dlim ++ ")\n" - script = SMTScript {scriptBody = tweaks ++ ppDecLim ++ pgm, scriptModel = Just (cont skolemMap)} + script = SMTScript {scriptBody = tweaks ++ ppDecLim ++ pgm, scriptModel = Just (cont (roundingMode cfg) 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)) @@ -64,27 +65,30 @@ , supportsUninterpretedSorts = True , supportsUnboundedInts = True , supportsReals = True + , supportsFloats = True + , supportsDoubles = True } } - where -- Get rid of the following when z3_4.0 is out - cleanErrs = intercalate "\n" . filter (not . junk) . lines + where cleanErrs = intercalate "\n" . filter (not . junk) . lines junk = ("WARNING:" `isPrefixOf`) - zero :: Kind -> String - zero (KBounded False 1) = "#b0" - zero (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' - zero KUnbounded = "0" - zero KReal = "0.0" - zero (KUninterpreted s) = error $ "SBV.Z3.zero: Unexpected uninterpreted sort: " ++ s - cont skolemMap = intercalate "\n" $ concatMap extract skolemMap + zero :: RoundingMode -> Kind -> String + zero _ (KBounded False 1) = "#b0" + zero _ (KBounded _ sz) = "#x" ++ replicate (sz `div` 4) '0' + zero _ KUnbounded = "0" + zero _ KReal = "0.0" + zero rm KFloat = showSMTFloat rm 0 + zero rm KDouble = showSMTDouble rm 0 + zero _ (KUninterpreted s) = error $ "SBV.Z3.zero: Unexpected uninterpreted sort: " ++ s + cont rm skolemMap = intercalate "\n" $ concatMap extract skolemMap where -- In the skolemMap: -- * Left's are universals: i.e., the model should be true for -- any of these. So, we simply "echo 0" for these values. -- * Right's are existentials. If there are no dependencies (empty list), then we can -- simply use get-value to extract it's value. Otherwise, we have to apply it to -- an appropriate number of 0's to get the final value. - extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero (kindOf s) ++ "))\")"] + extract (Left s) = ["(echo \"((" ++ show s ++ " " ++ zero rm (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 + extract (Right (s, ss)) = let g = "(get-value ((" ++ show s ++ concat [' ' : zero rm (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 _ g = [g] addTimeOut Nothing o = o diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs --- a/Data/SBV/SMT/SMT.hs +++ b/Data/SBV/SMT/SMT.hs @@ -28,6 +28,8 @@ import System.Exit (ExitCode(..)) import System.IO (hClose, hFlush, hPutStr, hGetContents, hGetLine) +import qualified Data.Map as M + import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data import Data.SBV.BitVectors.PrettyNum @@ -47,16 +49,18 @@ -- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation -- of the real value is not finite, i.e., if it is not rational. data SMTConfig = SMTConfig { - verbose :: Bool -- ^ Debug mode - , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.) - , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds) - , printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.) - , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) - , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified) - , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. - , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly) - , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1 - , solver :: SMTSolver -- ^ The actual SMT solver. + verbose :: Bool -- ^ Debug mode + , timing :: Bool -- ^ Print timing information on how long different phases took (construction, solving, etc.) + , timeOut :: Maybe Int -- ^ How much time to give to the solver. (In seconds) + , printBase :: Int -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.) + , printRealPrec :: Int -- ^ Print algebraic real values with this precision. (SReal, default: 16) + , solverTweaks :: [String] -- ^ Additional lines of script to give to the solver (user specified) + , satCmd :: String -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics. + , smtFile :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly) + , useSMTLib2 :: Bool -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1 + , solver :: SMTSolver -- ^ The actual SMT solver. + , roundingMode :: RoundingMode -- ^ Rounding mode to use for floating-point conversions + , useLogic :: Maybe Logic -- ^ If Nothing, pick automatically. Otherwise, either use the given one, or use the custom string. } -- | An SMT engine @@ -74,9 +78,9 @@ -- | A model, as returned by a solver data SMTModel = SMTModel { - modelAssocs :: [(String, CW)] - , modelArrays :: [(String, [String])] -- very crude! - , modelUninterps :: [(String, [String])] -- very crude! + modelAssocs :: [(String, CW)] -- ^ Mapping of symbolic values to constants. + , modelArrays :: [(String, [String])] -- ^ Arrays, very crude; only works with Yices. + , modelUninterps :: [(String, [String])] -- ^ Uninterpreted funcs; very crude; only works with Yices. } deriving Show @@ -263,6 +267,19 @@ -- | Extract a model, the result is a tuple where the first argument (if True) -- indicates whether the model was "probable". (i.e., if the solver returned unknown.) getModel :: SatModel b => a -> Either String (Bool, b) + -- | Extract a model dictionary. Extract a dictionary mapping the variables to + -- their respective values as returned by the SMT solver. Also see `getModelDictionaries`. + getModelDictionary :: a -> M.Map String CW + -- | Extract a model value for a given element. Also see `getModelValues`. + getModelValue :: SymWord b => String -> a -> Maybe b + getModelValue v r = fromCW `fmap` (v `M.lookup` getModelDictionary r) + -- | Extract a representative name for the model value of an uninterpreted kind. + -- This is supposed to correspond to the value as computed internally by the + -- SMT solver; and is unportable from solver to solver. Also see `getModelUninterpretedValues`. + getModelUninterpretedValue :: String -> a -> Maybe String + getModelUninterpretedValue v r = case v `M.lookup` getModelDictionary r of + Just (CW _ (CWUninterpreted s)) -> Just s + _ -> Nothing -- | A simpler variant of 'getModel' to get a model out without the fuss. extractModel :: SatModel b => a -> Maybe b @@ -275,13 +292,27 @@ extractModels :: SatModel a => AllSatResult -> [a] extractModels (AllSatResult (_, xs)) = [ms | Right (_, ms) <- map getModel xs] +-- | Get dictionaries from an all-sat call. Similar to `getModelDictionary`. +getModelDictionaries :: AllSatResult -> [M.Map String CW] +getModelDictionaries (AllSatResult (_, xs)) = map getModelDictionary xs + +-- | Extract value of a variable from an all-sat call. Similar to `getModelValue`. +getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b] +getModelValues s (AllSatResult (_, xs)) = map (s `getModelValue`) xs + +-- | Extract value of an uninterpreted variable from an all-sat call. Similar to `getModelUninterpretedValue`. +getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String] +getModelUninterpretedValues s (AllSatResult (_, xs)) = map (s `getModelUninterpretedValue`) xs + instance Modelable ThmResult where - getModel (ThmResult r) = getModel r - modelExists (ThmResult r) = modelExists r + getModel (ThmResult r) = getModel r + modelExists (ThmResult r) = modelExists r + getModelDictionary (ThmResult r) = getModelDictionary r instance Modelable SatResult where - getModel (SatResult r) = getModel r - modelExists (SatResult r) = modelExists r + getModel (SatResult r) = getModel r + modelExists (SatResult r) = modelExists r + getModelDictionary (SatResult r) = getModelDictionary r instance Modelable SMTResult where getModel (Unsatisfiable _) = Left "SBV.getModel: Unsatisfiable result" @@ -292,6 +323,11 @@ modelExists (Satisfiable{}) = True modelExists (Unknown{}) = False -- don't risk it modelExists _ = False + getModelDictionary (Unsatisfiable _) = M.empty + getModelDictionary (Unknown _ m) = M.fromList (modelAssocs m) + getModelDictionary (ProofError _ _) = M.empty + getModelDictionary (TimeOut _) = M.empty + getModelDictionary (Satisfiable _ m) = M.fromList (modelAssocs m) -- | Extract a model out, will throw error if parsing is unsuccessful parseModelOut :: SatModel a => SMTModel -> a @@ -396,7 +432,7 @@ msg $ "Calling: " ++ show (unwords (exec:opts)) case smtFile config of Nothing -> return () - Just f -> do putStrLn $ "** Saving the generated script in file: " ++ show f + Just f -> do msg $ "Saving the generated script in file: " ++ show f writeFile f (scriptBody script) contents <- timeIf isTiming nmSolver $ pipeProcess config nmSolver exec opts script cleanErrs msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents diff --git a/Data/SBV/SMT/SMTLib.hs b/Data/SBV/SMT/SMTLib.hs --- a/Data/SBV/SMT/SMTLib.hs +++ b/Data/SBV/SMT/SMTLib.hs @@ -19,12 +19,15 @@ import qualified Data.SBV.SMT.SMTLib1 as SMT1 import qualified Data.SBV.SMT.SMTLib2 as SMT2 +import qualified Data.Set as Set (Set, member, toList) + -- | 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 +type SMTLibConverter = RoundingMode -- ^ User selected rounding mode to be used for floating point arithmetic + -> Maybe Logic -- ^ User selected logic to use. If Nothing, pick automatically. + -> SolverCapabilities -- ^ Capabilities of the backend solver targeted + -> Set.Set Kind -- ^ Kinds used in the problem -> Bool -- ^ is this a sat problem? -> [String] -- ^ extra comments to place on top - -> [String] -- ^ uninterpreted sorts -> [(Quantifier, NamedSymVar)] -- ^ inputs and aliasing names -> [Either SW (SW, [SW])] -- ^ skolemized inputs -> [(SW, CW)] -- ^ constants @@ -43,30 +46,37 @@ -- | Convert to SMTLib-2 format toSMTLib2 :: SMTLibConverter (toSMTLib1, toSMTLib2) = (cvt SMTLib1, cvt SMTLib2) - where cvt v solverCaps boundedInfo@(needsIntegers, needsReals) isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out - | needsIntegers && not (supportsUnboundedInts solverCaps) + where cvt v roundMode smtLogic solverCaps kindInfo isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out + | KUnbounded `Set.member` kindInfo && not (supportsUnboundedInts solverCaps) = unsupported "unbounded integers" - | needsReals && not (supportsReals solverCaps) + | KReal `Set.member` kindInfo && not (supportsReals solverCaps) = unsupported "algebraic reals" + | needsFloats && not (supportsFloats solverCaps) + = unsupported "single-precision floating-point numbers" + | needsDoubles && not (supportsDoubles solverCaps) + = unsupported "double-precision floating-point numbers" | 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 + where sorts = [s | KUninterpreted s <- Set.toList kindInfo] + 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 solverCaps boundedInfo isSat comments sorts qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out + (pre, post) = converter roundMode smtLogic solverCaps kindInfo isSat comments qinps skolemMap consts tbls arrs uis axs asgnsSeq cstrs out + needsFloats = KFloat `Set.member` kindInfo + needsDoubles = KDouble `Set.member` kindInfo 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 -addNonEqConstraints _qinps cs p@(SMTLibPgm SMTLib1 _) = SMT1.addNonEqConstraints cs p -addNonEqConstraints qinps cs p@(SMTLibPgm SMTLib2 _) = SMT2.addNonEqConstraints qinps cs p +addNonEqConstraints :: RoundingMode -> [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String +addNonEqConstraints rm _qinps cs p@(SMTLibPgm SMTLib1 _) = SMT1.addNonEqConstraints rm cs p +addNonEqConstraints rm qinps cs p@(SMTLibPgm SMTLib2 _) = SMT2.addNonEqConstraints rm qinps cs p -- | Interpret solver output based on SMT-Lib standard output responses interpretSolverOutput :: SMTConfig -> ([String] -> SMTModel) -> [String] -> SMTResult @@ -86,8 +96,8 @@ where err r = error $ "*** Failed to parse SMT-Lib2 model output from: " ++ "*** " ++ show line ++ "\n" ++ "*** Reason: " ++ r ++ "\n" - getInput (SCon v) = isInput v - getInput (SApp (SCon v : _)) = isInput v + getInput (ECon v) = isInput v + getInput (EApp (ECon v : _)) = isInput v getInput _ = Nothing isInput ('s':v) | all isDigit v = let inpId :: Int @@ -98,12 +108,14 @@ matches -> error $ "SBV.SMTLib2: Cannot uniquely identify value for " ++ 's':v ++ " in " ++ show matches isInput _ = Nothing - extract (SApp [SApp [v, SNum i]]) | Just (n, s, nm) <- getInput v = [(n, (nm, mkConstCW (kindOf s) i))] - extract (SApp [SApp [v, SReal i]]) | Just (n, _, nm) <- getInput v = [(n, (nm, CW KReal (CWAlgReal i)))] - extract (SApp [SApp [v, SCon i]]) | Just (n, s, nm) <- getInput v = [(n, (nm, CW (kindOf s) (CWUninterpreted i)))] + extract (EApp [EApp [v, ENum i]]) | Just (n, s, nm) <- getInput v = [(n, (nm, mkConstCW (kindOf s) i))] + extract (EApp [EApp [v, EReal i]]) | Just (n, s, nm) <- getInput v, isReal s = [(n, (nm, CW KReal (CWAlgReal i)))] + extract (EApp [EApp [v, ECon i]]) | Just (n, s, nm) <- getInput v, isUninterpreted s = [(n, (nm, CW (kindOf s) (CWUninterpreted i)))] + extract (EApp [EApp [v, EDouble i]]) | Just (n, s, nm) <- getInput v, isDouble s = [(n, (nm, CW KDouble (CWDouble i)))] + extract (EApp [EApp [v, EFloat i]]) | Just (n, s, nm) <- getInput v, isFloat s = [(n, (nm, CW KFloat (CWFloat i)))] -- weird lambda app that CVC4 seems to throw out.. logic below derived from what I saw CVC4 print, hopefully sufficient - extract (SApp (SApp (v : SApp (SCon "LAMBDA" : xs) : _) : _)) | Just{} <- getInput v, not (null xs) = extract (SApp [SApp [v, last xs]]) - extract (SApp [SApp (v : r)]) | Just (_, _, nm) <- getInput v = error $ "SBV.SMTLib2: Cannot extract value for " ++ show nm + extract (EApp (EApp (v : EApp (ECon "LAMBDA" : xs) : _) : _)) | Just{} <- getInput v, not (null xs) = extract (EApp [EApp [v, last xs]]) + extract (EApp [EApp (v : r)]) | Just (_, _, nm) <- getInput v = error $ "SBV.SMTLib2: Cannot extract value for " ++ show nm ++ "\n\tInput: " ++ show line ++ "\n\tParse: " ++ show r extract _ = [] diff --git a/Data/SBV/SMT/SMTLib1.hs b/Data/SBV/SMT/SMTLib1.hs --- a/Data/SBV/SMT/SMTLib1.hs +++ b/Data/SBV/SMT/SMTLib1.hs @@ -12,15 +12,16 @@ module Data.SBV.SMT.SMTLib1(cvt, addNonEqConstraints) where -import qualified Data.Foldable as F (toList) +import qualified Data.Foldable as F (toList) +import qualified Data.Set as Set import Data.List (intercalate) import Data.SBV.BitVectors.Data -- | Add constraints to generate /new/ models. This function is used to query the SMT-solver, while -- disallowing a previous model. -addNonEqConstraints :: [[(String, CW)]] -> SMTLibPgm -> Maybe String -addNonEqConstraints nonEqConstraints (SMTLibPgm _ (aliasTable, pre, post)) = Just $ intercalate "\n" $ +addNonEqConstraints :: RoundingMode -> [[(String, CW)]] -> SMTLibPgm -> Maybe String +addNonEqConstraints _rm nonEqConstraints (SMTLibPgm _ (aliasTable, pre, post)) = Just $ intercalate "\n" $ pre ++ [ " ; --- refuted-models ---" ] ++ concatMap nonEqs (map (map intName) nonEqConstraints) @@ -40,11 +41,12 @@ nonEq (s, c) = "(not (= " ++ s ++ " " ++ cvtCW c ++ "))" -- | Translate a problem into an SMTLib1 script -cvt :: SolverCapabilities -- ^ capabilities of the current solver - -> (Bool, Bool) -- ^ has infinite precision integers/reals +cvt :: RoundingMode -- ^ User selected rounding mode to be used for floating point arithmetic + -> Maybe Logic -- ^ SMT-Lib logic, if requested by the user + -> SolverCapabilities -- ^ capabilities of the current solver + -> Set.Set Kind -- ^ kinds used -> Bool -- ^ is this a sat problem? -> [String] -- ^ extra comments to place on top - -> [String] -- ^ uninterpreted sorts -> [(Quantifier, NamedSymVar)] -- ^ inputs -> [Either SW (SW, [SW])] -- ^ skolemized version of the inputs -> [(SW, CW)] -- ^ constants @@ -56,8 +58,9 @@ -> [SW] -- ^ extra constraints -> SW -- ^ output variable -> ([String], [String]) -cvt _solverCaps _boundInfo isSat comments _sorts qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out = (pre, post) +cvt _roundingMode smtLogic _solverCaps _kindInfo isSat comments qinps _skolemInps consts tbls arrs uis axs asgnsSeq cstrs out = (pre, post) where logic + | Just l <- smtLogic = show l | null tbls && null arrs && null uis = "QF_BV" | True = "QF_AUFBV" inps = map (fst . snd) qinps @@ -264,4 +267,6 @@ kindType (KBounded _ s) = "BitVec[" ++ show s ++ "]" kindType KUnbounded = die "unbounded Integer" kindType KReal = die "real value" +kindType KFloat = die "float value" +kindType KDouble = die "double value" kindType (KUninterpreted s) = die $ "uninterpreted sort: " ++ s diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -12,20 +12,24 @@ module Data.SBV.SMT.SMTLib2(cvt, addNonEqConstraints) where -import Data.Bits (bit) +import Data.Bits (bit) +import Data.Function (on) +import Data.Ord (comparing) import qualified Data.Foldable as F (toList) import qualified Data.Map as M import qualified Data.IntMap as IM -import Data.List (intercalate, partition) +import qualified Data.Set as Set +import Data.List (intercalate, partition, groupBy, sortBy) import Numeric (showHex) import Data.SBV.BitVectors.AlgReals import Data.SBV.BitVectors.Data +import Data.SBV.BitVectors.PrettyNum (showSMTFloat, showSMTDouble, smtRoundingMode) -- | Add constraints to generate /new/ models. This function is used to query the SMT-solver, while -- disallowing a previous model. -addNonEqConstraints :: [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String -addNonEqConstraints qinps allNonEqConstraints (SMTLibPgm _ (aliasTable, pre, post)) +addNonEqConstraints :: RoundingMode -> [(Quantifier, NamedSymVar)] -> [[(String, CW)]] -> SMTLibPgm -> Maybe String +addNonEqConstraints rm qinps allNonEqConstraints (SMTLibPgm _ (aliasTable, pre, post)) | null allNonEqConstraints = Just $ intercalate "\n" $ pre ++ post | null refutedModel @@ -33,9 +37,9 @@ | True = Just $ intercalate "\n" $ pre ++ [ "; --- refuted-models ---" ] - ++ concatMap nonEqs (map (map intName) nonEqConstraints) + ++ refutedModel ++ post - where refutedModel = concatMap nonEqs (map (map intName) nonEqConstraints) + where refutedModel = concatMap (nonEqs rm) (map (map intName) nonEqConstraints) intName (s, c) | Just sw <- s `lookup` aliasTable = (show sw, c) | True = (s, c) @@ -43,25 +47,42 @@ nonEqConstraints = filter (not . null) $ map (filter (\(s, _) -> s `elem` topUnivs)) allNonEqConstraints topUnivs = [s | (_, (_, s)) <- takeWhile (\p -> fst p == EX) qinps] -nonEqs :: [(String, CW)] -> [String] -nonEqs [] = [] -nonEqs [sc] = ["(assert " ++ nonEq sc ++ ")"] -nonEqs (sc:r) = ["(assert (or " ++ nonEq sc] - ++ map ((" " ++) . nonEq) r - ++ [" ))"] +nonEqs :: RoundingMode -> [(String, CW)] -> [String] +nonEqs rm scs = format $ interp ps ++ disallow (map eqClass uninterpClasses) + where (ups, ps) = partition (isUninterpreted . snd) scs + format [] = [] + format [m] = ["(assert " ++ m ++ ")"] + format (m:ms) = ["(assert (or " ++ m] + ++ map (" " ++) ms + ++ [" ))"] + -- Regular (or interpreted) sorts simply get a constraint that we disallow the current assignment + interp = map $ nonEq rm + -- Determine the equivalnce classes of uninterpreted sorts: + uninterpClasses = filter (\l -> length l > 1) -- Only need this class if it has at least two members + . map (map fst) -- throw away sorts, we only need the names + . groupBy ((==) `on` snd) -- make sure they belong to the same sort and have the same value + . sortBy (comparing snd) -- sort them according to their sorts first + $ ups -- take the uninterpreted sorts + -- Uninterpreted sorts get a constraint that says the equivalence classes as determined by the solver are disallowed: + eqClass :: [String] -> String + eqClass [] = error "SBV.allSat.nonEqs: Impossible happened, disallow received an empty list" + eqClass cs = "(= " ++ unwords cs ++ ")" + -- Now, take the conjunction of equivalence classes and assert it's negation: + disallow = map $ \ec -> "(not " ++ ec ++ ")" -nonEq :: (String, CW) -> String -nonEq (s, c) = "(not (= " ++ s ++ " " ++ cvtCW c ++ "))" +nonEq :: RoundingMode -> (String, CW) -> String +nonEq rm (s, c) = "(not (= " ++ s ++ " " ++ cvtCW rm c ++ "))" tbd :: String -> a tbd e = error $ "SBV.SMTLib2: Not-yet-supported: " ++ e -- | Translate a problem into an SMTLib2 script -cvt :: SolverCapabilities -- ^ capabilities of the current solver - -> (Bool, Bool) -- ^ bounded info +cvt :: RoundingMode -- ^ User selected rounding mode to be used for floating point arithmetic + -> Maybe Logic -- ^ SMT-Lib logic, if requested by the user + -> SolverCapabilities -- ^ capabilities of the current solver + -> Set.Set Kind -- ^ kinds used -> Bool -- ^ is this a sat problem? -> [String] -- ^ extra comments to place on top - -> [String] -- ^ uninterpreted sorts -> [(Quantifier, NamedSymVar)] -- ^ inputs -> [Either SW (SW, [SW])] -- ^ skolemized version inputs -> [(SW, CW)] -- ^ constants @@ -73,9 +94,21 @@ -> [SW] -- ^ extra constraints -> SW -- ^ output variable -> ([String], [String]) -cvt solverCaps (hasInteger, hasReal) isSat comments sorts _inps skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, []) +cvt rm smtLogic solverCaps kindInfo isSat comments inputs skolemInps consts tbls arrs uis axs (SBVPgm asgnsSeq) cstrs out = (pre, []) where -- the logic is an over-approaximation + hasInteger = KUnbounded `Set.member` kindInfo + hasReal = KReal `Set.member` kindInfo + hasFloat = KFloat `Set.member` kindInfo + hasDouble = KDouble `Set.member` kindInfo + hasBVs = not $ null [() | KBounded{} <- Set.toList kindInfo] + sorts = [s | KUninterpreted s <- Set.toList kindInfo] logic + | Just l <- smtLogic + = ["(set-logic " ++ show l ++ ") ; NB. User specified."] + | hasDouble || hasFloat -- NB. We don't check for quantifiers here, we probably should.. + = if hasBVs + then ["(set-logic QF_FPABV)"] + else ["(set-logic QF_FPA)"] | hasInteger || hasReal || not (null sorts) = case mbDefaultLogic solverCaps of Nothing -> ["; Has unbounded values (Int/Real) or sorts; no logic specified."] -- combination, let the solver pick @@ -100,7 +133,7 @@ ++ [ "; --- literal constants ---" ] ++ concatMap (declConst (supportsMacros solverCaps)) consts ++ [ "; --- skolem constants ---" ] - ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType ss s ++ ")" | Right (s, ss) <- skolemInps] + ++ [ "(declare-fun " ++ show s ++ " " ++ swFunType ss s ++ ")" ++ userName s | Right (s, ss) <- skolemInps] ++ [ "; --- constant tables ---" ] ++ concatMap constTable constTables ++ [ "; --- skolemized tables ---" ] @@ -121,7 +154,7 @@ ++ [ impAlign (letAlign assertOut) ++ replicate noOfCloseParens ')' ] noOfCloseParens = length asgns + (if null foralls then 1 else 2) + (if null delayedEqualities then 0 else 1) (constTables, skolemTables) = ([(t, d) | (t, Left d) <- allTables], [(t, d) | (t, Right d) <- allTables]) - allTables = [(t, genTableData skolemMap (not (null foralls), forallArgs) (map fst consts) t) | t <- tbls] + allTables = [(t, genTableData rm skolemMap (not (null foralls), forallArgs) (map fst consts) t) | t <- tbls] (arrayConstants, allArrayDelayeds) = unzip $ map (declArray (not (null foralls)) (map fst consts) skolemMap) arrs delayedEqualities@(~(deH:deTs)) = concatMap snd skolemTables ++ concat allArrayDelayeds foralls = [s | Left s <- skolemInps] @@ -146,14 +179,17 @@ where mkConstTable (((t, _, _), _), _) = (t, "table" ++ show t) mkSkTable (((t, _, _), _), _) = (t, "table" ++ show t ++ forallArgs) asgns = F.toList asgnsSeq - mkLet (s, e) = "(let ((" ++ show s ++ " " ++ cvtExp skolemMap tableMap e ++ "))" + mkLet (s, e) = "(let ((" ++ show s ++ " " ++ cvtExp rm skolemMap tableMap e ++ "))" declConst useDefFun (s, c) - | useDefFun = ["(define-fun " ++ varT ++ " " ++ cvtCW c ++ ")"] + | useDefFun = ["(define-fun " ++ varT ++ " " ++ cvtCW rm c ++ ")"] | True = [ "(declare-fun " ++ varT ++ ")" - , "(assert (= " ++ show s ++ " " ++ cvtCW c ++ "))" + , "(assert (= " ++ show s ++ " " ++ cvtCW rm c ++ "))" ] where varT = show s ++ " " ++ swFunType [] s declSort s = "(declare-sort " ++ s ++ " 0)" + userName s = case s `lookup` map snd inputs of + Just u | show s /= u -> " ; tracks user variable " ++ show u + _ -> "" declUI :: (String, SBVType) -> [String] declUI (i, t) = ["(declare-fun " ++ i ++ " " ++ cvtType t ++ ")"] @@ -175,15 +211,15 @@ decl = "(declare-fun " ++ t ++ " (" ++ qs ++ smtType ak ++ ") " ++ smtType rk ++ ")" -- Left if all constants, Right if otherwise -genTableData :: SkolemMap -> (Bool, String) -> [SW] -> ((Int, Kind, Kind), [SW]) -> Either [String] [String] -genTableData skolemMap (_quantified, args) consts ((i, aknd, _), elts) +genTableData :: RoundingMode -> SkolemMap -> (Bool, String) -> [SW] -> ((Int, Kind, Kind), [SW]) -> Either [String] [String] +genTableData rm skolemMap (_quantified, args) consts ((i, aknd, _), elts) | null post = Left (map (topLevel . snd) pre) | True = Right (map (nested . snd) (pre ++ post)) where ssw = cvtSW skolemMap (pre, post) = partition fst (zipWith mkElt elts [(0::Int)..]) t = "table" ++ show i mkElt x k = (isReady, (idx, ssw x)) - where idx = cvtCW (mkConstCW aknd k) + where idx = cvtCW rm (mkConstCW aknd k) isReady = x `elem` consts topLevel (idx, v) = "(= (" ++ t ++ " " ++ idx ++ ") " ++ v ++ ")" nested (idx, v) = "(= (" ++ t ++ args ++ " " ++ idx ++ ") " ++ v ++ ")" @@ -232,6 +268,8 @@ smtType (KBounded _ sz) = "(_ BitVec " ++ show sz ++ ")" smtType KUnbounded = "Int" smtType KReal = "Real" +smtType KFloat = "(_ FP 8 24)" +smtType KDouble = "(_ FP 11 53)" smtType (KUninterpreted s) = s cvtType :: SBVType -> String @@ -255,24 +293,22 @@ hex sz v = "#x" ++ pad (sz `div` 4) (showHex v "") 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 - where CWAlgReal w = cwVal x -cvtCW x | not (isBounded x) = if w >= 0 then show w else "(- " ++ show (abs w) ++ ")" - where CWInteger w = cwVal x -cvtCW x | not (hasSign x) = hex (intSizeOf x) w - where CWInteger w = cwVal 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.. --- Hence, we punt and use binary notation in that particular case -cvtCW x | cwVal x == CWInteger least = mkMinBound (intSizeOf x) - where least = negate (2 ^ intSizeOf x) -cvtCW x = negIf (w < 0) $ hex (intSizeOf x) (abs w) - where CWInteger w = cwVal x +cvtCW :: RoundingMode -> CW -> String +cvtCW rm x + | isBoolean x, CWInteger w <- cwVal x = if w == 0 then "false" else "true" + | isUninterpreted x, CWUninterpreted s <- cwVal x = s + | isReal x, CWAlgReal r <- cwVal x = algRealToSMTLib2 r + | isFloat x, CWFloat f <- cwVal x = showSMTFloat rm f + | isDouble x, CWDouble d <- cwVal x = showSMTDouble rm d + | not (isBounded x), CWInteger w <- cwVal x = if w >= 0 then show w else "(- " ++ show (abs w) ++ ")" + | not (hasSign x) , CWInteger w <- cwVal x = hex (intSizeOf x) w + -- 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.. + -- Hence, we punt and use binary notation in that particular case + | hasSign x , CWInteger w <- cwVal x = if w == negate (2 ^ intSizeOf x) + then mkMinBound (intSizeOf x) + else negIf (w < 0) $ hex (intSizeOf x) (abs w) + | True = error $ "SBV.cvtCW: Impossible happened: Kind/Value disagreement on: " ++ show (kindOf x, x) negIf :: Bool -> String -> String negIf True a = "(bvneg " ++ a ++ ")" @@ -288,28 +324,42 @@ | Just tn <- i `IM.lookup` m = tn | True = error $ "SBV.SMTLib2: Cannot locate table " ++ show i -cvtExp :: SkolemMap -> TableMap -> SBVExpr -> String -cvtExp skolemMap tableMap expr@(SBVApp _ arguments) = sh expr +cvtExp :: RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String +cvtExp rm skolemMap tableMap expr@(SBVApp _ arguments) = sh expr where ssw = cvtSW skolemMap - bvOp = all isBounded arguments - intOp = any isInteger arguments - realOp = any isReal arguments - boolOp = all isBoolean arguments + bvOp = all isBounded arguments + intOp = any isInteger arguments + realOp = any isReal arguments + doubleOp = any isDouble arguments + floatOp = any isFloat 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 + addRM s = s ++ " " ++ smtRoundingMode rm lift2 o _ [x, y] = "(" ++ o ++ " " ++ x ++ " " ++ y ++ ")" lift2 o _ sbvs = error $ "SBV.SMTLib2.sh.lift2: Unexpected arguments: " ++ show (o, sbvs) + -- lift a binary operation with rounding-mode added; used for floating-point arithmetic + lift2WM o | doubleOp || floatOp = lift2 (addRM o) + | True = lift2 o lift2B bOp vOp | boolOp = lift2 bOp | True = lift2 vOp lift1B bOp vOp | boolOp = lift1 bOp | True = lift1 vOp - eq sgn sbvs + eqBV sgn sbvs | boolOp = lift2 "=" sgn sbvs | True = "(= " ++ lift2 "bvcomp" sgn sbvs ++ " #b1)" - neq sgn sbvs = "(not " ++ eq sgn sbvs ++ ")" + neqBV sgn sbvs = "(not " ++ eqBV sgn sbvs ++ ")" + equal sgn sbvs + | doubleOp = lift2 "==" sgn sbvs + | floatOp = lift2 "==" sgn sbvs + | True = lift2 "=" sgn sbvs + notEqual sgn sbvs + | doubleOp = "(not " ++ equal sgn sbvs ++ ")" + | floatOp = "(not " ++ equal sgn sbvs ++ ")" + | True = lift2 "distinct" sgn sbvs lift2S oU oS sgn = lift2 (if sgn then oS else oU) sgn lift1 o _ [x] = "(" ++ o ++ " " ++ x ++ ")" lift1 o _ sbvs = error $ "SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: " ++ show (o, sbvs) @@ -321,6 +371,8 @@ KBounded _ n -> (2::Integer)^n > fromIntegral l KUnbounded -> True KReal -> error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index" + KFloat -> error "SBV.SMT.SMTLib2.cvtExp: unexpected float valued index" + KDouble -> error "SBV.SMT.SMTLib2.cvtExp: unexpected double valued index" KUninterpreted s -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s lkUp = "(" ++ getTable tableMap t ++ " " ++ ssw i ++ ")" cond @@ -330,14 +382,20 @@ KBounded{} -> if hasSign i then ("bvslt", "bvsle") else ("bvult", "bvule") KUnbounded -> ("<", "<=") KReal -> ("<", "<=") + KFloat -> ("<", "<=") + KDouble -> ("<", "<=") KUninterpreted s -> error $ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " ++ s - mkCnst = cvtCW . mkConstCW (kindOf i) + mkCnst = cvtCW rm . mkConstCW (kindOf i) le0 = "(" ++ less ++ " " ++ ssw i ++ " " ++ mkCnst 0 ++ ")" gtl = "(" ++ leq ++ " " ++ mkCnst l ++ " " ++ ssw i ++ ")" 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) ++ ")" + sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm' ++ " " ++ unwords (map ssw args) ++ ")" + where -- slight hack needed here to take advantage of custom floating-point functions.. sigh. + fpSpecials = ["squareRoot", "fusedMA"] + nm' | (floatOp || doubleOp) && (nm `elem` fpSpecials) = addRM nm + | True = nm sh (SBVApp (Extract 0 0) [a]) -- special SInteger -> SReal conversion | kindOf a == KUnbounded = "(to_real " ++ ssw a ++ ")" @@ -351,12 +409,12 @@ | intOp = sh (SBVApp (Shr i) [a]) -- Haskell treats rotateR as shiftR for unbounded values | True = bad sh (SBVApp (Shl i) [a]) - | bvOp = shft ssw "bvshl" "bvshl" i a + | bvOp = shft rm ssw "bvshl" "bvshl" i a | i < 0 = sh (SBVApp (Shr (-i)) [a]) -- flip sign/direction | intOp = "(* " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftL by multiplication by 2^i | True = bad sh (SBVApp (Shr i) [a]) - | bvOp = shft ssw "bvlshr" "bvashr" i a + | bvOp = shft rm ssw "bvlshr" "bvashr" i a | i < 0 = sh (SBVApp (Shl (-i)) [a]) -- flip sign/direction | intOp = "(div " ++ ssw a ++ " " ++ show (bit i :: Integer) ++ ")" -- Implement shiftR by division by 2^i | True = bad @@ -379,6 +437,8 @@ = f (any hasSign args) (map ssw args) | realOp, Just f <- lookup op smtOpRealTable = f (any hasSign args) (map ssw args) + | floatOp || doubleOp, Just f <- lookup op smtOpFloatDoubleTable + = f (any hasSign args) (map ssw args) | Just f <- lookup op uninterpretedTable = f (map ssw args) | True @@ -388,25 +448,27 @@ , (Times, lift2 "bvmul") , (Quot, lift2S "bvudiv" "bvsdiv") , (Rem, lift2S "bvurem" "bvsrem") - , (Equal, eq) - , (NotEqual, neq) + , (Equal, eqBV) + , (NotEqual, neqBV) , (LessThan, lift2S "bvult" "bvslt") , (GreaterThan, lift2S "bvugt" "bvsgt") , (LessEq, lift2S "bvule" "bvsle") , (GreaterEq, lift2S "bvuge" "bvsge") ] smtOpRealTable = smtIntRealShared - ++ [ (Quot, lift2 "/") + ++ [ (Quot, lift2WM "/") ] smtOpIntTable = smtIntRealShared ++ [ (Quot, lift2 "div") , (Rem, lift2 "mod") ] - smtIntRealShared = [ (Plus, lift2 "+") - , (Minus, lift2 "-") - , (Times, lift2 "*") - , (Equal, lift2S "=" "=") - , (NotEqual, lift2S "distinct" "distinct") + smtOpFloatDoubleTable = smtIntRealShared + ++ [(Quot, lift2WM "/")] + smtIntRealShared = [ (Plus, lift2WM "+") + , (Minus, lift2WM "-") + , (Times, lift2WM "*") + , (Equal, equal) + , (NotEqual, notEqual) , (LessThan, lift2S "<" "<") , (GreaterThan, lift2S ">" ">") , (LessEq, lift2S "<=" "<=") @@ -420,8 +482,8 @@ rot :: (SW -> String) -> String -> Int -> SW -> String rot ssw o c x = "((_ " ++ o ++ " " ++ show c ++ ") " ++ ssw x ++ ")" -shft :: (SW -> String) -> String -> String -> Int -> SW -> String -shft ssw oW oS c x = "(" ++ o ++ " " ++ ssw x ++ " " ++ cvtCW c' ++ ")" +shft :: RoundingMode -> (SW -> String) -> String -> String -> Int -> SW -> String +shft rm ssw oW oS c x = "(" ++ o ++ " " ++ ssw x ++ " " ++ cvtCW rm c' ++ ")" where s = hasSign x c' = mkConstCW (kindOf x) c o = if s then oS else oW diff --git a/Data/SBV/Tools/ExpectedValue.hs b/Data/SBV/Tools/ExpectedValue.hs --- a/Data/SBV/Tools/ExpectedValue.hs +++ b/Data/SBV/Tools/ExpectedValue.hs @@ -38,7 +38,7 @@ let v' = zipWith (+) v t rnf v' `seq` warmup (n-1) v' runOnce :: StdGen -> IO [Integer] - runOnce g = do (_, Result _ _ _ _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' (Concrete g) (m >>= output) + runOnce g = do (_, Result _ _ _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' (Concrete g) (m >>= output) let cval o = case o `lookup` cs of Nothing -> error "SBV.expectedValue: Cannot compute expected-values in the presence of uninterpreted constants!" Just cw -> case (cwKind cw, cwVal cw) of diff --git a/Data/SBV/Tools/GenTest.hs b/Data/SBV/Tools/GenTest.hs --- a/Data/SBV/Tools/GenTest.hs +++ b/Data/SBV/Tools/GenTest.hs @@ -42,7 +42,7 @@ | True = do g <- newStdGen t <- tc g gen (i+1) (t:sofar) - tc g = do (_, Result _ _ tvals _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' (Concrete g) (m >>= output) + tc g = do (_, Result _ tvals _ _ cs _ _ _ _ _ cstrs os) <- runSymbolic' (Concrete g) (m >>= output) let cval = fromMaybe (error "Cannot generate tests in the presence of uninterpeted constants!") . (`lookup` cs) cond = all (cwToBool . cval) cstrs if cond @@ -121,6 +121,8 @@ KBounded True 32 -> "Int32" KBounded True 64 -> "Int64" KUnbounded -> "Integer" + KFloat -> "Float" + KDouble -> "Double" KReal -> error $ "SBV.renderTest: Unsupported real valued test value: " ++ show cw KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw @@ -128,6 +130,8 @@ KBounded False 1 -> take 5 (show (cwToBool cw) ++ repeat ' ') KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w KUnbounded -> let CWInteger w = cwVal cw in shexI False True w + KFloat -> let CWFloat w = cwVal cw in showHFloat w + KDouble -> let CWDouble w = cwVal cw in showHDouble w KReal -> let CWAlgReal w = cwVal cw in algRealToHaskell w KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us @@ -139,10 +143,17 @@ , "#include " , "#include " , "#include " + , "#include " , "" , "/* The boolean type */" , "typedef bool SBool;" , "" + , "/* The float type */" + , "typedef float SFloat;" + , "" + , "/* The double type */" + , "typedef double SDouble;" + , "" , "/* Unsigned bit-vectors */" , "typedef uint8_t SWord8 ;" , "typedef uint16_t SWord16;" @@ -196,6 +207,8 @@ KBounded True 16 -> "SInt16" KBounded True 32 -> "SInt32" KBounded True 64 -> "SInt64" + KFloat -> "SFloat" + KDouble -> "SDouble" KUnbounded -> error "SBV.renderTest: Unbounded integers are not supported when generating C test-cases." KReal -> error "SBV.renderTest: Real values are not supported when generating C test-cases." KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us @@ -205,6 +218,8 @@ KBounded False 1 -> if cwToBool cw then "true " else "false" KBounded sgn sz -> let CWInteger w = cwVal cw in shex False True (sgn, sz) w KUnbounded -> let CWInteger w = cwVal cw in shexI False True w + KFloat -> let CWFloat w = cwVal cw in showCFloat w + KDouble -> let CWDouble w = cwVal cw in showCDouble w KUninterpreted us -> error $ "SBV.renderTest: Unsupported uninterpreted sort: " ++ us KReal -> error "SBV.renderTest: Real values are not supported when generating C test-cases." outLine @@ -229,6 +244,8 @@ KBounded True 16 -> "%\"PRId16\"" KBounded True 32 -> "%\"PRId32\"L" KBounded True 64 -> "%\"PRId64\"LL" + KFloat -> "%f" + KDouble -> "%f" KUnbounded -> error "SBV.renderTest: Unsupported unbounded integers for C generation." KReal -> error "SBV.renderTest: Unsupported real valued values for C generation." _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw @@ -259,10 +276,14 @@ KBounded True 16 -> xlt 16 (cwVal cw) KBounded True 32 -> xlt 32 (cwVal cw) KBounded True 64 -> xlt 64 (cwVal cw) + KFloat -> error "SBV.renderTest: Float values are not supported when generating Forte test-cases." + KDouble -> error "SBV.renderTest: Double values are not supported when generating Forte test-cases." KReal -> error "SBV.renderTest: Real values are not supported when generating Forte test-cases." KUnbounded -> error "SBV.renderTest: Unbounded integers are not supported when generating Forte test-cases." _ -> error $ "SBV.renderTest: Unexpected CW: " ++ show cw xlt s (CWInteger v) = [toF (testBit v i) | i <- [s-1, s-2 .. 0]] + xlt _ (CWFloat r) = error $ "SBV.renderTest.Forte: Unexpected float value: " ++ show r + xlt _ (CWDouble r) = error $ "SBV.renderTest.Forte: Unexpected double value: " ++ show r xlt _ (CWAlgReal r) = error $ "SBV.renderTest.Forte: Unexpected real value: " ++ show r xlt _ (CWUninterpreted r) = error $ "SBV.renderTest.Forte: Unexpected uninterpreted value: " ++ show r mkLine (i, o) = "(" ++ mkTuple (form (fst ss) (concatMap blast i)) ++ ", " ++ mkTuple (form (snd ss) (concatMap blast o)) ++ ")" diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,6 +1,6 @@ SBV: SMT Based Verification in Haskell -Copyright (c) 2010-2013, Levent Erkok (erkokl@gmail.com) +Copyright (c) 2010-2014, Levent Erkok (erkokl@gmail.com) All rights reserved. Redistribution and use in source and binary forms, with or without diff --git a/SBVUnitTest/GoldFiles/addSub.gold b/SBVUnitTest/GoldFiles/addSub.gold --- a/SBVUnitTest/GoldFiles/addSub.gold +++ b/SBVUnitTest/GoldFiles/addSub.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -62,6 +69,7 @@ #include #include #include +#include #include #include "addSub.h" @@ -85,6 +93,7 @@ #include #include #include +#include #include "addSub.h" void addSub(const SWord8 x, const SWord8 y, SWord8 *sum, diff --git a/SBVUnitTest/GoldFiles/aes128Dec.gold b/SBVUnitTest/GoldFiles/aes128Dec.gold --- a/SBVUnitTest/GoldFiles/aes128Dec.gold +++ b/SBVUnitTest/GoldFiles/aes128Dec.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "aes128Dec.h" @@ -102,6 +110,7 @@ #include #include #include +#include #include "aes128Dec.h" void aes128Dec(const SWord32 *pt, const SWord32 *key, SWord32 *ct) diff --git a/SBVUnitTest/GoldFiles/aes128Enc.gold b/SBVUnitTest/GoldFiles/aes128Enc.gold --- a/SBVUnitTest/GoldFiles/aes128Enc.gold +++ b/SBVUnitTest/GoldFiles/aes128Enc.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "aes128Enc.h" @@ -102,6 +110,7 @@ #include #include #include +#include #include "aes128Enc.h" void aes128Enc(const SWord32 *pt, const SWord32 *key, SWord32 *ct) diff --git a/SBVUnitTest/GoldFiles/aes128Lib.gold b/SBVUnitTest/GoldFiles/aes128Lib.gold --- a/SBVUnitTest/GoldFiles/aes128Lib.gold +++ b/SBVUnitTest/GoldFiles/aes128Lib.gold @@ -4,6 +4,7 @@ #include #include #include +#include #include "aes128Lib.h" void aes128KeySchedule(const SWord32 *key, SWord32 *encKS, @@ -1742,6 +1743,7 @@ #include #include #include +#include #include "aes128Lib.h" void aes128BlockEncrypt(const SWord32 *pt, const SWord32 *xkey, @@ -2658,6 +2660,7 @@ #include #include #include +#include #include "aes128Lib.h" void aes128BlockDecrypt(const SWord32 *ct, const SWord32 *xkey, @@ -3577,10 +3580,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -3610,6 +3620,7 @@ #include #include #include +#include #include #include "aes128Lib.h" diff --git a/SBVUnitTest/GoldFiles/cgUninterpret.gold b/SBVUnitTest/GoldFiles/cgUninterpret.gold --- a/SBVUnitTest/GoldFiles/cgUninterpret.gold +++ b/SBVUnitTest/GoldFiles/cgUninterpret.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "tstShiftLeft.h" @@ -89,6 +97,7 @@ #include #include #include +#include #include "tstShiftLeft.h" /* User specified custom code for "SBV_SHIFTLEFT" */ diff --git a/SBVUnitTest/GoldFiles/codeGen1.gold b/SBVUnitTest/GoldFiles/codeGen1.gold --- a/SBVUnitTest/GoldFiles/codeGen1.gold +++ b/SBVUnitTest/GoldFiles/codeGen1.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -62,6 +69,7 @@ #include #include #include +#include #include #include "foo.h" @@ -114,6 +122,7 @@ #include #include #include +#include #include "foo.h" SInt16 foo(const SInt16 x, const SInt64 *xArr, SWord16 *z, diff --git a/SBVUnitTest/GoldFiles/crcUSB5_1.gold b/SBVUnitTest/GoldFiles/crcUSB5_1.gold --- a/SBVUnitTest/GoldFiles/crcUSB5_1.gold +++ b/SBVUnitTest/GoldFiles/crcUSB5_1.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "crcUSB5.h" @@ -79,6 +87,7 @@ #include #include #include +#include #include "crcUSB5.h" SWord16 crcUSB5(const SWord16 msg) diff --git a/SBVUnitTest/GoldFiles/crcUSB5_2.gold b/SBVUnitTest/GoldFiles/crcUSB5_2.gold --- a/SBVUnitTest/GoldFiles/crcUSB5_2.gold +++ b/SBVUnitTest/GoldFiles/crcUSB5_2.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "crcUSB5.h" @@ -79,6 +87,7 @@ #include #include #include +#include #include "crcUSB5.h" SWord16 crcUSB5(const SWord16 msg) diff --git a/SBVUnitTest/GoldFiles/fib1.gold b/SBVUnitTest/GoldFiles/fib1.gold --- a/SBVUnitTest/GoldFiles/fib1.gold +++ b/SBVUnitTest/GoldFiles/fib1.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "fib1.h" @@ -79,6 +87,7 @@ #include #include #include +#include #include "fib1.h" SWord64 fib1(const SWord64 n) diff --git a/SBVUnitTest/GoldFiles/fib2.gold b/SBVUnitTest/GoldFiles/fib2.gold --- a/SBVUnitTest/GoldFiles/fib2.gold +++ b/SBVUnitTest/GoldFiles/fib2.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "fib2.h" @@ -79,6 +87,7 @@ #include #include #include +#include #include "fib2.h" SWord64 fib2(const SWord64 n) diff --git a/SBVUnitTest/GoldFiles/gcd.gold b/SBVUnitTest/GoldFiles/gcd.gold --- a/SBVUnitTest/GoldFiles/gcd.gold +++ b/SBVUnitTest/GoldFiles/gcd.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "sgcd.h" @@ -79,6 +87,7 @@ #include #include #include +#include #include "sgcd.h" SWord8 sgcd(const SWord8 x, const SWord8 y) diff --git a/SBVUnitTest/GoldFiles/legato_c.gold b/SBVUnitTest/GoldFiles/legato_c.gold --- a/SBVUnitTest/GoldFiles/legato_c.gold +++ b/SBVUnitTest/GoldFiles/legato_c.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -62,6 +69,7 @@ #include #include #include +#include #include #include "legatoMult.h" @@ -85,6 +93,7 @@ #include #include #include +#include #include "legatoMult.h" void legatoMult(const SWord8 x, const SWord8 y, SWord8 *hi, diff --git a/SBVUnitTest/GoldFiles/merge.gold b/SBVUnitTest/GoldFiles/merge.gold --- a/SBVUnitTest/GoldFiles/merge.gold +++ b/SBVUnitTest/GoldFiles/merge.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "merge.h" @@ -93,6 +101,7 @@ #include #include #include +#include #include "merge.h" void merge(const SWord8 *xs, SWord8 *ys) diff --git a/SBVUnitTest/GoldFiles/popCount1.gold b/SBVUnitTest/GoldFiles/popCount1.gold --- a/SBVUnitTest/GoldFiles/popCount1.gold +++ b/SBVUnitTest/GoldFiles/popCount1.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "popCount.h" @@ -79,6 +87,7 @@ #include #include #include +#include #include "popCount.h" SWord8 popCount(const SWord64 x) diff --git a/SBVUnitTest/GoldFiles/popCount2.gold b/SBVUnitTest/GoldFiles/popCount2.gold --- a/SBVUnitTest/GoldFiles/popCount2.gold +++ b/SBVUnitTest/GoldFiles/popCount2.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "popCount.h" @@ -79,6 +87,7 @@ #include #include #include +#include #include "popCount.h" SWord8 popCount(const SWord64 x) diff --git a/SBVUnitTest/GoldFiles/selChecked.gold b/SBVUnitTest/GoldFiles/selChecked.gold --- a/SBVUnitTest/GoldFiles/selChecked.gold +++ b/SBVUnitTest/GoldFiles/selChecked.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "selChecked.h" @@ -79,6 +87,7 @@ #include #include #include +#include #include "selChecked.h" SWord8 selChecked(const SWord8 x) diff --git a/SBVUnitTest/GoldFiles/selUnchecked.gold b/SBVUnitTest/GoldFiles/selUnchecked.gold --- a/SBVUnitTest/GoldFiles/selUnchecked.gold +++ b/SBVUnitTest/GoldFiles/selUnchecked.gold @@ -33,10 +33,17 @@ #include #include #include +#include /* The boolean type */ typedef bool SBool; +/* The float type */ +typedef float SFloat; + +/* The double type */ +typedef double SDouble; + /* Unsigned bit-vectors */ typedef uint8_t SWord8 ; typedef uint16_t SWord16; @@ -61,6 +68,7 @@ #include #include #include +#include #include #include "selUnChecked.h" @@ -79,6 +87,7 @@ #include #include #include +#include #include "selUnChecked.h" SWord8 selUnChecked(const SWord8 x) diff --git a/SBVUnitTest/SBVTestCollection.hs b/SBVUnitTest/SBVTestCollection.hs --- a/SBVUnitTest/SBVTestCollection.hs +++ b/SBVUnitTest/SBVTestCollection.hs @@ -55,7 +55,8 @@ import qualified TestSuite.Uninterpreted.AUF as T10_01(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) +import qualified TestSuite.Uninterpreted.Sort as T10_04(testSuite) +import qualified TestSuite.Uninterpreted.Uninterpreted as T10_05(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* @@ -104,5 +105,6 @@ , ("auf1", True, T10_01.testSuite) , ("unint-axms", True, T10_02.testSuite) , ("auf2", True, T10_03.testSuite) - , ("unint", True, T10_04.testSuite) + , ("unint-sort", True, T10_04.testSuite) + , ("unint", True, T10_05.testSuite) ] diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs --- a/SBVUnitTest/SBVUnitTestBuildTime.hs +++ b/SBVUnitTest/SBVUnitTestBuildTime.hs @@ -2,4 +2,4 @@ module SBVUnitTestBuildTime (buildTime) where buildTime :: String -buildTime = "Thu Mar 21 21:14:54 PDT 2013" +buildTime = "Sun Feb 16 15:11:29 PST 2014" diff --git a/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs --- a/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs +++ b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs @@ -23,6 +23,7 @@ testSuite :: SBVTestSuite testSuite = mkTestSuite $ \_ -> test $ genReals + ++ genFloats ++ genQRems ++ genBinTest "+" (+) ++ genBinTest "-" (-) @@ -176,10 +177,7 @@ ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- i8s, y <- i8s , noOverflow x y] [x `sDivMod` y | x <- si8s, y <- si8s , noOverflow x y] ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- i16s, y <- i16s, noOverflow x y] [x `sDivMod` y | x <- si16s, y <- si16s, noOverflow x y] ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- i32s, y <- i32s, noOverflow x y] [x `sDivMod` y | x <- si32s, y <- si32s, noOverflow x y] - ++ (if divModInt64Bug -- see below - then [] - else zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- i64s, y <- i64s, noOverflow x y] [x `sDivMod` y | x <- si64s, y <- si64s, noOverflow x y] - ) + ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- i64s, y <- i64s, noOverflow x y] [x `sDivMod` y | x <- si64s, y <- si64s, noOverflow x y] ++ zipWith pair [("divMod", show x, show y, x `divMod'` y) | x <- iUBs, y <- iUBs] [x `sDivMod` y | x <- siUBs, y <- siUBs] ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w8s, y <- w8s ] [x `sQuotRem` y | x <- sw8s, y <- sw8s ] ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w16s, y <- w16s] [x `sQuotRem` y | x <- sw16s, y <- sw16s] @@ -195,6 +193,8 @@ pair (nm, x, y, (r1, r2)) (e1, e2) = (nm, x, y, show (fromIntegral r1 `asTypeOf` e1, fromIntegral r2 `asTypeOf` e2) == show (e1, e2)) mkTest (nm, x, y, s) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True" -- Haskell's divMod and quotRem overflows if x == minBound and y == -1 for bounded signed types; so avoid that case + -- NB. There's a bug filed against this; so remove this when it gets fixed: + -- See: https://ghc.haskell.org/trac/ghc/ticket/8695 noOverflow x y = not (x == minBound && y == -1) genReals :: [Test] @@ -212,6 +212,39 @@ where pair (x, y, a) b = (x, y, Just a == unliteral b) mkTest (nm, (x, y, s)) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True" +genFloats :: [Test] +genFloats = map mkTest $ + map ("+",) (zipWith pair [(show x, show y, x + y) | x <- fs, y <- fs ] [x + y | x <- sfs, y <- sfs ]) + ++ map ("-",) (zipWith pair [(show x, show y, x - y) | x <- fs, y <- fs ] [x - y | x <- sfs, y <- sfs ]) + ++ map ("*",) (zipWith pair [(show x, show y, x * y) | x <- fs, y <- fs ] [x * y | x <- sfs, y <- sfs ]) + ++ map ("<",) (zipWith pairB [( x, y, x < y) | x <- fs, y <- fs ] [x .< y | x <- sfs, y <- sfs ]) + ++ map ("<=",) (zipWith pairB [( x, y, x <= y) | x <- fs, y <- fs ] [x .<= y | x <- sfs, y <- sfs ]) + ++ map (">",) (zipWith pairB [( x, y, x > y) | x <- fs, y <- fs ] [x .> y | x <- sfs, y <- sfs ]) + ++ map (">=",) (zipWith pairB [( x, y, x >= y) | x <- fs, y <- fs ] [x .>= y | x <- sfs, y <- sfs ]) + ++ map ("==",) (zipWith pairB [( x, y, x == y) | x <- fs, y <- fs ] [x .== y | x <- sfs, y <- sfs ]) + ++ map ("/=",) (zipWith pairN [( x, y, x /= y) | x <- fs, y <- fs ] [x ./= y | x <- sfs, y <- sfs ]) + ++ map ("/",) (zipWith pair [(show x, show y, x / y) | x <- fs, y <- fs, y /= 0] [x / y | x <- sfs, y <- sfs, unliteral y /= Just 0]) + ++ map ("+",) (zipWith pair [(show x, show y, x + y) | x <- ds, y <- ds ] [x + y | x <- sds, y <- sds ]) + ++ map ("-",) (zipWith pair [(show x, show y, x - y) | x <- ds, y <- ds ] [x - y | x <- sds, y <- sds ]) + ++ map ("*",) (zipWith pair [(show x, show y, x * y) | x <- ds, y <- ds ] [x * y | x <- sds, y <- sds ]) + ++ map ("<",) (zipWith pairB [( x, y, x < y) | x <- ds, y <- ds ] [x .< y | x <- sds, y <- sds ]) + ++ map ("<=",) (zipWith pairB [( x, y, x <= y) | x <- ds, y <- ds ] [x .<= y | x <- sds, y <- sds ]) + ++ map (">",) (zipWith pairB [( x, y, x > y) | x <- ds, y <- ds ] [x .> y | x <- sds, y <- sds ]) + ++ map (">=",) (zipWith pairB [( x, y, x >= y) | x <- ds, y <- ds ] [x .>= y | x <- sds, y <- sds ]) + ++ map ("==",) (zipWith pairB [( x, y, x == y) | x <- ds, y <- ds ] [x .== y | x <- sds, y <- sds ]) + ++ map ("/=",) (zipWith pairN [( x, y, x /= y) | x <- ds, y <- ds ] [x ./= y | x <- sds, y <- sds ]) + ++ map ("/",) (zipWith pair [(show x, show y, x / y) | x <- ds, y <- ds, y /= 0] [x / y | x <- sds, y <- sds, unliteral y /= Just 0]) + where pair (x, y, a) b = (x, y, same a (unliteral b)) + same a (Just b) = (isNaN a &&& isNaN b) || (a == b) + same _ _ = False + pairB (x, y, a) b = (show x, show y, checkNaN f x y a (unliteral b)) where f v w = not (v || w) -- Other comparison: Both should be False + pairN (x, y, a) b = (show x, show y, checkNaN f x y a (unliteral b)) where f v w = v && w -- /=: Both should be True + checkNaN f x y a (Just b) + | isNaN x || isNaN y = f a b + | True = a == b + checkNaN _ _ _ _ _ = False + mkTest (nm, (x, y, s)) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y ~: s `showsAs` "True" + -- Concrete test data xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a] xsUnsigned = take 5 (iterate (1+) minBound) ++ take 5 (iterate (\x -> x-1) maxBound) @@ -272,16 +305,23 @@ siUBs = map literal iUBs rs :: [AlgReal] -rs = [fromRational (i % d) | i <- is, d <- ds] - where is = [-1000000 .. -999998] ++ [-2 .. 2] ++ [999998 .. 1000001] - ds = [2 .. 5] ++ [98 .. 102] ++ [999998 .. 1000000] +rs = [fromRational (i % d) | i <- nums, d <- dens] + where nums = [-1000000 .. -999998] ++ [-2 .. 2] ++ [999998 .. 1000001] + dens = [2 .. 5] ++ [98 .. 102] ++ [999998 .. 1000000] srs :: [SReal] srs = map literal rs +fs :: [Float] +fs = xs ++ [-0.5, 0, 0.5] ++ map (* (-1)) xs + where xs = [nan, infinity, 0.68302244, 0.5268265, 0.10283524, 5.8336496e-2] --- On 32 bit installations of GHC, divMod is buggy for Int64 --- Thus causing our tests to fail. See ticket: http://hackage.haskell.org/trac/ghc/ticket/7233 --- Luckily, it's easy to detect it and sidestep it until GHC is appropriately patched -divModInt64Bug :: Bool -divModInt64Bug = (1 `div` (minBound::Int64)) /= -1 -- Bug causes this expression to evaluate to 1 +sfs :: [SFloat] +sfs = map literal fs + +ds :: [Double] +ds = xs ++ [-0.5, 0, 0.5] ++ map (* (-1)) xs + where xs = [nan, infinity, 2.516632060108026e-2,0.8601891300751106,7.518897767550192e-2,1.1656043286207285e-2] + +sds :: [SDouble] +sds = map literal ds diff --git a/SBVUnitTest/TestSuite/Uninterpreted/Sort.hs b/SBVUnitTest/TestSuite/Uninterpreted/Sort.hs new file mode 100644 --- /dev/null +++ b/SBVUnitTest/TestSuite/Uninterpreted/Sort.hs @@ -0,0 +1,44 @@ +----------------------------------------------------------------------------- +-- | +-- Module : TestSuite.Uninterpreted.Sort +-- Copyright : (c) Levent Erkok +-- License : BSD3 +-- Maintainer : erkokl@gmail.com +-- Stability : experimental +-- +-- Test suite for uninterpreted sorts +----------------------------------------------------------------------------- + +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE ScopedTypeVariables #-} +module TestSuite.Uninterpreted.Sort where + +import Data.SBV +import SBVTest +import Data.Generics + +-- Test suite +testSuite :: SBVTestSuite +testSuite = mkTestSuite $ \_ -> test [ + "unint-sort" ~: assert . (==4) . length . (extractModels :: AllSatResult -> [L]) =<< allSat p0 + ] + +data L = Nil | Cons Int L deriving (Eq, Ord, Data, Typeable) +instance SymWord L +instance HasKind L +instance SatModel L where + parseCWs = undefined -- make GHC shut up about the missing method, we won't actually call it + +type SList = SBV L + +len :: SList -> SInteger +len = uninterpret "len" + +p0 :: Symbolic SBool +p0 = do + [l, l0, l1] <- symbolics ["l", "l0", "l1"] + constrain $ len l0 .== 0 + constrain $ len l1 .== 1 + x :: SInteger <- symbolic "x" + constrain $ x .== 0 ||| x.== 1 + return $ l .== l0 ||| l .== l1 diff --git a/sbv.cabal b/sbv.cabal --- a/sbv.cabal +++ b/sbv.cabal @@ -1,98 +1,15 @@ Name: sbv -Version: 2.10 +Version: 3.0 Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. Description: Express properties about Haskell programs and automatically prove them using SMT - (Satisfiability Modulo Theories) solvers. Automatically generate C programs from - Haskell functions. The SBV library adds support for symbolic bit vectors and other - symbolic types, allowing formal models of Haskell programs to be created. - . - > $ ghci -XScopedTypeVariables - > Prelude> :m Data.SBV - > Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x - > Q.E.D. - > Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x - > Falsifiable. Counter-example: - > x = 128 :: SWord8 - . - You can pick the SMT solver you want to use by importing the appropriate module. The SBV library currently - works with the the following SMT solvers: - . - [@import "Data.SBV"@] - Picks the default solver, which is currently set to be Z3. (Might change in the future!) - . - [@import "Data.SBV.Bridge.Z3"@] - Picks Z3 from Microsoft (). - . - [@import "Data.SBV.Bridge.Yices"@] - Picks Yices from SRI () - . - [@import "Data.SBV.Bridge.CVC4"@] - Picks CVC4 from New York University and the University of Iowa () - . - [@import "Data.SBV.Bridge.Boolector"@] - Picks Boolector from Johannes Kepler University at (). - . - SBV introduces the following types and concepts: - . - * 'SBool': Symbolic Booleans (bits) - . - * 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned) - . - * 'SInt8', 'SInt16', 'SInt32', 'SInt64': Symbolic Ints (signed) - . - * 'SInteger': Symbolic unbounded integers (signed) - . - * 'SReal': Symbolic algebraic reals (signed) - . - * 'SArray', 'SFunArray': Flat arrays of symbolic values - . - * 'STree': Full binary trees of symbolic values (for fast symbolic access) - . - * Symbolic polynomials over GF(2^n), and polynomial arithmetic - . - * Uninterpreted constants and functions over symbolic values, with user defined axioms. - . - * Uninterpreted sorts, and proofs over such sorts, potentially with axioms. - . - Functions built out of these types can be: - . - * proven correct via an external SMT solver (the 'prove' function) - . - * checked for satisfiability (the 'sat', and 'allSat' functions) - . - * used in synthesis (the 'sat' function with existential variables) - . - * optimized with respect to cost functions (the 'optimize', 'maximize', - and 'minimize' functions) - . - * quick-checked - . - * used in concrete test case generation (the 'genTest' function), rendered as - values in various languages, including Haskell and C. - . - Predicates can have both existential and universal variables. Use of - alternating quantifiers provides considerable expressive power. - Furthermore, existential variables allow synthesis via model generation. - . - The SBV library can also compile Haskell functions that manipulate symbolic - values directly to C, rendering them as straight-line C programs. - . - In addition to the library, the installation will create the - executable @SBVUnitTests@. You should run it once the installation is complete, - to make sure the unit tests are run and all is well. - . - SBV is hosted at GitHub: . Comments, - bug reports, and patches are always welcome. + (Satisfiability Modulo Theories) solvers. . - The following people reported bugs, provided comments/feedback, or contributed to the - development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John - Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and - Nis Wegmann. + For details, please see: . - Release notes can be seen at: . + Release notes: -Copyright: Levent Erkok, 2010-2013 +Copyright: Levent Erkok, 2010-2014 License: BSD3 License-file: LICENSE Stability: Experimental @@ -113,9 +30,7 @@ default-language: Haskell2010 ghc-options : -Wall other-extensions: BangPatterns - -- Currently commented out since Cabal doesn't yet recognize DefaultSignatures extension yet. Uncomment when it does. - -- The current list can be seen at: https://github.com/haskell/cabal/blob/master/Cabal/Language/Haskell/Extension.hs - -- DefaultSignatures + DefaultSignatures DeriveDataTypeable FlexibleContexts FlexibleInstances @@ -137,6 +52,7 @@ Exposed-modules : Data.SBV , Data.SBV.Bridge.Boolector , Data.SBV.Bridge.CVC4 + , Data.SBV.Bridge.MathSAT , Data.SBV.Bridge.Yices , Data.SBV.Bridge.Z3 , Data.SBV.Internals @@ -154,6 +70,8 @@ , Data.SBV.Examples.Crypto.RC4 , Data.SBV.Examples.Existentials.CRCPolynomial , Data.SBV.Examples.Existentials.Diophantine + , Data.SBV.Examples.Misc.Floating + , Data.SBV.Examples.Misc.ModelExtract , Data.SBV.Examples.Polynomials.Polynomials , Data.SBV.Examples.Puzzles.Coins , Data.SBV.Examples.Puzzles.Counts @@ -168,6 +86,7 @@ , Data.SBV.Examples.Uninterpreted.Function , Data.SBV.Examples.Uninterpreted.Shannon , Data.SBV.Examples.Uninterpreted.Sort + , Data.SBV.Examples.Uninterpreted.UISortAllSat Other-modules : Data.SBV.BitVectors.AlgReals , Data.SBV.BitVectors.Data , Data.SBV.BitVectors.Model @@ -187,6 +106,7 @@ , Data.SBV.Provers.CVC4 , Data.SBV.Provers.Yices , Data.SBV.Provers.Z3 + , Data.SBV.Provers.MathSAT , Data.SBV.Tools.ExpectedValue , Data.SBV.Tools.GenTest , Data.SBV.Tools.Optimize @@ -264,6 +184,7 @@ , TestSuite.Uninterpreted.AUF , TestSuite.Uninterpreted.Function , TestSuite.Uninterpreted.Uninterpreted + , TestSuite.Uninterpreted.Sort , TestSuite.Uninterpreted.Axioms Test-Suite SBVBasicTests