From ebfbe8efce20a99981dc362d3f89393034a21980 Mon Sep 17 00:00:00 2001 From: Andrei Date: Sun, 14 Jan 2024 06:32:56 +0000 Subject: [PATCH 1/2] Split on unique conditions. --- saw-core/src/Verifier/SAW/Rewriter.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index aa51f2638d..60b4c2d383 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/saw-core/src/Verifier/SAW/Rewriter.hs @@ -936,7 +936,7 @@ 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' + splitConds sc ss (Set.toList $ Set.fromList $ map fst conds) t' splitConds :: Ord a => SharedContext -> Simpset a -> [Term] -> Term -> IO Term From 451338fb9a85160b8732f31d843a14b98138037d Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 16 Jan 2024 03:19:30 +0000 Subject: [PATCH 2/2] 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 60b4c2d383..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 (Set.toList $ Set.fromList $ 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