{-# LANGUAGE LambdaCase #-}

{- |
This module provides MTL-Style-classes for building SMT-problems.

The following three classes form the core of this module:

1. 'MonadSMT' for plain SMT-problems. Create variables using 'var' and assert formulas via 'assert'.

2. 'MonadIncrSMT' for plain SMT-problems with addtional access to the external solvers incremental stack and it's operations.

3. 'MonadOMT' for SMT-problems with optimization. Optimize via 'minimize' and 'maximize' and softly assert formulas via 'assertSoft'.
-}
module Language.Hasmtlib.Type.MonadSMT
(
  -- * MonadSMT
  MonadSMT(..)
, var, smtvar
, constant, assertMaybe, quantify

  -- * MonadIncrSMT
, MonadIncrSMT(..)
, solve

  -- * MonadOMT
, MonadOMT(..)
, assertSoftWeighted
)
where

import Language.Hasmtlib.Type.Expr
import Language.Hasmtlib.Type.Value
import Language.Hasmtlib.Type.Option
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Codec
import Data.Proxy
import Control.Lens
import Control.Monad.State

-- | A 'MonadState' that holds an SMT-Problem.
--
-- ==== __Example__
--
-- @
-- problem :: MonadSMT s m => StateT s m (Expr IntSort)
-- problem = do
--   setLogic \"QF_LIA\"
--   x <- var @IntSort
--   assert $ x + 2 === x * 2
--   return x
-- @
class MonadState s m => MonadSMT s m where
  -- | Construct a variable.
  --   This is mainly intended for internal use.
  --   In the API use 'var'' instead.
  smtvar' :: forall t. KnownSMTSort t => Proxy t -> m (SMTVar t)

  -- | Construct a variable as expression.
  --
  -- ==== __Example__
  --
  -- @
  -- x <- var' (Proxy @RealType)
  -- @
  var' :: forall t. KnownSMTSort t => Proxy t -> m (Expr t)

  -- | Assert a boolean expression.
  --
  -- ==== __Example__
  --
  -- @
  -- x <- var @IntType
  -- assert $ x - 27 === 42
  -- @
  assert :: Expr BoolSort -> m ()

  -- | Set an SMT-Solver-Option.
  --
  -- ==== __Example__
  --
  -- @
  -- setOption $ Incremental True
  -- @
  setOption :: SMTOption -> m ()

  -- | Set the logic for the SMT-Solver to use.
  --
  -- ==== __Example__
  --
  -- @
  -- setLogic \"QF_LRA\"
  -- @
  setLogic :: String -> m ()

-- | Wrapper for 'var'' which hides the 'Proxy'.
--
-- ==== __Example__
--
-- @
-- x <- var @BoolSort
-- @
var :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (Expr t)
var :: forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m) =>
m (Expr t)
var = Proxy t -> m (Expr t)
forall s (m :: * -> *) (t :: SMTSort).
(MonadSMT s m, KnownSMTSort t) =>
Proxy t -> m (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (Expr t)
var' (forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @t)
{-# INLINE var #-}

-- | Wrapper for 'smtvar'' which hides the 'Proxy'.
--   This is mainly intended for internal use.
--   In the API use 'var' instead.
smtvar :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (SMTVar t)
smtvar :: forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m) =>
m (SMTVar t)
smtvar = Proxy t -> m (SMTVar t)
forall s (m :: * -> *) (t :: SMTSort).
(MonadSMT s m, KnownSMTSort t) =>
Proxy t -> m (SMTVar t)
forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (SMTVar t)
smtvar' (forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @t)
{-# INLINE smtvar #-}

-- | Create a constant.
--
-- ==== __Examples__
--
--   >>> constant True
--       Constant (BoolValue True)
--
--   >>> constant (10 :: Integer)
--       Constant (IntValue 10)
--
--   >>> constant @RealSort 5
--       Constant (RealValue 5.0)
--
--   >>> constant @(BvSort Unsigned 8) 14
--       Constant (BvValue 00001110)
constant :: KnownSMTSort t => HaskellType t -> Expr t
constant :: forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Expr t
constant = Value t -> Expr t
forall (t :: SMTSort). Value t -> Expr t
Constant (Value t -> Expr t)
-> (HaskellType t -> Value t) -> HaskellType t -> Expr t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue
{-# INLINE constant #-}

-- | Maybe assert a boolean expression.
--
--   Asserts given expression if 'Maybe' is a 'Just'.
--   Does nothing otherwise.
assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()
assertMaybe :: forall s (m :: * -> *).
MonadSMT s m =>
Maybe (Expr 'BoolSort) -> m ()
assertMaybe Maybe (Expr 'BoolSort)
Nothing = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertMaybe (Just Expr 'BoolSort
expr) = Expr 'BoolSort -> m ()
forall s (m :: * -> *). MonadSMT s m => Expr 'BoolSort -> m ()
assert Expr 'BoolSort
expr

-- | Assign quantified variables to all quantified subexpressions of an expression.
--
--   Quantifies bottom-up.
--
--   This is intended for internal use.
--   Usually before rendering an assert.
quantify :: MonadSMT s m => KnownSMTSort t => Expr t -> m (Expr t)
quantify :: forall s (m :: * -> *) (t :: SMTSort).
(MonadSMT s m, KnownSMTSort t) =>
Expr t -> m (Expr t)
quantify = (Expr t -> m (Expr t)) -> Expr t -> m (Expr t)
forall (m :: * -> *) a.
(Monad m, Plated a) =>
(a -> m a) -> a -> m a
transformM (
  \case (ForAll Maybe (SMTVar t1)
_ Expr t1 -> Expr 'BoolSort
f) -> do
          SMTVar t1
qVar <- m (SMTVar t1)
forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m) =>
m (SMTVar t)
smtvar
          Expr 'BoolSort
qBody <- Expr 'BoolSort -> m (Expr 'BoolSort)
forall s (m :: * -> *) (t :: SMTSort).
(MonadSMT s m, KnownSMTSort t) =>
Expr t -> m (Expr t)
quantify (Expr 'BoolSort -> m (Expr 'BoolSort))
-> Expr 'BoolSort -> m (Expr 'BoolSort)
forall a b. (a -> b) -> a -> b
$ Expr t1 -> Expr 'BoolSort
f (Expr t1 -> Expr 'BoolSort) -> Expr t1 -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ SMTVar t1 -> Expr t1
forall (t :: SMTSort). KnownSMTSort t => SMTVar t -> Expr t
Var SMTVar t1
qVar
          Expr 'BoolSort -> m (Expr 'BoolSort)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr 'BoolSort -> m (Expr 'BoolSort))
-> Expr 'BoolSort -> m (Expr 'BoolSort)
forall a b. (a -> b) -> a -> b
$ Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
ForAll (SMTVar t1 -> Maybe (SMTVar t1)
forall a. a -> Maybe a
Just SMTVar t1
qVar) (Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort
forall a b. a -> b -> a
const Expr 'BoolSort
qBody)
        (Exists Maybe (SMTVar t1)
_ Expr t1 -> Expr 'BoolSort
f) -> do
          SMTVar t1
qVar <- m (SMTVar t1)
forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m) =>
m (SMTVar t)
smtvar
          Expr 'BoolSort
qBody <- Expr 'BoolSort -> m (Expr 'BoolSort)
forall s (m :: * -> *) (t :: SMTSort).
(MonadSMT s m, KnownSMTSort t) =>
Expr t -> m (Expr t)
quantify (Expr 'BoolSort -> m (Expr 'BoolSort))
-> Expr 'BoolSort -> m (Expr 'BoolSort)
forall a b. (a -> b) -> a -> b
$ Expr t1 -> Expr 'BoolSort
f (Expr t1 -> Expr 'BoolSort) -> Expr t1 -> Expr 'BoolSort
forall a b. (a -> b) -> a -> b
$ SMTVar t1 -> Expr t1
forall (t :: SMTSort). KnownSMTSort t => SMTVar t -> Expr t
Var SMTVar t1
qVar
          Expr 'BoolSort -> m (Expr 'BoolSort)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr 'BoolSort -> m (Expr 'BoolSort))
