------------------------------------------------------------------------
-- |
-- module           : What4.Solver.DReal
-- Description      : Interface for running dReal
-- Copyright        : (c) Galois, Inc 2014-2020
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
--
-- This module provides an interface for running dReal and parsing
-- the results back.
------------------------------------------------------------------------
{-# 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.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
(Int -> DReal -> ShowS)
-> (DReal -> String) -> ([DReal] -> ShowS) -> Show DReal
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

-- | Path to dReal
drealPath :: ConfigOption (BaseStringType Unicode)
drealPath :: ConfigOption (BaseStringType Unicode)
drealPath = BaseTypeRepr (BaseStringType Unicode)
-> String -> ConfigOption (BaseStringType Unicode)
forall (tp :: BaseType).
BaseTypeRepr tp -> String -> ConfigOption tp
configOption BaseTypeRepr (BaseStringType Unicode)
forall k (f :: k -> Type) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr String
"dreal_path"

drealOptions :: [ConfigDesc]
drealOptions :: [ConfigDesc]
drealOptions =
  [ ConfigOption (BaseStringType Unicode)
-> OptionStyle (BaseStringType Unicode)
-> Maybe (Doc Void)
-> Maybe (ConcreteVal (BaseStringType Unicode))
-> ConfigDesc
forall (tp :: BaseType).
ConfigOption tp
-> OptionStyle tp
-> Maybe (Doc Void)
-> Maybe (ConcreteVal tp)
-> ConfigDesc
mkOpt
      ConfigOption (BaseStringType Unicode)
drealPath
      OptionStyle (BaseStringType Unicode)
executablePathOptSty
      (Doc Void -> Maybe (Doc Void)
forall a. a -> Maybe a
Just Doc Void
"Path to dReal executable")
      (ConcreteVal (BaseStringType Unicode)
-> Maybe (ConcreteVal (BaseStringType Unicode))
forall a. a -> Maybe a
Just (StringLiteral Unicode -> ConcreteVal (BaseStringType Unicode)
forall (si :: StringInfo).
StringLiteral si -> ConcreteVal (BaseStringType si)
ConcreteString StringLiteral Unicode
"dreal"))
  ]

drealAdapter :: SolverAdapter st
drealAdapter :: SolverAdapter st
drealAdapter =
  SolverAdapter :: forall (st :: Type -> Type).
String
-> [ConfigDesc]
-> (forall t fs a.
    ExprBuilder t st fs
    -> LogData
    -> [BoolExpr t]
    -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
        -> IO a)
    -> IO a)
-> (forall t fs.
    ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())
-> SolverAdapter st
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 ->
      ExprBuilder t st fs
-> LogData
-> [BoolExpr t]
-> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    -> IO a)
-> IO a
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)
 -> IO a)
-> (SatResult (WriterConn t (Writer DReal), DRealBindings) ()
    -> IO a)
-> IO a
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 <- WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t)
forall t.
WriterConn t (Writer DReal) -> DRealBindings -> IO (GroundEvalFn t)
getAvgBindings WriterConn t (Writer DReal)
c DRealBindings
m
             ExprRangeBindings t
rangeFn <- WriterConn t (Writer DReal)
-> DRealBindings -> IO (ExprRangeBindings t)
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 ((GroundEvalFn t, Maybe (ExprRangeBindings t))
-> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
forall mdl core. mdl -> SatResult mdl core
Sat (GroundEvalFn t
evalFn, ExprRangeBindings t -> Maybe (ExprRangeBindings t)
forall a. a -> Maybe a
Just ExprRangeBindings t
rangeFn))
           Unsat ()
x -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a
cont (() -> SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
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 SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) ()
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 fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
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 :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
writeDRealSMT2File ExprBuilder t st fs
sym Handle
h [BoolExpr t]
ps = do
  SymbolVarBimap t
bindings <- ExprBuilder t st fs -> IO (SymbolVarBimap t)
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 (OutputStream ByteString -> IO (OutputStream Text))
-> IO (OutputStream ByteString) -> IO (OutputStream Text)
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 <- IO (InputStream Text)
forall a. IO (InputStream a)
Streams.nullInput
  WriterConn t (Writer DReal)
