What4.Solver.CVC4

CVC4-specific tweaks to the basic SMTLib2 solver interface.

Documentation

data CVC4

Constructors

CVC4

Instances

Show CVC4

Defined in What4.Solver.CVC4

Methods

showsPrec :: Int -> CVC4 -> ShowS

show :: CVC4 -> String

showList :: [CVC4] -> ShowS

SMTLib2GenericSolver CVC4

Defined in What4.Solver.CVC4

Methods

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

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

defaultFeatures :: CVC4 -> ProblemFeatures

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

supportsResetAssertions :: CVC4 -> Bool

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

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

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

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

SMTLib2Tweaks CVC4

Defined in What4.Solver.CVC4

Methods

smtlib2tweaks :: CVC4

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 :: ByteString -> 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 CVC4)

Defined in What4.Solver.CVC4

Methods

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

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

cvc4Features :: ProblemFeatures

cvc4Adapter :: SolverAdapter st

cvc4Path :: ConfigOption (BaseStringType Unicode)

Path to cvc4

cvc4Timeout :: ConfigOption BaseIntegerType

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

cvc4Options :: [ConfigDesc]

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

withCVC4

Arguments

:: ExprBuilder t st fs

-> FilePath

Path to CVC4 executable

-> LogData

-> (Session t CVC4 -> IO a)

Action to run

-> IO a

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

writeCVC4SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()

writeMultiAsmpCVC4SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()