Copyright	(c) Galois Inc 2014-2023
License	BSD3
Maintainer	Ryan Scott <[email protected]>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

What4.Solver.Bitwuzla

Description

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

Synopsis

data Bitwuzla = Bitwuzla
bitwuzlaPath :: ConfigOption (BaseStringType Unicode)
bitwuzlaTimeout :: ConfigOption BaseIntegerType
bitwuzlaOptions :: [ConfigDesc]
bitwuzlaAdapter :: forall (st :: Type -> Type). SolverAdapter st
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
withBitwuzla :: forall t (st :: Type -> Type) fs a. ExprBuilder t st fs -> FilePath -> LogData -> (Session t Bitwuzla -> IO a) -> IO a
bitwuzlaFeatures :: ProblemFeatures

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 Methods smtlib2tweaks :: Bitwuzla Source # smtlib2exitCommand :: Maybe Command Source # smtlib2arrayType :: [Sort] -> Sort -> Sort Source # smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term) Source # smtlib2arraySelect :: Term -> [Term] -> Term Source # smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term Source # smtlib2StringSort :: Sort Source # smtlib2StringTerm :: Text -> Term Source # smtlib2StringLength :: Term -> Term Source # smtlib2StringAppend :: [Term] -> Term Source # smtlib2StringContains :: Term -> Term -> Term Source # smtlib2StringIndexOf :: Term -> Term -> Term -> Term Source # smtlib2StringIsPrefixOf :: Term -> Term -> Term Source # smtlib2StringIsSuffixOf :: Term -> Term -> Term Source # smtlib2StringSubstring :: Term -> Term -> Term -> Term Source # smtlib2StructSort :: [Sort] -> Sort Source # smtlib2StructCtor :: [Term] -> Term Source # smtlib2StructProj :: Int -> Int -> Term -> Term Source # smtlib2declareStructCmd :: Int -> Maybe Command Source #
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 #

bitwuzlaPath :: ConfigOption (BaseStringType Unicode) Source #

Path to bitwuzla

bitwuzlaTimeout :: ConfigOption BaseIntegerType Source #

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

bitwuzlaOptions :: [ConfigDesc] Source #

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.

bitwuzlaFeatures :: ProblemFeatures Source #