c <- DReal
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer DReal)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer DReal))
forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
SMT2.newWriter DReal
DReal OutputStream Text
out_str InputStream Text
in_str AcknowledgementAction t (Writer DReal)
forall t h. AcknowledgementAction t h
SMTWriter.nullAcknowledgementAction String
"dReal"
          Bool
False ProblemFeatures
useComputableReals Bool
False SymbolVarBimap t
bindings
  WriterConn t (Writer DReal) -> Bool -> IO ()
forall a t.
SMTLib2Tweaks a =>
WriterConn t (Writer a) -> Bool -> IO ()
SMT2.setProduceModels WriterConn t (Writer DReal)
c Bool
True
  WriterConn t (Writer DReal) -> Logic -> IO ()
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")
  [BoolExpr t] -> (BoolExpr t -> IO ()) -> IO ()
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [BoolExpr t]
ps (WriterConn t (Writer DReal) -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT2.assume WriterConn t (Writer DReal)
c)
  WriterConn t (Writer DReal) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSat WriterConn t (Writer DReal)
c
  WriterConn t (Writer DReal) -> IO ()
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 :: 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 Text
-> DRealBindings
-> Maybe (Either Bool (Maybe Rational, Maybe Rational))
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)
_) -> String -> m Bool
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Expected Boolean variable"
          Just (Left Bool
b) -> Bool -> m Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
b
          Maybe (Either Bool (Maybe Rational, Maybe Rational))
Nothing -> Bool -> m Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
False
      evalBV :: p -> p -> m a
evalBV p
_ p
_ = String -> m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not support bitvectors."
      evalStr :: p -> m a
evalStr p
_ = String -> m a
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 Text
-> DRealBindings
-> Maybe (Either Bool (Maybe Rational, Maybe Rational))
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) -> Rational -> m Rational
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
_) -> String -> m Rational
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Expected Real variable"
          Maybe (Either Bool (Maybe Rational, Maybe Rational))
Nothing -> Rational -> m Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
0
      evalFloat :: p -> p -> m a
evalFloat p
_ p
_ = String -> m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not support floats."
  let evalFns :: SMTEvalFunctions (Writer DReal)
evalFns = SMTEvalFunctions :: forall h.
(Term h -> IO Bool)
-> (forall (w :: Nat). NatRepr w -> Term h -> IO (BV w))
-> (Term h -> IO Rational)
-> (forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp
    -> Term h -> IO (BV (FloatPrecisionBits fpp)))
-> Maybe (SMTEvalBVArrayWrapper h)
-> (Term h -> IO ByteString)
-> SMTEvalFunctions h
SMTWriter.SMTEvalFunctions { smtEvalBool :: Term (Writer DReal) -> IO Bool
SMTWriter.smtEvalBool = Term (Writer DReal) -> IO Bool
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 (w :: Nat). NatRepr w -> Term (Writer DReal) -> IO (BV w)
forall (m :: Type -> Type) p p a. MonadFail m => p -> p -> m a
evalBV
                                           , smtEvalReal :: Term (Writer DReal) -> IO Rational
SMTWriter.smtEvalReal = Term (Writer DReal) -> IO Rational
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 (fpp :: FloatPrecision).
FloatPrecisionRepr fpp
-> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
forall (m :: Type -> Type) p p a. MonadFail m => p -> p -> m a
evalFloat
                                           , smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper (Writer DReal))
SMTWriter.smtEvalBvArray = Maybe (SMTEvalBVArrayWrapper (Writer DReal))
forall a. Maybe a
Nothing
                                           , smtEvalString :: Term (Writer DReal) -> IO ByteString
SMTWriter.smtEvalString = Term (Writer DReal) -> IO ByteString
forall (m :: Type -> Type) p a. MonadFail m => p -> m a
evalStr
                                           }
  WriterConn t (Writer DReal)
