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

Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Solver.Adapter

Description

 
Synopsis

Documentation

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

defaultWriteSMTLIB2Features :: ProblemFeatures Source #

Default featues to use for writing SMTLIB2 files.

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.