what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

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

Contents

- Logic
- Type
- Term
- Solvers and External interface
- Solver version
- Re-exports
- Orphan instances

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 {
  - unSort :: Builder
  }
- arraySort :: Sort -> Sort -> Sort
- newtype Term = T {
  - renderTerm :: Builder
  }
- 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

data Writer a Source #

#### Instances

Instances details

OnlineSolver (Writer Boolector) Source # |
Instance details Defined in What4.Solver.Boolector Methods startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Boolector)) Source # shutdownSolverProcess :: SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text) Source #
OnlineSolver (Writer CVC4) Source # |
Instance details Defined in What4.Solver.CVC4 Methods startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer CVC4)) Source # shutdownSolverProcess :: SolverProcess scope (Writer CVC4) -> IO (ExitCode, Text) Source #
OnlineSolver (Writer CVC5) Source # |
Instance details Defined in What4.Solver.CVC5 Methods startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer CVC5)) Source # shutdownSolverProcess :: SolverProcess scope (Writer CVC5) -> IO (ExitCode, Text) Source #
OnlineSolver (Writer STP) Source # |
Instance details Defined in What4.Solver.STP Methods startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer STP)) Source # shutdownSolverProcess :: SolverProcess scope (Writer STP) -> IO (ExitCode, Text) Source #
OnlineSolver (Writer Z3) Source # |
Instance details Defined in What4.Solver.Z3 Methods startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Z3)) Source # shutdownSolverProcess :: SolverProcess scope (Writer Z3) -> IO (ExitCode, Text) Source #
SMTLib2Tweaks a => SMTReadWriter (Writer a) Source # |

Instance details

Defined in What4.Protocol.SMTLib2

Methods

smtEvalFuns :: WriterConn t (Writer a) -> InputStream Text -> SMTEvalFunctions (Writer a) Source #

smtSatResult :: f (Writer a) -> WriterConn t (Writer a) -> IO (SatResult () ()) Source #

smtUnsatCoreResult :: f (Writer a) -> WriterConn t (Writer a) -> IO [Text] Source #

smtAbductResult :: f (Writer a) -> WriterConn t (Writer a) -> Text -> Term (Writer a) -> IO String Source #

smtAbductNextResult :: f (Writer a) -> WriterConn t (Writer a) -> IO String Source #

smtUnsatAssumptionsResult :: f (Writer a) -> WriterConn t (Writer a) -> IO [(Bool, Text)] Source #

SMTLib2Tweaks a => SMTWriter (Writer a) Source # |

Instance details

Defined in What4.Protocol.SMTLib2

Methods

forallExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a) Source #

existsExpr :: [(Text, Some TypeMap)] -> Term (Writer a) -> Term (Writer a) Source #

arrayConstant :: Maybe (ArrayConstantFn (Term (Writer a))) Source #

arraySelect :: Term (Writer a) -> [Term (Writer a)] -> Term (Writer a) Source #

arrayUpdate :: Term (Writer a) -> [Term (Writer a)] -> Term (Writer a) -> Term (Writer a) Source #

commentCommand :: f (Writer a) -> Builder -> Command (Writer a) Source #

assertCommand :: f (Writer a) -> Term (Writer a) -> Command (Writer a) Source #

assertNamedCommand :: f (Writer a) -> Term (Writer a) -> Text -> Command (Writer a) Source #

pushCommand :: f (Writer a) -> Command (Writer a) Source #

popCommand :: f (Writer a) -> Command (Writer a) Source #

push2Command :: f (Writer a) -> Command (Writer a) Source #

pop2Command :: f (Writer a) -> Command (Writer a) Source #

popManyCommands :: f (Writer a) -> Int -> [Command (Writer a)] Source #

resetCommand :: f (Writer a) -> Command (Writer a) Source #

checkCommands :: f (Writer a) -> [Command (Writer a)] Source #

checkWithAssumptionsCommands :: f (Writer a) -> [Text] -> [Command (Writer a)] Source #

getUnsatAssumptionsCommand :: f (Writer a) -> Command (Writer a) Source #