-> SMTEvalFunctions (Writer DReal) -> IO (GroundEvalFn t)
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 :: ((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 Text
-> DRealBindings
-> Maybe (Either Bool (Maybe Rational, Maybe Rational))
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)
_) -> String -> m Bool
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"expected boolean term"
          Just (Left Bool
b) -> Bool -> m Bool
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
b
          Maybe (Either Bool (Maybe Rational, Maybe Rational))
Nothing -> String -> m Bool
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"unbound boolean variable"
      evalBV :: p -> p -> m a
evalBV p
_ p
_ = String -> m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not return Bitvector values."
      evalStr :: p -> m a
evalStr p
_ = String -> m a
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 Text
-> DRealBindings
-> Maybe (Either Bool (Maybe Rational, Maybe Rational))
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  -> Rational -> IO Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
x
              Maybe Rational
Nothing -> IOError -> IO Rational
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError String
"unbound")
          Just (Left Bool
_) -> String -> IO Rational
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"expected real variable"
          Maybe (Either Bool (Maybe Rational, Maybe Rational))
Nothing -> IOError -> IO Rational
forall e a. Exception e => e -> IO a
throwIO (String -> IOError
userError String
"unbound")
      evalFloat :: p -> p -> m a
evalFloat p
_ p
_ = String -> m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"dReal does not support floats."
  let evalFns :: SMTEvalFunctions (Writer DReal)
evalFns = SMTEvalFunctions :: forall h.
(Term h -> IO Bool)
-> (forall (w :: Nat). NatRepr w -> Term h -> IO (BV w))
-> (Term h -> IO Rational)
-> (forall (fpp :: FloatPrecision).
    FloatPrecisionRepr fpp
    -> Term h -> IO (BV (FloatPrecisionBits fpp)))
-> Maybe (SMTEvalBVArrayWrapper h)
-> (Term h -> IO ByteString)
-> SMTEvalFunctions h
SMTWriter.SMTEvalFunctions { smtEvalBool :: Term (Writer DReal) -> IO Bool
SMTWriter.smtEvalBool = Term (Writer DReal) -> IO Bool
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 (w :: Nat). NatRepr w -> Term (Writer DReal) -> IO (BV w)
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
Term (Writer DReal) -> IO Rational
evalReal
                                           , smtEvalFloat :: forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp
-> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
SMTWriter.smtEvalFloat = forall (fpp :: FloatPrecision).
FloatPrecisionRepr fpp
-> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
forall (m :: Type -> Type) p p a. MonadFail m => p -> p -> m a
evalFloat
                                           , smtEvalBvArray :: Maybe (SMTEvalBVArrayWrapper (Writer DReal))
SMTWriter.smtEvalBvArray = Maybe (SMTEvalBVArrayWrapper (Writer DReal))
forall a. Maybe a
Nothing
                                           , smtEvalString :: Term (Writer DReal) -> IO ByteString
SMTWriter.smtEvalString = Term (Writer DReal) -> IO ByteString
forall (m :: Type -> Type) p a. MonadFail m => p -> m a
evalStr
                                           }
  GroundEvalFn forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
evalFn <- WriterConn t (Writer DReal)
-> SMTEvalFunctions (Writer DReal) -> IO (GroundEvalFn t)
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 String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"unbound" = do
        Maybe a -> IO (Maybe a)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
      handler IOError
e = IOError -> IO (Maybe a)
forall e a. Exception e => e -> IO a
throwIO IOError
e
  (RealExpr t -> IO (Maybe Rational))
-> IO (RealExpr t -> IO (Maybe Rational))
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((RealExpr t -> IO (Maybe Rational))
 -> IO (RealExpr t -> IO (Maybe Rational)))
