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

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Solver

Contents

- Solver Adapters
- ABC (external, via SMT-Lib2)
- Boolector
- CVC4
- CVC5
- DReal
- STP
- Yices
- Z3

Description

The module reexports the most commonly used types and operations for interacting with solvers.

Synopsis

- data SolverAdapter st = SolverAdapter {
  - solver_adapter_name :: !String
  - solver_adapter_config_options :: ![ConfigDesc]
  - solver_adapter_check_sat :: !(forall t fs a. ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a)
  - solver_adapter_write_smt2 :: !(forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())
  }
- type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)
- defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)
- solverAdapterOptions :: [SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st))
- data LogData = LogData {
  - logCallbackVerbose :: Int -> String -> IO ()
  - logVerbosity :: Int
  - logReason :: String
  - logHandle :: Maybe Handle
  }
- logCallback :: LogData -> String -> IO ()
- defaultLogData :: LogData
- smokeTest :: ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)
- module What4.SatResult
- data ExternalABC = ExternalABC
- externalABCAdapter :: SolverAdapter st
- abcPath :: ConfigOption (BaseStringType Unicode)
- abcOptions :: [ConfigDesc]
- runExternalABCInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
- writeABCSMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
- data Boolector = Boolector
- boolectorAdapter :: SolverAdapter st
- boolectorPath :: ConfigOption (BaseStringType Unicode)
- boolectorTimeout :: ConfigOption BaseIntegerType
- runBoolectorInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
- withBoolector :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t Boolector -> IO a) -> IO a
- boolectorOptions :: [ConfigDesc]
- boolectorFeatures :: ProblemFeatures
- data CVC4 = CVC4
- cvc4Adapter :: SolverAdapter st
- cvc4Path :: ConfigOption (BaseStringType Unicode)
- cvc4Timeout :: ConfigOption BaseIntegerType
- runCVC4InOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
- writeCVC4SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
- withCVC4 :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC4 -> IO a) -> IO a
- cvc4Options :: [ConfigDesc]
- cvc4Features :: ProblemFeatures
- data CVC5 = CVC5
- cvc5Adapter :: SolverAdapter st
- cvc5Path :: ConfigOption (BaseStringType Unicode)
- cvc5Timeout :: ConfigOption BaseIntegerType
- runCVC5InOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
- writeCVC5SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
- withCVC5 :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC5 -> IO a) -> IO a
- cvc5Options :: [ConfigDesc]
- cvc5Features :: ProblemFeatures
- data DReal = DReal
- type DRealBindings = Map Text (Either Bool (Maybe Rational, Maybe Rational))
- drealAdapter :: SolverAdapter st
- drealPath :: ConfigOption (BaseStringType Unicode)
- runDRealInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a) -> IO a
- writeDRealSMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
- data STP = STP
- stpAdapter :: SolverAdapter st
- stpPath :: ConfigOption (BaseStringType Unicode)
- stpTimeout :: ConfigOption BaseIntegerType
- runSTPInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
- withSTP :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t STP -> IO a) -> IO a
- stpOptions :: [ConfigDesc]
- stpFeatures :: ProblemFeatures
- yicesAdapter :: SolverAdapter t
- yicesPath :: ConfigOption (BaseStringType Unicode)
- yicesEnableMCSat :: ConfigOption BaseBoolType
- yicesEnableInteractive :: ConfigOption BaseBoolType
- yicesGoalTimeout :: ConfigOption BaseIntegerType
- runYicesInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t) () -> IO a) -> IO a
- writeYicesFile :: ExprBuilder t st fs -> FilePath -> BoolExpr t -> IO ()
- yicesOptions :: [ConfigDesc]
- yicesDefaultFeatures :: ProblemFeatures
- data Z3 = Z3
- z3Path :: ConfigOption (BaseStringType Unicode)
- z3Timeout :: ConfigOption BaseIntegerType
- z3Tactic :: ConfigOption (BaseStringType Unicode)
- z3TacticDefault :: Text
- z3Adapter :: SolverAdapter st
- runZ3InOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
- withZ3 :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t Z3 -> IO a) -> IO a
- z3Options :: [ConfigDesc]
- z3Features :: ProblemFeatures

# Solver Adapters

data SolverAdapter st Source #

The main interface for interacting with a solver in an "offline" fashion, which means that a new solver process is started for each query.

Constructors

SolverAdapter |

Fields

- solver_adapter_name :: !String
- solver_adapter_config_options :: ![ConfigDesc]

  Configuration options relevant to this solver adapter

- solver_adapter_check_sat :: !(forall t fs a. ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a)

  Operation to check the satisfiability of a formula. The final argument is a callback that calculates the ultimate result from a SatResult and operations for finding model values in the event of a SAT result. Note: the evaluation functions may cease to be avaliable after the callback completes, so any necessary information should be extracted from them before returning.

- solver_adapter_write_smt2 :: !(forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())

  Write an SMTLib2 problem instance onto the given handle, incorporating any solver-specific tweaks appropriate to this solver

#### Instances

Instances details

