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
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
|
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Control
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Control sublanguage for interacting with SMT solvers.
-----------------------------------------------------------------------------
{-# LANGUAGE ConstraintKinds #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Control (
-- $queryIntro
-- * User queries
ExtractIO(..), MonadQuery(..), Queriable(..), Fresh(..), Query, query
-- * Create a fresh variable
, freshVar_, freshVar
-- * Create a fresh array
, freshArray_, freshArray
-- * Checking satisfiability
, CheckSatResult(..), checkSat, ensureSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet
-- * Querying the solver
-- ** Extracting values
, getValue, registerUISMTFunction, getFunction, getUninterpretedValue, getModel, getAssignment, getSMTResult, getUnknownReason, getObservables
-- ** Extracting the unsat core
, getUnsatCore
-- ** Extracting a proof
, getProof
-- ** Extracting interpolants
, getInterpolantMathSAT, getInterpolantZ3
-- ** Getting abducts
, getAbduct, getAbductNext
-- ** Extracting assertions
, getAssertions
-- * Getting solver information
, SMTInfoFlag(..), SMTErrorBehavior(..), SMTInfoResponse(..)
, getInfo, getOption
-- * Entering and exiting assertion stack
, getAssertionStackDepth, push, pop, inNewAssertionStack
-- * Higher level tactics
, caseSplit
-- * Resetting the solver state
, resetAssertions
-- * Constructing assignments
, (|->)
-- * Terminating the query
, mkSMTResult
, exit
-- * Controlling the solver behavior
, ignoreExitCode, timeout
-- * Miscellaneous
, queryDebug
, echo
, io
-- * Solver options
, SMTOption(..)
) where
import Data.SBV.Core.Symbolic (MonadQuery(..), Query, Queriable(..), Fresh(..), Symbolic, QueryContext(..))
import Data.SBV.Control.BaseIO
import Data.SBV.Control.Query hiding ( getInfo, getOption, getUnknownReason, getObservables
, getSMTResult, getLexicographicOptResults
, getIndependentOptResults
, getParetoOptResults, getModel
, checkSatAssuming
, checkSatAssumingWithUnsatisfiableSet
, getAssertionStackDepth
, inNewAssertionStack, push, pop
, caseSplit, resetAssertions, echo, exit
, getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3
, getAbduct, getAbductNext
, getAssertions, getAssignment
, mkSMTResult, freshVar_, freshVar
, freshArray, freshArray_, checkSat, ensureSat
, checkSatUsing, getValue
, getUninterpretedValue, timeout, io)
import Data.SBV.Control.Utils (registerUISMTFunction)
import Data.SBV.Utils.ExtractIO (ExtractIO(..))
import qualified Data.SBV.Control.Utils as Trans
-- | Run a custom query
query :: Query a -> Symbolic a
query = Trans.executeQuery QueryExternal
{- $queryIntro
In certain cases, the user might want to take over the communication with the solver, programmatically
querying the engine and issuing commands accordingly. Queries can be extremely powerful as
they allow direct control of the solver. Here's a simple example:
@
module Test where
import Data.SBV
import Data.SBV.Control -- queries require this module to be imported!
test :: Symbolic (Maybe (Integer, Integer))
test = do x <- sInteger "x" -- a free variable named "x"
y <- sInteger "y" -- a free variable named "y"
-- require the sum to be 10
constrain $ x + y .== 10
-- Go into the Query mode
query $ do
-- Query the solver: Are the constraints satisfiable?
cs <- checkSat
case cs of
Unk -> error "Solver said unknown!"
DSat{} -> error "Solver said DSat!"
Unsat -> return Nothing -- no solution!
Sat -> -- Query the values:
do xv <- getValue x
yv <- getValue y
io $ putStrLn $ "Solver returned: " ++ show (xv, yv)
-- We can now add new constraints,
-- Or perform arbitrary computations and tell
-- the solver anything we want!
constrain $ x .> literal xv + literal yv
-- call checkSat again
csNew <- checkSat
case csNew of
Unk -> error "Solver said unknown!"
DSat{} -> error "Solver said DSat!"
Unsat -> return Nothing
Sat -> do xv2 <- getValue x
yv2 <- getValue y
return $ Just (xv2, yv2)
@
Note the type of @test@: it returns an optional pair of integers in the 'Symbolic' monad. We turn
it into an IO value with the 'Data.SBV.Control.runSMT' function: (There's also 'Data.SBV.Control.runSMTWith' that uses a user specified
solver instead of the default. Note that 'Data.SBV.Provers.z3' is best supported (and tested), if you use another solver your results may vary!)
@
pair :: IO (Maybe (Integer, Integer))
pair = runSMT test
@
When run, this can return:
@
*Test> pair
Solver returned: (10,0)
Just (11,-1)
@
demonstrating that the user has full contact with the solver and can guide it as the program executes. SBV
provides access to many SMTLib features in the query mode, as exported from this very module.
For other examples see:
- "Documentation.SBV.Examples.Queries.AllSat": Simulating SBV's 'Data.SBV.allSat' using queries.
- "Documentation.SBV.Examples.Queries.CaseSplit": Performing a case-split during a query.
- "Documentation.SBV.Examples.Queries.Enums": Using enumerations in queries.
- "Documentation.SBV.Examples.Queries.FourFours": Solution to a fun arithmetic puzzle, coded using queries.
- "Documentation.SBV.Examples.Queries.GuessNumber": The famous number guessing game.
- "Documentation.SBV.Examples.Queries.UnsatCore": Extracting unsat-cores using queries.
- "Documentation.SBV.Examples.Queries.Interpolants": Extracting interpolants using queries.
-}
|
