diff --git a/src/Language/Hasmtlib/Type/OMT.hs b/src/Language/Hasmtlib/Type/OMT.hs index 6b267de..fe908b4 100644 --- a/src/Language/Hasmtlib/Type/OMT.hs +++ b/src/Language/Hasmtlib/Type/OMT.hs @@ -29,14 +29,12 @@ 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 Language.Hasmtlib.Type.SMT import Data.List (isPrefixOf) import Data.Default import Data.Coerce import Data.Sequence hiding ((|>), filter) -import Data.Data (toConstr, showConstr) import Control.Monad.State import Control.Lens hiding (List) @@ -91,10 +89,7 @@ instance MonadState OMT m => MonadSMT OMT m where modify $ \s -> s & (smt.formulas) %~ (|> qExpr) {-# INLINE assert #-} - setOption opt = smt.options %= ((opt:) . filter (not . eqCon opt)) - where - eqCon :: SMTOption -> SMTOption -> Bool - eqCon l r = showConstr (toConstr l) == showConstr (toConstr r) + setOption opt = smt.options <>= pure opt setLogic l = smt.mlogic ?= l diff --git a/src/Language/Hasmtlib/Type/SMT.hs b/src/Language/Hasmtlib/Type/SMT.hs index 86805ae..6e56b26 100644 --- a/src/Language/Hasmtlib/Type/SMT.hs +++ b/src/Language/Hasmtlib/Type/SMT.hs @@ -25,7 +25,6 @@ import Data.List (isPrefixOf) import Data.Default import Data.Coerce import Data.Sequence hiding ((|>), filter) -import Data.Data (toConstr, showConstr) import Data.HashMap.Lazy (HashMap) import Control.Monad.State import Control.Lens hiding (List) @@ -71,9 +70,6 @@ instance MonadState SMT m => MonadSMT SMT m where modify $ \s -> s & formulas %~ (|> qExpr) {-# INLINE assert #-} - setOption opt = options %= ((opt:) . filter (not . eqCon opt)) - where - eqCon :: SMTOption -> SMTOption -> Bool - eqCon l r = showConstr (toConstr l) == showConstr (toConstr r) + setOption opt = options <>= pure opt setLogic l = mlogic ?= l