{-# LANGUAGE DataKinds #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
module What4.Solver.DReal
( DReal(..)
, DRealBindings
, ExprRangeBindings
, getAvgBindings
, getBoundBindings
, drealPath
, drealOptions
, drealAdapter
, writeDRealSMT2File
, runDRealInOverride
) where
import Control.Concurrent
import Control.Exception
import Control.Lens(folded)
import Control.Monad
import Data.Attoparsec.ByteString.Char8 hiding (try)
import qualified Data.ByteString.UTF8 as UTF8
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Text.Encoding ( decodeUtf8 )
import Data.Text.Lazy (Text)
import qualified Data.Text.Lazy as Text
import qualified Data.Text.Lazy.Builder as Builder
import Numeric
import System.Exit
import System.IO
import System.IO.Error
import qualified System.IO.Streams as Streams
import qualified System.IO.Streams.Attoparsec as Streams
import System.Process
import What4.BaseTypes
import What4.Config
import What4.Solver.Adapter
import What4.Concrete
import What4.Interface
import What4.ProblemFeatures
import What4.SatResult
import What4.Expr.Builder
import What4.Expr.GroundEval
import qualified What4.Protocol.SMTLib2 as SMT2
import qualified What4.Protocol.SMTLib2.Response as RSP
import qualified What4.Protocol.SMTWriter as SMTWriter
import What4.Utils.Process
import What4.Utils.Streams (logErrorStream)
import What4.Utils.HandleReader
data DReal = DReal deriving Int -> DReal -> ShowS
[DReal] -> ShowS
DReal -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DReal] -> ShowS
$cshowList :: [DReal] -> ShowS
show :: DReal -> String
$cshow :: DReal -> String
showsPrec :: Int -> DReal -> ShowS
$cshowsPrec :: Int -> DReal -> ShowS
Show
drealPath :: ConfigOption (BaseStringType Unicode)
drealPath :: ConfigOption (BaseStringType Unicode)
drealPath = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"solver.dreal.path"
drealPathOLD :: ConfigOption (BaseStringType Unicode)
drealPathOLD :: ConfigOption (BaseStringType Unicode)
drealPathOLD = forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"dreal_path"
drealOptions :: [ConfigDesc]
drealOptions :: [ConfigDesc]
drealOptions =
let dpOpt :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
dpOpt ConfigOption (BaseStringType Unicode)
co = forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt ConfigOption (BaseStringType Unicode)
co
OptionStyle (BaseStringType Unicode)
executablePathOptSty
(forall a. a -> Maybe a
Just Doc Void
"Path to dReal executable")
(forall a. a -> Maybe a
Just (forall (si :: StringInfo).
StringLiteral si -> ConcreteVal ('BaseStringType si)
ConcreteString StringLiteral Unicode
"dreal"))
dp :: ConfigDesc
dp = ConfigOption (BaseStringType Unicode) -> ConfigDesc
dpOpt ConfigOption (BaseStringType Unicode)
drealPath
in [ ConfigDesc
dp
, [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
dp] forall a b. (a -> b) -> a -> b
$ ConfigOption (BaseStringType Unicode) -> ConfigDesc
dpOpt ConfigOption (BaseStringType Unicode)
drealPathOLD
] forall a. Semigroup a => a -> a -> a
<> [ConfigDesc]
SMT2.smtlib2Options
drealAdapter :: SolverAdapter st
drealAdapter :: forall (st :: Type -> Type). SolverAdapter st
drealAdapter =
SolverAdapter
{ solver_adapter_name :: String
solver_adapter_name = String
"dreal"
, solver_adapter_config_options :: [ConfigDesc]
solver_adapter_config_options = [ConfigDesc]
drealOptions
, solver_adapter_check_sat :: forall t fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
-> IO a)
-> IO a
solver_adapter_check_sat = \ExprBuilder t st fs
sym LogData
logData [BoolExpr t]
ps SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
cont ->
forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
-> IO a)
-> IO a
runDRealInOverride ExprBuilder t st fs
sym LogData
logData [BoolExpr t]
ps forall a b. (a -> b) -> a -> b
$ \SatResult (WriterConn t (Writer DReal), DRealBindings) ()
res ->
case SatResult (WriterConn t (Writer DReal), DRealBindings) ()
res of
Sat (WriterConn t (Writer DReal)
c,DRealBindings
m) -> do
GroundEvalFn t
evalFn <- forall t.
WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t)
getAvgBindings WriterConn t (Writer DReal)
c DRealBindings
m
ExprRangeBindings t
rangeFn <- forall t.
WriterConn t (Writer DReal)
-> DRealBindings -> IO (ExprRangeBindings t)
getBoundBindings WriterConn t (Writer DReal)
c DRealBindings
m
SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
cont (forall mdl core. mdl -> SatResult mdl core
Sat (GroundEvalFn t
evalFn, forall a. a -> Maybe a
Just ExprRangeBindings t
rangeFn))
Unsat ()
x -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
cont (forall mdl core. core -> SatResult mdl core
Unsat ()
x)
SatResult (WriterConn t (Writer DReal), DRealBindings) ()
Unknown -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
cont forall mdl core. SatResult mdl core
Unknown
, solver_adapter_write_smt2 :: forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
solver_adapter_write_smt2 = forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeDRealSMT2File
}
instance SMT2.SMTLib2Tweaks DReal where
smtlib2tweaks :: DReal
smtlib2tweaks = DReal
DReal
writeDRealSMT2File
:: ExprBuilder t st fs
-> Handle
-> [BoolExpr t]
-> IO ()
writeDRealSMT2File :: forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeDRealSMT2File ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps = do
SymbolVarBimap t
bindings <- forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
getSymbolVarBimap ExprBuilder t st fs
sym
OutputStream Text
out_str <- OutputStream ByteString -> IO (OutputStream Text)
Streams.encodeUtf8 forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
h
InputStream Text
in_str <- forall a. IO (InputStream a)
Streams.nullInput
let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
ResponseStrictness
strictness <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe ResponseStrictness
SMTWriter.Strict
(\ConcreteVal BaseBoolType
c -> if ConcreteVal BaseBoolType -> Bool
fromConcreteBool ConcreteVal BaseBoolType
c
then ResponseStrictness
SMTWriter.Strict
else ResponseStrictness
SMTWriter.Lenient) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
(forall (tp :: BaseType).
OptionSetting tp -> IO (Maybe (ConcreteVal tp))
getOption forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
RSP.strictSMTParsing Config
cfg)
WriterConn t (Writer DReal)
c <- forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> ResponseStrictness
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
SMT2.newWriter DReal
DReal OutputStream Text
out_str InputStream Text
in_str forall t h. AcknowledgementAction t h
SMTWriter.nullAcknowledgementAction ResponseStrictness
strictness String
"dReal"
Bool
False ProblemFeatures
useComputableReals Bool
False SymbolVarBimap t
bindings
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer DReal)
c Bool
True
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer DReal)
c (Builder -> Logic
SMT2.Logic Builder
"QF_NRA")
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [BoolExpr t]
ps (forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT2.assume WriterConn t (Writer DReal)
c)
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSat WriterConn t (Writer DReal)
c
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeExit WriterConn t (Writer DReal)
c
type DRealBindings = Map Text (Either Bool (Maybe Rational, Maybe Rational))
getAvgBindings :: SMT2.WriterConn t (SMT2.Writer DReal)
-> DRealBindings
-> IO (GroundEvalFn t)
getAvgBindings :: forall t.
WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t)
getAvgBindings WriterConn t (Writer DReal)
c DRealBindings
m = do
let evalBool :: Term -> m Bool
evalBool Term
tm =
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Builder -> Text
Builder.toLazyText (Term -> Builder
SMT2.renderTerm Term
tm)) DRealBindings
m of
Just (Right (Maybe Rational, Maybe Rational)
_) -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Expected Boolean variable"
Just (Left Bool
b) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
b
Maybe (Either Bool (Maybe Rational, Maybe Rational))
Nothing -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False
evalBV :: p -> p -> m a
evalBV p
_ p
_ = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not support bitvectors."
evalStr :: p -> m a
evalStr p
_ = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not support strings."
evalReal :: Term -> m Rational
evalReal Term
tm = do
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Builder -> Text
Builder.toLazyText (Term -> Builder
SMT2.renderTerm Term
tm)) DRealBindings
m of
Just (Right (Maybe Rational, Maybe Rational)
vs) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Maybe Rational, Maybe Rational) -> Rational
drealAvgBinding (Maybe Rational, Maybe Rational)
vs)
Just (Left Bool
_) -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Expected Real variable"
Maybe (Either Bool (Maybe Rational, Maybe Rational))
Nothing -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
0
evalFloat :: p -> p -> m a
evalFloat p
_ p
_ = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not support floats."
let evalFns :: SMTEvalFunctions (Writer DReal)
evalFns = SMTWriter.SMTEvalFunctions { smtEvalBool :: Term (Writer DReal) -> IO Bool
SMTWriter.smtEvalBool = forall {m :: Type -> Type}. MonadFail m => Term -> m Bool
evalBool
, smtEvalBV :: forall (w :: Nat). NatRepr w -> Term (Writer DReal) -> IO (BV w)
SMTWriter.smtEvalBV = forall {m :: Type -> Type} {p} {p} {a}.
MonadFail m =>
p -> p -> m a
evalBV
, smtEvalReal :: Term (Writer DReal) -> IO Rational
SMTWriter.smtEvalReal = forall {m :: Type -> Type}. MonadFail m => Term -> m Rational
evalReal
, smtEvalFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp
-> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
SMTWriter.smtEvalFloat = forall {m :: Type -> Type} {p} {p} {a}.
MonadFail m =>
p -> p -> m a
evalFloat
, smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper (Writer DReal))
SMTWriter.smtEvalBvArray = forall a. Maybe a
Nothing
, smtEvalString :: Term (Writer DReal) -> IO Text
SMTWriter.smtEvalString = forall {m :: Type -> Type} {p} {a}. MonadFail m => p -> m a
evalStr
}
forall t h.
SMTWriter h =>
WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
SMTWriter.smtExprGroundEvalFn WriterConn t (Writer DReal)
c SMTEvalFunctions (Writer DReal)
evalFns
getMaybeEval :: ((Maybe Rational, Maybe Rational) -> Maybe Rational)
-> SMT2.WriterConn t (SMT2.Writer DReal)
-> DRealBindings
-> IO (RealExpr t -> IO (Maybe Rational))
getMaybeEval :: forall t.
((Maybe Rational, Maybe Rational) -> Maybe Rational)
-> WriterConn t (Writer DReal)
-> DRealBindings
-> IO (RealExpr t -> IO (Maybe Rational))
getMaybeEval (Maybe Rational, Maybe Rational) -> Maybe Rational
proj WriterConn t (Writer DReal)
c DRealBindings
m = do
let evalBool :: Term -> m Bool
evalBool Term
tm =
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Builder -> Text
Builder.toLazyText (Term -> Builder
SMT2.renderTerm Term
tm)) DRealBindings
m of
Just (Right (Maybe Rational, Maybe Rational)
_) -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"expected boolean term"
Just (Left Bool
b) -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
b
Maybe (Either Bool (Maybe Rational, Maybe Rational))
Nothing -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"unbound boolean variable"
evalBV :: p -> p -> m a
evalBV p
_ p
_ = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not return Bitvector values."
evalStr :: p -> m a
evalStr p
_ = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not return string values."
evalReal :: Term -> IO Rational
evalReal Term
tm = do
case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Builder -> Text
Builder.toLazyText (Term -> Builder
SMT2.renderTerm Term
tm)) DRealBindings
m of
Just (Right (Maybe Rational, Maybe Rational)
v) ->
case (Maybe Rational, Maybe Rational) -> Maybe Rational
proj (Maybe Rational, Maybe Rational)
v of
Just Rational
x -> forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
x
Maybe Rational
Nothing -> forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError String
"unbound")
Just (Left Bool
_) -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"expected real variable"
Maybe (Either Bool (Maybe Rational, Maybe Rational))
Nothing -> forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError String
"unbound")
evalFloat :: p -> p -> m a
evalFloat p
_ p
_ = forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not support floats."
let evalFns :: SMTEvalFunctions (Writer DReal)
evalFns = SMTWriter.SMTEvalFunctions { smtEvalBool :: Term (Writer DReal) -> IO Bool
SMTWriter.smtEvalBool = forall {m :: Type -> Type}. MonadFail m => Term -> m Bool
evalBool
, smtEvalBV :: forall (w :: Nat). NatRepr w -> Term (Writer DReal) -> IO (BV w)
SMTWriter.smtEvalBV = forall {m :: Type -> Type} {p} {p} {a}.
MonadFail m =>
p -> p -> m a
evalBV
, smtEvalReal :: Term (Writer DReal) -> IO Rational
SMTWriter.smtEvalReal = Term -> IO Rational
evalReal
, smtEvalFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp
-> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
SMTWriter.smtEvalFloat = forall {m :: Type -> Type} {p} {p} {a}.
MonadFail m =>
p -> p -> m a
evalFloat
, smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper (Writer DReal))
SMTWriter.smtEvalBvArray = forall a. Maybe a
Nothing
, smtEvalString :: Term (Writer DReal) -> IO Text
SMTWriter.smtEvalString = forall {m :: Type -> Type} {p} {a}. MonadFail m => p -> m a
evalStr
}
GroundEvalFn forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
evalFn <- forall t h.
SMTWriter h =>
WriterConn t h -> SMTEvalFunctions h -> IO (GroundEvalFn t)
SMTWriter.smtExprGroundEvalFn WriterConn t (Writer DReal)
c SMTEvalFunctions (Writer DReal)
evalFns
let handler :: IOError -> IO (Maybe a)
handler IOError
e | IOError -> Bool
isUserError IOError
e
, IOError -> String
ioeGetErrorString IOError
e forall a. Eq a => a -> a -> Bool
== String
"unbound" = do
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
handler IOError
e = forall e a. Exception e => e -> IO a
throwIO IOError
e
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \RealExpr t
elt -> (forall a. a -> Maybe a
Just forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
evalFn RealExpr t
elt) forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` forall {a}. IOError -> IO (Maybe a)
handler
getBoundBindings :: SMT2.WriterConn t (SMT2.Writer DReal)
-> DRealBindings
-> IO (ExprRangeBindings t)
getBoundBindings :: forall t.
WriterConn t (Writer DReal)
-> DRealBindings -> IO (ExprRangeBindings t)
getBoundBindings WriterConn t (Writer DReal)
c DRealBindings
m = do
RealExpr t -> IO (Maybe Rational)
l_evalFn <- forall t.
((Maybe Rational, Maybe Rational) -> Maybe Rational)
-> WriterConn t (Writer DReal)
-> DRealBindings
-> IO (RealExpr t -> IO (Maybe Rational))
getMaybeEval forall a b. (a, b) -> a
fst WriterConn t (Writer DReal)
c DRealBindings
m
RealExpr t -> IO (Maybe Rational)
h_evalFn <- forall t.
((Maybe Rational, Maybe Rational) -> Maybe Rational)
-> WriterConn t (Writer DReal)
-> DRealBindings
-> IO (RealExpr t -> IO (Maybe Rational))
getMaybeEval forall a b. (a, b) -> b
snd WriterConn t (Writer DReal)
c DRealBindings
m
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \RealExpr t
e -> (,) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RealExpr t -> IO (Maybe Rational)
l_evalFn RealExpr t
e forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> RealExpr t -> IO (Maybe Rational)
h_evalFn RealExpr t
e
drealAvgBinding :: (Maybe Rational, Maybe Rational) -> Rational
drealAvgBinding :: (Maybe Rational, Maybe Rational) -> Rational
drealAvgBinding (Maybe Rational
Nothing, Maybe Rational
Nothing) = Rational
0
drealAvgBinding (Maybe Rational
Nothing, Just Rational
r) = Rational
r
drealAvgBinding (Just Rational
r, Maybe Rational
Nothing) = Rational
r
drealAvgBinding (Just Rational
r1, Just Rational
r2) = (Rational
r1forall a. Num a => a -> a -> a
+Rational
r2)forall a. Fractional a => a -> a -> a
/Rational
2
dRealResponse :: Parser (SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
dRealResponse :: Parser
(SatResult
[(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
dRealResponse =
forall (t :: Type -> Type) (m :: Type -> Type) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ do ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"unsat"
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall mdl core. core -> SatResult mdl core
Unsat ())
, do ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"unknown"
forall (m :: Type -> Type) a. Monad m => a -> m a
return forall mdl core. SatResult mdl core
Unknown
, do ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"delta-sat"
ByteString
_ <- (Char -> Bool) -> Parser ByteString
takeTill (\Char
c -> Char
c forall a. Eq a => a -> a -> Bool
== Char
'\n' Bool -> Bool -> Bool
|| Char
c forall a. Eq a => a -> a -> Bool
== Char
'\r')
Parser ()
endOfLine
[(Text, Either Bool (Maybe Rational, Maybe Rational))]
bs <- forall (m :: Type -> Type) a. MonadPlus m => m a -> m [a]
many' Parser (Text, Either Bool (Maybe Rational, Maybe Rational))
dRealBinding
forall t. Chunk t => Parser t ()
endOfInput
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall mdl core. mdl -> SatResult mdl core
Sat [(Text, Either Bool (Maybe Rational, Maybe Rational))]
bs)
]
dRealBinding :: Parser (Text, Either Bool (Maybe Rational, Maybe Rational))
dRealBinding :: Parser (Text, Either Bool (Maybe Rational, Maybe Rational))
dRealBinding = do
Parser ()
skipSpace
ByteString
nm <- (Char -> Bool) -> Parser ByteString
takeWhile1 (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace)
Parser ()
skipSpace
Char
_ <- Char -> Parser Char
char Char
':'
Parser ()
skipSpace
Either Bool (Maybe Rational, Maybe Rational)
val <- forall (t :: Type -> Type) (m :: Type -> Type) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum
[ do ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"False"
Parser ()
skipSpace
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left Bool
False)
, do ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"True"
Parser ()
skipSpace
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left Bool
True)
, do Maybe Rational
lo <- Parser (Maybe Rational)
dRealLoBound
Parser ()
skipSpace
Char
_ <- Char -> Parser Char
char Char
','
Parser ()
skipSpace
Maybe Rational
hi <- Parser (Maybe Rational)
dRealHiBound
Parser ()
skipSpace
Char
_ <- forall (f :: Type -> Type) a. Alternative f => a -> f a -> f a
option Char
' ' (Char -> Parser Char
char Char
';')
Parser ()
skipSpace
forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (Maybe Rational
lo,Maybe Rational
hi))
]
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Text -> Text
Text.fromStrict (ByteString -> Text
decodeUtf8 ByteString
nm),Either Bool (Maybe Rational, Maybe Rational)
val)
dRealLoBound :: Parser (Maybe Rational)
dRealLoBound :: Parser (Maybe Rational)
dRealLoBound = forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
choice
[ ByteString -> Parser ByteString
string ByteString
"(-inf" forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
, do Char
_ <- Char -> Parser Char
char Char
'['
Rational
sign <- forall (f :: Type -> Type) a. Alternative f => a -> f a -> f a
option Rational
1 (Char -> Parser Char
char Char
'-' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return (-Rational
1))
ByteString
num <- (Char -> Bool) -> Parser ByteString
takeWhile1 (\Char
c -> Char
c forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` (String
"0123456789+-eE." :: String))
case forall a. RealFrac a => ReadS a
readFloat (ByteString -> String
UTF8.toString ByteString
num) of
(Rational
x,String
""):[(Rational, String)]
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Rational
sign forall a. Num a => a -> a -> a
* Rational
x)
[(Rational, String)]
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"expected rational bound"
]
dRealHiBound :: Parser (Maybe Rational)
dRealHiBound :: Parser (Maybe Rational)
dRealHiBound = forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
choice
[ ByteString -> Parser ByteString
string ByteString
"inf)" forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
, do Rational
sign <- forall (f :: Type -> Type) a. Alternative f => a -> f a -> f a
option Rational
1 (Char -> Parser Char
char Char
'-' forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> forall (m :: Type -> Type) a. Monad m => a -> m a
return (-Rational
1))
ByteString
num <- (Char -> Bool) -> Parser ByteString
takeWhile1 (\Char
c -> Char
c forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` (String
"0123456789+-eE." :: String))
Char
_ <- Char -> Parser Char
char Char
']'
case forall a. RealFrac a => ReadS a
readFloat (ByteString -> String
UTF8.toString ByteString
num) of
(Rational
x,String
""):[(Rational, String)]
_ -> forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Rational
sign forall a. Num a => a -> a -> a
* Rational
x)
[(Rational, String)]
_ -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"expected rational bound"
]
runDRealInOverride
:: ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (SMT2.WriterConn t (SMT2.Writer DReal), DRealBindings) () -> IO a)
-> IO a
runDRealInOverride :: forall t (st :: Type -> Type) fs a.
ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
-> IO a)
-> IO a
runDRealInOverride ExprBuilder t st fs
sym LogData
logData [BoolExpr t]
ps SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a
modelFn = do
BoolExpr t
p <- forall sym s.
IsExprBuilder sym =>
sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
andAllOf ExprBuilder t st fs
sym forall (f :: Type -> Type) a. Foldable f => IndexedFold Int (f a) a
folded [BoolExpr t]
ps
String
solver_path <- ConfigOption (BaseStringType Unicode) -> Config -> IO String
findSolverPath ConfigOption (BaseStringType Unicode)
drealPath (forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym)
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
(SolverStartSATQuery -> SolverEvent
SolverStartSATQuery forall a b. (a -> b) -> a -> b
$ SolverStartSATQueryRec
{ satQuerySolverName :: String
satQuerySolverName = String
"dReal"
, satQueryReason :: String
satQueryReason = LogData -> String
logReason LogData
logData
})
forall a.
String
-> [String]
-> Maybe String
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
-> IO a
withProcessHandles String
solver_path [String
"--model", String
"--in", String
"--format", String
"smt2"] forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ \(Handle
in_h, Handle
out_h, Handle
err_h, ProcessHandle
ph) -> do
InputStream ByteString
err_stream <- Handle -> IO (InputStream ByteString)
Streams.handleToInputStream Handle
err_h
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ IO () -> IO ThreadId
forkIO forall a b. (a -> b) -> a -> b
$ InputStream ByteString -> (String -> IO ()) -> IO ()
logErrorStream InputStream ByteString
err_stream (LogData -> Int -> String -> IO ()
logCallbackVerbose LogData
logData Int
2)
LogData -> Int -> String -> IO ()
logCallbackVerbose LogData
logData Int
2 String
"Sending Satisfiability problem to dReal"
SymbolVarBimap t
bindings <- forall t (st :: Type -> Type) fs.
ExprBuilder t st fs -> IO (SymbolVarBimap t)
getSymbolVarBimap ExprBuilder t st fs
sym
OutputStream Text
out_str <-
case LogData -> Maybe Handle
logHandle LogData
logData of
Maybe Handle
Nothing -> OutputStream ByteString -> IO (OutputStream Text)
Streams.encodeUtf8 forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
in_h
Just Handle
aux_h ->
do OutputStream ByteString
aux_str <- Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
aux_h
OutputStream ByteString -> IO (OutputStream Text)
Streams.encodeUtf8 forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a. OutputStream a -> OutputStream a -> IO (OutputStream a)
teeOutputStream OutputStream ByteString
aux_str forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
in_h
InputStream Text
in_str <- forall a. IO (InputStream a)
Streams.nullInput
let cfg :: Config
cfg = forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
ResponseStrictness
strictness <- forall b a. b -> (a -> b) -> Maybe a -> b
maybe ResponseStrictness
SMTWriter.Strict
(\ConcreteVal BaseBoolType
c -> if ConcreteVal BaseBoolType -> Bool
fromConcreteBool ConcreteVal BaseBoolType
c
then ResponseStrictness
SMTWriter.Strict
else ResponseStrictness
SMTWriter.Lenient) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
(forall (tp :: BaseType).
OptionSetting tp -> IO (Maybe (ConcreteVal tp))
getOption forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (tp :: BaseType).
ConfigOption tp -> Config -> IO (OptionSetting tp)
getOptionSetting ConfigOption BaseBoolType
RSP.strictSMTParsing Config
cfg)
WriterConn t (Writer DReal)
c <- forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> ResponseStrictness
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
SMT2.newWriter DReal
DReal OutputStream Text
out_str InputStream Text
in_str forall t h. AcknowledgementAction t h
SMTWriter.nullAcknowledgementAction ResponseStrictness
strictness String
"dReal"
Bool
False ProblemFeatures
useComputableReals Bool
False SymbolVarBimap t
bindings
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Logic -> IO ()
SMT2.setLogic WriterConn t (Writer DReal)
c (Builder -> Logic
SMT2.Logic Builder
"QF_NRA")
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT2.assume WriterConn t (Writer DReal)
c BoolExpr t
p
InputStream ByteString
out_stream <- Handle -> IO (InputStream ByteString)
Streams.handleToInputStream Handle
out_h
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSat WriterConn t (Writer DReal)
c
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeExit WriterConn t (Writer DReal)
c
Handle -> IO ()
hClose Handle
in_h
LogData -> Int -> String -> IO ()
logCallbackVerbose LogData
logData Int
2 String
"Parsing result from solver"
Either
ParseException
(SatResult
[(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
msat_result <- forall e a. Exception e => IO a -> IO (Either e a)
try forall a b. (a -> b) -> a -> b
$ forall r. Parser r -> InputStream ByteString -> IO r
Streams.parseFromStream Parser
(SatResult
[(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
dRealResponse InputStream ByteString
out_stream
SatResult (WriterConn t (Writer DReal), DRealBindings) ()
res <-
case Either
ParseException
(SatResult
[(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
msat_result of
Left ex :: ParseException
ex@Streams.ParseException{} -> forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String
"Could not parse dReal result.", forall e. Exception e => e -> String
displayException ParseException
ex]
Right (Unsat ()) -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall mdl core. core -> SatResult mdl core
Unsat ())
Right SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
Unknown -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall mdl core. SatResult mdl core
Unknown
Right (Sat [(Text, Either Bool (Maybe Rational, Maybe Rational))]
bs) -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall mdl core. mdl -> SatResult mdl core
Sat (WriterConn t (Writer DReal)
c, forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Text, Either Bool (Maybe Rational, Maybe Rational))]
bs))
a
r <- SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a
modelFn SatResult (WriterConn t (Writer DReal), DRealBindings) ()
res
LogData -> Int -> String -> IO ()
logCallbackVerbose LogData
logData Int
2 String
"Waiting for dReal to exit"
ExitCode
ec <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
ph
case ExitCode
ec of
ExitCode
ExitSuccess -> do
LogData -> Int -> String -> IO ()
logCallbackVerbose LogData
logData Int
2 String
"dReal terminated."
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
(SolverEndSATQuery -> SolverEvent
SolverEndSATQuery forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec
{ satQueryResult :: SatResult () ()
satQueryResult = forall a b. SatResult a b -> SatResult () ()
forgetModelAndCore SatResult (WriterConn t (Writer DReal), DRealBindings) ()
res
, satQueryError :: Maybe String
satQueryError = forall a. Maybe a
Nothing
})
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
r
ExitFailure Int
exit_code ->
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail forall a b. (a -> b) -> a -> b
$ String
"dReal exited with unexpected code: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
exit_code