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

What4.Solver.CVC4

Description

CVC4-specific tweaks to the basic SMTLib2 solver interface.

Synopsis

Documentation

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

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

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 #

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 #

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.

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

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