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