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

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

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

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

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

    -- * Auxiliary
  , module Data.Default
  ) where

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

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

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

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

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

import System.IO (hClose)

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

-- * Tactics

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

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

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

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

-- | Tactic to find only a proof of satisfiability.
onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential
onlySat :: Options -> Backend a -> Proof Existential
onlySat opts :: Options
opts backend :: 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  = "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 ()
  }

-- | Tactic to find only a proof of validity.
onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal
onlyValidity :: Options -> Backend a -> Proof Universal
onlyValidity opts :: Options
opts backend :: 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  = "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 ()
  }

-- | Tactic to find a proof by standard 1-induction.
--
-- The values for @startK@ and @maxK@ in the options are ignored.
induction :: SmtFormat a => Options -> Backend a -> Proof Universal
induction :: Options -> Backend a -> Proof Universal
induction opts :: Options
opts backend :: 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  = "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' 0 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 ()
  }

-- | Tactic to find a proof by k-induction.
kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
kInduction :: Options -> Backend a -> Proof Universal
kInduction opts :: Options
opts backend :: 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  = "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

-- | Backend to the Yices 2 SMT solver.
--
-- It enables non-linear arithmetic (@QF_NRA@), which means MCSat will be used.
--
-- The command @yices-smt2@ must be in the user's @PATH@.
yices :: Backend SmtLib
yices :: Backend SmtLib
yices = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
  { name :: String
name            = "Yices"
  , cmd :: String
cmd             = "yices-smt2"
  , cmdOpts :: [String]
cmdOpts         = ["--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           = "QF_NRA"
  , interpret :: String -> Maybe SatResult
interpret       = String -> Maybe SatResult
SMTLib.interpret
  }

-- | Backend to the cvc4 SMT solver.
--
-- It enables support for uninterpreted functions and mixed nonlinear
-- arithmetic (@QF_NIRA@).
--
-- The command @cvc4@ must be in the user's @PATH@.
cvc4 :: Backend SmtLib
cvc4 :: Backend SmtLib
cvc4 = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
  { name :: String
name            = "CVC4"
  , cmd :: String
cmd             = "cvc4"
  , cmdOpts :: [String]
cmdOpts         = ["--incremental", "--lang=smt2", "--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           = "QF_UFNIRA"
  , interpret :: String -> Maybe SatResult
interpret       = String -> Maybe SatResult
SMTLib.interpret
  }

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

-- | Backend to the Z3 theorem prover.
--
-- The command @z3@ must be in the user's @PATH@.
z3 :: Backend SmtLib
z3 :: Backend SmtLib
z3 = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
  { name :: String
name            = "Z3"
  , cmd :: String
cmd             = "z3"
  , cmdOpts :: [String]
cmdOpts         = ["-smt2", "-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           = ""
  , interpret :: String -> Maybe SatResult
interpret       = String -> Maybe SatResult
SMTLib.interpret
  }

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

-- | Backend to the Mathsat SMT solver.
--
-- It enables non-linear arithmetic (@QF_NRA@).
--
-- The command @mathsat@ must be in the user's @PATH@.
mathsat :: Backend SmtLib
mathsat :: Backend SmtLib
mathsat = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
  { name :: String
name            = "MathSAT"
  , cmd :: String
cmd             = "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           = "QF_NRA"
  , interpret :: String -> Maybe SatResult
interpret       = String -> Maybe SatResult
SMTLib.interpret
  }

-- | Backend to the MetiTaski theorem prover.
--
-- The command @metit@ must be in the user's @PATH@.
--
-- The argument string is the path to the @tptp@ subdirectory of the metitarski
-- install location.
metit :: String -> Backend Tptp
metit :: String -> Backend Tptp
metit installDir :: String
installDir = Backend :: forall a.
String
-> String
-> [String]
-> (Handle -> IO ())
-> Bool
-> String
-> (String -> Maybe SatResult)
-> Backend a
Backend
  { name :: String
name            = "MetiTarski"
  , cmd :: String
cmd             = "metit"
  , cmdOpts :: [String]
cmdOpts         =
      [ "--time", "5"
      , "--autoInclude"
      , "--tptp", String
installDir
      , "/dev/stdin"
      ]
  , inputTerminator :: Handle -> IO ()
inputTerminator = Handle -> IO ()
hClose
  , incremental :: Bool
incremental     = Bool
False
  , logic :: String
logic           = ""
  , 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 ps :: 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 assumptionIds :: [String]
assumptionIds toCheckIds :: [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 (as :: [Expr]
as, as' :: [Expr]
as')       = [String] -> Map String ([Expr], Expr) -> ([Expr], [Expr])
selectProps [String]
assumptionIds Map String ([Expr], Expr)
properties
      (as'' :: [Expr]
as'', toCheck :: [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 sid :: 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
    Nothing -> SolverId -> ProofScript b (Solver b)
forall b. SmtFormat b => SolverId -> ProofScript b (Solver b)
startNewSolver SolverId
sid
    Just solver :: 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 sid :: SolverId
sid solver :: 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
$ \s :: 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 sid :: 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
$ \s :: 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 sid :: 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 sid :: SolverId
sid vs :: [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 sid :: SolverId
sid cs :: [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 sid :: SolverId
sid cs :: [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 sid :: 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 0 = "induction"
proofKind k :: Integer
k = "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]
++ ")"

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 sid :: SolverId
sid assumptions :: [Expr]
assumptions props :: [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 _             -> []
          ConstI _ _           -> []
          ConstR _             -> []
          Ite _ e1 :: Expr
e1 e2 :: Expr
e2 e3 :: 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 _ _ e :: Expr
e            -> Expr -> [VarDescr]
getVars' Expr
e
          Op2 _ _ e1 :: Expr
e1 e2 :: Expr
e2        -> Expr -> [VarDescr]
getVars' Expr
e1 [VarDescr] -> [VarDescr] -> [VarDescr]
forall a. [a] -> [a] -> [a]
++ Expr -> [VarDescr]
getVars' Expr
e2
          SVal t :: Type
t seq :: String
seq (Fixed i :: Integer
i) -> [String -> Type -> [Type] -> VarDescr
VarDescr (String
seq String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i) Type
t []]
          SVal t :: Type
t seq :: String
seq (Var i :: Integer
i)   -> [String -> Type -> [Type] -> VarDescr
VarDescr (String
seq String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
i) Type
t []]
          FunApp t :: Type
t name :: String
name args :: [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' msg :: 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 msg :: 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 msg :: 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 msg :: 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' startK :: Word32
startK maxK :: Word32
maxK s :: ProofState b
s as :: [String]
as ps :: [String]
ps = (Output -> Maybe Output -> Output
forall a. a -> Maybe a -> a
fromMaybe (Status -> [String] -> Output
Output Status
P.Unknown ["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 k :: Integer
k = do
      (modelInit :: [Expr]
modelInit, modelRec :: [Expr]
modelRec, toCheck :: [Expr]
toCheck, inductive :: 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 <- [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 <- [0 .. Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 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 <- [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
+ 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
        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
$ "base case failed for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
proofKind Integer
k
        Unknown -> ProofScript b Output
forall b a. ProofScript b a
unknown
        Unsat   ->
          if Bool -> Bool
not Bool
inductive then String -> ProofScript b Output
forall b. String -> ProofScript b Output
valid ("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
            Sat     -> ProofScript b Output
forall b a. ProofScript b a
unknown
            Unknown -> ProofScript b Output
forall b a. ProofScript b a
unknown
            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
$ "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' s :: ProofState b
s as :: [String]
as ps :: [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
      (modelInit :: [Expr]
modelInit, modelRec :: [Expr]
modelRec, toCheck :: [Expr]
toCheck, inductive :: 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 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 0)) [Expr]
toCheck

      if Bool
inductive
        then String -> ProofScript b Output
forall b. String -> ProofScript b Output
unknown' "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
          Unsat   -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
invalid "prop not satisfiable"
          Unknown -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
unknown' "failed to find a satisfying model"
          Sat     -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
sat "prop is satisfiable"

onlyValidity' :: SmtFormat b => ProofState b -> [PropId] -> [PropId] -> IO Output
onlyValidity' :: ProofState b -> [String] -> [String] -> IO Output
onlyValidity' s :: ProofState b
s as :: [String]
as ps :: [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
      (modelInit :: [Expr]
modelInit, modelRec :: [Expr]
modelRec, toCheck :: [Expr]
toCheck, inductive :: 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 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 0)) [Expr]
toCheck

      if Bool
inductive
        then String -> ProofScript b Output
forall b. String -> ProofScript b Output
unknown' "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
          Unsat   -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
valid "proof by SMT solver"
          Unknown -> ProofScript b Output
forall b a. ProofScript b a
unknown
          Sat     -> String -> ProofScript b Output
forall b. String -> ProofScript b Output
invalid "SMT solver found a counter-example."

selectProps :: [PropId] -> Map PropId ([Expr], Expr) -> ([Expr], [Expr])
selectProps :: [String] -> Map String ([Expr], Expr) -> ([Expr], [Expr])
selectProps propIds :: [String]
propIds properties :: 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) | (id :: String
id, (as :: [Expr]
as, p :: 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 (a :: t [a]
a, b :: b
b) = (t [a] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat t [a]
a, b
b)

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