{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs             #-}
{-# LANGUAGE LambdaCase        #-}
{-# LANGUAGE NamedFieldPuns    #-}
{-# LANGUAGE RankNTypes        #-}
{-# LANGUAGE Trustworthy       #-}

-- | Connections to various SMT solvers and theorem provers.
module Copilot.Theorem.Prover.SMT
  (

    -- * Backends
    Backend
  , SmtFormat
  , SmtLib
  , Tptp
  , yices, dReal, altErgo, metit, z3, cvc4, mathsat

    -- * Tactics
  , Options (..)
  , induction, kInduction, onlySat, onlyValidity

    -- * Auxiliary
  , module Data.Default
  ) where

import Copilot.Theorem.IL.Translate
import Copilot.Theorem.IL
import Copilot.Theorem.Prove (Output (..), check, Proof, Universal, Existential)
import qualified Copilot.Theorem.Prove as P

import Copilot.Theorem.Prover.Backend
import qualified Copilot.Theorem.Prover.SMTIO as SMT

import Copilot.Theorem.Prover.SMTLib (SmtLib)
import Copilot.Theorem.Prover.TPTP (Tptp)
import qualified Copilot.Theorem.Prover.SMTLib as SMTLib
import qualified Copilot.Theorem.Prover.TPTP as TPTP

import Control.Monad (msum, unless, mzero)
import Control.Monad.State (StateT, runStateT, lift, get, modify)
import Control.Monad.IO.Class (liftIO)
import Control.Monad.Trans.Maybe (MaybeT (..))

import Data.Word
import Data.Maybe (fromJust, fromMaybe)
import Data.Function (on)
import Data.Default (Default(..))
import Data.Map (Map)
import qualified Data.Map as Map
import Copilot.Theorem.Misc.Utils

import System.IO (hClose)

-- * Tactics

-- | Options to configure the provers.
data Options = Options
  { Options -> Word32
startK :: Word32
    -- ^ Initial @k@ for the k-induction algorithm.

  , Options -> Word32
maxK :: Word32
    -- ^ The maximum number of steps of the k-induction algorithm the prover runs
    -- before giving up.

  , Options -> Bool
debug :: Bool
    -- ^ If @debug@ is set to @True@, the SMTLib/TPTP queries produced by the
    -- prover are displayed in the standard output.
  }

-- | Default 'Options' with a @0@ @k@ and a max of @10@ steps, and that produce
-- no debugging info.
instance Default Options where
  def :: Options
def = Options
    { startK :: Word32
startK = Word32
0
    , maxK :: Word32
maxK   = Word32
10
    , debug :: Bool
debug  = Bool
False
    }

-- | Tactic to find only a proof of satisfiability.
onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential
onlySat :: forall a. SmtFormat a => Options -> Backend a -> Proof Existential
onlySat Options
opts Backend a
backend = forall a. Prover -> Proof a
check P.Prover
  { proverName :: PropId
P.proverName  = PropId
"OnlySat"
  , startProver :: Spec -> IO (ProofState a)
P.startProver = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b.
Options
-> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
ProofState Options
opts Backend a
backend forall k a. Map k a
Map.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> IL
translateWithBounds
  , askProver :: ProofState a -> [PropId] -> [PropId] -> IO Output
P.askProver   = forall b.
SmtFormat b =>
ProofState b -> [PropId] -> [PropId] -> IO Output
onlySat'
  , closeProver :: ProofState a -> IO ()
P.closeProver = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  }

-- | Tactic to find only a proof of validity.
onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal
onlyValidity :: forall a. SmtFormat a => Options -> Backend a -> Proof Universal
onlyValidity Options
opts Backend a
backend = forall a. Prover -> Proof a
check P.Prover
  { proverName :: PropId
P.proverName  = PropId
"OnlyValidity"
  , startProver :: Spec -> IO (ProofState a)
P.startProver = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b.
Options
-> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
ProofState Options
opts Backend a
backend forall k a. Map k a
Map.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> IL
translateWithBounds
  , askProver :: ProofState a -> [PropId] -> [PropId] -> IO Output
P.askProver   = forall b.
SmtFormat b =>
ProofState b -> [PropId] -> [PropId] -> IO Output
onlyValidity'
  , closeProver :: ProofState a -> IO ()
P.closeProver = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  }

-- | Tactic to find a proof by standard 1-induction.
--
-- The values for @startK@ and @maxK@ in the options are ignored.
induction :: SmtFormat a => Options -> Backend a -> Proof Universal
induction :: forall a. SmtFormat a => Options -> Backend a -> Proof Universal
induction Options
opts Backend a
backend = forall a. Prover -> Proof a
check P.Prover
  { proverName :: PropId
P.proverName  = PropId
"Induction"
  , startProver :: Spec -> IO (ProofState a)
P.startProver = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b.
Options
-> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
ProofState Options
opts Backend a
backend forall k a. Map k a
Map.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> IL
translateWithBounds
  , askProver :: ProofState a -> [PropId] -> [PropId] -> IO Output
P.askProver   = forall b.
SmtFormat b =>
Word32
-> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
kInduction' Word32
0 Word32
0
  , closeProver :: ProofState a -> IO ()
P.closeProver = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  }

-- | Tactic to find a proof by k-induction.
kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
kInduction :: forall a. SmtFormat a => Options -> Backend a -> Proof Universal
kInduction Options
opts Backend a
backend = forall a. Prover -> Proof a
check P.Prover
  { proverName :: PropId
P.proverName  = PropId
"K-Induction"
  , startProver :: Spec -> IO (ProofState a)
P.startProver = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b.
Options
-> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
ProofState Options
opts Backend a
backend forall k a. Map k a
Map.empty forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> IL
translateWithBounds
  , askProver :: ProofState a -> [PropId] -> [PropId] -> IO Output
P.askProver   = forall b.
SmtFormat b =>
Word32
-> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
kInduction' (Options -> Word32
startK Options
opts) (Options -> Word32
maxK Options
opts)
  , closeProver :: ProofState a -> IO ()
P.closeProver = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  }

-- * Backends

-- | Backend to the Yices 2 SMT solver.
--
-- It enables non-linear arithmetic (@QF_NRA@), which means MCSat will be used.
--
-- The command @yices-smt2@ must be in the user's @PATH@.
yices :: Backend SmtLib
yices :: Backend SmtLib
yices = Backend
  { name :: PropId
name            = PropId
"Yices"
  , cmd :: PropId
cmd             = PropId
"yices-smt2"
  , cmdOpts :: [PropId]
cmdOpts         = [PropId
"--incremental"]
  , inputTerminator :: Handle -> IO ()
inputTerminator = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  , incremental :: Bool
incremental     = Bool
True
  , logic :: PropId
logic           = PropId
"QF_NRA"
  , interpret :: PropId -> Maybe SatResult
interpret       = PropId -> Maybe SatResult
SMTLib.interpret
  }

-- | Backend to the cvc4 SMT solver.
--
-- It enables support for uninterpreted functions and mixed nonlinear
-- arithmetic (@QF_NIRA@).
--
-- The command @cvc4@ must be in the user's @PATH@.
cvc4 :: Backend SmtLib
cvc4 :: Backend SmtLib
cvc4 = Backend
  { name :: PropId
name            = PropId
"CVC4"
  , cmd :: PropId
cmd             = PropId
"cvc4"
  , cmdOpts :: [PropId]
cmdOpts         = [PropId
"--incremental", PropId
"--lang=smt2", PropId
"--tlimit-per=5000"]
  , inputTerminator :: Handle -> IO ()
inputTerminator = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  , incremental :: Bool
incremental     = Bool
True
  , logic :: PropId
logic           = PropId
"QF_UFNIRA"
  , interpret :: PropId -> Maybe SatResult
interpret       = PropId -> Maybe SatResult
SMTLib.interpret
  }

-- | Backend to the Alt-Ergo SMT solver.
--
-- It enables support for uninterpreted functions and mixed nonlinear
-- arithmetic (@QF_NIRA@).
--
-- The command @alt-ergo.opt@ must be in the user's @PATH@.
altErgo :: Backend SmtLib
altErgo :: Backend SmtLib
altErgo = Backend
  { name :: PropId
name            = PropId
"Alt-Ergo"
  , cmd :: PropId
cmd             = PropId
"alt-ergo.opt"
  , cmdOpts :: [PropId]
cmdOpts         = []
  , inputTerminator :: Handle -> IO ()
inputTerminator = Handle -> IO ()
hClose
  , incremental :: Bool
incremental     = Bool
False
  , logic :: PropId
logic           = PropId
"QF_UFNIRA"
  , interpret :: PropId -> Maybe SatResult
interpret       = PropId -> Maybe SatResult
SMTLib.interpret
  }

-- | Backend to the Z3 theorem prover.
--
-- The command @z3@ must be in the user's @PATH@.
z3 :: Backend SmtLib
z3 :: Backend SmtLib
z3 = Backend
  { name :: PropId
name            = PropId
"Z3"
  , cmd :: PropId
cmd             = PropId
"z3"
  , cmdOpts :: [PropId]
cmdOpts         = [PropId
"-smt2", PropId
"-in"]
  , inputTerminator :: Handle -> IO ()
inputTerminator = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  , incremental :: Bool
incremental     = Bool
True
  , logic :: PropId
logic           = PropId
""
  , interpret :: PropId -> Maybe SatResult
interpret       = PropId -> Maybe SatResult
SMTLib.interpret
  }

-- | Backend to the dReal SMT solver.
--
-- It enables non-linear arithmetic (@QF_NRA@).
--
-- The libraries for dReal must be installed and @perl@ must be in the user's
-- @PATH@.
dReal :: Backend SmtLib
dReal :: Backend SmtLib
dReal = Backend
  { name :: PropId
name            = PropId
"dReal"
  , cmd :: PropId
cmd             = PropId
"perl"
  , cmdOpts :: [PropId]
cmdOpts         = [PropId
"-e", PropId
"alarm 10; exec dReal"]
  , inputTerminator :: Handle -> IO ()
inputTerminator = Handle -> IO ()
hClose
  , incremental :: Bool
incremental     = Bool
False
  , logic :: PropId
logic           = PropId
"QF_NRA"
  , interpret :: PropId -> Maybe SatResult
interpret       = PropId -> Maybe SatResult
SMTLib.interpret
  }

-- | Backend to the Mathsat SMT solver.
--
-- It enables non-linear arithmetic (@QF_NRA@).
--
-- The command @mathsat@ must be in the user's @PATH@.
mathsat :: Backend SmtLib
mathsat :: Backend SmtLib
mathsat = Backend
  { name :: PropId
name            = PropId
"MathSAT"
  , cmd :: PropId
cmd             = PropId
"mathsat"
  , cmdOpts :: [PropId]
cmdOpts         = []
  , inputTerminator :: Handle -> IO ()
inputTerminator = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
  , incremental :: Bool
incremental     = Bool
True
  , logic :: PropId
logic           = PropId
"QF_NRA"
  , interpret :: PropId -> Maybe SatResult
interpret       = PropId -> Maybe SatResult
SMTLib.interpret
  }

-- | Backend to the MetiTaski theorem prover.
--
-- The command @metit@ must be in the user's @PATH@.
--
-- The argument string is the path to the @tptp@ subdirectory of the metitarski
-- install location.
metit :: String -> Backend Tptp
metit :: PropId -> Backend Tptp
metit PropId
installDir = Backend
  { name :: PropId
name            = PropId
"MetiTarski"
  , cmd :: PropId
cmd             = PropId
"metit"
  , cmdOpts :: [PropId]
cmdOpts         =
      [ PropId
"--time", PropId
"5"
      , PropId
"--autoInclude"
      , PropId
"--tptp", PropId
installDir
      , PropId
"/dev/stdin"
      ]
  , inputTerminator :: Handle -> IO ()
inputTerminator = Handle -> IO ()
hClose
  , incremental :: Bool
incremental     = Bool
False
  , logic :: PropId
logic           = PropId
""
  , interpret :: PropId -> Maybe SatResult
interpret       = PropId -> Maybe SatResult
TPTP.interpret
  }

-- | Checks the Copilot specification with k-induction

type ProofScript b = MaybeT (StateT (ProofState b) IO)

runPS :: ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS :: forall b a.
ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS ProofScript b a
ps = forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT ProofScript b a
ps)

data ProofState b = ProofState
  { forall b. ProofState b -> Options
options :: Options
  , forall b. ProofState b -> Backend b
backend :: Backend b
  , forall b. ProofState b -> Map SolverId (Solver b)
solvers :: Map SolverId (SMT.Solver b)
  , forall b. ProofState b -> IL
spec    :: IL
  }

data SolverId = Base | Step
  deriving (Int -> SolverId -> ShowS
[SolverId] -> ShowS
SolverId -> PropId
forall a.
(Int -> a -> ShowS) -> (a -> PropId) -> ([a] -> ShowS) -> Show a
showList :: [SolverId] -> ShowS
$cshowList :: [SolverId] -> ShowS
show :: SolverId -> PropId
$cshow :: SolverId -> PropId
showsPrec :: Int -> SolverId -> ShowS
$cshowsPrec :: Int -> SolverId -> ShowS
Show, Eq SolverId
SolverId -> SolverId -> Bool
SolverId -> SolverId -> Ordering
SolverId -> SolverId -> SolverId
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SolverId -> SolverId -> SolverId
$cmin :: SolverId -> SolverId -> SolverId
max :: SolverId -> SolverId -> SolverId
$cmax :: SolverId -> SolverId -> SolverId
>= :: SolverId -> SolverId -> Bool
$c>= :: SolverId -> SolverId -> Bool
> :: SolverId -> SolverId -> Bool
$c> :: SolverId -> SolverId -> Bool
<= :: SolverId -> SolverId -> Bool
$c<= :: SolverId -> SolverId -> Bool
< :: SolverId -> SolverId -> Bool
$c< :: SolverId -> SolverId -> Bool
compare :: SolverId -> SolverId -> Ordering
$ccompare :: SolverId -> SolverId -> Ordering
Ord, SolverId -> SolverId -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SolverId -> SolverId -> Bool
$c/= :: SolverId -> SolverId -> Bool
== :: SolverId -> SolverId -> Bool
$c== :: SolverId -> SolverId -> Bool
Eq)

getModels :: [PropId] -> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
getModels :: forall b.
[PropId]
-> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
getModels [PropId]
assumptionIds [PropId]
toCheckIds = do
  IL {[Expr]
modelInit :: IL -> [Expr]
modelInit :: [Expr]
modelInit, [Expr]
modelRec :: IL -> [Expr]
modelRec :: [Expr]
modelRec, Map PropId ([Expr], Expr)
properties :: IL -> Map PropId ([Expr], Expr)
properties :: Map PropId ([Expr], Expr)
properties, Bool
inductive :: IL -> Bool
inductive :: Bool
inductive} <- forall b. ProofState b -> IL
spec forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
  let ([Expr]
as, [Expr]
as')       = [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
selectProps [PropId]
assumptionIds Map PropId ([Expr], Expr)
properties
      ([Expr]
as'', [Expr]
toCheck) = [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
selectProps [PropId]
toCheckIds Map PropId ([Expr], Expr)
properties
      modelRec' :: [Expr]
modelRec'       = [Expr]
modelRec forall a. [a] -> [a] -> [a]
++ [Expr]
as forall a. [a] -> [a] -> [a]
++ [Expr]
as' forall a. [a] -> [a] -> [a]
++ [Expr]
as''
  forall (m :: * -> *) a. Monad m => a -> m a
return ([Expr]
modelInit, [Expr]
modelRec', [Expr]
toCheck, Bool
inductive)

getSolver :: SmtFormat b => SolverId -> ProofScript b (SMT.Solver b)
getSolver :: forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid = do
  Map SolverId (Solver b)
solvers <- forall b. ProofState b -> Map SolverId (Solver b)
solvers forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SolverId
sid Map SolverId (Solver b)
solvers of
    Maybe (Solver b)
Nothing -> forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
startNewSolver SolverId
sid
    Just Solver b
solver -> forall (m :: * -> *) a. Monad m => a -> m a
return Solver b
solver

setSolver :: SolverId -> SMT.Solver b -> ProofScript b ()
setSolver :: forall b. SolverId -> Solver b -> ProofScript b ()
setSolver SolverId
sid Solver b
solver =
  (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify) forall a b. (a -> b) -> a -> b
$ \ProofState b
s -> ProofState b
s { solvers :: Map SolverId (Solver b)
solvers = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SolverId
sid Solver b
solver (forall b. ProofState b -> Map SolverId (Solver b)
solvers ProofState b
s) }

deleteSolver :: SolverId -> ProofScript b ()
deleteSolver :: forall b. SolverId -> ProofScript b ()
deleteSolver SolverId
sid =
  (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify) forall a b. (a -> b) -> a -> b
$ \ProofState b
s -> ProofState b
s { solvers :: Map SolverId (Solver b)
solvers = forall k a. Ord k => k -> Map k a -> Map k a
Map.delete SolverId
sid (forall b. ProofState b -> Map SolverId (Solver b)
solvers ProofState b
s) }

startNewSolver :: SmtFormat b => SolverId -> ProofScript b (SMT.Solver b)
startNewSolver :: forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
startNewSolver SolverId
sid = do
  Bool
dbg <- (forall b. ProofState b -> Options
options forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options -> Bool
debug)
  Backend b
backend <- forall b. ProofState b -> Backend b
backend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
  Solver b
s <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a.
SmtFormat a =>
PropId -> Bool -> Backend a -> IO (Solver a)
SMT.startNewSolver (forall a. Show a => a -> PropId
show SolverId
sid) Bool
dbg Backend b
backend
  forall b. SolverId -> Solver b -> ProofScript b ()
setSolver SolverId
sid Solver b
s
  forall (m :: * -> *) a. Monad m => a -> m a
return Solver b
s

declVars :: SmtFormat b => SolverId -> [VarDescr] -> ProofScript b ()
declVars :: forall b. SmtFormat b => SolverId -> [VarDescr] -> ProofScript b ()
declVars SolverId
sid [VarDescr]
vs = do
  Solver b
s <- forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid
  Solver b
s' <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. SmtFormat a => Solver a -> [VarDescr] -> IO (Solver a)
SMT.declVars Solver b
s [VarDescr]
vs
  forall b. SolverId -> Solver b -> ProofScript b ()
setSolver SolverId
sid Solver b
s'

assume :: SmtFormat b => SolverId -> [Expr] -> ProofScript b ()
assume :: forall b. SmtFormat b => SolverId -> [Expr] -> ProofScript b ()
assume SolverId
sid [Expr]
cs = do
  Solver b
s <- forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid
  Solver b
s' <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. SmtFormat a => Solver a -> [Expr] -> IO (Solver a)
SMT.assume Solver b
s [Expr]
cs
  forall b. SolverId -> Solver b -> ProofScript b ()
setSolver SolverId
sid Solver b
s'

entailed :: SmtFormat b => SolverId -> [Expr] -> ProofScript b SatResult
entailed :: forall b.
SmtFormat b =>
SolverId -> [Expr] -> ProofScript b SatResult
entailed SolverId
sid [Expr]
cs = do
  Backend b
backend <- forall b. ProofState b -> Backend b
backend forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
  Solver b
s <- forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid
  SatResult
result <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. SmtFormat a => Solver a -> [Expr] -> IO SatResult
SMT.entailed Solver b
s [Expr]
cs
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Backend a -> Bool
incremental Backend b
backend) forall a b. (a -> b) -> a -> b
$ forall b. SmtFormat b => SolverId -> ProofScript b ()
stop SolverId
sid
  forall (m :: * -> *) a. Monad m => a -> m a
return SatResult
result

stop :: SmtFormat b => SolverId -> ProofScript b ()
stop :: forall b. SmtFormat b => SolverId -> ProofScript b ()
stop SolverId
sid = do
  Solver b
s <- forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid
  forall b. SolverId -> ProofScript b ()
deleteSolver SolverId
sid
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. Solver a -> IO ()
SMT.stop Solver b
s

proofKind :: Integer -> String
proofKind :: Integer -> PropId
proofKind Integer
0 = PropId
"induction"
proofKind Integer
k = PropId
"k-induction (k = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> PropId
show Integer
k forall a. [a] -> [a] -> [a]
++ PropId
")"

stopSolvers :: SmtFormat b => ProofScript b ()
stopSolvers :: forall b. SmtFormat b => ProofScript b ()
stopSolvers = do
  Map SolverId (Solver b)
solvers <- forall b. ProofState b -> Map SolverId (Solver b)
solvers forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s (m :: * -> *). MonadState s m => m s
get
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall b. SmtFormat b => SolverId -> ProofScript b ()
stop (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Map k a -> [(k, a)]
Map.toList Map SolverId (Solver b)
solvers)

entailment :: SmtFormat b => SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment :: forall b.
SmtFormat b =>
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
sid [Expr]
assumptions [Expr]
props = do
  forall b. SmtFormat b => SolverId -> [VarDescr] -> ProofScript b ()
declVars SolverId
sid forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
nub' forall a b. (a -> b) -> a -> b
$ [Expr] -> [VarDescr]
getVars [Expr]
assumptions forall a. [a] -> [a] -> [a]
++ [Expr] -> [VarDescr]
getVars [Expr]
props
  forall b. SmtFormat b => SolverId -> [Expr] -> ProofScript b ()
assume SolverId
sid [Expr]
assumptions
  forall b.
SmtFormat b =>
SolverId -> [Expr] -> ProofScript b SatResult
entailed SolverId
sid [Expr]
props

getVars :: [Expr] -> [VarDescr]
getVars :: [Expr] -> [VarDescr]
getVars = forall a. (a -> a -> Ordering) -> [a] -> [a]
nubBy' (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` VarDescr -> PropId
varName) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [VarDescr]
getVars'
  where
    getVars' :: Expr -> [VarDescr]
    getVars' :: Expr -> [VarDescr]
getVars' = \case
      ConstB Bool
_             -> []
      ConstI Type
_ Integer
_           -> []
      ConstR Double
_             -> []
      Ite Type
_ Expr
e1 Expr
e2 Expr
e3       -> Expr -> [VarDescr]
getVars' Expr
e1 forall a. [a] -> [a] -> [a]
++ Expr -> [VarDescr]
getVars' Expr
e2 forall a. [a] -> [a] -> [a]
++ Expr -> [VarDescr]
getVars' Expr
e3
      Op1 Type
_ Op1
_ Expr
e            -> Expr -> [VarDescr]
getVars' Expr
e
      Op2 Type
_ Op2
_ Expr
e1 Expr
e2        -> Expr -> [VarDescr]
getVars' Expr
e1 forall a. [a] -> [a] -> [a]
++ Expr -> [VarDescr]
getVars' Expr
e2
      SVal Type
t PropId
seq (Fixed Integer
i) -> [PropId -> Type -> [Type] -> VarDescr
VarDescr (PropId
seq forall a. [a] -> [a] -> [a]
++ PropId
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> PropId
show Integer
i) Type
t []]
      SVal Type
t PropId
seq (Var Integer
i)   -> [PropId -> Type -> [Type] -> VarDescr
VarDescr (PropId
seq forall a. [a] -> [a] -> [a]
++ PropId
"_n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> PropId
show Integer
i) Type
t []]
      FunApp Type
t PropId
name [Expr]
args   -> [PropId -> Type -> [Type] -> VarDescr
VarDescr PropId
name Type
t (forall a b. (a -> b) -> [a] -> [b]
map Expr -> Type
typeOf [Expr]
args)]
                              forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [VarDescr]
getVars' [Expr]
args

unknown :: ProofScript b a
unknown :: forall b a. ProofScript b a
unknown = forall (m :: * -> *) a. MonadPlus m => m a
mzero

unknown' :: String -> ProofScript b Output
unknown' :: forall b. PropId -> ProofScript b Output
unknown' PropId
msg = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Status -> [PropId] -> Output
Output Status
P.Unknown [PropId
msg]

invalid :: String -> ProofScript b Output
invalid :: forall b. PropId -> ProofScript b Output
invalid PropId
msg = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Status -> [PropId] -> Output
Output Status
P.Invalid [PropId
msg]

sat :: String -> ProofScript b Output
sat :: forall b. PropId -> ProofScript b Output
sat PropId
msg = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Status -> [PropId] -> Output
Output Status
P.Sat [PropId
msg]

valid :: String -> ProofScript b Output
valid :: forall b. PropId -> ProofScript b Output
valid PropId
msg = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Status -> [PropId] -> Output
Output Status
P.Valid [PropId
msg]

kInduction' :: SmtFormat b => Word32 -> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
kInduction' :: forall b.
SmtFormat b =>
Word32
-> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
kInduction' Word32
startK Word32
maxK ProofState b
s [PropId]
as [PropId]
ps = (forall a. a -> Maybe a -> a
fromMaybe (Status -> [PropId] -> Output
Output Status
P.Unknown [PropId
"proof by k-induction failed"]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst)
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b a.
ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS (forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall a b. (a -> b) -> [a] -> [b]
map Integer -> MaybeT (StateT (ProofState b) IO) Output
induction [(forall a. Integral a => a -> Integer
toInteger Word32
startK) .. (forall a. Integral a => a -> Integer
toInteger Word32
maxK)]) forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall b. SmtFormat b => ProofScript b ()
stopSolvers) ProofState b
s
  where
    induction :: Integer -> MaybeT (StateT (ProofState b) IO) Output
induction Integer
k = do
      ([Expr]
modelInit, [Expr]
modelRec, [Expr]
toCheck, Bool
inductive) <- forall b.
[PropId]
-> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
getModels [PropId]
as [PropId]
ps

      let base :: [Expr]
base    = [SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
i) Expr
m | Expr
m <- [Expr]
modelRec, Integer
i <- [Integer
0 .. Integer
k]]
          baseInv :: [Expr]
baseInv = [SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
k) Expr
m | Expr
m <- [Expr]
toCheck]

      let step :: [Expr]
step    = [SeqIndex -> Expr -> Expr
evalAt (forall a. Integral a => a -> SeqIndex
_n_plus Integer
i) Expr
m | Expr
m <- [Expr]
modelRec, Integer
i <- [Integer
0 .. Integer
k forall a. Num a => a -> a -> a
+ Integer
1]]
                    forall a. [a] -> [a] -> [a]
++ [SeqIndex -> Expr -> Expr
evalAt (forall a. Integral a => a -> SeqIndex
_n_plus Integer
i) Expr
m | Expr
m <- [Expr]
toCheck, Integer
i <- [Integer
0 .. Integer
k]]
          stepInv :: [Expr]
stepInv = [SeqIndex -> Expr -> Expr
evalAt (forall a. Integral a => a -> SeqIndex
_n_plus forall a b. (a -> b) -> a -> b
$ Integer
k forall a. Num a => a -> a -> a
+ Integer
1) Expr
m | Expr
m <- [Expr]
toCheck]

      forall b.
SmtFormat b =>
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
Base ([Expr]
modelInit forall a. [a] -> [a] -> [a]
++ [Expr]
base) [Expr]
baseInv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        SatResult
Sat     -> forall b. PropId -> ProofScript b Output
invalid forall a b. (a -> b) -> a -> b
$ PropId
"base case failed for " forall a. [a] -> [a] -> [a]
++ Integer -> PropId
proofKind Integer
k
        SatResult
Unknown -> forall b a. ProofScript b a
unknown
        SatResult
Unsat   ->
          if Bool -> Bool
not Bool
inductive then forall b. PropId -> ProofScript b Output
valid (PropId
"proved without induction")
          else forall b.
SmtFormat b =>
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
Step [Expr]
step [Expr]
stepInv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            SatResult
Sat     -> forall b a. ProofScript b a
unknown
            SatResult
Unknown -> forall b a. ProofScript b a
unknown
            SatResult
Unsat   -> forall b. PropId -> ProofScript b Output
valid forall a b. (a -> b) -> a -> b
$ PropId
"proved with " forall a. [a] -> [a] -> [a]
++ Integer -> PropId
proofKind Integer
k

onlySat' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output
onlySat' :: forall b.
SmtFormat b =>
ProofState b -> [PropId] -> [PropId] -> IO Output
onlySat' ProofState b
s [PropId]
as [PropId]
ps = (forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b a.
ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS (MaybeT (StateT (ProofState b) IO) Output
script forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall b. SmtFormat b => ProofScript b ()
stopSolvers) ProofState b
s
  where
    script :: MaybeT (StateT (ProofState b) IO) Output
script  = do
      ([Expr]
modelInit, [Expr]
modelRec, [Expr]
toCheck, Bool
inductive) <- forall b.
[PropId]
-> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
getModels [PropId]
as [PropId]
ps

      let base :: [Expr]
base    = forall a b. (a -> b) -> [a] -> [b]
map (SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
0)) [Expr]
modelRec
          baseInv :: [Expr]
baseInv = forall a b. (a -> b) -> [a] -> [b]
map (SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
0)) [Expr]
toCheck

      if Bool
