what4-1.5.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2022
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellSafe-Inferred
LanguageHaskell2010

What4.Solver.CVC5

Description

CVC5-specific tweaks to the basic SMTLib2 solver interface.

Synopsis

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

SMTLib2Tweaks CVC5 Source # 
Instance details

Defined in What4.Solver.CVC5

OnlineSolver (Writer CVC5) Source # 
Instance details

Defined in What4.Solver.CVC5

cvc5Timeout :: ConfigOption BaseIntegerType Source #

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

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.

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 #