-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.TP.Kernel
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Kernel of the TP prover API.
-----------------------------------------------------------------------------

{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE NamedFieldPuns       #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeAbstractions     #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.TP.Kernel (
         Proposition,  Proof(..)
       , axiom
       , lemma
       , lemmaWith
       , internalAxiom
       , TPProofContext (..), smtProofStep
       ) where

import Control.Monad.Trans  (liftIO, MonadIO)

import Data.List  (intercalate)
import Data.Maybe (catMaybes)

import Data.SBV.Core.Data     hiding (None)
import Data.SBV.Trans.Control hiding (getProof)
import Data.SBV.Core.Symbolic (MonadSymbolic)

import Data.SBV.SMT.SMT
import Data.SBV.Core.Model
import Data.SBV.Provers.Prover

import Data.SBV.TP.Utils

import Data.Time (NominalDiffTime)
import Data.SBV.Utils.TDiff

import Data.Dynamic

-- | A proposition is something SBV is capable of proving/disproving in TP.
type Proposition a = ( QNot a
                     , QuantifiedBool a
                     , QSaturate Symbolic a
                     , Skolemize (NegatesTo a)
                     , Satisfiable (Symbolic (SkolemsTo (NegatesTo a)))
                     , Constraint  Symbolic  (SkolemsTo (NegatesTo a))
                     , Typeable a
                     )

-- | Accept the given definition as a fact. Usually used to introduce definitial axioms,
-- giving meaning to uninterpreted symbols. Note that we perform no checks on these propositions,
-- if you assert nonsense, then you get nonsense back. So, calls to 'axiom' should be limited to
-- definitions, or basic axioms (like commutativity, associativity) of uninterpreted function symbols.
axiom :: Proposition a => String -> a -> TP (Proof a)
axiom :: forall a. Proposition a => String -> a -> TP (Proof a)
axiom String
nm a
p = do SMTConfig
cfg <- TP SMTConfig
getTPConfig
                TPUnique
u   <- TP TPUnique
tpGetNextUnique
                Int
_   <- IO Int -> TP Int
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> TP Int) -> IO Int -> TP Int
forall a b. (a -> b) -> a -> b
$ SMTConfig -> Bool -> String -> Int -> TPProofContext -> IO Int
startTP SMTConfig
cfg Bool
True String
"Axiom" Int
0 (String -> [ProofObj] -> TPProofContext
TPProofOneShot String
nm [])
                let Proof ProofObj
iax = String -> a -> Proof a
forall a. Proposition a => String -> a -> Proof a
internalAxiom String
nm a
p
                Proof a -> TP (Proof a)
forall a. a -> TP a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof a -> TP (Proof a)) -> Proof a -> TP (Proof a)
forall a b. (a -> b) -> a -> b
$ ProofObj -> Proof a
forall a. ProofObj -> Proof a
Proof (ProofObj
iax { isUserAxiom = True, uniqId = u })

-- | Internal axiom generator; so we can keep truck of TP's trusted axioms, vs. user given axioms.
internalAxiom :: Proposition a => String -> a -> Proof a
internalAxiom :: forall a. Proposition a => String -> a -> Proof a
internalAxiom String
nm a
p = ProofObj -> Proof a
forall a. ProofObj -> Proof a
Proof (ProofObj -> Proof a) -> ProofObj -> Proof a
forall a b. (a -> b) -> a -> b
$ ProofObj { dependencies :: [ProofObj]
dependencies = []
                                      , isUserAxiom :: Bool
isUserAxiom  = Bool
False
                                      , getObjProof :: SBool
getObjProof  = String -> SBool -> SBool
forall a. SymVal a => String -> SBV a -> SBV a
label String
nm (a -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool a
p)
                                      , getProp :: Dynamic
getProp      = a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
p
                                      , proofName :: String
proofName    = String
nm
                                      , uniqId :: TPUnique
uniqId       = TPUnique
TPInternal
                                      , isCached :: Bool
isCached     = Bool
False
                                      }

