Copyright	(c) Galois Inc 2014-2020
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	None
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 # show :: DReal -> String # showList :: [DReal] -> ShowS #
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 :: ByteString -> 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