-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
--
-- Express properties about Haskell programs and automatically prove them
-- using SMT (Satisfiability Modulo Theories) solvers.
--
-- For details, please see: http://leventerkok.github.com/sbv/
@package sbv
@version 7.4
-- | Test generation from symbolic programs
module Data.SBV.Tools.GenTest
-- | Generate a set of concrete test values from a symbolic program. The
-- output can be rendered as test vectors in different languages as
-- necessary. Use the function output call to indicate what fields
-- should be in the test result. (Also see constrain for filtering
-- acceptable test values.)
genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors
-- | Type of test vectors (abstract)
data TestVectors
-- | Retrieve the test vectors for further processing. This function is
-- useful in cases where renderTest is not sufficient and custom
-- output (or further preprocessing) is needed.
getTestValues :: TestVectors -> [([CW], [CW])]
-- | Render the test as a Haskell value with the given name n.
renderTest :: TestStyle -> TestVectors -> String
-- | Test output style
data TestStyle
-- | As a Haskell value with given name
Haskell :: String -> TestStyle
-- | As a C array of structs with given name
C :: String -> TestStyle
-- | As a Forte/Verilog value with given name. If the boolean is True then
-- vectors are blasted big-endian, otherwise little-endian The indices
-- are the split points on bit-vectors for input and output values
Forte :: String -> Bool -> ([Int], [Int]) -> TestStyle
-- | Control sublanguage for interacting with SMT solvers.
module Data.SBV.Control
-- | A query is a user-guided mechanism to directly communicate and extract
-- results from the solver.
data Query a
-- | Run a custom query
query :: Query a -> Symbolic a
-- | Similar to freshVar, except creates unnamed variable.
freshVar_ :: forall a. SymWord a => Query (SBV a)
-- | Create a fresh variable in query mode. You should prefer creating
-- input variables using sBool, sInt32, etc., which act
-- as primary inputs to the model and can be existential or universal.
-- Use freshVar only in query mode for anonymous temporary
-- variables. Such variables are always existential. Note that
-- freshVar should hardly be needed: Your input variables and
-- symbolic expressions should suffice for most major use cases.
freshVar :: forall a. SymWord a => String -> Query (SBV a)
-- | Result of a checkSat or checkSatAssuming call.
data CheckSatResult
Sat :: CheckSatResult
Unsat :: CheckSatResult
Unk :: CheckSatResult
-- | Check for satisfiability.
checkSat :: Query CheckSatResult
-- | Check for satisfiability with a custom check-sat-using command.
checkSatUsing :: String -> Query CheckSatResult
-- | Check for satisfiability, under the given conditions. Similar to
-- checkSat except it allows making further assumptions as
-- captured by the first argument of booleans. (Also see
-- checkSatAssumingWithUnsatisfiableSet for a variant that returns
-- the subset of the given assumptions that led to the Unsat
-- conclusion.)
checkSatAssuming :: [SBool] -> Query CheckSatResult
-- | Check for satisfiability, under the given conditions. Returns the
-- unsatisfiable set of assumptions. Similar to checkSat except it
-- allows making further assumptions as captured by the first argument of
-- booleans. If the result is Unsat, the user will also receive a
-- subset of the given assumptions that led to the Unsat
-- conclusion. Note that while this set will be a subset of the inputs,
-- it is not necessarily guaranteed to be minimal.
--
-- You must have arranged for the production of unsat assumptions first
-- (via setOption $ ProduceUnsatAssumptions
-- True) for this call to not error out!
--
-- Usage note: getUnsatCore is usually easier to use than
-- checkSatAssumingWithUnsatisfiableSet, as it allows the use of
-- named assertions, as obtained by namedAssert. If
-- getUnsatCore fills your needs, you should definitely prefer it
-- over checkSatAssumingWithUnsatisfiableSet.
checkSatAssumingWithUnsatisfiableSet :: [SBool] -> Query (CheckSatResult, Maybe [SBool])
-- | A class which allows for sexpr-conversion to values
class SMTValue a
sexprToVal :: SMTValue a => SExpr -> Maybe a
sexprToVal :: (SMTValue a, Read a) => SExpr -> Maybe a
-- | Get the value of a term.
getValue :: SMTValue a => SBV a -> Query a
-- | Get the value of an uninterpreted sort, as a String
getUninterpretedValue :: HasKind a => SBV a -> Query String
-- | Collect model values. It is implicitly assumed that we are in a
-- check-sat context. See getSMTResult for a variant that issues a
-- check-sat first and returns an SMTResult.
getModel :: Query SMTModel
-- | Retrieve the assignment. This is a lightweight version of
-- getValue, where the solver returns the truth value for all
-- named subterms of type Bool.
getAssignment :: Query [(String, Bool)]
-- | Issue check-sat and get an SMT Result out.
getSMTResult :: Query SMTResult
-- | Get the reason unknown. Only internally used.
getUnknownReason :: Query String
-- | Retrieve the unsat-core. Note you must have arranged for unsat cores
-- to be produced first (via setOption $
-- ProduceUnsatCores True) for this call to not error
-- out!
getUnsatCore :: Query [String]
-- | Retrieve the proof. Note you must have arranged for proofs to be
-- produced first (via setOption $ ProduceProofs
-- True) for this call to not error out!
--
-- A proof is simply a String, as returned by the solver. In the
-- future, SBV might provide a better datatype, depending on the use
-- cases. Please get in touch if you use this function and can suggest a
-- better API.
getProof :: Query String
-- | Retrieve interpolants after an Unsat result is obtained. Note
-- you must have arranged for interpolants to be produced first
-- (via setOption $ ProduceInterpolants
-- True) for this call to not error out!
--
-- To get an interpolant for a pair of formulas A and
-- B, use a namedConstraint to attach names to A
-- and B. Then call getInterpolant ["A", "B"],
-- assuming those are the names you gave to the formulas.
--
-- An interpolant for A and B is a formula I
-- such that:
--
--
-- A ==> I
-- and B ==> not I
--
--
-- That is, it's evidence that A and B cannot be true
-- together since A implies I but B implies
-- not I; establishing that A and B cannot be
-- satisfied at the same time. Furthermore, I will have only the
-- symbols that are common to A and B.
--
-- Interpolants generalize to sequences: If you pass more than two
-- formulas, then you will get a sequence of interpolants. In general,
-- for N formulas that are not satisfiable together, you will be
-- returned N-1 interpolants. If formulas are A1 .. An,
-- then interpolants will be I1 .. I(N-1), such that A1
-- ==> I1, A2 /\ I1 ==> I2, A3 /\ I2 ==>
-- I3, ..., and finally AN ===> not I(N-1).
--
-- Currently, SBV only returns simple and sequence interpolants, and does
-- not support tree-interpolants. If you need these, please get in touch.
-- Furthermore, the result will be a list of mere strings representing
-- the interpolating formulas, as opposed to a more structured type.
-- Please get in touch if you use this function and can suggest a better
-- API.
getInterpolant :: [String] -> Query [String]
-- | Retrieve assertions. Note you must have arranged for assertions to be
-- available first (via setOption $
-- ProduceAssertions True) for this call to not error
-- out!
--
-- Note that the set of assertions returned is merely a list of strings,
-- just like the case for getProof. In the future, SBV might
-- provide a better datatype, depending on the use cases. Please get in
-- touch if you use this function and can suggest a better API.
getAssertions :: Query [String]
-- | Collectable information from the solver.
data SMTInfoFlag
AllStatistics :: SMTInfoFlag
AssertionStackLevels :: SMTInfoFlag
Authors :: SMTInfoFlag
ErrorBehavior :: SMTInfoFlag
Name :: SMTInfoFlag
ReasonUnknown :: SMTInfoFlag
Version :: SMTInfoFlag
InfoKeyword :: String -> SMTInfoFlag
-- | Behavior of the solver for errors.
data SMTErrorBehavior
ErrorImmediateExit :: SMTErrorBehavior
ErrorContinuedExecution :: SMTErrorBehavior
-- | Reason for reporting unknown.
data SMTReasonUnknown
UnknownMemOut :: SMTReasonUnknown
UnknownIncomplete :: SMTReasonUnknown
UnknownOther :: String -> SMTReasonUnknown
-- | Collectable information from the solver.
data SMTInfoResponse
Resp_Unsupported :: SMTInfoResponse
Resp_AllStatistics :: [(String, String)] -> SMTInfoResponse
Resp_AssertionStackLevels :: Integer -> SMTInfoResponse
Resp_Authors :: [String] -> SMTInfoResponse
Resp_Error :: SMTErrorBehavior -> SMTInfoResponse
Resp_Name :: String -> SMTInfoResponse
Resp_ReasonUnknown :: SMTReasonUnknown -> SMTInfoResponse
Resp_Version :: String -> SMTInfoResponse
Resp_InfoKeyword :: String -> [String] -> SMTInfoResponse
-- | Ask solver for info.
getInfo :: SMTInfoFlag -> Query SMTInfoResponse
-- | Retrieve the value of an 'SMTOption.' The curious function argument is
-- on purpose here, simply pass the constructor name. Example: the call
-- getOption ProduceUnsatCores will return either
-- Nothing or Just (ProduceUnsatCores True) or Just
-- (ProduceUnsatCores False).
--
-- Result will be Nothing if the solver does not support this
-- option.
getOption :: (a -> SMTOption) -> Query (Maybe SMTOption)
-- | The current assertion stack depth, i.e., pops after start. Always
-- non-negative.
getAssertionStackDepth :: Query Int
-- | Push the context, entering a new one. Pushes multiple levels if
-- n > 1.
push :: Int -> Query ()
-- | Pop the context, exiting a new one. Pops multiple levels if n
-- > 1. It's an error to pop levels that don't exist.
pop :: Int -> Query ()
-- | Run the query in a new assertion stack. That is, we push the context,
-- run the query commands, and pop it back.
inNewAssertionStack :: Query a -> Query a
-- | Search for a result via a sequence of case-splits, guided by the user.
-- If one of the conditions lead to a satisfiable result, returns
-- Just that result. If none of them do, returns
-- Nothing. Note that we automatically generate a coverage case
-- and search for it automatically as well. In that latter case, the
-- string returned will be Coverage. The first argument controls
-- printing progress messages
caseSplit :: Bool -> [(String, SBool)] -> Query (Maybe (String, SMTResult))
-- | Reset the solver, by forgetting all the assertions. However, bindings
-- are kept as is, as opposed to reset. Use this variant to
-- clean-up the solver state while leaving the bindings intact. Pops all
-- assertion levels. Declarations and definitions resulting from the
-- setLogic command are unaffected. Note that SBV implicitly uses
-- global-declarations, so bindings will remain intact.
resetAssertions :: Query ()
-- | Make an assignment. The type Assignment is abstract, the result
-- is typically passed to mkSMTResult:
--
--
-- mkSMTResult [ a |-> 332
-- , b |-> 2.3
-- , c |-> True
-- ]
--
--
-- End users should use getModel for automatically constructing
-- models from the current solver state. However, an explicit
-- Assignment might be handy in complex scenarios where a model
-- needs to be created manually.
(|->) :: SymWord a => SBV a -> a -> Assignment
infix 1 |->
-- | Produce the query result from an assignment.
mkSMTResult :: [Assignment] -> Query SMTResult
-- | Exit the solver. This action will cause the solver to terminate.
-- Needless to say, trying to communicate with the solver after issuing
-- "exit" will simply fail.
exit :: Query ()
-- | If true, we shall ignore the exit code upon exit. Otherwise we require
-- ExitSuccess.
ignoreExitCode :: SMTConfig -> Bool
-- | Timeout a query action, typically a command call to the underlying SMT
-- solver. The duration is in microseconds (1/10^6 seconds). If
-- the duration is negative, then no timeout is imposed. When specifying
-- long timeouts, be careful not to exceed maxBound :: Int. (On
-- a 64 bit machine, this bound is practically infinite. But on a 32 bit
-- machine, it corresponds to about 36 minutes!)
--
-- Semantics: The call timeout n q causes the timeout value to
-- be applied to all interactive calls that take place as we execute the
-- query q. That is, each call that happens during the execution
-- of q gets a separate time-out value, as opposed to one
-- timeout value that limits the whole query. This is typically the
-- intended behavior. It is advisible to apply this combinator to calls
-- that involve a single call to the solver for finer control, as opposed
-- to an entire set of interactions. However, different use cases might
-- call for different scenarios.
--
-- If the solver responds within the time-out specified, then we continue
-- as usual. However, if the backend solver times-out using this
-- mechanism, there is no telling what the state of the solver will be.
-- Thus, we raise an error in this case.
timeout :: Int -> Query a -> Query a
-- | If verbose is True, print the message, useful for
-- debugging messages in custom queries. Note that redirectVerbose
-- will be respected: If a file redirection is given, the output will go
-- to the file.
queryDebug :: [String] -> Query ()
-- | Echo a string. Note that the echoing is done by the solver, not by
-- SBV.
echo :: String -> Query ()
-- | Perform an arbitrary IO action.
io :: IO a -> Query a
-- | Option values that can be set in the solver, following the SMTLib
-- specification http://smtlib.cs.uiowa.edu/language.shtml.
--
-- Note that not all solvers may support all of these!
--
-- Furthermore, SBV doesn't support the following options allowed by
-- SMTLib.
--
--
-- - :interactive-mode (Deprecated in SMTLib, use
-- ProduceAssertions instead.)
-- - :print-success (SBV critically needs this to be True in
-- query mode.)
-- - :produce-models (SBV always sets this option so it can
-- extract models.)
-- - :regular-output-channel (SBV always requires regular
-- output to come on stdout for query purposes.)
-- - :global-declarations (SBV always uses global declarations
-- since definitions are accumulative.)
--
--
-- Note that SetLogic and SetInfo are, strictly speaking,
-- not SMTLib options. However, we treat it as such here uniformly, as it
-- fits better with how options work.
data SMTOption
DiagnosticOutputChannel :: FilePath -> SMTOption
ProduceAssertions :: Bool -> SMTOption
ProduceAssignments :: Bool -> SMTOption
ProduceProofs :: Bool -> SMTOption
ProduceInterpolants :: Bool -> SMTOption
ProduceUnsatAssumptions :: Bool -> SMTOption
ProduceUnsatCores :: Bool -> SMTOption
RandomSeed :: Integer -> SMTOption
ReproducibleResourceLimit :: Integer -> SMTOption
SMTVerbosity :: Integer -> SMTOption
OptionKeyword :: String -> [String] -> SMTOption
SetLogic :: Logic -> SMTOption
SetInfo :: String -> [String] -> SMTOption
-- | SMT-Lib logics. If left unspecified SBV will pick the logic based on
-- what it determines is needed. However, the user can override this
-- choice using the tactic SetOptions This is especially handy
-- if one is experimenting with custom logics that might be supported on
-- new solvers. See http://smtlib.cs.uiowa.edu/logics.shtml for
-- the official list.
data Logic
-- | Formulas over the theory of linear integer arithmetic and arrays
-- extended with free sort and function symbols but restricted to arrays
-- with integer indices and values.
AUFLIA :: Logic
-- | Linear formulas with free sort and function symbols over one- and
-- two-dimentional arrays of integer index and real value.
AUFLIRA :: Logic
-- | Formulas with free function and predicate symbols over a theory of
-- arrays of arrays of integer index and real value.
AUFNIRA :: Logic
-- | Linear formulas in linear real arithmetic.
LRA :: Logic
-- | Quantifier-free formulas over the theory of bitvectors and bitvector
-- arrays.
QF_ABV :: Logic
-- | Quantifier-free formulas over the theory of bitvectors and bitvector
-- arrays extended with free sort and function symbols.
QF_AUFBV :: Logic
-- | Quantifier-free linear formulas over the theory of integer arrays
-- extended with free sort and function symbols.
QF_AUFLIA :: Logic
-- | Quantifier-free formulas over the theory of arrays with
-- extensionality.
QF_AX :: Logic
-- | Quantifier-free formulas over the theory of fixed-size bitvectors.
QF_BV :: Logic
-- | Difference Logic over the integers. Boolean combinations of
-- inequations of the form x - y < b where x and y are integer
-- variables and b is an integer constant.
QF_IDL :: Logic
-- | Unquantified linear integer arithmetic. In essence, Boolean
-- combinations of inequations between linear polynomials over integer
-- variables.
QF_LIA :: Logic
-- | Unquantified linear real arithmetic. In essence, Boolean combinations
-- of inequations between linear polynomials over real variables.
QF_LRA :: Logic
-- | Quantifier-free integer arithmetic.
QF_NIA :: Logic
-- | Quantifier-free real arithmetic.
QF_NRA :: Logic
-- | Difference Logic over the reals. In essence, Boolean combinations of
-- inequations of the form x - y < b where x and y are real variables
-- and b is a rational constant.
QF_RDL :: Logic
-- | Unquantified formulas built over a signature of uninterpreted (i.e.,
-- free) sort and function symbols.
QF_UF :: Logic
-- | Unquantified formulas over bitvectors with uninterpreted sort function
-- and symbols.
QF_UFBV :: Logic
-- | Difference Logic over the integers (in essence) but with uninterpreted
-- sort and function symbols.
QF_UFIDL :: Logic
-- | Unquantified linear integer arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLIA :: Logic
-- | Unquantified linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFLRA :: Logic
-- | Unquantified non-linear real arithmetic with uninterpreted sort and
-- function symbols.
QF_UFNRA :: Logic
-- | Unquantified non-linear real integer arithmetic with uninterpreted
-- sort and function symbols.
QF_UFNIRA :: Logic
-- | Linear real arithmetic with uninterpreted sort and function symbols.
UFLRA :: Logic
-- | Non-linear integer arithmetic with uninterpreted sort and function
-- symbols.
UFNIA :: Logic
-- | Quantifier-free formulas over the theory of floating point numbers,
-- arrays, and bit-vectors.
QF_FPBV :: Logic
-- | Quantifier-free formulas over the theory of floating point numbers.
QF_FP :: Logic
-- | Quantifier-free finite domains
QF_FD :: Logic
-- | The catch-all value
Logic_ALL :: Logic
-- | In case you need a really custom string!
CustomLogic :: String -> Logic
-- | Implementation of full-binary symbolic trees, providing logarithmic
-- time access to elements. Both reads and writes are supported.
module Data.SBV.Tools.STree
-- | A symbolic tree containing values of type e, indexed by elements of
-- type i. Note that these are full-trees, and their their shapes remain
-- constant. There is no API provided that can change the shape of the
-- tree. These structures are useful when dealing with data-structures
-- that are indexed with symbolic values where access time is important.
-- STree structures provide logarithmic time reads and writes.
type STree i e = STreeInternal (SBV i) (SBV e)
-- | Reading a value. We bit-blast the index and descend down the full tree
-- according to bit-values.
readSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e
-- | Writing a value, similar to how reads are done. The important thing is
-- that the tree representation keeps updates to a minimum.
writeSTree :: (Num i, Bits i, SymWord i, SymWord e) => STree i e -> SBV i -> SBV e -> STree i e
-- | Construct the fully balanced initial tree using the given values.
mkSTree :: forall i e. HasKind i => [SBV e] -> STree i e
instance GHC.Show.Show e => GHC.Show.Show (Data.SBV.Tools.STree.STreeInternal i e)
instance Data.SBV.Core.Data.SymWord e => Data.SBV.Core.Model.Mergeable (Data.SBV.Tools.STree.STree i e)
-- | Implementation of polynomial arithmetic
module Data.SBV.Tools.Polynomial
-- | Implements polynomial addition, multiplication, division, and modulus
-- operations over GF(2^n). NB. Similar to sQuotRem, division by
-- 0 is interpreted as follows:
--
--
-- x pDivMod 0 = (0, x)
--
--
-- for all x (including 0)
--
-- Minimal complete definition: pMult, pDivMod,
-- showPolynomial
class (Num a, Bits a) => Polynomial a
-- | Given bit-positions to be set, create a polynomial For instance
--
--
-- polynomial [0, 1, 3] :: SWord8
--
--
-- will evaluate to 11, since it sets the bits 0,
-- 1, and 3. Mathematicans would write this polynomial
-- as x^3 + x + 1. And in fact, showPoly will show it
-- like that.
polynomial :: Polynomial a => [Int] -> a
-- | Add two polynomials in GF(2^n).
pAdd :: Polynomial a => a -> a -> a
-- | Multiply two polynomials in GF(2^n), and reduce it by the irreducible
-- specified by the polynomial as specified by coefficients of the third
-- argument. Note that the third argument is specifically left in this
-- form as it is usally in GF(2^(n+1)), which is not available in our
-- formalism. (That is, we would need SWord9 for SWord8 multiplication,
-- etc.) Also note that we do not support symbolic irreducibles, which is
-- a minor shortcoming. (Most GF's will come with fixed irreducibles, so
-- this should not be a problem in practice.)
--
-- Passing [] for the third argument will multiply the polynomials and
-- then ignore the higher bits that won't fit into the resulting size.
pMult :: Polynomial a => (a, a, [Int]) -> a
-- | Divide two polynomials in GF(2^n), see above note for division by 0.
pDiv :: Polynomial a => a -> a -> a
-- | Compute modulus of two polynomials in GF(2^n), see above note for
-- modulus by 0.
pMod :: Polynomial a => a -> a -> a
-- | Division and modulus packed together.
pDivMod :: Polynomial a => a -> a -> (a, a)
-- | Display a polynomial like a mathematician would (over the monomial
-- x), with a type.
showPoly :: Polynomial a => a -> String
-- | Display a polynomial like a mathematician would (over the monomial
-- x), the first argument controls if the final type is shown as
-- well.
showPolynomial :: Polynomial a => Bool -> a -> String
-- | Compute CRC's over polynomials, i.e., symbolic words. The first
-- Int argument plays the same role as the one in the crcBV
-- function.
crc :: (FromBits (SBV a), FromBits (SBV b), Num a, Num b, Bits a, Bits b, SymWord a, SymWord b) => Int -> SBV a -> SBV b -> SBV b
-- | Compute CRCs over bit-vectors. The call crcBV n m p computes
-- the CRC of the message m with respect to polynomial
-- p. The inputs are assumed to be blasted big-endian. The
-- number n specifies how many bits of CRC is needed. Note that
-- n is actually the degree of the polynomial p, and
-- thus it seems redundant to pass it in. However, in a typical proof
-- context, the polynomial can be symbolic, so we cannot compute the
-- degree easily. While this can be worked-around by generating code that
-- accounts for all possible degrees, the resulting code would be
-- unnecessarily big and complicated, and much harder to reason with.
-- (Also note that a CRC is just the remainder from the polynomial
-- division, but this routine is much faster in practice.)
--
-- NB. The nth bit of the polynomial p must be
-- set for the CRC to be computed correctly. Note that the polynomial
-- argument p will not even have this bit present most of the
-- time, as it will typically contain bits 0 through
-- n-1 as usual in the CRC literature. The higher order
-- nth bit is simply assumed to be set, as it does not make
-- sense to use a polynomial of a lesser degree. This is usually not a
-- problem since CRC polynomials are designed and expressed this way.
--
-- NB. The literature on CRC's has many variants on how CRC's are
-- computed. We follow the following simple procedure:
--
--
-- - Extend the message m by adding n 0 bits on the
-- right
-- - Divide the polynomial thus obtained by the p
-- - The remainder is the CRC value.
--
--
-- There are many variants on final XOR's, reversed polynomials etc., so
-- it is essential to double check you use the correct algorithm.
crcBV :: Int -> [SBool] -> [SBool] -> [SBool]
-- | Run down a boolean condition over two lists. Note that this is
-- different than zipWith as shorter list is assumed to be filled with
-- false at the end (i.e., zero-bits); which nicely pads it when
-- considered as an unsigned number in little-endian form.
ites :: SBool -> [SBool] -> [SBool] -> [SBool]
-- | Compute modulus/remainder of polynomials on bit-vectors.
mdp :: [SBool] -> [SBool] -> ([SBool], [SBool])
-- | Add two polynomials
addPoly :: [SBool] -> [SBool] -> [SBool]
instance Data.SBV.Tools.Polynomial.Polynomial GHC.Word.Word8
instance Data.SBV.Tools.Polynomial.Polynomial GHC.Word.Word16
instance Data.SBV.Tools.Polynomial.Polynomial GHC.Word.Word32
instance Data.SBV.Tools.Polynomial.Polynomial GHC.Word.Word64
instance Data.SBV.Tools.Polynomial.Polynomial Data.SBV.Core.Data.SWord8
instance Data.SBV.Tools.Polynomial.Polynomial Data.SBV.Core.Data.SWord16
instance Data.SBV.Tools.Polynomial.Polynomial Data.SBV.Core.Data.SWord32
instance Data.SBV.Tools.Polynomial.Polynomial Data.SBV.Core.Data.SWord64
-- | Code-generation from SBV programs.
module Data.SBV.Tools.CodeGen
-- | The code-generation monad. Allows for precise layout of input values
-- reference parameters (for returning composite values in languages such
-- as C), and return values.
data SBVCodeGen a
-- | Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large
-- value etc. on/off. Default: False.
cgPerformRTCs :: Bool -> SBVCodeGen ()
-- | Sets driver program run time values, useful for generating programs
-- with fixed drivers for testing. Default: None, i.e., use random
-- values.
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
-- | Should we generate a driver program? Default: True. When a
-- library is generated, it will have a driver if any of the contituent
-- functions has a driver. (See compileToCLib.)
cgGenerateDriver :: Bool -> SBVCodeGen ()
-- | Should we generate a Makefile? Default: True.
cgGenerateMakefile :: Bool -> SBVCodeGen ()
-- | Creates an atomic input in the generated code.
cgInput :: SymWord a => String -> SBVCodeGen (SBV a)
-- | Creates an array input in the generated code.
cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a]
-- | Creates an atomic output in the generated code.
cgOutput :: String -> SBV a -> SBVCodeGen ()
-- | Creates an array output in the generated code.
cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen ()
-- | Creates a returned (unnamed) value in the generated code.
cgReturn :: SBV a -> SBVCodeGen ()
-- | Creates a returned (unnamed) array value in the generated code.
cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen ()
-- | Adds the given lines to the header file generated, useful for
-- generating programs with uninterpreted functions.
cgAddPrototype :: [String] -> SBVCodeGen ()
-- | Adds the given lines to the program file generated, useful for
-- generating programs with uninterpreted functions.
cgAddDecl :: [String] -> SBVCodeGen ()
-- | Adds the given words to the compiler options in the generated
-- Makefile, useful for linking extra stuff in.
cgAddLDFlags :: [String] -> SBVCodeGen ()
-- | Ignore assertions (those generated by sAssert calls) in the
-- generated C code
cgIgnoreSAssert :: Bool -> SBVCodeGen ()
-- | Sets number of bits to be used for representing the SInteger
-- type in the generated C code. The argument must be one of 8,
-- 16, 32, or 64. Note that this is
-- essentially unsafe as the semantics of unbounded Haskell integers
-- becomes reduced to the corresponding bit size, as typical in most C
-- implementations.
cgIntegerSize :: Int -> SBVCodeGen ()
-- | Sets the C type to be used for representing the SReal type in
-- the generated C code. The setting can be one of C's "float",
-- "double", or "long double", types, depending on the
-- precision needed. Note that this is essentially unsafe as the
-- semantics of infinite precision SReal values becomes reduced to the
-- corresponding floating point type in C, and hence it is subject to
-- rounding errors.
cgSRealType :: CgSRealType -> SBVCodeGen ()
-- | Possible mappings for the SReal type when translated to C. Used
-- in conjunction with the function cgSRealType. Note that the
-- particular characteristics of the mapped types depend on the platform
-- and the compiler used for compiling the generated C program. See
-- http://en.wikipedia.org/wiki/C_data_types for details.
data CgSRealType
-- |
-- float
--
CgFloat :: CgSRealType
-- |
-- double
--
CgDouble :: CgSRealType
-- |
-- long double
--
CgLongDouble :: CgSRealType
-- | Given a symbolic computation, render it as an equivalent collection of
-- files that make up a C program:
--
--
-- - The first argument is the directory name under which the files
-- will be saved. To save files in the current directory pass
-- Just ".". Use Nothing for printing to
-- stdout.
-- - The second argument is the name of the C function to
-- generate.
-- - The final argument is the function to be compiled.
--
--
-- Compilation will also generate a Makefile, a header file, and
-- a driver (test) program, etc.
compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()
-- | Create code to generate a library archive (.a) from given symbolic
-- functions. Useful when generating code from multiple functions that
-- work together as a library.
--
--
-- - The first argument is the directory name under which the files
-- will be saved. To save files in the current directory pass
-- Just ".". Use Nothing for printing to
-- stdout.
-- - The second argument is the name of the archive to generate.
-- - The third argument is the list of functions to include, in the
-- form of function-name/code pairs, similar to the second and third
-- arguments of compileToC, except in a list.
--
compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()
-- | Low level functions to access the SBV infrastructure, for developers
-- who want to build further tools on top of SBV. End-users of the
-- library should not need to use this module.
module Data.SBV.Internals
-- | Result of running a symbolic computation
data Result
Result :: Set Kind -> [(String, CW)] -> [(String, [String])] -> ([(Quantifier, NamedSymVar)], [NamedSymVar]) -> [(SW, CW)] -> [((Int, Kind, Kind), [SW])] -> [(Int, ArrayInfo)] -> [(String, SBVType)] -> [(String, [String])] -> SBVPgm -> [(Maybe String, SW)] -> [(String, Maybe CallStack, SW)] -> [SW] -> Result
-- | kinds used in the program
[reskinds] :: Result -> Set Kind
-- | quick-check counter-example information (if any)
[resTraces] :: Result -> [(String, CW)]
-- | uninterpeted code segments
[resUISegs] :: Result -> [(String, [String])]
-- | inputs (possibly existential) + tracker vars
[resInputs] :: Result -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
-- | constants
[resConsts] :: Result -> [(SW, CW)]
-- | tables (automatically constructed) (tableno, index-type, result-type)
-- elts
[resTables] :: Result -> [((Int, Kind, Kind), [SW])]
-- | arrays (user specified)
[resArrays] :: Result -> [(Int, ArrayInfo)]
-- | uninterpreted constants
[resUIConsts] :: Result -> [(String, SBVType)]
-- | axioms
[resAxioms] :: Result -> [(String, [String])]
-- | assignments
[resAsgns] :: Result -> SBVPgm
-- | additional constraints (boolean)
[resConstraints] :: Result -> [(Maybe String, SW)]
-- | assertions
[resAssertions] :: Result -> [(String, Maybe CallStack, SW)]
-- | outputs
[resOutputs] :: Result -> [SW]
-- | Different means of running a symbolic piece of code
data SBVRunMode
-- | In regular mode, with a stage. Bool is True if this is SAT.
SMTMode :: IStage -> Bool -> SMTConfig -> SBVRunMode
-- | Code generation mode.
CodeGen :: SBVRunMode
-- | Concrete simulation mode.
Concrete :: SBVRunMode
-- | Stage of an interactive run
data IStage
ISetup :: IStage
IRun :: IStage
-- | Translation tricks needed for specific capabilities afforded by each
-- solver
data SolverCapabilities
SolverCapabilities :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> SolverCapabilities
-- | Support for SMT-Lib2 style quantifiers?
[supportsQuantifiers] :: SolverCapabilities -> Bool
-- | Support for SMT-Lib2 style uninterpreted-sorts
[supportsUninterpretedSorts] :: SolverCapabilities -> Bool
-- | Support for unbounded integers?
[supportsUnboundedInts] :: SolverCapabilities -> Bool
-- | Support for reals?
[supportsReals] :: SolverCapabilities -> Bool
-- | Supports printing of approximations of reals?
[supportsApproxReals] :: SolverCapabilities -> Bool
-- | Support for floating point numbers?
[supportsIEEE754] :: SolverCapabilities -> Bool
-- | Support for optimization routines?
[supportsOptimization] :: SolverCapabilities -> Bool
-- | Support for pseudo-boolean operations?
[supportsPseudoBooleans] :: SolverCapabilities -> Bool
-- | Support for interactive queries per SMT-Lib?
[supportsCustomQueries] :: SolverCapabilities -> Bool
-- | Support for global decls, needed for push-pop.
[supportsGlobalDecls] :: SolverCapabilities -> Bool
-- | A symbolic boolean/bit
type SBool = SBV Bool
-- | 8-bit unsigned symbolic value
type SWord8 = SBV Word8
-- | 16-bit unsigned symbolic value
type SWord16 = SBV Word16
-- | 32-bit unsigned symbolic value
type SWord32 = SBV Word32
-- | 64-bit unsigned symbolic value
type SWord64 = SBV Word64
-- | 8-bit signed symbolic value, 2's complement representation
type SInt8 = SBV Int8
-- | 16-bit signed symbolic value, 2's complement representation
type SInt16 = SBV Int16
-- | 32-bit signed symbolic value, 2's complement representation
type SInt32 = SBV Int32
-- | 64-bit signed symbolic value, 2's complement representation
type SInt64 = SBV Int64
-- | Infinite precision signed symbolic value
type SInteger = SBV Integer
-- | Infinite precision symbolic algebraic real value
type SReal = SBV AlgReal
-- | IEEE-754 single-precision floating point numbers
type SFloat = SBV Float
-- | IEEE-754 double-precision floating point numbers
type SDouble = SBV Double
-- | Not-A-Number for Double and Float. Surprisingly, Haskell
-- Prelude doesn't have this value defined, so we provide it here.
nan :: Floating a => a
-- | Infinity for Double and Float. Surprisingly, Haskell
-- Prelude doesn't have this value defined, so we provide it here.
infinity :: Floating a => a
-- | Symbolic variant of Not-A-Number. This value will inhabit both
-- SDouble and SFloat.
sNaN :: (Floating a, SymWord a) => SBV a
-- | Symbolic variant of infinity. This value will inhabit both
-- SDouble and SFloat.
sInfinity :: (Floating a, SymWord a) => SBV a
-- | Rounding mode to be used for the IEEE floating-point operations. Note
-- that Haskell's default is RoundNearestTiesToEven. If you use a
-- different rounding mode, then the counter-examples you get may not
-- match what you observe in Haskell.
data RoundingMode
-- | Round to nearest representable floating point value. If precisely at
-- half-way, pick the even number. (In this context, even means
-- the lowest-order bit is zero.)
RoundNearestTiesToEven :: RoundingMode
-- | Round to nearest representable floating point value. If precisely at
-- half-way, pick the number further away from 0. (That is, for positive
-- values, pick the greater; for negative values, pick the smaller.)
RoundNearestTiesToAway :: RoundingMode
-- | Round towards positive infinity. (Also known as rounding-up or
-- ceiling.)
RoundTowardPositive :: RoundingMode
-- | Round towards negative infinity. (Also known as rounding-down or
-- floor.)
RoundTowardNegative :: RoundingMode
-- | Round towards zero. (Also known as truncation.)
RoundTowardZero :: RoundingMode
-- | The symbolic variant of RoundingMode
type SRoundingMode = SBV RoundingMode
-- | Symbolic variant of RoundNearestTiesToEven
sRoundNearestTiesToEven :: SRoundingMode
-- | Symbolic variant of RoundNearestTiesToAway
sRoundNearestTiesToAway :: SRoundingMode
-- | Symbolic variant of RoundNearestPositive
sRoundTowardPositive :: SRoundingMode
-- | Symbolic variant of RoundTowardNegative
sRoundTowardNegative :: SRoundingMode
-- | Symbolic variant of RoundTowardZero
sRoundTowardZero :: SRoundingMode
-- | Alias for sRoundNearestTiesToEven
sRNE :: SRoundingMode
-- | Alias for sRoundNearestTiesToAway
sRNA :: SRoundingMode
-- | Alias for sRoundTowardPositive
sRTP :: SRoundingMode
-- | Alias for sRoundTowardNegative
sRTN :: SRoundingMode
-- | Alias for sRoundTowardZero
sRTZ :: SRoundingMode
-- | A SymWord is a potential symbolic bitvector that can be created
-- instances of to be fed to a symbolic program. Note that these methods
-- are typically not needed in casual uses with prove,
-- sat, allSat etc, as default instances automatically
-- provide the necessary bits.
class (HasKind a, Ord a) => SymWord a
-- | Create a user named input (universal)
forall :: SymWord a => String -> Symbolic (SBV a)
-- | Create an automatically named input
forall_ :: SymWord a => Symbolic (SBV a)
-- | Get a bunch of new words
mkForallVars :: SymWord a => Int -> Symbolic [SBV a]
-- | Create an existential variable
exists :: SymWord a => String -> Symbolic (SBV a)
-- | Create an automatically named existential variable
exists_ :: SymWord a => Symbolic (SBV a)
-- | Create a bunch of existentials
mkExistVars :: SymWord a => Int -> Symbolic [SBV a]
-- | Create a free variable, universal in a proof, existential in sat
free :: SymWord a => String -> Symbolic (SBV a)
-- | Create an unnamed free variable, universal in proof, existential in
-- sat
free_ :: SymWord a => Symbolic (SBV a)
-- | Create a bunch of free vars
mkFreeVars :: SymWord a => Int -> Symbolic [SBV a]
-- | Similar to free; Just a more convenient name
symbolic :: SymWord a => String -> Symbolic (SBV a)
-- | Similar to mkFreeVars; but automatically gives names based on the
-- strings
symbolics :: SymWord a => [String] -> Symbolic [SBV a]
-- | Turn a literal constant to symbolic
literal :: SymWord a => a -> SBV a
-- | Extract a literal, if the value is concrete
unliteral :: SymWord a => SBV a -> Maybe a
-- | Extract a literal, from a CW representation
fromCW :: SymWord a => CW -> a
-- | Is the symbolic word concrete?
isConcrete :: SymWord a => SBV a -> Bool
-- | Is the symbolic word really symbolic?
isSymbolic :: SymWord a => SBV a -> Bool
-- | Does it concretely satisfy the given predicate?
isConcretely :: SymWord a => SBV a -> (a -> Bool) -> Bool
-- | One stop allocator
mkSymWord :: SymWord a => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
-- | Turn a literal constant to symbolic
literal :: (SymWord a, Show a) => a -> SBV a
-- | Extract a literal, from a CW representation
fromCW :: (SymWord a, Read a) => CW -> a
-- | One stop allocator
mkSymWord :: (SymWord a, Read a, Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
-- | CW represents a concrete word of a fixed size: Endianness is
-- mostly irrelevant (see the FromBits class). For signed words,
-- the most significant digit is considered to be the sign.
data CW
CW :: !Kind -> !CWVal -> CW
[_cwKind] :: CW -> !Kind
[cwVal] :: CW -> !CWVal
-- | A constant value
data CWVal
-- | algebraic real
CWAlgReal :: !AlgReal -> CWVal
-- | bit-vector/unbounded integer
CWInteger :: !Integer -> CWVal
-- | float
CWFloat :: !Float -> CWVal
-- | double
CWDouble :: !Double -> CWVal
-- | value of an uninterpreted/user kind. The Maybe Int shows index
-- position for enumerations
CWUserSort :: !(Maybe Int, String) -> CWVal
-- | Algebraic reals. Note that the representation is left abstract. We
-- represent rational results explicitly, while the roots-of-polynomials
-- are represented implicitly by their defining equation
data AlgReal
AlgRational :: Bool -> Rational -> AlgReal
AlgPolyRoot :: (Integer, Polynomial) -> (Maybe String) -> AlgReal
-- | A simple expression type over extendent values, covering infinity,
-- epsilon and intervals.
data ExtCW
Infinite :: Kind -> ExtCW
Epsilon :: Kind -> ExtCW
Interval :: ExtCW -> ExtCW -> ExtCW
BoundedCW :: CW -> ExtCW
AddExtCW :: ExtCW -> ExtCW -> ExtCW
MulExtCW :: ExtCW -> ExtCW -> ExtCW
-- | A generalized CW allows for expressions involving infinite and epsilon
-- values/intervals Used in optimization problems.
data GeneralizedCW
ExtendedCW :: ExtCW -> GeneralizedCW
RegularCW :: CW -> GeneralizedCW
-- | Is this a regular CW?
isRegularCW :: GeneralizedCW -> Bool
-- | Are two CW's of the same type?
cwSameType :: CW -> CW -> Bool
-- | Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded)
cwToBool :: CW -> Bool
-- | Create a constant word from an integral.
mkConstCW :: Integral a => Kind -> a -> CW
-- | Lift a binary function through a CW
liftCW2 :: (AlgReal -> AlgReal -> b) -> (Integer -> Integer -> b) -> (Float -> Float -> b) -> (Double -> Double -> b) -> ((Maybe Int, String) -> (Maybe Int, String) -> b) -> CW -> CW -> b
-- | Map a unary function through a CW.
mapCW :: (AlgReal -> AlgReal) -> (Integer -> Integer) -> (Float -> Float) -> (Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW
-- | Map a binary function through a CW.
mapCW2 :: (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> (Float -> Float -> Float) -> (Double -> Double -> Double) -> ((Maybe Int, String) -> (Maybe Int, String) -> (Maybe Int, String)) -> CW -> CW -> CW
-- | A symbolic word, tracking it's signedness and size.
data SW
SW :: !Kind -> !NodeId -> SW
-- | Constant True as an SW. Note that this value always occupies slot -1.
trueSW :: SW
-- | Constant False as an SW. Note that this value always occupies slot -2.
falseSW :: SW
-- | Constant True as a CW. We represent it using the integer value 1.
trueCW :: CW
-- | Constant False as a CW. We represent it using the integer value 0.
falseCW :: CW
-- | Normalize a CW. Essentially performs modular arithmetic to make sure
-- the value can fit in the given bit-size. Note that this is rather
-- tricky for negative values, due to asymmetry. (i.e., an 8-bit negative
-- number represents values in the range -128 to 127; thus we have to be
-- careful on the negative side.)
normCW :: CW -> CW
-- | The Symbolic value. Either a constant (Left) or a
-- symbolic value (Right Cached). Note that caching is essential
-- for making sure sharing is preserved.
data SVal
SVal :: !Kind -> !(Either CW (Cached SW)) -> SVal
-- | The Symbolic value. The parameter a is phantom, but is
-- extremely important in keeping the user interface strongly typed.
newtype SBV a
SBV :: SVal -> SBV a
[unSBV] :: SBV a -> SVal
-- | A symbolic node id
newtype NodeId
NodeId :: Int -> NodeId
-- | Create a symbolic variable.
mkSymSBV :: forall a. Maybe Quantifier -> Kind -> Maybe String -> Symbolic (SBV a)
-- | The context of a symbolic array as created
data ArrayContext
-- | A new array, the contents are uninitialized
ArrayFree :: ArrayContext
-- | An array created by mutating another array at a given cell
ArrayMutate :: Int -> SW -> SW -> ArrayContext
-- | An array created by symbolically merging two other arrays
ArrayMerge :: SW -> Int -> Int -> ArrayContext
-- | Representation for symbolic arrays
type ArrayInfo = (String, (Kind, Kind), ArrayContext)
-- | Flat arrays of symbolic values An array a b is an array
-- indexed by the type SBV a, with elements of type
-- SBV b.
--
-- While it's certainly possible for user to create instances of
-- SymArray, the SArray and SFunArray instances
-- already provided should cover most use cases in practice. (There are
-- some differences between these models, however, see the corresponding
-- declaration.)
--
-- Minimal complete definition: All methods are required, no defaults.
class SymArray array
-- | Create a new anonymous array
newArray_ :: (SymArray array, HasKind a, HasKind b) => Symbolic (array a b)
-- | Create a named new array
newArray :: (SymArray array, HasKind a, HasKind b) => String -> Symbolic (array a b)
-- | Read the array element at a
readArray :: SymArray array => array a b -> SBV a -> SBV b
-- | Update the element at a to be b
writeArray :: (SymArray array, SymWord b) => array a b -> SBV a -> SBV b -> array a b
-- | Merge two given arrays on the symbolic condition Intuitively:
-- mergeArrays cond a b = if cond then a else b. Merging pushes
-- the if-then-else choice down on to elements
mergeArrays :: (SymArray array, SymWord b) => SBV Bool -> array a b -> array a b -> array a b
-- | Arrays implemented internally as functions
--
--
-- - Internally handled by the library and not mapped to SMT-Lib
-- - Reading an uninitialized value is considered an error (will throw
-- exception)
-- - Cannot check for equality (internally represented as
-- functions)
-- - Can quick-check
-- - Typically faster as it gets compiled away during translation
--
newtype SFunArray a b
SFunArray :: (SBV a -> SBV b) -> SFunArray a b
-- | Lift a function to an array. Useful for creating arrays in a pure
-- context. (Otherwise use newArray.)
mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
-- | Arrays implemented in terms of SMT-arrays:
-- http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
--
--
-- - Maps directly to SMT-lib arrays
-- - Reading from an unintialized value is OK and yields an unspecified
-- result
-- - Can check for equality of these arrays
-- - Cannot quick-check theorems using SArray values
-- - Typically slower as it heavily relies on SMT-solving for the array
-- theory
--
newtype SArray a b
SArray :: SArr -> SArray a b
[unSArray] :: SArray a b -> SArr
-- | Convert a symbolic value to a symbolic-word
sbvToSW :: State -> SBV a -> IO SW
-- | Convert a symbolic value to an SW, inside the Symbolic monad
sbvToSymSW :: SBV a -> Symbolic SW
-- | Forcing an argument; this is a necessary evil to make sure all the
-- arguments to an uninterpreted function are evaluated before called;
-- the semantics of uinterpreted functions is necessarily strict;
-- deviating from Haskell's
forceSWArg :: SW -> IO ()
-- | A symbolic expression
data SBVExpr
SBVApp :: !Op -> ![SW] -> SBVExpr
-- | Create a new expression; hash-cons as necessary
newExpr :: State -> Kind -> SBVExpr -> IO SW
-- | Cache a state-based computation
cache :: (State -> IO a) -> Cached a
-- | We implement a peculiar caching mechanism, applicable to the use case
-- in implementation of SBV's. Whenever we do a state based computation,
-- we do not want to keep on evaluating it in the then-current state.
-- That will produce essentially a semantically equivalent value. Thus,
-- we want to run it only once, and reuse that result, capturing the
-- sharing at the Haskell level. This is similar to the "type-safe
-- observable sharing" work, but also takes into the account of how
-- symbolic simulation executes.
--
-- See Andy Gill's type-safe obervable sharing trick for the inspiration
-- behind this technique:
-- http://ittc.ku.edu/~andygill/paper.php?label=DSLExtract09
--
-- Note that this is *not* a general memo utility!
data Cached a
-- | Uncache a previously cached computation
uncache :: Cached SW -> State -> IO SW
-- | Uncache, retrieving array indexes
uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
-- | A class for capturing values that have a sign and a size (finite or
-- infinite) minimal complete definition: kindOf. This class can be
-- automatically derived for data-types that have a Data
-- instance; this is useful for creating uninterpreted sorts.
class HasKind a
kindOf :: HasKind a => a -> Kind
hasSign :: HasKind a => a -> Bool
intSizeOf :: HasKind a => a -> Int
isBoolean :: HasKind a => a -> Bool
isBounded :: HasKind a => a -> Bool
isReal :: HasKind a => a -> Bool
isFloat :: HasKind a => a -> Bool
isDouble :: HasKind a => a -> Bool
isInteger :: HasKind a => a -> Bool
isUninterpreted :: HasKind a => a -> Bool
showType :: HasKind a => a -> String
kindOf :: (HasKind a, Read a, Data a) => a -> Kind
-- | Symbolic operations
data Op
Plus :: Op
Times :: Op
Minus :: Op
UNeg :: Op
Abs :: Op
Quot :: Op
Rem :: Op
Equal :: Op
NotEqual :: Op
LessThan :: Op
GreaterThan :: Op
LessEq :: Op
GreaterEq :: Op
Ite :: Op
And :: Op
Or :: Op
XOr :: Op
Not :: Op
Shl :: Op
Shr :: Op
Rol :: Int -> Op
Ror :: Int -> Op
Extract :: Int -> Int -> Op
Join :: Op
LkUp :: (Int, Kind, Kind, Int) -> !SW -> !SW -> Op
ArrEq :: Int -> Int -> Op
ArrRead :: Int -> Op
KindCast :: Kind -> Kind -> Op
Uninterpreted :: String -> Op
Label :: String -> Op
IEEEFP :: FPOp -> Op
PseudoBoolean :: PBOp -> Op
-- | Pseudo-boolean operations
data PBOp
-- | At most k
PB_AtMost :: Int -> PBOp
-- | At least k
PB_AtLeast :: Int -> PBOp
-- | Exactly k
PB_Exactly :: Int -> PBOp
-- | At most k, with coefficients given. Generalizes PB_AtMost
PB_Le :: [Int] -> Int -> PBOp
-- | At least k, with coefficients given. Generalizes PB_AtLeast
PB_Ge :: [Int] -> Int -> PBOp
-- | Exactly k, with coefficients given. Generalized PB_Exactly
PB_Eq :: [Int] -> Int -> PBOp
-- | Floating point operations
data FPOp
FP_Cast :: Kind -> Kind -> SW -> FPOp
FP_Reinterpret :: Kind -> Kind -> FPOp
FP_Abs :: FPOp
FP_Neg :: FPOp
FP_Add :: FPOp
FP_Sub :: FPOp
FP_Mul :: FPOp
FP_Div :: FPOp
FP_FMA :: FPOp
FP_Sqrt :: FPOp
FP_Rem :: FPOp
FP_RoundToIntegral :: FPOp
FP_Min :: FPOp
FP_Max :: FPOp
FP_ObjEqual :: FPOp
FP_IsNormal :: FPOp
FP_IsSubnormal :: FPOp
FP_IsZero :: FPOp
FP_IsInfinite :: FPOp
FP_IsNaN :: FPOp
FP_IsNegative :: FPOp
FP_IsPositive :: FPOp
-- | NamedSymVar pairs symbolic words and user given/automatically
-- generated names
type NamedSymVar = (SW, String)
-- | Create a new table; hash-cons as necessary
getTableIndex :: State -> Kind -> Kind -> [SW] -> IO Int
-- | A program is a sequence of assignments
newtype SBVPgm
SBVPgm :: Seq (SW, SBVExpr) -> SBVPgm
[pgmAssignments] :: SBVPgm -> Seq (SW, SBVExpr)
-- | A Symbolic computation. Represented by a reader monad carrying the
-- state of the computation, layered on top of IO for creating unique
-- references to hold onto intermediate results.
data Symbolic a
-- | Run a symbolic computation, and return a extra value paired up with
-- the Result
runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result)
-- | Return and clean and incState
--
-- The state of the symbolic interpreter
data State
-- | Get the current path condition
getPathCondition :: State -> SBool
-- | Extend the path condition with the given test value.
extendPathCondition :: State -> (SBool -> SBool) -> State
-- | Are we running in proof mode?
inSMTMode :: State -> IO Bool
-- | Different means of running a symbolic piece of code
data SBVRunMode
-- | In regular mode, with a stage. Bool is True if this is SAT.
SMTMode :: IStage -> Bool -> SMTConfig -> SBVRunMode
-- | Code generation mode.
CodeGen :: SBVRunMode
-- | Concrete simulation mode.
Concrete :: SBVRunMode
-- | Kind of symbolic value
data Kind
KBool :: Kind
KBounded :: !Bool -> !Int -> Kind
KUnbounded :: Kind
KReal :: Kind
KUserSort :: String -> (Either String [String]) -> Kind
KFloat :: Kind
KDouble :: Kind
-- | A class representing what can be returned from a symbolic computation.
class Outputtable a
-- | Mark an interim result as an output. Useful when constructing Symbolic
-- programs that return multiple values, or when the result is
-- programmatically computed.
output :: Outputtable a => a -> Symbolic a
-- | Result of running a symbolic computation
data Result
Result :: Set Kind -> [(String, CW)] -> [(String, [String])] -> ([(Quantifier, NamedSymVar)], [NamedSymVar]) -> [(SW, CW)] -> [((Int, Kind, Kind), [SW])] -> [(Int, ArrayInfo)] -> [(String, SBVType)] -> [(String, [String])] -> SBVPgm -> [(Maybe String, SW)] -> [(String, Maybe CallStack, SW)] -> [SW] -> Result
-- | kinds used in the program
[reskinds] :: Result -> Set Kind
-- | quick-check counter-example information (if any)
[resTraces] :: Result -> [(String, CW)]
-- | uninterpeted code segments
[resUISegs] :: Result -> [(String, [String])]
-- | inputs (possibly existential) + tracker vars
[resInputs] :: Result -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
-- | constants
[resConsts] :: Result -> [(SW, CW)]
-- | tables (automatically constructed) (tableno, index-type, result-type)
-- elts
[resTables] :: Result -> [((Int, Kind, Kind), [SW])]
-- | arrays (user specified)
[resArrays] :: Result -> [(Int, ArrayInfo)]
-- | uninterpreted constants
[resUIConsts] :: Result -> [(String, SBVType)]
-- | axioms
[resAxioms] :: Result -> [(String, [String])]
-- | assignments
[resAsgns] :: Result -> SBVPgm
-- | additional constraints (boolean)
[resConstraints] :: Result -> [(Maybe String, SW)]
-- | assertions
[resAssertions] :: Result -> [(String, Maybe CallStack, SW)]
-- | outputs
[resOutputs] :: Result -> [SW]
-- | Actions we can do in a context: Either at problem description time or
-- while we are dynamically querying. Symbolic and Query
-- are two instances of this class. Note that we use this mechanism
-- internally and do not export it from SBV.
class SolverContext m
-- | Add a constraint, any satisfying instance must satisfy this condition
constrain :: SolverContext m => SBool -> m ()
-- | Add a named constraint. The name is used in unsat-core extraction.
namedConstraint :: SolverContext m => String -> SBool -> m ()
-- | Set info. Example: setInfo ":status" ["unsat"].
setInfo :: SolverContext m => String -> [String] -> m ()
-- | Set an option.
setOption :: SolverContext m => SMTOption -> m ()
-- | Set the logic.
setLogic :: SolverContext m => Logic -> m ()
-- | Set a solver time-out value, in milli-seconds. This function
-- essentially translates to the SMTLib call (set-info :timeout
-- val), and your backend solver may or may not support it! The
-- amount given is in milliseconds. Also see the function
-- timeOut for finer level control of time-outs, directly from
-- SBV.
setTimeOut :: SolverContext m => Integer -> m ()
-- | Create an internal variable, which acts as an input but isn't visible
-- to the user. Such variables are existentially quantified in a SAT
-- context, and universally quantified in a proof context.
internalVariable :: State -> Kind -> IO SW
-- | Require a boolean condition to be true in the state. Only used for
-- internal purposes.
internalConstraint :: State -> Maybe String -> SVal -> IO ()
-- | Is this a CodeGen run? (i.e., generating code)
isCodeGenMode :: State -> IO Bool
-- | A simple type for SBV computations, used mainly for uninterpreted
-- constants. We keep track of the signedness/size of the arguments. A
-- non-function will have just one entry in the list.
newtype SBVType
SBVType :: [Kind] -> SBVType
-- | Create a new uninterpreted symbol, possibly with user given code
newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
-- | Add a user specified axiom to the generated SMT-Lib file. The first
-- argument is a mere string, use for commenting purposes. The second
-- argument is intended to hold the multiple-lines of the axiom text as
-- expressed in SMT-Lib notation. Note that we perform no checks on the
-- axiom itself, to see whether it's actually well-formed or is sensical
-- by any means. A separate formalization of SMT-Lib would be very useful
-- here.
addAxiom :: String -> [String] -> Symbolic ()
-- | Quantifiers: forall or exists. Note that we allow arbitrary nestings.
data Quantifier
ALL :: Quantifier
EX :: Quantifier
-- | Are there any existential quantifiers?
needsExistentials :: [Quantifier] -> Bool
-- | Representation of an SMT-Lib program. In between pre and post goes the
-- refuted models
data SMTLibPgm
SMTLibPgm :: SMTLibVersion -> [String] -> SMTLibPgm
-- | Representation of SMTLib Program versions. As of June 2015, we're
-- dropping support for SMTLib1, and supporting SMTLib2 only. We keep
-- this data-type around in case SMTLib3 comes along and we want to
-- support 2 and 3 simultaneously.
data SMTLibVersion
SMTLib2 :: SMTLibVersion
-- | The extension associated with the version
smtLibVersionExtension :: SMTLibVersion -> String
-- | Names reserved by SMTLib. This list is current as of Dec 6 2015; but
-- of course there's no guarantee it'll stay that way.
smtLibReservedNames :: [String]
-- | Translation tricks needed for specific capabilities afforded by each
-- solver
data SolverCapabilities
SolverCapabilities :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> SolverCapabilities
-- | Support for SMT-Lib2 style quantifiers?
[supportsQuantifiers] :: SolverCapabilities -> Bool
-- | Support for SMT-Lib2 style uninterpreted-sorts
[supportsUninterpretedSorts] :: SolverCapabilities -> Bool
-- | Support for unbounded integers?
[supportsUnboundedInts] :: SolverCapabilities -> Bool
-- | Support for reals?
[supportsReals] :: SolverCapabilities -> Bool
-- | Supports printing of approximations of reals?
[supportsApproxReals] :: SolverCapabilities -> Bool
-- | Support for floating point numbers?
[supportsIEEE754] :: SolverCapabilities -> Bool
-- | Support for optimization routines?
[supportsOptimization] :: SolverCapabilities -> Bool
-- | Support for pseudo-boolean operations?
[supportsPseudoBooleans] :: SolverCapabilities -> Bool
-- | Support for interactive queries per SMT-Lib?
[supportsCustomQueries] :: SolverCapabilities -> Bool
-- | Support for global decls, needed for push-pop.
[supportsGlobalDecls] :: SolverCapabilities -> Bool
-- | Grab the program from a running symbolic simulation state.
extractSymbolicSimulationState :: State -> IO Result
-- | A script, to be passed to the solver.
data SMTScript
SMTScript :: String -> [String] -> SMTScript
-- | Initial feed
[scriptBody] :: SMTScript -> String
-- | Continuation script, to extract results
[scriptModel] :: SMTScript -> [String]
-- | Solvers that SBV is aware of
data Solver
Z3 :: Solver
Yices :: Solver
Boolector :: Solver
CVC4 :: Solver
MathSAT :: Solver
ABC :: Solver
-- | An SMT solver
data SMTSolver
SMTSolver :: Solver -> String -> (SMTConfig -> [String]) -> SMTEngine -> SolverCapabilities -> SMTSolver
-- | The solver in use
[name] :: SMTSolver -> Solver
-- | The path to its executable
[executable] :: SMTSolver -> String
-- | Options to provide to the solver
[options] :: SMTSolver -> SMTConfig -> [String]
-- | The solver engine, responsible for interpreting solver output
[engine] :: SMTSolver -> SMTEngine
-- | Various capabilities of the solver
[capabilities] :: SMTSolver -> SolverCapabilities
-- | The result of an SMT solver call. Each constructor is tagged with the
-- SMTConfig that created it so that further tools can inspect it
-- and build layers of results, if needed. For ordinary uses of the
-- library, this type should not be needed, instead use the accessor
-- functions on it. (Custom Show instances and model extractors.)
data SMTResult
-- | Unsatisfiable
Unsatisfiable :: SMTConfig -> SMTResult
-- | Satisfiable with model
Satisfiable :: SMTConfig -> SMTModel -> SMTResult
-- | Prover returned a model, but in an extension field containing
-- Infinite/epsilon
SatExtField :: SMTConfig -> SMTModel -> SMTResult
-- | Prover returned unknown, with the given reason
Unknown :: SMTConfig -> String -> SMTResult
-- | Prover errored out
ProofError :: SMTConfig -> [String] -> SMTResult
-- | A model, as returned by a solver
data SMTModel
SMTModel :: [(String, GeneralizedCW)] -> [(String, CW)] -> SMTModel
-- | Mapping of symbolic values to objective values.
[modelObjectives] :: SMTModel -> [(String, GeneralizedCW)]
-- | Mapping of symbolic values to constants.
[modelAssocs] :: SMTModel -> [(String, CW)]
-- | Solver configuration. See also z3, yices,
-- cvc4, boolector, mathSAT, etc. 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 not
-- necessarily have finite decimal representations, and hence we have to
-- stop printing at some depth. It is important to emphasize that such
-- values always have infinite precision internally. The issue is merely
-- with how we print such an infinite precision value on the screen. The
-- field printRealPrec controls the printing precision, by
-- specifying the number of digits after the decimal point. The default
-- value is 16, but it can be set to any positive integer.
--
-- When printing, SBV will add the suffix ... at the and of a
-- real-value, if the given bound is not sufficient to represent the
-- real-value exactly. Otherwise, the number will be written out in
-- standard decimal notation. Note that SBV will always print the whole
-- value if it is precise (i.e., if it fits in a finite number of
-- digits), regardless of the precision limit. The limit only applies if
-- the representation of the real value is not finite, i.e., if it is not
-- rational.
--
-- The printBase field can be used to print numbers in base 2, 10,
-- or 16. If base 2 or 16 is used, then floating-point values will be
-- printed in their internal memory-layout format as well, which can come
-- in handy for bit-precise analysis.
data SMTConfig
SMTConfig :: Bool -> Timing -> Int -> Int -> String -> Maybe Int -> (String -> Bool) -> Maybe FilePath -> SMTLibVersion -> SMTSolver -> RoundingMode -> [SMTOption] -> Bool -> Maybe FilePath -> SMTConfig
-- | Debug mode
[verbose] :: SMTConfig -> Bool
-- | Print timing information on how long different phases took
-- (construction, solving, etc.)
[timing] :: SMTConfig -> Timing
-- | Print integral literals in this base (2, 10, and 16 are supported.)
[printBase] :: SMTConfig -> Int
-- | Print algebraic real values with this precision. (SReal, default: 16)
[printRealPrec] :: SMTConfig -> Int
-- | Usually "(check-sat)". However, users might tweak it based on solver
-- characteristics.
[satCmd] :: SMTConfig -> String
-- | In an allSat call, return at most this many models. If nothing, return
-- all.
[allSatMaxModelCount] :: SMTConfig -> Maybe Int
-- | When constructing a model, ignore variables whose name satisfy this
-- predicate. (Default: (const False), i.e., don't ignore anything)
[isNonModelVar] :: SMTConfig -> String -> Bool
-- | If Just, the entire interaction will be recorded as a playable file
-- (for debugging purposes mostly)
[transcript] :: SMTConfig -> Maybe FilePath
-- | What version of SMT-lib we use for the tool
[smtLibVersion] :: SMTConfig -> SMTLibVersion
-- | The actual SMT solver.
[solver] :: SMTConfig -> SMTSolver
-- | Rounding mode to use for floating-point conversions
[roundingMode] :: SMTConfig -> RoundingMode
-- | Options to set as we start the solver
[solverSetOptions] :: SMTConfig -> [SMTOption]
-- | If true, we shall ignore the exit code upon exit. Otherwise we require
-- ExitSuccess.
[ignoreExitCode] :: SMTConfig -> Bool
-- | Redirect the verbose output to this file if given. If Nothing, stdout
-- is implied.
[redirectVerbose] :: SMTConfig -> Maybe FilePath
-- | Declare a new symbolic array, with a potential initial value
declNewSArray :: forall a b. (HasKind a, HasKind b) => (Int -> String) -> Symbolic (SArray a b)
-- | Declare a new functional symbolic array. Note that a read from an
-- uninitialized cell will result in an error.
declNewSFunArray :: forall a b. (HasKind a, HasKind b) => Maybe String -> Symbolic (SFunArray a b)
-- | Style of optimization. Note that in the pareto case the user is
-- allowed to specify a max number of fronts to query the solver for,
-- since there might potentially be an infinite number of them and there
-- is no way to know exactly how many ahead of time. If Nothing is
-- given, SBV will possibly loop forever if the number is really
-- infinite.
data OptimizeStyle
-- | Objectives are optimized in the order given, earlier objectives have
-- higher priority. This is the default.
Lexicographic :: OptimizeStyle
-- | Each objective is optimized independently.
Independent :: OptimizeStyle
-- | Objectives are optimized according to pareto front: That is, no
-- objective can be made better without making some other worse.
Pareto :: (Maybe Int) -> OptimizeStyle
-- | Penalty for a soft-assertion. The default penalty is 1, with
-- all soft-assertions belonging to the same objective goal. A positive
-- weight and an optional group can be provided by using the
-- Penalty constructor.
data Penalty
-- | Default: Penalty of 1 and no group attached
DefaultPenalty :: Penalty
-- | Penalty with a weight and an optional group
Penalty :: Rational -> (Maybe String) -> Penalty
-- | Objective of optimization. We can minimize, maximize, or give a soft
-- assertion with a penalty for not satisfying it.
data Objective a
-- | Minimize this metric
Minimize :: String -> a -> Objective a
-- | Maximize this metric
Maximize :: String -> a -> Objective a
-- | A soft assertion, with an associated penalty
AssertSoft :: String -> a -> Penalty -> Objective a
-- | The state we keep track of as we interact with the solver
data QueryState
QueryState :: (Maybe Int -> String -> IO String) -> (Maybe Int -> String -> IO ()) -> (Maybe Int -> IO String) -> SMTConfig -> IO () -> Maybe Int -> Int -> QueryState
[queryAsk] :: QueryState -> Maybe Int -> String -> IO String
[querySend] :: QueryState -> Maybe Int -> String -> IO ()
[queryRetrieveResponse] :: QueryState -> Maybe Int -> IO String
[queryConfig] :: QueryState -> SMTConfig
[queryTerminate] :: QueryState -> IO ()
[queryTimeOutValue] :: QueryState -> Maybe Int
[queryAssertionStackDepth] :: QueryState -> Int
-- | A query is a user-guided mechanism to directly communicate and extract
-- results from the solver.
newtype Query a
Query :: (StateT State IO a) -> Query a
-- | Internal representation of a symbolic simulation result
newtype SMTProblem
-- | SMTLib representation, given the config
SMTProblem :: (SMTConfig -> SMTLibPgm) -> SMTProblem
[smtLibPgm] :: SMTProblem -> SMTConfig -> SMTLibPgm
-- | Generate a finite constant bitvector
genLiteral :: Integral a => Kind -> a -> SBV b
-- | Convert a constant to an integral value
genFromCW :: Integral a => CW -> a
-- | CW represents a concrete word of a fixed size: Endianness is
-- mostly irrelevant (see the FromBits class). For signed words,
-- the most significant digit is considered to be the sign.
data CW
CW :: !Kind -> !CWVal -> CW
[_cwKind] :: CW -> !Kind
[cwVal] :: CW -> !CWVal
-- | Generically make a symbolic var
genMkSymVar :: Kind -> Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
-- | Perform a sanity check that we should receive precisely the same
-- number of bits as required by the resulting type. The input is
-- little-endian
checkAndConvert :: (Num a, Bits a, SymWord a) => Int -> [SBool] -> SBV a
-- | Parse a signed/sized value from a sequence of CWs
genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
-- | Show a model in human readable form. Ignore bindings to those
-- variables that start with "__internal_sbv_" and also those marked as
-- "nonModelVar" in the config; as these are only for internal purposes
showModel :: SMTConfig -> SMTModel -> String
-- | A model, as returned by a solver
data SMTModel
SMTModel :: [(String, GeneralizedCW)] -> [(String, CW)] -> SMTModel
-- | Mapping of symbolic values to objective values.
[modelObjectives] :: SMTModel -> [(String, GeneralizedCW)]
-- | Mapping of symbolic values to constants.
[modelAssocs] :: SMTModel -> [(String, CW)]
-- | Lift QRem to symbolic words. Division by 0 is defined s.t.
-- x/0 = 0; which holds even when x is 0
-- itself.
liftQRem :: SymWord a => SBV a -> SBV a -> (SBV a, SBV a)
-- | Lift DMod to symbolic words. Division by 0 is defined s.t.
-- x/0 = 0; which holds even when x is 0
-- itself. Essentially, this is conversion from quotRem (truncate to 0)
-- to divMod (truncate towards negative infinity)
liftDMod :: (SymWord a, Num a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
-- | Lower level version of compileToC, producing a
-- CgPgmBundle
compileToC' :: String -> SBVCodeGen () -> IO CgPgmBundle
-- | Lower level version of compileToCLib, producing a
-- CgPgmBundle
compileToCLib' :: String -> [(String, SBVCodeGen ())] -> IO CgPgmBundle
-- | The code-generation monad. Allows for precise layout of input values
-- reference parameters (for returning composite values in languages such
-- as C), and return values.
newtype SBVCodeGen a
SBVCodeGen :: (StateT CgState Symbolic a) -> SBVCodeGen a
-- | Creates an atomic input in the generated code.
cgInput :: SymWord a => String -> SBVCodeGen (SBV a)
-- | Creates an array input in the generated code.
cgInputArr :: SymWord a => Int -> String -> SBVCodeGen [SBV a]
-- | Creates an atomic output in the generated code.
cgOutput :: String -> SBV a -> SBVCodeGen ()
-- | Creates an array output in the generated code.
cgOutputArr :: SymWord a => String -> [SBV a] -> SBVCodeGen ()
-- | Creates a returned (unnamed) value in the generated code.
cgReturn :: SBV a -> SBVCodeGen ()
-- | Creates a returned (unnamed) array value in the generated code.
cgReturnArr :: SymWord a => [SBV a] -> SBVCodeGen ()
-- | Creates an atomic input in the generated code.
svCgInput :: Kind -> String -> SBVCodeGen SVal
-- | Creates an array input in the generated code.
svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
-- | Creates an atomic output in the generated code.
svCgOutput :: String -> SVal -> SBVCodeGen ()
-- | Creates an array output in the generated code.
svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
-- | Creates a returned (unnamed) value in the generated code.
svCgReturn :: SVal -> SBVCodeGen ()
-- | Creates a returned (unnamed) array value in the generated code.
svCgReturnArr :: [SVal] -> SBVCodeGen ()
-- | Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large
-- value etc. on/off. Default: False.
cgPerformRTCs :: Bool -> SBVCodeGen ()
-- | Sets driver program run time values, useful for generating programs
-- with fixed drivers for testing. Default: None, i.e., use random
-- values.
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
-- | Adds the given lines to the header file generated, useful for
-- generating programs with uninterpreted functions.
cgAddPrototype :: [String] -> SBVCodeGen ()
-- | Adds the given lines to the program file generated, useful for
-- generating programs with uninterpreted functions.
cgAddDecl :: [String] -> SBVCodeGen ()
-- | Adds the given words to the compiler options in the generated
-- Makefile, useful for linking extra stuff in.
cgAddLDFlags :: [String] -> SBVCodeGen ()
-- | Ignore assertions (those generated by sAssert calls) in the
-- generated C code
cgIgnoreSAssert :: Bool -> SBVCodeGen ()
-- | Sets number of bits to be used for representing the SInteger
-- type in the generated C code. The argument must be one of 8,
-- 16, 32, or 64. Note that this is
-- essentially unsafe as the semantics of unbounded Haskell integers
-- becomes reduced to the corresponding bit size, as typical in most C
-- implementations.
cgIntegerSize :: Int -> SBVCodeGen ()
-- | Sets the C type to be used for representing the SReal type in
-- the generated C code. The setting can be one of C's "float",
-- "double", or "long double", types, depending on the
-- precision needed. Note that this is essentially unsafe as the
-- semantics of infinite precision SReal values becomes reduced to the
-- corresponding floating point type in C, and hence it is subject to
-- rounding errors.
cgSRealType :: CgSRealType -> SBVCodeGen ()
-- | Possible mappings for the SReal type when translated to C. Used
-- in conjunction with the function cgSRealType. Note that the
-- particular characteristics of the mapped types depend on the platform
-- and the compiler used for compiling the generated C program. See
-- http://en.wikipedia.org/wiki/C_data_types for details.
data CgSRealType
-- |
-- float
--
CgFloat :: CgSRealType
-- |
-- double
--
CgDouble :: CgSRealType
-- |
-- long double
--
CgLongDouble :: CgSRealType
-- | Abstract over code generation for different languages
class CgTarget a
targetName :: CgTarget a => a -> String
translate :: CgTarget a => a -> CgConfig -> String -> CgState -> Result -> CgPgmBundle
-- | Options for code-generation.
data CgConfig
CgConfig :: Bool -> Maybe Int -> Maybe CgSRealType -> [Integer] -> Bool -> Bool -> Bool -> CgConfig
-- | If True, perform run-time-checks for index-out-of-bounds or
-- shifting-by-large values etc.
[cgRTC] :: CgConfig -> Bool
-- | Bit-size to use for representing SInteger (if any)
[cgInteger] :: CgConfig -> Maybe Int
-- | Type to use for representing SReal (if any)
[cgReal] :: CgConfig -> Maybe CgSRealType
-- | Values to use for the driver program generated, useful for generating
-- non-random drivers.
[cgDriverVals] :: CgConfig -> [Integer]
-- | If True, will generate a driver program
[cgGenDriver] :: CgConfig -> Bool
-- | If True, will generate a makefile
[cgGenMakefile] :: CgConfig -> Bool
-- | If True, will ignore sAssert calls
[cgIgnoreAsserts] :: CgConfig -> Bool
-- | Code-generation state
data CgState
CgState :: [(String, CgVal)] -> [(String, CgVal)] -> [CgVal] -> [String] -> [String] -> [String] -> CgConfig -> CgState
[cgInputs] :: CgState -> [(String, CgVal)]
[cgOutputs] :: CgState -> [(String, CgVal)]
[cgReturns] :: CgState -> [CgVal]
[cgPrototypes] :: CgState -> [String]
[cgDecls] :: CgState -> [String]
[cgLDFlags] :: CgState -> [String]
[cgFinalConfig] :: CgState -> CgConfig
-- | Representation of a collection of generated programs.
data CgPgmBundle
CgPgmBundle :: (Maybe Int, Maybe CgSRealType) -> [(FilePath, (CgPgmKind, [Doc]))] -> CgPgmBundle
-- | Different kinds of "files" we can produce. Currently this is quite
-- C specific.
data CgPgmKind
CgMakefile :: [String] -> CgPgmKind
CgHeader :: [Doc] -> CgPgmKind
CgSource :: CgPgmKind
CgDriver :: CgPgmKind
-- | Abstraction of target language values
data CgVal
CgAtomic :: SW -> CgVal
CgArray :: [SW] -> CgVal
-- | Default options for code generation. The run-time checks are
-- turned-off, and the driver values are completely random.
defaultCgConfig :: CgConfig
-- | Initial configuration for code-generation
initCgState :: CgState
-- | Is this a driver program?
isCgDriver :: CgPgmKind -> Bool
-- | Is this a make file?
isCgMakefile :: CgPgmKind -> Bool
-- | Should we generate a driver program? Default: True. When a
-- library is generated, it will have a driver if any of the contituent
-- functions has a driver. (See compileToCLib.)
cgGenerateDriver :: Bool -> SBVCodeGen ()
-- | Should we generate a Makefile? Default: True.
cgGenerateMakefile :: Bool -> SBVCodeGen ()
-- | Generate code for a symbolic program, returning a Code-gen bundle,
-- i.e., collection of makefiles, source code, headers, etc.
codeGen :: CgTarget l => l -> CgConfig -> String -> SBVCodeGen () -> IO CgPgmBundle
-- | Render a code-gen bundle to a directory or to stdout
renderCgPgmBundle :: Maybe FilePath -> CgPgmBundle -> IO ()
-- | A variant of round; except defaulting to 0 when fed NaN or Infinity
fpRound0 :: (RealFloat a, Integral b) => a -> b
-- | A variant of toRational; except defaulting to 0 when fed NaN or
-- Infinity
fpRatio0 :: (RealFloat a) => a -> Rational
-- | The SMT-Lib (in particular Z3) implementation for min/max for floats
-- does not agree with Haskell's; and also it does not agree with what
-- the hardware does. Sigh.. See:
-- https://ghc.haskell.org/trac/ghc/ticket/10378
-- https://github.com/Z3Prover/z3/issues/68 So, we codify here
-- what the Z3 (SMTLib) is implementing for fpMax. The discrepancy with
-- Haskell is that the NaN propagation doesn't work in Haskell The
-- discrepancy with x86 is that given +0/-0, x86 returns the second
-- argument; SMTLib is non-deterministic
fpMaxH :: RealFloat a => a -> a -> a
-- | SMTLib compliant definition for fpMin. See the comments for
-- fpMax.
fpMinH :: RealFloat a => a -> a -> a
-- | Convert double to float and back. Essentially fromRational .
-- toRational except careful on NaN, Infinities, and -0.
fp2fp :: (RealFloat a, RealFloat b) => a -> b
-- | Compute the "floating-point" remainder function, the float/double
-- value that remains from the division of x and y.
-- There are strict rules around 0's, Infinities, and NaN's as coded
-- below, See http://smt-lib.org/papers/BTRW14.pdf, towards the
-- end of section 4.c.
fpRemH :: RealFloat a => a -> a -> a
-- | Convert a float to the nearest integral representable in that type
fpRoundToIntegralH :: RealFloat a => a -> a
-- | Check that two floats are the exact same values, i.e., +0/-0 does not
-- compare equal, and NaN's compare equal to themselves.
fpIsEqualObjectH :: RealFloat a => a -> a -> Bool
-- | Check if a number is "normal." Note that +0/-0 is not considered a
-- normal-number and also this is not simply the negation of
-- isDenormalized!
fpIsNormalizedH :: RealFloat a => a -> Bool
-- | PrettyNum class captures printing of numbers in hex and binary
-- formats; also supporting negative numbers.
--
-- Minimal complete definition: hexS and binS
class PrettyNum a
-- | Show a number in hexadecimal (starting with 0x and type.)
hexS :: PrettyNum a => a -> String
-- | Show a number in binary (starting with 0b and type.)
binS :: PrettyNum a => a -> String
-- | Show a number in hex, without prefix, or types.
hex :: PrettyNum a => a -> String
-- | Show a number in bin, without prefix, or types.
bin :: PrettyNum a => a -> String
-- | A more convenient interface for reading binary numbers, also supports
-- negative numbers
readBin :: Num a => String -> a
-- | Show as a hexadecimal value. First bool controls whether type info is
-- printed while the second boolean controls wether 0x prefix is printed.
-- The tuple is the signedness and the bit-length of the input. The
-- length of the string will not depend on the value, but rather
-- the bit-length.
shex :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
-- | Show as a hexadecimal value, integer version. Almost the same as shex
-- above except we don't have a bit-length so the length of the string
-- will depend on the actual value.
shexI :: Bool -> Bool -> Integer -> String
-- | Similar to shex; except in binary.
sbin :: (Show a, Integral a) => Bool -> Bool -> (Bool, Int) -> a -> String
-- | Similar to shexI; except in binary.
sbinI :: Bool -> Bool -> Integer -> String
-- | A version of show for floats that generates correct C literals for
-- nan/infinite. NB. Requires "math.h" to be included.
showCFloat :: Float -> String
-- | A version of show for doubles that generates correct C literals for
-- nan/infinite. NB. Requires "math.h" to be included.
showCDouble :: Double -> String
-- | A version of show for floats that generates correct Haskell literals
-- for nan/infinite
showHFloat :: Float -> String
-- | A version of show for doubles that generates correct Haskell literals
-- for nan/infinite
showHDouble :: Double -> String
-- | A version of show for floats that generates correct SMTLib literals
-- using the rounding mode
showSMTFloat :: RoundingMode -> Float -> String
-- | A version of show for doubles that generates correct SMTLib literals
-- using the rounding mode
showSMTDouble :: RoundingMode -> Double -> String
-- | Convert a rounding mode to the format SMT-Lib2 understands.
smtRoundingMode :: RoundingMode -> String
-- | Convert a CW to an SMTLib2 compliant value
cwToSMTLib :: RoundingMode -> CW -> String
-- | Create a skolem 0 for the kind
mkSkolemZero :: RoundingMode -> Kind -> String
-- | Specify how to save timing information, if at all.
data Timing
NoTiming :: Timing
PrintTiming :: Timing
SaveTiming :: (IORef NominalDiffTime) -> Timing
-- | Show NominalDiffTime in human readable form.
-- NominalDiffTime is essentially picoseconds (10^-12 seconds). We
-- show it so that it's represented at the day:hour:minute:second.XXX
-- granularity.
showTDiff :: NominalDiffTime -> String
-- | Send an arbitrary string to the solver in a query. Note that this is
-- inherently dangerous as it can put the solver in an arbitrary state
-- and confuse SBV. If you use this feature, you are on your own!
sendStringToSolver :: String -> Query ()
-- | Send an arbitrary string to the solver in a query, and return a
-- response. Note that this is inherently dangerous as it can put the
-- solver in an arbitrary state and confuse SBV.
sendRequestToSolver :: String -> Query String
-- | Retrieve multiple responses from the solver, until it responds with a
-- user given tag that we shall arrange for internally. The optional
-- timeout is in milliseconds. If the time-out is exceeded, then we will
-- raise an error. Note that this is inherently dangerous as it can put
-- the solver in an arbitrary state and confuse SBV. If you use this
-- feature, you are on your own!
retrieveResponseFromSolver :: String -> Maybe Int -> Query [String]
-- | (The sbv library is hosted at
-- http://github.com/LeventErkok/sbv. Comments, bug reports, and
-- patches are always welcome.)
--
-- SBV: SMT Based Verification
--
-- Express properties about Haskell programs and automatically prove them
-- using SMT solvers.
--
--
-- >>> prove $ \x -> x `shiftL` 2 .== 4 * (x :: SWord8)
-- Q.E.D.
--
--
--
-- >>> prove $ \x -> x `shiftL` 2 .== 2 * (x :: SWord8)
-- Falsifiable. Counter-example:
-- s0 = 32 :: Word8
--
--
-- The function prove has the following type:
--
--
-- prove :: Provable a => a -> IO ThmResult
--
--
-- The class Provable comes with instances for n-ary predicates,
-- for arbitrary n. The predicates are just regular Haskell functions
-- over symbolic types listed below. Functions for checking
-- satisfiability (sat and allSat) are also provided.
--
-- The sbv library introduces the following symbolic types:
--
--
-- - SBool: Symbolic Booleans (bits).
-- - SWord8, SWord16, SWord32, SWord64:
-- Symbolic Words (unsigned).
-- - SInt8, SInt16, SInt32, SInt64:
-- Symbolic Ints (signed).
-- - SInteger: Unbounded signed integers.
-- - SReal: Algebraic-real numbers
-- - SFloat: IEEE-754 single-precision floating point
-- values
-- - SDouble: IEEE-754 double-precision floating point
-- values
-- - SArray, SFunArray: Flat arrays of symbolic
-- values.
-- - Symbolic polynomials over GF(2^n), polynomial arithmetic, and
-- CRCs.
-- - Uninterpreted constants and functions over symbolic values, with
-- user defined SMT-Lib axioms.
-- - Uninterpreted sorts, and proofs over such sorts, potentially with
-- axioms.
--
--
-- The user can construct ordinary Haskell programs using these types,
-- which behave very similar to their concrete counterparts. In
-- particular these types belong to the standard classes Num,
-- Bits, custom versions of Eq (EqSymbolic) and
-- Ord (OrdSymbolic), along with several other custom
-- classes for simplifying programming with symbolic values. The
-- framework takes full advantage of Haskell's type inference to avoid
-- many common mistakes.
--
-- Furthermore, predicates (i.e., functions that return SBool)
-- built out of these types can also be:
--
--
-- - proven correct via an external SMT solver (the prove
-- function)
-- - checked for satisfiability (the sat, allSat
-- functions)
-- - used in synthesis (the sat function with existentials)
-- - quick-checked
--
--
-- If a predicate is not valid, prove will return a
-- counterexample: An assignment to inputs such that the predicate fails.
-- The sat function will return a satisfying assignment, if there
-- is one. The allSat function returns all satisfying assignments.
--
-- The sbv library uses third-party SMT solvers via the standard SMT-Lib
-- interface: http://smtlib.cs.uiowa.edu/
--
-- The SBV library is designed to work with any SMT-Lib compliant
-- SMT-solver. Currently, we support the following SMT-Solvers out-of-the
-- box:
--
--
--
-- SBV requires recent versions of these solvers; please see the file
-- SMTSolverVersions.md in the source distribution for
-- specifics.
--
-- SBV also allows calling these solvers in parallel, either getting
-- results from multiple solvers or returning the fastest one. (See
-- proveWithAll, proveWithAny, etc.)
--
-- 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.
module Data.SBV
-- | A symbolic boolean/bit
type SBool = SBV Bool
-- | 8-bit unsigned symbolic value
type SWord8 = SBV Word8
-- | 16-bit unsigned symbolic value
type SWord16 = SBV Word16
-- | 32-bit unsigned symbolic value
type SWord32 = SBV Word32
-- | 64-bit unsigned symbolic value
type SWord64 = SBV Word64
-- | 8-bit signed symbolic value, 2's complement representation
type SInt8 = SBV Int8
-- | 16-bit signed symbolic value, 2's complement representation
type SInt16 = SBV Int16
-- | 32-bit signed symbolic value, 2's complement representation
type SInt32 = SBV Int32
-- | 64-bit signed symbolic value, 2's complement representation
type SInt64 = SBV Int64
-- | Infinite precision signed symbolic value
type SInteger = SBV Integer
-- | IEEE-754 single-precision floating point numbers
type SFloat = SBV Float
-- | IEEE-754 double-precision floating point numbers
type SDouble = SBV Double
-- | Infinite precision symbolic algebraic real value
type SReal = SBV AlgReal
-- | Algebraic reals. Note that the representation is left abstract. We
-- represent rational results explicitly, while the roots-of-polynomials
-- are represented implicitly by their defining equation
data AlgReal
-- | Convert an SReal to an SInteger. That is, it computes the largest
-- integer n that satisfies sIntegerToSReal n <= r
-- essentially giving us the floor.
--
-- For instance, 1.3 will be 1, but -1.3 will
-- be -2.
sRealToSInteger :: SReal -> SInteger
-- | Declare an SBool
sBool :: String -> Symbolic SBool
-- | Declare an SWord8
sWord8 :: String -> Symbolic SWord8
-- | Declare an SWord16
sWord16 :: String -> Symbolic SWord16
-- | Declare an SWord32
sWord32 :: String -> Symbolic SWord32
-- | Declare an SWord64
sWord64 :: String -> Symbolic SWord64
-- | Declare an SInt8
sInt8 :: String -> Symbolic SInt8
-- | Declare an SInt16
sInt16 :: String -> Symbolic SInt16
-- | Declare an SInt32
sInt32 :: String -> Symbolic SInt32
-- | Declare an SInt64
sInt64 :: String -> Symbolic SInt64
-- | Declare an SInteger
sInteger :: String -> Symbolic SInteger
-- | Declare an SReal
sReal :: String -> Symbolic SReal
-- | Declare an SFloat
sFloat :: String -> Symbolic SFloat
-- | Declare an SDouble
sDouble :: String -> Symbolic SDouble
-- | Declare a list of SBools
sBools :: [String] -> Symbolic [SBool]
-- | Declare a list of SWord8s
sWord8s :: [String] -> Symbolic [SWord8]
-- | Declare a list of SWord16s
sWord16s :: [String] -> Symbolic [SWord16]
-- | Declare a list of SWord32s
sWord32s :: [String] -> Symbolic [SWord32]
-- | Declare a list of SWord64s
sWord64s :: [String] -> Symbolic [SWord64]
-- | Declare a list of SInt8s
sInt8s :: [String] -> Symbolic [SInt8]
-- | Declare a list of SInt16s
sInt16s :: [String] -> Symbolic [SInt16]
-- | Declare a list of SInt32s
sInt32s :: [String] -> Symbolic [SInt32]
-- | Declare a list of SInt64s
sInt64s :: [String] -> Symbolic [SInt64]
-- | Declare a list of SIntegers
sIntegers :: [String] -> Symbolic [SInteger]
-- | Declare a list of SReals
sReals :: [String] -> Symbolic [SReal]
-- | Declare a list of SFloats
sFloats :: [String] -> Symbolic [SFloat]
-- | Declare a list of SDoubles
sDoubles :: [String] -> Symbolic [SDouble]
-- | The Symbolic value. The parameter a is phantom, but is
-- extremely important in keeping the user interface strongly typed.
data SBV a
-- | A class for capturing values that have a sign and a size (finite or
-- infinite) minimal complete definition: kindOf. This class can be
-- automatically derived for data-types that have a Data
-- instance; this is useful for creating uninterpreted sorts.
class HasKind a
kindOf :: HasKind a => a -> Kind
hasSign :: HasKind a => a -> Bool
intSizeOf :: HasKind a => a -> Int
isBoolean :: HasKind a => a -> Bool
isBounded :: HasKind a => a -> Bool
isReal :: HasKind a => a -> Bool
isFloat :: HasKind a => a -> Bool
isDouble :: HasKind a => a -> Bool
isInteger :: HasKind a => a -> Bool
isUninterpreted :: HasKind a => a -> Bool
showType :: HasKind a => a -> String
kindOf :: (HasKind a, Read a, Data a) => a -> Kind
-- | Kind of symbolic value
data Kind
KBool :: Kind
KBounded :: !Bool -> !Int -> Kind
KUnbounded :: Kind
KReal :: Kind
KUserSort :: String -> (Either String [String]) -> Kind
KFloat :: Kind
KDouble :: Kind
-- | Flat arrays of symbolic values An array a b is an array
-- indexed by the type SBV a, with elements of type
-- SBV b.
--
-- While it's certainly possible for user to create instances of
-- SymArray, the SArray and SFunArray instances
-- already provided should cover most use cases in practice. (There are
-- some differences between these models, however, see the corresponding
-- declaration.)
--
-- Minimal complete definition: All methods are required, no defaults.
class SymArray array
-- | Create a new anonymous array
newArray_ :: (SymArray array, HasKind a, HasKind b) => Symbolic (array a b)
-- | Create a named new array
newArray :: (SymArray array, HasKind a, HasKind b) => String -> Symbolic (array a b)
-- | Read the array element at a
readArray :: SymArray array => array a b -> SBV a -> SBV b
-- | Update the element at a to be b
writeArray :: (SymArray array, SymWord b) => array a b -> SBV a -> SBV b -> array a b
-- | Merge two given arrays on the symbolic condition Intuitively:
-- mergeArrays cond a b = if cond then a else b. Merging pushes
-- the if-then-else choice down on to elements
mergeArrays :: (SymArray array, SymWord b) => SBV Bool -> array a b -> array a b -> array a b
-- | Arrays implemented in terms of SMT-arrays:
-- http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
--
--
-- - Maps directly to SMT-lib arrays
-- - Reading from an unintialized value is OK and yields an unspecified
-- result
-- - Can check for equality of these arrays
-- - Cannot quick-check theorems using SArray values
-- - Typically slower as it heavily relies on SMT-solving for the array
-- theory
--
data SArray a b
-- | Arrays implemented internally as functions
--
--
-- - Internally handled by the library and not mapped to SMT-Lib
-- - Reading an uninitialized value is considered an error (will throw
-- exception)
-- - Cannot check for equality (internally represented as
-- functions)
-- - Can quick-check
-- - Typically faster as it gets compiled away during translation
--
data SFunArray a b
-- | Lift a function to an array. Useful for creating arrays in a pure
-- context. (Otherwise use newArray.)
mkSFunArray :: (SBV a -> SBV b) -> SFunArray a b
-- | Replacement for testBit. Since testBit requires a
-- Bool to be returned, we cannot implement it for symbolic words.
-- Index 0 is the least-significant bit.
sTestBit :: SBV a -> Int -> SBool
-- | Variant of sTestBit, where we want to extract multiple bit
-- positions.
sExtractBits :: SBV a -> [Int] -> [SBool]
-- | Replacement for popCount. Since popCount returns an
-- Int, we cannot implement it for symbolic words. Here, we return
-- an SWord8, which can overflow when used on quantities that have
-- more than 255 bits. Currently, that's only the SInteger type
-- that SBV supports, all other types are safe. Even with
-- SInteger, this will only overflow if there are at least
-- 256-bits set in the number, and the smallest such number is 2^256-1,
-- which is a pretty darn big number to worry about for practical
-- purposes. In any case, we do not support sPopCount for
-- unbounded symbolic integers, as the only possible implementation
-- wouldn't symbolically terminate. So the only overflow issue is with
-- really-really large concrete SInteger values.
sPopCount :: (Num a, Bits a, SymWord a) => SBV a -> SWord8
-- | Generalization of shiftL, when the shift-amount is symbolic.
-- Since Haskell's shiftL only takes an Int as the shift
-- amount, it cannot be used when we have a symbolic amount to shift
-- with.
sShiftLeft :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
-- | Generalization of shiftR, when the shift-amount is symbolic.
-- Since Haskell's shiftR only takes an Int as the shift
-- amount, it cannot be used when we have a symbolic amount to shift
-- with.
--
-- NB. If the shiftee is signed, then this is an arithmetic shift;
-- otherwise it's logical, following the usual Haskell convention. See
-- sSignedShiftArithRight for a variant that explicitly uses the
-- msb as the sign bit, even for unsigned underlying types.
sShiftRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
-- | Generalization of rotateL, when the shift-amount is symbolic.
-- Since Haskell's rotateL only takes an Int as the shift
-- amount, it cannot be used when we have a symbolic amount to shift
-- with. The first argument should be a bounded quantity.
sRotateLeft :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a
-- | Generalization of rotateR, when the shift-amount is symbolic.
-- Since Haskell's rotateR only takes an Int as the shift
-- amount, it cannot be used when we have a symbolic amount to shift
-- with. The first argument should be a bounded quantity.
sRotateRight :: (SIntegral a, SIntegral b, SDivisible (SBV b)) => SBV a -> SBV b -> SBV a
-- | Arithmetic shift-right with a symbolic unsigned shift amount. This is
-- equivalent to sShiftRight when the argument is signed. However,
-- if the argument is unsigned, then it explicitly treats its msb as a
-- sign-bit, and uses it as the bit that gets shifted in. Useful when
-- using the underlying unsigned bit representation to implement custom
-- signed operations. Note that there is no direct Haskell analogue of
-- this function.
sSignedShiftArithRight :: (SIntegral a, SIntegral b) => SBV a -> SBV b -> SBV a
-- | Conversion between integral-symbolic values, akin to Haskell's
-- fromIntegral
sFromIntegral :: forall a b. (Integral a, HasKind a, Num a, SymWord a, HasKind b, Num b, SymWord b) => SBV a -> SBV b
-- | Generalization of setBit based on a symbolic boolean. Note that
-- setBit and clearBit are still available on Symbolic
-- words, this operation comes handy when the condition to set/clear
-- happens to be symbolic.
setBitTo :: (Num a, Bits a, SymWord a) => SBV a -> Int -> SBool -> SBV a
-- | Returns 1 if the boolean is true, otherwise 0.
oneIf :: (Num a, SymWord a) => SBool -> SBV a
-- | Least significant bit of a word, always stored at index 0.
lsb :: SBV a -> SBool
-- | Most significant bit of a word, always stored at the last position.
msb :: (Num a, Bits a, SymWord a) => SBV a -> SBool
-- | label: Label the result of an expression. This is essentially a no-op,
-- but useful as it generates a comment in the generated C/SMT-Lib code.
-- Note that if the argument is a constant, then the label is dropped
-- completely, per the usual constant folding strategy.
label :: SymWord a => String -> SBV a -> SBV a
-- | 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)
-- | 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)
-- | Symbolic exponentiation using bit blasting and repeated squaring.
--
-- N.B. The exponent must be unsigned. Signed exponents will be rejected.
(.^) :: (Mergeable b, Num b, SIntegral e) => b -> SBV e -> b
-- | Big-endian blasting of a word into its bits. Also see the
-- FromBits class.
blastBE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]
-- | Little-endian blasting of a word into its bits. Also see the
-- FromBits class.
blastLE :: (Num a, Bits a, SymWord a) => SBV a -> [SBool]
-- | Unblasting a value from symbolic-bits. The bits can be given
-- little-endian or big-endian. For a signed number in little-endian, we
-- assume the very last bit is the sign digit. This is a bit awkward, but
-- it is more consistent with the "reverse" view of little-big-endian
-- representations
--
-- Minimal complete definition: fromBitsLE
class FromBits a
fromBitsLE, fromBitsBE :: FromBits a => [SBool] -> a
fromBitsLE, fromBitsBE :: FromBits a => [SBool] -> a
-- | Splitting an a into two b's and joining back.
-- Intuitively, a is a larger bit-size word than b,
-- typically double. The extend operation captures embedding of a
-- b value into an a without changing its semantic
-- value.
--
-- Minimal complete definition: All, no defaults.
class Splittable a b | b -> a
split :: Splittable a b => a -> (b, b)
(#) :: Splittable a b => b -> b -> a
extend :: Splittable a b => b -> a
-- | Symbolic conditionals are modeled by the Mergeable class,
-- describing how to merge the results of an if-then-else call with a
-- symbolic test. SBV provides all basic types as instances of this
-- class, so users only need to declare instances for custom data-types
-- of their programs as needed.
--
-- A Mergeable instance may be automatically derived for a custom
-- data-type with a single constructor where the type of each field is an
-- instance of Mergeable, such as a record of symbolic values.
-- Users only need to add Generic and Mergeable to the
-- deriving clause for the data-type. See Status for an
-- example and an illustration of what the instance would look like if
-- written by hand.
--
-- The function select is a total-indexing function out of a list
-- of choices with a default value, simulating array/list indexing. It's
-- an n-way generalization of the ite function.
--
-- Minimal complete definition: None, if the type is instance of
-- Generic. Otherwise symbolicMerge. Note that most types
-- subject to merging are likely to be trivial instances of
-- Generic.
class Mergeable a
-- | Merge two values based on the condition. The first argument states
-- whether we force the then-and-else branches before the merging, at the
-- word level. This is an efficiency concern; one that we'd rather not
-- make but unfortunately necessary for getting symbolic simulation
-- working efficiently.
symbolicMerge :: Mergeable a => Bool -> SBool -> a -> a -> a
-- | Total indexing operation. select xs default index is
-- intuitively the same as xs !! index, except it evaluates to
-- default if index underflows/overflows.
select :: (Mergeable a, SymWord b, Num b) => [a] -> a -> SBV b -> a
-- | Merge two values based on the condition. The first argument states
-- whether we force the then-and-else branches before the merging, at the
-- word level. This is an efficiency concern; one that we'd rather not
-- make but unfortunately necessary for getting symbolic simulation
-- working efficiently.
symbolicMerge :: (Mergeable a, Generic a, GMergeable (Rep a)) => Bool -> SBool -> a -> a -> a
-- | If-then-else. This is by definition symbolicMerge with both
-- branches forced. This is typically the desired behavior, but also see
-- iteLazy should you need more laziness.
ite :: Mergeable a => SBool -> a -> a -> a
-- | A Lazy version of ite, which does not force its arguments. This might
-- cause issues for symbolic simulation with large thunks around, so use
-- with care.
iteLazy :: Mergeable a => SBool -> a -> a -> a
-- | Symbolic Numbers. This is a simple class that simply incorporates all
-- number like base types together, simplifying writing polymorphic
-- type-signatures that work for all symbolic numbers, such as
-- SWord8, SInt8 etc. For instance, we can write a generic
-- list-minimum function as follows:
--
--
-- mm :: SIntegral a => [SBV a] -> SBV a
-- mm = foldr1 (a b -> ite (a .<= b) a b)
--
--
-- It is similar to the standard Integral class, except ranging
-- over symbolic instances.
class (SymWord a, Num a, Bits a) => SIntegral a
-- | The SDivisible class captures the essence of division.
-- Unfortunately we cannot use Haskell's Integral class since the
-- Real and Enum superclasses are not implementable for
-- symbolic bit-vectors. However, quotRem and divMod makes
-- perfect sense, and the SDivisible class captures this
-- operation. One issue is how division by 0 behaves. The verification
-- technology requires total functions, and there are several design
-- choices here. We follow Isabelle/HOL approach of assigning the value 0
-- for division by 0. Therefore, we impose the following pair of laws:
--
--
-- x sQuotRem 0 = (0, x)
-- x sDivMod 0 = (0, x)
--
--
-- Note that our instances implement this law even when x is
-- 0 itself.
--
-- NB. quot truncates toward zero, while div truncates
-- toward negative infinity.
--
-- Minimal complete definition: sQuotRem, sDivMod
class SDivisible a
sQuotRem :: SDivisible a => a -> a -> (a, a)
sDivMod :: SDivisible a => a -> a -> (a, a)
sQuot :: SDivisible a => a -> a -> a
sRem :: SDivisible a => a -> a -> a
sDiv :: SDivisible a => a -> a -> a
sMod :: SDivisible a => a -> a -> a
-- | The Boolean class: a generalization of Haskell's Bool
-- type Haskell Bool and SBV's SBool are instances of
-- this class, unifying the treatment of boolean values.
--
-- Minimal complete definition: true, bnot,
-- &&& However, it's advisable to define false,
-- and ||| as well (typically), for clarity.
class Boolean b
-- | logical true
true :: Boolean b => b
-- | logical false
false :: Boolean b => b
-- | complement
bnot :: Boolean b => b -> b
-- | and
(&&&) :: Boolean b => b -> b -> b
-- | or
(|||) :: Boolean b => b -> b -> b
-- | nand
(~&) :: Boolean b => b -> b -> b
-- | nor
(~|) :: Boolean b => b -> b -> b
-- | xor
(<+>) :: Boolean b => b -> b -> b
-- | implies
(==>) :: Boolean b => b -> b -> b
-- | equivalence
(<=>) :: Boolean b => b -> b -> b
-- | cast from Bool
fromBool :: Boolean b => Bool -> b
-- | Generalization of and
bAnd :: Boolean b => [b] -> b
-- | Generalization of or
bOr :: Boolean b => [b] -> b
-- | Generalization of any
bAny :: Boolean b => (a -> b) -> [a] -> b
-- | Generalization of all
bAll :: Boolean b => (a -> b) -> [a] -> b
-- | Uninterpreted constants and functions. An uninterpreted constant is a
-- value that is indexed by its name. The only property the prover
-- assumes about these values are that they are equivalent to themselves;
-- i.e., (for functions) they return the same results when applied to
-- same arguments. We support uninterpreted-functions as a general means
-- of black-box'ing operations that are irrelevant for the
-- purposes of the proof; i.e., when the proofs can be performed without
-- any knowledge about the function itself.
--
-- Minimal complete definition: sbvUninterpret. However, most
-- instances in practice are already provided by SBV, so end-users should
-- not need to define their own instances.
class Uninterpreted a
-- | Uninterpret a value, receiving an object that can be used instead. Use
-- this version when you do not need to add an axiom about this value.
uninterpret :: Uninterpreted a => String -> a
-- | Uninterpret a value, only for the purposes of code-generation. For
-- execution and verification the value is used as is. For
-- code-generation, the alternate definition is used. This is useful when
-- we want to take advantage of native libraries on the target languages.
cgUninterpret :: Uninterpreted a => String -> [String] -> a -> a
-- | Most generalized form of uninterpretation, this function should not be
-- needed by end-user-code, but is rather useful for the library
-- development.
sbvUninterpret :: Uninterpreted a => Maybe ([String], a) -> String -> a
-- | Add a user specified axiom to the generated SMT-Lib file. The first
-- argument is a mere string, use for commenting purposes. The second
-- argument is intended to hold the multiple-lines of the axiom text as
-- expressed in SMT-Lib notation. Note that we perform no checks on the
-- axiom itself, to see whether it's actually well-formed or is sensical
-- by any means. A separate formalization of SMT-Lib would be very useful
-- here.
addAxiom :: String -> [String] -> Symbolic ()
-- | Symbolic Equality. Note that we can't use Haskell's Eq class
-- since Haskell insists on returning Bool Comparing symbolic values will
-- necessarily return a symbolic value.
class EqSymbolic a
-- | Symbolic equality.
(.==) :: EqSymbolic a => a -> a -> SBool
-- | Symbolic inequality.
(./=) :: EqSymbolic a => a -> a -> SBool
-- | Returns (symbolic) true if all the elements of the given list are
-- different.
distinct :: EqSymbolic a => [a] -> SBool
-- | Returns (symbolic) true if all the elements of the given list are the
-- same.
allEqual :: EqSymbolic a => [a] -> SBool
-- | Symbolic membership test.
sElem :: EqSymbolic a => a -> [a] -> SBool
-- | Symbolic Comparisons. Similar to Eq, we cannot implement
-- Haskell's Ord class since there is no way to return an
-- Ordering value from a symbolic comparison. Furthermore,
-- OrdSymbolic requires Mergeable to implement
-- if-then-else, for the benefit of implementing symbolic versions of
-- max and min functions.
class (Mergeable a, EqSymbolic a) => OrdSymbolic a
-- | Symbolic less than.
(.<) :: OrdSymbolic a => a -> a -> SBool
-- | Symbolic less than or equal to.
(.<=) :: OrdSymbolic a => a -> a -> SBool
-- | Symbolic greater than.
(.>) :: OrdSymbolic a => a -> a -> SBool
-- | Symbolic greater than or equal to.
(.>=) :: OrdSymbolic a => a -> a -> SBool
-- | Symbolic minimum.
smin :: OrdSymbolic a => a -> a -> a
-- | Symbolic maximum.
smax :: OrdSymbolic a => a -> a -> a
-- | Is the value withing the allowed inclusive range?
inRange :: OrdSymbolic a => a -> (a, a) -> SBool
-- | Equality as a proof method. Allows for very concise construction of
-- equivalence proofs, which is very typical in bit-precise proofs.
class Equality a
(===) :: Equality a => a -> a -> IO ThmResult
-- | Add a constraint, any satisfying instance must satisfy this condition
constrain :: SolverContext m => SBool -> m ()
-- | Add a named constraint. The name is used in unsat-core extraction.
namedConstraint :: SolverContext m => String -> SBool -> m ()
-- | true if at most k of the input arguments are
-- true
pbAtMost :: [SBool] -> Int -> SBool
-- | true if at least k of the input arguments are
-- true
pbAtLeast :: [SBool] -> Int -> SBool
-- | true if exactly k of the input arguments are
-- true
pbExactly :: [SBool] -> Int -> SBool
-- | true if the sum of coefficients for true elements is at
-- most k. Generalizes pbAtMost.
pbLe :: [(Int, SBool)] -> Int -> SBool
-- | true if the sum of coefficients for true elements is at
-- least k. Generalizes pbAtLeast.
pbGe :: [(Int, SBool)] -> Int -> SBool
-- | true if the sum of coefficients for true elements is
-- exactly least k. Useful for coding exactly K-of-N
-- constraints, and in particular mutex constraints.
pbEq :: [(Int, SBool)] -> Int -> SBool
-- | true if there is at most one set bit
pbMutexed :: [SBool] -> SBool
-- | true if there is exactly one set bit
pbStronglyMutexed :: [SBool] -> SBool
-- | Make an enumeration a symbolic type.
mkSymbolicEnumeration :: Name -> Q [Dec]
-- | A predicate is a symbolic program that returns a (symbolic) boolean
-- value. For all intents and purposes, it can be treated as an n-ary
-- function from symbolic-values to a boolean. The Symbolic monad
-- captures the underlying representation, and can/should be ignored by
-- the users of the library, unless you are building further utilities on
-- top of SBV itself. Instead, simply use the Predicate type when
-- necessary.
type Predicate = Symbolic SBool
-- | A goal is a symbolic program that returns no values. The idea is that
-- the constraints/min-max goals will serve as appropriate directives for
-- sat/prove calls.
type Goal = Symbolic ()
-- | A type a is provable if we can turn it into a predicate. Note
-- that a predicate can be made from a curried function of arbitrary
-- arity, where each element is either a symbolic type or up-to a 7-tuple
-- of symbolic-types. So predicates can be constructed from almost
-- arbitrary Haskell functions that have arbitrary shapes. (See the
-- instance declarations below.)
class Provable a
-- | Turns a value into a universally quantified predicate, internally
-- naming the inputs. In this case the sbv library will use names of the
-- form s1, s2, etc. to name these variables Example:
--
--
-- forAll_ $ \(x::SWord8) y -> x `shiftL` 2 .== y
--
--
-- is a predicate with two arguments, captured using an ordinary Haskell
-- function. Internally, x will be named s0 and
-- y will be named s1.
forAll_ :: Provable a => a -> Predicate
-- | Turns a value into a predicate, allowing users to provide names for
-- the inputs. If the user does not provide enough number of names for
-- the variables, the remaining ones will be internally generated. Note
-- that the names are only used for printing models and has no other
-- significance; in particular, we do not check that they are unique.
-- Example:
--
--
-- forAll ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y
--
--
-- This is the same as above, except the variables will be named
-- x and y respectively, simplifying the
-- counter-examples when they are printed.
forAll :: Provable a => [String] -> a -> Predicate
-- | Turns a value into an existentially quantified predicate. (Indeed,
-- exists would have been a better choice here for the name, but
-- alas it's already taken.)
forSome_ :: Provable a => a -> Predicate
-- | Version of forSome that allows user defined names.
forSome :: Provable a => [String] -> a -> Predicate
-- | Prove a predicate, using the default solver.
prove :: Provable a => a -> IO ThmResult
-- | Prove the predicate using the given SMT-solver.
proveWith :: Provable a => SMTConfig -> a -> IO ThmResult
-- | Find a satisfying assignment for a predicate, using the default
-- solver.
sat :: Provable a => a -> IO SatResult
-- | Find a satisfying assignment using the given SMT-solver.
satWith :: Provable a => SMTConfig -> a -> IO SatResult
-- | Find all satisfying assignments, using the default solver. See
-- allSatWith for details.
allSat :: Provable a => a -> IO AllSatResult
-- | Return all satisfying assignments for a predicate, equivalent to
-- allSatWith defaultSMTCfg. Note that this call
-- will block until all satisfying assignments are found. If you have a
-- problem with infinitely many satisfying models (consider
-- SInteger) or a very large number of them, you might have to
-- wait for a long time. To avoid such cases, use the
-- allSatMaxModelCount parameter in the configuration.
--
-- NB. Uninterpreted constant/function values and counter-examples for
-- array values are ignored for the purposes of allSat.
-- That is, only the satisfying assignments modulo uninterpreted
-- functions and array inputs will be returned. This is due to the
-- limitation of not having a robust means of getting a function
-- counter-example back from the SMT solver. Find all satisfying
-- assignments using the given SMT-solver
allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult
-- | Optimize a given collection of Objectives
optimize :: Provable a => OptimizeStyle -> a -> IO OptimizeResult
-- | Optimizes the objectives using the given SMT-solver.
optimizeWith :: Provable a => SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult
-- | Check if the constraints given are consistent, using the default
-- solver.
isVacuous :: Provable a => a -> IO Bool
-- | Determine if the constraints are vacuous using the given SMT-solver.
isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool
-- | Checks theoremhood using the default solver.
isTheorem :: Provable a => a -> IO Bool
-- | Check whether a given property is a theorem.
isTheoremWith :: Provable a => SMTConfig -> a -> IO Bool
-- | Checks satisfiability using the default solver.
isSatisfiable :: Provable a => a -> IO Bool
-- | Check whether a given property is satisfiable.
isSatisfiableWith :: Provable a => SMTConfig -> a -> IO Bool
-- | Prove a property with multiple solvers, running them in separate
-- threads. The results will be returned in the order produced.
proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
-- | Prove a property with multiple solvers, running them in separate
-- threads. Only the result of the first one to finish will be returned,
-- remaining threads will be killed. Note that we send a
-- ThreadKilled to the losing processes, but we do *not*
-- actually wait for them to finish. In rare cases this can lead to
-- zombie processes. In previous experiments, we found that some
-- processes take their time to terminate. So, this solution favors quick
-- turnaround.
proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
-- | Find a satisfying assignment to a property with multiple solvers,
-- running them in separate threads. The results will be returned in the
-- order produced.
satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
-- | Find a satisfying assignment to a property with multiple solvers,
-- running them in separate threads. Only the result of the first one to
-- finish will be returned, remaining threads will be killed. Note that
-- we send a ThreadKilled to the losing processes, but we do
-- *not* actually wait for them to finish. In rare cases this can lead to
-- zombie processes. In previous experiments, we found that some
-- processes take their time to terminate. So, this solution favors quick
-- turnaround.
satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
-- | Create an SMT-Lib2 benchmark. The Bool argument controls
-- whether this is a SAT instance, i.e., translate the query directly, or
-- a PROVE instance, i.e., translate the negated query.
generateSMTBenchmark :: Provable a => Bool -> a -> IO String
-- | Symbolic assert. Check that the given boolean condition is always true
-- in the given path. The optional first argument can be used to provide
-- call-stack info via GHC's location facilities.
sAssert :: Maybe CallStack -> String -> SBool -> SBV a -> SBV a
-- | Check if a safe-call was safe or not, turning a SafeResult to a
-- Bool.
isSafe :: SafeResult -> Bool
-- | Symbolically executable program fragments. This class is mainly used
-- for safe calls, and is sufficently populated internally to
-- cover most use cases. Users can extend it as they wish to allow
-- safe checks for SBV programs that return/take types that are
-- user-defined.
class SExecutable a
sName_ :: SExecutable a => a -> Symbolic ()
sName :: SExecutable a => [String] -> a -> Symbolic ()
-- | Check safety using the default solver.
safe :: SExecutable a => a -> IO [SafeResult]
-- | Check if any of the sAssert calls can be violated.
safeWith :: SExecutable a => SMTConfig -> a -> IO [SafeResult]
-- | Form the symbolic conjunction of a given list of boolean conditions.
-- Useful in expressing problems with constraints, like the following:
--
--
-- do [x, y, z] <- sIntegers ["x", "y", "z"]
-- solve [x .> 5, y + z .< x]
--
solve :: [SBool] -> Symbolic SBool
-- | Quick check an SBV property. Note that a regular quickCheck
-- call will work just as well. Use this variant if you want to receive
-- the boolean result.
sbvQuickCheck :: Symbolic SBool -> IO Bool
-- | Run an arbitrary symbolic computation, equivalent to
-- runSMTWith defaultSMTCfg
runSMT :: Symbolic a -> IO a
-- | Runs an arbitrary symbolic computation, exposed to the user in SAT
-- mode
runSMTWith :: SMTConfig -> Symbolic a -> IO a
-- | Style of optimization. Note that in the pareto case the user is
-- allowed to specify a max number of fronts to query the solver for,
-- since there might potentially be an infinite number of them and there
-- is no way to know exactly how many ahead of time. If Nothing is
-- given, SBV will possibly loop forever if the number is really
-- infinite.
data OptimizeStyle
-- | Objectives are optimized in the order given, earlier objectives have
-- higher priority. This is the default.
Lexicographic :: OptimizeStyle
-- | Each objective is optimized independently.
Independent :: OptimizeStyle
-- | Objectives are optimized according to pareto front: That is, no
-- objective can be made better without making some other worse.
Pareto :: (Maybe Int) -> OptimizeStyle
-- | Penalty for a soft-assertion. The default penalty is 1, with
-- all soft-assertions belonging to the same objective goal. A positive
-- weight and an optional group can be provided by using the
-- Penalty constructor.
data Penalty
-- | Default: Penalty of 1 and no group attached
DefaultPenalty :: Penalty
-- | Penalty with a weight and an optional group
Penalty :: Rational -> (Maybe String) -> Penalty
-- | Objective of optimization. We can minimize, maximize, or give a soft
-- assertion with a penalty for not satisfying it.
data Objective a
-- | Minimize this metric
Minimize :: String -> a -> Objective a
-- | Maximize this metric
Maximize :: String -> a -> Objective a
-- | A soft assertion, with an associated penalty
AssertSoft :: String -> a -> Penalty -> Objective a
-- | Minimize a named metric
minimize :: Metric a => String -> a -> Symbolic ()
-- | Maximize a named metric
maximize :: Metric a => String -> a -> Symbolic ()
-- | Introduce a soft assertion, with an optional penalty
assertSoft :: String -> SBool -> Penalty -> Symbolic ()
-- | A simple expression type over extendent values, covering infinity,
-- epsilon and intervals.
data ExtCW
Infinite :: Kind -> ExtCW
Epsilon :: Kind -> ExtCW
Interval :: ExtCW -> ExtCW -> ExtCW
BoundedCW :: CW -> ExtCW
AddExtCW :: ExtCW -> ExtCW -> ExtCW
MulExtCW :: ExtCW -> ExtCW -> ExtCW
-- | A generalized CW allows for expressions involving infinite and epsilon
-- values/intervals Used in optimization problems.
data GeneralizedCW
ExtendedCW :: ExtCW -> GeneralizedCW
RegularCW :: CW -> GeneralizedCW
-- | A prove call results in a ThmResult
newtype ThmResult
ThmResult :: SMTResult -> ThmResult
-- | A sat call results in a SatResult The reason for
-- having a separate SatResult is to have a more meaningful
-- Show instance.
newtype SatResult
SatResult :: SMTResult -> SatResult
-- | An allSat call results in a AllSatResult. The first
-- boolean says whether we hit the max-model limit as we searched. The
-- second boolean says whether there were prefix-existentials.
newtype AllSatResult
AllSatResult :: (Bool, Bool, [SMTResult]) -> AllSatResult
-- | A safe call results in a SafeResult
newtype SafeResult
SafeResult :: (Maybe String, String, SMTResult) -> SafeResult
-- | An optimize call results in a OptimizeResult. In the
-- ParetoResult case, the boolean is True if we reached
-- pareto-query limit and so there might be more unqueried results
-- remaining. If False, it means that we have all the pareto
-- fronts returned. See the Pareto OptimizeStyle for
-- details.
data OptimizeResult
LexicographicResult :: SMTResult -> OptimizeResult
ParetoResult :: (Bool, [SMTResult]) -> OptimizeResult
IndependentResult :: [(String, SMTResult)] -> OptimizeResult
-- | The result of an SMT solver call. Each constructor is tagged with the
-- SMTConfig that created it so that further tools can inspect it
-- and build layers of results, if needed. For ordinary uses of the
-- library, this type should not be needed, instead use the accessor
-- functions on it. (Custom Show instances and model extractors.)
data SMTResult
-- | Unsatisfiable
Unsatisfiable :: SMTConfig -> SMTResult
-- | Satisfiable with model
Satisfiable :: SMTConfig -> SMTModel -> SMTResult
-- | Prover returned a model, but in an extension field containing
-- Infinite/epsilon
SatExtField :: SMTConfig -> SMTModel -> SMTResult
-- | Prover returned unknown, with the given reason
Unknown :: SMTConfig -> String -> SMTResult
-- | Prover errored out
ProofError :: SMTConfig -> [String] -> SMTResult
-- | A class of floating-point (IEEE754) operations, some of which behave
-- differently based on rounding modes. Note that unless the rounding
-- mode is concretely RoundNearestTiesToEven, we will not concretely
-- evaluate these, but rather pass down to the SMT solver.
class (SymWord a, RealFloat a) => IEEEFloating a
-- | Compute the floating point absolute value.
fpAbs :: IEEEFloating a => SBV a -> SBV a
-- | Compute the unary negation. Note that 0 - x is not equivalent
-- to -x for floating-point, since -0 and 0
-- are different.
fpNeg :: IEEEFloating a => SBV a -> SBV a
-- | Add two floating point values, using the given rounding mode
fpAdd :: IEEEFloating a => SRoundingMode -> SBV a -> SBV a -> SBV a
-- | Subtract two floating point values, using the given rounding mode
fpSub :: IEEEFloating a => SRoundingMode -> SBV a -> SBV a -> SBV a
-- | Multiply two floating point values, using the given rounding mode
fpMul :: IEEEFloating a => SRoundingMode -> SBV a -> SBV a -> SBV a
-- | Divide two floating point values, using the given rounding mode
fpDiv :: IEEEFloating a => SRoundingMode -> SBV a -> SBV a -> SBV a
-- | Fused-multiply-add three floating point values, using the given
-- rounding mode. fpFMA x y z = x*y+z but with only one rounding
-- done for the whole operation; not two. Note that we will never
-- concretely evaluate this function since Haskell lacks an FMA
-- implementation.
fpFMA :: IEEEFloating a => SRoundingMode -> SBV a -> SBV a -> SBV a -> SBV a
-- | Compute the square-root of a float, using the given rounding mode
fpSqrt :: IEEEFloating a => SRoundingMode -> SBV a -> SBV a
-- | Compute the remainder: x - y * n, where n is the
-- truncated integer nearest to x/y. The rounding mode is implicitly
-- assumed to be RoundNearestTiesToEven.
fpRem :: IEEEFloating a => SBV a -> SBV a -> SBV a
-- | Round to the nearest integral value, using the given rounding mode.
fpRoundToIntegral :: IEEEFloating a => SRoundingMode -> SBV a -> SBV a
-- | Compute the minimum of two floats, respects infinity and
-- NaN values
fpMin :: IEEEFloating a => SBV a -> SBV a -> SBV a
-- | Compute the maximum of two floats, respects infinity and
-- NaN values
fpMax :: IEEEFloating a => SBV a -> SBV a -> SBV a
-- | Are the two given floats exactly the same. That is, NaN will
-- compare equal to itself, +0 will not compare equal to
-- -0 etc. This is the object level equality, as opposed to the
-- semantic equality. (For the latter, just use .==.)
fpIsEqualObject :: IEEEFloating a => SBV a -> SBV a -> SBool
-- | Is the floating-point number a normal value. (i.e., not denormalized.)
fpIsNormal :: IEEEFloating a => SBV a -> SBool
-- | Is the floating-point number a subnormal value. (Also known as
-- denormal.)
fpIsSubnormal :: IEEEFloating a => SBV a -> SBool
-- | Is the floating-point number 0? (Note that both +0 and -0 will satisfy
-- this predicate.)
fpIsZero :: IEEEFloating a => SBV a -> SBool
-- | Is the floating-point number infinity? (Note that both +oo and -oo
-- will satisfy this predicate.)
fpIsInfinite :: IEEEFloating a => SBV a -> SBool
-- | Is the floating-point number a NaN value?
fpIsNaN :: IEEEFloating a => SBV a -> SBool
-- | Is the floating-point number negative? Note that -0 satisfies this
-- predicate but +0 does not.
fpIsNegative :: IEEEFloating a => SBV a -> SBool
-- | Is the floating-point number positive? Note that +0 satisfies this
-- predicate but -0 does not.
fpIsPositive :: IEEEFloating a => SBV a -> SBool
-- | Is the floating point number -0?
fpIsNegativeZero :: IEEEFloating a => SBV a -> SBool
-- | Is the floating point number +0?
fpIsPositiveZero :: IEEEFloating a => SBV a -> SBool
-- | Is the floating-point number a regular floating point, i.e., not NaN,
-- nor +oo, nor -oo. Normals or denormals are allowed.
fpIsPoint :: IEEEFloating a => SBV a -> SBool
-- | Capture convertability from/to FloatingPoint representations NB.
-- fromSFloat and fromSDouble are underspecified when given
-- when given a NaN, +oo, or -oo value that
-- cannot be represented in the target domain. For these inputs, we
-- define the result to be +0, arbitrarily.
class IEEEFloatConvertable a
fromSFloat :: IEEEFloatConvertable a => SRoundingMode -> SFloat -> SBV a
toSFloat :: IEEEFloatConvertable a => SRoundingMode -> SBV a -> SFloat
fromSDouble :: IEEEFloatConvertable a => SRoundingMode -> SDouble -> SBV a
toSDouble :: IEEEFloatConvertable a => SRoundingMode -> SBV a -> SDouble
-- | Rounding mode to be used for the IEEE floating-point operations. Note
-- that Haskell's default is RoundNearestTiesToEven. If you use a
-- different rounding mode, then the counter-examples you get may not
-- match what you observe in Haskell.
data RoundingMode
-- | Round to nearest representable floating point value. If precisely at
-- half-way, pick the even number. (In this context, even means
-- the lowest-order bit is zero.)
RoundNearestTiesToEven :: RoundingMode
-- | Round to nearest representable floating point value. If precisely at
-- half-way, pick the number further away from 0. (That is, for positive
-- values, pick the greater; for negative values, pick the smaller.)
RoundNearestTiesToAway :: RoundingMode
-- | Round towards positive infinity. (Also known as rounding-up or
-- ceiling.)
RoundTowardPositive :: RoundingMode
-- | Round towards negative infinity. (Also known as rounding-down or
-- floor.)
RoundTowardNegative :: RoundingMode
-- | Round towards zero. (Also known as truncation.)
RoundTowardZero :: RoundingMode
-- | The symbolic variant of RoundingMode
type SRoundingMode = SBV RoundingMode
-- | Not-A-Number for Double and Float. Surprisingly, Haskell
-- Prelude doesn't have this value defined, so we provide it here.
nan :: Floating a => a
-- | Infinity for Double and Float. Surprisingly, Haskell
-- Prelude doesn't have this value defined, so we provide it here.
infinity :: Floating a => a
-- | Symbolic variant of Not-A-Number. This value will inhabit both
-- SDouble and SFloat.
sNaN :: (Floating a, SymWord a) => SBV a
-- | Symbolic variant of infinity. This value will inhabit both
-- SDouble and SFloat.
sInfinity :: (Floating a, SymWord a) => SBV a
-- | Symbolic variant of RoundNearestTiesToEven
sRoundNearestTiesToEven :: SRoundingMode
-- | Symbolic variant of RoundNearestTiesToAway
sRoundNearestTiesToAway :: SRoundingMode
-- | Symbolic variant of RoundNearestPositive
sRoundTowardPositive :: SRoundingMode
-- | Symbolic variant of RoundTowardNegative
sRoundTowardNegative :: SRoundingMode
-- | Symbolic variant of RoundTowardZero
sRoundTowardZero :: SRoundingMode
-- | Alias for sRoundNearestTiesToEven
sRNE :: SRoundingMode
-- | Alias for sRoundNearestTiesToAway
sRNA :: SRoundingMode
-- | Alias for sRoundTowardPositive
sRTP :: SRoundingMode
-- | Alias for sRoundTowardNegative
sRTN :: SRoundingMode
-- | Alias for sRoundTowardZero
sRTZ :: SRoundingMode
-- | Convert an SFloat to an SWord32, preserving the
-- bit-correspondence. Note that since the representation for
-- NaNs are not unique, this function will return a symbolic
-- value when given a concrete NaN.
--
-- Implementation note: Since there's no corresponding function in SMTLib
-- for conversion to bit-representation due to partiality, we use a
-- translation trick by allocating a new word variable, converting it to
-- float, and requiring it to be equivalent to the input. In
-- code-generation mode, we simply map it to a simple conversion.
sFloatAsSWord32 :: SFloat -> SWord32
-- | Reinterpret the bits in a 32-bit word as a single-precision floating
-- point number
sWord32AsSFloat :: SWord32 -> SFloat
-- | Convert an SDouble to an SWord64, preserving the
-- bit-correspondence. Note that since the representation for
-- NaNs are not unique, this function will return a symbolic
-- value when given a concrete NaN.
--
-- See the implementation note for sFloatAsSWord32, as it applies
-- here as well.
sDoubleAsSWord64 :: SDouble -> SWord64
-- | Reinterpret the bits in a 32-bit word as a single-precision floating
-- point number
sWord64AsSDouble :: SWord64 -> SDouble
-- | Extract the sign/exponent/mantissa of a single-precision float. The
-- output will have 8 bits in the second argument for exponent, and 23 in
-- the third for the mantissa.
blastSFloat :: SFloat -> (SBool, [SBool], [SBool])
-- | Extract the sign/exponent/mantissa of a single-precision float. The
-- output will have 11 bits in the second argument for exponent, and 52
-- in the third for the mantissa.
blastSDouble :: SDouble -> (SBool, [SBool], [SBool])
-- | Instances of SatModel can be automatically extracted from
-- models returned by the solvers. The idea is that the sbv
-- infrastructure provides a stream of CW's (constant-words)
-- coming from the solver, and the type a is interpreted based
-- on these constants. Many typical instances are already provided, so
-- new instances can be declared with relative ease.
--
-- Minimum complete definition: parseCWs
class SatModel a
-- | Given a sequence of constant-words, extract one instance of the type
-- a, returning the remaining elements untouched. If the next
-- element is not what's expected for this type you should return
-- Nothing
parseCWs :: SatModel a => [CW] -> Maybe (a, [CW])
-- | Given a parsed model instance, transform it using f, and
-- return the result. The default definition for this method should be
-- sufficient in most use cases.
cvtModel :: SatModel a => (a -> Maybe b) -> Maybe (a, [CW]) -> Maybe (b, [CW])
-- | Given a sequence of constant-words, extract one instance of the type
-- a, returning the remaining elements untouched. If the next
-- element is not what's expected for this type you should return
-- Nothing
parseCWs :: (SatModel a, Read a) => [CW] -> Maybe (a, [CW])
-- | Various SMT results that we can extract models out of.
class Modelable a
-- | Is there a model?
modelExists :: Modelable a => a -> Bool
-- | Extract assignments of a model, the result is a tuple where the first
-- argument (if True) indicates whether the model was "probable". (i.e.,
-- if the solver returned unknown.)
getModelAssignment :: (Modelable a, SatModel b) => a -> Either String (Bool, b)
-- | Extract a model dictionary. Extract a dictionary mapping the variables
-- to their respective values as returned by the SMT solver. Also see
-- getModelDictionaries.
getModelDictionary :: Modelable a => a -> Map String CW
-- | Extract a model value for a given element. Also see
-- getModelValues.
getModelValue :: (Modelable a, SymWord b) => String -> a -> Maybe b
-- | Extract a representative name for the model value of an uninterpreted
-- kind. This is supposed to correspond to the value as computed
-- internally by the SMT solver; and is unportable from solver to solver.
-- Also see getModelUninterpretedValues.
getModelUninterpretedValue :: Modelable a => String -> a -> Maybe String
-- | A simpler variant of getModelAssignment to get a model out
-- without the fuss.
extractModel :: (Modelable a, SatModel b) => a -> Maybe b
-- | Extract model objective values, for all optimization goals.
getModelObjectives :: Modelable a => a -> Map String GeneralizedCW
-- | Extract the value of an objective
getModelObjectiveValue :: Modelable a => String -> a -> Maybe GeneralizedCW
-- | Given an allSat call, we typically want to iterate over it
-- and print the results in sequence. The displayModels function
-- automates this task by calling disp on each result,
-- consecutively. The first Int argument to disp 'is the
-- current model number. The second argument is a tuple, where the first
-- element indicates whether the model is alleged (i.e., if the solver is
-- not sure, returing Unknown)
displayModels :: SatModel a => (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
-- | Return all the models from an allSat call, similar to
-- extractModel but is suitable for the case of multiple results.
extractModels :: SatModel a => AllSatResult -> [a]
-- | Get dictionaries from an all-sat call. Similar to
-- getModelDictionary.
getModelDictionaries :: AllSatResult -> [Map String CW]
-- | Extract value of a variable from an all-sat call. Similar to
-- getModelValue.
getModelValues :: SymWord b => String -> AllSatResult -> [Maybe b]
-- | Extract value of an uninterpreted variable from an all-sat call.
-- Similar to getModelUninterpretedValue.
getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
-- | Solver configuration. See also z3, yices,
-- cvc4, boolector, mathSAT, etc. 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 not
-- necessarily have finite decimal representations, and hence we have to
-- stop printing at some depth. It is important to emphasize that such
-- values always have infinite precision internally. The issue is merely
-- with how we print such an infinite precision value on the screen. The
-- field printRealPrec controls the printing precision, by
-- specifying the number of digits after the decimal point. The default
-- value is 16, but it can be set to any positive integer.
--
-- When printing, SBV will add the suffix ... at the and of a
-- real-value, if the given bound is not sufficient to represent the
-- real-value exactly. Otherwise, the number will be written out in
-- standard decimal notation. Note that SBV will always print the whole
-- value if it is precise (i.e., if it fits in a finite number of
-- digits), regardless of the precision limit. The limit only applies if
-- the representation of the real value is not finite, i.e., if it is not
-- rational.
--
-- The printBase field can be used to print numbers in base 2, 10,
-- or 16. If base 2 or 16 is used, then floating-point values will be
-- printed in their internal memory-layout format as well, which can come
-- in handy for bit-precise analysis.
data SMTConfig
SMTConfig :: Bool -> Timing -> Int -> Int -> String -> Maybe Int -> (String -> Bool) -> Maybe FilePath -> SMTLibVersion -> SMTSolver -> RoundingMode -> [SMTOption] -> Bool -> Maybe FilePath -> SMTConfig
-- | Debug mode
[verbose] :: SMTConfig -> Bool
-- | Print timing information on how long different phases took
-- (construction, solving, etc.)
[timing] :: SMTConfig -> Timing
-- | Print integral literals in this base (2, 10, and 16 are supported.)
[printBase] :: SMTConfig -> Int
-- | Print algebraic real values with this precision. (SReal, default: 16)
[printRealPrec] :: SMTConfig -> Int
-- | Usually "(check-sat)". However, users might tweak it based on solver
-- characteristics.
[satCmd] :: SMTConfig -> String
-- | In an allSat call, return at most this many models. If nothing, return
-- all.
[allSatMaxModelCount] :: SMTConfig -> Maybe Int
-- | When constructing a model, ignore variables whose name satisfy this
-- predicate. (Default: (const False), i.e., don't ignore anything)
[isNonModelVar] :: SMTConfig -> String -> Bool
-- | If Just, the entire interaction will be recorded as a playable file
-- (for debugging purposes mostly)
[transcript] :: SMTConfig -> Maybe FilePath
-- | What version of SMT-lib we use for the tool
[smtLibVersion] :: SMTConfig -> SMTLibVersion
-- | The actual SMT solver.
[solver] :: SMTConfig -> SMTSolver
-- | Rounding mode to use for floating-point conversions
[roundingMode] :: SMTConfig -> RoundingMode
-- | Options to set as we start the solver
[solverSetOptions] :: SMTConfig -> [SMTOption]
-- | If true, we shall ignore the exit code upon exit. Otherwise we require
-- ExitSuccess.
[ignoreExitCode] :: SMTConfig -> Bool
-- | Redirect the verbose output to this file if given. If Nothing, stdout
-- is implied.
[redirectVerbose] :: SMTConfig -> Maybe FilePath
-- | Specify how to save timing information, if at all.
data Timing
NoTiming :: Timing
PrintTiming :: Timing
SaveTiming :: (IORef NominalDiffTime) -> Timing
-- | Representation of SMTLib Program versions. As of June 2015, we're
-- dropping support for SMTLib1, and supporting SMTLib2 only. We keep
-- this data-type around in case SMTLib3 comes along and we want to
-- support 2 and 3 simultaneously.
data SMTLibVersion
SMTLib2 :: SMTLibVersion
-- | Solvers that SBV is aware of
data Solver
Z3 :: Solver
Yices :: Solver
Boolector :: Solver
CVC4 :: Solver
MathSAT :: Solver
ABC :: Solver
-- | An SMT solver
data SMTSolver
SMTSolver :: Solver -> String -> (SMTConfig -> [String]) -> SMTEngine -> SolverCapabilities -> SMTSolver
-- | The solver in use
[name] :: SMTSolver -> Solver
-- | The path to its executable
[executable] :: SMTSolver -> String
-- | Options to provide to the solver
[options] :: SMTSolver -> SMTConfig -> [String]
-- | The solver engine, responsible for interpreting solver output
[engine] :: SMTSolver -> SMTEngine
-- | Various capabilities of the solver
[capabilities] :: SMTSolver -> SolverCapabilities
-- | Default configuration for the Boolector SMT solver
boolector :: SMTConfig
-- | Default configuration for the CVC4 SMT Solver.
cvc4 :: SMTConfig
-- | Default configuration for the Yices SMT Solver.
yices :: SMTConfig
-- | Default configuration for the Z3 SMT solver
z3 :: SMTConfig
-- | Default configuration for the MathSAT SMT solver
mathSAT :: SMTConfig
-- | Default configuration for the ABC synthesis and verification tool.
abc :: SMTConfig
-- | The default configs corresponding to supported SMT solvers
defaultSolverConfig :: Solver -> SMTConfig
-- | The default solver used by SBV. This is currently set to z3.
defaultSMTCfg :: SMTConfig
-- | Check whether the given solver is installed and is ready to go. This
-- call does a simple call to the solver to ensure all is well.
sbvCheckSolverInstallation :: SMTConfig -> IO Bool
-- | Return the known available solver configs, installed on your machine.
sbvAvailableSolvers :: IO [SMTConfig]
-- | Set the logic.
setLogic :: SolverContext m => Logic -> m ()
-- | Set an option.
setOption :: SolverContext m => SMTOption -> m ()
-- | Set info. Example: setInfo ":status" ["unsat"].
setInfo :: SolverContext m => String -> [String] -> m ()
-- | Set a solver time-out value, in milli-seconds. This function
-- essentially translates to the SMTLib call (set-info :timeout
-- val), and your backend solver may or may not support it! The
-- amount given is in milliseconds. Also see the function
-- timeOut for finer level control of time-outs, directly from
-- SBV.
setTimeOut :: SolverContext m => Integer -> m ()
-- | A Symbolic computation. Represented by a reader monad carrying the
-- state of the computation, layered on top of IO for creating unique
-- references to hold onto intermediate results.
data Symbolic a
-- | Mark an interim result as an output. Useful when constructing Symbolic
-- programs that return multiple values, or when the result is
-- programmatically computed.
output :: Outputtable a => a -> Symbolic a
-- | A SymWord is a potential symbolic bitvector that can be created
-- instances of to be fed to a symbolic program. Note that these methods
-- are typically not needed in casual uses with prove,
-- sat, allSat etc, as default instances automatically
-- provide the necessary bits.
class (HasKind a, Ord a) => SymWord a
-- | Create a user named input (universal)
forall :: SymWord a => String -> Symbolic (SBV a)
-- | Create an automatically named input
forall_ :: SymWord a => Symbolic (SBV a)
-- | Get a bunch of new words
mkForallVars :: SymWord a => Int -> Symbolic [SBV a]
-- | Create an existential variable
exists :: SymWord a => String -> Symbolic (SBV a)
-- | Create an automatically named existential variable
exists_ :: SymWord a => Symbolic (SBV a)
-- | Create a bunch of existentials
mkExistVars :: SymWord a => Int -> Symbolic [SBV a]
-- | Create a free variable, universal in a proof, existential in sat
free :: SymWord a => String -> Symbolic (SBV a)
-- | Create an unnamed free variable, universal in proof, existential in
-- sat
free_ :: SymWord a => Symbolic (SBV a)
-- | Create a bunch of free vars
mkFreeVars :: SymWord a => Int -> Symbolic [SBV a]
-- | Similar to free; Just a more convenient name
symbolic :: SymWord a => String -> Symbolic (SBV a)
-- | Similar to mkFreeVars; but automatically gives names based on the
-- strings
symbolics :: SymWord a => [String] -> Symbolic [SBV a]
-- | Turn a literal constant to symbolic
literal :: SymWord a => a -> SBV a
-- | Extract a literal, if the value is concrete
unliteral :: SymWord a => SBV a -> Maybe a
-- | Extract a literal, from a CW representation
fromCW :: SymWord a => CW -> a
-- | Is the symbolic word concrete?
isConcrete :: SymWord a => SBV a -> Bool
-- | Is the symbolic word really symbolic?
isSymbolic :: SymWord a => SBV a -> Bool
-- | Does it concretely satisfy the given predicate?
isConcretely :: SymWord a => SBV a -> (a -> Bool) -> Bool
-- | One stop allocator
mkSymWord :: SymWord a => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
-- | Turn a literal constant to symbolic
literal :: (SymWord a, Show a) => a -> SBV a
-- | Extract a literal, from a CW representation
fromCW :: (SymWord a, Read a) => CW -> a
-- | One stop allocator
mkSymWord :: (SymWord a, Read a, Data a) => Maybe Quantifier -> Maybe String -> Symbolic (SBV a)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality (Data.SBV.Core.Data.SBV a -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality (Data.SBV.Core.Data.SBV a -> Data.SBV.Core.Data.SBV b -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality ((Data.SBV.Core.Data.SBV a, Data.SBV.Core.Data.SBV b) -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality (Data.SBV.Core.Data.SBV a -> Data.SBV.Core.Data.SBV b -> Data.SBV.Core.Data.SBV c -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality ((Data.SBV.Core.Data.SBV a, Data.SBV.Core.Data.SBV b, Data.SBV.Core.Data.SBV c) -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Data.SymWord d, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality (Data.SBV.Core.Data.SBV a -> Data.SBV.Core.Data.SBV b -> Data.SBV.Core.Data.SBV c -> Data.SBV.Core.Data.SBV d -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Data.SymWord d, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality ((Data.SBV.Core.Data.SBV a, Data.SBV.Core.Data.SBV b, Data.SBV.Core.Data.SBV c, Data.SBV.Core.Data.SBV d) -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Data.SymWord d, Data.SBV.Core.Data.SymWord e, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality (Data.SBV.Core.Data.SBV a -> Data.SBV.Core.Data.SBV b -> Data.SBV.Core.Data.SBV c -> Data.SBV.Core.Data.SBV d -> Data.SBV.Core.Data.SBV e -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Data.SymWord d, Data.SBV.Core.Data.SymWord e, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality ((Data.SBV.Core.Data.SBV a, Data.SBV.Core.Data.SBV b, Data.SBV.Core.Data.SBV c, Data.SBV.Core.Data.SBV d, Data.SBV.Core.Data.SBV e) -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Data.SymWord d, Data.SBV.Core.Data.SymWord e, Data.SBV.Core.Data.SymWord f, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality (Data.SBV.Core.Data.SBV a -> Data.SBV.Core.Data.SBV b -> Data.SBV.Core.Data.SBV c -> Data.SBV.Core.Data.SBV d -> Data.SBV.Core.Data.SBV e -> Data.SBV.Core.Data.SBV f -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Data.SymWord d, Data.SBV.Core.Data.SymWord e, Data.SBV.Core.Data.SymWord f, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality ((Data.SBV.Core.Data.SBV a, Data.SBV.Core.Data.SBV b, Data.SBV.Core.Data.SBV c, Data.SBV.Core.Data.SBV d, Data.SBV.Core.Data.SBV e, Data.SBV.Core.Data.SBV f) -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Data.SymWord d, Data.SBV.Core.Data.SymWord e, Data.SBV.Core.Data.SymWord f, Data.SBV.Core.Data.SymWord g, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality (Data.SBV.Core.Data.SBV a -> Data.SBV.Core.Data.SBV b -> Data.SBV.Core.Data.SBV c -> Data.SBV.Core.Data.SBV d -> Data.SBV.Core.Data.SBV e -> Data.SBV.Core.Data.SBV f -> Data.SBV.Core.Data.SBV g -> z)
instance (Data.SBV.Core.Data.SymWord a, Data.SBV.Core.Data.SymWord b, Data.SBV.Core.Data.SymWord c, Data.SBV.Core.Data.SymWord d, Data.SBV.Core.Data.SymWord e, Data.SBV.Core.Data.SymWord f, Data.SBV.Core.Data.SymWord g, Data.SBV.Core.Model.EqSymbolic z) => Data.SBV.Equality ((Data.SBV.Core.Data.SBV a, Data.SBV.Core.Data.SBV b, Data.SBV.Core.Data.SBV c, Data.SBV.Core.Data.SBV d, Data.SBV.Core.Data.SBV e, Data.SBV.Core.Data.SBV f, Data.SBV.Core.Data.SBV g) -> z)
instance Data.SBV.Provers.Prover.Provable Data.SBV.Provers.Prover.Goal
-- | Demonstrates uninterpreted sorts and how all-sat behaves for them.
-- Thanks to Eric Seidel for the idea.
module Data.SBV.Examples.Uninterpreted.UISortAllSat
-- | A "list-like" data type, but one we plan to uninterpret at the SMT
-- level. The actual shape is really immaterial for us, but could be used
-- as a proxy to generate test cases or explore data-space in some other
-- part of a program. Note that we neither rely on the shape of this
-- data, nor need the actual constructors.
data L
Nil :: L
Cons :: Int -> L -> L
-- | Declare instances to make L a usable uninterpreted sort. First
-- we need the SymWord instance, with the default definition
-- sufficing.
-- | Similarly, HasKinds default implementation is sufficient.
-- | An uninterpreted "classify" function. Really, we only care about the
-- fact that such a function exists, not what it does.
classify :: SBV L -> SInteger
-- | Formulate a query that essentially asserts a cardinality constraint on
-- the uninterpreted sort L. The goal is to say there are
-- precisely 3 such things, as it might be the case. We manage this by
-- declaring four elements, and asserting that for a free variable of
-- this sort, the shape of the data matches one of these three instances.
-- That is, we assert that all the instances of the data L can be
-- classified into 3 equivalence classes. Then, allSat returns all the
-- possible instances, which of course are all uninterpreted.
--
-- As expected, we have:
--
--
-- >>> genLs
-- Solution #1:
-- l = L!val!0 :: L
-- l0 = L!val!0 :: L
-- l1 = L!val!1 :: L
-- l2 = L!val!2 :: L
-- Solution #2:
-- l = L!val!1 :: L
-- l0 = L!val!0 :: L
-- l1 = L!val!1 :: L
-- l2 = L!val!2 :: L
-- Solution #3:
-- l = L!val!2 :: L
-- l0 = L!val!0 :: L
-- l1 = L!val!1 :: L
-- l2 = L!val!2 :: L
-- Found 3 different solutions.
--
genLs :: IO AllSatResult
instance Data.Data.Data Data.SBV.Examples.Uninterpreted.UISortAllSat.L
instance GHC.Read.Read Data.SBV.Examples.Uninterpreted.UISortAllSat.L
instance GHC.Show.Show Data.SBV.Examples.Uninterpreted.UISortAllSat.L
instance GHC.Classes.Ord Data.SBV.Examples.Uninterpreted.UISortAllSat.L
instance GHC.Classes.Eq Data.SBV.Examples.Uninterpreted.UISortAllSat.L
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Uninterpreted.UISortAllSat.L
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Uninterpreted.UISortAllSat.L
-- | Demonstrates uninterpreted sorts, together with axioms.
module Data.SBV.Examples.Uninterpreted.Sort
-- | A new data-type that we expect to use in an uninterpreted fashion in
-- the backend SMT solver. Note the custom deriving clause,
-- which takes care of most of the boilerplate. The () field is needed so
-- SBV will not translate it to an enumerated data-type
newtype Q
Q :: () -> Q
-- | Declare an uninterpreted function that works over Q's
f :: SBV Q -> SBV Q
-- | A satisfiable example, stating that there is an element of the domain
-- Q such that f returns a different element. Note that
-- this is valid only when the domain Q has at least two elements.
-- We have:
--
--
-- >>> t1
-- Satisfiable. Model:
-- x = Q!val!0 :: Q
--
t1 :: IO SatResult
-- | This is a variant on the first example, except we also add an axiom
-- for the sort, stating that the domain Q has only one element.
-- In this case the problem naturally becomes unsat. We have:
--
--
-- >>> t2
-- Unsatisfiable
--
t2 :: IO SatResult
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Uninterpreted.Sort.Q
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Uninterpreted.Sort.Q
instance GHC.Show.Show Data.SBV.Examples.Uninterpreted.Sort.Q
instance GHC.Read.Read Data.SBV.Examples.Uninterpreted.Sort.Q
instance Data.Data.Data Data.SBV.Examples.Uninterpreted.Sort.Q
instance GHC.Classes.Ord Data.SBV.Examples.Uninterpreted.Sort.Q
instance GHC.Classes.Eq Data.SBV.Examples.Uninterpreted.Sort.Q
-- | Proves (instances of) Shannon's expansion theorem and other relevant
-- facts. See: http://en.wikipedia.org/wiki/Shannon's_expansion
module Data.SBV.Examples.Uninterpreted.Shannon
-- | A ternary boolean function
type Ternary = SBool -> SBool -> SBool -> SBool
-- | A binary boolean function
type Binary = SBool -> SBool -> SBool
-- | Positive Shannon cofactor of a boolean function, with respect to its
-- first argument
pos :: (SBool -> a) -> a
-- | Negative Shannon cofactor of a boolean function, with respect to its
-- first argument
neg :: (SBool -> a) -> a
-- | Shannon's expansion over the first argument of a function. We have:
--
--
-- >>> shannon
-- Q.E.D.
--
shannon :: IO ThmResult
-- | Alternative form of Shannon's expansion over the first argument of a
-- function. We have:
--
--
-- >>> shannon2
-- Q.E.D.
--
shannon2 :: IO ThmResult
-- | Computing the derivative of a boolean function (boolean difference).
-- Defined as exclusive-or of Shannon cofactors with respect to that
-- variable.
derivative :: Ternary -> Binary
-- | 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
-- | Universal quantification of a boolean function with respect to a
-- variable. Simply defined as the conjunction of the Shannon cofactors.
universal :: Ternary -> Binary
-- | 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
-- | Existential quantification of a boolean function with respect to a
-- variable. Simply defined as the conjunction of the Shannon cofactors.
existential :: Ternary -> Binary
-- | 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
-- | Demonstrates function counter-examples
module Data.SBV.Examples.Uninterpreted.Function
-- | An uninterpreted function
f :: SWord8 -> SWord8 -> SWord16
-- | Asserts that f x z == f (y+2) z whenever x == y+2.
-- Naturally correct:
--
--
-- >>> prove thmGood
-- Q.E.D.
--
thmGood :: SWord8 -> SWord8 -> SWord8 -> SBool
-- | Demonstrates uninterpreted sorts and how they can be used for
-- deduction. This example is inspired by the discussion at
-- http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3,
-- essentially showing how to show the required deduction using SBV.
module Data.SBV.Examples.Uninterpreted.Deduce
-- | The uninterpreted sort B, corresponding to the carrier. To
-- prevent SBV from translating it to an enumerated type, we simply
-- attach an unused field
newtype B
B :: () -> B
-- | Handy shortcut for the type of symbolic values over B
type SB = SBV B
-- | Uninterpreted logical connective and
and :: SB -> SB -> SB
-- | Uninterpreted logical connective or
or :: SB -> SB -> SB
-- | Uninterpreted logical connective not
not :: SB -> SB
-- | Distributivity of OR over AND, as an axiom in terms of the
-- uninterpreted functions we have introduced. Note how variables range
-- over the uninterpreted sort B.
ax1 :: [String]
-- | One of De Morgan's laws, again as an axiom in terms of our
-- uninterpeted logical connectives.
ax2 :: [String]
-- | Double negation axiom, similar to the above.
ax3 :: [String]
-- | Proves the equivalence NOT (p OR (q AND r)) == (NOT p AND NOT q)
-- OR (NOT p AND NOT r), following from the axioms we have specified
-- above. We have:
--
--
-- >>> test
-- Q.E.D.
--
test :: IO ThmResult
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Uninterpreted.Deduce.B
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Uninterpreted.Deduce.B
instance Data.Data.Data Data.SBV.Examples.Uninterpreted.Deduce.B
instance GHC.Read.Read Data.SBV.Examples.Uninterpreted.Deduce.B
instance GHC.Show.Show Data.SBV.Examples.Uninterpreted.Deduce.B
instance GHC.Classes.Ord Data.SBV.Examples.Uninterpreted.Deduce.B
instance GHC.Classes.Eq Data.SBV.Examples.Uninterpreted.Deduce.B
-- | Formalizes and proves the following theorem, about arithmetic,
-- uninterpreted functions, and arrays. (For reference, see
-- http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf
-- slide number 24):
--
--
-- x + 2 = y implies f (read (write (a, x, 3), y - 2)) = f (y - x + 1)
--
--
-- We interpret the types as follows (other interpretations certainly
-- possible):
--
--
-- - x SWord32 (32-bit unsigned address)
-- - y SWord32 (32-bit unsigned address)
-- - a An array, indexed by 32-bit addresses, returning
-- 32-bit unsigned integers
-- - f An uninterpreted function of type
-- SWord32 -> SWord64
--
--
-- The function read and write are usual array
-- operations.
module Data.SBV.Examples.Uninterpreted.AUF
-- | The array type, takes symbolic 32-bit unsigned indexes and stores
-- 32-bit unsigned symbolic values. These are functional arrays where
-- reading before writing a cell throws an exception.
type A = SFunArray Word32 Word32
-- | Uninterpreted function in the theorem
f :: SWord32 -> SWord64
-- | Correctness theorem. We state it for all values of x,
-- y, and the given array a.
thm1 :: SWord32 -> SWord32 -> A -> SBool
-- | Prints Q.E.D. when run, as expected
--
--
-- >>> proveThm1
-- Q.E.D.
--
proveThm1 :: IO ThmResult
-- | This version directly uses SMT-arrays and hence does not need an
-- initializer. Reading an element before writing to it returns an
-- arbitrary value.
type B = SArray Word32 Word32
-- | Same as thm1, except we don't need an initializer with the
-- SArray model.
thm2 :: SWord32 -> SWord32 -> B -> SBool
-- | Prints Q.E.D. when run, as expected:
--
--
-- >>> proveThm2
-- Q.E.D.
--
proveThm2 :: IO ThmResult
-- | Demonstrates extraction of unsat-cores via queries.
module Data.SBV.Examples.Queries.UnsatCore
-- | A simple goal with three constraints, two of which are conflicting
-- with each other. The third is irrelevant, in the sense that it does
-- not contribute to the fact that the goal is unsatisfiable.
p :: Symbolic (Maybe [String])
-- | Extract the unsat-core of p. We have:
--
--
-- >>> ucCore
-- Unsat core is: ["less than 5","more than 10"]
--
--
-- Demonstrating that the constraint a .> b is not
-- needed for unsatisfiablity in this case.
ucCore :: IO ()
-- | Demonstrates extraction of interpolants via queries.
module Data.SBV.Examples.Queries.Interpolants
-- | Compute the interpolant for formulas y = 2x and y =
-- 2z+1. These formulas are not satisfiable together since it would
-- mean y is both even and odd at the same time. An interpolant
-- for this pair of formulas is a formula that's expressed only in terms
-- of y, which is the only common symbol among them. We have:
--
--
-- >>> runSMT evenOdd
-- ["(<= 0 (+ (div s1 2) (div (* (- 1) s1) 2)))"]
--
--
-- This is a bit hard to read unfortunately, due to translation artifacts
-- and use of strings. To analyze, we need to know that s1 is
-- y through SBV's translation. Let's express it in regular
-- infix notation with y for s1:
--
--
-- 0 <= (y div 2) + ((-y) div 2)
--
--
-- Notice that the only symbol is y, as required. To establish
-- that this is indeed an interpolant, we should establish that when
-- y is even, this formula is True; and if y
-- is odd, then then it should be False. You can argue
-- mathematically that this indeed the case, but let's just use SBV to
-- prove these:
--
--
-- >>> prove $ \y -> (y `sMod` 2 .== 0) ==> (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))
-- Q.E.D.
--
--
-- And:
--
--
-- >>> prove $ \y -> (y `sMod` 2 .== 1) ==> bnot (0 .<= (y `sDiv` 2) + ((-y) `sDiv` 2::SInteger))
-- Q.E.D.
--
--
-- This establishes that we indeed have an interpolant!
evenOdd :: Symbolic [String]
-- | A simple number-guessing game implementation via queries. Clearly an
-- SMT solver is hardly needed for this problem, but it is a nice demo
-- for the interactive-query programming.
module Data.SBV.Examples.Queries.GuessNumber
-- | Use the backend solver to guess the number given as argument. The
-- number is assumed to be between 0 and 1000, and we
-- use a simple binary search. Returns the sequence of guesses we
-- performed during the search process.
guess :: Integer -> Symbolic [Integer]
-- | Play a round of the game, making the solver guess the secret number
-- 42. Note that you can generate a random-number and make the solver
-- guess it too! We have:
--
--
-- >>> play
-- Current bounds: (0,1000)
-- Current bounds: (0,521)
-- Current bounds: (21,521)
-- Current bounds: (31,521)
-- Current bounds: (36,521)
-- Current bounds: (39,521)
-- Current bounds: (40,521)
-- Current bounds: (41,521)
-- Current bounds: (42,521)
-- Solved in: 9 guesses:
-- 1000 0 21 31 36 39 40 41 42
--
play :: IO ()
-- | A query based solution to the four-fours puzzle. Inspired by
-- http://www.gigamonkeys.com/trees/
--
--
-- Try to make every number between 0 and 20 using only four 4s and any
-- mathematical operation, with all four 4s being used each time.
--
--
-- We pretty much follow the structure of
-- http://www.gigamonkeys.com/trees/, with the exception that we
-- generate the trees filled with symbolic operators and ask the SMT
-- solver to find the appropriate fillings.
module Data.SBV.Examples.Queries.FourFours
-- | Supported binary operators. To keep the search-space small, we will
-- only allow division by 2 or 4, and exponentiation
-- will only be to the power 0. This does restrict the search
-- space, but is sufficient to solve all the instances.
data BinOp
Plus :: BinOp
Minus :: BinOp
Times :: BinOp
Divide :: BinOp
Expt :: BinOp
-- | Make BinOp a symbolic value.
-- | Make BinOp a symbolic value.
-- | Make BinOp a symbolic value.
-- | Make BinOp a symbolic value.
-- | Make BinOp a symbolic value.
-- | Make BinOp a symbolic value.
-- | Make BinOp a symbolic value.
-- | Make BinOp a symbolic value.
-- | Make BinOp a symbolic value.
-- | Supported unary operators. Similar to BinOp case, we will
-- restrict square-root and factorial to be only applied to the value @4.
data UnOp
Negate :: UnOp
Sqrt :: UnOp
Factorial :: UnOp
-- | Make UnOp a symbolic value.
-- | Make UnOp a symbolic value.
-- | Make UnOp a symbolic value.
-- | Make UnOp a symbolic value.
-- | Make UnOp a symbolic value.
-- | Make UnOp a symbolic value.
-- | Make UnOp a symbolic value.
-- | Make UnOp a symbolic value.
-- | Make UnOp a symbolic value.
-- | Symbolic variant of BinOp.
type SBinOp = SBV BinOp
-- | Symbolic variant of UnOp.
type SUnOp = SBV UnOp
-- | The shape of a tree, either a binary node, or a unary node, or the
-- number 4, represented hear by the constructor F. We
-- parameterize by the operator type: When doing symbolic computations,
-- we'll fill those with SBinOp and SUnOp. When finding the
-- shapes, we will simply put unit values, i.e., holes.
data T b u
B :: b -> (T b u) -> (T b u) -> T b u
U :: u -> (T b u) -> T b u
F :: T b u
-- | A rudimentary Show instance for trees, nothing fancy.
-- | Construct all possible tree shapes. The argument here follows the
-- logic in http://www.gigamonkeys.com/trees/: We simply construct
-- all possible shapes and extend with the operators. The number of such
-- trees is:
--
--
-- >>> length allPossibleTrees
-- 640
--
--
-- Note that this is a lot smaller than what is generated by
-- http://www.gigamonkeys.com/trees/. (There, the number of trees
-- is 10240000: 16000 times more than what we have to consider!)
allPossibleTrees :: [T () ()]
-- | Given a tree with hols, fill it with symbolic operators. This is the
-- trick that allows us to consider only 640 trees as opposed to
-- over 10 million.
fill :: T () () -> Symbolic (T SBinOp SUnOp)
-- | Minor helper for writing "symbolic" case statements. Simply walks down
-- a list of values to match against a symbolic version of the key.
sCase :: (SymWord a, Mergeable v) => SBV a -> [(a, v)] -> v
-- | Evaluate a symbolic tree, obtaining a symbolic value. Note how we
-- structure this evaluation so we impose extra constraints on what
-- values square-root, divide etc. can take. This is the power of the
-- symbolic approach: We can put arbitrary symbolic constraints as we
-- evaluate the tree.
eval :: T SBinOp SUnOp -> Symbolic SInteger
-- | In the query mode, find a filling of a given tree shape t, such
-- that it evalutes to the requested number i. Note that we return
-- back a concrete tree.
generate :: Integer -> T () () -> IO (Maybe (T BinOp UnOp))
-- | Given an integer, walk through all possible tree shapes (at most 640
-- of them), and find a filling that solves the puzzle.
find :: Integer -> IO ()
-- | Solution to the puzzle. When you run this puzzle, the solver can
-- produce different results than what's shown here, but the expressions
-- should still be all valid!
--
--
-- ghci> puzzle
-- 0 [OK]: (4 - (4 + (4 - 4)))
-- 1 [OK]: (4 / (4 + (4 - 4)))
-- 2 [OK]: sqrt((4 + (4 * (4 - 4))))
-- 3 [OK]: (4 - (4 ^ (4 - 4)))
-- 4 [OK]: (4 + (4 * (4 - 4)))
-- 5 [OK]: (4 + (4 ^ (4 - 4)))
-- 6 [OK]: (4 + sqrt((4 * (4 / 4))))
-- 7 [OK]: (4 + (4 - (4 / 4)))
-- 8 [OK]: (4 - (4 - (4 + 4)))
-- 9 [OK]: (4 + (4 + (4 / 4)))
-- 10 [OK]: (4 + (4 + (4 - sqrt(4))))
-- 11 [OK]: (4 + ((4 + 4!) / 4))
-- 12 [OK]: (4 * (4 - (4 / 4)))
-- 13 [OK]: (4! + ((sqrt(4) - 4!) / sqrt(4)))
-- 14 [OK]: (4 + (4 + (4 + sqrt(4))))
-- 15 [OK]: (4 + ((4! - sqrt(4)) / sqrt(4)))
-- 16 [OK]: (4 * (4 * (4 / 4)))
-- 17 [OK]: (4 + ((sqrt(4) + 4!) / sqrt(4)))
-- 18 [OK]: -(4 + (4 - (sqrt(4) + 4!)))
-- 19 [OK]: -(4 - (4! - (4 / 4)))
-- 20 [OK]: (4 * (4 + (4 / 4)))
--
puzzle :: IO ()
instance GHC.Classes.Eq Data.SBV.Examples.Queries.FourFours.UnOp
instance GHC.Show.Show Data.SBV.Examples.Queries.FourFours.UnOp
instance GHC.Classes.Ord Data.SBV.Examples.Queries.FourFours.UnOp
instance GHC.Read.Read Data.SBV.Examples.Queries.FourFours.UnOp
instance Data.Data.Data Data.SBV.Examples.Queries.FourFours.UnOp
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Queries.FourFours.UnOp
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Queries.FourFours.UnOp
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Queries.FourFours.UnOp
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Queries.FourFours.UnOp
instance GHC.Show.Show (Data.SBV.Examples.Queries.FourFours.T Data.SBV.Examples.Queries.FourFours.BinOp Data.SBV.Examples.Queries.FourFours.UnOp)
instance GHC.Classes.Eq Data.SBV.Examples.Queries.FourFours.BinOp
instance GHC.Show.Show Data.SBV.Examples.Queries.FourFours.BinOp
instance GHC.Classes.Ord Data.SBV.Examples.Queries.FourFours.BinOp
instance GHC.Read.Read Data.SBV.Examples.Queries.FourFours.BinOp
instance Data.Data.Data Data.SBV.Examples.Queries.FourFours.BinOp
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Queries.FourFours.BinOp
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Queries.FourFours.BinOp
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Queries.FourFours.BinOp
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Queries.FourFours.BinOp
-- | Demonstrates the use of enumeration values during queries.
module Data.SBV.Examples.Queries.Enums
-- | Days of the week. We make it symbolic using the
-- mkSymbolicEnumeration splice.
data Day
Monday :: Day
Tuesday :: Day
Wednesday :: Day
Thursday :: Day
Friday :: Day
Saturday :: Day
Sunday :: Day
-- | Make Day a symbolic value.
-- | Make Day a symbolic value.
-- | Make Day a symbolic value.
-- | Make Day a symbolic value.
-- | Make Day a symbolic value.
-- | Make Day a symbolic value.
-- | Make Day a symbolic value.
-- | Make Day a symbolic value.
-- | Make Day a symbolic value.
-- | The type synonym SDay is the symbolic variant of Day.
-- (Similar to 'SInteger'/'Integer' and others.)
type SDay = SBV Day
-- | A trivial query to find three consecutive days that's all before
-- Thursday. The point here is that we can perform queries on such
-- enumerated values and use getValue on them and return their
-- values from queries just like any other value. We have:
--
--
-- >>> findDays
-- [Monday,Tuesday,Wednesday]
--
findDays :: IO [Day]
instance GHC.Classes.Eq Data.SBV.Examples.Queries.Enums.Day
instance GHC.Show.Show Data.SBV.Examples.Queries.Enums.Day
instance GHC.Classes.Ord Data.SBV.Examples.Queries.Enums.Day
instance GHC.Read.Read Data.SBV.Examples.Queries.Enums.Day
instance Data.Data.Data Data.SBV.Examples.Queries.Enums.Day
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Queries.Enums.Day
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Queries.Enums.Day
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Queries.Enums.Day
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Queries.Enums.Day
-- | A couple of demonstrations for the caseSplit tactic.
module Data.SBV.Examples.Queries.CaseSplit
-- | A simple floating-point problem, but we do the sat-analysis via a
-- case-split. Due to the nature of floating-point numbers, a case-split
-- on the characteristics of the number (such as NaN, negative-zero, etc.
-- is most suitable.)
--
-- We have: >>> csDemo1 Case fpIsNegativeZero: Starting Case
-- fpIsNegativeZero: Unsatisfiable Case fpIsPositiveZero: Starting Case
-- fpIsPositiveZero: Unsatisfiable Case fpIsNormal: Starting Case
-- fpIsNormal: Unsatisfiable Case fpIsSubnormal: Starting Case
-- fpIsSubnormal: Unsatisfiable Case fpIsPoint: Starting Case fpIsPoint:
-- Unsatisfiable Case fpIsNaN: Starting Case fpIsNaN: Satisfiable
-- ("fpIsNaN",NaN)
csDemo1 :: IO (String, Float)
-- | Demonstrates the "coverage" case.
--
-- We have: >>> csDemo2 Case negative: Starting Case negative:
-- Unsatisfiable Case less than 8: Starting Case less than 8:
-- Unsatisfiable Case Coverage: Starting Case Coverage: Satisfiable
-- (Coverage,10)
csDemo2 :: IO (String, Integer)
-- | When we would like to find all solutions to a problem, we can query
-- the solver repeatedly, telling it to give us a new model each time.
-- SBV already provides allSat that precisely does this. However,
-- this example demonstrates how the query mode can be used to achieve
-- the same, and can also incorporate extra conditions with easy as we
-- walk through solutions.
module Data.SBV.Examples.Queries.AllSat
-- | Find all solutions to x + y .== 10 for positive x
-- and y, but at each iteration we would like to ensure that the
-- value of x we get is at least twice as large as the previous
-- one. This is rather silly, but demonstrates how we can dynamically
-- query the result and put in new constraints based on those.
goodSum :: Symbolic [(Integer, Integer)]
-- | Run the query. We have:
--
--
-- >>> demo
-- Starting the all-sat engine!
-- Iteration: 1
-- Current solution is: (0,10)
-- Iteration: 2
-- Current solution is: (1,9)
-- Iteration: 3
-- Current solution is: (2,8)
-- Iteration: 4
-- Current solution is: (4,6)
-- Iteration: 5
-- Current solution is: (8,2)
-- Iteration: 6
-- No other solution!
-- [(0,10),(1,9),(2,8),(4,6),(8,2)]
--
demo :: IO ()
-- | The famous U2 bridge crossing puzzle:
-- http://www.braingle.com/brainteasers/515/u2.html
module Data.SBV.Examples.Puzzles.U2Bridge
-- | U2 band members. We want to translate this to SMT-Lib as a data-type,
-- and hence the call to mkSymbolicEnumeration.
data U2Member
Bono :: U2Member
Edge :: U2Member
Adam :: U2Member
Larry :: U2Member
-- | Make U2Member a symbolic value.
-- | Make U2Member a symbolic value.
-- | Make U2Member a symbolic value.
-- | Make U2Member a symbolic value.
-- | Make U2Member a symbolic value.
-- | Make U2Member a symbolic value.
-- | Make U2Member a symbolic value.
-- | Make U2Member a symbolic value.
-- | Make U2Member a symbolic value.
-- | Symbolic shorthand for a U2Member
type SU2Member = SBV U2Member
-- | Shorthands for symbolic versions of the members
bono :: SU2Member
-- | Shorthands for symbolic versions of the members
edge :: SU2Member
-- | Shorthands for symbolic versions of the members
adam :: SU2Member
-- | Shorthands for symbolic versions of the members
larry :: SU2Member
-- | Model time using 32 bits
type Time = Word32
-- | Symbolic variant for time
type STime = SBV Time
-- | Crossing times for each member of the band
crossTime :: U2Member -> Time
-- | The symbolic variant.. The duplication is unfortunate.
sCrossTime :: SU2Member -> STime
-- | Location of the flash
data Location
Here :: Location
There :: Location
-- | Make Location a symbolic value.
-- | Make Location a symbolic value.
-- | Make Location a symbolic value.
-- | Make Location a symbolic value.
-- | Make Location a symbolic value.
-- | Make Location a symbolic value.
-- | Make Location a symbolic value.
-- | Make Location a symbolic value.
-- | Make Location a symbolic value.
-- | Symbolic variant of Location
type SLocation = SBV Location
-- | Shorthands for symbolic versions of locations
here :: SLocation
-- | Shorthands for symbolic versions of locations
there :: SLocation
-- | The status of the puzzle after each move
--
-- This type is equipped with an automatically derived Mergeable
-- instance because each field is Mergeable. A Generic
-- instance must also be derived for this to work, and the
-- DeriveAnyClass language extension must be enabled. The
-- derived Mergeable instance simply walks down the structure
-- field by field and merges each one. An equivalent hand-written
-- Mergeable instance is provided in a comment below.
data Status
Status :: STime -> SLocation -> SLocation -> SLocation -> SLocation -> SLocation -> Status
-- | elapsed time
[time] :: Status -> STime
-- | location of the flash
[flash] :: Status -> SLocation
-- | location of Bono
[lBono] :: Status -> SLocation
-- | location of Edge
[lEdge] :: Status -> SLocation
-- | location of Adam
[lAdam] :: Status -> SLocation
-- | location of Larry
[lLarry] :: Status -> SLocation
-- | Start configuration, time elapsed is 0 and everybody is here
start :: Status
-- | A puzzle move is modeled as a state-transformer
type Move a = State Status a
-- | Mergeable instance for Move simply pushes the merging the data
-- after run of each branch starting from the same state.
-- | Read the state via an accessor function
peek :: (Status -> a) -> Move a
-- | Given an arbitrary member, return his location
whereIs :: SU2Member -> Move SLocation
-- | Transferring the flash to the other side
xferFlash :: Move ()
-- | Transferring a person to the other side
xferPerson :: SU2Member -> Move ()
-- | Increment the time, when only one person crosses
bumpTime1 :: SU2Member -> Move ()
-- | Increment the time, when two people cross together
bumpTime2 :: SU2Member -> SU2Member -> Move ()
-- | Symbolic version of when
whenS :: SBool -> Move () -> Move ()
-- | Move one member, remembering to take the flash
move1 :: SU2Member -> Move ()
-- | Move two members, again with the flash
move2 :: SU2Member -> SU2Member -> Move ()
-- | A move action is a sequence of triples. The first component is
-- symbolically True if only one member crosses. (In this case the third
-- element of the triple is irrelevant.) If the first component is
-- (symbolically) False, then both members move together
type Actions = [(SBool, SU2Member, SU2Member)]
-- | Run a sequence of given actions.
run :: Actions -> Move [Status]
-- | Check if a given sequence of actions is valid, i.e., they must all
-- cross the bridge according to the rules and in less than 17 seconds
isValid :: Actions -> SBool
-- | See if there is a solution that has precisely n steps
solveN :: Int -> IO Bool
-- | Solve the U2-bridge crossing puzzle, starting by testing solutions
-- with increasing number of steps, until we find one. We have:
--
--
-- >>> solveU2
-- Checking for solutions with 1 move.
-- Checking for solutions with 2 moves.
-- Checking for solutions with 3 moves.
-- Checking for solutions with 4 moves.
-- Checking for solutions with 5 moves.
-- Solution #1:
-- 0 --> Edge, Bono
-- 2 <-- Bono
-- 3 --> Larry, Adam
-- 13 <-- Edge
-- 15 --> Edge, Bono
-- Total time: 17
-- Solution #2:
-- 0 --> Edge, Bono
-- 2 <-- Edge
-- 4 --> Larry, Adam
-- 14 <-- Bono
-- 15 --> Edge, Bono
-- Total time: 17
-- Found: 2 solutions with 5 moves.
--
--
-- Finding all possible solutions to the puzzle.
solveU2 :: IO ()
instance Data.SBV.Core.Model.Mergeable Data.SBV.Examples.Puzzles.U2Bridge.Status
instance GHC.Generics.Generic Data.SBV.Examples.Puzzles.U2Bridge.Status
instance GHC.Classes.Eq Data.SBV.Examples.Puzzles.U2Bridge.Location
instance GHC.Show.Show Data.SBV.Examples.Puzzles.U2Bridge.Location
instance GHC.Classes.Ord Data.SBV.Examples.Puzzles.U2Bridge.Location
instance GHC.Read.Read Data.SBV.Examples.Puzzles.U2Bridge.Location
instance Data.Data.Data Data.SBV.Examples.Puzzles.U2Bridge.Location
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Puzzles.U2Bridge.Location
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Puzzles.U2Bridge.Location
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Puzzles.U2Bridge.Location
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Puzzles.U2Bridge.Location
instance Data.SBV.Core.Model.Mergeable a => Data.SBV.Core.Model.Mergeable (Data.SBV.Examples.Puzzles.U2Bridge.Move a)
instance GHC.Classes.Eq Data.SBV.Examples.Puzzles.U2Bridge.U2Member
instance GHC.Show.Show Data.SBV.Examples.Puzzles.U2Bridge.U2Member
instance GHC.Classes.Ord Data.SBV.Examples.Puzzles.U2Bridge.U2Member
instance GHC.Read.Read Data.SBV.Examples.Puzzles.U2Bridge.U2Member
instance Data.Data.Data Data.SBV.Examples.Puzzles.U2Bridge.U2Member
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Puzzles.U2Bridge.U2Member
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Puzzles.U2Bridge.U2Member
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Puzzles.U2Bridge.U2Member
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Puzzles.U2Bridge.U2Member
-- | The Sudoku solver, quintessential SMT solver example!
module Data.SBV.Examples.Puzzles.Sudoku
-- | A row is a sequence of 8-bit words, too large indeed for representing
-- 1-9, but does not harm
type Row = [SWord8]
-- | A Sudoku board is a sequence of 9 rows
type Board = [Row]
-- | Given a series of elements, make sure they are all different and they
-- all are numbers between 1 and 9
check :: [SWord8] -> SBool
-- | Given a full Sudoku board, check that it is valid
valid :: Board -> SBool
-- | A puzzle is a pair: First is the number of missing elements, second is
-- a function that given that many elements returns the final board.
type Puzzle = (Int, [SWord8] -> Board)
-- | Solve a given puzzle and print the results
sudoku :: Puzzle -> IO ()
-- | Helper function to display results nicely, not really needed, but
-- helps presentation
dispSolution :: Puzzle -> (Bool, [Word8]) -> IO ()
-- | Find all solutions to a puzzle
solveAll :: Puzzle -> IO ()
-- | Find an arbitrary good board
puzzle0 :: Puzzle
-- | A random puzzle, found on the internet..
puzzle1 :: Puzzle
-- | Another random puzzle, found on the internet..
puzzle2 :: Puzzle
-- | Another random puzzle, found on the internet..
puzzle3 :: Puzzle
-- | According to the web, this is the toughest sudoku puzzle ever.. It
-- even has a name: Al Escargot:
-- http://zonkedyak.blogspot.com/2006/11/worlds-hardest-sudoku-puzzle-al.html
puzzle4 :: Puzzle
-- | This one has been called diabolical, apparently
puzzle5 :: Puzzle
-- | The following is nefarious according to
-- http://haskell.org/haskellwiki/Sudoku
puzzle6 :: Puzzle
-- | Solve them all, this takes a fraction of a second to run for each case
allPuzzles :: IO ()
-- | Solves the classic send + more = money puzzle.
module Data.SBV.Examples.Puzzles.SendMoreMoney
-- | Solve the puzzle. We have:
--
--
-- >>> sendMoreMoney
-- Solution #1:
-- s = 9 :: Integer
-- e = 5 :: Integer
-- n = 6 :: Integer
-- d = 7 :: Integer
-- m = 1 :: Integer
-- o = 0 :: Integer
-- r = 8 :: Integer
-- y = 2 :: Integer
-- This is the only solution.
--
--
-- That is:
--
--
-- >>> 9567 + 1085 == 10652
-- True
--
sendMoreMoney :: IO AllSatResult
-- | Solves the NQueens puzzle:
-- http://en.wikipedia.org/wiki/Eight_queens_puzzle
module Data.SBV.Examples.Puzzles.NQueens
-- | A solution is a sequence of row-numbers where queens should be placed
type Solution = [SWord8]
-- | Checks that a given solution of n-queens is valid, i.e., no
-- queen captures any other.
isValid :: Int -> Solution -> SBool
-- | Given n, it solves the n-queens puzzle, printing all
-- possible solutions.
nQueens :: Int -> IO ()
-- | Solves the magic-square puzzle. An NxN magic square is one where all
-- entries are filled with numbers from 1 to NxN such that sums of all
-- rows, columns and diagonals is the same.
module Data.SBV.Examples.Puzzles.MagicSquare
-- | Use 32-bit words for elements.
type Elem = SWord32
-- | A row is a list of elements
type Row = [Elem]
-- | The puzzle board is a list of rows
type Board = [Row]
-- | Checks that all elements in a list are within bounds
check :: Elem -> Elem -> [Elem] -> SBool
-- | Get the diagonal of a square matrix
diag :: [[a]] -> [a]
-- | Test if a given board is a magic square
isMagic :: Board -> SBool
-- | Group a list of elements in the sublists of length i
chunk :: Int -> [a] -> [[a]]
-- | Given n, magic n prints all solutions to the
-- nxn magic square problem
magic :: Int -> IO ()
-- | Solves the following logic puzzle:
--
--
-- - The Briton lives in the red house.
-- - The Swede keeps dogs as pets.
-- - The Dane drinks tea.
-- - The green house is left to the white house.
-- - The owner of the green house drinks coffee.
-- - The person who plays football rears birds.
-- - The owner of the yellow house plays baseball.
-- - The man living in the center house drinks milk.
-- - The Norwegian lives in the first house.
-- - The man who plays volleyball lives next to the one who keeps
-- cats.
-- - The man who keeps the horse lives next to the one who plays
-- baseball.
-- - The owner who plays tennis drinks beer.
-- - The German plays hockey.
-- - The Norwegian lives next to the blue house.
-- - The man who plays volleyball has a neighbor who drinks water.
--
--
-- Who owns the fish?
module Data.SBV.Examples.Puzzles.Fish
-- | Colors of houses
data Color
Red :: Color
Green :: Color
White :: Color
Yellow :: Color
Blue :: Color
-- | Make Color a symbolic value.
-- | Make Color a symbolic value.
-- | Make Color a symbolic value.
-- | Make Color a symbolic value.
-- | Make Color a symbolic value.
-- | Make Color a symbolic value.
-- | Make Color a symbolic value.
-- | Make Color a symbolic value.
-- | Make Color a symbolic value.
-- | Nationalities of the occupants
data Nationality
Briton :: Nationality
Dane :: Nationality
Swede :: Nationality
Norwegian :: Nationality
German :: Nationality
-- | Make Nationality a symbolic value.
-- | Make Nationality a symbolic value.
-- | Make Nationality a symbolic value.
-- | Make Nationality a symbolic value.
-- | Make Nationality a symbolic value.
-- | Make Nationality a symbolic value.
-- | Make Nationality a symbolic value.
-- | Make Nationality a symbolic value.
-- | Make Nationality a symbolic value.
-- | Beverage choices
data Beverage
Tea :: Beverage
Coffee :: Beverage
Milk :: Beverage
Beer :: Beverage
Water :: Beverage
-- | Make Beverage a symbolic value.
-- | Make Beverage a symbolic value.
-- | Make Beverage a symbolic value.
-- | Make Beverage a symbolic value.
-- | Make Beverage a symbolic value.
-- | Make Beverage a symbolic value.
-- | Make Beverage a symbolic value.
-- | Make Beverage a symbolic value.
-- | Make Beverage a symbolic value.
-- | Pets they keep
data Pet
Dog :: Pet
Horse :: Pet
Cat :: Pet
Bird :: Pet
Fish :: Pet
-- | Make Pet a symbolic value.
-- | Make Pet a symbolic value.
-- | Make Pet a symbolic value.
-- | Make Pet a symbolic value.
-- | Make Pet a symbolic value.
-- | Make Pet a symbolic value.
-- | Make Pet a symbolic value.
-- | Make Pet a symbolic value.
-- | Make Pet a symbolic value.
-- | Sports they engage in
data Sport
Football :: Sport
Baseball :: Sport
Volleyball :: Sport
Hockey :: Sport
Tennis :: Sport
-- | Make Sport a symbolic value.
-- | Make Sport a symbolic value.
-- | Make Sport a symbolic value.
-- | Make Sport a symbolic value.
-- | Make Sport a symbolic value.
-- | Make Sport a symbolic value.
-- | Make Sport a symbolic value.
-- | Make Sport a symbolic value.
-- | Make Sport a symbolic value.
-- | We have:
--
--
-- >>> fishOwner
-- German
--
--
-- It's not hard to modify this program to grab the values of all the
-- assignments, i.e., the full solution to the puzzle. We leave that as
-- an exercise to the interested reader!
fishOwner :: IO ()
instance GHC.Classes.Eq Data.SBV.Examples.Puzzles.Fish.Sport
instance GHC.Show.Show Data.SBV.Examples.Puzzles.Fish.Sport
instance GHC.Classes.Ord Data.SBV.Examples.Puzzles.Fish.Sport
instance GHC.Read.Read Data.SBV.Examples.Puzzles.Fish.Sport
instance Data.Data.Data Data.SBV.Examples.Puzzles.Fish.Sport
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Puzzles.Fish.Sport
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Puzzles.Fish.Sport
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Puzzles.Fish.Sport
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Puzzles.Fish.Sport
instance GHC.Classes.Eq Data.SBV.Examples.Puzzles.Fish.Pet
instance GHC.Show.Show Data.SBV.Examples.Puzzles.Fish.Pet
instance GHC.Classes.Ord Data.SBV.Examples.Puzzles.Fish.Pet
instance GHC.Read.Read Data.SBV.Examples.Puzzles.Fish.Pet
instance Data.Data.Data Data.SBV.Examples.Puzzles.Fish.Pet
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Puzzles.Fish.Pet
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Puzzles.Fish.Pet
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Puzzles.Fish.Pet
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Puzzles.Fish.Pet
instance GHC.Classes.Eq Data.SBV.Examples.Puzzles.Fish.Beverage
instance GHC.Show.Show Data.SBV.Examples.Puzzles.Fish.Beverage
instance GHC.Classes.Ord Data.SBV.Examples.Puzzles.Fish.Beverage
instance GHC.Read.Read Data.SBV.Examples.Puzzles.Fish.Beverage
instance Data.Data.Data Data.SBV.Examples.Puzzles.Fish.Beverage
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Puzzles.Fish.Beverage
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Puzzles.Fish.Beverage
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Puzzles.Fish.Beverage
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Puzzles.Fish.Beverage
instance GHC.Classes.Eq Data.SBV.Examples.Puzzles.Fish.Nationality
instance GHC.Show.Show Data.SBV.Examples.Puzzles.Fish.Nationality
instance GHC.Classes.Ord Data.SBV.Examples.Puzzles.Fish.Nationality
instance GHC.Read.Read Data.SBV.Examples.Puzzles.Fish.Nationality
instance Data.Data.Data Data.SBV.Examples.Puzzles.Fish.Nationality
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Puzzles.Fish.Nationality
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Puzzles.Fish.Nationality
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Puzzles.Fish.Nationality
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Puzzles.Fish.Nationality
instance GHC.Classes.Eq Data.SBV.Examples.Puzzles.Fish.Color
instance GHC.Show.Show Data.SBV.Examples.Puzzles.Fish.Color
instance GHC.Classes.Ord Data.SBV.Examples.Puzzles.Fish.Color
instance GHC.Read.Read Data.SBV.Examples.Puzzles.Fish.Color
instance Data.Data.Data Data.SBV.Examples.Puzzles.Fish.Color
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Puzzles.Fish.Color
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Puzzles.Fish.Color
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Puzzles.Fish.Color
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Puzzles.Fish.Color
-- | A solution to Project Euler problem #185:
-- http://projecteuler.net/index.php?section=problems&id=185
module Data.SBV.Examples.Puzzles.Euler185
-- | The given guesses and the correct digit counts, encoded as a simple
-- list.
guesses :: [(String, SWord8)]
-- | Encode the problem, note that we check digits are within 0-9 as we use
-- 8-bit words to represent them. Otherwise, the constraints are simply
-- generated by zipping the alleged solution with each guess, and making
-- sure the number of matching digits match what's given in the problem
-- statement.
euler185 :: Symbolic SBool
-- | Print out the solution nicely. We have:
--
--
-- >>> solveEuler185
-- 4640261571849533
-- Number of solutions: 1
--
solveEuler185 :: IO ()
-- | Puzzle: Spend exactly 100 dollars and buy exactly 100 animals. Dogs
-- cost 15 dollars, cats cost 1 dollar, and mice cost 25 cents each. You
-- have to buy at least one of each. How many of each should you buy?
module Data.SBV.Examples.Puzzles.DogCatMouse
-- | Prints the only solution:
--
--
-- >>> puzzle
-- Solution #1:
-- dog = 3 :: Integer
-- cat = 41 :: Integer
-- mouse = 56 :: Integer
-- This is the only solution.
--
puzzle :: IO AllSatResult
-- | Consider the sentence:
--
--
-- In this sentence, the number of occurrences of 0 is _, of 1 is _, of 2 is _,
-- of 3 is _, of 4 is _, of 5 is _, of 6 is _, of 7 is _, of 8 is _, and of 9 is _.
--
--
-- The puzzle is to fill the blanks with numbers, such that the sentence
-- will be correct. There are precisely two solutions to this puzzle,
-- both of which are found by SBV successfully.
--
-- References:
--
--
module Data.SBV.Examples.Puzzles.Counts
-- | We will assume each number can be represented by an 8-bit word, i.e.,
-- can be at most 128.
type Count = SWord8
-- | Given a number, increment the count array depending on the digits of
-- the number
count :: Count -> [Count] -> [Count]
-- | Encoding of the puzzle. The solution is a sequence of 10 numbers for
-- the occurrences of the digits such that if we count each digit, we
-- find these numbers.
puzzle :: [Count] -> SBool
-- | Finds all two known solutions to this puzzle. We have:
--
--
-- >>> counts
-- Solution #1
-- In this sentence, the number of occurrences of 0 is 1, of 1 is 7, of 2 is 3, of 3 is 2, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 2, of 8 is 1, of 9 is 1.
-- Solution #2
-- In this sentence, the number of occurrences of 0 is 1, of 1 is 11, of 2 is 2, of 3 is 1, of 4 is 1, of 5 is 1, of 6 is 1, of 7 is 1, of 8 is 1, of 9 is 1.
-- Found: 2 solution(s).
--
counts :: IO ()
-- | Solves the following puzzle:
--
--
-- You and a friend pass by a standard coin operated vending machine and you decide to get a candy bar.
-- The price is US $0.95, but after checking your pockets you only have a dollar (US $1) and the machine
-- only takes coins. You turn to your friend and have this conversation:
-- you: Hey, do you have change for a dollar?
-- friend: Let's see. I have 6 US coins but, although they add up to a US $1.15, I can't break a dollar.
-- you: Huh? Can you make change for half a dollar?
-- friend: No.
-- you: How about a quarter?
-- friend: Nope, and before you ask I cant make change for a dime or nickel either.
-- you: Really? and these six coins are all US government coins currently in production?
-- friend: Yes.
-- you: Well can you just put your coins into the vending machine and buy me a candy bar, and I'll pay you back?
-- friend: Sorry, I would like to but I cant with the coins I have.
-- What coins are your friend holding?
--
--
-- To be fair, the problem has no solution mathematically. But
-- there is a solution when one takes into account that vending machines
-- typically do not take the 50 cent coins!
module Data.SBV.Examples.Puzzles.Coins
-- | We will represent coins with 16-bit words (more than enough precision
-- for coins).
type Coin = SWord16
-- | Create a coin. The argument Int argument just used for naming the
-- coin. Note that we constrain the value to be one of the valid U.S.
-- coin values as we create it.
mkCoin :: Int -> Symbolic Coin
-- | Return all combinations of a sequence of values.
combinations :: [a] -> [[a]]
-- | Constraint 1: Cannot make change for a dollar.
c1 :: [Coin] -> SBool
-- | Constraint 2: Cannot make change for half a dollar.
c2 :: [Coin] -> SBool
-- | Constraint 3: Cannot make change for a quarter.
c3 :: [Coin] -> SBool
-- | Constraint 4: Cannot make change for a dime.
c4 :: [Coin] -> SBool
-- | Constraint 5: Cannot make change for a nickel
c5 :: [Coin] -> SBool
-- | Constraint 6: Cannot buy the candy either. Here's where we need to
-- have the extra knowledge that the vending machines do not take 50 cent
-- coins.
c6 :: [Coin] -> SBool
-- | Solve the puzzle. We have:
--
--
-- >>> puzzle
-- Satisfiable. Model:
-- c1 = 50 :: Word16
-- c2 = 25 :: Word16
-- c3 = 10 :: Word16
-- c4 = 10 :: Word16
-- c5 = 10 :: Word16
-- c6 = 10 :: Word16
--
--
-- i.e., your friend has 4 dimes, a quarter, and a half dollar.
puzzle :: IO SatResult
-- | This is a formalization of the Cheryl's birthday problem, which went
-- viral in April 2015. (See
-- http://www.nytimes.com/2015/04/15/science/a-math-problem-from-singapore-goes-viral-when-is-cheryls-birthday.html.)
--
-- Here's the puzzle:
--
--
-- Albert and Bernard just met Cheryl. “When’s your birthday?” Albert asked Cheryl.
--
-- Cheryl thought a second and said, “I’m not going to tell you, but I’ll give you some clues.” She wrote down a list of 10 dates:
--
-- May 15, May 16, May 19
-- June 17, June 18
-- July 14, July 16
-- August 14, August 15, August 17
--
-- “My birthday is one of these,” she said.
--
-- Then Cheryl whispered in Albert’s ear the month — and only the month — of her birthday. To Bernard, she whispered the day, and only the day.
-- “Can you figure it out now?” she asked Albert.
--
-- Albert: I don’t know when your birthday is, but I know Bernard doesn’t know, either.
-- Bernard: I didn’t know originally, but now I do.
-- Albert: Well, now I know, too!
--
-- When is Cheryl’s birthday?
--
--
-- NB. Thanks to Amit Goel for suggesting the formalization strategy used
-- in here.
module Data.SBV.Examples.Puzzles.Birthday
-- | Represent month by 8-bit words; We can also use an uninterpreted type,
-- but numbers work well here.
type Month = SWord8
-- | Represent day by 8-bit words; Again, an uninterpreted type would work
-- as well.
type Day = SWord8
-- | Months referenced in the problem.
may :: SWord8
-- | Months referenced in the problem.
june :: SWord8
-- | Months referenced in the problem.
july :: SWord8
-- | Months referenced in the problem.
august :: SWord8
-- | Check that a given month/day combo is a possible birth-date.
valid :: Month -> Day -> SBool
-- | Assert that the given function holds for one of the possible days.
existsDay :: (Day -> SBool) -> SBool
-- | Assert that the given function holds for all of the possible days.
forallDay :: (Day -> SBool) -> SBool
-- | Assert that the given function holds for one of the possible months.
existsMonth :: (Month -> SBool) -> SBool
-- | Assert that the given function holds for all of the possible months.
forallMonth :: (Month -> SBool) -> SBool
-- | Encode the conversation as given in the puzzle.
--
-- NB. Lee Pike pointed out that not all the constraints are actually
-- necessary! (Private communication.) The puzzle still has a unique
-- solution if the statements a1 and b1 (i.e., Albert
-- and Bernard saying they themselves do not know the answer) are
-- removed. To experiment you can simply comment out those statements and
-- observe that there still is a unique solution. Thanks to Lee for
-- pointing this out! In fact, it is instructive to assert the
-- conversation line-by-line, and see how the search-space gets reduced
-- in each step.
puzzle :: Predicate
-- | Find all solutions to the birthday problem. We have:
--
--
-- >>> cheryl
-- Solution #1:
-- birthDay = 16 :: Word8
-- birthMonth = 7 :: Word8
-- This is the only solution.
--
cheryl :: IO ()
-- | Simple usage of polynomials over GF(2^n), using Rijndael's finite
-- field:
-- http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field
--
-- The functions available are:
--
--
-- - pMult GF(2^n) Multiplication
-- - pDiv GF(2^n) Division
-- - pMod GF(2^n) Modulus
-- - pDivMod GF(2^n) Division/Modulus, packed
-- together
--
--
-- Note that addition in GF(2^n) is simply xor, so no custom
-- function is provided.
module Data.SBV.Examples.Polynomials.Polynomials
-- | Helper synonym for representing GF(2^8); which are merely 8-bit
-- unsigned words. Largest term in such a polynomial has degree 7.
type GF28 = SWord8
-- | Multiplication in Rijndael's field; usual polynomial multiplication
-- followed by reduction by the irreducible polynomial. The irreducible
-- used by Rijndael's field is the polynomial x^8 + x^4 + x^3 + x +
-- 1, which we write by giving it's exponents in SBV. See:
-- http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field.
-- Note that the irreducible itself is not in GF28! It has a degree of 8.
--
-- NB. You can use the showPoly function to print polynomials
-- nicely, as a mathematician would write.
gfMult :: GF28 -> GF28 -> GF28
-- | States that the unit polynomial 1, is the unit element
multUnit :: GF28 -> SBool
-- | States that multiplication is commutative
multComm :: GF28 -> GF28 -> SBool
-- | States that multiplication is associative, note that associativity
-- proofs are notoriously hard for SAT/SMT solvers
multAssoc :: GF28 -> GF28 -> GF28 -> SBool
-- | States that the usual multiplication rule holds over GF(2^n)
-- polynomials Checks:
--
--
-- if (a, b) = x pDivMod y then x = y pMult a + b
--
--
-- being careful about y = 0. When divisor is 0, then quotient
-- is defined to be 0 and the remainder is the numerator. (Note that
-- addition is simply xor in GF(2^8).)
polyDivMod :: GF28 -> GF28 -> SBool
-- | Queries
testGF28 :: IO ()
-- | Solves a VM allocation problem using optimization features
module Data.SBV.Examples.Optimization.VM
-- | The allocation problem. Inspired by:
-- http://rise4fun.com/z3opt/tutorialcontent/guide#h25
--
--
-- - We have three virtual machines (VMs) which require 100, 50 and 15
-- GB hard disk respectively.
-- - There are three servers with capabilities 100, 75 and 200 GB in
-- that order.
-- - Find out a way to place VMs into servers in order
-- to
- Minimize the number of servers used
- Minimize the
-- operation cost (the servers have fixed daily costs 10, 5 and 20 USD
-- respectively.)
--
--
-- We have:
--
--
-- >>> optimize Lexicographic allocate
-- Optimal model:
-- x11 = False :: Bool
-- x12 = False :: Bool
-- x13 = True :: Bool
-- x21 = False :: Bool
-- x22 = False :: Bool
-- x23 = True :: Bool
-- x31 = False :: Bool
-- x32 = False :: Bool
-- x33 = True :: Bool
-- noOfServers = 1 :: Integer
-- cost = 20 :: Integer
--
--
-- That is, we should put all the jobs on the third server, for a total
-- cost of 20.
allocate :: Goal
-- | Solves a simple linear optimization problem
module Data.SBV.Examples.Optimization.Production
-- | Taken from
-- http://people.brunel.ac.uk/~mastjjb/jeb/or/morelp.html
--
-- A company makes two products (X and Y) using two machines (A and B).
--
--
-- - Each unit of X that is produced requires 50 minutes processing
-- time on machine A and 30 minutes processing time on machine B.
-- - Each unit of Y that is produced requires 24 minutes processing
-- time on machine A and 33 minutes processing time on machine B.
-- - At the start of the current week there are 30 units of X and 90
-- units of Y in stock. Available processing time on machine A is
-- forecast to be 40 hours and on machine B is forecast to be 35
-- hours.
-- - The demand for X in the current week is forecast to be 75 units
-- and for Y is forecast to be 95 units.
-- - Company policy is to maximise the combined sum of the units of X
-- and the units of Y in stock at the end of the week.
--
--
-- How much of each product should we make in the current week?
--
-- We have:
--
--
-- >>> optimize Lexicographic production
-- Optimal model:
-- X = 45 :: Integer
-- Y = 6 :: Integer
-- stock = 1 :: Integer
--
--
-- That is, we should produce 45 X's and 6 Y's, with the final maximum
-- stock of just 1 expected!
production :: Goal
-- | Simple linear optimization example, as found in operations research
-- texts.
module Data.SBV.Examples.Optimization.LinearOpt
-- | Taken from
-- http://people.brunel.ac.uk/~mastjjb/jeb/or/morelp.html
--
--
-- - maximize 5x1 + 6x2
-- - subject to
- x1 + x2 <= 10
- x1 - x2 >=
-- 3
- 5x1 + 4x2 <= 35
- x1 >= 0
- x2 >=
-- 0
--
--
--
-- >>> optimize Lexicographic problem
-- Optimal model:
-- x1 = 47 % 9 :: Real
-- x2 = 20 % 9 :: Real
-- goal = 355 % 9 :: Real
--
problem :: Goal
-- | Demonstrates the extension field (oo/epsilon)
-- optimization results.
module Data.SBV.Examples.Optimization.ExtField
-- | Optimization goals where min/max values might require assignments to
-- values that are infinite (integer case), or infinite/epsion (real
-- case). This simple example demostrates how SBV can be used to extract
-- such values.
--
-- We have:
--
--
-- >>> optimize Independent problem
-- Objective "one-x": Optimal in an extension field:
-- one-x = oo :: Integer
-- min_y = 7.0 + (2.0 * epsilon) :: Real
-- min_z = 5.0 + epsilon :: Real
-- Objective "min_y": Optimal in an extension field:
-- one-x = oo :: Integer
-- min_y = 7.0 + (2.0 * epsilon) :: Real
-- min_z = 5.0 + epsilon :: Real
-- Objective "min_z": Optimal in an extension field:
-- one-x = oo :: Integer
-- min_y = 7.0 + (2.0 * epsilon) :: Real
-- min_z = 5.0 + epsilon :: Real
--
problem :: Goal
-- | Demonstrates how new sizes of word/int types can be defined and used
-- with SBV.
module Data.SBV.Examples.Misc.Word4
-- | Word4 as a newtype. Invariant: Word4 x should satisfy x
-- < 16.
newtype Word4
Word4 :: Word8 -> Word4
-- | Smart constructor; simplifies conversion from Word8
word4 :: Word8 -> Word4
-- | Show instance
-- | Read instance. We read as an 8-bit word, and coerce
-- | Bounded instance; from 0 to 255
-- | Enum instance, trivial definitions.
-- | Num instance, merely lifts underlying 8-bit operation and casts back
-- | Real instance simply uses the Word8 instance
-- | Integral instance, again using Word8 instance and casting. NB. we do
-- not need to use the smart constructor here as neither the quotient nor
-- the remainder can overflow a Word4.
-- | Bits instance
-- | Random instance, used in quick-check
-- | SWord4 type synonym
type SWord4 = SBV Word4
-- | SymWord instance, allowing this type to be used in proofs/sat etc.
-- | HasKind instance; simply returning the underlying kind for the type
-- | SatModel instance, merely uses the generic parsing method.
-- | SDvisible instance, using 0-extension
-- | SDvisible instance, using default methods
-- | SIntegral instance, using default methods
-- | Conversion from bits
-- | Joiningsplitting tofrom Word8
instance Data.Data.Data Data.SBV.Examples.Misc.Word4.Word4
instance GHC.Classes.Ord Data.SBV.Examples.Misc.Word4.Word4
instance GHC.Classes.Eq Data.SBV.Examples.Misc.Word4.Word4
instance Data.SBV.Core.Model.SDivisible Data.SBV.Examples.Misc.Word4.SWord4
instance Data.SBV.Core.Splittable.FromBits Data.SBV.Examples.Misc.Word4.SWord4
instance GHC.Show.Show Data.SBV.Examples.Misc.Word4.Word4
instance GHC.Read.Read Data.SBV.Examples.Misc.Word4.Word4
instance GHC.Enum.Bounded Data.SBV.Examples.Misc.Word4.Word4
instance GHC.Enum.Enum Data.SBV.Examples.Misc.Word4.Word4
instance GHC.Num.Num Data.SBV.Examples.Misc.Word4.Word4
instance GHC.Real.Real Data.SBV.Examples.Misc.Word4.Word4
instance GHC.Real.Integral Data.SBV.Examples.Misc.Word4.Word4
instance Data.Bits.Bits Data.SBV.Examples.Misc.Word4.Word4
instance System.Random.Random Data.SBV.Examples.Misc.Word4.Word4
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Misc.Word4.Word4
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Misc.Word4.Word4
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Misc.Word4.Word4
instance Data.SBV.Core.Model.SDivisible Data.SBV.Examples.Misc.Word4.Word4
instance Data.SBV.Core.Model.SIntegral Data.SBV.Examples.Misc.Word4.Word4
instance Data.SBV.Core.Splittable.Splittable GHC.Word.Word8 Data.SBV.Examples.Misc.Word4.Word4
-- | Demonstrates SBV's assertion checking facilities
module Data.SBV.Examples.Misc.NoDiv0
-- | A simple variant of division, where we explicitly require the caller
-- to make sure the divisor is not 0.
checkedDiv :: (?loc :: CallStack) => SInt32 -> SInt32 -> SInt32
-- | Check whether an arbitrary call to checkedDiv is safe. Clearly,
-- we do not expect this to be safe:
--
--
-- >>> test1
-- [Data/SBV/Examples/Misc/NoDiv0.hs:36:14:checkedDiv: Divisor should not be 0: Violated. Model:
-- s0 = 0 :: Int32
-- s1 = 0 :: Int32]
--
test1 :: IO [SafeResult]
-- | Repeat the test, except this time we explicitly protect against the
-- bad case. We have:
--
--
-- >>> test2
-- [Data/SBV/Examples/Misc/NoDiv0.hs:44:41:checkedDiv: Divisor should not be 0: No violations detected]
--
test2 :: IO [SafeResult]
-- | Demonstrates use of programmatic model extraction. When programming
-- with SBV, we typically use sat/allSat calls to compute
-- models automatically. In more advanced uses, however, the user might
-- want to use programmable extraction features to do fancier
-- programming. We demonstrate some of these utilities here.
module Data.SBV.Examples.Misc.ModelExtract
-- | A simple function to generate a new integer value, that is not in the
-- given set of values. We also require the value to be non-negative
outside :: [Integer] -> IO SatResult
-- | We now use "outside" repeatedly to generate 10 integers, such that we
-- not only disallow previously generated elements, but also any value
-- that differs from previous solutions by less than 5. Here, we use the
-- getModelValue function. We could have also extracted the
-- dictionary via getModelDictionary and did fancier programming
-- as well, as necessary. We have:
--
--
-- >>> genVals
-- [45,40,35,30,25,20,15,10,5,0]
--
genVals :: IO [Integer]
-- | Several examples involving IEEE-754 floating point numbers, i.e.,
-- single precision Float (SFloat) and double precision
-- Double (SDouble) types.
--
-- Note that arithmetic with floating point is full of surprises; due to
-- precision issues associativity of arithmetic operations typically do
-- not hold. Also, the presence of NaN is always something to
-- look out for.
module Data.SBV.Examples.Misc.Floating
-- | Prove that floating point addition is not associative. For
-- illustration purposes, we will require one of the inputs to be a
-- NaN. We have:
--
--
-- >>> prove $ assocPlus (0/0)
-- Falsifiable. Counter-example:
-- s0 = 0.0 :: Float
-- s1 = 0.0 :: Float
--
--
-- Indeed:
--
--
-- >>> let i = 0/0 :: Float
--
-- >>> i + (0.0 + 0.0)
-- NaN
--
-- >>> ((i + 0.0) + 0.0)
-- NaN
--
--
-- But keep in mind that NaN does not equal itself in the
-- floating point world! We have:
--
--
-- >>> let nan = 0/0 :: Float in nan == nan
-- False
--
assocPlus :: SFloat -> SFloat -> SFloat -> SBool
-- | Prove that addition is not associative, even if we ignore
-- NaN/Infinity values. To do this, we use the
-- predicate fpIsPoint, which is true of a floating point number
-- (SFloat or SDouble) if it is neither NaN nor
-- Infinity. (That is, it's a representable point in the
-- real-number line.)
--
-- We have:
--
--
-- >>> assocPlusRegular
-- Falsifiable. Counter-example:
-- x = 1.9259302e-34 :: Float
-- y = -1.9259117e-34 :: Float
-- z = -1.814176e-39 :: Float
--
--
-- Indeed, we have:
--
--
-- >>> ((1.9259302e-34) + ((-1.9259117e-34) + (-1.814176e-39))) :: Float
-- 3.4438e-41
--
-- >>> (((1.9259302e-34) + ((-1.9259117e-34))) + (-1.814176e-39)) :: Float
-- 3.4014e-41
--
--
-- Note the difference between two additions!
assocPlusRegular :: IO ThmResult
-- | Demonstrate that a+b = a does not necessarily mean b
-- is 0 in the floating point world, even when we disallow the
-- obvious solution when a and b are Infinity.
-- We have:
--
--
-- >>> nonZeroAddition
-- Falsifiable. Counter-example:
-- a = 2.424457e-38 :: Float
-- b = -1.0e-45 :: Float
--
--
-- Indeed, we have:
--
--
-- >>> (2.424457e-38 + (-1.0e-45)) == (2.424457e-38 :: Float)
-- True
--
--
-- But:
--
--
-- >>> -1.0e-45 == (0 :: Float)
-- False
--
nonZeroAddition :: IO ThmResult
-- | This example illustrates that a * (1/a) does not necessarily
-- equal 1. Again, we protect against division by 0 and
-- NaN/Infinity.
--
-- We have:
--
--
-- >>> multInverse
-- Falsifiable. Counter-example:
-- a = 1.119056263978578e-308 :: Double
--
--
-- Indeed, we have:
--
--
-- >>> let a = 1.119056263978578e-308 :: Double
--
-- >>> a * (1/a)
-- 0.9999999999999999
--
multInverse :: IO ThmResult
-- | One interesting aspect of floating-point is that the chosen
-- rounding-mode can effect the results of a computation if the exact
-- result cannot be precisely represented. SBV exports the functions
-- fpAdd, fpSub, fpMul, fpDiv, fpFMA
-- and fpSqrt which allows users to specify the IEEE supported
-- RoundingMode for the operation. (Also see the class
-- RoundingFloat.) This example illustrates how SBV can be used
-- to find rounding-modes where, for instance, addition can produce
-- different results. We have:
--
--
-- >>> roundingAdd
-- Satisfiable. Model:
-- rm = RoundTowardPositive :: RoundingMode
-- x = -256.0 :: Float
-- y = 4.6475088e-10 :: Float
--
--
-- (Note that depending on your version of Z3, you might get a different
-- result.) Unfortunately we can't directly validate this result at the
-- Haskell level, as Haskell only supports RoundNearestTiesToEven.
-- We have:
--
--
-- >>> (-256.0 + 4.6475088e-10) :: Float
-- -256.0
--
--
-- While we cannot directly see the result when the mode is
-- RoundTowardPositive in Haskell, we can use SBV to provide us
-- with that result thusly:
--
--
-- >>> sat $ \z -> z .== fpAdd sRoundTowardPositive (-256.0) (4.6475088e-10 :: SFloat)
-- Satisfiable. Model:
-- s0 = -255.99998 :: Float
--
--
-- We can see why these two resuls are indeed different: The
-- RoundTowardsPositive (which rounds towards positive-infinity)
-- produces a larger result. Indeed, if we treat these numbers as
-- Double values, we get:
--
--
-- >>> (-256.0 + 4.6475088e-10) :: Double
-- -255.99999999953525
--
--
-- we see that the "more precise" result is larger than what the
-- Float value is, justifying the larger value with
-- RoundTowardPositive. A more detailed study is beyond our
-- current scope, so we'll merely -- note that floating point
-- representation and semantics is indeed a thorny subject, and point to
-- https://ece.uwaterloo.ca/~dwharder/NumericalAnalysis/02Numerics/Double/paper.pdf
-- as an excellent guide.
roundingAdd :: IO SatResult
-- | Demonstrates how enumerations can be translated to their SMT-Lib
-- counterparts, without losing any information content. Also see
-- Data.SBV.Examples.Puzzles.U2Bridge for a more detailed example
-- involving enumerations.
module Data.SBV.Examples.Misc.Enumerate
-- | A simple enumerated type, that we'd like to translate to SMT-Lib
-- intact; i.e., this type will not be uninterpreted but rather preserved
-- and will be just like any other symbolic type SBV provides.
--
-- Also note that we need to have the following LANGUAGE options
-- defined: TemplateHaskell, StandaloneDeriving,
-- DeriveDataTypeable, DeriveAnyClass for this to work.
data E
A :: E
B :: E
C :: E
-- | Make E a symbolic value.
-- | Make E a symbolic value.
-- | Make E a symbolic value.
-- | Make E a symbolic value.
-- | Make E a symbolic value.
-- | Make E a symbolic value.
-- | Make E a symbolic value.
-- | Make E a symbolic value.
-- | Make E a symbolic value.
-- | Give a name to the symbolic variants of E, for convenience
type SE = SBV E
-- | Have the SMT solver enumerate the elements of the domain. We have:
--
--
-- >>> elts
-- Solution #1:
-- s0 = B :: E
-- Solution #2:
-- s0 = A :: E
-- Solution #3:
-- s0 = C :: E
-- Found 3 different solutions.
--
elts :: IO AllSatResult
-- | Shows that if we require 4 distinct elements of the type E, we
-- shall fail; as the domain only has three elements. We have:
--
--
-- >>> four
-- Unsatisfiable
--
four :: IO SatResult
-- | Enumerations are automatically ordered, so we can ask for the maximum
-- element. Note the use of quantification. We have:
--
--
-- >>> maxE
-- Satisfiable. Model:
-- maxE = C :: E
--
maxE :: IO SatResult
-- | Similarly, we get the minumum element. We have:
--
--
-- >>> minE
-- Satisfiable. Model:
-- minE = A :: E
--
minE :: IO SatResult
instance GHC.Classes.Eq Data.SBV.Examples.Misc.Enumerate.E
instance GHC.Show.Show Data.SBV.Examples.Misc.Enumerate.E
instance GHC.Classes.Ord Data.SBV.Examples.Misc.Enumerate.E
instance GHC.Read.Read Data.SBV.Examples.Misc.Enumerate.E
instance Data.Data.Data Data.SBV.Examples.Misc.Enumerate.E
instance Data.SBV.Core.Data.SymWord Data.SBV.Examples.Misc.Enumerate.E
instance Data.SBV.Core.Kind.HasKind Data.SBV.Examples.Misc.Enumerate.E
instance Data.SBV.Control.Utils.SMTValue Data.SBV.Examples.Misc.Enumerate.E
instance Data.SBV.SMT.SMT.SatModel Data.SBV.Examples.Misc.Enumerate.E
-- | Demonstrates model construction with auxiliary variables. Sometimes we
-- need to introduce a variable in our problem as an existential
-- variable, but it's "internal" to the problem and we do not consider it
-- as part of the solution. Also, in an allSat scenario, we may
-- not care for models that only differ in these auxiliaries. SBV allows
-- designating such variables as isNonModelVar so we can still use
-- them like any other variable, but without considering them explicitly
-- in model construction.
module Data.SBV.Examples.Misc.Auxiliary
-- | A simple predicate, based on two variables x and y,
-- true when 0 <= x <= 1 and x - abs y is
-- 0.
problem :: Predicate
-- | Generate all satisfying assignments for our problem. We have:
--
--
-- >>> allModels
-- Solution #1:
-- x = 0 :: Integer
-- y = 0 :: Integer
-- Solution #2:
-- x = 1 :: Integer
-- y = 1 :: Integer
-- Solution #3:
-- x = 1 :: Integer
-- y = -1 :: Integer
-- Found 3 different solutions.
--
--
-- Note that solutions 2 and 3 share the value x =
-- 1, since there are multiple values of y that make this
-- particular choice of x satisfy our constraint.
allModels :: IO AllSatResult
-- | Generate all satisfying assignments, but we first tell SBV that
-- y should not be considered as a model problem, i.e., it's
-- auxiliary. We have:
--
--
-- >>> modelsWithYAux
-- Solution #1:
-- x = 0 :: Integer
-- Solution #2:
-- x = 1 :: Integer
-- Found 2 different solutions.
--
--
-- Note that we now have only two solutions, one for each unique value of
-- x that satisfy our constraint.
modelsWithYAux :: IO AllSatResult
-- | Finding minimal natural number solutions to linear Diophantine
-- equations, using explicit quantification.
module Data.SBV.Examples.Existentials.Diophantine
-- | For a homogeneous problem, the solution is any linear combination of
-- the resulting vectors. For a non-homogeneous problem, the solution is
-- any linear combination of the vectors in the second component plus one
-- of the vectors in the first component.
data Solution
Homogeneous :: [[Integer]] -> Solution
NonHomogeneous :: [[Integer]] -> [[Integer]] -> Solution
-- | ldn: Solve a (L)inear (D)iophantine equation, returning minimal
-- solutions over (N)aturals. The input is given as a rows of equations,
-- with rhs values separated into a tuple. The first parameter limits the
-- search to bound: In case there are too many solutions, you might want
-- to limit your search space.
ldn :: Maybe Int -> [([Integer], Integer)] -> IO Solution
-- | Find the basis solution. By definition, the basis has all non-trivial
-- (i.e., non-0) solutions that cannot be written as the sum of two other
-- solutions. We use the mathematically equivalent statement that a
-- solution is in the basis if it's least according to the lexicographic
-- order using the ordinary less-than relation. (NB. We explicitly tell
-- z3 to use the logic AUFLIA for this problem, as the BV solver that is
-- chosen automatically has a performance issue. See:
-- https://z3.codeplex.com/workitem/88.)
basis :: Maybe Int -> [[SInteger]] -> IO [[Integer]]
-- | Solve the equation:
--
--
-- 2x + y - z = 2
--
--
-- We have:
--
--
-- >>> test
-- NonHomogeneous [[0,2,0],[1,0,0]] [[0,1,1],[1,0,2]]
--
--
-- which means that the solutions are of the form:
--
--
-- (1, 0, 0) + k (0, 1, 1) + k' (1, 0, 2) = (1+k', k, k+2k')
--
--
-- OR
--
--
-- (0, 2, 0) + k (0, 1, 1) + k' (1, 0, 2) = (k', 2+k, k+2k')
--
--
-- for arbitrary k, k'. It's easy to see that these are
-- really solutions to the equation given. It's harder to see that they
-- cover all possibilities, but a moments thought reveals that is indeed
-- the case.
test :: IO Solution
-- | A puzzle: Five sailors and a monkey escape from a naufrage and reach
-- an island with coconuts. Before dawn, they gather a few of them and
-- decide to sleep first and share the next day. At night, however, one
-- of them awakes, counts the nuts, makes five parts, gives the remaining
-- nut to the monkey, saves his share away, and sleeps. All other sailors
-- do the same, one by one. When they all wake up in the morning, they
-- again make 5 shares, and give the last remaining nut to the monkey.
-- How many nuts were there at the beginning?
--
-- We can model this as a series of diophantine equations:
--
--
-- x_0 = 5 x_1 + 1
-- 4 x_1 = 5 x_2 + 1
-- 4 x_2 = 5 x_3 + 1
-- 4 x_3 = 5 x_4 + 1
-- 4 x_4 = 5 x_5 + 1
-- 4 x_5 = 5 x_6 + 1
--
--
-- We need to solve for x_0, over the naturals. We have:
--
--
-- >>> sailors
-- [15621,3124,2499,1999,1599,1279,1023]
--
--
-- That is:
--
--
-- * There was a total of 15621 coconuts
-- * 1st sailor: 15621 = 3124*5+1, leaving 15621-3124-1 = 12496
-- * 2nd sailor: 12496 = 2499*5+1, leaving 12496-2499-1 = 9996
-- * 3rd sailor: 9996 = 1999*5+1, leaving 9996-1999-1 = 7996
-- * 4th sailor: 7996 = 1599*5+1, leaving 7996-1599-1 = 6396
-- * 5th sailor: 6396 = 1279*5+1, leaving 6396-1279-1 = 5116
-- * In the morning, they had: 5116 = 1023*5+1.
--
--
-- Note that this is the minimum solution, that is, we are guaranteed
-- that there's no solution with less number of coconuts. In fact, any
-- member of [15625*k-4 | k <- [1..]] is a solution, i.e., so
-- are 31246, 46871, 62496, 78121,
-- etc.
--
-- Note that we iteratively deepen our search by requesting increasing
-- number of solutions to avoid the all-sat pitfall.
sailors :: IO [Integer]
instance GHC.Show.Show Data.SBV.Examples.Existentials.Diophantine.Solution
-- | This program demonstrates the use of the existentials and the QBVF
-- (quantified bit-vector solver). We generate CRC polynomials of degree
-- 16 that can be used for messages of size 48-bits. The query finds all
-- such polynomials that have hamming distance is at least 4. That is, if
-- the CRC can't tell two different 48-bit messages apart, then they must
-- differ in at least 4 bits.
module Data.SBV.Examples.Existentials.CRCPolynomial
-- | SBV doesn't support 48 bit words natively. So, we represent them as a
-- tuple, 32 high-bits and 16 low-bits.
type SWord48 = (SWord32, SWord16)
-- | Compute the 16 bit CRC of a 48 bit message, using the given polynomial
crc_48_16 :: SWord48 -> SWord16 -> [SBool]
-- | Count the differing bits in the message and the corresponding CRC
diffCount :: (SWord48, [SBool]) -> (SWord48, [SBool]) -> SWord8
-- | Given a hamming distance value hd, crcGood returns
-- true if the 16 bit polynomial can distinguish all messages
-- that has at most hd different bits. Note that we express this
-- conversely: If the sent and received messages are
-- different, then it must be the case that that must differ from each
-- other (including CRCs), in more than hd bits.
crcGood :: SWord8 -> SWord16 -> SWord48 -> SWord48 -> SBool
-- | Generate good CRC polynomials for 48-bit words, given the hamming
-- distance hd.
genPoly :: SWord8 -> IO ()
-- | Find and display all degree 16 polynomials with hamming distance at
-- least 4, for 48 bit messages.
--
-- When run, this function prints:
--
--
-- Polynomial #1. x^16 + x^2 + x + 1
-- Polynomial #2. x^16 + x^15 + x^2 + 1
-- Polynomial #3. x^16 + x^15 + x^2 + x + 1
-- Polynomial #4. x^16 + x^14 + x^10 + 1
-- Polynomial #5. x^16 + x^14 + x^9 + 1
-- ...
--
--
--
-- Note that different runs can produce different results, depending on
-- the random numbers used by the solver, solver version, etc. (Also, the
-- solver will take some time to generate these results. On my machine,
-- the first five polynomials were generated in about 5 minutes.)
findHD4Polynomials :: IO ()
-- | An implementation of RC4 (AKA Rivest Cipher 4 or Alleged RC4/ARC4),
-- using SBV. For information on RC4, see:
-- http://en.wikipedia.org/wiki/RC4.
--
-- We make no effort to optimize the code, and instead focus on a clear
-- implementation. In fact, the RC4 algorithm relies on in-place update
-- of its state heavily for efficiency, and is therefore unsuitable for a
-- purely functional implementation.
module Data.SBV.Examples.Crypto.RC4
-- | RC4 State contains 256 8-bit values. We use the symbolically
-- accessible full-binary type STree to represent the state, since
-- RC4 needs access to the array via a symbolic index and it's important
-- to minimize access time.
type S = STree Word8 Word8
-- | Construct the fully balanced initial tree, where the leaves are simply
-- the numbers 0 through 255.
initS :: S
-- | The key is a stream of Word8 values.
type Key = [SWord8]
-- | Represents the current state of the RC4 stream: it is the S
-- array along with the i and j index values used by
-- the PRGA.
type RC4 = (S, SWord8, SWord8)
-- | Swaps two elements in the RC4 array.
swap :: SWord8 -> SWord8 -> S -> S
-- | Implements the PRGA used in RC4. We return the new state and the next
-- key value generated.
prga :: RC4 -> (SWord8, RC4)
-- | Constructs the state to be used by the PRGA using the given key.
initRC4 :: Key -> S
-- | The key-schedule. Note that this function returns an infinite list.
keySchedule :: Key -> [SWord8]
-- | Generate a key-schedule from a given key-string.
keyScheduleString :: String -> [SWord8]
-- | RC4 encryption. We generate key-words and xor it with the input. The
-- following test-vectors are from Wikipedia
-- http://en.wikipedia.org/wiki/RC4:
--
--
-- >>> concatMap hex2 $ encrypt "Key" "Plaintext"
-- "bbf316e8d940af0ad3"
--
--
--
-- >>> concatMap hex2 $ encrypt "Wiki" "pedia"
-- "1021bf0420"
--
--
--
-- >>> concatMap hex2 $ encrypt "Secret" "Attack at dawn"
-- "45a01f645fc35b383552544b9bf5"
--
encrypt :: String -> String -> [SWord8]
-- | RC4 decryption. Essentially the same as decryption. For the above test
-- vectors we have:
--
--
-- >>> decrypt "Key" [0xbb, 0xf3, 0x16, 0xe8, 0xd9, 0x40, 0xaf, 0x0a, 0xd3]
-- "Plaintext"
--
--
--
-- >>> decrypt "Wiki" [0x10, 0x21, 0xbf, 0x04, 0x20]
-- "pedia"
--
--
--
-- >>> decrypt "Secret" [0x45, 0xa0, 0x1f, 0x64, 0x5f, 0xc3, 0x5b, 0x38, 0x35, 0x52, 0x54, 0x4b, 0x9b, 0xf5]
-- "Attack at dawn"
--
decrypt :: String -> [SWord8] -> String
-- | Prove that round-trip encryption/decryption leaves the plain-text
-- unchanged. The theorem is stated parametrically over key and
-- plain-text sizes. The expression performs the proof for a 40-bit key
-- (5 bytes) and 40-bit plaintext (again 5 bytes).
--
-- Note that this theorem is trivial to prove, since it is essentially
-- establishing xor'in the same value twice leaves a word unchanged
-- (i.e., x xor y xor y = x). However, the proof
-- takes quite a while to complete, as it gives rise to a fairly large
-- symbolic trace.
rc4IsCorrect :: IO ThmResult
-- | For doctest purposes only
hex2 :: (SymWord a, Show a, Integral a) => SBV a -> String
-- | An implementation of AES (Advanced Encryption Standard), using SBV.
-- For details on AES, see
-- http://en.wikipedia.org/wiki/Advanced_Encryption_Standard.
--
-- We do a T-box implementation, which leads to good C code as we can
-- take advantage of look-up tables. Note that we make virtually no
-- attempt to optimize our Haskell code. The concern here is not with
-- getting Haskell running fast at all. The idea is to program the T-Box
-- implementation as naturally and clearly as possible in Haskell, and
-- have SBV's code-generator generate fast C code automatically.
-- Therefore, we merely use ordinary Haskell lists as our
-- data-structures, and do not bother with any unboxing or strictness
-- annotations. Thus, we achieve the separation of concerns: Correctness
-- via clairty and simplicity and proofs on the Haskell side, performance
-- by relying on SBV's code generator. If necessary, the generated code
-- can be FFI'd back into Haskell to complete the loop.
--
-- All 3 valid key sizes (128, 192, and 256) as required by the FIPS-197
-- standard are supported.
module Data.SBV.Examples.Crypto.AES
-- | An element of the Galois Field 2^8, which are essentially polynomials
-- with maximum degree 7. They are conveniently represented as values
-- between 0 and 255.
type GF28 = SWord8
-- | Multiplication in GF(2^8). This is simple polynomial multipliation,
-- followed by the irreducible polynomial x^8+x^4+x^3+x^1+1. We
-- simply use the pMult function exported by SBV to do the
-- operation.
gf28Mult :: GF28 -> GF28 -> GF28
-- | Exponentiation by a constant in GF(2^8). The implementation uses the
-- usual square-and-multiply trick to speed up the computation.
gf28Pow :: GF28 -> Int -> GF28
-- | Computing inverses in GF(2^8). By the mathematical properties of
-- GF(2^8) and the particular irreducible polynomial used
-- x^8+x^5+x^3+x^1+1, it turns out that raising to the 254 power
-- gives us the multiplicative inverse. Of course, we can prove this
-- using SBV:
--
--
-- >>> prove $ \x -> x ./= 0 ==> x `gf28Mult` gf28Inverse x .== 1
-- Q.E.D.
--
--
-- Note that we exclude 0 in our theorem, as it does not have a
-- multiplicative inverse.
gf28Inverse :: GF28 -> GF28
-- | AES state. The state consists of four 32-bit words, each of which is
-- in turn treated as four GF28's, i.e., 4 bytes. The T-Box
-- implementation keeps the four-bytes together for efficient
-- representation.
type State = [SWord32]
-- | The key, which can be 128, 192, or 256 bits. Represented as a sequence
-- of 32-bit words.
type Key = [SWord32]
-- | The key schedule. AES executes in rounds, and it treats first and last
-- round keys slightly differently than the middle ones. We reflect that
-- choice by being explicit about it in our type. The length of the
-- middle list of keys depends on the key-size, which in turn determines
-- the number of rounds.
type KS = (Key, [Key], Key)
-- | Conversion from 32-bit words to 4 constituent bytes.
toBytes :: SWord32 -> [GF28]
-- | Conversion from 4 bytes, back to a 32-bit row, inverse of
-- toBytes above. We have the following simple theorems stating
-- this relationship formally:
--
--
-- >>> prove $ \a b c d -> toBytes (fromBytes [a, b, c, d]) .== [a, b, c, d]
-- Q.E.D.
--
--
--
-- >>> prove $ \r -> fromBytes (toBytes r) .== r
-- Q.E.D.
--
fromBytes :: [GF28] -> SWord32
-- | Rotating a state row by a fixed amount to the right.
rotR :: [GF28] -> Int -> [GF28]
-- | Definition of round-constants, as specified in Section 5.2 of the AES
-- standard.
roundConstants :: [GF28]
-- | The InvMixColumns transformation, as described in Section
-- 5.3.3 of the standard. Note that this transformation is only used
-- explicitly during key-expansion in the T-Box implementation of AES.
invMixColumns :: State -> State
-- | Key expansion. Starting with the given key, returns an infinite
-- sequence of words, as described by the AES standard, Section 5.2,
-- Figure 11.
keyExpansion :: Int -> Key -> [Key]
-- | The values of the AES S-box table. Note that we describe the S-box
-- programmatically using the mathematical construction given in Section
-- 5.1.1 of the standard. However, the code-generation will turn this
-- into a mere look-up table, as it is just a constant table, all
-- computation being done at "compile-time".
sboxTable :: [GF28]
-- | The sbox transformation. We simply select from the sbox table. Note
-- that we are obliged to give a default value (here 0) to be
-- used if the index is out-of-bounds as required by SBV's select
-- function. However, that will never happen since the table has all 256
-- elements in it.
sbox :: GF28 -> GF28
-- | The values of the inverse S-box table. Again, the construction is
-- programmatic.
unSBoxTable :: [GF28]
-- | The inverse s-box transformation.
unSBox :: GF28 -> GF28
-- | Prove that the sbox and unSBox are inverses. We have:
--
--
-- >>> prove sboxInverseCorrect
-- Q.E.D.
--
sboxInverseCorrect :: GF28 -> SBool
-- | Adding the round-key to the current state. We simply exploit the fact
-- that addition is just xor in implementing this transformation.
addRoundKey :: Key -> State -> State
-- | T-box table generation function for encryption
t0Func :: GF28 -> [GF28]
-- | First look-up table used in encryption
t0 :: GF28 -> SWord32
-- | Second look-up table used in encryption
t1 :: GF28 -> SWord32
-- | Third look-up table used in encryption
t2 :: GF28 -> SWord32
-- | Fourth look-up table used in encryption
t3 :: GF28 -> SWord32
-- | T-box table generating function for decryption
u0Func :: GF28 -> [GF28]
-- | First look-up table used in decryption
u0 :: GF28 -> SWord32
-- | Second look-up table used in decryption
u1 :: GF28 -> SWord32
-- | Third look-up table used in decryption
u2 :: GF28 -> SWord32
-- | Fourth look-up table used in decryption
u3 :: GF28 -> SWord32
-- | Generic round function. Given the function to perform one round, a
-- key-schedule, and a starting state, it performs the AES rounds.
doRounds :: (Bool -> State -> Key -> State) -> KS -> State -> State
-- | One encryption round. The first argument indicates whether this is the
-- final round or not, in which case the construction is slightly
-- different.
aesRound :: Bool -> State -> Key -> State
-- | One decryption round. Similar to the encryption round, the first
-- argument indicates whether this is the final round or not.
aesInvRound :: Bool -> State -> Key -> State
-- | Key schedule. Given a 128, 192, or 256 bit key, expand it to get
-- key-schedules for encryption and decryption. The key is given as a
-- sequence of 32-bit words. (4 elements for 128-bits, 6 for 192, and 8
-- for 256.)
aesKeySchedule :: Key -> (KS, KS)
-- | Block encryption. The first argument is the plain-text, which must
-- have precisely 4 elements, for a total of 128-bits of input. The
-- second argument is the key-schedule to be used, obtained by a call to
-- aesKeySchedule. The output will always have 4 32-bit words,
-- which is the cipher-text.
aesEncrypt :: [SWord32] -> KS -> [SWord32]
-- | Block decryption. The arguments are the same as in aesEncrypt,
-- except the first argument is the cipher-text and the output is the
-- corresponding plain-text.
aesDecrypt :: [SWord32] -> KS -> [SWord32]
-- | 128-bit encryption test, from Appendix C.1 of the AES standard:
--
--
-- >>> map hex8 t128Enc
-- ["69c4e0d8","6a7b0430","d8cdb780","70b4c55a"]
--
t128Enc :: [SWord32]
-- | 128-bit decryption test, from Appendix C.1 of the AES standard:
--
--
-- >>> map hex8 t128Dec
-- ["00112233","44556677","8899aabb","ccddeeff"]
--
t128Dec :: [SWord32]
-- | 192-bit encryption test, from Appendix C.2 of the AES standard:
--
--
-- >>> map hex8 t192Enc
-- ["dda97ca4","864cdfe0","6eaf70a0","ec0d7191"]
--
t192Enc :: [SWord32]
-- | 192-bit decryption test, from Appendix C.2 of the AES standard:
--
--
-- >>> map hex8 t192Dec
-- ["00112233","44556677","8899aabb","ccddeeff"]
--
t192Dec :: [SWord32]
-- | 256-bit encryption, from Appendix C.3 of the AES standard:
--
--
-- >>> map hex8 t256Enc
-- ["8ea2b7ca","516745bf","eafc4990","4b496089"]
--
t256Enc :: [SWord32]
-- | 256-bit decryption, from Appendix C.3 of the AES standard:
--
--
-- >>> map hex8 t256Dec
-- ["00112233","44556677","8899aabb","ccddeeff"]
--
t256Dec :: [SWord32]
-- | Correctness theorem for 128-bit AES. Ideally, we would run:
--
--
-- prove aes128IsCorrect
--
--
-- to get a proof automatically. Unfortunately, while SBV will
-- successfully generate the proof obligation for this theorem and ship
-- it to the SMT solver, it would be naive to expect the SMT-solver to
-- finish that proof in any reasonable time with the currently available
-- SMT solving technologies. Instead, we can issue:
--
--
-- quickCheck aes128IsCorrect
--
--
-- and get some degree of confidence in our code. Similar predicates can
-- be easily constructed for 192, and 256 bit cases as well.
aes128IsCorrect :: (SWord32, SWord32, SWord32, SWord32) -> (SWord32, SWord32, SWord32, SWord32) -> SBool
-- | Code generation for 128-bit AES encryption.
--
-- The following sample from the generated code-lines show how T-Boxes
-- are rendered as C arrays:
--
--
-- static const SWord32 table1[] = {
-- 0xc66363a5UL, 0xf87c7c84UL, 0xee777799UL, 0xf67b7b8dUL,
-- 0xfff2f20dUL, 0xd66b6bbdUL, 0xde6f6fb1UL, 0x91c5c554UL,
-- 0x60303050UL, 0x02010103UL, 0xce6767a9UL, 0x562b2b7dUL,
-- 0xe7fefe19UL, 0xb5d7d762UL, 0x4dababe6UL, 0xec76769aUL,
-- ...
-- }
--
--
-- The generated program has 5 tables (one sbox table, and 4-Tboxes), all
-- converted to fast C arrays. Here is a sample of the generated
-- straightline C-code:
--
--
-- const SWord8 s1915 = (SWord8) s1912;
-- const SWord8 s1916 = table0[s1915];
-- const SWord16 s1917 = (((SWord16) s1914) << 8) | ((SWord16) s1916);
-- const SWord32 s1918 = (((SWord32) s1911) << 16) | ((SWord32) s1917);
-- const SWord32 s1919 = s1844 ^ s1918;
-- const SWord32 s1920 = s1903 ^ s1919;
--
--
-- The GNU C-compiler does a fine job of optimizing this straightline
-- code to generate a fairly efficient C implementation.
cgAES128BlockEncrypt :: IO ()
-- | Components of the AES-128 implementation that the library is generated
-- from
aes128LibComponents :: [(String, SBVCodeGen ())]
-- | Generate a C library, containing functions for performing 128-bit
-- encdeckey-expansion. A note on performance: In a very rough
-- speed test, the generated code was able to do 6.3 million block
-- encryptions per second on a decent MacBook Pro. On the same machine,
-- OpenSSL reports 8.2 million block encryptions per second. So, the
-- generated code is about 25% slower as compared to the highly optimized
-- OpenSSL implementation. (Note that the speed test was done somewhat
-- simplistically, so these numbers should be considered very rough
-- estimates.)
cgAES128Library :: IO ()
-- | For doctest purposes only
hex8 :: (SymWord a, Show a, Integral a) => SBV a -> String
-- | Demonstrates the use of uninterpreted functions for the purposes of
-- code generation. This facility is important when we want to take
-- advantage of native libraries in the target platform, or when we'd
-- like to hand-generate code for certain functions for various purposes,
-- such as efficiency, or reliability.
module Data.SBV.Examples.CodeGeneration.Uninterpreted
-- | A definition of shiftLeft that can deal with variable length shifts.
-- (Note that the `shiftL` method from the Bits class
-- requires an Int shift amount.) Unfortunately, this'll generate
-- rather clumsy C code due to the use of tables etc., so we uninterpret
-- it for code generation purposes using the cgUninterpret
-- function.
shiftLeft :: SWord32 -> SWord32 -> SWord32
-- | Test function that uses shiftLeft defined above. When used as a normal
-- Haskell function or in verification the definition is fully used,
-- i.e., no uninterpretation happens. To wit, we have:
--
--
-- >>> tstShiftLeft 3 4 5
-- 224 :: SWord32
--
--
--
-- >>> prove $ \x y -> tstShiftLeft x y 0 .== x + y
-- Q.E.D.
--
tstShiftLeft :: SWord32 -> SWord32 -> SWord32 -> SWord32
-- | Generate C code for "tstShiftLeft". In this case, SBV will *use* the
-- user given definition verbatim, instead of generating code for it.
-- (Also see the functions cgAddDecl, cgAddLDFlags, and
-- cgAddPrototype.)
genCCode :: IO ()
-- | Computing population-counts (number of set bits) and automatically
-- generating C code.
module Data.SBV.Examples.CodeGeneration.PopulationCount
-- | Given a 64-bit quantity, the simplest (and obvious) way to count the
-- number of bits that are set in it is to simply walk through all the
-- bits and add 1 to a running count. This is slow, as it requires 64
-- iterations, but is simple and easy to convince yourself that it is
-- correct. For instance:
--
--
-- >>> popCountSlow 0x0123456789ABCDEF
-- 32 :: SWord8
--
popCountSlow :: SWord64 -> SWord8
-- | Faster version. This is essentially the same algorithm, except we go 8
-- bits at a time instead of one by one, by using a precomputed table of
-- population-count values for each byte. This algorithm loops
-- only 8 times, and hence is at least 8 times more efficient.
popCountFast :: SWord64 -> SWord8
-- | Look-up table, containing population counts for all possible 8-bit
-- value, from 0 to 255. Note that we do not "hard-code" the values, but
-- merely use the slow version to compute them.
pop8 :: [SWord8]
-- | States the correctness of faster population-count algorithm, with
-- respect to the reference slow version. Turns out Z3's default tactic
-- is rather slow for this one, but there's a magic incantation to make
-- it go fast. See https://github.com/Z3Prover/z3/issues/1150 for
-- details.
--
--
-- >>> let cmd = "(check-sat-using (then (using-params ackermannize_bv :div0_ackermann_limit 1000000) simplify bit-blast sat))"
--
-- >>> proveWith z3{satCmd = cmd} fastPopCountIsCorrect
-- Q.E.D.
--
fastPopCountIsCorrect :: SWord64 -> SBool
-- | Not only we can prove that faster version is correct, but we can also
-- automatically generate C code to compute population-counts for us.
-- This action will generate all the C files that you will need,
-- including a driver program for test purposes.
--
-- Below is the generated header file for popCountFast:
--
--
-- >>> genPopCountInC
-- == BEGIN: "Makefile" ================
-- # Makefile for popCount. Automatically generated by SBV. Do not edit!
--
-- # include any user-defined .mk file in the current directory.
-- -include *.mk
--
-- CC?=gcc
-- CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
--
-- all: popCount_driver
--
-- popCount.o: popCount.c popCount.h
-- ${CC} ${CCFLAGS} -c $< -o $@
--
-- popCount_driver.o: popCount_driver.c
-- ${CC} ${CCFLAGS} -c $< -o $@
--
-- popCount_driver: popCount.o popCount_driver.o
-- ${CC} ${CCFLAGS} $^ -o $@
--
-- clean:
-- rm -f *.o
--
-- veryclean: clean
-- rm -f popCount_driver
-- == END: "Makefile" ==================
-- == BEGIN: "popCount.h" ================
-- /* Header file for popCount. Automatically generated by SBV. Do not edit! */
--
-- #ifndef __popCount__HEADER_INCLUDED__
-- #define __popCount__HEADER_INCLUDED__
--
-- #include <stdio.h>
-- #include <stdlib.h>
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include <stdbool.h>
-- #include <string.h>
-- #include <math.h>
--
-- /* The boolean type */
-- typedef bool SBool;
--
-- /* The float type */
-- typedef float SFloat;
--
-- /* The double type */
-- typedef double SDouble;
--
-- /* Unsigned bit-vectors */
-- typedef uint8_t SWord8 ;
-- typedef uint16_t SWord16;
-- typedef uint32_t SWord32;
-- typedef uint64_t SWord64;
--
-- /* Signed bit-vectors */
-- typedef int8_t SInt8 ;
-- typedef int16_t SInt16;
-- typedef int32_t SInt32;
-- typedef int64_t SInt64;
--
-- /* Entry point prototype: */
-- SWord8 popCount(const SWord64 x);
--
-- #endif /* __popCount__HEADER_INCLUDED__ */
-- == END: "popCount.h" ==================
-- == BEGIN: "popCount_driver.c" ================
-- /* Example driver program for popCount. */
-- /* Automatically generated by SBV. Edit as you see fit! */
--
-- #include <stdio.h>
-- #include "popCount.h"
--
-- int main(void)
-- {
-- const SWord8 __result = popCount(0x1b02e143e4f0e0e5ULL);
--
-- printf("popCount(0x1b02e143e4f0e0e5ULL) = %"PRIu8"\n", __result);
--
-- return 0;
-- }
-- == END: "popCount_driver.c" ==================
-- == BEGIN: "popCount.c" ================
-- /* File: "popCount.c". Automatically generated by SBV. Do not edit! */
--
-- #include "popCount.h"
--
-- SWord8 popCount(const SWord64 x)
-- {
-- const SWord64 s0 = x;
-- static const SWord8 table0[] = {
-- 0, 1, 1, 2, 1, 2, 2, 3, 1, 2, 2, 3, 2, 3, 3, 4, 1, 2, 2, 3, 2, 3,
-- 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 1, 2, 2, 3, 2, 3, 3, 4, 2, 3, 3, 4,
-- 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 1, 2,
-- 2, 3, 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5,
-- 3, 4, 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5,
-- 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 1, 2, 2, 3,
-- 2, 3, 3, 4, 2, 3, 3, 4, 3, 4, 4, 5, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4,
-- 4, 5, 4, 5, 5, 6, 2, 3, 3, 4, 3, 4, 4, 5, 3, 4, 4, 5, 4, 5, 5, 6,
-- 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 2, 3, 3, 4, 3, 4,
-- 4, 5, 3, 4, 4, 5, 4, 5, 5, 6, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6,
-- 5, 6, 6, 7, 3, 4, 4, 5, 4, 5, 5, 6, 4, 5, 5, 6, 5, 6, 6, 7, 4, 5,
-- 5, 6, 5, 6, 6, 7, 5, 6, 6, 7, 6, 7, 7, 8
-- };
-- const SWord64 s11 = s0 & 0x00000000000000ffULL;
-- const SWord8 s12 = table0[s11];
-- const SWord64 s14 = s0 >> 8;
-- const SWord64 s15 = 0x00000000000000ffULL & s14;
-- const SWord8 s16 = table0[s15];
-- const SWord8 s17 = s12 + s16;
-- const SWord64 s18 = s14 >> 8;
-- const SWord64 s19 = 0x00000000000000ffULL & s18;
-- const SWord8 s20 = table0[s19];
-- const SWord8 s21 = s17 + s20;
-- const SWord64 s22 = s18 >> 8;
-- const SWord64 s23 = 0x00000000000000ffULL & s22;
-- const SWord8 s24 = table0[s23];
-- const SWord8 s25 = s21 + s24;
-- const SWord64 s26 = s22 >> 8;
-- const SWord64 s27 = 0x00000000000000ffULL & s26;
-- const SWord8 s28 = table0[s27];
-- const SWord8 s29 = s25 + s28;
-- const SWord64 s30 = s26 >> 8;
-- const SWord64 s31 = 0x00000000000000ffULL & s30;
-- const SWord8 s32 = table0[s31];
-- const SWord8 s33 = s29 + s32;
-- const SWord64 s34 = s30 >> 8;
-- const SWord64 s35 = 0x00000000000000ffULL & s34;
-- const SWord8 s36 = table0[s35];
-- const SWord8 s37 = s33 + s36;
-- const SWord64 s38 = s34 >> 8;
-- const SWord64 s39 = 0x00000000000000ffULL & s38;
-- const SWord8 s40 = table0[s39];
-- const SWord8 s41 = s37 + s40;
--
-- return s41;
-- }
-- == END: "popCount.c" ==================
--
genPopCountInC :: IO ()
-- | Computing GCD symbolically, and generating C code for it. This example
-- illustrates symbolic termination related issues when programming with
-- SBV, when the termination of a recursive algorithm crucially depends
-- on the value of a symbolic variable. The technique we use is to
-- statically enforce termination by using a recursion depth counter.
module Data.SBV.Examples.CodeGeneration.GCD
-- | The symbolic GCD algorithm, over two 8-bit numbers. We define sgcd
-- a 0 to be a for all a, which implies sgcd 0
-- 0 = 0. Note that this is essentially Euclid's algorithm, except
-- with a recursion depth counter. We need the depth counter since the
-- algorithm is not symbolically terminating, as we don't have a
-- means of determining that the second argument (b) will
-- eventually reach 0 in a symbolic context. Hence we stop after 12
-- iterations. Why 12? We've empirically determined that this algorithm
-- will recurse at most 12 times for arbitrary 8-bit numbers. Of course,
-- this is a claim that we shall prove below.
sgcd :: SWord8 -> SWord8 -> SWord8
-- | We have:
--
--
-- >>> prove sgcdIsCorrect
-- Q.E.D.
--
sgcdIsCorrect :: SWord8 -> SWord8 -> SWord8 -> SBool
-- | This call will generate the required C files. The following is the
-- function body generated for sgcd. (We are not showing the
-- generated header, Makefile, and the driver programs for
-- brevity.) Note that the generated function is a constant time
-- algorithm for GCD. It is not necessarily fastest, but it will take
-- precisely the same amount of time for all values of x and
-- y.
--
--
-- /* File: "sgcd.c". Automatically generated by SBV. Do not edit! */
--
-- #include <stdio.h>
-- #include <stdlib.h>
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include <stdbool.h>
-- #include "sgcd.h"
--
-- SWord8 sgcd(const SWord8 x, const SWord8 y)
-- {
-- const SWord8 s0 = x;
-- const SWord8 s1 = y;
-- const SBool s3 = s1 == 0;
-- const SWord8 s4 = (s1 == 0) ? s0 : (s0 % s1);
-- const SWord8 s5 = s3 ? s0 : s4;
-- const SBool s6 = 0 == s5;
-- const SWord8 s7 = (s5 == 0) ? s1 : (s1 % s5);
-- const SWord8 s8 = s6 ? s1 : s7;
-- const SBool s9 = 0 == s8;
-- const SWord8 s10 = (s8 == 0) ? s5 : (s5 % s8);
-- const SWord8 s11 = s9 ? s5 : s10;
-- const SBool s12 = 0 == s11;
-- const SWord8 s13 = (s11 == 0) ? s8 : (s8 % s11);
-- const SWord8 s14 = s12 ? s8 : s13;
-- const SBool s15 = 0 == s14;
-- const SWord8 s16 = (s14 == 0) ? s11 : (s11 % s14);
-- const SWord8 s17 = s15 ? s11 : s16;
-- const SBool s18 = 0 == s17;
-- const SWord8 s19 = (s17 == 0) ? s14 : (s14 % s17);
-- const SWord8 s20 = s18 ? s14 : s19;
-- const SBool s21 = 0 == s20;
-- const SWord8 s22 = (s20 == 0) ? s17 : (s17 % s20);
-- const SWord8 s23 = s21 ? s17 : s22;
-- const SBool s24 = 0 == s23;
-- const SWord8 s25 = (s23 == 0) ? s20 : (s20 % s23);
-- const SWord8 s26 = s24 ? s20 : s25;
-- const SBool s27 = 0 == s26;
-- const SWord8 s28 = (s26 == 0) ? s23 : (s23 % s26);
-- const SWord8 s29 = s27 ? s23 : s28;
-- const SBool s30 = 0 == s29;
-- const SWord8 s31 = (s29 == 0) ? s26 : (s26 % s29);
-- const SWord8 s32 = s30 ? s26 : s31;
-- const SBool s33 = 0 == s32;
-- const SWord8 s34 = (s32 == 0) ? s29 : (s29 % s32);
-- const SWord8 s35 = s33 ? s29 : s34;
-- const SBool s36 = 0 == s35;
-- const SWord8 s37 = s36 ? s32 : s35;
-- const SWord8 s38 = s33 ? s29 : s37;
-- const SWord8 s39 = s30 ? s26 : s38;
-- const SWord8 s40 = s27 ? s23 : s39;
-- const SWord8 s41 = s24 ? s20 : s40;
-- const SWord8 s42 = s21 ? s17 : s41;
-- const SWord8 s43 = s18 ? s14 : s42;
-- const SWord8 s44 = s15 ? s11 : s43;
-- const SWord8 s45 = s12 ? s8 : s44;
-- const SWord8 s46 = s9 ? s5 : s45;
-- const SWord8 s47 = s6 ? s1 : s46;
-- const SWord8 s48 = s3 ? s0 : s47;
--
-- return s48;
-- }
--
genGCDInC :: IO ()
-- | Computing Fibonacci numbers and generating C code. Inspired by Lee
-- Pike's original implementation, modified for inclusion in the package.
-- It illustrates symbolic termination issues one can have when working
-- with recursive algorithms and how to deal with such, eventually
-- generating good C code.
module Data.SBV.Examples.CodeGeneration.Fibonacci
-- | This is a naive implementation of fibonacci, and will work fine
-- (albeit slow) for concrete inputs:
--
--
-- >>> map fib0 [0..6]
-- [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--
--
-- However, it is not suitable for doing proofs or generating code, as it
-- is not symbolically terminating when it is called with a symbolic
-- value n. When we recursively call fib0 on
-- n-1 (or n-2), the test against 0 will
-- always explore both branches since the result will be symbolic, hence
-- will not terminate. (An integrated theorem prover can establish
-- termination after a certain number of unrollings, but this would be
-- quite expensive to implement, and would be impractical.)
fib0 :: SWord64 -> SWord64
-- | The recursion-depth limited version of fibonacci. Limiting the maximum
-- number to be 20, we can say:
--
--
-- >>> map (fib1 20) [0..6]
-- [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--
--
-- The function will work correctly, so long as the index we query is at
-- most top, and otherwise will return the value at
-- top. Note that we also use accumulating parameters here for
-- efficiency, although this is orthogonal to the termination concern.
--
-- A note on modular arithmetic: The 64-bit word we use to represent the
-- values will of course eventually overflow, beware! Fibonacci is a fast
-- growing function..
fib1 :: SWord64 -> SWord64 -> SWord64
-- | We can generate code for fib1 using the genFib1 action.
-- Note that the generated code will grow larger as we pick larger values
-- of top, but only linearly, thanks to the accumulating
-- parameter trick used by fib1. The following is an excerpt from
-- the code generated for the call genFib1 10, where the code
-- will work correctly for indexes up to 10:
--
--
-- SWord64 fib1(const SWord64 x)
-- {
-- const SWord64 s0 = x;
-- const SBool s2 = s0 == 0x0000000000000000ULL;
-- const SBool s4 = s0 == 0x0000000000000001ULL;
-- const SBool s6 = s0 == 0x0000000000000002ULL;
-- const SBool s8 = s0 == 0x0000000000000003ULL;
-- const SBool s10 = s0 == 0x0000000000000004ULL;
-- const SBool s12 = s0 == 0x0000000000000005ULL;
-- const SBool s14 = s0 == 0x0000000000000006ULL;
-- const SBool s17 = s0 == 0x0000000000000007ULL;
-- const SBool s19 = s0 == 0x0000000000000008ULL;
-- const SBool s22 = s0 == 0x0000000000000009ULL;
-- const SWord64 s25 = s22 ? 0x0000000000000022ULL : 0x0000000000000037ULL;
-- const SWord64 s26 = s19 ? 0x0000000000000015ULL : s25;
-- const SWord64 s27 = s17 ? 0x000000000000000dULL : s26;
-- const SWord64 s28 = s14 ? 0x0000000000000008ULL : s27;
-- const SWord64 s29 = s12 ? 0x0000000000000005ULL : s28;
-- const SWord64 s30 = s10 ? 0x0000000000000003ULL : s29;
-- const SWord64 s31 = s8 ? 0x0000000000000002ULL : s30;
-- const SWord64 s32 = s6 ? 0x0000000000000001ULL : s31;
-- const SWord64 s33 = s4 ? 0x0000000000000001ULL : s32;
-- const SWord64 s34 = s2 ? 0x0000000000000000ULL : s33;
--
-- return s34;
-- }
--
genFib1 :: SWord64 -> IO ()
-- | Compute the fibonacci numbers statically at code-generation
-- time and put them in a table, accessed by the select call.
fib2 :: SWord64 -> SWord64 -> SWord64
-- | Once we have fib2, we can generate the C code
-- straightforwardly. Below is an excerpt from the code that SBV
-- generates for the call genFib2 64. Note that this code is a
-- constant-time look-up table implementation of fibonacci, with no
-- run-time overhead. The index can be made arbitrarily large, naturally.
-- (Note that this function returns 0 if the index is larger
-- than 64, as specified by the call to select with default
-- 0.)
--
--
-- SWord64 fibLookup(const SWord64 x)
-- {
-- const SWord64 s0 = x;
-- static const SWord64 table0[] = {
-- 0x0000000000000000ULL, 0x0000000000000001ULL,
-- 0x0000000000000001ULL, 0x0000000000000002ULL,
-- 0x0000000000000003ULL, 0x0000000000000005ULL,
-- 0x0000000000000008ULL, 0x000000000000000dULL,
-- 0x0000000000000015ULL, 0x0000000000000022ULL,
-- 0x0000000000000037ULL, 0x0000000000000059ULL,
-- 0x0000000000000090ULL, 0x00000000000000e9ULL,
-- 0x0000000000000179ULL, 0x0000000000000262ULL,
-- 0x00000000000003dbULL, 0x000000000000063dULL,
-- 0x0000000000000a18ULL, 0x0000000000001055ULL,
-- 0x0000000000001a6dULL, 0x0000000000002ac2ULL,
-- 0x000000000000452fULL, 0x0000000000006ff1ULL,
-- 0x000000000000b520ULL, 0x0000000000012511ULL,
-- 0x000000000001da31ULL, 0x000000000002ff42ULL,
-- 0x000000000004d973ULL, 0x000000000007d8b5ULL,
-- 0x00000000000cb228ULL, 0x0000000000148addULL,
-- 0x0000000000213d05ULL, 0x000000000035c7e2ULL,
-- 0x00000000005704e7ULL, 0x00000000008cccc9ULL,
-- 0x0000000000e3d1b0ULL, 0x0000000001709e79ULL,
-- 0x0000000002547029ULL, 0x0000000003c50ea2ULL,
-- 0x0000000006197ecbULL, 0x0000000009de8d6dULL,
-- 0x000000000ff80c38ULL, 0x0000000019d699a5ULL,
-- 0x0000000029cea5ddULL, 0x0000000043a53f82ULL,
-- 0x000000006d73e55fULL, 0x00000000b11924e1ULL,
-- 0x000000011e8d0a40ULL, 0x00000001cfa62f21ULL,
-- 0x00000002ee333961ULL, 0x00000004bdd96882ULL,
-- 0x00000007ac0ca1e3ULL, 0x0000000c69e60a65ULL,
-- 0x0000001415f2ac48ULL, 0x000000207fd8b6adULL,
-- 0x0000003495cb62f5ULL, 0x0000005515a419a2ULL,
-- 0x00000089ab6f7c97ULL, 0x000000dec1139639ULL,
-- 0x000001686c8312d0ULL, 0x000002472d96a909ULL,
-- 0x000003af9a19bbd9ULL, 0x000005f6c7b064e2ULL, 0x000009a661ca20bbULL
-- };
-- const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0];
--
-- return s65;
-- }
--
genFib2 :: SWord64 -> IO ()
-- | Computing the CRC symbolically, using the USB polynomial. We also
-- generating C code for it as well. This example demonstrates the use of
-- the crcBV function, along with how CRC's can be computed
-- mathematically using polynomial division. While the results are the
-- same (i.e., proven equivalent, see crcGood below), the internal
-- CRC implementation generates much better code, compare cg1 vs
-- cg2 below.
module Data.SBV.Examples.CodeGeneration.CRC_USB5
-- | The USB CRC polynomial: x^5 + x^2 + 1. Although this
-- polynomial needs just 6 bits to represent (5 if higher order bit is
-- implicitly assumed to be set), we'll simply use a 16 bit number for
-- its representation to keep things simple for code generation purposes.
usb5 :: SWord16
-- | Given an 11 bit message, compute the CRC of it using the USB
-- polynomial, which is 5 bits, and then append it to the msg to get a
-- 16-bit word. Again, the incoming 11-bits is represented as a 16-bit
-- word, with 5 highest bits essentially ignored for input purposes.
crcUSB :: SWord16 -> SWord16
-- | Alternate method for computing the CRC, mathematically. We
-- shift the number to the left by 5, and then compute the remainder from
-- the polynomial division by the USB polynomial. The result is then
-- appended to the end of the message.
crcUSB' :: SWord16 -> SWord16
-- | Prove that the custom crcBV function is equivalent to the
-- mathematical definition of CRC's for 11 bit messages. We have:
--
--
-- >>> crcGood
-- Q.E.D.
--
crcGood :: IO ThmResult
-- | Generate a C function to compute the USB CRC, using the internal CRC
-- function.
cg1 :: IO ()
-- | Generate a C function to compute the USB CRC, using the mathematical
-- definition of the CRCs. While this version generates functionally
-- eqivalent C code, it's less efficient; it has about 30% more code. So,
-- the above version is preferable for code generation purposes.
cg2 :: IO ()
-- | Simple code generation example.
module Data.SBV.Examples.CodeGeneration.AddSub
-- | Simple function that returns add/sum of args
addSub :: SWord8 -> SWord8 -> (SWord8, SWord8)
-- | Generate C code for addSub. Here's the output showing the generated C
-- code:
--
--
-- >>> genAddSub
-- == BEGIN: "Makefile" ================
-- # Makefile for addSub. Automatically generated by SBV. Do not edit!
--
-- # include any user-defined .mk file in the current directory.
-- -include *.mk
--
-- CC?=gcc
-- CCFLAGS?=-Wall -O3 -DNDEBUG -fomit-frame-pointer
--
-- all: addSub_driver
--
-- addSub.o: addSub.c addSub.h
-- ${CC} ${CCFLAGS} -c $< -o $@
--
-- addSub_driver.o: addSub_driver.c
-- ${CC} ${CCFLAGS} -c $< -o $@
--
-- addSub_driver: addSub.o addSub_driver.o
-- ${CC} ${CCFLAGS} $^ -o $@
--
-- clean:
-- rm -f *.o
--
-- veryclean: clean
-- rm -f addSub_driver
-- == END: "Makefile" ==================
-- == BEGIN: "addSub.h" ================
-- /* Header file for addSub. Automatically generated by SBV. Do not edit! */
--
-- #ifndef __addSub__HEADER_INCLUDED__
-- #define __addSub__HEADER_INCLUDED__
--
-- #include <stdio.h>
-- #include <stdlib.h>
-- #include <inttypes.h>
-- #include <stdint.h>
-- #include <stdbool.h>
-- #include <string.h>
-- #include <math.h>
--
-- /* The boolean type */
-- typedef bool SBool;
--
-- /* The float type */
-- typedef float SFloat;
--
-- /* The double type */
-- typedef double SDouble;
--
-- /* Unsigned bit-vectors */
-- typedef uint8_t SWord8 ;
-- typedef uint16_t SWord16;
-- typedef uint32_t SWord32;
-- typedef uint64_t SWord64;
--
-- /* Signed bit-vectors */
-- typedef int8_t SInt8 ;
-- typedef int16_t SInt16;
-- typedef int32_t SInt32;
-- typedef int64_t SInt64;
--
-- /* Entry point prototype: */
-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
-- SWord8 *dif);
--
-- #endif /* __addSub__HEADER_INCLUDED__ */
-- == END: "addSub.h" ==================
-- == BEGIN: "addSub_driver.c" ================
-- /* Example driver program for addSub. */
-- /* Automatically generated by SBV. Edit as you see fit! */
--
-- #include <stdio.h>
-- #include "addSub.h"
--
-- int main(void)
-- {
-- SWord8 sum;
-- SWord8 dif;
--
-- addSub(132, 241, &sum, &dif);
--
-- printf("addSub(132, 241, &sum, &dif) ->\n");
-- printf(" sum = %"PRIu8"\n", sum);
-- printf(" dif = %"PRIu8"\n", dif);
--
-- return 0;
-- }
-- == END: "addSub_driver.c" ==================
-- == BEGIN: "addSub.c" ================
-- /* File: "addSub.c". Automatically generated by SBV. Do not edit! */
--
-- #include "addSub.h"
--
-- void addSub(const SWord8 x, const SWord8 y, SWord8 *sum,
-- SWord8 *dif)
-- {
-- const SWord8 s0 = x;
-- const SWord8 s1 = y;
-- const SWord8 s2 = s0 + s1;
-- const SWord8 s3 = s0 - s1;
--
-- *sum = s2;
-- *dif = s3;
-- }
-- == END: "addSub.c" ==================
--
genAddSub :: IO ()
-- | The PrefixSum algorithm over power-lists and proof of the
-- Ladner-Fischer implementation. See
-- http://dl.acm.org/citation.cfm?id=197356 and
-- http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf.
module Data.SBV.Examples.BitPrecise.PrefixSum
-- | A poor man's representation of powerlists and basic operations on
-- them: http://dl.acm.org/citation.cfm?id=197356 We merely
-- represent power-lists by ordinary lists.
type PowerList a = [a]
-- | The tie operator, concatenation.
tiePL :: PowerList a -> PowerList a -> PowerList a
-- | The zip operator, zips the power-lists of the same size, returns a
-- powerlist of double the size.
zipPL :: PowerList a -> PowerList a -> PowerList a
-- | Inverse of zipping.
unzipPL :: PowerList a -> (PowerList a, PowerList a)
-- | Reference prefix sum (ps) is simply Haskell's scanl1
-- function.
ps :: (a, a -> a -> a) -> PowerList a -> PowerList a
-- | The Ladner-Fischer (lf) implementation of prefix-sum. See
-- http://www.cs.utexas.edu/~plaxton/c/337/05f/slides/ParallelRecursion-4.pdf
-- or pg. 16 of http://dl.acm.org/citation.cfm?id=197356
lf :: (a, a -> a -> a) -> PowerList a -> PowerList a
-- | Correctness theorem, for a powerlist of given size, an associative
-- operator, and its left-unit element.
flIsCorrect :: Int -> (forall a. (OrdSymbolic a, Num a, Bits a) => (a, a -> a -> a)) -> Symbolic SBool
-- | Proves Ladner-Fischer is equivalent to reference specification for
-- addition. 0 is the left-unit element, and we use a power-list
-- of size 8. We have:
--
--
-- >>> thm1
-- Q.E.D.
--
thm1 :: IO ThmResult
-- | Proves Ladner-Fischer is equivalent to reference specification for the
-- function max. 0 is the left-unit element, and we use
-- a power-list of size 16. We have:
--
--
-- >>> thm2
-- Q.E.D.
--
thm2 :: IO ThmResult
-- | An SBV solution to the bit-precise puzzle of shuffling the bits in a
-- 64-bit word in a custom order. The idea is to take a 64-bit value:
--
--
-- 1.......2.......3.......4.......5.......6.......7.......8.......
--
--
-- And turn it into another 64-bit value, that looks like this:
--
--
-- 12345678........................................................
--
--
-- We do not care what happens to the bits that are represented by dots.
-- The problem is to do this with one mask and one multiplication.
--
-- Apparently this operation has several applications, including in
-- programs that play chess of all things. We use SBV to find the
-- appropriate mask and the multiplier.
--
-- Note that this is an instance of the program synthesis problem, where
-- we "fill in the blanks" given a certain skeleton that satisfy a
-- certain property, using quantified formulas.
module Data.SBV.Examples.BitPrecise.MultMask
-- | Find the multiplier and the mask as described. We have:
--
--
-- >>> maskAndMult
-- Satisfiable. Model:
-- mask = 0x8080808080808080 :: Word64
-- mult = 0xc202040810204081 :: Word64
--
--
-- That is, any 64 bit value masked by the first and multipled by the
-- second value above will have its bits at positions
-- [7,15,23,31,39,47,55,63] moved to positions
-- [56,57,58,59,60,61,62,63] respectively.
maskAndMult :: IO ()
-- | Symbolic implementation of merge-sort and its correctness.
module Data.SBV.Examples.BitPrecise.MergeSort
-- | Element type of lists we'd like to sort. For simplicity, we'll just
-- use SWord8 here, but we can pick any symbolic type.
type E = SWord8
-- | Merging two given sorted lists, preserving the order.
merge :: [E] -> [E] -> [E]
-- | Simple merge-sort implementation. We simply divide the input list in
-- two two halves so long as it has at least two elements, sort each half
-- on its own, and then merge.
mergeSort :: [E] -> [E]
-- | Check whether a given sequence is non-decreasing.
nonDecreasing :: [E] -> SBool
-- | Check whether two given sequences are permutations. We simply check
-- that each sequence is a subset of the other, when considered as a set.
-- The check is slightly complicated for the need to account for possibly
-- duplicated elements.
isPermutationOf :: [E] -> [E] -> SBool
-- | Asserting correctness of merge-sort for a list of the given size. Note
-- that we can only check correctness for fixed-size lists. Also, the
-- proof will get more and more complicated for the backend SMT solver as
-- n increases. A value around 5 or 6 should be fairly easy to
-- prove. For instance, we have:
--
--
-- >>> correctness 5
-- Q.E.D.
--
correctness :: Int -> IO ThmResult
-- | Generate C code for merge-sorting an array of size n. Again,
-- we're restricted to fixed size inputs. While the output is not how one
-- would code merge sort in C by hand, it's a faithful rendering of all
-- the operations merge-sort would do as described by its Haskell
-- counterpart.
codeGen :: Int -> IO ()
-- | An encoding and correctness proof of Legato's multiplier in Haskell.
-- Bill Legato came up with an interesting way to multiply two 8-bit
-- numbers on Mostek, as described here:
-- http://www.cs.utexas.edu/~moore/acl2/workshop-2004/contrib/legato/Weakest-Preconditions-Report.pdf
--
-- Here's Legato's algorithm, as coded in Mostek assembly:
--
--
-- step1 : LDX #8 ; load X immediate with the integer 8
-- step2 : LDA #0 ; load A immediate with the integer 0
-- step3 : LOOP ROR F1 ; rotate F1 right circular through C
-- step4 : BCC ZCOEF ; branch to ZCOEF if C = 0
-- step5 : CLC ; set C to 0
-- step6 : ADC F2 ; set A to A+F2+C and C to the carry
-- step7 : ZCOEF ROR A ; rotate A right circular through C
-- step8 : ROR LOW ; rotate LOW right circular through C
-- step9 : DEX ; set X to X-1
-- step10: BNE LOOP ; branch to LOOP if Z = 0
--
--
-- This program came to be known as the Legato's challenge in the
-- community, where the challenge was to prove that it indeed does
-- perform multiplication. This file formalizes the Mostek architecture
-- in Haskell and proves that Legato's algorithm is indeed correct.
module Data.SBV.Examples.BitPrecise.Legato
-- | The memory is addressed by 32-bit words.
type Address = SWord32
-- | We model only two registers of Mostek that is used in the above
-- algorithm, can add more.
data Register
RegX :: Register
RegA :: Register
-- | The carry flag (FlagC) and the zero flag (FlagZ)
data Flag
FlagC :: Flag
FlagZ :: Flag
-- | Mostek was an 8-bit machine.
type Value = SWord8
-- | Convenient synonym for symbolic machine bits.
type Bit = SBool
-- | Register bank
type Registers = Array Register Value
-- | Flag bank
type Flags = Array Flag Bit
-- | The memory maps 32-bit words to 8-bit words. (The Model
-- data-type is defined later, depending on the verification model used.)
type Memory = Model Word32 Word8
-- | Abstraction of the machine: The CPU consists of memory, registers, and
-- flags. Unlike traditional hardware, we assume the program is stored in
-- some other memory area that we need not model. (No self modifying
-- programs!)
--
-- Mostek is equipped with an automatically derived
-- Mergeable instance because each field is Mergeable.
data Mostek
Mostek :: Memory -> Registers -> Flags -> Mostek
[memory] :: Mostek -> Memory
[registers] :: Mostek -> Registers
[flags] :: Mostek -> Flags
-- | Given a machine state, compute a value out of it
type Extract a = Mostek -> a
-- | Programs are essentially state transformers (on the machine state)
type Program = Mostek -> Mostek
-- | Get the value of a given register
getReg :: Register -> Extract Value
-- | Set the value of a given register
setReg :: Register -> Value -> Program
-- | Get the value of a flag
getFlag :: Flag -> Extract Bit
-- | Set the value of a flag
setFlag :: Flag -> Bit -> Program
-- | Read memory
peek :: Address -> Extract Value
-- | Write to memory
poke :: Address -> Value -> Program
-- | Checking overflow. In Legato's multipler the ADC instruction
-- needs to see if the expression x + y + c overflowed, as checked by
-- this function. Note that we verify the correctness of this check
-- separately below in checkOverflowCorrect.
checkOverflow :: SWord8 -> SWord8 -> SBool -> SBool
-- | Correctness theorem for our checkOverflow implementation.
--
-- We have:
--
--
-- >>> checkOverflowCorrect
-- Q.E.D.
--
checkOverflowCorrect :: IO ThmResult
-- | An instruction is modeled as a Program transformer. We model
-- mostek programs in direct continuation passing style.
type Instruction = Program -> Program
-- | LDX: Set register X to value v
ldx :: Value -> Instruction
-- | LDA: Set register A to value v
lda :: Value -> Instruction
-- | CLC: Clear the carry flag
clc :: Instruction
-- | ROR, memory version: Rotate the value at memory location a to
-- the right by 1 bit, using the carry flag as a transfer position. That
-- is, the final bit of the memory location becomes the new carry and the
-- carry moves over to the first bit. This very instruction is one of the
-- reasons why Legato's multiplier is quite hard to understand and is
-- typically presented as a verification challenge.
rorM :: Address -> Instruction
-- | ROR, register version: Same as rorM, except through register
-- r.
rorR :: Register -> Instruction
-- | BCC: branch to label l if the carry flag is false
bcc :: Program -> Instruction
-- | ADC: Increment the value of register A by the value of memory
-- contents at address a, using the carry-bit as the carry-in
-- for the addition.
adc :: Address -> Instruction
-- | DEX: Decrement the value of register X
dex :: Instruction
-- | BNE: Branch if the zero-flag is false
bne :: Program -> Instruction
-- | The end combinator "stops" our program, providing the final
-- continuation that does nothing.
end :: Program
-- | Parameterized by the addresses of locations of the factors
-- (F1 and F2), the following program multiplies them,
-- storing the low-byte of the result in the memory location
-- lowAddr, and the high-byte in register A. The
-- implementation is a direct transliteration of Legato's algorithm given
-- at the top, using our notation.
legato :: Address -> Address -> Address -> Program
-- | Given address/value pairs for F1 and F2, and the location of where the
-- low-byte of the result should go, runLegato takes an
-- arbitrary machine state m and returns the high and low bytes
-- of the multiplication.
runLegato :: (Address, Value) -> (Address, Value) -> Address -> Mostek -> (Value, Value)
-- | Helper synonym for capturing relevant bits of Mostek
type InitVals = (Value, Value, Bit, Bit)
-- | Create an instance of the Mostek machine, initialized by the memory
-- and the relevant values of the registers and the flags
initMachine :: Memory -> InitVals -> Mostek
-- | The correctness theorem. For all possible memory configurations, the
-- factors (x and y below), the location of the
-- low-byte result and the initial-values of registers and the flags,
-- this function will return True only if running Legato's algorithm does
-- indeed compute the product of x and y correctly.
legatoIsCorrect :: Memory -> (Address, Value) -> (Address, Value) -> Address -> InitVals -> SBool
-- | Choose the appropriate array model to be used for modeling the memory.
-- (See Memory.) The SFunArray is the function based model.
-- SArray is the SMT-Lib array's based model.
type Model = SFunArray
-- | The correctness theorem. On a 2011 MacBook, this proof takes about 1
-- minute 45 seconds with the SFunArray memory model using
-- boolector as the solver.
correctnessTheorem :: IO ThmResult
-- | Generate a C program that implements Legato's algorithm automatically.
legatoInC :: IO ()
instance Data.SBV.Core.Model.Mergeable Data.SBV.Examples.BitPrecise.Legato.Mostek
instance GHC.Generics.Generic Data.SBV.Examples.BitPrecise.Legato.Mostek
instance GHC.Enum.Enum Data.SBV.Examples.BitPrecise.Legato.Flag
instance GHC.Enum.Bounded Data.SBV.Examples.BitPrecise.Legato.Flag
instance GHC.Arr.Ix Data.SBV.Examples.BitPrecise.Legato.Flag
instance GHC.Classes.Ord Data.SBV.Examples.BitPrecise.Legato.Flag
instance GHC.Classes.Eq Data.SBV.Examples.BitPrecise.Legato.Flag
instance GHC.Enum.Enum Data.SBV.Examples.BitPrecise.Legato.Register
instance GHC.Enum.Bounded Data.SBV.Examples.BitPrecise.Legato.Register
instance GHC.Arr.Ix Data.SBV.Examples.BitPrecise.Legato.Register
instance GHC.Classes.Ord Data.SBV.Examples.BitPrecise.Legato.Register
instance GHC.Classes.Eq Data.SBV.Examples.BitPrecise.Legato.Register
-- | Checks the correctness of a few tricks from the large collection found
-- in: https://graphics.stanford.edu/~seander/bithacks.html
module Data.SBV.Examples.BitPrecise.BitTricks
-- | Formalizes
-- https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax
fastMinCorrect :: SInt32 -> SInt32 -> SBool
-- | Formalizes
-- https://graphics.stanford.edu/~seander/bithacks.html#IntegerMinOrMax
fastMaxCorrect :: SInt32 -> SInt32 -> SBool
-- | Formalizes
-- https://graphics.stanford.edu/~seander/bithacks.html#DetectOppositeSigns
oppositeSignsCorrect :: SInt32 -> SInt32 -> SBool
-- | Formalizes
-- https://graphics.stanford.edu/~seander/bithacks.html#ConditionalSetOrClearBitsWithoutBranching
conditionalSetClearCorrect :: SBool -> SWord32 -> SWord32 -> SBool
-- | Formalizes
-- https://graphics.stanford.edu/~seander/bithacks.html#DetermineIfPowerOf2
powerOfTwoCorrect :: SWord32 -> SBool
-- | Collection of queries
queries :: IO ()
-- | Dynamically typed low-level API to the SBV library, for users who want
-- to generate symbolic values at run-time. Note that with this API it is
-- possible to create terms that are not type correct; use at your own
-- risk!
module Data.SBV.Dynamic
-- | The Symbolic value. Either a constant (Left) or a
-- symbolic value (Right Cached). Note that caching is essential
-- for making sure sharing is preserved.
data SVal
-- | A class for capturing values that have a sign and a size (finite or
-- infinite) minimal complete definition: kindOf. This class can be
-- automatically derived for data-types that have a Data
-- instance; this is useful for creating uninterpreted sorts.
class HasKind a
kindOf :: HasKind a => a -> Kind
hasSign :: HasKind a => a -> Bool
intSizeOf :: HasKind a => a -> Int
isBoolean :: HasKind a => a -> Bool
isBounded :: HasKind a => a -> Bool
isReal :: HasKind a => a -> Bool
isFloat :: HasKind a => a -> Bool
isDouble :: HasKind a => a -> Bool
isInteger :: HasKind a => a -> Bool
isUninterpreted :: HasKind a => a -> Bool
showType :: HasKind a => a -> String
kindOf :: (HasKind a, Read a, Data a) => a -> Kind
-- | Kind of symbolic value
data Kind
KBool :: Kind
KBounded :: !Bool -> !Int -> Kind
KUnbounded :: Kind
KReal :: Kind
KUserSort :: String -> (Either String [String]) -> Kind
KFloat :: Kind
KDouble :: Kind
-- | CW represents a concrete word of a fixed size: Endianness is
-- mostly irrelevant (see the FromBits class). For signed words,
-- the most significant digit is considered to be the sign.
data CW
CW :: !Kind -> !CWVal -> CW
[_cwKind] :: CW -> !Kind
[cwVal] :: CW -> !CWVal
-- | A constant value
data CWVal
-- | algebraic real
CWAlgReal :: !AlgReal -> CWVal
-- | bit-vector/unbounded integer
CWInteger :: !Integer -> CWVal
-- | float
CWFloat :: !Float -> CWVal
-- | double
CWDouble :: !Double -> CWVal
-- | value of an uninterpreted/user kind. The Maybe Int shows index
-- position for enumerations
CWUserSort :: !(Maybe Int, String) -> CWVal
-- | Convert a CW to a Haskell boolean (NB. Assumes input is well-kinded)
cwToBool :: CW -> Bool
-- | Arrays implemented in terms of SMT-arrays:
-- http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
--
--
-- - Maps directly to SMT-lib arrays
-- - Reading from an unintialized value is OK and yields an unspecified
-- result
-- - Can check for equality of these arrays
-- - Cannot quick-check theorems using SArr values
-- - Typically slower as it heavily relies on SMT-solving for the array
-- theory
--
data SArr
-- | Read the array element at a
readSArr :: SArr -> SVal -> SVal
-- | Update the element at a to be b
writeSArr :: SArr -> SVal -> SVal -> SArr
-- | Merge two given arrays on the symbolic condition Intuitively:
-- mergeArrays cond a b = if cond then a else b. Merging pushes
-- the if-then-else choice down on to elements
mergeSArr :: SVal -> SArr -> SArr -> SArr
-- | Create a named new array, with an optional initial value
newSArr :: (Kind, Kind) -> (Int -> String) -> Symbolic SArr
-- | Compare two arrays for equality
eqSArr :: SArr -> SArr -> SVal
-- | A Symbolic computation. Represented by a reader monad carrying the
-- state of the computation, layered on top of IO for creating unique
-- references to hold onto intermediate results.
data Symbolic a
-- | Quantifiers: forall or exists. Note that we allow arbitrary nestings.
data Quantifier
ALL :: Quantifier
EX :: Quantifier
-- | Create a symbolic value, based on the quantifier we have. If an
-- explicit quantifier is given, we just use that. If not, then we pick
-- the quantifier appropriately based on the run-mode. randomCW
-- is used for generating random values for this variable when used for
-- quickCheck or genTest purposes.
svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
-- | Boolean True.
svTrue :: SVal
-- | Boolean False.
svFalse :: SVal
-- | Convert from a Boolean.
svBool :: Bool -> SVal
-- | Extract a bool, by properly interpreting the integer stored.
svAsBool :: SVal -> Maybe Bool
-- | Convert from an Integer.
svInteger :: Kind -> Integer -> SVal
-- | Extract an integer from a concrete value.
svAsInteger :: SVal -> Maybe Integer
-- | Convert from a Float
svFloat :: Float -> SVal
-- | Convert from a Float
svDouble :: Double -> SVal
-- | Convert from a Rational
svReal :: Rational -> SVal
-- | Grab the numerator of an SReal, if available
svNumerator :: SVal -> Maybe Integer
-- | Grab the denominator of an SReal, if available
svDenominator :: SVal -> Maybe Integer
-- | Equality.
svEqual :: SVal -> SVal -> SVal
-- | Inequality.
svNotEqual :: SVal -> SVal -> SVal
-- | Constructing [x, y, .. z] and [x .. y]. Only works when all arguments
-- are concrete and integral and the result is guaranteed finite Note
-- that the it isn't "obviously" clear why the following works; after all
-- we're doing the construction over Integer's and mapping it back to
-- other types such as SIntN/SWordN. The reason is that the values we
-- receive are guaranteed to be in their domains; and thus the lifting to
-- Integers preserves the bounds; and then going back is just fine. So,
-- things like [1, 5 .. 200] :: [SInt8] work just fine (end
-- evaluate to empty list), since we see [1, 5 .. -56] in the
-- Integer domain. Also note the explicit check for s /=
-- f below to make sure we don't stutter and produce an infinite
-- list.
svEnumFromThenTo :: SVal -> Maybe SVal -> SVal -> Maybe [SVal]
-- | Less than.
svLessThan :: SVal -> SVal -> SVal
-- | Greater than.
svGreaterThan :: SVal -> SVal -> SVal
-- | Less than or equal to.
svLessEq :: SVal -> SVal -> SVal
-- | Greater than or equal to.
svGreaterEq :: SVal -> SVal -> SVal
-- | Addition.
svPlus :: SVal -> SVal -> SVal
-- | Multiplication.
svTimes :: SVal -> SVal -> SVal
-- | Subtraction.
svMinus :: SVal -> SVal -> SVal
-- | Unary minus.
svUNeg :: SVal -> SVal
-- | Absolute value.
svAbs :: SVal -> SVal
-- | Division.
svDivide :: SVal -> SVal -> SVal
-- | Quotient: Overloaded operation whose meaning depends on the kind at
-- which it is used: For unbounded integers, it corresponds to the
-- SMT-Lib "div" operator (Euclidean division, which always has a
-- non-negative remainder). For unsigned bitvectors, it is "bvudiv"; and
-- for signed bitvectors it is "bvsdiv", which rounds toward zero.
-- Division by 0 is defined s.t. x/0 = 0, which holds even when
-- x itself is 0.
svQuot :: SVal -> SVal -> SVal
-- | Remainder: Overloaded operation whose meaning depends on the kind at
-- which it is used: For unbounded integers, it corresponds to the
-- SMT-Lib "mod" operator (always non-negative). For unsigned bitvectors,
-- it is "bvurem"; and for signed bitvectors it is "bvsrem", which rounds
-- toward zero (sign of remainder matches that of x). Division
-- by 0 is defined s.t. x/0 = 0, which holds even when
-- x itself is 0.
svRem :: SVal -> SVal -> SVal
-- | Combination of quot and rem
svQuotRem :: SVal -> SVal -> (SVal, SVal)
-- | Exponentiation.
svExp :: SVal -> SVal -> SVal
-- | Add a constant value:
svAddConstant :: Integral a => SVal -> a -> SVal
-- | Increment:
svIncrement :: SVal -> SVal
-- | Decrement:
svDecrement :: SVal -> SVal
-- | Bitwise and.
svAnd :: SVal -> SVal -> SVal
-- | Bitwise or.
svOr :: SVal -> SVal -> SVal
-- | Bitwise xor.
svXOr :: SVal -> SVal -> SVal
-- | Bitwise complement.
svNot :: SVal -> SVal
-- | Shift left by a constant amount. Translates to the "bvshl" operation
-- in SMT-Lib.
svShl :: SVal -> Int -> SVal
-- | Shift right by a constant amount. Translates to either "bvlshr"
-- (logical shift right) or "bvashr" (arithmetic shift right) in SMT-Lib,
-- depending on whether x is a signed bitvector.
svShr :: SVal -> Int -> SVal
-- | Rotate-left, by a constant
svRol :: SVal -> Int -> SVal
-- | Rotate-right, by a constant
svRor :: SVal -> Int -> SVal
-- | Extract bit-sequences.
svExtract :: Int -> Int -> SVal -> SVal
-- | Join two words, by concataneting
svJoin :: SVal -> SVal -> SVal
-- | Convert a symbolic bitvector from unsigned to signed.
svSign :: SVal -> SVal
-- | Convert a symbolic bitvector from signed to unsigned.
svUnsign :: SVal -> SVal
-- | Convert a symbolic bitvector from one integral kind to another.
svFromIntegral :: Kind -> SVal -> SVal
-- | Total indexing operation. svSelect xs default index is
-- intuitively the same as xs !! index, except it evaluates to
-- default if index overflows. Translates to SMT-Lib
-- tables.
svSelect :: [SVal] -> SVal -> SVal -> SVal
-- | Convert an SVal from kind Bool to an unsigned bitvector of size 1.
svToWord1 :: SVal -> SVal
-- | Convert an SVal from a bitvector of size 1 (signed or unsigned) to
-- kind Bool.
svFromWord1 :: SVal -> SVal
-- | Test the value of a bit. Note that we do an extract here as opposed to
-- masking and checking against zero, as we found extraction to be much
-- faster with large bit-vectors.
svTestBit :: SVal -> Int -> SVal
-- | Set a given bit at index
svSetBit :: SVal -> Int -> SVal
-- | Generalization of svShl, where the shift-amount is symbolic.
svShiftLeft :: SVal -> SVal -> SVal
-- | Generalization of svShr, where the shift-amount is symbolic.
--
-- NB. If the shiftee is signed, then this is an arithmetic shift;
-- otherwise it's logical.
svShiftRight :: SVal -> SVal -> SVal
-- | Generalization of svRol, where the rotation amount is symbolic.
-- If the first argument is not bounded, then the this is the same as
-- shift.
svRotateLeft :: SVal -> SVal -> SVal
-- | Generalization of svRor, where the rotation amount is symbolic.
-- If the first argument is not bounded, then the this is the same as
-- shift.
svRotateRight :: SVal -> SVal -> SVal
-- | Un-bit-blast from little-endian representation to a word of the right
-- size. The input is assumed to be unsigned.
svWordFromBE :: [SVal] -> SVal
-- | Un-bit-blast from big-endian representation to a word of the right
-- size. The input is assumed to be unsigned.
svWordFromLE :: [SVal] -> SVal
-- | Bit-blast: Little-endian. Assumes the input is a bit-vector.
svBlastLE :: SVal -> [SVal]
-- | Bit-blast: Big-endian. Assumes the input is a bit-vector.
svBlastBE :: SVal -> [SVal]
-- | If-then-else. This one will force branches.
svIte :: SVal -> SVal -> SVal -> SVal
-- | Lazy If-then-else. This one will delay forcing the branches unless
-- it's really necessary.
svLazyIte :: Kind -> SVal -> SVal -> SVal -> SVal
-- | Merge two symbolic values, at kind k, possibly
-- force'ing the branches to make sure they do not evaluate to
-- the same result.
svSymbolicMerge :: Kind -> Bool -> SVal -> SVal -> SVal -> SVal
-- | Uninterpreted constants and functions. An uninterpreted constant is a
-- value that is indexed by its name. The only property the prover
-- assumes about these values are that they are equivalent to themselves;
-- i.e., (for functions) they return the same results when applied to
-- same arguments. We support uninterpreted-functions as a general means
-- of black-box'ing operations that are irrelevant for the
-- purposes of the proof; i.e., when the proofs can be performed without
-- any knowledge about the function itself.
svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal
-- | Proves the predicate using the given SMT-solver
proveWith :: SMTConfig -> Symbolic SVal -> IO ThmResult
-- | Find a satisfying assignment using the given SMT-solver
satWith :: SMTConfig -> Symbolic SVal -> IO SatResult
-- | Find all satisfying assignments using the given SMT-solver
allSatWith :: SMTConfig -> Symbolic SVal -> IO AllSatResult
-- | Check safety using the given SMT-solver
safeWith :: SMTConfig -> Symbolic SVal -> IO [SafeResult]
-- | Prove a property with multiple solvers, running them in separate
-- threads. The results will be returned in the order produced.
proveWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, ThmResult)]
-- | Prove a property with multiple solvers, running them in separate
-- threads. Only the result of the first one to finish will be returned,
-- remaining threads will be killed.
proveWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, ThmResult)
-- | Find a satisfying assignment to a property with multiple solvers,
-- running them in separate threads. The results will be returned in the
-- order produced.
satWithAll :: [SMTConfig] -> Symbolic SVal -> IO [(Solver, NominalDiffTime, SatResult)]
-- | Find a satisfying assignment to a property with multiple solvers,
-- running them in separate threads. Only the result of the first one to
-- finish will be returned, remaining threads will be killed.
satWithAny :: [SMTConfig] -> Symbolic SVal -> IO (Solver, NominalDiffTime, SatResult)
-- | Dynamic variant of quick-check
svQuickCheck :: Symbolic SVal -> IO Bool
-- | A prove call results in a ThmResult
newtype ThmResult
ThmResult :: SMTResult -> ThmResult
-- | A sat call results in a SatResult The reason for
-- having a separate SatResult is to have a more meaningful
-- Show instance.
newtype SatResult
SatResult :: SMTResult -> SatResult
-- | An allSat call results in a AllSatResult. The first
-- boolean says whether we hit the max-model limit as we searched. The
-- second boolean says whether there were prefix-existentials.
newtype AllSatResult
AllSatResult :: (Bool, Bool, [SMTResult]) -> AllSatResult
-- | A safe call results in a SafeResult
newtype SafeResult
SafeResult :: (Maybe String, String, SMTResult) -> SafeResult
-- | An optimize call results in a OptimizeResult. In the
-- ParetoResult case, the boolean is True if we reached
-- pareto-query limit and so there might be more unqueried results
-- remaining. If False, it means that we have all the pareto
-- fronts returned. See the Pareto OptimizeStyle for
-- details.
data OptimizeResult
LexicographicResult :: SMTResult -> OptimizeResult
ParetoResult :: (Bool, [SMTResult]) -> OptimizeResult
IndependentResult :: [(String, SMTResult)] -> OptimizeResult
-- | The result of an SMT solver call. Each constructor is tagged with the
-- SMTConfig that created it so that further tools can inspect it
-- and build layers of results, if needed. For ordinary uses of the
-- library, this type should not be needed, instead use the accessor
-- functions on it. (Custom Show instances and model extractors.)
data SMTResult
-- | Unsatisfiable
Unsatisfiable :: SMTConfig -> SMTResult
-- | Satisfiable with model
Satisfiable :: SMTConfig -> SMTModel -> SMTResult
-- | Prover returned a model, but in an extension field containing
-- Infinite/epsilon
SatExtField :: SMTConfig -> SMTModel -> SMTResult
-- | Prover returned unknown, with the given reason
Unknown :: SMTConfig -> String -> SMTResult
-- | Prover errored out
ProofError :: SMTConfig -> [String] -> SMTResult
-- | Parse a signed/sized value from a sequence of CWs
genParse :: Integral a => Kind -> [CW] -> Maybe (a, [CW])
-- | Extract a model, the result is a tuple where the first argument (if
-- True) indicates whether the model was "probable". (i.e., if the solver
-- returned unknown.)
getModelAssignment :: SMTResult -> Either String (Bool, [CW])
-- | Extract a model dictionary. Extract a dictionary mapping the variables
-- to their respective values as returned by the SMT solver. Also see
-- getModelDictionaries.
getModelDictionary :: SMTResult -> Map String CW
-- | Solver configuration. See also z3, yices,
-- cvc4, boolector, mathSAT, etc. 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 not
-- necessarily have finite decimal representations, and hence we have to
-- stop printing at some depth. It is important to emphasize that such
-- values always have infinite precision internally. The issue is merely
-- with how we print such an infinite precision value on the screen. The
-- field printRealPrec controls the printing precision, by
-- specifying the number of digits after the decimal point. The default
-- value is 16, but it can be set to any positive integer.
--
-- When printing, SBV will add the suffix ... at the and of a
-- real-value, if the given bound is not sufficient to represent the
-- real-value exactly. Otherwise, the number will be written out in
-- standard decimal notation. Note that SBV will always print the whole
-- value if it is precise (i.e., if it fits in a finite number of
-- digits), regardless of the precision limit. The limit only applies if
-- the representation of the real value is not finite, i.e., if it is not
-- rational.
--
-- The printBase field can be used to print numbers in base 2, 10,
-- or 16. If base 2 or 16 is used, then floating-point values will be
-- printed in their internal memory-layout format as well, which can come
-- in handy for bit-precise analysis.
data SMTConfig
SMTConfig :: Bool -> Timing -> Int -> Int -> String -> Maybe Int -> (String -> Bool) -> Maybe FilePath -> SMTLibVersion -> SMTSolver -> RoundingMode -> [SMTOption] -> Bool -> Maybe FilePath -> SMTConfig
-- | Debug mode
[verbose] :: SMTConfig -> Bool
-- | Print timing information on how long different phases took
-- (construction, solving, etc.)
[timing] :: SMTConfig -> Timing
-- | Print integral literals in this base (2, 10, and 16 are supported.)
[printBase] :: SMTConfig -> Int
-- | Print algebraic real values with this precision. (SReal, default: 16)
[printRealPrec] :: SMTConfig -> Int
-- | Usually "(check-sat)". However, users might tweak it based on solver
-- characteristics.
[satCmd] :: SMTConfig -> String
-- | In an allSat call, return at most this many models. If nothing, return
-- all.
[allSatMaxModelCount] :: SMTConfig -> Maybe Int
-- | When constructing a model, ignore variables whose name satisfy this
-- predicate. (Default: (const False), i.e., don't ignore anything)
[isNonModelVar] :: SMTConfig -> String -> Bool
-- | If Just, the entire interaction will be recorded as a playable file
-- (for debugging purposes mostly)
[transcript] :: SMTConfig -> Maybe FilePath
-- | What version of SMT-lib we use for the tool
[smtLibVersion] :: SMTConfig -> SMTLibVersion
-- | The actual SMT solver.
[solver] :: SMTConfig -> SMTSolver
-- | Rounding mode to use for floating-point conversions
[roundingMode] :: SMTConfig -> RoundingMode
-- | Options to set as we start the solver
[solverSetOptions] :: SMTConfig -> [SMTOption]
-- | If true, we shall ignore the exit code upon exit. Otherwise we require
-- ExitSuccess.
[ignoreExitCode] :: SMTConfig -> Bool
-- | Redirect the verbose output to this file if given. If Nothing, stdout
-- is implied.
[redirectVerbose] :: SMTConfig -> Maybe FilePath
-- | Representation of SMTLib Program versions. As of June 2015, we're
-- dropping support for SMTLib1, and supporting SMTLib2 only. We keep
-- this data-type around in case SMTLib3 comes along and we want to
-- support 2 and 3 simultaneously.
data SMTLibVersion
SMTLib2 :: SMTLibVersion
-- | Solvers that SBV is aware of
data Solver
Z3 :: Solver
Yices :: Solver
Boolector :: Solver
CVC4 :: Solver
MathSAT :: Solver
ABC :: Solver
-- | An SMT solver
data SMTSolver
SMTSolver :: Solver -> String -> (SMTConfig -> [String]) -> SMTEngine -> SolverCapabilities -> SMTSolver
-- | The solver in use
[name] :: SMTSolver -> Solver
-- | The path to its executable
[executable] :: SMTSolver -> String
-- | Options to provide to the solver
[options] :: SMTSolver -> SMTConfig -> [String]
-- | The solver engine, responsible for interpreting solver output
[engine] :: SMTSolver -> SMTEngine
-- | Various capabilities of the solver
[capabilities] :: SMTSolver -> SolverCapabilities
-- | Default configuration for the Boolector SMT solver
boolector :: SMTConfig
-- | Default configuration for the CVC4 SMT Solver.
cvc4 :: SMTConfig
-- | Default configuration for the Yices SMT Solver.
yices :: SMTConfig
-- | Default configuration for the Z3 SMT solver
z3 :: SMTConfig
-- | Default configuration for the MathSAT SMT solver
mathSAT :: SMTConfig
-- | Default configuration for the ABC synthesis and verification tool.
abc :: SMTConfig
-- | The default configs corresponding to supported SMT solvers
defaultSolverConfig :: Solver -> SMTConfig
-- | The default solver used by SBV. This is currently set to z3.
defaultSMTCfg :: SMTConfig
-- | Check whether the given solver is installed and is ready to go. This
-- call does a simple call to the solver to ensure all is well.
sbvCheckSolverInstallation :: SMTConfig -> IO Bool
-- | Return the known available solver configs, installed on your machine.
sbvAvailableSolvers :: IO [SMTConfig]
-- | Mark an interim result as an output. Useful when constructing Symbolic
-- programs that return multiple values, or when the result is
-- programmatically computed.
outputSVal :: SVal -> Symbolic ()
-- | The code-generation monad. Allows for precise layout of input values
-- reference parameters (for returning composite values in languages such
-- as C), and return values.
data SBVCodeGen a
-- | Sets RTC (run-time-checks) for index-out-of-bounds, shift-with-large
-- value etc. on/off. Default: False.
cgPerformRTCs :: Bool -> SBVCodeGen ()
-- | Sets driver program run time values, useful for generating programs
-- with fixed drivers for testing. Default: None, i.e., use random
-- values.
cgSetDriverValues :: [Integer] -> SBVCodeGen ()
-- | Should we generate a driver program? Default: True. When a
-- library is generated, it will have a driver if any of the contituent
-- functions has a driver. (See compileToCLib.)
cgGenerateDriver :: Bool -> SBVCodeGen ()
-- | Should we generate a Makefile? Default: True.
cgGenerateMakefile :: Bool -> SBVCodeGen ()
-- | Creates an atomic input in the generated code.
svCgInput :: Kind -> String -> SBVCodeGen SVal
-- | Creates an array input in the generated code.
svCgInputArr :: Kind -> Int -> String -> SBVCodeGen [SVal]
-- | Creates an atomic output in the generated code.
svCgOutput :: String -> SVal -> SBVCodeGen ()
-- | Creates an array output in the generated code.
svCgOutputArr :: String -> [SVal] -> SBVCodeGen ()
-- | Creates a returned (unnamed) value in the generated code.
svCgReturn :: SVal -> SBVCodeGen ()
-- | Creates a returned (unnamed) array value in the generated code.
svCgReturnArr :: [SVal] -> SBVCodeGen ()
-- | Adds the given lines to the header file generated, useful for
-- generating programs with uninterpreted functions.
cgAddPrototype :: [String] -> SBVCodeGen ()
-- | Adds the given lines to the program file generated, useful for
-- generating programs with uninterpreted functions.
cgAddDecl :: [String] -> SBVCodeGen ()
-- | Adds the given words to the compiler options in the generated
-- Makefile, useful for linking extra stuff in.
cgAddLDFlags :: [String] -> SBVCodeGen ()
-- | Ignore assertions (those generated by sAssert calls) in the
-- generated C code
cgIgnoreSAssert :: Bool -> SBVCodeGen ()
-- | Sets number of bits to be used for representing the SInteger
-- type in the generated C code. The argument must be one of 8,
-- 16, 32, or 64. Note that this is
-- essentially unsafe as the semantics of unbounded Haskell integers
-- becomes reduced to the corresponding bit size, as typical in most C
-- implementations.
cgIntegerSize :: Int -> SBVCodeGen ()
-- | Sets the C type to be used for representing the SReal type in
-- the generated C code. The setting can be one of C's "float",
-- "double", or "long double", types, depending on the
-- precision needed. Note that this is essentially unsafe as the
-- semantics of infinite precision SReal values becomes reduced to the
-- corresponding floating point type in C, and hence it is subject to
-- rounding errors.
cgSRealType :: CgSRealType -> SBVCodeGen ()
-- | Possible mappings for the SReal type when translated to C. Used
-- in conjunction with the function cgSRealType. Note that the
-- particular characteristics of the mapped types depend on the platform
-- and the compiler used for compiling the generated C program. See
-- http://en.wikipedia.org/wiki/C_data_types for details.
data CgSRealType
-- |
-- float
--
CgFloat :: CgSRealType
-- |
-- double
--
CgDouble :: CgSRealType
-- |
-- long double
--
CgLongDouble :: CgSRealType
-- | Given a symbolic computation, render it as an equivalent collection of
-- files that make up a C program:
--
--
-- - The first argument is the directory name under which the files
-- will be saved. To save files in the current directory pass
-- Just ".". Use Nothing for printing to
-- stdout.
-- - The second argument is the name of the C function to
-- generate.
-- - The final argument is the function to be compiled.
--
--
-- Compilation will also generate a Makefile, a header file, and
-- a driver (test) program, etc.
compileToC :: Maybe FilePath -> String -> SBVCodeGen () -> IO ()
-- | Create code to generate a library archive (.a) from given symbolic
-- functions. Useful when generating code from multiple functions that
-- work together as a library.
--
--
-- - The first argument is the directory name under which the files
-- will be saved. To save files in the current directory pass
-- Just ".". Use Nothing for printing to
-- stdout.
-- - The second argument is the name of the archive to generate.
-- - The third argument is the list of functions to include, in the
-- form of function-name/code pairs, similar to the second and third
-- arguments of compileToC, except in a list.
--
compileToCLib :: Maybe FilePath -> String -> [(String, SBVCodeGen ())] -> IO ()
-- | Create SMT-Lib benchmarks. The first argument is the basename of the
-- file, we will automatically add ".smt2" per SMT-Lib2 convention. The
-- Bool argument controls whether this is a SAT instance, i.e.,
-- translate the query directly, or a PROVE instance, i.e., translate the
-- negated query.
generateSMTBenchmark :: Bool -> Symbolic SVal -> IO String