| Copyright | (c) Galois Inc 2014-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Rob Dockins <rdockins@galois.com> |
| Stability | provisional |
| Safe Haskell | None |
| Language | Haskell2010 |
What4.Protocol.SMTLib2
Description
This module defines operations for producing SMTLib2-compatible queries useful for interfacing with solvers that accecpt SMTLib2 as an input language.
Synopsis
- data Writer a
- class Show a => SMTLib2Tweaks a where
- smtlib2tweaks :: a
- smtlib2exitCommand :: Maybe Command
- smtlib2arrayType :: [Sort] -> Sort -> Sort
- smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term)
- smtlib2arraySelect :: Term -> [Term] -> Term
- smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term
- smtlib2StringSort :: Sort
- smtlib2StringTerm :: ByteString -> Term
- smtlib2StringLength :: Term -> Term
- smtlib2StringAppend :: [Term] -> Term
- smtlib2StringContains :: Term -> Term -> Term
- smtlib2StringIndexOf :: Term -> Term -> Term -> Term
- smtlib2StringIsPrefixOf :: Term -> Term -> Term
- smtlib2StringIsSuffixOf :: Term -> Term -> Term
- smtlib2StringSubstring :: Term -> Term -> Term -> Term
- smtlib2StructSort :: [Sort] -> Sort
- smtlib2StructCtor :: [Term] -> Term
- smtlib2StructProj :: Int -> Int -> Term -> Term
- smtlib2declareStructCmd :: Int -> Maybe Command
- newWriter :: a -> OutputStream Text -> InputStream Text -> AcknowledgementAction t (Writer a) -> String -> Bool -> ProblemFeatures -> Bool -> SymbolVarBimap t -> IO (WriterConn t (Writer a))
- writeCheckSat :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
- writeExit :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
- writeGetValue :: SMTLib2Tweaks a => WriterConn t (Writer a) -> [Term] -> IO ()
- runCheckSat :: forall b t a. SMTLib2Tweaks b => Session t b -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
- asSMT2Type :: forall a tp. SMTLib2Tweaks a => TypeMap tp -> Sort
- setOption :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Text -> IO ()
- getVersion :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
- versionResult :: SMTReadWriter h => f h -> InputStream Text -> IO Text
- getName :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
- nameResult :: SMTReadWriter h => f h -> InputStream Text -> IO Text
- setProduceModels :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Bool -> IO ()
- smtLibEvalFuns :: forall t a. SMTLib2Tweaks a => Session t a -> SMTEvalFunctions (Writer a)
- newtype Logic = Logic Builder
- qf_bv :: Logic
- allSupported :: Logic
- all_supported :: Logic
- setLogic :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Logic -> IO ()
- newtype Sort = Sort {}
- arraySort :: Sort -> Sort -> Sort
- newtype Term = T {}
- arrayConst :: Sort -> Sort -> Term -> Term
- arraySelect :: Term -> Term -> Term
- arrayStore :: Term -> Term -> Term -> Term
- data Session t a = Session {
- sessionWriter :: !(WriterConn t (Writer a))
- sessionResponse :: !(InputStream Text)
- class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where
- defaultSolverPath :: a -> ExprBuilder t st fs -> IO FilePath
- defaultSolverArgs :: a -> ExprBuilder t st fs -> IO [String]
- defaultFeatures :: a -> ProblemFeatures
- getErrorBehavior :: a -> WriterConn t (Writer a) -> InputStream Text -> IO ErrorBehavior
- supportsResetAssertions :: a -> Bool
- setDefaultLogicAndOptions :: WriterConn t (Writer a) -> IO ()
- newDefaultWriter :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer a))
- withSolver :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t a -> IO b) -> IO b
- runSolverInOverride :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b
- writeDefaultSMT2 :: SMTLib2Tweaks a => a -> String -> ProblemFeatures -> ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
- startSolver :: SMTLib2GenericSolver a => a -> AcknowledgementAction t (Writer a) -> (WriterConn t (Writer a) -> IO ()) -> ProblemFeatures -> Maybe Handle -> ExprBuilder t st fs -> IO (SolverProcess t (Writer a))
- shutdownSolver :: SMTLib2GenericSolver a => a -> SolverProcess t (Writer a) -> IO (ExitCode, Text)
- smtAckResult :: AcknowledgementAction t (Writer a)
- data SMTLib2Exception
- ppSolverVersionCheckError :: SolverVersionCheckError -> Doc ann
- ppSolverVersionError :: SolverVersionError -> Doc ann
- checkSolverVersion :: SMTLib2Tweaks solver => SolverProcess scope (Writer solver) -> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
- checkSolverVersion' :: SMTLib2Tweaks solver => Map Text SolverBounds -> SolverProcess scope (Writer solver) -> IO (Either SolverVersionCheckError (Maybe SolverVersionError))
- queryErrorBehavior :: SMTLib2Tweaks a => WriterConn t (Writer a) -> InputStream Text -> IO ErrorBehavior
- defaultSolverBounds :: Map Text SolverBounds
- data WriterConn t (h :: Type)
- assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
- supportedFeatures :: WriterConn t h -> ProblemFeatures
- nullAcknowledgementAction :: AcknowledgementAction t h
Documentation
Instances
class Show a => SMTLib2Tweaks a where Source #
This class exists so that solvers supporting the SMTLib2 format can support features that go slightly beyond the standard.
In particular, there is no standardized syntax for constant arrays (arrays
which map every index to the same value). Solvers that support the theory of
arrays and have custom syntax for constant arrays should implement
smtlib2arrayConstant. In addition, solvers may override the default
representation of complex numbers if necessary. The default is to represent
complex numbers as "(Array Bool Real)" and to build instances by updating a
constant array.
Minimal complete definition
Methods
smtlib2tweaks :: a Source #
smtlib2exitCommand :: Maybe Command Source #
smtlib2arrayType :: [Sort] -> Sort -> Sort Source #
Return a representation of the type associated with a (multi-dimensional) symbolic array.
By default, we encode symbolic arrays using a nested representation. If the solver, supports tuples/structs it may wish to change this.
smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term) Source #
smtlib2arraySelect :: Term -> [Term] -> Term Source #
smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term Source #
smtlib2StringSort :: Sort Source #
smtlib2StringTerm :: ByteString -> Term Source #
smtlib2StringLength :: Term -> Term Source #
smtlib2StringAppend :: [Term] -> Term Source #
smtlib2StringContains :: Term -> Term -> Term Source #
smtlib2StringIndexOf :: Term -> Term -> Term -> Term Source #
smtlib2StringIsPrefixOf :: Term -> Term -> Term Source #
smtlib2StringIsSuffixOf :: Term -> Term -> Term Source #
smtlib2StringSubstring :: Term -> Term -> Term -> Term Source #
smtlib2StructSort :: [Sort] -> Sort Source #
The sort of structs with the given field types.
By default, this uses SMTLIB2 datatypes and are not primitive to the language.
smtlib2StructCtor :: [Term] -> Term Source #
Construct a struct value from the given field values
Arguments
| :: Int | number of fields in the struct |
| -> Int | 0-based index of the struct field |
| -> Term | struct term to project from |
| -> Term |
Construct a struct field projection term
Instances
Arguments
| :: a | |
| -> OutputStream Text | Stream to write queries onto |
| -> InputStream Text | Input stream to read responses from
(may be the |
| -> AcknowledgementAction t (Writer a) | Action to run for consuming acknowledgement messages |
| -> String | Name of solver for reporting purposes. |
| -> Bool | Flag indicating if it is permitted to use "define-fun" when generating SMTLIB |
| -> ProblemFeatures | Indicates what features are supported by the solver |
| -> Bool | Indicates if quantifiers are supported. |
| -> SymbolVarBimap t | Variable bindings for names. |
| -> IO (WriterConn t (Writer a)) |
writeCheckSat :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO () Source #
Write check sat command
writeExit :: forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO () Source #
writeGetValue :: SMTLib2Tweaks a => WriterConn t (Writer a) -> [Term] -> IO () Source #
Arguments
| :: forall b t a. SMTLib2Tweaks b | |
| => Session t b | |
| -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) | Function for evaluating model. The evaluation should be complete before |
| -> IO a |
This function runs a check sat command
asSMT2Type :: forall a tp. SMTLib2Tweaks a => TypeMap tp -> Sort Source #
setOption :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Text -> IO () Source #
getVersion :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO () Source #
versionResult :: SMTReadWriter h => f h -> InputStream Text -> IO Text Source #
Get the result of a version query
getName :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO () Source #
nameResult :: SMTReadWriter h => f h -> InputStream Text -> IO Text Source #
Get the result of a version query
setProduceModels :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Bool -> IO () Source #
Set the produce models option (We typically want this)
smtLibEvalFuns :: forall t a. SMTLib2Tweaks a => Session t a -> SMTEvalFunctions (Writer a) Source #
Logic
Identifies the set of predefined sorts and operators available.
allSupported :: Logic Source #
Set the logic to all supported logics.
all_supported :: Logic Source #
Deprecated: Use allSupported
Set the logic to all supported logics.
setLogic :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Logic -> IO () Source #
Type
arraySort :: Sort -> Sort -> Sort Source #
arraySort a b denotes the set of functions from a to be b.
Term
Denotes an expression in the SMT solver
Constructors
| T | |
Fields | |
Instances
Solvers and External interface
This is an interactive session with an SMT solver
Constructors
| Session | |
Fields
| |
class (SMTLib2Tweaks a, Show a) => SMTLib2GenericSolver a where Source #
Minimal complete definition
defaultSolverPath, defaultSolverArgs, defaultFeatures, setDefaultLogicAndOptions
Methods
defaultSolverPath :: a -> ExprBuilder t st fs -> IO FilePath Source #
defaultSolverArgs :: a -> ExprBuilder t st fs -> IO [String] Source #
defaultFeatures :: a -> ProblemFeatures Source #
getErrorBehavior :: a -> WriterConn t (Writer a) -> InputStream Text -> IO ErrorBehavior Source #
supportsResetAssertions :: a -> Bool Source #
setDefaultLogicAndOptions :: WriterConn t (Writer a) -> IO () Source #
newDefaultWriter :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer a)) Source #
Arguments
| :: a | |
| -> AcknowledgementAction t (Writer a) | |
| -> ProblemFeatures | |
| -> ExprBuilder t st fs | |
| -> FilePath | Path to solver executable |
| -> LogData | |
| -> (Session t a -> IO b) | Action to run |
| -> IO b |
Run the solver in a session.
runSolverInOverride :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #
Instances
Arguments
| :: SMTLib2Tweaks a | |
| => a | |
| -> String | Name of solver for reporting. |
| -> ProblemFeatures | Features supported by solver |
| -> ExprBuilder t st fs | |
| -> Handle | |
| -> [BoolExpr t] | |
| -> IO () |
A default method for writing SMTLib2 problems without any solver-specific tweaks.
Arguments
| :: SMTLib2GenericSolver a | |
| => a | |
| -> AcknowledgementAction t (Writer a) | Action for acknowledging command responses |
| -> (WriterConn t (Writer a) -> IO ()) | Action for setting start-up-time options and logic |
| -> ProblemFeatures | |
| -> Maybe Handle | |
| -> ExprBuilder t st fs | |
| -> IO (SolverProcess t (Writer a)) |
shutdownSolver :: SMTLib2GenericSolver a => a -> SolverProcess t (Writer a) -> IO (ExitCode, Text) Source #
smtAckResult :: AcknowledgementAction t (Writer a) Source #
data SMTLib2Exception Source #
Constructors
| SMTLib2Unsupported Command | |
| SMTLib2Error Command Text | |
| SMTLib2ParseError [Command] Text |
Instances
| Show SMTLib2Exception Source # | |
Defined in What4.Protocol.SMTLib2 Methods showsPrec :: Int -> SMTLib2Exception -> ShowS # show :: SMTLib2Exception -> String # showList :: [SMTLib2Exception] -> ShowS # | |
| Exception SMTLib2Exception Source # | |
Defined in What4.Protocol.SMTLib2 Methods toException :: SMTLib2Exception -> SomeException # | |
Solver version
ppSolverVersionCheckError :: SolverVersionCheckError -> Doc ann Source #
ppSolverVersionError :: SolverVersionError -> Doc ann Source #
checkSolverVersion :: SMTLib2Tweaks solver => SolverProcess scope (Writer solver) -> IO (Either SolverVersionCheckError (Maybe SolverVersionError)) Source #
Ensure the solver's version falls within a known-good range.
checkSolverVersion' :: SMTLib2Tweaks solver => Map Text SolverBounds -> SolverProcess scope (Writer solver) -> IO (Either SolverVersionCheckError (Maybe SolverVersionError)) Source #
Ensure the solver's version falls within a known-good range.
queryErrorBehavior :: SMTLib2Tweaks a => WriterConn t (Writer a) -> InputStream Text -> IO ErrorBehavior Source #
Query the solver's error behavior setting
defaultSolverBounds :: Map Text SolverBounds Source #
Solver version bounds computed from "solverBounds.config"
Re-exports
data WriterConn t (h :: Type) Source #
assume :: SMTWriter h => WriterConn t h -> BoolExpr t -> IO () Source #
Write assume formula predicates for asserting predicate holds.
supportedFeatures :: WriterConn t h -> ProblemFeatures Source #
Indicates features supported by the solver.
nullAcknowledgementAction :: AcknowledgementAction t h Source #
An acknowledgement action that does nothing