what4-1.6.3: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2014-2023
LicenseBSD3
MaintainerRyan Scott <rscott@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Solver.Bitwuzla

Description

This module provides an interface for running Bitwuzla and parsing the results back.

Synopsis

Documentation

data Bitwuzla Source #

Constructors

Bitwuzla 

Instances

Instances details
Show Bitwuzla Source # 
Instance details

Defined in What4.Solver.Bitwuzla

Methods

showsPrec :: Int -> Bitwuzla -> ShowS

show :: Bitwuzla -> String

showList :: [Bitwuzla] -> ShowS

SMTLib2GenericSolver Bitwuzla Source # 
Instance details

Defined in What4.Solver.Bitwuzla

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. Bitwuzla -> ExprBuilder t st fs -> IO FilePath Source #

defaultSolverArgs :: forall t (st :: Type -> Type) fs. Bitwuzla -> ExprBuilder t st fs -> IO [String] Source #

defaultFeatures :: Bitwuzla -> ProblemFeatures Source #

getErrorBehavior :: Bitwuzla -> WriterConn t (Writer Bitwuzla) -> IO ErrorBehavior Source #

supportsResetAssertions :: Bitwuzla -> Bool Source #

setDefaultLogicAndOptions :: WriterConn t (Writer Bitwuzla) -> IO () Source #

newDefaultWriter :: forall t (st :: Type -> Type) fs. Bitwuzla -> AcknowledgementAction t (Writer Bitwuzla) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Bitwuzla)) Source #

withSolver :: forall t (st :: Type -> Type) fs b. Bitwuzla -> AcknowledgementAction t (Writer Bitwuzla) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t Bitwuzla -> IO b) -> IO b Source #

runSolverInOverride :: forall t (st :: Type -> Type) fs b. Bitwuzla -> AcknowledgementAction t (Writer Bitwuzla) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #

SMTLib2Tweaks Bitwuzla Source # 
Instance details

Defined in What4.Solver.Bitwuzla

OnlineSolver (Writer Bitwuzla) Source # 
Instance details

Defined in What4.Solver.Bitwuzla

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Bitwuzla)) Source #

shutdownSolverProcess :: SolverProcess scope (Writer Bitwuzla) -> IO (ExitCode, Text) Source #

bitwuzlaTimeout :: ConfigOption BaseIntegerType Source #

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

bitwuzlaAdapter :: forall (st :: Type -> Type). SolverAdapter st Source #

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

withBitwuzla Source #

Arguments

:: forall t (st :: Type -> Type) fs a. ExprBuilder t st fs 
-> FilePath

Path to Bitwuzla executable

-> LogData 
-> (Session t Bitwuzla -> IO a)

Action to run

-> IO a 

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