what4-1.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Stabilityprovisional
Safe HaskellNone
LanguageHaskell2010

What4.Solver.CVC4

Description

CVC4-specific tweaks to the basic SMTLib2 solver interface.

Synopsis

Documentation

data CVC4 Source #

Constructors

CVC4 

Instances

Instances details
Show CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

Methods

showsPrec :: Int -> CVC4 -> ShowS #

show :: CVC4 -> String #

showList :: [CVC4] -> ShowS #

SMTLib2GenericSolver CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

SMTLib2Tweaks CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

OnlineSolver (Writer CVC4) Source # 
Instance details

Defined in What4.Solver.CVC4

cvc4Timeout :: ConfigOption BaseIntegerType Source #

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

withCVC4 Source #

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.