Copyright	(c) Galois Inc 2022
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	Safe-Inferred
Language	Haskell2010

What4.Solver.CVC5

Description

CVC5-specific tweaks to the basic SMTLib2 solver interface.

Synopsis

data CVC5 = CVC5
cvc5Features :: ProblemFeatures
cvc5Adapter :: SolverAdapter st
cvc5Path :: ConfigOption (BaseStringType Unicode)
cvc5Timeout :: ConfigOption BaseIntegerType
cvc5Options :: [ConfigDesc]
runCVC5InOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
withCVC5 :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC5 -> IO a) -> IO a
writeCVC5SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeMultiAsmpCVC5SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
runCVC5SyGuS :: sym ~ ExprBuilder t st fs => sym -> LogData -> [SomeSymFn sym] -> [BoolExpr t] -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
withCVC5_SyGuS :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC5_SyGuS -> IO a) -> IO a
writeCVC5SyFile :: sym ~ ExprBuilder t st fs => sym -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO ()

Documentation

data CVC5 Source #

Constructors

CVC5

Instances

Instances details

Show CVC5 Source #
Instance details Defined in What4.Solver.CVC5 Methods showsPrec :: Int -> CVC5 -> ShowS # show :: CVC5 -> String # showList :: [CVC5] -> ShowS #
SMTLib2GenericSolver CVC5 Source #
Instance details Defined in What4.Solver.CVC5 Methods defaultSolverPath :: forall t (st :: Type -> Type) fs. CVC5 -> ExprBuilder t st fs -> IO FilePath Source # defaultSolverArgs :: forall t (st :: Type -> Type) fs. CVC5 -> ExprBuilder t st fs -> IO [String] Source # defaultFeatures :: CVC5 -> ProblemFeatures Source # getErrorBehavior :: CVC5 -> WriterConn t (Writer CVC5) -> IO ErrorBehavior Source # supportsResetAssertions :: CVC5 -> Bool Source # setDefaultLogicAndOptions :: WriterConn t (Writer CVC5) -> IO () Source # newDefaultWriter :: forall t (st :: Type -> Type) fs. CVC5 -> AcknowledgementAction t (Writer CVC5) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer CVC5)) Source # withSolver :: forall t (st :: Type -> Type) fs b. CVC5 -> AcknowledgementAction t (Writer CVC5) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC5 -> IO b) -> IO b Source # runSolverInOverride :: forall t (st :: Type -> Type) fs b. CVC5 -> AcknowledgementAction t (Writer CVC5) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #
SMTLib2Tweaks CVC5 Source #
Instance details Defined in What4.Solver.CVC5 Methods smtlib2tweaks :: CVC5 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 CVC5) Source #
Instance details Defined in What4.Solver.CVC5 Methods startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer CVC5)) Source # shutdownSolverProcess :: SolverProcess scope (Writer CVC5) -> IO (ExitCode, Text) Source #

cvc5Features :: ProblemFeatures Source #

cvc5Adapter :: SolverAdapter st Source #

cvc5Path :: ConfigOption (BaseStringType Unicode) Source #

Path to cvc5

cvc5Timeout :: ConfigOption BaseIntegerType Source #

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

cvc5Options :: [ConfigDesc] Source #

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

withCVC5 Source #

Arguments

:: ExprBuilder t st fs
-> FilePath	Path to cvc5 executable
-> LogData
-> (Session t CVC5 -> IO a)	Action to run
-> IO a

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

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

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

runCVC5SyGuS :: sym ~ ExprBuilder t st fs => sym -> LogData -> [SomeSymFn sym] -> [BoolExpr t] -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ()) Source #

Find a solution to a Syntax-Guided Synthesis (SyGuS) problem.

For more information, see the SyGuS standard.

withCVC5_SyGuS :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC5_SyGuS -> IO a) -> IO a Source #

Run CVC5 SyGuS in a session, with the default configuration.

writeCVC5SyFile :: sym ~ ExprBuilder t st fs => sym -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO () Source #