-- | Prove a lemma, using the given configuration
lemmaWith :: Proposition a => SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
lemmaWith :: forall a.
Proposition a =>
SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
lemmaWith cfg :: SMTConfig
cfg@SMTConfig{tpOptions :: SMTConfig -> TPOptions
tpOptions = TPOptions{Bool
printStats :: Bool
printStats :: TPOptions -> Bool
printStats}} String
nm a
inputProp [ProofObj]
by = String -> TP (Proof a) -> TP (Proof a)
forall a. Typeable a => String -> TP (Proof a) -> TP (Proof a)
withProofCache String
nm (TP (Proof a) -> TP (Proof a)) -> TP (Proof a) -> TP (Proof a)
forall a b. (a -> b) -> a -> b
$ do
                 TPState
tpSt <- TP TPState
getTPState
                 TPUnique
u    <- TP TPUnique
tpGetNextUnique
                 IO (Proof a) -> TP (Proof a)
forall a. IO a -> TP a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Proof a) -> TP (Proof a)) -> IO (Proof a) -> TP (Proof a)
forall a b. (a -> b) -> a -> b
$ Bool -> IO (Maybe UTCTime)
forall (m :: * -> *). MonadIO m => Bool -> m (Maybe UTCTime)
getTimeStampIf Bool
printStats IO (Maybe UTCTime)
-> (Maybe UTCTime -> IO (Proof a)) -> IO (Proof a)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SMTConfig -> SymbolicT IO (Proof a) -> IO (Proof a)
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
runSMTWith SMTConfig
cfg (SymbolicT IO (Proof a) -> IO (Proof a))
-> (Maybe UTCTime -> SymbolicT IO (Proof a))
-> Maybe UTCTime
-> IO (Proof a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TPState -> TPUnique -> Maybe UTCTime -> SymbolicT IO (Proof a)
forall {m :: * -> *} {a}.
(ExtractIO m, MonadSymbolic (QueryT m),
 QSaturate (SymbolicT m) a) =>
TPState -> TPUnique -> Maybe UTCTime -> SymbolicT m (Proof a)
go TPState
tpSt TPUnique
u
  where go :: TPState -> TPUnique -> Maybe UTCTime -> SymbolicT m (Proof a)
go TPState
tpSt TPUnique
u Maybe UTCTime
mbStartTime = do a -> SymbolicT m ()
forall (m :: * -> *) a.
(Monad m, MonadIO m, SolverContext m, QSaturate m a) =>
a -> m ()
qSaturateSavingObservables a
inputProp
                                   (ProofObj -> SymbolicT m ()) -> [ProofObj] -> SymbolicT m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SBool -> SymbolicT m ()
forall a. QuantifiedBool a => a -> SymbolicT m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT m ())
-> (ProofObj -> SBool) -> ProofObj -> SymbolicT m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofObj -> SBool
getObjProof) [ProofObj]
by
                                   QueryT m (Proof a) -> SymbolicT m (Proof a)
forall (m :: * -> *) a. ExtractIO m => QueryT m a -> SymbolicT m a
query (QueryT m (Proof a) -> SymbolicT m (Proof a))
-> QueryT m (Proof a) -> SymbolicT m (Proof a)
forall a b. (a -> b) -> a -> b
$ SMTConfig
-> TPState
-> String
-> Int
-> TPProofContext
-> Maybe SBool
-> a
-> [(String, SVal)]
-> ((Int, Maybe NominalDiffTime) -> IO (Proof a))
-> QueryT m (Proof a)
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, MonadSymbolic m,
 Proposition a) =>
SMTConfig
-> TPState
-> String
-> Int
-> TPProofContext
-> Maybe SBool
-> a
-> [(String, SVal)]
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep SMTConfig
cfg TPState
tpSt String
"Lemma" Int
0 (String -> [ProofObj] -> TPProofContext
TPProofOneShot String
nm [ProofObj]
by) Maybe SBool
forall a. Maybe a
Nothing a
inputProp [] (Maybe UTCTime
-> TPUnique -> (Int, Maybe NominalDiffTime) -> IO (Proof a)
forall {m :: * -> *} {a}.
MonadIO m =>
Maybe UTCTime
-> TPUnique -> (Int, Maybe NominalDiffTime) -> m (Proof a)
good Maybe UTCTime
mbStartTime TPUnique
u)

        -- What to do if all goes well
        good :: Maybe UTCTime
