{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Trustworthy #-}
module Copilot.Theorem.Prover.SMT
(
Backend
, SmtFormat
, SmtLib
, Tptp
, yices, dReal, altErgo, metit, z3, cvc4, mathsat
, Options (..)
, induction, kInduction, onlySat, onlyValidity
, 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)
data Options = Options
{ Options -> Word32
startK :: Word32
, Options -> Word32
maxK :: Word32
, Options -> Bool
debug :: Bool
}
instance Default Options where
def :: Options
def = Options
{ startK :: Word32
startK = Word32
0
, maxK :: Word32
maxK = Word32
10
, debug :: Bool
debug = Bool
False
}
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 ()
}
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 ()
}
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 ()
}
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 ()
}
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
}
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
}
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
}
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
}
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
}
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
}
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
}
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)