-> Expr 'BoolSort -> m (Expr 'BoolSort)
forall a b. (a -> b) -> a -> b
$ Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
forall (t1 :: SMTSort).
KnownSMTSort t1 =>
Maybe (SMTVar t1) -> (Expr t1 -> Expr 'BoolSort) -> Expr 'BoolSort
Exists (SMTVar t1 -> Maybe (SMTVar t1)
forall a. a -> Maybe a
Just SMTVar t1
qVar) (Expr 'BoolSort -> Expr t1 -> Expr 'BoolSort
forall a b. a -> b -> a
const Expr 'BoolSort
qBody)
        Expr t
expr -> Expr t -> m (Expr t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr t
expr
  )

-- | A 'MonadSMT' that addtionally allows incremental solving with access to a solvers incremental stack.
--
-- Some solvers require to have 'SMTOption' 'Incremental' set first.
--
-- ==== __Example__
--
-- @
-- problem :: MonadIncrSMT s m => StateT s m ()
-- problem = do
--   setOption $ Incremental True
--   setLogic \"QF_LIA\"
--   x <- var @IntSort
--   push
--   assert $ x + 2 === x * 2
--   res <- checkSat
--   case res of
--     Sat -> do
--       x' <- getValue x
--       ...
--     _ -> pop ...
--   return ()
-- @
class MonadSMT s m => MonadIncrSMT s m where
  -- | Push a new context (one) to the solvers context-stack.
  push :: m ()

  -- | Pop the solvers context-stack by one.
  pop :: m ()

  -- | Run @check-sat@ on the current problem.
  checkSat :: m Result

  -- | Run get-model on the current problem.
  --   This can be used to decode temporary models within the SMT-Problem.
  --
  -- ==== __Example__
  --
  -- @
  -- x <- var @RealSort
  -- y <- var
  -- assert $ x >? y && y <? (-1)
  -- res <- checkSat
  -- case res of
  --   Sat -> do
  --     model <- getModel
  --     liftIO $ print $ decode model x
  --   r -> print $ show r <> ": Cannot get model."
  -- @
  getModel :: m Solution

  -- | Evaluate any expressions value in the solvers model.
  --   Requires a 'Sat' or 'Unknown' check-sat response beforehand.
  --
  -- ==== __Example__
  --
  -- @
  -- x <- var @RealSort
  -- assert $ x >? 10
  -- res <- checkSat
  -- case res of
  --   Unsat -> print "Unsat. Cannot get value for 'x'."
  --   r     -> do
  --     x' <- getValue x
  --     liftIO $ print $ show r ++ ": x = " ++ show x'
  -- @
  getValue :: KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))

-- | First run 'checkSat' and then 'getModel' on the current problem.
--
-- ==== __Example__
--
-- @
-- x <- var @BoolSort
-- assert $ x `xor` false
-- (res, sol) <- solve
-- case res of
--   Sat -> do
--     liftIO $ print $ decode sol x
--   r -> print r
-- @
solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)
solve :: forall s (m :: * -> *).
(MonadIncrSMT s m, MonadIO m) =>
m (Result, Solution)
solve = do
  Result
res <- m Result
forall s (m :: * -> *). MonadIncrSMT s m => m Result
checkSat
  case Result
res of
    Result
Sat -> do
      Solution
sol <- m Solution
forall s (m :: * -> *). MonadIncrSMT s m => m Solution
getModel
      (Result, Solution) -> m (Result, Solution)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
Sat, Solution
sol)
    Result
r -> (Result, Solution) -> m (Result, Solution)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
r, Solution
forall a. Monoid a => a
mempty)

-- | A 'MonadSMT' that addtionally allows optimization targets.
--
-- ==== __Example__
--
-- @
-- problem :: MonadOMT s m => StateT s m (Expr (BvSort Unsigned 8))
-- problem = do
--   setLogic \"QF_BV\"
--   x <- var @(BvSort Unsigned 8)
--   assertSoftWeighted (x <? maxBound) 2.0
--   maximize x
--   return x
-- @
class MonadSMT s m => MonadOMT s m where
  -- | Minimizes a numerical expression within the OMT-Problem.
  --
  -- ==== __Example__
  --
  -- @
  -- x <- var @IntSort
  -- assert $ x >? -2
  -- minimize x
  -- @
  --
  -- will give @x := -1@ as solution.
  minimize :: (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()

  -- | Maximizes a numerical expression within the OMT-Problem.
  --
  -- ==== __Example__
  --
  -- @
  -- x <- var @(BvSort Signed 4)
  -- assert $ x <? 2
  -- maximize x
  -- @
  --
  -- will give @x := 0001@ as solution.
  maximize :: (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()

  -- | Softly asserts a boolean expression.
  --
  --   May take a weight and an identifier for grouping.
  --
  -- ==== __Example__
  --
  -- @
  -- x <- var @BoolSort
  -- assertSoft x (Just 0.5) (Just "myId")
  -- @
  assertSoft :: Expr BoolSort -> Maybe Double -> Maybe String -> m ()

-- | Like 'assertSoft' but forces a weight and omits the group-id.
assertSoftWeighted :: MonadOMT s m => Expr BoolSort -> Double -> m ()
assertSoftWeighted :: forall s (m :: * -> *).
MonadOMT s m =>
Expr 'BoolSort -> Double -> m ()
assertSoftWeighted Expr 'BoolSort
expr Double
w = Expr 'BoolSort -> Maybe Double -> Maybe String -> m ()
forall s (m :: * -> *).
MonadOMT s m =>
Expr 'BoolSort -> Maybe Double -> Maybe String -> m ()
assertSoft Expr 'BoolSort
expr (Double -> Maybe Double
forall a. a -> Maybe a
Just Double
w) Maybe String
forall a. Maybe a
Nothing