Make saw-core simulator use separate IntMaps for open/closed subterms.

This gives a significant speedup to mkMemoLocal, because memo table
updates are done with insertions into a much smaller table.

saw-core/src/Verifier/SAW/Simulator.hs

@@ -501,18 +501,19 @@ evalClosedTermF cfg memoClosed tf = evalTermF cfg lam recEval tf []
 mkMemoLocal :: forall l. (VMonadLazy l, Show (Extra l)) =>
                SimulatorConfig l -> IntMap (Thunk l) ->
                Term -> Env l -> EvalM l (IntMap (Thunk l))
-mkMemoLocal cfg memoClosed t env = go memoClosed t
+mkMemoLocal cfg memoClosed t env = go mempty t
   where
     go :: IntMap (Thunk l) -> Term -> EvalM l (IntMap (Thunk l))
     go memo (Unshared tf) = goTermF memo tf
-    go memo (STApp{ stAppIndex = i, stAppTermF = tf }) =
-      case IMap.lookup i memo of
-        Just _ -> return memo
-        Nothing -> do
-          memo' <- goTermF memo tf
-          thunk <- delay (evalLocalTermF cfg memoClosed memo' tf env)
-          return (IMap.insert i thunk memo')
-
+    go memo (STApp{ stAppIndex = i, stAppFreeVars = fv, stAppTermF = tf })
+      | fv == emptyBitSet = pure memo
+      | otherwise =
+        case IMap.lookup i memo of
+          Just _ -> pure memo
+          Nothing ->
+            do memo' <- goTermF memo tf
+               thunk <- delay (evalLocalTermF cfg memoClosed memo' tf env)
+               pure (IMap.insert i thunk memo')
     goTermF :: IntMap (Thunk l) -> TermF Term -> EvalM l (IntMap (Thunk l))
     goTermF memo tf =
       case tf of
@@ -548,10 +549,11 @@ evalLocalTermF cfg memoClosed memoLocal tf0 env = evalTermF cfg lam recEval tf0
   where
     lam = evalOpen cfg memoClosed
     recEval (Unshared tf) = evalTermF cfg lam recEval tf env
-    recEval (STApp{ stAppIndex = i }) =
-      case IMap.lookup i memoLocal of
+    recEval (STApp{ stAppIndex = i, stAppFreeVars = fv }) =
+      case IMap.lookup i memo of
         Just x -> force x
         Nothing -> panic "evalLocalTermF" ["internal error"]
+      where memo = if fv == emptyBitSet then memoClosed else memoLocal
 
 {-# SPECIALIZE evalOpen ::
   Show (Extra l) =>
@@ -576,10 +578,11 @@ evalOpen cfg memoClosed t env = do
   memoLocal <- mkMemoLocal cfg memoClosed t env
   let eval :: Term -> MValue l
       eval (Unshared tf) = evalF tf
-      eval (STApp{ stAppIndex = i, stAppTermF = tf }) =
-        case IMap.lookup i memoLocal of
+      eval (STApp{ stAppIndex = i, stAppFreeVars = fv, stAppTermF = tf }) =
+        case IMap.lookup i memo of
           Just x -> force x
           Nothing -> evalF tf
+        where memo = if fv == emptyBitSet then memoClosed else memoLocal
       evalF :: TermF Term -> MValue l
       evalF tf = evalTermF cfg (evalOpen cfg memoClosed) eval tf env
   eval t