-> TPUnique -> (Int, Maybe NominalDiffTime) -> m (Proof a)
good Maybe UTCTime
mbStart TPUnique
u (Int, Maybe NominalDiffTime)
d = do Maybe NominalDiffTime
mbElapsed <- Maybe UTCTime -> m (Maybe NominalDiffTime)
forall (m :: * -> *).
MonadIO m =>
Maybe UTCTime -> m (Maybe NominalDiffTime)
getElapsedTime Maybe UTCTime
mbStart
                              IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ SMTConfig
-> String
-> (Int, Maybe NominalDiffTime)
-> [NominalDiffTime]
-> IO ()
finishTP SMTConfig
cfg (String
"Q.E.D." String -> String -> String
forall a. [a] -> [a] -> [a]
++ [ProofObj] -> String
concludeModulo [ProofObj]
by) (Int, Maybe NominalDiffTime)
d ([NominalDiffTime] -> IO ()) -> [NominalDiffTime] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Maybe NominalDiffTime] -> [NominalDiffTime]
forall a. [Maybe a] -> [a]
catMaybes [Maybe NominalDiffTime
mbElapsed]
                              Proof a -> m (Proof a)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof a -> m (Proof a)) -> Proof a -> m (Proof a)
forall a b. (a -> b) -> a -> b
$ ProofObj -> Proof a
forall a. ProofObj -> Proof a
Proof (ProofObj -> Proof a) -> ProofObj -> Proof a
forall a b. (a -> b) -> a -> b
$ ProofObj { dependencies :: [ProofObj]
dependencies = [ProofObj]
by
                                                      , isUserAxiom :: Bool
isUserAxiom  = Bool
False
                                                      , getObjProof :: SBool
getObjProof  = String -> SBool -> SBool
forall a. SymVal a => String -> SBV a -> SBV a
label String
nm (a -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool a
inputProp)
                                                      , getProp :: Dynamic
getProp      = a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
inputProp
                                                      , proofName :: String
proofName    = String
nm
                                                      , uniqId :: TPUnique
uniqId       = TPUnique
u
                                                      , isCached :: Bool
isCached     = Bool
False
                                                      }

-- | Prove a given statement, using auxiliaries as helpers. Using the default solver.
lemma :: Proposition a => String -> a -> [ProofObj] -> TP (Proof a)
lemma :: forall a.
Proposition a =>
String -> a -> [ProofObj] -> TP (Proof a)
lemma String
nm a
f [ProofObj]
by = do SMTConfig
cfg <- TP SMTConfig
getTPConfig
                   SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
forall a.
Proposition a =>
SMTConfig -> String -> a -> [ProofObj] -> TP (Proof a)
lemmaWith SMTConfig
cfg String
nm a
f [ProofObj]
by

-- | Capture the general flow of a proof-step. Note that this is the only point where we call the backend solver
-- in a TP proof.
smtProofStep :: (SolverContext m, MonadIO m, MonadQuery m, MonadSymbolic m, Proposition a)
   => SMTConfig                              -- ^ config
   -> TPState                                -- ^ TPState
   -> String                                 -- ^ tag
   -> Int                                    -- ^ level
   -> TPProofContext                         -- ^ the context in which we're doing the proof
   -> Maybe SBool                            -- ^ Assumptions under which we do the check-sat. If there's one we'll push/pop
   -> a                                      -- ^ what we want to prove
   -> [(String, SVal)]                       -- ^ Values to display in case of failure
   -> ((Int, Maybe NominalDiffTime) -> IO r) -- ^ what to do when unsat, with the tab amount and time elapsed (if asked)
   -> m r
