Copyright	(c) Galois Inc 2020
License	BSD3
Maintainer	Aaron Tomb <[email protected]>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

What4.Solver.ExternalABC

Description

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

Synopsis

data ExternalABC = ExternalABC
externalABCAdapter :: forall (st :: Type -> Type). SolverAdapter st
abcPath :: ConfigOption (BaseStringType Unicode)
abcOptions :: [ConfigDesc]
runExternalABCInOverride :: forall t (st :: Type -> Type) fs a. ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
writeABCSMT2File :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()

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 Methods smtlib2tweaks :: ExternalABC 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 #

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

abcPath :: ConfigOption (BaseStringType Unicode) Source #

Path to ABC

abcOptions :: [ConfigDesc] Source #

runExternalABCInOverride :: 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 #

writeABCSMT2File :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #