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.DReal

Description

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

Synopsis

Documentation

type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational) Source #

Function that calculates upper and lower bounds for real-valued elements. This type is used for solvers (e.g., dReal) that give only approximate solutions.

runDRealInOverride Source #

Arguments

:: ExprBuilder t st fs 
-> LogData 
-> [BoolExpr t]

propositions to check

-> (SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a) 
-> IO a