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

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

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Tools.KD.Kernel (
         Proposition,  Proof(..)
       , axiom
       , lemma,   lemmaWith,   lemmaGen
       , theorem, theoremWith
       , sorry
       , internalAxiom
       , KDProofContext (..), 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.SMT.SMT
import Data.SBV.Core.Model
import Data.SBV.Provers.Prover

import Data.SBV.Tools.KD.Utils

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

import Data.Dynamic

-- | A proposition is something SBV is capable of proving/disproving in KnuckleDragger.
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 -> KD Proof
axiom :: forall a. Proposition a => String -> a -> KD Proof
axiom String
nm a
p = do SMTConfig
cfg <- KD SMTConfig
getKDConfig
                Int
_   <- IO Int -> KD Int
forall a. IO a -> KD a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> KD Int) -> IO Int -> KD Int
forall a b. (a -> b) -> a -> b
$ SMTConfig -> Bool -> String -> Int -> KDProofContext -> IO Int
startKD SMTConfig
cfg Bool
True String
"Axiom" Int
0 (String -> [Proof] -> KDProofContext
KDProofOneShot String
nm [])
                Proof -> KD Proof
forall a. a -> KD a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> a -> Proof
forall a. Proposition a => String -> a -> Proof
internalAxiom String
nm a
p) { isUserAxiom = True }

-- | Internal axiom generator; so we can keep truck of KnuckleDrugger's trusted axioms, vs. user given axioms.
internalAxiom :: Proposition a => String -> a -> Proof
internalAxiom :: forall a. Proposition a => String -> a -> Proof
internalAxiom String
nm a
p = Proof { rootOfTrust :: RootOfTrust
rootOfTrust = RootOfTrust
None
                           , isUserAxiom :: Bool
isUserAxiom = Bool
False
                           , getProof :: SBV Bool
getProof    = String -> SBV Bool -> SBV Bool
forall a. SymVal a => String -> SBV a -> SBV a
label String
nm (a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
p)
                           , getProp :: Dynamic
getProp     = a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
p
                           , proofName :: String
proofName   = String
nm
                           }

-- | A manifestly false theorem. This is useful when we want to prove a theorem that the underlying solver
-- cannot deal with, or if we want to postpone the proof for the time being. KnuckleDragger will keep
-- track of the uses of 'sorry' and will print them appropriately while printing proofs.
sorry :: Proof
sorry :: Proof
sorry = Proof { rootOfTrust :: RootOfTrust
rootOfTrust = RootOfTrust
Self
              , isUserAxiom :: Bool
isUserAxiom = Bool
False
              , getProof :: SBV Bool
getProof    = String -> SBV Bool -> SBV Bool
forall a. SymVal a => String -> SBV a -> SBV a
label String
"sorry" ((Forall "__sbvKD_sorry" Bool -> SBV Bool) -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool Forall "__sbvKD_sorry" Bool -> SBV Bool
p)
              , getProp :: Dynamic
getProp     = (Forall "__sbvKD_sorry" Bool -> SBV Bool) -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn Forall "__sbvKD_sorry" Bool -> SBV Bool
p
              , proofName :: String
proofName   = String
"sorry"
              }
  where -- ideally, I'd rather just use
        --   p = sFalse
        -- but then SBV constant folds the boolean, and the generated script
        -- doesn't contain the actual contents, as SBV determines unsatisfiability
        -- itself. By using the following proposition (which is easy for the backend
        -- solver to determine as false, we avoid the constant folding.
        p :: Forall "__sbvKD_sorry" Bool -> SBV Bool
p (Forall @"__sbvKD_sorry" (SBV Bool
x :: SBool)) = String -> SBV Bool -> SBV Bool
forall a. SymVal a => String -> SBV a -> SBV a
label String
"SORRY: KnuckleDragger, proof uses \"sorry\"" SBV Bool
x

-- | Helper to generate lemma/theorem statements.
lemmaGen :: Proposition a => SMTConfig -> String -> String -> a -> [Proof] -> KD Proof
lemmaGen :: forall a.
Proposition a =>
SMTConfig -> String -> String -> a -> [Proof] -> KD Proof
lemmaGen cfg :: SMTConfig
cfg@SMTConfig{kdOptions :: SMTConfig -> KDOptions
kdOptions = KDOptions{Bool
measureTime :: Bool
measureTime :: KDOptions -> Bool
measureTime}} String
tag String
nm a
inputProp [Proof]
by = do
        KDState
kdSt <- KD KDState
getKDState
        IO Proof -> KD Proof
forall a. IO a -> KD a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Proof -> KD Proof) -> IO Proof -> KD Proof
forall a b. (a -> b) -> a -> b
$ Bool -> IO (Maybe UTCTime)
forall (m :: * -> *). MonadIO m => Bool -> m (Maybe UTCTime)
getTimeStampIf Bool
measureTime IO (Maybe UTCTime) -> (Maybe UTCTime -> IO Proof) -> IO Proof
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 -> IO Proof
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
runSMTWith SMTConfig
cfg (SymbolicT IO Proof -> IO Proof)
-> (Maybe UTCTime -> SymbolicT IO Proof)
-> Maybe UTCTime
-> IO Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. KDState -> Maybe UTCTime -> SymbolicT IO Proof
forall {m :: * -> *}.
(ExtractIO m, QSaturate (SymbolicT m) a) =>
KDState -> Maybe UTCTime -> SymbolicT m Proof
go KDState
kdSt
  where go :: KDState -> Maybe UTCTime -> SymbolicT m Proof