-> (RealExpr t -> IO (Maybe Rational))
-> IO (RealExpr t -> IO (Maybe Rational))
forall a b. (a -> b) -> a -> b
$ \RealExpr t
elt -> (Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational -> Maybe Rational) -> IO Rational -> IO (Maybe Rational)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RealExpr t -> IO (GroundValue BaseRealType)
forall (tp :: BaseType). Expr t tp -> IO (GroundValue tp)
evalFn RealExpr t
elt) IO (Maybe Rational)
-> (IOError -> IO (Maybe Rational)) -> IO (Maybe Rational)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` IOError -> IO (Maybe Rational)
forall a. IOError -> IO (Maybe a)
handler

getBoundBindings :: SMT2.WriterConn t (SMT2.Writer DReal)
                 -> DRealBindings
                 -> IO (ExprRangeBindings t)
getBoundBindings :: WriterConn t (Writer DReal)
-> DRealBindings -> IO (ExprRangeBindings t)
getBoundBindings WriterConn t (Writer DReal)
c DRealBindings
m = do
  RealExpr t -> IO (Maybe Rational)
l_evalFn <- ((Maybe Rational, Maybe Rational) -> Maybe Rational)
-> WriterConn t (Writer DReal)
-> DRealBindings
-> IO (RealExpr t -> IO (Maybe Rational))
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
forall a b. (a, b) -> a
fst WriterConn t (Writer DReal)
c DRealBindings
m
  RealExpr t -> IO (Maybe Rational)
h_evalFn <- ((Maybe Rational, Maybe Rational) -> Maybe Rational)
-> WriterConn t (Writer DReal)
-> DRealBindings
-> IO (RealExpr t -> IO (Maybe Rational))
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
forall a b. (a, b) -> b
snd WriterConn t (Writer DReal)
c DRealBindings
m
  ExprRangeBindings t -> IO (ExprRangeBindings t)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExprRangeBindings t -> IO (ExprRangeBindings t))
-> ExprRangeBindings t -> IO (ExprRangeBindings t)
forall a b. (a -> b) -> a -> b
$ \RealExpr t
e -> (,) (Maybe Rational
 -> Maybe Rational -> (Maybe Rational, Maybe Rational))
-> IO (Maybe Rational)
-> IO (Maybe Rational -> (Maybe Rational, Maybe Rational))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> RealExpr t -> IO (Maybe Rational)
l_evalFn RealExpr t
e IO (Maybe Rational -> (Maybe Rational, Maybe Rational))
-> IO (Maybe Rational) -> IO (Maybe Rational, Maybe Rational)
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
r1Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
+Rational
r2)Rational -> Rational -> Rational
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 =
  [Parser
   (SatResult
      [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())]
-> Parser
     (SatResult
        [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
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"
       SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
-> Parser
     (SatResult
        [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return (()
-> SatResult
     [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
forall mdl core. core -> SatResult mdl core
Unsat ())

  , do ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"unknown"
       SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
-> Parser
     (SatResult
        [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
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 Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\n' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\r')
       Parser ()
endOfLine
       [(Text, Either Bool (Maybe Rational, Maybe Rational))]
bs <- Parser
  ByteString (Text, Either Bool (Maybe Rational, Maybe Rational))
-> Parser
     ByteString [(Text, Either Bool (Maybe Rational, Maybe Rational))]
forall (m :: Type -> Type) a. MonadPlus m => m a -> m [a]
many' Parser
  ByteString (Text, Either Bool (Maybe Rational, Maybe Rational))
dRealBinding
       Parser ()
forall t. Chunk t => Parser t ()
endOfInput
       SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
-> Parser
     (SatResult
        [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
forall (m :: Type -> Type) a. Monad m => a -> m a
return ([(Text, Either Bool (Maybe Rational, Maybe Rational))]
-> SatResult
     [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
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
  ByteString (Text, Either Bool (Maybe Rational, Maybe Rational))
dRealBinding = do
    Parser ()
skipSpace

    ByteString
nm <- (Char -> Bool) -> Parser ByteString
takeWhile1 (Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
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 <- [Parser ByteString (Either Bool (Maybe Rational, Maybe Rational))]
-> Parser ByteString (Either Bool (Maybe Rational, Maybe Rational))
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
           Either Bool (Maybe Rational, Maybe Rational)
-> Parser ByteString (Either Bool (Maybe Rational, Maybe Rational))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool -> Either Bool (Maybe Rational, Maybe Rational)
forall a b. a -> Either a b
Left Bool
False)

      , do ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"True"
           Parser ()
skipSpace
           Either Bool (Maybe Rational, Maybe Rational)
-> Parser ByteString (Either Bool (Maybe Rational, Maybe Rational))
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Bool -> Either Bool (Maybe Rational, Maybe Rational)
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
_ <- Char -> Parser Char -> Parser Char
forall (f :: Type -> Type) a. Alternative f => a -> f a -> f a
option Char
' ' (Char -> Parser Char
char Char
';')
           Parser ()
skipSpace
           Either Bool (Maybe Rational, Maybe Rational)
-> Parser ByteString (Either Bool (Maybe Rational, Maybe Rational))
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Maybe Rational, Maybe Rational)
-> Either Bool (Maybe Rational, Maybe Rational)
forall a b. b -> Either a b
Right (Maybe Rational
lo,Maybe Rational
hi))
      ]
    (Text, Either Bool (Maybe Rational, Maybe Rational))
-> Parser
     ByteString (Text, Either Bool (Maybe Rational, Maybe Rational))
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 = [Parser (Maybe Rational)] -> Parser (Maybe Rational)
forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
choice
   [ ByteString -> Parser ByteString
string ByteString
"(-inf" Parser ByteString
-> Parser (Maybe Rational) -> Parser (Maybe Rational)
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Maybe Rational -> Parser (Maybe Rational)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe Rational
forall a. Maybe a
Nothing
   , do Char
_ <- Char -> Parser Char
char Char
'['
        Rational
sign <- Rational
-> Parser ByteString Rational -> Parser ByteString Rational
forall (f :: Type -> Type) a. Alternative f => a -> f a -> f a
option Rational
1 (Char -> Parser Char
char Char
'-' Parser Char
-> Parser ByteString Rational -> Parser ByteString Rational
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Rational -> Parser ByteString Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return (-Rational
1))
        ByteString
num <- (Char -> Bool) -> Parser ByteString
takeWhile1 (\Char
c -> Char
c Char -> String -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` (String
"0123456789+-eE." :: String))
        case ReadS Rational