smtProofStep :: forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, MonadSymbolic m,
 Proposition a) =>
SMTConfig
-> TPState
-> String
-> Int
-> TPProofContext
-> Maybe SBool
-> a
-> [(String, SVal)]
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep cfg :: SMTConfig
cfg@SMTConfig{Bool
verbose :: Bool
verbose :: SMTConfig -> Bool
verbose, tpOptions :: SMTConfig -> TPOptions
tpOptions = TPOptions{Bool
printStats :: TPOptions -> Bool
printStats :: Bool
printStats}} TPState
tpState String
tag Int
level TPProofContext
ctx Maybe SBool
mbAssumptions a
prop [(String, SVal)]
disps (Int, Maybe NominalDiffTime) -> IO r
unsat = do

        case Maybe SBool
mbAssumptions of
           Maybe SBool
Nothing  -> do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"; smtProofStep: No context value to push."]
                          m r
check
           Just SBool
asm -> do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"; smtProofStep: Pushing in the context: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBool -> String
forall a. Show a => a -> String
show SBool
asm]
                          m r -> m r
forall (m :: * -> *) a. (MonadIO m, MonadQuery m) => m a -> m a
inNewAssertionStack (m r -> m r) -> m r -> m r
forall a b. (a -> b) -> a -> b
$ do SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain SBool
asm
                                                   m r
check

 where check :: m r
check = do
           Int
tab <- IO Int -> m Int
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> m Int) -> IO Int -> m Int
forall a b. (a -> b) -> a -> b
$ SMTConfig -> Bool -> String -> Int -> TPProofContext -> IO Int
startTP SMTConfig
cfg Bool
verbose String
tag Int
level TPProofContext
ctx

           -- It's tempting to skolemize here.. But skolemization creates fresh constants
           -- based on the name given, and they mess with all else. So, don't skolemize!
           SBool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool -> SBool
sNot (a -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool a
prop)

           (Maybe NominalDiffTime
mbT, CheckSatResult
r) <- Bool
-> m CheckSatResult -> m (Maybe NominalDiffTime, CheckSatResult)
forall (m :: * -> *) a.
MonadIO m =>
Bool -> m a -> m (Maybe NominalDiffTime, a)
timeIf Bool
printStats m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat

           TPState -> (TPStats -> TPStats) -> m ()
forall (m :: * -> *).
MonadIO m =>
TPState -> (TPStats -> TPStats) -> m ()
updStats TPState
tpState (\TPStats
s -> TPStats
s{noOfCheckSats = noOfCheckSats s + 1})

           case Maybe NominalDiffTime
mbT of
             Maybe NominalDiffTime
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
             Just NominalDiffTime
t  -> TPState -> (TPStats -> TPStats) -> m ()
forall (m :: * -> *).
MonadIO m =>
TPState -> (TPStats -> TPStats) -> m ()
updStats TPState
tpState (\TPStats
s -> TPStats
s{solverElapsed = solverElapsed s + t})

           case CheckSatResult
r of
             CheckSatResult
Unk    -> m r
forall {b}. m b
unknown
             CheckSatResult
Sat    -> m r
forall {b}. m b
cex
             DSat{} -> m r
forall {b}. m b
cex
             CheckSatResult
Unsat  -> IO r -> m r
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO r -> m r) -> IO r -> m r
forall a b. (a -> b) -> a -> b
$ (Int, Maybe NominalDiffTime) -> IO r
unsat (Int
tab, Maybe NominalDiffTime
mbT)

       die :: a
die = String -> a
forall a. HasCallStack => String -> a
error String
"Failed"

       fullNm :: String
fullNm = case TPProofContext
ctx of
                  TPProofOneShot       String
s [ProofObj]
_    -> String
s
                  TPProofStep    Bool
True  String
s [String]
_ [String]
ss -> String
"assumptions for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ss)
                  TPProofStep    Bool
False String
s [String]
_ [String]
ss ->                       String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
ss)

       unknown :: m b
