What4.Solver.Bitwuzla

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

Documentation

data Bitwuzla

Constructors

Bitwuzla

Instances

Show Bitwuzla

Defined in What4.Solver.Bitwuzla

Methods

showsPrec :: Int -> Bitwuzla -> ShowS

show :: Bitwuzla -> String

showList :: [Bitwuzla] -> ShowS

SMTLib2GenericSolver Bitwuzla

Defined in What4.Solver.Bitwuzla

Methods

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

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

defaultFeatures :: Bitwuzla -> ProblemFeatures

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

supportsResetAssertions :: Bitwuzla -> Bool

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

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

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

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

SMTLib2Tweaks Bitwuzla

Defined in What4.Solver.Bitwuzla

Methods

smtlib2tweaks :: Bitwuzla

smtlib2exitCommand :: Maybe Command

smtlib2arrayType :: [Sort] -> Sort -> Sort

smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term)

smtlib2arraySelect :: Term -> [Term] -> Term

smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term

smtlib2StringSort :: Sort

smtlib2StringTerm :: Text -> Term

smtlib2StringLength :: Term -> Term

smtlib2StringAppend :: [Term] -> Term

smtlib2StringContains :: Term -> Term -> Term

smtlib2StringIndexOf :: Term -> Term -> Term -> Term

smtlib2StringIsPrefixOf :: Term -> Term -> Term

smtlib2StringIsSuffixOf :: Term -> Term -> Term

smtlib2StringSubstring :: Term -> Term -> Term -> Term

smtlib2StructSort :: [Sort] -> Sort

smtlib2StructCtor :: [Term] -> Term

smtlib2StructProj :: Int -> Int -> Term -> Term

smtlib2declareStructCmd :: Int -> Maybe Command

OnlineSolver (Writer Bitwuzla)

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

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

bitwuzlaPath :: ConfigOption (BaseStringType Unicode)

Path to bitwuzla

bitwuzlaTimeout :: ConfigOption BaseIntegerType

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

bitwuzlaOptions :: [ConfigDesc]

bitwuzlaAdapter :: SolverAdapter st

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

withBitwuzla

Arguments

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

bitwuzlaFeatures :: ProblemFeatures