getUnsatCoreCommand :: f (Writer a) -> Command (Writer a) Source #

getAbductCommand :: f (Writer a) -> Text -> Term (Writer a) -> Command (Writer a) Source #

getAbductNextCommand :: f (Writer a) -> Command (Writer a) Source #

setOptCommand :: f (Writer a) -> Text -> Text -> Command (Writer a) Source #

declareCommand :: forall f (args :: Ctx BaseType) (rtp :: BaseType). f (Writer a) -> Text -> Assignment TypeMap args -> TypeMap rtp -> Command (Writer a) Source #

defineCommand :: forall f (rtp :: BaseType). f (Writer a) -> Text -> [(Text, Some TypeMap)] -> TypeMap rtp -> Term (Writer a) -> Command (Writer a) Source #

synthFunCommand :: forall f (tp :: BaseType). f (Writer a) -> Text -> [(Text, Some TypeMap)] -> TypeMap tp -> Command (Writer a) Source #

declareVarCommand :: forall f (tp :: BaseType). f (Writer a) -> Text -> TypeMap tp -> Command (Writer a) Source #

constraintCommand :: f (Writer a) -> Term (Writer a) -> Command (Writer a) Source #

declareStructDatatype :: forall t (args :: Ctx BaseType). WriterConn t (Writer a) -> Assignment TypeMap args -> IO () Source #

structCtor :: forall (args :: Ctx BaseType). Assignment TypeMap args -> [Term (Writer a)] -> Term (Writer a) Source #

structProj :: forall (args :: Ctx BaseType) (tp :: BaseType). Assignment TypeMap args -> Index args tp -> Term (Writer a) -> Term (Writer a) Source #

stringTerm :: Text -> Term (Writer a) Source #

stringLength :: Term (Writer a) -> Term (Writer a) Source #

stringIndexOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringContains :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringIsPrefixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringIsSuffixOf :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringSubstring :: Term (Writer a) -> Term (Writer a) -> Term (Writer a) -> Term (Writer a) Source #

stringAppend :: [Term (Writer a)] -> Term (Writer a) Source #

resetDeclaredStructs :: WriterConn t (Writer a) -> IO () Source #

writeCommand :: WriterConn t (Writer a) -> Command (Writer a) -> IO () Source #

type Command (Writer a) Source # |
Instance details Defined in What4.Protocol.SMTLib2 type Command (Writer a) = Command
type Term (Writer a) Source # |
Instance details Defined in What4.Protocol.SMTLib2 type Term (Writer a) = Term

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

smtlib2tweaks

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

smtlib2StructProj Source #

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

smtlib2declareStructCmd :: Int -> Maybe Command Source #

#### Instances

Instances details

SMTLib2Tweaks Boolector Source # |

Instance details

Defined in What4.Solver.Boolector

Methods

smtlib2tweaks :: Boolector Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

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 #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

SMTLib2Tweaks CVC4 Source # |

Instance details

Defined in What4.Solver.CVC4

Methods

smtlib2tweaks :: CVC4 Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

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 #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

SMTLib2Tweaks CVC5 Source # |

Instance details

Defined in What4.Solver.CVC5

Methods

smtlib2tweaks :: CVC5 Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

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 #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

SMTLib2Tweaks DReal Source # |

Instance details

Defined in What4.Solver.DReal

Methods

smtlib2tweaks :: DReal Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

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 #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

SMTLib2Tweaks ExternalABC Source # |

Instance details

Defined in What4.Solver.ExternalABC

Methods

smtlib2tweaks :: ExternalABC Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

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 #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

SMTLib2Tweaks STP Source # |

Instance details

Defined in What4.Solver.STP

Methods

smtlib2tweaks :: STP Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

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 #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

SMTLib2Tweaks Z3 Source # |

Instance details

Defined in What4.Solver.Z3

Methods

smtlib2tweaks :: Z3 Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

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 #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

SMTLib2Tweaks () Source # |

Instance details

Defined in What4.Protocol.SMTLib2

Methods

smtlib2tweaks :: () Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

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 #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

