{-# LANGUAGE LambdaCase, NamedFieldPuns, FlexibleInstances, RankNTypes, GADTs #-}
{-# 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 :: Word32 -> Word32 -> Bool -> Options
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 :: Options -> Backend a -> Proof Existential
onlySat Options
opts Backend a
backend = Prover -> Proof Existential
forall a. Prover -> Proof a
check Prover :: forall r.
String
-> (Spec -> IO r)
-> (r -> [String] -> [String] -> IO Output)
-> (r -> IO ())
-> Prover
P.Prover
{ proverName :: String
P.proverName = String
"OnlySat"
, startProver :: Spec -> IO (ProofState a)
P.startProver = ProofState a -> IO (ProofState a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState a -> IO (ProofState a))
-> (Spec -> ProofState a) -> Spec -> IO (ProofState a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options
-> Backend a -> Map SolverId (Solver a) -> IL -> ProofState a
forall b.
Options
-> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
ProofState Options
opts Backend a
backend Map SolverId (Solver a)
forall k a. Map k a
Map.empty (IL -> ProofState a) -> (Spec -> IL) -> Spec -> ProofState a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> IL
translateWithBounds
, askProver :: ProofState a -> [String] -> [String] -> IO Output
P.askProver = ProofState a -> [String] -> [String] -> IO Output
forall b.
SmtFormat b =>
ProofState b -> [String] -> [String] -> IO Output
onlySat'
, closeProver :: ProofState a -> IO ()
P.closeProver = IO () -> ProofState a -> IO ()
forall a b. a -> b -> a
const (IO () -> ProofState a -> IO ()) -> IO () -> ProofState a -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
}
onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal
onlyValidity :: Options -> Backend a -> Proof Universal
onlyValidity Options
opts Backend a
backend = Prover -> Proof Universal
forall a. Prover -> Proof a
check Prover :: forall r.
String
-> (Spec -> IO r)
-> (r -> [String] -> [String] -> IO Output)
-> (r -> IO ())
-> Prover
P.Prover
{ proverName :: String
P.proverName = String
"OnlyValidity"
, startProver :: Spec -> IO (ProofState a)
P.startProver = ProofState a -> IO (ProofState a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState a -> IO (ProofState a))
-> (Spec -> ProofState a) -> Spec -> IO (ProofState a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options
-> Backend a -> Map SolverId (Solver a) -> IL -> ProofState a
forall b.
Options
-> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
ProofState Options
opts Backend a
backend Map SolverId (Solver a)
forall k a. Map k a
Map.empty (IL -> ProofState a) -> (Spec -> IL) -> Spec -> ProofState a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> IL
translateWithBounds
, askProver :: ProofState a -> [String] -> [String] -> IO Output
P.askProver = ProofState a -> [String] -> [String] -> IO Output
forall b.
SmtFormat b =>
ProofState b -> [String] -> [String] -> IO Output
onlyValidity'
, closeProver :: ProofState a -> IO ()
P.closeProver = IO () -> ProofState a -> IO ()
forall a b. a -> b -> a
const (IO () -> ProofState a -> IO ()) -> IO () -> ProofState a -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
}
induction :: SmtFormat a => Options -> Backend a -> Proof Universal
induction :: Options -> Backend a -> Proof Universal
induction Options
opts Backend a
backend = Prover -> Proof Universal
forall a. Prover -> Proof a
check Prover :: forall r.
String
-> (Spec -> IO r)
-> (r -> [String] -> [String] -> IO Output)
-> (r -> IO ())
-> Prover
P.Prover
{ proverName :: String
P.proverName = String
"Induction"
, startProver :: Spec -> IO (ProofState a)
P.startProver = ProofState a -> IO (ProofState a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState a -> IO (ProofState a))
-> (Spec -> ProofState a) -> Spec -> IO (ProofState a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options
-> Backend a -> Map SolverId (Solver a) -> IL -> ProofState a
forall b.
Options
-> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
ProofState Options
opts Backend a
backend Map SolverId (Solver a)
forall k a. Map k a
Map.empty (IL -> ProofState a) -> (Spec -> IL) -> Spec -> ProofState a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> IL
translateWithBounds
, askProver :: ProofState a -> [String] -> [String] -> IO Output
P.askProver = Word32
-> Word32 -> ProofState a -> [String] -> [String] -> IO Output
forall b.
SmtFormat b =>
Word32
-> Word32 -> ProofState b -> [String] -> [String] -> IO Output
kInduction' Word32
0 Word32
0
, closeProver :: ProofState a -> IO ()
P.closeProver = IO () -> ProofState a -> IO ()
forall a b. a -> b -> a
const (IO () -> ProofState a -> IO ()) -> IO () -> ProofState a -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
}
kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
kInduction :: Options -> Backend a -> Proof Universal
kInduction Options
opts Backend a
backend = Prover -> Proof Universal
forall a. Prover -> Proof a
check Prover :: forall r.
String
-> (Spec -> IO r)
-> (r -> [String] -> [String] -> IO Output)
-> (r -> IO ())
-> Prover
P.Prover
{ proverName :: String
P.proverName = String
"K-Induction"
, startProver :: Spec -> IO (ProofState a)
P.startProver = ProofState a -> IO (ProofState a)
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState a -> IO (ProofState a))
-> (Spec -> ProofState a) -> Spec -> IO (ProofState a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options
-> Backend a -> Map SolverId (Solver a) -> IL -> ProofState a
forall b.
Options
-> Backend b -> Map SolverId (Solver b) -> IL -> ProofState b
ProofState Options
opts Backend a
backend Map SolverId (Solver a)
forall k a. Map k a
Map.empty (IL -> ProofState a) -> (Spec -> IL) -> Spec -> ProofState a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> IL
translateWithBounds
, askProver :: ProofState a -> [String] -> [String] -> IO Output
P.askProver = Word32
-> Word32 -> ProofState a -> [String] -> [String] -> IO Output
forall b.
SmtFormat b =>
Word32
-> Word32 -> ProofState b -> [String] -> [String] -> IO Output
kInduction' (Options -> Word32
startK Options
opts) (Options -> Word32
maxK Options
opts)
, closeProver :: ProofState a -> IO ()
P.closeProver = IO () -> ProofState a -> IO ()
forall a b. a -> b -> a
const (IO () -> ProofState a -> IO ()) -> IO () -> ProofState a -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
}
yices :: Backend SmtLib
yices :: Backend SmtLib
yices = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
{ name :: String
name = String
"Yices"
, cmd :: String
cmd = String
"yices-smt2"
, cmdOpts :: [String]
cmdOpts = [String
"--incremental"]
, inputTerminator :: Handle -> IO ()
inputTerminator = IO () -> Handle -> IO ()
forall a b. a -> b -> a
const (IO () -> Handle -> IO ()) -> IO () -> Handle -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, incremental :: Bool
incremental = Bool
True
, logic :: String
logic = String
"QF_NRA"
, interpret :: String -> Maybe SatResult
interpret = String -> Maybe SatResult
SMTLib.interpret
}
cvc4 :: Backend SmtLib
cvc4 :: Backend SmtLib
cvc4 = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
{ name :: String
name = String
"CVC4"
, cmd :: String
cmd = String
"cvc4"
, cmdOpts :: [String]
cmdOpts = [String
"--incremental", String
"--lang=smt2", String
"--tlimit-per=5000"]
, inputTerminator :: Handle -> IO ()
inputTerminator = IO () -> Handle -> IO ()
forall a b. a -> b -> a
const (IO () -> Handle -> IO ()) -> IO () -> Handle -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, incremental :: Bool
incremental = Bool
True
, logic :: String
logic = String
"QF_UFNIRA"
, interpret :: String -> Maybe SatResult
interpret = String -> Maybe SatResult
SMTLib.interpret
}
altErgo :: Backend SmtLib
altErgo :: Backend SmtLib
altErgo = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
{ name :: String
name = String
"Alt-Ergo"
, cmd :: String
cmd = String
"alt-ergo.opt"
, cmdOpts :: [String]
cmdOpts = []
, inputTerminator :: Handle -> IO ()
inputTerminator = Handle -> IO ()
hClose
, incremental :: Bool
incremental = Bool
False
, logic :: String
logic = String
"QF_UFNIRA"
, interpret :: String -> Maybe SatResult
interpret = String -> Maybe SatResult
SMTLib.interpret
}
z3 :: Backend SmtLib
z3 :: Backend SmtLib
z3 = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
{ name :: String
name = String
"Z3"
, cmd :: String
cmd = String
"z3"
, cmdOpts :: [String]
cmdOpts = [String
"-smt2", String
"-in"]
, inputTerminator :: Handle -> IO ()
inputTerminator = IO () -> Handle -> IO ()
forall a b. a -> b -> a
const (IO () -> Handle -> IO ()) -> IO () -> Handle -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, incremental :: Bool
incremental = Bool
True
, logic :: String
logic = String
""
, interpret :: String -> Maybe SatResult
interpret = String -> Maybe SatResult
SMTLib.interpret
}
dReal :: Backend SmtLib
dReal :: Backend SmtLib
dReal = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
{ name :: String
name = String
"dReal"
, cmd :: String
cmd = String
"perl"
, cmdOpts :: [String]
cmdOpts = [String
"-e", String
"alarm 10; exec dReal"]
, inputTerminator :: Handle -> IO ()
inputTerminator = Handle -> IO ()
hClose
, incremental :: Bool
incremental = Bool
False
, logic :: String
logic = String
"QF_NRA"
, interpret :: String -> Maybe SatResult
interpret = String -> Maybe SatResult
SMTLib.interpret
}
mathsat :: Backend SmtLib
mathsat :: Backend SmtLib
mathsat = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
{ name :: String
name = String
"MathSAT"
, cmd :: String
cmd = String
"mathsat"
, cmdOpts :: [String]
cmdOpts = []
, inputTerminator :: Handle -> IO ()
inputTerminator = IO () -> Handle -> IO ()
forall a b. a -> b -> a
const (IO () -> Handle -> IO ()) -> IO () -> Handle -> IO ()
forall a b. (a -> b) -> a -> b
$ () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
, incremental :: Bool
incremental = Bool
True
, logic :: String
logic = String
"QF_NRA"
, interpret :: String -> Maybe SatResult
interpret = String -> Maybe SatResult
SMTLib.interpret
}
metit :: String -> Backend Tptp
metit :: String -> Backend Tptp
metit String
installDir = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
{ name :: String
name = String
"MetiTarski"
, cmd :: String
cmd = String
"metit"
, cmdOpts :: [String]
cmdOpts =
[ String
"--time", String
"5"
, String
"--autoInclude"
, String
"--tptp", String
installDir
, String
"/dev/stdin"
]
, inputTerminator :: Handle -> IO ()
inputTerminator = Handle -> IO ()
hClose
, incremental :: Bool
incremental = Bool
False
, logic :: String
logic = String
""
, interpret :: String -> Maybe SatResult
interpret = String -> Maybe SatResult
TPTP.interpret
}
type ProofScript b = MaybeT (StateT (ProofState b) IO)
runPS :: ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS :: ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS ProofScript b a
ps = StateT (ProofState b) IO (Maybe a)
-> ProofState b -> IO (Maybe a, ProofState b)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (ProofScript b a -> StateT (ProofState b) IO (Maybe a)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT ProofScript b a
ps)
data ProofState b = ProofState
{ ProofState b -> Options
options :: Options
, ProofState b -> Backend b
backend :: Backend b
, ProofState b -> Map SolverId (Solver b)
solvers :: Map SolverId (SMT.Solver b)
, ProofState b -> IL
spec :: IL
}
data SolverId = Base | Step
deriving (Int -> SolverId -> ShowS
[SolverId] -> ShowS
SolverId -> String
(Int -> SolverId -> ShowS)
-> (SolverId -> String) -> ([SolverId] -> ShowS) -> Show SolverId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SolverId] -> ShowS
$cshowList :: [SolverId] -> ShowS
show :: SolverId -> String
$cshow :: SolverId -> String
showsPrec :: Int -> SolverId -> ShowS
$cshowsPrec :: Int -> SolverId -> ShowS
Show, Eq SolverId
Eq SolverId
-> (SolverId -> SolverId -> Ordering)
-> (SolverId -> SolverId -> Bool)
-> (SolverId -> SolverId -> Bool)
-> (SolverId -> SolverId -> Bool)
-> (SolverId -> SolverId -> Bool)
-> (SolverId -> SolverId -> SolverId)
-> (SolverId -> SolverId -> SolverId)
-> Ord 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
$cp1Ord :: Eq SolverId
Ord, SolverId -> SolverId -> Bool
(SolverId -> SolverId -> Bool)
-> (SolverId -> SolverId -> Bool) -> Eq SolverId
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 :: [String]
-> [String] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
getModels [String]
assumptionIds [String]
toCheckIds = do
IL {[Expr]
modelInit :: IL -> [Expr]
modelInit :: [Expr]
modelInit, [Expr]
modelRec :: IL -> [Expr]
modelRec :: [Expr]
modelRec, Map String ([Expr], Expr)
properties :: IL -> Map String ([Expr], Expr)
properties :: Map String ([Expr], Expr)
properties, Bool
inductive :: IL -> Bool
inductive :: Bool
inductive} <- ProofState b -> IL
forall b. ProofState b -> IL
spec (ProofState b -> IL)
-> MaybeT (StateT (ProofState b) IO) (ProofState b)
-> MaybeT (StateT (ProofState b) IO) IL
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (StateT (ProofState b) IO) (ProofState b)
forall s (m :: * -> *). MonadState s m => m s
get
let ([Expr]
as, [Expr]
as') = [String] -> Map String ([Expr], Expr) -> ([Expr], [Expr])
selectProps [String]
assumptionIds Map String ([Expr], Expr)
properties
([Expr]
as'', [Expr]
toCheck) = [String] -> Map String ([Expr], Expr) -> ([Expr], [Expr])
selectProps [String]
toCheckIds Map String ([Expr], Expr)
properties
modelRec' :: [Expr]
modelRec' = [Expr]
modelRec [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
as [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
as' [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
as''
([Expr], [Expr], [Expr], Bool)
-> ProofScript b ([Expr], [Expr], [Expr], Bool)
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 :: SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid = do
Map SolverId (Solver b)
solvers <- ProofState b -> Map SolverId (Solver b)
forall b. ProofState b -> Map SolverId (Solver b)
solvers (ProofState b -> Map SolverId (Solver b))
-> MaybeT (StateT (ProofState b) IO) (ProofState b)
-> MaybeT (StateT (ProofState b) IO) (Map SolverId (Solver b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (StateT (ProofState b) IO) (ProofState b)
forall s (m :: * -> *). MonadState s m => m s
get
case SolverId -> Map SolverId (Solver b) -> Maybe (Solver b)
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 -> SolverId -> ProofScript b (Solver b)
forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
startNewSolver SolverId
sid
Just Solver b
solver -> Solver b -> ProofScript b (Solver b)
forall (m :: * -> *) a. Monad m => a -> m a
return Solver b
solver
setSolver :: SolverId -> SMT.Solver b -> ProofScript b ()
setSolver :: SolverId -> Solver b -> ProofScript b ()
setSolver SolverId
sid Solver b
solver =
(StateT (ProofState b) IO () -> ProofScript b ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT (ProofState b) IO () -> ProofScript b ())
-> ((ProofState b -> ProofState b) -> StateT (ProofState b) IO ())
-> (ProofState b -> ProofState b)
-> ProofScript b ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProofState b -> ProofState b) -> StateT (ProofState b) IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify) ((ProofState b -> ProofState b) -> ProofScript b ())
-> (ProofState b -> ProofState b) -> ProofScript b ()
forall a b. (a -> b) -> a -> b
$ \ProofState b
s -> ProofState b
s { solvers :: Map SolverId (Solver b)
solvers = SolverId
-> Solver b -> Map SolverId (Solver b) -> Map SolverId (Solver b)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SolverId
sid Solver b
solver (ProofState b -> Map SolverId (Solver b)
forall b. ProofState b -> Map SolverId (Solver b)
solvers ProofState b
s) }
deleteSolver :: SolverId -> ProofScript b ()
deleteSolver :: SolverId -> ProofScript b ()
deleteSolver SolverId
sid =
(StateT (ProofState b) IO () -> ProofScript b ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT (ProofState b) IO () -> ProofScript b ())
-> ((ProofState b -> ProofState b) -> StateT (ProofState b) IO ())
-> (ProofState b -> ProofState b)
-> ProofScript b ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ProofState b -> ProofState b) -> StateT (ProofState b) IO ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify) ((ProofState b -> ProofState b) -> ProofScript b ())
-> (ProofState b -> ProofState b) -> ProofScript b ()
forall a b. (a -> b) -> a -> b
$ \ProofState b
s -> ProofState b
s { solvers :: Map SolverId (Solver b)
solvers = SolverId -> Map SolverId (Solver b) -> Map SolverId (Solver b)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete SolverId
sid (ProofState b -> Map SolverId (Solver b)
forall b. ProofState b -> Map SolverId (Solver b)
solvers ProofState b
s) }
startNewSolver :: SmtFormat b => SolverId -> ProofScript b (SMT.Solver b)
startNewSolver :: SolverId -> ProofScript b (Solver b)
startNewSolver SolverId
sid = do
Bool
dbg <- (ProofState b -> Options
forall b. ProofState b -> Options
options (ProofState b -> Options)
-> MaybeT (StateT (ProofState b) IO) (ProofState b)
-> MaybeT (StateT (ProofState b) IO) Options
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (StateT (ProofState b) IO) (ProofState b)
forall s (m :: * -> *). MonadState s m => m s
get MaybeT (StateT (ProofState b) IO) Options
-> (Options -> MaybeT (StateT (ProofState b) IO) Bool)
-> MaybeT (StateT (ProofState b) IO) Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Bool -> MaybeT (StateT (ProofState b) IO) Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> MaybeT (StateT (ProofState b) IO) Bool)
-> (Options -> Bool)
-> Options
-> MaybeT (StateT (ProofState b) IO) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Options -> Bool
debug)
Backend b
backend <- ProofState b -> Backend b
forall b. ProofState b -> Backend b
backend (ProofState b -> Backend b)
-> MaybeT (StateT (ProofState b) IO) (ProofState b)
-> MaybeT (StateT (ProofState b) IO) (Backend b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (StateT (ProofState b) IO) (ProofState b)
forall s (m :: * -> *). MonadState s m => m s
get
Solver b
s <- IO (Solver b) -> ProofScript b (Solver b)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Solver b) -> ProofScript b (Solver b))
-> IO (Solver b) -> ProofScript b (Solver b)
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Backend b -> IO (Solver b)
forall a.
SmtFormat a =>
String -> Bool -> Backend a -> IO (Solver a)
SMT.startNewSolver (SolverId -> String
forall a. Show a => a -> String
show SolverId
sid) Bool
dbg Backend b
backend
SolverId -> Solver b -> ProofScript b ()
forall b. SolverId -> Solver b -> ProofScript b ()
setSolver SolverId
sid Solver b
s
Solver b -> ProofScript b (Solver b)
forall (m :: * -> *) a. Monad m => a -> m a
return Solver b
s
declVars :: SmtFormat b => SolverId -> [VarDescr] -> ProofScript b ()
declVars :: SolverId -> [VarDescr] -> ProofScript b ()
declVars SolverId
sid [VarDescr]
vs = do
Solver b
s <- SolverId -> ProofScript b (Solver b)
forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid
Solver b
s' <- IO (Solver b) -> ProofScript b (Solver b)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Solver b) -> ProofScript b (Solver b))
-> IO (Solver b) -> ProofScript b (Solver b)
forall a b. (a -> b) -> a -> b
$ Solver b -> [VarDescr] -> IO (Solver b)
forall a. SmtFormat a => Solver a -> [VarDescr] -> IO (Solver a)
SMT.declVars Solver b
s [VarDescr]
vs
SolverId -> Solver b -> ProofScript b ()
forall b. SolverId -> Solver b -> ProofScript b ()
setSolver SolverId
sid Solver b
s'
assume :: SmtFormat b => SolverId -> [Expr] -> ProofScript b ()
assume :: SolverId -> [Expr] -> ProofScript b ()
assume SolverId
sid [Expr]
cs = do
Solver b
s <- SolverId -> ProofScript b (Solver b)
forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid
Solver b
s' <- IO (Solver b) -> ProofScript b (Solver b)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Solver b) -> ProofScript b (Solver b))
-> IO (Solver b) -> ProofScript b (Solver b)
forall a b. (a -> b) -> a -> b
$ Solver b -> [Expr] -> IO (Solver b)
forall a. SmtFormat a => Solver a -> [Expr] -> IO (Solver a)
SMT.assume Solver b
s [Expr]
cs
SolverId -> Solver b -> ProofScript b ()
forall b. SolverId -> Solver b -> ProofScript b ()
setSolver SolverId
sid Solver b
s'
entailed :: SmtFormat b => SolverId -> [Expr] -> ProofScript b SatResult
entailed :: SolverId -> [Expr] -> ProofScript b SatResult
entailed SolverId
sid [Expr]
cs = do
Backend b
backend <- ProofState b -> Backend b
forall b. ProofState b -> Backend b
backend (ProofState b -> Backend b)
-> MaybeT (StateT (ProofState b) IO) (ProofState b)
-> MaybeT (StateT (ProofState b) IO) (Backend b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (StateT (ProofState b) IO) (ProofState b)
forall s (m :: * -> *). MonadState s m => m s
get
Solver b
s <- SolverId -> ProofScript b (Solver b)
forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid
SatResult
result <- IO SatResult -> ProofScript b SatResult
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SatResult -> ProofScript b SatResult)
-> IO SatResult -> ProofScript b SatResult
forall a b. (a -> b) -> a -> b
$ Solver b -> [Expr] -> IO SatResult
forall a. SmtFormat a => Solver a -> [Expr] -> IO SatResult
SMT.entailed Solver b
s [Expr]
cs
Bool
-> MaybeT (StateT (ProofState b) IO) ()
-> MaybeT (StateT (ProofState b) IO) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Backend b -> Bool
forall a. Backend a -> Bool
incremental Backend b
backend) (MaybeT (StateT (ProofState b) IO) ()
-> MaybeT (StateT (ProofState b) IO) ())
-> MaybeT (StateT (ProofState b) IO) ()
-> MaybeT (StateT (ProofState b) IO) ()
forall a b. (a -> b) -> a -> b
$ SolverId -> MaybeT (StateT (ProofState b) IO) ()
forall b. SmtFormat b => SolverId -> ProofScript b ()
stop SolverId
sid
SatResult -> ProofScript b SatResult
forall (m :: * -> *) a. Monad m => a -> m a
return SatResult
result
stop :: SmtFormat b => SolverId -> ProofScript b ()
stop :: SolverId -> ProofScript b ()
stop SolverId
sid = do
Solver b
s <- SolverId -> ProofScript b (Solver b)
forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
getSolver SolverId
sid
SolverId -> ProofScript b ()
forall b. SolverId -> ProofScript b ()
deleteSolver SolverId
sid
IO () -> ProofScript b ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> ProofScript b ()) -> IO () -> ProofScript b ()
forall a b. (a -> b) -> a -> b
$ Solver b -> IO ()
forall a. Solver a -> IO ()
SMT.stop Solver b
s
proofKind :: Integer -> String
proofKind :: Integer -> String
proofKind Integer
0 = String
"induction"
proofKind Integer
k = String
"k-induction (k = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
stopSolvers :: SmtFormat b => ProofScript b ()
stopSolvers :: ProofScript b ()
stopSolvers = do
Map SolverId (Solver b)
solvers <- ProofState b -> Map SolverId (Solver b)
forall b. ProofState b -> Map SolverId (Solver b)
solvers (ProofState b -> Map SolverId (Solver b))
-> MaybeT (StateT (ProofState b) IO) (ProofState b)
-> MaybeT (StateT (ProofState b) IO) (Map SolverId (Solver b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MaybeT (StateT (ProofState b) IO) (ProofState b)
forall s (m :: * -> *). MonadState s m => m s
get
(SolverId -> ProofScript b ()) -> [SolverId] -> ProofScript b ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SolverId -> ProofScript b ()
forall b. SmtFormat b => SolverId -> ProofScript b ()
stop ((SolverId, Solver b) -> SolverId
forall a b. (a, b) -> a
fst ((SolverId, Solver b) -> SolverId)
-> [(SolverId, Solver b)] -> [SolverId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map SolverId (Solver b) -> [(SolverId, Solver 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 :: SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
sid [Expr]
assumptions [Expr]
props = do
SolverId -> [VarDescr] -> ProofScript b ()
forall b. SmtFormat b => SolverId -> [VarDescr] -> ProofScript b ()
declVars SolverId
sid ([VarDescr] -> ProofScript b ()) -> [VarDescr] -> ProofScript b ()
forall a b. (a -> b) -> a -> b
$ [VarDescr] -> [VarDescr]
forall a. Ord a => [a] -> [a]
nub' ([VarDescr] -> [VarDescr]) -> [VarDescr] -> [VarDescr]
forall a b. (a -> b) -> a -> b
$ [Expr] -> [VarDescr]
getVars [Expr]
assumptions [VarDescr] -> [VarDescr] -> [VarDescr]
forall a. [a] -> [a] -> [a]
++ [Expr] -> [VarDescr]
getVars [Expr]
props
SolverId -> [Expr] -> ProofScript b ()
forall b. SmtFormat b => SolverId -> [Expr] -> ProofScript b ()
assume SolverId
sid [Expr]
assumptions
SolverId -> [Expr] -> ProofScript b SatResult
forall b.
SmtFormat b =>
SolverId -> [Expr] -> ProofScript b SatResult
entailed SolverId
sid [Expr]
props
getVars :: [Expr] -> [VarDescr]
getVars :: [Expr] -> [VarDescr]
getVars = (VarDescr -> VarDescr -> Ordering) -> [VarDescr] -> [VarDescr]
forall a. (a -> a -> Ordering) -> [a] -> [a]
nubBy' (String -> String -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (String -> String -> Ordering)
-> (VarDescr -> String) -> VarDescr -> VarDescr -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` VarDescr -> String
varName) ([VarDescr] -> [VarDescr])
-> ([Expr] -> [VarDescr]) -> [Expr] -> [VarDescr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr -> [VarDescr]) -> [Expr] -> [VarDescr]
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 [VarDescr] -> [VarDescr] -> [VarDescr]
forall a. [a] -> [a] -> [a]
++ Expr -> [VarDescr]
getVars' Expr
e2 [VarDescr] -> [VarDescr] -> [VarDescr]
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 [VarDescr] -> [VarDescr] -> [VarDescr]
forall a. [a] -> [a] -> [a]
++ Expr -> [VarDescr]
getVars' Expr
e2
SVal Type
t String
seq (Fixed Integer
i) -> [String -> Type -> [Type] -> VarDescr
VarDescr (String
seq String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i) Type
t []]
SVal Type
t String
seq (Var Integer
i) -> [String -> Type -> [Type] -> VarDescr
VarDescr (String
seq String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"_n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i) Type
t []]
FunApp Type
t String
name [Expr]
args -> [String -> Type -> [Type] -> VarDescr
VarDescr String
name Type
t ((Expr -> Type) -> [Expr] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Type
typeOf [Expr]
args)]
[VarDescr] -> [VarDescr] -> [VarDescr]
forall a. [a] -> [a] -> [a]
++ (Expr -> [VarDescr]) -> [Expr] -> [VarDescr]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Expr -> [VarDescr]
getVars' [Expr]
args
unknown :: ProofScript b a
unknown :: ProofScript b a
unknown = ProofScript b a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
unknown' :: String -> ProofScript b Output
unknown' :: String -> ProofScript b Output
unknown' String
msg = Output -> ProofScript b Output
forall (m :: * -> *) a. Monad m => a -> m a
return (Output -> ProofScript b Output) -> Output -> ProofScript b Output
forall a b. (a -> b) -> a -> b
$ Status -> [String] -> Output
Output Status
P.Unknown [String
msg]
invalid :: String -> ProofScript b Output
invalid :: String -> ProofScript b Output
invalid String
msg = Output -> ProofScript b Output
forall (m :: * -> *) a. Monad m => a -> m a
return (Output -> ProofScript b Output) -> Output -> ProofScript b Output
forall a b. (a -> b) -> a -> b
$ Status -> [String] -> Output
Output Status
P.Invalid [String
msg]
sat :: String -> ProofScript b Output
sat :: String -> ProofScript b Output
sat String
msg = Output -> ProofScript b Output
forall (m :: * -> *) a. Monad m => a -> m a
return (Output -> ProofScript b Output) -> Output -> ProofScript b Output
forall a b. (a -> b) -> a -> b
$ Status -> [String] -> Output
Output Status
P.Sat [String
msg]
valid :: String -> ProofScript b Output
valid :: String -> ProofScript b Output
valid String
msg = Output -> ProofScript b Output
forall (m :: * -> *) a. Monad m => a -> m a
return (Output -> ProofScript b Output) -> Output -> ProofScript b Output
forall a b. (a -> b) -> a -> b
$ Status -> [String] -> Output
Output Status
P.Valid [String
msg]
kInduction' :: SmtFormat b => Word32 -> Word32 -> ProofState b -> [PropId] -> [PropId] -> IO Output
kInduction' :: Word32
-> Word32 -> ProofState b -> [String] -> [String] -> IO Output
kInduction' Word32
startK Word32
maxK ProofState b
s [String]
as [String]
ps = (Output -> Maybe Output -> Output
forall a. a -> Maybe a -> a
fromMaybe (Status -> [String] -> Output
Output Status
P.Unknown [String
"proof by k-induction failed"]) (Maybe Output -> Output)
-> ((Maybe Output, ProofState b) -> Maybe Output)
-> (Maybe Output, ProofState b)
-> Output
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Output, ProofState b) -> Maybe Output
forall a b. (a, b) -> a
fst)
((Maybe Output, ProofState b) -> Output)
-> IO (Maybe Output, ProofState b) -> IO Output
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProofScript b Output
-> ProofState b -> IO (Maybe Output, ProofState b)
forall b a.
ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS ([ProofScript b Output] -> ProofScript b Output
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ((Integer -> ProofScript b Output)
-> [Integer] -> [ProofScript b Output]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> ProofScript b Output
induction [(Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
startK) .. (Word32 -> Integer
forall a. Integral a => a -> Integer
toInteger Word32
maxK)]) ProofScript b Output
-> MaybeT (StateT (ProofState b) IO) () -> ProofScript b Output
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* MaybeT (StateT (ProofState b) IO) ()
forall b. SmtFormat b => ProofScript b ()
stopSolvers) ProofState b
s
where
induction :: Integer -> ProofScript b Output
induction Integer
k = do
([Expr]
modelInit, [Expr]
modelRec, [Expr]
toCheck, Bool
inductive) <- [String]
-> [String] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
forall b.
[String]
-> [String] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
getModels [String]
as [String]
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 (Integer -> SeqIndex
forall a. Integral a => a -> SeqIndex
_n_plus Integer
i) Expr
m | Expr
m <- [Expr]
modelRec, Integer
i <- [Integer
0 .. Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1]]
[Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
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 (Integer -> SeqIndex
forall a. Integral a => a -> SeqIndex
_n_plus (Integer -> SeqIndex) -> Integer -> SeqIndex
forall a b. (a -> b) -> a -> b
$ Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1) Expr
m | Expr
m <- [Expr]
toCheck]
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
forall b.
SmtFormat b =>
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
Base ([Expr]
modelInit [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
base) [Expr]
baseInv ProofScript b SatResult
-> (SatResult -> ProofScript b Output) -> ProofScript b Output
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
SatResult
Sat -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
invalid (String -> ProofScript b Output) -> String -> ProofScript b Output
forall a b. (a -> b) -> a -> b
$ String
"base case failed for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
proofKind Integer
k
SatResult
Unknown -> ProofScript b Output
forall b a. ProofScript b a
unknown
SatResult
Unsat ->
if Bool -> Bool
not Bool
inductive then String -> ProofScript b Output
forall b. String -> ProofScript b Output
valid (String
"proved without induction")
else SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
forall b.
SmtFormat b =>
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
Step [Expr]
step [Expr]
stepInv ProofScript b SatResult
-> (SatResult -> ProofScript b Output) -> ProofScript b Output
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
SatResult
Sat -> ProofScript b Output
forall b a. ProofScript b a
unknown
SatResult
Unknown -> ProofScript b Output
forall b a. ProofScript b a
unknown
SatResult
Unsat -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
valid (String -> ProofScript b Output) -> String -> ProofScript b Output
forall a b. (a -> b) -> a -> b
$ String
"proved with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
proofKind Integer
k
onlySat' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output
onlySat' :: ProofState b -> [String] -> [String] -> IO Output
onlySat' ProofState b
s [String]
as [String]
ps = (Maybe Output -> Output
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Output -> Output)
-> ((Maybe Output, ProofState b) -> Maybe Output)
-> (Maybe Output, ProofState b)
-> Output
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Output, ProofState b) -> Maybe Output
forall a b. (a, b) -> a
fst) ((Maybe Output, ProofState b) -> Output)
-> IO (Maybe Output, ProofState b) -> IO Output
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProofScript b Output
-> ProofState b -> IO (Maybe Output, ProofState b)
forall b a.
ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS (ProofScript b Output
script ProofScript b Output
-> MaybeT (StateT (ProofState b) IO) () -> ProofScript b Output
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* MaybeT (StateT (ProofState b) IO) ()
forall b. SmtFormat b => ProofScript b ()
stopSolvers) ProofState b
s
where
script :: ProofScript b Output
script = do
([Expr]
modelInit, [Expr]
modelRec, [Expr]
toCheck, Bool
inductive) <- [String]
-> [String] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
forall b.
[String]
-> [String] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
getModels [String]
as [String]
ps
let base :: [Expr]
base = (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
0)) [Expr]
modelRec
baseInv :: [Expr]
baseInv = (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
0)) [Expr]
toCheck
if Bool
inductive
then String -> ProofScript b Output
forall b. String -> ProofScript b Output
unknown' String
"proposition requires induction to prove."
else SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
forall b.
SmtFormat b =>
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
Base ([Expr]
modelInit [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
base) ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Op1 -> Expr -> Expr
Op1 Type
Bool Op1
Not) [Expr]
baseInv) ProofScript b SatResult
-> (SatResult -> ProofScript b Output) -> ProofScript b Output
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
SatResult
Unsat -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
invalid String
"prop not satisfiable"
SatResult
Unknown -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
unknown' String
"failed to find a satisfying model"
SatResult
Sat -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
sat String
"prop is satisfiable"
onlyValidity' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output
onlyValidity' :: ProofState b -> [String] -> [String] -> IO Output
onlyValidity' ProofState b
s [String]
as [String]
ps = (Maybe Output -> Output
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Output -> Output)
-> ((Maybe Output, ProofState b) -> Maybe Output)
-> (Maybe Output, ProofState b)
-> Output
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Output, ProofState b) -> Maybe Output
forall a b. (a, b) -> a
fst) ((Maybe Output, ProofState b) -> Output)
-> IO (Maybe Output, ProofState b) -> IO Output
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProofScript b Output
-> ProofState b -> IO (Maybe Output, ProofState b)
forall b a.
ProofScript b a -> ProofState b -> IO (Maybe a, ProofState b)
runPS (ProofScript b Output
script ProofScript b Output
-> MaybeT (StateT (ProofState b) IO) () -> ProofScript b Output
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* MaybeT (StateT (ProofState b) IO) ()
forall b. SmtFormat b => ProofScript b ()
stopSolvers) ProofState b
s
where
script :: ProofScript b Output
script = do
([Expr]
modelInit, [Expr]
modelRec, [Expr]
toCheck, Bool
inductive) <- [String]
-> [String] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
forall b.
[String]
-> [String] -> ProofScript b ([Expr], [Expr], [Expr], Bool)
getModels [String]
as [String]
ps
let base :: [Expr]
base = (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
0)) [Expr]
modelRec
baseInv :: [Expr]
baseInv = (Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map (SeqIndex -> Expr -> Expr
evalAt (Integer -> SeqIndex
Fixed Integer
0)) [Expr]
toCheck
if Bool
inductive
then String -> ProofScript b Output
forall b. String -> ProofScript b Output
unknown' String
"proposition requires induction to prove."
else SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
forall b.
SmtFormat b =>
SolverId -> [Expr] -> [Expr] -> ProofScript b SatResult
entailment SolverId
Base ([Expr]
modelInit [Expr] -> [Expr] -> [Expr]
forall a. [a] -> [a] -> [a]
++ [Expr]
base) [Expr]
baseInv ProofScript b SatResult
-> (SatResult -> ProofScript b Output) -> ProofScript b Output
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
SatResult
Unsat -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
valid String
"proof by SMT solver"
SatResult
Unknown -> ProofScript b Output
forall b a. ProofScript b a
unknown
SatResult
Sat -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
invalid String
"SMT solver found a counter-example."
selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
selectProps :: [String] -> Map String ([Expr], Expr) -> ([Expr], [Expr])
selectProps [String]
propIds Map String ([Expr], Expr)
properties =
(([[Expr]], [Expr]) -> ([Expr], [Expr])
forall (t :: * -> *) a b. Foldable t => (t [a], b) -> ([a], b)
squash (([[Expr]], [Expr]) -> ([Expr], [Expr]))
-> ([([Expr], Expr)] -> ([[Expr]], [Expr]))
-> [([Expr], Expr)]
-> ([Expr], [Expr])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [([Expr], Expr)] -> ([[Expr]], [Expr])
forall a b. [(a, b)] -> ([a], [b])
unzip) [([Expr]
as, Expr
p) | (String
id, ([Expr]
as, Expr
p)) <- Map String ([Expr], Expr) -> [(String, ([Expr], Expr))]
forall k a. Map k a -> [(k, a)]
Map.toList Map String ([Expr], Expr)
properties, String
id String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
propIds]
where squash :: (t [a], b) -> ([a], b)
squash (t [a]
a, b
b) = (t [a] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat t [a]
a, b
b)