inductive
        then forall b. PropId -> ProofScript b Output
unknown' PropId
"proposition requires induction to prove."
        else forall b.
SmtFormat b =>
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
Base ([Expr]
modelInit forall a. [a] -> [a] -> [a]
++ [Expr]
base) (forall a b. (a -> b) -> [a] -> [b]
map (Type -> Op1 -> Expr -> Expr
Op1 Type
Bool Op1
Not) [Expr]
baseInv) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          SatResult
Unsat   -> forall b. PropId -> ProofScript b Output
invalid PropId
"prop not satisfiable"
          SatResult
Unknown -> forall b. PropId -> ProofScript b Output
unknown' PropId
"failed to find a satisfying model"
          SatResult
Sat     -> forall b. PropId -> ProofScript b Output
sat PropId
"prop is satisfiable"

onlyValidity' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output
onlyValidity' :: forall b.
SmtFormat b =>
ProofState b -> [PropId] -> [PropId] -> IO Output
onlyValidity' ProofState b
s [PropId]
as [PropId]
ps = (forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b a.
ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS (MaybeT (StateT (ProofState b) IO) Output
script forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall b. SmtFormat b => ProofScript b ()
stopSolvers) ProofState b
s
  where
    script :: MaybeT (StateT (ProofState b) IO) Output
script  = do
      ([Expr]
modelInit, [Expr]
modelRec, [Expr]
toCheck, Bool
inductive) <- forall b.
[PropId]
-> [PropId] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
getModels [PropId]
as [PropId]
ps

      let base :: [Expr]
base    = forall a b. (a -> b) -> [a] -> [b]
map (SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
0)) [Expr]
modelRec
          baseInv :: [Expr]
