-----------------------------------------------------------------------------
-- |
-- 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
       , checkSatThen
       ) where

import Control.Monad.Trans  (liftIO, MonadIO)

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

import Data.SBV.Core.Data hiding (None)
import Data.SBV.Core.Symbolic (isEmptyModel)
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" [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]
nms 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
-> Bool
-> Maybe (SBV Bool)
-> a
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO Proof)
-> QueryT m Proof
forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Bool
-> Maybe (SBV Bool)
-> a
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
checkSatThen SMTConfig
cfg KDState
kdSt String
tag Bool
False Maybe (SBV Bool)
forall a. Maybe a
Nothing a
inputProp [Proof]
by [String]
nms Maybe [String]
forall a. Maybe a
Nothing Maybe (IO ())
forall a. Maybe a
Nothing (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
                nm :: String
nm = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." [String]
nms

-- | 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 String
nm = SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
lemmaGen SMTConfig
cfg String
"Lemma" [String
nm]

-- | 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 String
nm = SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
forall a.
Proposition a =>
SMTConfig -> String -> [String] -> a -> [Proof] -> KD Proof
lemmaGen SMTConfig
cfg String
"Theorem" [String
nm]

-- | Capture the general flow after a checkSat. We run the sat case if model is empty.
-- NB. This is the only place in Knuckledragger where we actually call check-sat;
-- so all interaction goes through here.
checkSatThen :: (SolverContext m, MonadIO m, MonadQuery m, Proposition a)
   => SMTConfig                              -- ^ config
   -> KDState                                -- ^ KDState
   -> String                                 -- ^ tag
   -> Bool                                   -- in query mode already (True), or lemmaGen (False)?
   -> Maybe SBool                            -- ^ context if any. If there's one we'll push/pop
   -> a                                      -- ^ what we want to prove
   -> [Proof]                                -- ^ helpers in the context. NB. Only used for printing cex's. We assume they're already asserted.
   -> [String]                               -- ^ sub-proof
   -> Maybe [String]                         -- ^ full-path to the proof, if different than sub-proof
   -> Maybe (IO ())                          -- ^ special code to run if model is empty (if any)
   -> ((Int, Maybe NominalDiffTime) -> IO r) -- ^ what to do when unsat, with the tab amount and time elapsed (if asked)
   -> m r
checkSatThen :: forall (m :: * -> *) a r.
(SolverContext m, MonadIO m, MonadQuery m, Proposition a) =>
SMTConfig
-> KDState
-> String
-> Bool
-> Maybe (SBV Bool)
-> a
-> [Proof]
-> [String]
-> Maybe [String]
-> Maybe (IO ())
-> ((Int, Maybe NominalDiffTime) -> IO r)
-> m r
checkSatThen 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 Bool
inQuery Maybe (SBV Bool)
mbCtx a
prop [Proof]
by [String]
nms Maybe [String]
fullNms Maybe (IO ())
mbSat (Int, Maybe NominalDiffTime) -> IO r
unsat = do

        case Maybe (SBV Bool)
mbCtx of
           Just{}  -> m r -> m r
forall (m :: * -> *) a. (MonadIO m, MonadQuery m) => m a -> m a
inNewAssertionStack m r
check
           Maybe (SBV Bool)
Nothing -> 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 -> [String] -> IO Int
startKD SMTConfig
cfg Bool
verbose String
tag [String]
nms

           case mbCtx of
             Maybe (SBV Bool)
Nothing  -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"; checkSatThen: No context value to push."]
             Just SBV Bool
ctx -> do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"; checkSatThen: Pushing in the context: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBV Bool -> String
forall a. Show a => a -> String
show SBV Bool
ctx]
                            SBV Bool -> m ()
forall a. QuantifiedBool a => a -> m ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain SBV Bool
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 = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall {a}. Eq a => [a] -> [a]
squeeze ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (String -> Bool) -> String -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) ([String] -> Maybe [String] -> [String]
forall a. a -> Maybe a -> a
fromMaybe [String]
nms Maybe [String]
fullNms)
       squeeze :: [a] -> [a]
squeeze (a
x:a
y:[a]
rest) | a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
y = [a] -> [a]
squeeze (a
ya -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
rest)
       squeeze (a
x:[a]
rest)            = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a]
squeeze [a]
rest
       squeeze []                  = []

       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 <- if Bool
inQuery
                        then 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
                        else -- 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

                 let isEmpty = case SMTResult
res of
                                 Unsatisfiable{} -> -- Shouldn't really happen! bail out
                                                    String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String
" SBV.KnuckleDragger: Unexpected unsat-result while extracting a model."
                                                                    , String
"Please report this as a bug!"
                                                                    ]
                                 Satisfiable SMTConfig
_ SMTModel
m -> SMTModel -> Bool
isEmptyModel SMTModel
m  -- Expected case
                                 DeltaSat SMTConfig
_ Maybe String
_  SMTModel
m -> SMTModel -> Bool
isEmptyModel SMTModel
m  -- Unlikely but why not
                                 SatExtField SMTConfig
_ SMTModel
m -> SMTModel -> Bool
isEmptyModel SMTModel
m  -- Can't really happen
                                 Unknown{}       -> Bool
False           -- Possible, I suppose. Just print it
                                 ProofError{}    -> Bool
False           -- Ditto

                 liftIO $ case (isEmpty, mbSat) of
                           (Bool
True,  Just IO ()
act) -> IO ()
act
                           (Bool, Maybe (IO ()))
_                 -> 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

                 die