newWriter Source #

Arguments

:: a |
-> OutputStream Text | Stream to write queries onto
-> InputStream Text | Input stream to read responses from (may be the `nullInput` stream if no responses are expected)
-> 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

runCheckSat 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

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

newtype Logic Source #

Identifies the set of predefined sorts and operators available.

Constructors

Logic Builder |

qf_bv :: Logic Source #

Use the QF_BV logic

allSupported :: Logic Source #

Deprecated: Use allLogic instead

Set the logic to all supported logics.

hornLogic :: Logic Source #

Use the Horn logic

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

newtype Sort Source #

Sort for SMTLIB expressions

Constructors

Sort |

Fields

- unSort :: Builder

arraySort :: Sort -> Sort -> Sort Source #

`arraySort a b` denotes the set of functions from `a` to be `b`.

# Term

newtype Term Source #

Denotes an expression in the SMT solver

Constructors

T |

Fields

- renderTerm :: Builder

#### Instances

Instances details

IsString Term Source # |
Instance details Defined in What4.Protocol.SMTLib2.Syntax Methods fromString :: String -> Term Source #
Monoid Term Source # |
Instance details Defined in What4.Protocol.SMTLib2.Syntax Methods mempty :: Term Source # mappend :: Term -> Term -> Term Source # mconcat :: [Term] -> Term Source #
Semigroup Term Source # |
Instance details Defined in What4.Protocol.SMTLib2.Syntax Methods (<>) :: Term -> Term -> Term Source # sconcat :: NonEmpty Term -> Term Source # stimes :: Integral b => b -> Term -> Term Source #
Num Term Source # |
Instance details Defined in What4.Protocol.SMTLib2 Methods (+) :: Term -> Term -> Term Source # (-) :: Term -> Term -> Term Source # (*) :: Term -> Term -> Term Source # negate :: Term -> Term Source # abs :: Term -> Term Source # signum :: Term -> Term Source # fromInteger :: Integer -> Term Source #
SupportTermOps Term Source # |

Instance details

Defined in What4.Protocol.SMTLib2

Methods

boolExpr :: Bool -> Term Source #

notExpr :: Term -> Term Source #

andAll :: [Term] -> Term Source #

orAll :: [Term] -> Term Source #

(.&&) :: Term -> Term -> Term Source #

(.||) :: Term -> Term -> Term Source #

(.==) :: Term -> Term -> Term Source #

(./=) :: Term -> Term -> Term Source #

impliesExpr :: Term -> Term -> Term Source #

letExpr :: [(Text, Term)] -> Term -> Term Source #

ite :: Term -> Term -> Term -> Term Source #

sumExpr :: [Term] -> Term Source #

termIntegerToReal :: Term -> Term Source #

termRealToInteger :: Term -> Term Source #

integerTerm :: Integer -> Term Source #

rationalTerm :: Rational -> Term Source #

(.<=) :: Term -> Term -> Term Source #

(.<) :: Term -> Term -> Term Source #

(.>) :: Term -> Term -> Term Source #

(.>=) :: Term -> Term -> Term Source #

intAbs :: Term -> Term Source #

intDiv :: Term -> Term -> Term Source #

intMod :: Term -> Term -> Term Source #

intDivisible :: Term -> Natural -> Term Source #

bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> Term Source #

bvNeg :: Term -> Term Source #

bvAdd :: Term -> Term -> Term Source #

bvSub :: Term -> Term -> Term Source #

bvMul :: Term -> Term -> Term Source #

bvSLe :: Term -> Term -> Term Source #

bvULe :: Term -> Term -> Term Source #

bvSLt :: Term -> Term -> Term Source #

bvULt :: Term -> Term -> Term Source #

bvUDiv :: Term -> Term -> Term Source #

bvURem :: Term -> Term -> Term Source #

bvSDiv :: Term -> Term -> Term Source #

bvSRem :: Term -> Term -> Term Source #

bvAnd :: Term -> Term -> Term Source #

bvOr :: Term -> Term -> Term Source #

bvXor :: Term -> Term -> Term Source #