forall a. RealFrac a => ReadS a
readFloat (ByteString -> String
UTF8.toString ByteString
num) of
          (Rational
x,String
""):[(Rational, String)]
_ -> Maybe Rational -> Parser (Maybe Rational)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe Rational -> Parser (Maybe Rational))
-> Maybe Rational -> Parser (Maybe Rational)
forall a b. (a -> b) -> a -> b
$ Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational
sign Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
x)
          [(Rational, String)]
_ -> String -> Parser (Maybe Rational)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"expected rational bound"
   ]

dRealHiBound :: Parser (Maybe Rational)
dRealHiBound :: Parser (Maybe Rational)
dRealHiBound = [Parser (Maybe Rational)] -> Parser (Maybe Rational)
forall (f :: Type -> Type) a. Alternative f => [f a] -> f a
choice
   [ ByteString -> Parser ByteString
string ByteString
"inf)" Parser ByteString
-> Parser (Maybe Rational) -> Parser (Maybe Rational)
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Maybe Rational -> Parser (Maybe Rational)
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe Rational
forall a. Maybe a
Nothing
   , do Rational
sign <- Rational
-> Parser ByteString Rational -> Parser ByteString Rational
forall (f :: Type -> Type) a. Alternative f => a -> f a -> f a
option Rational
1 (Char -> Parser Char
char Char
'-' Parser Char
-> Parser ByteString Rational -> Parser ByteString Rational
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Rational -> Parser ByteString Rational
forall (m :: Type -> Type) a. Monad m => a -> m a
return (-Rational
1))
        ByteString
num <- (Char -> Bool) -> Parser ByteString
takeWhile1 (\Char
c -> Char
c Char -> String -> Bool
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 ReadS Rational
forall a. RealFrac a => ReadS a
readFloat (ByteString -> String
UTF8.toString ByteString
num) of
          (Rational
x,String
""):[(Rational, String)]
_ -> Maybe Rational -> Parser (Maybe Rational)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Maybe Rational -> Parser (Maybe Rational))
-> Maybe Rational -> Parser (Maybe Rational)
forall a b. (a -> b) -> a -> b
$ Rational -> Maybe Rational
forall a. a -> Maybe a
Just (Rational
sign Rational -> Rational -> Rational
forall a. Num a => a -> a -> a
* Rational
x)
          [(Rational, String)]
_ -> String -> Parser (Maybe Rational)
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"expected rational bound"
   ]