go KDState
kdSt Maybe UTCTime
mbStartTime = do a -> SymbolicT m ()
forall (m :: * -> *) a.
(Monad m, MonadIO m, SolverContext m, QSaturate m a) =>
a -> m ()
qSaturateSavingObservables a
inputProp
                                 (Proof -> SymbolicT m ()) -> [Proof] -> SymbolicT m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SBV Bool -> SymbolicT m ()
forall a. QuantifiedBool a => a -> SymbolicT m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBV Bool -> SymbolicT m ())
-> (Proof -> SBV Bool) -> Proof -> SymbolicT m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof -> SBV Bool
getProof) [Proof]
by
                                 QueryT m Proof -> SymbolicT m Proof
forall (m :: * -> *) a. ExtractIO m => QueryT m a -> SymbolicT m a
query (QueryT m Proof -> SymbolicT m Proof)
-> QueryT m Proof -> SymbolicT m Proof
forall a b. (a -> b) -> a -> b
$ SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe (SBV Bool)
-> a
-> ((Int, Maybe NominalDiffTime) -> IO Proof)
-> QueryT m Proof
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe (SBV Bool)
-> a
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep SMTConfig
cfg KDState
kdSt String
tag Int
0 (String -> [Proof] -> KDProofContext
KDProofOneShot String
nm [Proof]
by) Maybe (SBV Bool)
forall a. Maybe a
Nothing a
inputProp (Maybe UTCTime -> (Int, Maybe NominalDiffTime) -> IO Proof
forall {m :: * -> *}.
MonadIO m =>
Maybe UTCTime -> (Int, Maybe NominalDiffTime) -> m Proof
good Maybe UTCTime
mbStartTime)

        -- What to do if all goes well
        good :: Maybe UTCTime -> (Int, Maybe NominalDiffTime) -> m Proof
