{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

{- |
This module provides a concrete implementation for 'MonadSMT' with it's state 'SMT'.
-}
module Language.Hasmtlib.Type.SMT
(
  -- * Type
  SMT(..)

  -- * Lens
, lastVarId, vars, formulas
, mlogic, options
, sharingMode, Language.Hasmtlib.Type.SMT.stableMap
)
where

import Language.Hasmtlib.Internal.Sharing
import Language.Hasmtlib.Type.MonadSMT
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Option
import Language.Hasmtlib.Type.Expr
import Data.Some.Constraint
import Data.List (isPrefixOf)
import Data.Default
import Data.Coerce
import Data.Sequence hiding ((|>), filter)
import Data.HashMap.Lazy (HashMap)
import Control.Monad.State
import Control.Lens hiding (List)
import System.Mem.StableName

-- | The state of the SMT-problem.
data SMT = SMT
  { SMT -> Int
_lastVarId :: {-# UNPACK #-} !Int                                 -- ^ Last Id assigned to a new var
  , SMT -> Seq (SomeKnownSMTSort SMTVar)
_vars      :: !(Seq (SomeKnownSMTSort SMTVar))                    -- ^ All constructed variables
  , SMT -> Seq (Expr 'BoolSort)
_formulas  :: !(Seq (Expr BoolSort))                              -- ^ All asserted formulas
  , SMT -> Maybe String
_mlogic    :: Maybe String                                        -- ^ Logic for the SMT-Solver
  , SMT -> [SMTOption]
_options   :: [SMTOption]                                         -- ^ All manually configured SMT-Solver-Options
  , SMT -> SharingMode
_sharingMode :: !SharingMode                                       -- ^ How to share common expressions
  , SMT -> HashMap (StableName ()) (SomeKnownSMTSort Expr)
_stableMap :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))  -- ^ Mapping between a 'StableName' and it's 'Expr' we may share
  }
$(makeLenses ''SMT)

instance Default SMT where
  def :: SMT
def = Int
-> Seq (SomeKnownSMTSort SMTVar)
-> Seq (Expr 'BoolSort)
-> Maybe String
-> [SMTOption]
-> SharingMode
-> HashMap (StableName ()) (SomeKnownSMTSort Expr)
-> SMT
SMT Int
0 Seq (SomeKnownSMTSort SMTVar)
forall a. Monoid a => a
mempty Seq (Expr 'BoolSort)
forall a. Monoid a => a
mempty Maybe String
forall a. Monoid a => a
mempty [Bool -> SMTOption
ProduceModels Bool
True] SharingMode
forall a. Default a => a
def HashMap (StableName ()) (SomeKnownSMTSort Expr)
forall a. Monoid a => a
mempty

instance Sharing SMT where
  type SharingMonad SMT = Monad
  stableMap :: Lens' SMT (HashMap (StableName ()) (SomeKnownSMTSort Expr))
stableMap = (HashMap (StableName ()) (SomeKnownSMTSort Expr)
 -> f (HashMap (StableName ()) (SomeKnownSMTSort Expr)))
-> SMT -> f SMT
Lens' SMT (HashMap (StableName ()) (SomeKnownSMTSort Expr))
Language.Hasmtlib.Type.SMT.stableMap
  assertSharedNode :: forall (m :: * -> *).
(MonadState SMT m, SharingMonad SMT m) =>
StableName () -> Expr 'BoolSort -> m ()
assertSharedNode StableName ()
_ Expr 'BoolSort
expr = ASetter SMT SMT (Seq (Expr 'BoolSort)) (Seq (Expr 'BoolSort))
-> (Seq (Expr 'BoolSort) -> Seq (Expr 'BoolSort)) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying ASetter SMT SMT (Seq (Expr 'BoolSort)) (Seq (Expr 'BoolSort))
Lens' SMT (Seq (Expr 'BoolSort))
formulas (Seq (Expr 'BoolSort) -> Expr 'BoolSort -> Seq (Expr 'BoolSort)
forall s a. Snoc s s a a => s -> a -> s
|> Expr 'BoolSort
expr)
  setSharingMode :: forall (m :: * -> *). MonadState SMT m => SharingMode -> m ()
setSharingMode SharingMode
sm = (SharingMode -> Identity SharingMode) -> SMT -> Identity SMT
Lens' SMT SharingMode
sharingMode ((SharingMode -> Identity SharingMode) -> SMT -> Identity SMT)
-> SharingMode -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= SharingMode
sm

instance MonadState SMT m => MonadSMT SMT m where
  smtvar' :: forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (SMTVar t)
smtvar' Proxy t
_ = (Int -> SMTVar t) -> m Int -> m (SMTVar t)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> SMTVar t
forall a b. Coercible a b => a -> b
coerce (m Int -> m (SMTVar t)) -> m Int -> m (SMTVar t)
forall a b. (a -> b) -> a -> b
$ (Int -> (Int, Int)) -> SMT -> (Int, SMT)
Lens' SMT Int
lastVarId ((Int -> (Int, Int)) -> SMT -> (Int, SMT)) -> Int -> m Int
forall s (m :: * -> *) a.
(MonadState s m, Num a) =>
LensLike' ((,) a) s a -> a -> m a
<+= Int
1
  {-# INLINE smtvar' #-}

  var' :: forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (Expr t)
var' Proxy t
p = do
    SMTVar t
newVar <- 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' Proxy t
p
    (Seq (SomeKnownSMTSort SMTVar)
 -> Identity (Seq (SomeKnownSMTSort SMTVar)))
-> SMT -> Identity SMT
Lens' SMT (Seq (SomeKnownSMTSort SMTVar))
vars ((Seq (SomeKnownSMTSort SMTVar)
  -> Identity (Seq (SomeKnownSMTSort SMTVar)))
 -> SMT -> Identity SMT)
-> (Seq (SomeKnownSMTSort SMTVar) -> Seq (SomeKnownSMTSort SMTVar))
-> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (Seq (SomeKnownSMTSort SMTVar)
-> SomeKnownSMTSort SMTVar -> Seq (SomeKnownSMTSort SMTVar)
forall s a. Snoc s s a a => s -> a -> s
|> SMTVar t -> SomeKnownSMTSort SMTVar
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 SMTVar t
newVar)
    Expr t -> m (Expr t)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t -> m (Expr t)) -> Expr t -> m (Expr t)
forall a b. (a -> b) -> a -> b
$ SMTVar t -> Expr t
forall (t :: SMTSort). KnownSMTSort t => SMTVar t -> Expr t
Var SMTVar t
newVar
  {-# INLINEABLE var' #-}

  assert :: Expr 'BoolSort -> m ()
assert Expr 'BoolSort
expr = do
    SMT
smt <- m SMT
forall s (m :: * -> *). MonadState s m => m s
get
    Expr 'BoolSort
sExpr <- SharingMode -> Expr 'BoolSort -> m (Expr 'BoolSort)
forall (t :: SMTSort) s (m :: * -> *).
(KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) =>
SharingMode -> Expr t -> m (Expr t)
runSharing (SMT
smtSMT -> Getting SharingMode SMT SharingMode -> SharingMode
forall s a. s -> Getting a s a -> a
^.Getting SharingMode SMT SharingMode
Lens' SMT SharingMode
sharingMode) Expr 'BoolSort
expr
    Expr 'BoolSort
qExpr <- case SMT
smtSMT -> Getting (Maybe String) SMT (Maybe String) -> Maybe String
forall s a. s -> Getting a s a -> a
^.Getting (Maybe String) SMT (Maybe String)
Lens' SMT (Maybe String)
mlogic of
      Maybe String
Nothing    -> Expr 'BoolSort -> m (Expr 'BoolSort)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr 'BoolSort
sExpr
      Just String
logic -> if String
"QF" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
logic then Expr 'BoolSort -> m (Expr 'BoolSort)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr 'BoolSort
sExpr else Expr 'BoolSort -> m (Expr 'BoolSort)
forall s (m :: * -> *) (t :: SMTSort).
(MonadSMT s m, KnownSMTSort t) =>
Expr t -> m (Expr t)
quantify Expr 'BoolSort
sExpr
    (SMT -> SMT) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((SMT -> SMT) -> m ()) -> (SMT -> SMT) -> m ()
