Skip to content

Commit

Permalink
remove MonadSymbolic constraint from registerUISMTFunction and smtFun…
Browse files Browse the repository at this point in the history
…Name
  • Loading branch information
lsrcz committed Jul 12, 2024
1 parent 52ad01b commit 7bdf325
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Data/SBV/Control/Utils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -398,7 +398,7 @@ getValue s = do
-- | A class which allows for sexpr-conversion to functions
class (HasKind r, SatModel r) => SMTFunction fun a r | fun -> a r where
sexprToArg :: fun -> [SExpr] -> Maybe a
smtFunName :: (MonadIO m, SolverContext m, MonadSymbolic m) => fun -> m ((String, Maybe [String]), Bool)
smtFunName :: (MonadIO m, SolverContext m) => fun -> m ((String, Maybe [String]), Bool)
smtFunSaturate :: fun -> SBV r
smtFunType :: fun -> SBVType
smtFunDefault :: fun -> Maybe r
Expand Down Expand Up @@ -476,7 +476,7 @@ class (HasKind r, SatModel r) => SMTFunction fun a r | fun -> a r where
-- | Registering an uninterpreted SMT function. This is typically not necessary as uses of the UI
-- function itself will register it automatically. But there are cases where doing this explicitly can
-- come in handy.
registerUISMTFunction :: (MonadIO m, SolverContext m, MonadSymbolic m) => SMTFunction fun a r => fun -> m ()
registerUISMTFunction :: (MonadIO m, SolverContext m) => SMTFunction fun a r => fun -> m ()
registerUISMTFunction f = do st <- contextState
(nmas, isCurried) <- smtFunName f
io $ newUninterpreted st nmas (smtFunType f) (UINone isCurried)
Expand Down

0 comments on commit 7bdf325

Please sign in to comment.