From 3aa9f31e0fadcdba96855f58c916bfa670bc449a Mon Sep 17 00:00:00 2001
From: Andrei Stefanescu <andrei@stefanescu.io>
Date: Mon, 15 Jan 2024 22:19:44 -0800
Subject: [PATCH] Split on unique conditions. (#2010)

* Split on unique conditions.

* Address comments.
---
 saw-core/saw-core.cabal               | 1 +
 saw-core/src/Verifier/SAW/Rewriter.hs | 6 +++++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/saw-core/saw-core.cabal b/saw-core/saw-core.cabal
index f5be965b28..6fee0be5fc 100644
--- a/saw-core/saw-core.cabal
+++ b/saw-core/saw-core.cabal
@@ -32,6 +32,7 @@ library
     data-inttrie,
     data-ref,
     directory,
+    extra,
     filepath,
     hashable >= 1.3.4,
     lens >= 3.8,
diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs
index aa51f2638d..92fb67eb54 100644
--- a/saw-core/src/Verifier/SAW/Rewriter.hs
+++ b/saw-core/src/Verifier/SAW/Rewriter.hs
@@ -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
@@ -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