what4-1.5.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2020
LicenseBSD3
MaintainerAaron Tomb <atomb@galois.com>
Stabilityprovisional
Safe HaskellSafe-Inferred
LanguageHaskell2010

What4.Solver.ExternalABC

Description

ABC-specific tweaks to the basic SMT-LIB2 solver interface.

Synopsis

Documentation

data ExternalABC Source #

Constructors

ExternalABC 

Instances

Instances details
Show ExternalABC Source # 
Instance details

Defined in What4.Solver.ExternalABC

Methods

showsPrec :: Int -> ExternalABC -> ShowS

show :: ExternalABC -> String

showList :: [ExternalABC] -> ShowS

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

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 #