unknown = do SMTReasonUnknown
r <- m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                    IO b -> m b
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO b -> m b) -> IO b -> m b
forall a b. (a -> b) -> a -> b
$ do String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n*** Failed to prove " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fullNm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."
                                String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n*** Solver reported: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTReasonUnknown -> String
forall a. Show a => a -> String
show SMTReasonUnknown
r
                                IO b
forall {a}. a
die

       -- What to do if the proof fails
       cex :: m b
cex = do
         IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"\n*** Failed to prove " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fullNm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"."

         SMTResult
res <- case TPProofContext
ctx of
                  TPProofStep{} -> do ((String, SVal) -> m ()) -> [(String, SVal)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((String -> SVal -> m ()) -> (String, SVal) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> SVal -> m ()
forall (m :: * -> *). MonadSymbolic m => String -> SVal -> m ()
sObserve) [(String, SVal)]
disps
                                      SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                  TPProofOneShot String
_ [ProofObj]
by ->
                     -- When trying to get a counter-example not in query mode, we
                     -- do a skolemized sat call, which gets better counter-examples.
                     -- We only include the those facts that are user-given axioms. This
                     -- way our counter-example will be more likely to be relevant
                     -- to the proposition we're currently proving. (Hopefully.)
                     -- Remember that we first have to negate, and then skolemize!
                     do SatResult SMTResult
res <- IO SatResult -> m SatResult
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SatResult -> m SatResult) -> IO SatResult -> m SatResult
forall a b. (a -> b) -> a -> b
$ SMTConfig -> Symbolic (SkolemsTo (NegatesTo a)) -> IO SatResult
forall (m :: * -> *) a.
SatisfiableM m a =>
SMTConfig -> a -> m SatResult
satWith SMTConfig
cfg (Symbolic (SkolemsTo (NegatesTo a)) -> IO SatResult)
-> Symbolic (SkolemsTo (NegatesTo a)) -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do
                                           a -> SymbolicT IO ()
forall (m :: * -> *) a.
(Monad m, MonadIO m, SolverContext m, QSaturate m a) =>
a -> m ()
qSaturateSavingObservables a
prop
                                           (SBool -> SymbolicT IO ()) -> [SBool] -> SymbolicT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain [SBool
getObjProof | ProofObj{Bool
isUserAxiom :: ProofObj -> Bool
isUserAxiom :: Bool
isUserAxiom, SBool
getObjProof :: ProofObj -> SBool
getObjProof :: SBool
getObjProof} <- [ProofObj]
by, Bool
isUserAxiom] :: Symbolic ()
                                           ((String, SVal) -> SymbolicT IO ())
-> [(String, SVal)] -> SymbolicT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((String -> SVal -> SymbolicT IO ())
-> (String, SVal) -> SymbolicT IO ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> SVal -> SymbolicT IO ()
forall (m :: * -> *). MonadSymbolic m => String -> SVal -> m ()
sObserve) [(String, SVal)]
disps
                                           SkolemsTo (NegatesTo a) -> Symbolic (SkolemsTo (NegatesTo a))
forall a. a -> SymbolicT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SkolemsTo (NegatesTo a) -> Symbolic (SkolemsTo (NegatesTo a)))
-> SkolemsTo (NegatesTo a) -> Symbolic (SkolemsTo (NegatesTo a))
forall a b. (a -> b) -> a -> b
$ NegatesTo a -> SkolemsTo (NegatesTo a)
forall a.
(Skolemize a, Constraint Symbolic (SkolemsTo a), Skolemize a) =>
a -> SkolemsTo a
skolemize (a -> NegatesTo a
forall a. QNot a => a -> NegatesTo a
qNot a
prop)
                        SMTResult -> m SMTResult
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SMTResult
res

         IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ ThmResult -> IO ()
forall a. Show a => a -> IO ()
print (ThmResult -> IO ()) -> ThmResult -> IO ()
forall a b. (a -> b) -> a -> b
$ SMTResult -> ThmResult
ThmResult SMTResult
res

         m b
forall {a}. a
die