Skip to content

Commit

Permalink
107-smart-ite: fix bug where setOption would overwrite any Custom Option
Browse files Browse the repository at this point in the history
  • Loading branch information
bruderj15 committed Sep 26, 2024
1 parent b4f4040 commit 8a03a0a
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 11 deletions.
7 changes: 1 addition & 6 deletions src/Language/Hasmtlib/Type/OMT.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down Expand Up @@ -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

Expand Down
6 changes: 1 addition & 5 deletions src/Language/Hasmtlib/Type/SMT.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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

0 comments on commit 8a03a0a

Please sign in to comment.