-----------------------------------------------------------------------------
-- |
-- 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 cfg <- KD SMTConfig
getKDConfig
                _   <- liftIO $ startKD cfg True "Axiom" 0 (KDProofOneShot nm [])
                pure (internalAxiom nm 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
        kdSt <- KD KDState
getKDState
        liftIO $ getTimeStampIf measureTime >>= runSMTWith cfg . go 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 mbElapsed <- Maybe UTCTime -> m (Maybe NominalDiffTime)
forall (m :: * -> *).
MonadIO m =>
Maybe UTCTime -> m (Maybe NominalDiffTime)
getElapsedTime Maybe UTCTime
mbStart
                            liftIO $ finishKD cfg ("Q.E.D." ++ modulo) d $ catMaybes [mbElapsed]
                            pure Proof { rootOfTrust = ros
                                       , isUserAxiom = False
                                       , getProof    = label nm (quantifiedBool inputProp)
                                       , getProp     = toDyn inputProp
                                       , proofName   = 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 cfg <- KD SMTConfig
getKDConfig
                   lemmaWith cfg nm f 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 cfg <- KD SMTConfig
getKDConfig
                     theoremWith cfg nm f 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
           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!
           constrain $ sNot (quantifiedBool prop)

           (mbT, r) <- timeIf measureTime checkSat

           updStats kdState (\KDStats
s -> KDStats
s{noOfCheckSats = noOfCheckSats s + 1})

           case 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 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]
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]
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 r <- m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                    liftIO $ do putStrLn $ "\n*** Failed to prove " ++ fullNm ++ "."
                                putStrLn $ "\n*** Solver reported: " ++ show r
                                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
"."

         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 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)
                        pure res

         liftIO $ print $ ThmResult res

         die