bvNot :: Term -> Term Source #

bvShl :: Term -> Term -> Term Source #

bvLshr :: Term -> Term -> Term Source #

bvAshr :: Term -> Term -> Term Source #

bvConcat :: Term -> Term -> Term Source #

bvExtract :: forall (w :: Nat). NatRepr w -> Natural -> Natural -> Term -> Term Source #

bvTestBit :: forall (w :: Nat). NatRepr w -> Natural -> Term -> Term Source #

bvSumExpr :: forall (w :: Nat). NatRepr w -> [Term] -> Term Source #

floatTerm :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> Term Source #

floatNeg :: Term -> Term Source #

floatAbs :: Term -> Term Source #

floatSqrt :: RoundingMode -> Term -> Term Source #

floatAdd :: RoundingMode -> Term -> Term -> Term Source #

floatSub :: RoundingMode -> Term -> Term -> Term Source #

floatMul :: RoundingMode -> Term -> Term -> Term Source #

floatDiv :: RoundingMode -> Term -> Term -> Term Source #

floatRem :: Term -> Term -> Term Source #

floatFMA :: RoundingMode -> Term -> Term -> Term -> Term Source #

floatEq :: Term -> Term -> Term Source #

floatFpEq :: Term -> Term -> Term Source #

floatLe :: Term -> Term -> Term Source #

floatLt :: Term -> Term -> Term Source #

floatIsNaN :: Term -> Term Source #

floatIsInf :: Term -> Term Source #

floatIsZero :: Term -> Term Source #

floatIsPos :: Term -> Term Source #

floatIsNeg :: Term -> Term Source #

floatIsSubnorm :: Term -> Term Source #

floatIsNorm :: Term -> Term Source #

floatCast :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatRound :: RoundingMode -> Term -> Term Source #

floatFromBinary :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> Term -> Term Source #

bvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

sbvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

realToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatToBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToSBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToReal :: Term -> Term Source #

realIsInteger :: Term -> Term Source #

realDiv :: Term -> Term -> Term Source #

realSin :: Term -> Term Source #

realCos :: Term -> Term Source #

realTan :: Term -> Term Source #

realATan2 :: Term -> Term -> Term Source #

realSinh :: Term -> Term Source #

realCosh :: Term -> Term Source #

realTanh :: Term -> Term Source #

realExp :: Term -> Term Source #

realLog :: Term -> Term Source #

smtFnApp :: Term -> [Term] -> Term Source #

smtFnUpdate :: Maybe (Term -> [Term] -> Term -> Term) Source #

lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> Term -> Term) Source #

fromText :: Text -> Term Source #

arrayConst :: Sort -> Sort -> Term -> Term Source #

arraySelect :: Term -> Term -> Term Source #

arrayStore :: Term -> Term -> Term -> Term Source #

# Solvers and External interface

data Session t a Source #

This is an interactive session with an SMT solver

Constructors

Session |

Fields

- sessionWriter :: !(WriterConn t (Writer a))
- sessionResponse :: !(InputStream Text)

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 #

newDefaultWriter 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)) |

withSolver Source #

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.

runSolverInOverride Source #

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

Instances details

SMTLib2GenericSolver Boolector Source # |

Instance details

Defined in What4.Solver.Boolector

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. Boolector -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. Boolector -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: Boolector -> ProblemFeatures Source #

getErrorBehavior :: Boolector -> WriterConn t (Writer Boolector) -> IO ErrorBehavior Source #

supportsResetAssertions :: Boolector -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer Boolector) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Boolector)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t Boolector -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver CVC4 Source # |

Instance details

Defined in What4.Solver.CVC4

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. CVC4 -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. CVC4 -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: CVC4 -> ProblemFeatures Source #

getErrorBehavior :: CVC4 -> WriterConn t (Writer CVC4) -> IO ErrorBehavior Source #

supportsResetAssertions :: CVC4 -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer CVC4) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. CVC4 -> AcknowledgementAction t (Writer CVC4) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer CVC4)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. CVC4 -> AcknowledgementAction t (Writer CVC4) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC4 -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. CVC4 -> AcknowledgementAction t (Writer CVC4) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver CVC5 Source # |

