Copyright | (c) Galois Inc 2014-2020 |
---|---|
License | BSD3 |
Maintainer | Rob Dockins <rdockins@galois.com> |
Stability | provisional |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
What4.Solver.DReal
Description
This module provides an interface for running dReal and parsing the results back.
Synopsis
- data DReal = DReal
- type DRealBindings = Map Text (Either Bool (Maybe Rational, Maybe Rational))
- type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)
- getAvgBindings :: WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t)
- getBoundBindings :: WriterConn t (Writer DReal) -> DRealBindings -> IO (ExprRangeBindings t)
- drealPath :: ConfigOption (BaseStringType Unicode)
- drealOptions :: [ConfigDesc]
- drealAdapter :: SolverAdapter st
- writeDRealSMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
- runDRealInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a) -> IO a
Documentation
Constructors
DReal |
Instances
type DRealBindings = Map Text (Either Bool (Maybe Rational, Maybe Rational)) Source #
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.
getAvgBindings :: WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t) Source #
getBoundBindings :: WriterConn t (Writer DReal) -> DRealBindings -> IO (ExprRangeBindings t) Source #
drealPath :: ConfigOption (BaseStringType Unicode) Source #
Path to dReal
drealOptions :: [ConfigDesc] Source #
drealAdapter :: SolverAdapter st Source #
writeDRealSMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #
Arguments
:: ExprBuilder t st fs | |
-> LogData | |
-> [BoolExpr t] | propositions to check |
-> (SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a) | |
-> IO a |