good Maybe UTCTime
mbStart (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 ()
finishKD SMTConfig
cfg (String
"Q.E.D." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
modulo) (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 -> m Proof
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Proof { rootOfTrust :: RootOfTrust
rootOfTrust = RootOfTrust
ros
                                       , isUserAxiom :: Bool
isUserAxiom = Bool
False
                                       , getProof :: SBV Bool
getProof    = String -> SBV Bool -> SBV Bool
forall a. SymVal a => String -> SBV a -> SBV a
label String
nm (a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
quantifiedBool a
inputProp)
                                       , getProp :: Dynamic
getProp     = a -> Dynamic
forall a. Typeable a => a -> Dynamic
toDyn a
inputProp
                                       , proofName :: String
proofName   = String
nm
                                       }
          where (RootOfTrust
ros, String
modulo) = String -> [Proof] -> (RootOfTrust, String)
calculateRootOfTrust String
nm [Proof]
by

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

-- | Prove a given statement, using auxiliaries as helpers. Using the given solver.
lemmaWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
lemmaWith :: forall a.
Proposition a =>
SMTConfig -> String -> a -> [Proof] -> KD Proof
lemmaWith SMTConfig
cfg = SMTConfig -> String -> String -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> String -> a -> [Proof] -> KD Proof
lemmaGen SMTConfig
cfg String
"Lemma"

-- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemma', except for the name, using the default solver.
theorem :: Proposition a => String -> a -> [Proof] -> KD Proof
theorem :: forall a. Proposition a => String -> a -> [Proof] -> KD Proof
theorem String
nm a
f [Proof]
by = do SMTConfig
cfg <- KD SMTConfig
getKDConfig
                     SMTConfig -> String -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> a -> [Proof] -> KD Proof
theoremWith SMTConfig
cfg String
nm a
f [Proof]
by

-- | Prove a given statement, using auxiliaries as helpers. Essentially the same as 'lemmaWith', except for the name.
theoremWith :: Proposition a => SMTConfig -> String -> a -> [Proof] -> KD Proof
theoremWith :: forall a.
Proposition a =>
SMTConfig -> String -> a -> [Proof] -> KD Proof
theoremWith SMTConfig
cfg = SMTConfig -> String -> String -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> String -> a -> [Proof] -> KD Proof
lemmaGen SMTConfig
cfg String
"Theorem"

-- | Capture the general flow of a proof-step.
smtProofStep :: (SolverContext m, MonadIO m, MonadQuery m, Proposition a)
   => SMTConfig                              -- ^ config
   -> KDState                                -- ^ KDState
   -> String                                 -- ^ tag
   -> Int                                    -- ^ level
   -> KDProofContext                         -- ^ 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
   -> ((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, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Int
-> KDProofContext
-> Maybe (SBV Bool)
-> a
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
smtProofStep cfg :: SMTConfig
cfg@SMTConfig{Bool
verbose :: Bool
verbose :: SMTConfig -> Bool
verbose, kdOptions :: SMTConfig -> KDOptions
kdOptions = KDOptions{Bool
measureTime :: KDOptions -> Bool
measureTime :: Bool
measureTime}} KDState
kdState String
tag Int
level KDProofContext
ctx Maybe (SBV Bool)
mbAssumptions a
prop (Int, Maybe NominalDiffTime) -> IO r
unsat = do

        case Maybe (SBV Bool)
mbAssumptions of
           Maybe (SBV Bool)
Nothing  -> do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"; smtProofStep: No context value to push."]
                          m r
check
           Just SBV Bool
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]
++ SBV Bool -> String
forall a. Show a => a -> String
show SBV Bool
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 SBV Bool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain SBV Bool
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 -> KDProofContext -> IO Int
startKD SMTConfig
cfg Bool
verbose String
tag Int
level KDProofContext
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!
           SBV Bool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBV Bool -> m ()) -> SBV Bool -> m ()
forall a b. (a -> b) -> a -> b
$ SBV Bool -> SBV Bool
sNot (a -> SBV Bool
forall a. QuantifiedBool a => a -> SBV Bool
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
measureTime m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat

           KDState -> (KDStats -> KDStats) -> m ()
forall (m :: * -> *).
MonadIO m =>
KDState -> (KDStats -> KDStats) -> m ()
updStats KDState
kdState (\KDStats
s -> KDStats
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  -> KDState -> (KDStats -> KDStats) -> m ()
forall (m :: * -> *).
MonadIO m =>
KDState -> (KDStats -> KDStats) -> m ()
updStats KDState
kdState (\KDStats
s -> KDStats
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 KDProofContext
ctx of
                  KDProofOneShot       String
s [Proof]
_    -> String
s
                  KDProofStep    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)
                  KDProofStep    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 KDProofContext
ctx of
                  KDProofStep{}       -> 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
                  KDProofOneShot String
_ [Proof]
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
                                           (SBV Bool -> SymbolicT IO ()) -> [SBV Bool] -> SymbolicT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SBV Bool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain [SBV Bool
getProof | Proof{Bool
isUserAxiom :: Proof -> Bool
isUserAxiom :: Bool
isUserAxiom, SBV Bool
getProof :: Proof -> SBV Bool
getProof :: SBV Bool
getProof} <- [Proof]
by, Bool
isUserAxiom] :: Symbolic ()
                                           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