1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Internals
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- 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.
--
-- NB. There are various coding invariants in SBV that are maintained
-- throughout the code. Indiscriminate use of functions in this module
-- can break those invariants. So, you are on your own if you do utilize
-- the functions here. (Unfortunately, what exactly those invariants are
-- is a very good but also a very difficult question to answer!)
-----------------------------------------------------------------------------
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Internals (
-- * Running symbolic programs /manually/
Result(..), SBVRunMode(..), IStage(..), QueryContext(..), VarContext(..), mkNewState
-- * Solver capabilities
, SolverCapabilities(..)
-- * Internal structures useful for low-level programming
, module Data.SBV.Core.Data
-- * Operations useful for instantiating SBV type classes
, genLiteral, genFromCV, CV(..), genMkSymVar, genParse, showModel, SMTModel(..), liftQRem, liftDMod, registerKind, svToSV
, ProvableM(), SatisfiableM(), UICodeKind(..)
-- * Compilation to C, extras
, compileToC', compileToCLib'
-- * Code generation primitives
, module Data.SBV.Compilers.CodeGen
-- * Various math utilities around floats
, module Data.SBV.Utils.Numeric
-- * Pretty number printing
, module Data.SBV.Utils.PrettyNum
-- * Timing computations
, module Data.SBV.Utils.TDiff
-- * Coordinating with the solver
-- $coordinateSolverInfo
, sendStringToSolver, sendRequestToSolver, retrieveResponseFromSolver
-- * Defining new metrics
, addSValOptGoal
, sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord
, sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint
-- * lambdas and axioms
, lambda, lambdaStr, namedLambda, namedLambdaStr, constraint, constraintStr, Lambda(..), Constraint(..)
) where
import Control.Monad.IO.Class (MonadIO)
import Data.SBV.Core.Data hiding (Forall(..), Exists(..), ForallN(..), ExistsN(..), ExistsUnique(..), Skolemize(..), QNot(..))
import Data.SBV.Core.Kind (BVIsNonZero, ValidFloat)
import Data.SBV.Core.Sized (SWord)
import Data.SBV.Core.Model (genLiteral, genFromCV, genMkSymVar, liftQRem, liftDMod)
import Data.SBV.Core.Symbolic (IStage(..), QueryContext(..), MonadQuery, addSValOptGoal, registerKind, VarContext(..), svToSV, mkNewState, UICodeKind(..))
import Data.SBV.Core.Floating ( sFloatAsComparableSWord32, sDoubleAsComparableSWord64, sFloatingPointAsComparableSWord)
import qualified Data.SBV.Core.Floating as CF (sComparableSWord32AsSFloat, sComparableSWord64AsSDouble, sComparableSWordAsSFloatingPoint)
import Data.SBV.Compilers.C (compileToC', compileToCLib')
import Data.SBV.Compilers.CodeGen
import Data.SBV.SMT.SMT (genParse, showModel)
import Data.SBV.Provers.Prover (ProvableM, SatisfiableM)
import Data.SBV.Utils.Numeric
import Data.SBV.Utils.TDiff
import Data.SBV.Utils.PrettyNum
import GHC.TypeLits
import qualified Data.SBV.Control.Utils as Query
import Data.SBV.Lambda
--- $setup
--- >>> -- For doctest purposes only:
--- >>> import Data.SBV
-- | 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 :: (MonadIO m, MonadQuery m) => String -> m ()
sendStringToSolver = Query.send False
-- | 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 :: (MonadIO m, MonadQuery m) => String -> Maybe Int -> m [String]
retrieveResponseFromSolver = Query.retrieveResponse
-- | 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 :: (MonadIO m, MonadQuery m) => String -> m String
sendRequestToSolver = Query.ask
{- $coordinateSolverInfo
In rare cases it might be necessary to send an arbitrary string down to the solver. Needless to say, this
should be avoided if at all possible. Users should prefer the provided API. If you do find yourself
needing 'Data.SBV.Control.Utils.send' and 'Data.SBV.Control.Utils.ask' directly, please get in touch to see if SBV can support a typed API for your use case.
Similarly, the function 'retrieveResponseFromSolver' might occasionally be necessary to clean-up the communication
buffer. We would like to hear if you do need these functions regularly so we can provide better support.
-}
-- | Inverse transformation to 'sFloatAsComparableSWord32'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@.
-- Otherwise, it's faithful:
--
-- >>> prove $ \x -> let f = sComparableSWord32AsSFloat x in fpIsNaN f .|| fpIsNegativeZero f .|| sFloatAsComparableSWord32 f .== x
-- Q.E.D.
-- >>> prove $ \x -> fpIsNegativeZero x .|| sComparableSWord32AsSFloat (sFloatAsComparableSWord32 x) `fpIsEqualObject` x
-- Q.E.D.
sComparableSWord32AsSFloat :: SWord32 -> SFloat
sComparableSWord32AsSFloat = CF.sComparableSWord32AsSFloat
-- | Inverse transformation to 'sDoubleAsComparableSWord64'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@.
-- Otherwise, it's faithful:
--
-- >>> prove $ \x -> let d = sComparableSWord64AsSDouble x in fpIsNaN d .|| fpIsNegativeZero d .|| sDoubleAsComparableSWord64 d .== x
-- Q.E.D.
-- >>> prove $ \x -> fpIsNegativeZero x .|| sComparableSWord64AsSDouble (sDoubleAsComparableSWord64 x) `fpIsEqualObject` x
-- Q.E.D.
sComparableSWord64AsSDouble :: SWord64 -> SDouble
sComparableSWord64AsSDouble = CF.sComparableSWord64AsSDouble
-- | Inverse transformation to 'sFloatingPointAsComparableSWord'. Note that this isn't a perfect inverse, since @-0@ maps to @0@ and back to @0@.
-- Otherwise, it's faithful:
--
-- >>> prove $ \x -> let d = sComparableSWordAsSFloatingPoint x in fpIsNaN d .|| fpIsNegativeZero d .|| sFloatingPointAsComparableSWord (d :: SFPHalf) .== x
-- Q.E.D.
-- >>> prove $ \x -> fpIsNegativeZero x .|| sComparableSWordAsSFloatingPoint (sFloatingPointAsComparableSWord x) `fpIsEqualObject` (x :: SFPHalf)
-- Q.E.D.
sComparableSWordAsSFloatingPoint :: forall eb sb. (KnownNat (eb + sb), BVIsNonZero (eb + sb), ValidFloat eb sb) => SWord (eb + sb) -> SFloatingPoint eb sb
sComparableSWordAsSFloatingPoint = CF.sComparableSWordAsSFloatingPoint
{- HLint ignore module "Use import/export shortcut" -}
|