forall a b. (a -> b) -> a -> b
$ \SMT
s -> SMT
s SMT -> (SMT -> SMT) -> SMT
forall a b. a -> (a -> b) -> b
& ASetter SMT SMT (Seq (Expr 'BoolSort)) (Seq (Expr 'BoolSort))
Lens' SMT (Seq (Expr 'BoolSort))
formulas ASetter SMT SMT (Seq (Expr 'BoolSort)) (Seq (Expr 'BoolSort))
-> (Seq (Expr 'BoolSort) -> Seq (Expr 'BoolSort)) -> SMT -> SMT
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Seq (Expr 'BoolSort) -> Expr 'BoolSort -> Seq (Expr 'BoolSort)
forall s a. Snoc s s a a => s -> a -> s
|> Expr 'BoolSort
qExpr)
  {-# INLINE assert #-}

  setOption :: SMTOption -> m ()
setOption SMTOption
opt = ([SMTOption] -> Identity [SMTOption]) -> SMT -> Identity SMT
Lens' SMT [SMTOption]
options (([SMTOption] -> Identity [SMTOption]) -> SMT -> Identity SMT)
-> [SMTOption] -> m ()
forall s (m :: * -> *) a.
(MonadState s m, Semigroup a) =>
ASetter' s a -> a -> m ()
<>= SMTOption -> [SMTOption]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure SMTOption
opt

  setLogic :: String -> m ()
setLogic String
l = (Maybe String -> Identity (Maybe String)) -> SMT -> Identity SMT
Lens' SMT (Maybe String)
mlogic ((Maybe String -> Identity (Maybe String)) -> SMT -> Identity SMT)
-> String -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a (Maybe b) -> b -> m ()
?= String
l