runDRealInOverride
   :: ExprBuilder t st fs
   -> LogData
   -> [BoolExpr t]   -- ^ propositions to check
   -> (SatResult (SMT2.WriterConn t (SMT2.Writer DReal), DRealBindings) () -> IO a)
   -> IO a
runDRealInOverride :: 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 <- ExprBuilder t st fs
-> Fold [BoolExpr t] (Pred (ExprBuilder t st fs))
-> [BoolExpr t]
-> IO (Pred (ExprBuilder t st fs))
forall sym s.
IsExprBuilder sym =>
sym -> Fold s (Pred sym) -> s -> IO (Pred sym)
andAllOf ExprBuilder t st fs
sym Fold [BoolExpr t] (Pred (ExprBuilder t st fs))
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 (ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym)
  ExprBuilder t st fs -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
    SolverStartSATQuery :: String -> String -> SolverEvent
SolverStartSATQuery
    { satQuerySolverName :: String
satQuerySolverName = String
"dReal"
    , satQueryReason :: String
satQueryReason = LogData -> String
logReason LogData
logData
    }
  String
-> [String]
-> Maybe String
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a)
-> IO a
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"] Maybe String
forall a. Maybe a
Nothing (((Handle, Handle, Handle, ProcessHandle) -> IO a) -> IO a)
-> ((Handle, Handle, Handle, ProcessHandle) -> IO a) -> IO a
forall a b. (a -> b) -> a -> b
$ \(Handle
in_h, Handle
out_h, Handle
err_h, ProcessHandle
ph) -> do

      -- Log stderr to output.
      InputStream ByteString
err_stream <- Handle -> IO (InputStream ByteString)
Streams.handleToInputStream Handle
err_h
      IO ThreadId -> IO ()
forall (f :: Type -> Type) a. Functor f => f a -> f ()
void (IO ThreadId -> IO ()) -> IO ThreadId -> IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
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)

      -- Write SMTLIB to standard input.
      LogData -> Int -> String -> IO ()
logCallbackVerbose LogData
logData Int
2 String
"Sending Satisfiability problem to dReal"
      -- dReal does not support (define-fun ...)
      SymbolVarBimap t
bindings <- ExprBuilder t st fs -> IO (SymbolVarBimap t)
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 (OutputStream ByteString -> IO (OutputStream Text))
-> IO (OutputStream ByteString) -> IO (OutputStream Text)
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 (OutputStream ByteString -> IO (OutputStream Text))
-> IO (OutputStream ByteString) -> IO (OutputStream Text)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< OutputStream ByteString
-> OutputStream ByteString -> IO (OutputStream ByteString)
forall a. OutputStream a -> OutputStream a -> IO (OutputStream a)
teeOutputStream OutputStream ByteString
aux_str (OutputStream ByteString -> IO (OutputStream ByteString))
-> IO (OutputStream ByteString) -> IO (OutputStream ByteString)
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 <- IO (InputStream Text)
forall a. IO (InputStream a)
Streams.nullInput

      WriterConn t (Writer DReal)
c <- DReal
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer DReal)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer DReal))
forall a t.
a
-> OutputStream Text
-> InputStream Text
-> AcknowledgementAction t (Writer a)
-> String
-> Bool
-> ProblemFeatures
-> Bool
-> SymbolVarBimap t
-> IO (WriterConn t (Writer a))
SMT2.newWriter DReal
DReal OutputStream Text
out_str InputStream Text
in_str AcknowledgementAction t (Writer DReal)
forall t h. AcknowledgementAction t h
SMTWriter.nullAcknowledgementAction String
"dReal"
             Bool
