what4-1.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.Solver

Description

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

Synopsis

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

Instances

Instances details
Eq (SolverAdapter st) Source # 
Instance details

Defined in What4.Solver.Adapter

Ord (SolverAdapter st) Source # 
Instance details

Defined in What4.Solver.Adapter

Show (SolverAdapter st) Source # 
Instance details

Defined in What4.Solver.Adapter

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.

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

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.

ABC (external, via SMT-Lib2)

data ExternalABC Source #

Constructors

ExternalABC 

Instances

Instances details
Show ExternalABC Source # 
Instance details

Defined in What4.Solver.ExternalABC

SMTLib2GenericSolver ExternalABC Source # 
Instance details

Defined in What4.Solver.ExternalABC

SMTLib2Tweaks ExternalABC Source # 
Instance details

Defined in What4.Solver.ExternalABC

Boolector

data Boolector Source #

Constructors

Boolector 

Instances

Instances details
Show Boolector Source # 
Instance details

Defined in What4.Solver.Boolector

SMTLib2GenericSolver Boolector Source # 
Instance details

Defined in What4.Solver.Boolector

SMTLib2Tweaks Boolector Source # 
Instance details

Defined in What4.Solver.Boolector

OnlineSolver (Writer Boolector) Source # 
Instance details

Defined in What4.Solver.Boolector

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.

CVC4

data CVC4 Source #

Constructors

CVC4 

Instances

Instances details
Show CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

Methods

showsPrec :: Int -> CVC4 -> ShowS #

show :: CVC4 -> String #

showList :: [CVC4] -> ShowS #

SMTLib2GenericSolver CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

SMTLib2Tweaks CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

OnlineSolver (Writer CVC4) Source # 
Instance details

Defined in What4.Solver.CVC4

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.

DReal

runDRealInOverride Source #

Arguments

:: ExprBuilder t st fs 
-> LogData 
-> [BoolExpr t]

propositions to check

-> (SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a) 
-> IO a 

STP

data STP Source #

Constructors

STP 

Instances

Instances details
Show STP Source # 
Instance details

Defined in What4.Solver.STP

Methods

showsPrec :: Int -> STP -> ShowS #

show :: STP -> String #

showList :: [STP] -> ShowS #

SMTLib2GenericSolver STP Source # 
Instance details

Defined in What4.Solver.STP

SMTLib2Tweaks STP Source # 
Instance details

Defined in What4.Solver.STP

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 #

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.

Yices

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.

Z3

data Z3 Source #

Constructors

Z3 

Instances

Instances details
Show Z3 Source # 
Instance details

Defined in What4.Solver.Z3

Methods

showsPrec :: Int -> Z3 -> ShowS #

show :: Z3 -> String #

showList :: [Z3] -> ShowS #

SMTLib2GenericSolver Z3 Source # 
Instance details

Defined in What4.Solver.Z3

SMTLib2Tweaks Z3 Source # 
Instance details

Defined in What4.Solver.Z3

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 #

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.