Add the ability to emit "reset" commands to solvers.

The semantics of "reset" are, roughly, to forget all assertions
and pushed assertion frames.  However, as with push/pop semanics,
there are some solver-specific differences in how this works.

Yices will remember declarations and definitions even across "reset",
whereas SMTLib2-compliant solvers will instead forget definitions
and declarations.

Note that we specifically use the "(reset-asserions)"
command in SMTLib2, rather than the "(reset)" command.  This is beacuse
"(reset)" forgets all logic settings, option settings, etc, in addition
to the assertion state, which is more agressive than we want.

what4/src/What4/Protocol/Online.hs

@@ -16,6 +16,7 @@ module What4.Protocol.Online
   , killSolver
   , push
   , pop
+  , reset
   , inNewFrame
   , check
   , getModel
@@ -122,6 +123,10 @@ checkSatisfiableWithModel proc p k =
 --------------------------------------------------------------------------------
 -- Basic solver interaction.
 
+reset :: SMTReadWriter s => WriterConn t s -> IO ()
+reset c = do resetEntryStack c
+             addCommand c (resetCommand c)
+
 -- | Push a new solver assumption frame.
 push :: SMTReadWriter s => WriterConn t s -> IO ()
 push c = do pushEntryStack c

what4/src/What4/Protocol/SMTLib2.hs

@@ -395,6 +395,8 @@ instance SMTLib2Tweaks a => SMTWriter (Writer a) where
 
   pushCommand _  = Cmd "(push 1)"
   popCommand _   = Cmd "(pop 1)"
+  resetCommand _ = Cmd "(reset-assertions)"
+
   checkCommand _ = checkSatCommand
   setOptCommand _ x y = setOptionCommand (Option opt)
     where opt = Builder.fromText x <> Builder.fromText " " <> y

what4/src/What4/Protocol/SMTWriter.hs

@@ -57,6 +57,7 @@ module What4.Protocol.SMTWriter
               )
   , connState
   , newWriterConn
+  , resetEntryStack
   , pushEntryStack
   , popEntryStack
   , Command(..)
@@ -584,6 +585,12 @@ data WriterConn t (h :: *) =
                -- ^ The specific connection information.
              }
 
+-- | Clear the entry stack, and start with a fresh one.
+resetEntryStack :: WriterConn t h -> IO ()
+resetEntryStack c = do
+  h <- newIdxCache
+  writeIORef (entryStack c) [h]
+
 -- | Push a new frame to the stack for maintaining the writer cache.
 pushEntryStack :: WriterConn t h -> IO ()
 pushEntryStack c = do
@@ -677,6 +684,9 @@ class (SupportTermOps (Term h)) => SMTWriter h where
   -- | Pop 1 existing scope
   popCommand    :: f h -> Command h
 
+  -- | Reset the solver state, forgetting all pushed frames and assertions
+  resetCommand  :: f h -> Command h
+
   -- | Check if the current set of assumption is satisfiable
   checkCommand  :: f h -> Command h
 

what4/src/What4/Solver/Yices.hs

@@ -335,6 +335,7 @@ instance SMTWriter (Connection s) where
 
   pushCommand _   = Cmd "(push)"
   popCommand _    = Cmd "(pop)"
+  resetCommand _  = Cmd "(reset)"
   checkCommand _  = Cmd "(check)"
   setOptCommand _ x o = setParamCommand x o
   assertCommand _ (T nm) = Cmd $ app "assert" [nm]