False ProblemFeatures
useComputableReals Bool
False SymbolVarBimap t
bindings

      -- Set the dReal default logic
      WriterConn t (Writer DReal) -> Logic -> IO ()
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")
      WriterConn t (Writer DReal) -> BoolExpr t -> IO ()
forall h t. SMTWriter h => WriterConn t h -> BoolExpr t -> IO ()
SMT2.assume WriterConn t (Writer DReal)
c BoolExpr t
p

      -- Create stream for output from solver.
      InputStream ByteString
out_stream <- Handle -> IO (InputStream ByteString)
Streams.handleToInputStream Handle
out_h

      -- dReal wants to parse its entire input, all the way through <EOF> before it does anything
      -- Also (apparently) you _must_ include the exit command to get any response at all...
      WriterConn t (Writer DReal) -> IO ()
forall a t. SMTLib2Tweaks a => WriterConn t (Writer a) -> IO ()
SMT2.writeCheckSat WriterConn t (Writer DReal)
c
      WriterConn t (Writer DReal) -> IO ()
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 <- IO
  (SatResult
     [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
-> IO
     (Either
        ParseException
        (SatResult
           [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()))
forall e a. Exception e => IO a -> IO (Either e a)
try (IO
   (SatResult
      [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
 -> IO
      (Either
         ParseException
         (SatResult
            [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())))
-> IO
     (SatResult
        [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
-> IO
     (Either
        ParseException
        (SatResult
           [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()))
forall a b. (a -> b) -> a -> b
$ Parser
  (SatResult
     [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
-> InputStream ByteString
-> IO
     (SatResult
        [(Text, Either Bool (Maybe Rational, Maybe Rational))] ())
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{} -> String
-> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
 -> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ()))
-> String
-> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String
"Could not parse dReal result.", ParseException -> String
forall e. Exception e => e -> String
displayException ParseException
ex]
          Right (Unsat ()) -> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
-> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (() -> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
forall mdl core. core -> SatResult mdl core
Unsat ())
          Right SatResult [(Text, Either Bool (Maybe Rational, Maybe Rational))] ()
Unknown    -> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
-> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SatResult (WriterConn t (Writer DReal), DRealBindings) ()
forall mdl core. SatResult mdl core
Unknown
          Right (Sat [(Text, Either Bool (Maybe Rational, Maybe Rational))]
bs)   -> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
-> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((WriterConn t (Writer DReal), DRealBindings)
-> SatResult (WriterConn t (Writer DReal), DRealBindings) ()
forall mdl core. mdl -> SatResult mdl core
Sat (WriterConn t (Writer DReal)
c, [(Text, Either Bool (Maybe Rational, Maybe Rational))]
-> DRealBindings
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

      -- Check error code.
      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
          -- Return result.
          LogData -> Int -> String -> IO ()
logCallbackVerbose LogData
logData Int
2 String
"dReal terminated."

          ExprBuilder t st fs -> SolverEvent -> IO ()
forall sym. IsExprBuilder sym => sym -> SolverEvent -> IO ()
logSolverEvent ExprBuilder t st fs
sym
             SolverEndSATQuery :: SatResult () () -> Maybe String -> SolverEvent
SolverEndSATQuery
             { satQueryResult :: SatResult () ()
satQueryResult = SatResult (WriterConn t (Writer DReal), DRealBindings) ()
-> SatResult () ()
forall a b. SatResult a b -> SatResult () ()
forgetModelAndCore SatResult (WriterConn t (Writer DReal), DRealBindings) ()
res
             , satQueryError :: Maybe String
satQueryError  = Maybe String
forall a. Maybe a
Nothing
             }

          a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
r
        ExitFailure Int
exit_code ->
          String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO a) -> String -> IO a
forall a b. (a -> b) -> a -> b
$ String
"dReal exited with unexpected code: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
exit_code