Skip to content

Commit

Permalink
Split on unique conditions. (#2010)
Browse files Browse the repository at this point in the history
* Split on unique conditions.

* Address comments.
  • Loading branch information
andreistefanescu authored Jan 16, 2024
1 parent a5457b0 commit 3aa9f31
Show file tree
Hide file tree
Showing 2 changed files with 6 additions and 1 deletion.
1 change: 1 addition & 0 deletions saw-core/saw-core.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ library
data-inttrie,
data-ref,
directory,
extra,
filepath,
hashable >= 1.3.4,
lens >= 3.8,
Expand Down
6 changes: 5 additions & 1 deletion saw-core/src/Verifier/SAW/Rewriter.hs
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ import Data.IORef
import qualified Data.Foldable as Foldable
import Data.Map (Map)
import qualified Data.List as List
import Data.List.Extra (nubOrd)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set
Expand Down Expand Up @@ -936,7 +937,10 @@ hoistIfs sc t = do
let ss :: Simpset () = addRules rules emptySimpset

(t', conds) <- doHoistIfs sc ss cache itePat . snd =<< rewriteSharedTerm sc ss t
splitConds sc ss (map fst conds) t'

-- remove duplicate conditions from the list, as muxing in SAW can result in
-- many copies of the same condition, which cause a performance issue
splitConds sc ss (nubOrd $ map fst conds) t'


splitConds :: Ord a => SharedContext -> Simpset a -> [Term] -> Term -> IO Term
Expand Down

0 comments on commit 3aa9f31

Please sign in to comment.