--------------------------------------------------------------------------------

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

module Copilot.Theorem.Prover.SMT
  ( module Data.Default
  , Options (..)
  , induction, kInduction, onlySat, onlyValidity
  , yices, dReal, altErgo, metit, z3, cvc4, mathsat
  , Backend, SmtFormat
  , SmtLib, Tptp
  ) 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

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

  -- If `debug` is set to `True`, the SMTLib/TPTP queries produced by the
  -- prover are displayed in the standard output.
  , 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 ()
  }

-------------------------------------------------------------------------------

-- | Backends

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
  }

-- The argument is the path to the "tptp" subdirectory of the metitarski
-- install location.
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
  }

-------------------------------------------------------------------------------

-- | 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 :: 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)

--------------------------------------------------------------------------------