what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

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

data DReal Source #

Constructors

DReal |

#### Instances

Instances details

Show DReal Source # |
Instance details Defined in What4.Solver.DReal Methods showsPrec :: Int -> DReal -> ShowS Source # show :: DReal -> String Source # showList :: [DReal] -> ShowS Source #
SMTLib2Tweaks DReal Source # |

Instance details

Defined in What4.Solver.DReal

Methods

smtlib2tweaks :: DReal Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term) Source #

smtlib2arraySelect :: Term -> [Term] -> Term Source #

smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term Source #

smtlib2StringSort :: Sort Source #

smtlib2StringTerm :: Text -> Term Source #

smtlib2StringLength :: Term -> Term Source #

smtlib2StringAppend :: [Term] -> Term Source #

smtlib2StringContains :: Term -> Term -> Term Source #

smtlib2StringIndexOf :: Term -> Term -> Term -> Term Source #

smtlib2StringIsPrefixOf :: Term -> Term -> Term Source #

smtlib2StringIsSuffixOf :: Term -> Term -> Term Source #

smtlib2StringSubstring :: Term -> Term -> Term -> Term Source #

smtlib2StructSort :: [Sort] -> Sort Source #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

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 #

runDRealInOverride Source #

Arguments

:: ExprBuilder t st fs |
-> LogData |
-> [BoolExpr t] | propositions to check
-> (SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a) |
-> IO a |