Instance details

Defined in What4.Solver.CVC5

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. CVC5 -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. CVC5 -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: CVC5 -> ProblemFeatures Source #

getErrorBehavior :: CVC5 -> WriterConn t (Writer CVC5) -> IO ErrorBehavior Source #

supportsResetAssertions :: CVC5 -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer CVC5) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. CVC5 -> AcknowledgementAction t (Writer CVC5) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer CVC5)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. CVC5 -> AcknowledgementAction t (Writer CVC5) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC5 -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. CVC5 -> AcknowledgementAction t (Writer CVC5) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver ExternalABC Source # |

Instance details

Defined in What4.Solver.ExternalABC

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. ExternalABC -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. ExternalABC -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: ExternalABC -> ProblemFeatures Source #

getErrorBehavior :: ExternalABC -> WriterConn t (Writer ExternalABC) -> IO ErrorBehavior Source #

supportsResetAssertions :: ExternalABC -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer ExternalABC) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. ExternalABC -> AcknowledgementAction t (Writer ExternalABC) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer ExternalABC)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. ExternalABC -> AcknowledgementAction t (Writer ExternalABC) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t ExternalABC -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. ExternalABC -> AcknowledgementAction t (Writer ExternalABC) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver STP Source # |

Instance details

Defined in What4.Solver.STP

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. STP -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. STP -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: STP -> ProblemFeatures Source #

getErrorBehavior :: STP -> WriterConn t (Writer STP) -> IO ErrorBehavior Source #

supportsResetAssertions :: STP -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer STP) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. STP -> AcknowledgementAction t (Writer STP) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer STP)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. STP -> AcknowledgementAction t (Writer STP) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t STP -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. STP -> AcknowledgementAction t (Writer STP) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2GenericSolver Z3 Source # |

Instance details

Defined in What4.Solver.Z3

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. Z3 -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. Z3 -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: Z3 -> ProblemFeatures Source #

getErrorBehavior :: Z3 -> WriterConn t (Writer Z3) -> IO ErrorBehavior Source #

supportsResetAssertions :: Z3 -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer Z3) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. Z3 -> AcknowledgementAction t (Writer Z3) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Z3)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. Z3 -> AcknowledgementAction t (Writer Z3) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t Z3 -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. Z3 -> AcknowledgementAction t (Writer Z3) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

writeDefaultSMT2 Source #

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 #

startSolver 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

Instances details

Exception SMTLib2Exception Source # |
Instance details Defined in What4.Protocol.SMTLib2.Response Methods toException :: SMTLib2Exception -> SomeException Source # fromException :: SomeException -> Maybe SMTLib2Exception Source # displayException :: SMTLib2Exception -> String Source #
Show SMTLib2Exception Source # |
Instance details Defined in What4.Protocol.SMTLib2.Response Methods showsPrec :: Int -> SMTLib2Exception -> ShowS Source # show :: SMTLib2Exception -> String Source # showList :: [SMTLib2Exception] -> ShowS Source #

# 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

# Orphan instances

Num Term Source # |
Instance details Methods (+) :: Term -> Term -> Term Source # (-) :: Term -> Term -> Term Source # (*) :: Term -> Term -> Term Source # negate :: Term -> Term Source # abs :: Term -> Term Source # signum :: Term -> Term Source # fromInteger :: Integer -> Term Source #
SupportTermOps Term Source # |

Instance details

Methods

boolExpr :: Bool -> Term Source #

notExpr :: Term -> Term Source #

andAll :: [Term] -> Term Source #

orAll :: [Term] -> Term Source #

(.&&) :: Term -> Term -> Term Source #

(.||) :: Term -> Term -> Term Source #

(.==) :: Term -> Term -> Term Source #

(./=) :: Term -> Term -> Term Source #

impliesExpr :: Term -> Term -> Term Source #

letExpr :: [(Text, Term)] -> Term -> Term Source #

ite :: Term -> Term -> Term -> Term Source #