Show (SolverAdapter st) Source # |
Instance details Defined in What4.Solver.Adapter Methods showsPrec :: Int -> SolverAdapter st -> ShowS Source # show :: SolverAdapter st -> String Source # showList :: [SolverAdapter st] -> ShowS Source #
Eq (SolverAdapter st) Source # |
Instance details Defined in What4.Solver.Adapter Methods (==) :: SolverAdapter st -> SolverAdapter st -> Bool Source # (/=) :: SolverAdapter st -> SolverAdapter st -> Bool Source #
Ord (SolverAdapter st) Source # |

Instance details

Defined in What4.Solver.Adapter

Methods

compare :: SolverAdapter st -> SolverAdapter st -> Ordering Source #

(<) :: SolverAdapter st -> SolverAdapter st -> Bool Source #

(<=) :: SolverAdapter st -> SolverAdapter st -> Bool Source #

(>) :: SolverAdapter st -> SolverAdapter st -> Bool Source #

(>=) :: SolverAdapter st -> SolverAdapter st -> Bool Source #

max :: SolverAdapter st -> SolverAdapter st -> SolverAdapter st Source #

min :: SolverAdapter st -> SolverAdapter st -> SolverAdapter st Source #

type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational) Source #

Function that calculates upper and lower bounds for real-valued elements. This type is used for solvers (e.g., dReal) that give only approximate solutions.

defaultSolverAdapter :: ConfigOption (BaseStringType Unicode) Source #

solverAdapterOptions :: [SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st)) Source #

data LogData Source #

A collection of operations for producing output from solvers. Solvers can produce messages at varying verbosity levels that might be appropriate for user output by using the `logCallbackVerbose` operation. If a `logHandle` is provided, the entire interaction sequence with the solver will be mirrored into that handle.

Constructors

LogData |

Fields

- logCallbackVerbose :: Int -> String -> IO ()

  takes a verbosity and a message to log

- logVerbosity :: Int

  the default verbosity; typical default is 2

- logReason :: String

  the reason for performing the operation

- logHandle :: Maybe Handle

  handle on which to mirror solver input/responses

logCallback :: LogData -> String -> IO () Source #

defaultLogData :: LogData Source #

smokeTest :: ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException) Source #

Test the ability to interact with a solver by peforming a check-sat query on a trivially unsatisfiable problem.

module What4.SatResult

# ABC (external, via SMT-Lib2)

data ExternalABC Source #

Constructors

ExternalABC |

#### Instances

Instances details

Show ExternalABC Source # |
Instance details Defined in What4.Solver.ExternalABC Methods showsPrec :: Int -> ExternalABC -> ShowS Source # show :: ExternalABC -> String Source # showList :: [ExternalABC] -> ShowS 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 #

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 #

externalABCAdapter :: SolverAdapter st Source #

abcPath :: ConfigOption (BaseStringType Unicode) Source #

Path to ABC

abcOptions :: [ConfigDesc] Source #

runExternalABCInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a Source #

writeABCSMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #

# Boolector

data Boolector Source #

Constructors

Boolector |

#### Instances

Instances details

Show Boolector Source # |
Instance details Defined in What4.Solver.Boolector Methods showsPrec :: Int -> Boolector -> ShowS Source # show :: Boolector -> String Source # showList :: [Boolector] -> ShowS Source #
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 #

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 #

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 #

boolectorAdapter :: SolverAdapter st Source #

boolectorPath :: ConfigOption (BaseStringType Unicode) Source #

Path to boolector

boolectorTimeout :: ConfigOption BaseIntegerType Source #

Per-check timeout, in milliseconds (zero is none)

runBoolectorInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a Source #

withBoolector Source #

Arguments

:: ExprBuilder t st fs |
-> FilePath | Path to Boolector executable
-> LogData |
-> (Session t Boolector -> IO a) | Action to run
-> IO a |

Run Boolector in a session. Boolector will be configured to produce models, but otherwise left with the default configuration.

boolectorOptions :: [ConfigDesc] Source #

boolectorFeatures :: ProblemFeatures Source #

# CVC4

data CVC4 Source #

Constructors

CVC4 |

#### Instances

Instances details

Show CVC4 Source # |
Instance details Defined in What4.Solver.CVC4 Methods showsPrec :: Int -> CVC4 -> ShowS Source # show :: CVC4 -> String Source # showList :: [CVC4] -> ShowS 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 #

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 #

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 #

cvc4Adapter :: SolverAdapter st Source #

cvc4Path :: ConfigOption (BaseStringType Unicode) Source #

Path to cvc4

cvc4Timeout :: ConfigOption BaseIntegerType Source #

Per-check timeout, in milliseconds (zero is none)

runCVC4InOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a Source #

writeCVC4SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #

withCVC4 Source #

Arguments

:: ExprBuilder t st fs |
-> FilePath | Path to CVC4 executable
-> LogData |
-> (Session t CVC4 -> IO a) | Action to run
-> IO a |

Run CVC4 in a session. CVC4 will be configured to produce models, but otherwise left with the default configuration.

cvc4Options :: [ConfigDesc] Source #

cvc4Features :: ProblemFeatures Source #

# CVC5

data CVC5 Source #

Constructors

CVC5 |

#### Instances

Instances details

Show CVC5 Source # |
Instance details Defined in What4.Solver.CVC5 Methods showsPrec :: Int -> CVC5 -> ShowS Source # show :: CVC5 -> String Source # showList :: [CVC5] -> ShowS 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 #

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 #

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 #

cvc5Adapter :: SolverAdapter st Source #

cvc5Path :: ConfigOption (BaseStringType Unicode) Source #

Path to cvc5

cvc5Timeout :: ConfigOption BaseIntegerType Source #

Per-check timeout, in milliseconds (zero is none)

runCVC5InOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a Source #

writeCVC5SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #

withCVC5 Source #

Arguments

:: ExprBuilder t st fs |
-> FilePath | Path to cvc5 executable
-> LogData |
-> (Session t CVC5 -> IO a) | Action to run
-> IO a |

Run cvc5 in a session. cvc5 will be configured to produce models, but otherwise left with the default configuration.

cvc5Options :: [ConfigDesc] Source #

cvc5Features :: ProblemFeatures Source #

# DReal

data DReal Source #

Constructors

DReal |

#### Instances

Instances details

Show DReal Source # |
Instance details Defined in What4.Solver.DReal Methods showsPrec :: Int -> DReal -> ShowS Source # show :: DReal -> String Source # showList :: [DReal] -> ShowS 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 #

type DRealBindings = Map Text (Either Bool (Maybe Rational, Maybe Rational)) Source #

drealAdapter :: SolverAdapter st Source #

drealPath :: ConfigOption (BaseStringType Unicode) Source #

Path to dReal

runDRealInOverride Source #

Arguments

:: ExprBuilder t st fs |
-> LogData |
-> [BoolExpr t] | propositions to check
-> (SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a) |
-> IO a |

writeDRealSMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #

# STP

data STP Source #

Constructors

STP |

#### Instances

Instances details

Show STP Source # |
Instance details Defined in What4.Solver.STP Methods showsPrec :: Int -> STP -> ShowS Source # show :: STP -> String Source # showList :: [STP] -> ShowS 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 #

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 #

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 #

stpAdapter :: SolverAdapter st Source #

stpPath :: ConfigOption (BaseStringType Unicode) Source #

Path to stp

stpTimeout :: ConfigOption BaseIntegerType Source #

Per-check timeout, in milliseconds (zero is none)

runSTPInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a Source #

withSTP Source #

Arguments

:: ExprBuilder t st fs |
-> FilePath | Path to STP executable
-> LogData |
-> (Session t STP -> IO a) | Action to run
-> IO a |

Run STP in a session. STP will be configured to produce models, buth otherwise left with the default configuration.

stpOptions :: [ConfigDesc] Source #

stpFeatures :: ProblemFeatures Source #

# Yices

yicesAdapter :: SolverAdapter t Source #

yicesPath :: ConfigOption (BaseStringType Unicode) Source #

Path to yices

yicesEnableMCSat :: ConfigOption BaseBoolType Source #

Enable the MC-SAT solver

yicesEnableInteractive :: ConfigOption BaseBoolType Source #

Enable interactive mode (necessary for per-goal timeouts)

yicesGoalTimeout :: ConfigOption BaseIntegerType Source #

Set a per-goal timeout in seconds.

runYicesInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t) () -> IO a) -> IO a Source #

Run writer and get a yices result.

writeYicesFile Source #

Arguments

:: ExprBuilder t st fs | Builder for getting current bindings.
-> FilePath | Path to file
-> BoolExpr t | Predicate to check
-> IO () |

Write a yices file that checks the satisfiability of the given predicate.

yicesOptions :: [ConfigDesc] Source #

yicesDefaultFeatures :: ProblemFeatures Source #

# Z3

data Z3 Source #

Constructors

Z3 |

#### Instances

Instances details

Show Z3 Source # |
Instance details Defined in What4.Solver.Z3 Methods showsPrec :: Int -> Z3 -> ShowS Source # show :: Z3 -> String Source # showList :: [Z3] -> ShowS 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 #

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 #

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 #

z3Path :: ConfigOption (BaseStringType Unicode) Source #

Path to Z3

z3Timeout :: ConfigOption BaseIntegerType Source #

Per-check timeout, in milliseconds (zero is none)

z3Tactic :: ConfigOption (BaseStringType Unicode) Source #

Z3 tactic

z3TacticDefault :: Text Source #

z3Adapter :: SolverAdapter st Source #

runZ3InOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a Source #

withZ3 Source #

Arguments

:: ExprBuilder t st fs |
-> FilePath | Path to Z3 executable
-> LogData |
-> (Session t Z3 -> IO a) | Action to run
-> IO a |

Run Z3 in a session. Z3 will be configured to produce models, but otherwise left with the default configuration.

z3Options :: [ConfigDesc] Source #

z3Features :: ProblemFeatures Source #