content: {-# 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 = var' (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 = smtvar' (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 = Constant . 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 Nothing = return ()
  assertMaybe (Just expr) = assert 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 = transformM (
    \case (ForAll _ f) -> do
            qVar <- smtvar
            qBody <- quantify $ f $ Var qVar
            return $ ForAll (Just qVar) (const qBody)
          (Exists _ f) -> do
            qVar <- smtvar
            qBody <- quantify $ f $ Var qVar
            return $ Exists (Just qVar) (const qBody)
          expr -> return 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 = do
    res <- checkSat
    case res of
      Sat -> do
        sol <- getModel
        return (Sat, sol)
      r -> return (r, 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 expr w = assertSoft expr (Just w) Nothing
  