| Copyright | (c) Galois Inc 2014-2020 |
|---|---|
| License | BSD3 |
| Maintainer | Rob Dockins <rdockins@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| 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 :: Text -> 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) -> ResponseStrictness -> 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 ()
- writeGetAbduct :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Term -> IO ()
- writeGetAbductNext :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
- writeCheckSynth :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
- runCheckSat :: forall b t a. SMTLib2Tweaks b => Session t b -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
- runGetAbducts :: SMTLib2Tweaks a => Session t a -> Int -> Text -> Term -> IO [String]
- 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 :: WriterConn t a -> IO Text
- getName :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
- nameResult :: WriterConn t a -> IO Text
- setProduceModels :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Bool -> IO ()
- smtLibEvalFuns :: forall t a. SMTLib2Tweaks a => Session t a -> SMTEvalFunctions (Writer a)
- smtlib2Options :: [ConfigDesc]
- parseFnModel :: sym ~ ExprBuilder t st fs => sym -> WriterConn t h -> [SomeSymFn sym] -> SExp -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
- parseFnValues :: sym ~ ExprBuilder t st fs => sym -> WriterConn t h -> [SomeSymFn sym] -> SExp -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym))
- newtype Logic = Logic Builder
- qf_bv :: Logic
- allSupported :: Logic
- hornLogic :: 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) -> IO ErrorBehavior
- supportsResetAssertions :: a -> Bool
- setDefaultLogicAndOptions :: WriterConn t (Writer a) -> IO ()
- newDefaultWriter :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer a))
- withSolver :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t a -> IO b) -> IO b
- runSolverInOverride :: a -> AcknowledgementAction t (Writer a) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b
- writeDefaultSMT2 :: SMTLib2Tweaks a => a -> String -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
- defaultFileWriter :: SMTLib2Tweaks a => a -> String -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> Handle -> IO (WriterConn t (Writer a))
- startSolver :: SMTLib2GenericSolver a => a -> AcknowledgementAction t (Writer a) -> (WriterConn t (Writer a) -> IO ()) -> SolverGoalTimeout -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> 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
- = SMTLib2Unsupported Command
- | SMTLib2Error Command Text
- | SMTLib2ParseError SMTLib2Intent [Command] Text
- | SMTLib2ResponseUnrecognized Command Text
- | SMTLib2InvalidResponse Command SMTLib2Intent SMTResponse
- 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) -> 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 :: Text -> 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 |
| -> ResponseStrictness | Be strict in parsing SMT solver responses? |
| -> 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 #
writeGetAbduct :: SMTLib2Tweaks a => WriterConn t (Writer a) -> Text -> Term -> IO () Source #
writeGetAbductNext :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO () Source #
writeCheckSynth :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO () Source #
Write check-synth command
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
runGetAbducts :: SMTLib2Tweaks a => Session t a -> Int -> Text -> Term -> IO [String] Source #
runGetAbducts s nm p n, returns n formulas (as strings) the disjunction of which entails p (along with all the assertions in the context)
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 :: WriterConn t a -> IO Text Source #
Get the result of a version query
getName :: SMTLib2Tweaks a => WriterConn t (Writer a) -> IO () Source #
nameResult :: WriterConn t a -> 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 #
smtlib2Options :: [ConfigDesc] Source #
parseFnModel :: sym ~ ExprBuilder t st fs => sym -> WriterConn t h -> [SomeSymFn sym] -> SExp -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym)) Source #
parseFnValues :: sym ~ ExprBuilder t st fs => sym -> WriterConn t h -> [SomeSymFn sym] -> SExp -> IO (MapF (SymFnWrapper sym) (SymFnWrapper sym)) Source #
Logic
Identifies the set of predefined sorts and operators available.
allSupported :: Logic Source #
Deprecated: Use allLogic instead
Set the logic to all supported logics.
all_supported :: Logic Source #
Deprecated: Use allLogic instead
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) -> IO ErrorBehavior Source #
supportsResetAssertions :: a -> Bool Source #
setDefaultLogicAndOptions :: WriterConn t (Writer a) -> IO () Source #
Arguments
| :: a | |
| -> AcknowledgementAction t (Writer a) | |
| -> ProblemFeatures | |
| -> Maybe (ConfigOption BaseBoolType) | strictness override configuration |
| -> ExprBuilder t st fs | |
| -> OutputStream Text | |
| -> InputStream Text | |
| -> IO (WriterConn t (Writer a)) |
Arguments
| :: a | |
| -> AcknowledgementAction t (Writer a) | |
| -> ProblemFeatures | |
| -> Maybe (ConfigOption BaseBoolType) | strictness override configuration |
| -> 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.
Arguments
| :: a | |
| -> AcknowledgementAction t (Writer a) | |
| -> ProblemFeatures | |
| -> Maybe (ConfigOption BaseBoolType) | strictness override configuration |
| -> ExprBuilder t st fs | |
| -> LogData | |
| -> [BoolExpr t] | |
| -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) | |
| -> IO b |
Instances
Arguments
| :: SMTLib2Tweaks a | |
| => a | |
| -> String | Name of solver for reporting. |
| -> ProblemFeatures | Features supported by solver |
| -> Maybe (ConfigOption BaseBoolType) | strictness override configuration |
| -> ExprBuilder t st fs | |
| -> Handle | |
| -> [BoolExpr t] | |
| -> IO () |
A default method for writing SMTLib2 problems without any solver-specific tweaks.
defaultFileWriter :: SMTLib2Tweaks a => a -> String -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> Handle -> IO (WriterConn t (Writer a)) Source #
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 |
| -> SolverGoalTimeout | |
| -> ProblemFeatures | |
| -> Maybe (ConfigOption BaseBoolType) | strictness override configuration |
| -> 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 SMTLib2Intent [Command] Text | |
| SMTLib2ResponseUnrecognized Command Text | |
| SMTLib2InvalidResponse Command SMTLib2Intent SMTResponse |
Instances
| Exception SMTLib2Exception Source # | |
Defined in What4.Protocol.SMTLib2.Response Methods toException :: SMTLib2Exception -> SomeException # | |
| Show SMTLib2Exception Source # | |
Defined in What4.Protocol.SMTLib2.Response Methods showsPrec :: Int -> SMTLib2Exception -> ShowS # show :: SMTLib2Exception -> String # showList :: [SMTLib2Exception] -> ShowS # | |
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) -> 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