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
|
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Trans.Control
-- Copyright : (c) Brian Schroeder
-- Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- More generalized alternative to @Data.SBV.Control@ for advanced client use
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Trans.Control (
-- * User queries
ExtractIO(..), MonadQuery(..), QueryT, Query, query
-- * Create a fresh variable
, freshVar_, freshVar
-- * Create a fresh array
, freshArray_, freshArray, freshLambdaArray_, freshLambdaArray
-- * Checking satisfiability
, CheckSatResult(..), checkSat, ensureSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet
-- * Querying the solver
-- ** Extracting values
, getValue, 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(..), QueryT, Query, SymbolicT, QueryContext(..))
import Data.SBV.Control.Query
import Data.SBV.Control.Utils (queryDebug, executeQuery, getFunction)
import Data.SBV.Utils.ExtractIO
-- | Run a custom query.
query :: ExtractIO m => QueryT m a -> SymbolicT m a
query = executeQuery QueryExternal
|