sumExpr :: [Term] -> Term Source #

termIntegerToReal :: Term -> Term Source #

termRealToInteger :: Term -> Term Source #

integerTerm :: Integer -> Term Source #

rationalTerm :: Rational -> Term Source #

(.<=) :: Term -> Term -> Term Source #

(.<) :: Term -> Term -> Term Source #

(.>) :: Term -> Term -> Term Source #

(.>=) :: Term -> Term -> Term Source #

intAbs :: Term -> Term Source #

intDiv :: Term -> Term -> Term Source #

intMod :: Term -> Term -> Term Source #

intDivisible :: Term -> Natural -> Term Source #

bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> Term Source #

bvNeg :: Term -> Term Source #

bvAdd :: Term -> Term -> Term Source #

bvSub :: Term -> Term -> Term Source #

bvMul :: Term -> Term -> Term Source #

bvSLe :: Term -> Term -> Term Source #

bvULe :: Term -> Term -> Term Source #

bvSLt :: Term -> Term -> Term Source #

bvULt :: Term -> Term -> Term Source #

bvUDiv :: Term -> Term -> Term Source #

bvURem :: Term -> Term -> Term Source #

bvSDiv :: Term -> Term -> Term Source #

bvSRem :: Term -> Term -> Term Source #

bvAnd :: Term -> Term -> Term Source #

bvOr :: Term -> Term -> Term Source #

bvXor :: Term -> Term -> Term Source #

bvNot :: Term -> Term Source #

bvShl :: Term -> Term -> Term Source #

bvLshr :: Term -> Term -> Term Source #

bvAshr :: Term -> Term -> Term Source #

bvConcat :: Term -> Term -> Term Source #

bvExtract :: forall (w :: Nat). NatRepr w -> Natural -> Natural -> Term -> Term Source #

bvTestBit :: forall (w :: Nat). NatRepr w -> Natural -> Term -> Term Source #

bvSumExpr :: forall (w :: Nat). NatRepr w -> [Term] -> Term Source #

floatTerm :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> Term Source #

floatNeg :: Term -> Term Source #

floatAbs :: Term -> Term Source #

floatSqrt :: RoundingMode -> Term -> Term Source #

floatAdd :: RoundingMode -> Term -> Term -> Term Source #

floatSub :: RoundingMode -> Term -> Term -> Term Source #

floatMul :: RoundingMode -> Term -> Term -> Term Source #

floatDiv :: RoundingMode -> Term -> Term -> Term Source #

floatRem :: Term -> Term -> Term Source #

floatFMA :: RoundingMode -> Term -> Term -> Term -> Term Source #

floatEq :: Term -> Term -> Term Source #

floatFpEq :: Term -> Term -> Term Source #

floatLe :: Term -> Term -> Term Source #

floatLt :: Term -> Term -> Term Source #

floatIsNaN :: Term -> Term Source #

floatIsInf :: Term -> Term Source #

floatIsZero :: Term -> Term Source #

floatIsPos :: Term -> Term Source #

floatIsNeg :: Term -> Term Source #

floatIsSubnorm :: Term -> Term Source #

floatIsNorm :: Term -> Term Source #

floatCast :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatRound :: RoundingMode -> Term -> Term Source #

floatFromBinary :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> Term -> Term Source #

bvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

sbvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

realToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatToBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToSBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToReal :: Term -> Term Source #

realIsInteger :: Term -> Term Source #

realDiv :: Term -> Term -> Term Source #

realSin :: Term -> Term Source #

realCos :: Term -> Term Source #

realTan :: Term -> Term Source #

realATan2 :: Term -> Term -> Term Source #

realSinh :: Term -> Term Source #

realCosh :: Term -> Term Source #

realTanh :: Term -> Term Source #

realExp :: Term -> Term Source #

realLog :: Term -> Term Source #

smtFnApp :: Term -> [Term] -> Term Source #

smtFnUpdate :: Maybe (Term -> [Term] -> Term -> Term) Source #

lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> Term -> Term) Source #

fromText :: Text -> Term Source #