------------------------------------------------------------------------
-- |
-- 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
(Int -> DReal -> ShowS)
-> (DReal -> String) -> ([DReal] -> ShowS) -> Show DReal
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DReal -> ShowS
showsPrec :: Int -> DReal -> ShowS
$cshow :: DReal -> String
show :: DReal -> String
$cshowList :: [DReal] -> ShowS
showList :: [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
"solver.dreal.path"

drealPathOLD :: ConfigOption (BaseStringType Unicode)
drealPathOLD :: ConfigOption (BaseStringType Unicode)
drealPathOLD = 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 =
  let dpOpt :: ConfigOption (BaseStringType Unicode) -> ConfigDesc
dpOpt ConfigOption (BaseStringType Unicode)
co = 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)
co
                 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"))
      dp :: ConfigDesc
dp = ConfigOption (BaseStringType Unicode) -> ConfigDesc
dpOpt ConfigOption (BaseStringType Unicode)
drealPath
  in [ ConfigDesc
dp
     , [ConfigDesc] -> ConfigDesc -> ConfigDesc
deprecatedOpt [ConfigDesc
dp] (ConfigDesc -> ConfigDesc) -> ConfigDesc -> ConfigDesc
forall a b. (a -> b) -> a -> b
$ ConfigOption (BaseStringType Unicode) -> ConfigDesc
dpOpt ConfigOption (BaseStringType Unicode)
drealPathOLD
     ] [ConfigDesc] -> [ConfigDesc] -> [ConfigDesc]
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 ->
      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
             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
             rangeFn <- getBoundBindings c m
             cont (Sat (evalFn, Just 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 = ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
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 :: 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
  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
  out_str <- Streams.encodeUtf8 =<< Streams.handleToOutputStream h
  in_str <- Streams.nullInput
  let cfg = ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
  strictness <- maybe SMTWriter.Strict
                (\ConcreteVal BaseBoolType
c -> if ConcreteVal BaseBoolType -> Bool
fromConcreteBool ConcreteVal BaseBoolType
c
                       then ResponseStrictness
SMTWriter.Strict
                       else ResponseStrictness
SMTWriter.Lenient) <$>
                (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)
  c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal"
          False useComputableReals False bindings
  SMT2.setProduceModels c True
  SMT2.setLogic c (SMT2.Logic "QF_NRA")
  forM_ ps (SMT2.assume c)
  SMT2.writeCheckSat c
  SMT2.writeExit 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 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 a. String -> m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"Expected Boolean variable"
          Just (Left Bool
b) -> Bool -> m Bool
forall a. a -> m a
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 a. a -> m a
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 a. 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 a. 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 a. a -> m a
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 a. String -> m a
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 a. a -> m a
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 a. 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 = SMTWriter.SMTEvalFunctions { smtEvalBool :: Term (Writer DReal) -> IO Bool
SMTWriter.smtEvalBool = Term -> IO Bool
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 = NatRepr w -> Term (Writer DReal) -> IO (BV w)
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
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 = FloatPrecisionRepr fpp
-> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
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 Text
SMTWriter.smtEvalString = Term -> IO Text
Term (Writer DReal) -> IO Text
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 :: 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 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 a. String -> m a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail String
"expected boolean term"
          Just (Left Bool
b) -> Bool -> m Bool
forall a. a -> m a
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 a. String -> m a
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 a. 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 a. 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 a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Rational
x
              Maybe Rational
Nothing -> IOError -> IO Rational
forall e a. (HasCallStack, Exception e) => e -> IO a
throwIO (String -> IOError
userError String
"unbound")
          Just (Left Bool
_) -> String -> IO Rational
forall a. String -> IO a
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. (HasCallStack, Exception e) => e -> IO a
throwIO (String -> IOError
userError String
"unbound")
      evalFloat :: p -> p -> m a
evalFloat p
_ p
_ = String -> m a
forall a. 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 = SMTWriter.SMTEvalFunctions { smtEvalBool :: Term (Writer DReal) -> IO Bool
SMTWriter.smtEvalBool = Term -> IO Bool
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 = NatRepr w -> Term (Writer DReal) -> IO (BV w)
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 = FloatPrecisionRepr fpp
-> Term (Writer DReal) -> IO (BV (FloatPrecisionBits fpp))
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 Text
SMTWriter.smtEvalString = Term -> IO Text
Term (Writer DReal) -> IO Text
forall {m :: Type -> Type} {p} {a}. MonadFail m => p -> m a
evalStr
                                           }
  GroundEvalFn 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
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 a. a -> IO 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. (HasCallStack, Exception e) => e -> IO a
throwIO IOError
e
  return $ \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 :: forall t.
WriterConn t (Writer DReal)
-> DRealBindings -> IO (ExprRangeBindings t)
getBoundBindings WriterConn t (Writer DReal)
c DRealBindings
m = do
  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
  h_evalFn <- getMaybeEval snd c m
  return $ \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 a b. IO (a -> b) -> IO a -> IO b
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 -> Parser ByteString
string ByteString
"unsat"
       return (Unsat ())

  , do _ <- ByteString -> Parser ByteString
string ByteString
"unknown"
       return Unknown

  , do _ <- ByteString -> Parser ByteString
string ByteString
"delta-sat"
       _ <- 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')
       endOfLine
       bs <- many' dRealBinding
       endOfInput
       return (Sat bs)
  ]

dRealBinding :: Parser (Text, Either Bool (Maybe Rational, Maybe Rational))
dRealBinding :: Parser
  ByteString (Text, Either Bool (Maybe Rational, Maybe Rational))
dRealBinding = do
    Parser ()
skipSpace

    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)

    skipSpace
    _ <- char ':'
    skipSpace

    val <- msum
      [ do _ <- string "False"
           skipSpace
           return (Left False)

      , do _ <- string "True"
           skipSpace
           return (Left True)

      , do lo <- dRealLoBound

           skipSpace
           _ <- char ','
           skipSpace

           hi <- dRealHiBound

           skipSpace
           _ <- option ' ' (char ';')
           skipSpace
           return (Right (lo,hi))
      ]
    return (Text.fromStrict (decodeUtf8 nm),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 a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Maybe Rational -> Parser (Maybe Rational)
forall a. a -> Parser ByteString a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe Rational
forall a. Maybe a
Nothing
   , do _ <- Char -> Parser Char
char Char
'['
        sign <- option 1 (char '-' >> return (-1))
        num <- takeWhile1 (\Char
c -> Char
c Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` (String
"0123456789+-eE." :: String))
        case readFloat (UTF8.toString num) of
          (Rational
x,String
""):[(Rational, String)]
_ -> Maybe Rational -> Parser (Maybe Rational)
forall a. a -> Parser ByteString a
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 a. String -> Parser ByteString a
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 a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Maybe Rational -> Parser (Maybe Rational)
forall a. a -> Parser ByteString a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Maybe Rational
forall a. Maybe a
Nothing
   , do 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 a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Rational -> Parser ByteString Rational
forall a. a -> Parser ByteString a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (-Rational
1))
        num <- takeWhile1 (\Char
c -> Char
c Char -> String -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: Type -> Type) a.
(Foldable t, Eq a) =>
a -> t a -> Bool
`elem` (String
"0123456789+-eE." :: String))
        _ <- char ']'
        case readFloat (UTF8.toString num) of
          (Rational
x,String
""):[(Rational, String)]
_ -> Maybe Rational -> Parser (Maybe Rational)
forall a. a -> Parser ByteString a
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 a. String -> Parser ByteString a
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
  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 (Pred (ExprBuilder t st fs) -> f (Pred (ExprBuilder t st fs)))
-> [BoolExpr t] -> f [BoolExpr t]
(BoolExpr t -> f (BoolExpr t)) -> [BoolExpr t] -> f [BoolExpr t]
Fold [BoolExpr t] (Pred (ExprBuilder t st fs))
forall (f :: Type -> Type) a. Foldable f => IndexedFold Int (f a) a
IndexedFold Int [BoolExpr t] (BoolExpr t)
folded [BoolExpr t]
ps
  solver_path <- findSolverPath drealPath (getConfiguration sym)
  logSolverEvent sym
    (SolverStartSATQuery $ SolverStartSATQueryRec
    { satQuerySolverName = "dReal"
    , satQueryReason = logReason logData
    })
  withProcessHandles solver_path ["--model", "--in", "--format", "smt2"] Nothing $ \(Handle
in_h, Handle
out_h, Handle
err_h, ProcessHandle
ph) -> do

      -- Log stderr to output.
      err_stream <- Handle -> IO (InputStream ByteString)
Streams.handleToInputStream Handle
err_h
      void $ forkIO $ logErrorStream err_stream (logCallbackVerbose logData 2)

      -- Write SMTLIB to standard input.
      logCallbackVerbose logData 2 "Sending Satisfiability problem to dReal"
      -- dReal does not support (define-fun ...)
      bindings <- getSymbolVarBimap sym

      out_str  <-
        case logHandle 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 aux_str <- Handle -> IO (OutputStream ByteString)
Streams.handleToOutputStream Handle
aux_h
               Streams.encodeUtf8 =<< teeOutputStream aux_str =<< Streams.handleToOutputStream in_h

      in_str <- Streams.nullInput

      let cfg = ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
getConfiguration ExprBuilder t st fs
sym
      strictness <- maybe SMTWriter.Strict
                    (\ConcreteVal BaseBoolType
c -> if ConcreteVal BaseBoolType -> Bool
fromConcreteBool ConcreteVal BaseBoolType
c
                           then ResponseStrictness
SMTWriter.Strict
                           else ResponseStrictness
SMTWriter.Lenient) <$>
                    (getOption =<< getOptionSetting RSP.strictSMTParsing cfg)

      c <- SMT2.newWriter DReal out_str in_str SMTWriter.nullAcknowledgementAction strictness "dReal"
             False useComputableReals False bindings

      -- Set the dReal default logic
      SMT2.setLogic c (SMT2.Logic "QF_NRA")
      SMT2.assume c p

      -- Create stream for output from solver.
      out_stream <- Streams.handleToInputStream 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...
      SMT2.writeCheckSat c
      SMT2.writeExit c
      hClose in_h

      logCallbackVerbose logData 2 "Parsing result from solver"

      msat_result <- try $ Streams.parseFromStream dRealResponse out_stream

      res <-
        case msat_result of
          Left ex :: ParseException
ex@Streams.ParseException{} -> String
-> IO (SatResult (WriterConn t (Writer DReal), DRealBindings) ())
forall a. String -> IO a
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 a. a -> IO a
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 a. a -> IO a
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 a. a -> IO a
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))

      r <- modelFn res

      -- Check error code.
      logCallbackVerbose logData 2 "Waiting for dReal to exit"

      ec <- waitForProcess ph
      case 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 -> SolverEvent
SolverEndSATQuery (SolverEndSATQuery -> SolverEvent)
-> SolverEndSATQuery -> SolverEvent
forall a b. (a -> b) -> a -> b
$ SolverEndSATQueryRec
             { 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 a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return a
r
        ExitFailure Int
exit_code ->
          String -> IO a
forall a. 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