------------------------------------------------------------------------
-- |
-- 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.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

-- | Path to dReal
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]   -- ^ propositions to check
   -> (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

      -- Log stderr to output.
      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)

      -- 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 <- 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

      -- Set the dReal default logic
      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

      -- 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...
      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

      -- 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."

          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