Add a command to clear the SAWCore term cache.

This cache is used for hash-consing.  It shouldn't affect
correctness to clear it, although it may make hash-consing
less effective.

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

@@ -59,6 +59,7 @@ module Verifier.SAW.SharedTerm
   , SharedContext
   , mkSharedContext
   , scGetModuleMap
+  , scClearTermCache
     -- ** Low-level generic term constructors
   , scTermF
   , scFlatTermF
@@ -358,6 +359,7 @@ data SharedContext = SharedContext
   , scNamingEnv      :: IORef SAWNamingEnv
   , scGlobalEnv      :: IORef (HashMap Ident Term)
   , scFreshGlobalVar :: IO VarIndex
+  , scClearTermCache :: IO ()
   }
 
 -- | Create a new term from a lower-level 'FlatTermF' term.
@@ -2331,6 +2333,7 @@ mkSharedContext = do
            , scFreshGlobalVar = freshGlobalVar
            , scNamingEnv = envRef
            , scGlobalEnv = gr
+           , scClearTermCache = modifyMVar cr (\_ -> return (emptyAppCache , ()))
            }
 
 useChangeCache :: C m => Cache m k (Change v) -> k -> ChangeT m v -> ChangeT m v

src/SAWScript/Builtins.hs

@@ -411,6 +411,11 @@ getTopLevelPPOpts = do
   opts <- fmap rwPPOpts getTopLevelRW
   return (SV.sawPPOpts opts)
 
+clear_term_cache :: TopLevel ()
+clear_term_cache =
+  do sc <- getSharedContext
+     io $ scClearTermCache sc
+
 show_term :: Term -> TopLevel String
 show_term t =
   do opts <- getTopLevelPPOpts

src/SAWScript/Interpreter.hs

@@ -1033,6 +1033,14 @@ primitives = Map.fromList
     Current
     [ "Return the type of the given term." ]
 
+  , prim "clear_term_cache"    "TopLevel ()"
+    (pureVal clear_term_cache)
+    Experimental
+    [ "Empty the hash-consing cache for SAWCore terms."
+    , "This can be useful to help control memory usage, but makes"
+    , "hash-consing less effective."
+    ]
+
   , prim "show_term"           "Term -> String"
     (funVal1 show_term)
     Current