baseInv = forall a b. (a -> b) -> [a] -> [b]
map (SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
0)) [Expr]
toCheck

      if Bool
inductive
        then forall b. PropId -> ProofScript b Output
unknown' PropId
"proposition requires induction to prove."
        else forall b.
SmtFormat b =>
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
Base ([Expr]
modelInit forall a. [a] -> [a] -> [a]
++ [Expr]
base) [Expr]
baseInv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          SatResult
Unsat   -> forall b. PropId -> ProofScript b Output
valid PropId
"proof by SMT solver"
          SatResult
Unknown -> forall b a. ProofScript b a
unknown
          SatResult
Sat     -> forall b. PropId -> ProofScript b Output
invalid PropId
"SMT solver found a counter-example."

selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
selectProps [PropId]
propIds Map PropId ([Expr], Expr)
properties =
  (forall {t :: * -> *} {a} {b}. Foldable t => (t [a], b) -> ([a], b)
squash forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [(a, b)] -> ([a], [b])
unzip) [([Expr]
as, Expr
p) | (PropId
id, ([Expr]
as, Expr
p)) <- forall k a. Map k a -> [(k, a)]
Map.toList Map PropId ([Expr], Expr)
properties, PropId
id forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PropId]
propIds]
    where
      squash :: (t [a], b) -> ([a], b)
squash (t [a]
a, b
b) = (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat t [a]
a, b
b)