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

What4.Solver.Boolector

Description

This module provides an interface for running Boolector and parsing the results back.

Synopsis

Documentation

data Boolector Source #

Constructors

Boolector 

Instances

Instances details
Show Boolector Source # 
Instance details

Defined in What4.Solver.Boolector

SMTLib2GenericSolver Boolector Source # 
Instance details

Defined in What4.Solver.Boolector

SMTLib2Tweaks Boolector Source # 
Instance details

Defined in What4.Solver.Boolector

OnlineSolver (Writer Boolector) Source # 
Instance details

Defined in What4.Solver.Boolector

withBoolector Source #

Arguments

:: ExprBuilder t st fs 
-> FilePath

Path to Boolector executable

-> LogData 
-> (Session t Boolector -> IO a)

Action to run

-> IO a 

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