Best way to copy solver state?

Hey Levent,

I have a peculiar use case that I was hoping you'd have some insight on. I have a long computation in symbolic mode, and then lots of push/pop calls in query mode where I'll be retrieving a lot of models. Because model generation is a substantial amount of time in this domain I am trying to do this asynchronously with a pool of sbv threads.

So I essentially want to copy the symbolic and query state and "refresh" the threads internal states. I have a pool of solvers, and a channel they listen to for query computations. When one of these solvers receives a query computation I want to set its internal solver state appropriately so that the underlying z3 instance has the right information.

I experimented in my sbv fork with freezing the states, like this: Notice no IORefs

data FrozenState  = FrozenState { fpathCond     :: !SVal                             -- ^ kind KBool
                                , fstartTime    :: !UTCTime
                                , frunMode      :: !SBVRunMode
                                , frIncState    :: !FrozenIncState
                                , frCInfo       :: ![(String, CV)]
                                , frObservables :: !(S.Seq (Name, CV -> Bool, SV))
                                , frctr         :: !Int
                                , frUsedKinds   :: !KindSet
                                , frUsedLbls    :: !(Set.Set String)
                                , frinps        :: !Inputs
                                , frConstraints :: !(S.Seq (Bool, [(String, String)], SV))
                                , frouts        :: ![SV]
                                , frtblMap      :: !TableMap
                                , fspgm         :: !SBVPgm
                                , frconstMap    :: !CnstMap
                                , frexprMap     :: !ExprMap
                                , frArrayMap    :: !ArrayMap
                                , frFArrayMap   :: !FArrayMap
                                , frUIMap       :: !UIMap
                                , frCgMap       :: !CgMap
                                , fraxioms      :: ![(String, [String])]
                                , frSMTOptions  :: ![SMTOption]
                                , frOptGoals    :: ![Objective (SV, SV)]
                                , frAsserts     :: ![(String, Maybe CallStack, SV)]
                                , frSVCache     :: !(Cache SV)
                                , frAICache     :: !(Cache ArrayIndex)
                                , frFAICache    :: !(Cache FArrayIndex)
                                , frQueryState  :: !(Maybe QueryState)
                                }

So this state will be pure and immutable data (I did the same thing for IncState) Then I have two methods freeze and unfreeze, I'll show the IncState versions because they're smaller:

freezeIncSt :: MonadSymbolic m => m FrozenIncState
{-# INLINE freezeIncSt #-}
freezeIncSt = do st <- symbolicEnv >>= liftIO . readIORef . rIncState
                 !sNewInps        <- liftIO $ readIORef (rNewInps        st)
                 !sNewKinds       <- liftIO $ readIORef (rNewKinds       st)
                 !sNewConsts      <- liftIO $ readIORef (rNewConsts      st)
                 !sNewArrs        <- liftIO $ readIORef (rNewArrs        st)
                 !sNewTbls        <- liftIO $ readIORef (rNewTbls        st)
                 !sNewUIs         <- liftIO $ readIORef (rNewUIs         st)
                 !sNewAsgns       <- liftIO $ readIORef (rNewAsgns       st)
                 !sNewConstraints <- liftIO $ readIORef (rNewConstraints st)
                 return $! FrozenIncState { fNewInps        = sNewInps
                                          , fNewKinds       = sNewKinds
                                          , fNewConsts      = sNewConsts
                                          , fNewArrs        = sNewArrs
                                          , fNewTbls        = sNewTbls
                                          , fNewUIs         = sNewUIs
                                          , fNewAsgns       = sNewAsgns
                                          , fNewConstraints = sNewConstraints
                                          }

and

unfreezeIncSt :: (MonadSymbolic m, MonadIO m) => FrozenIncState -> m ()
unfreezeIncSt st =
  do let sNewInps         = fNewInps        st
         sNewKinds        = fNewKinds       st
         sNewConsts       = fNewConsts      st
         sNewArrs         = fNewArrs        st
         sNewTbls         = fNewTbls        st
         sNewUIs          = fNewUIs         st
         sNewAsgns        = fNewAsgns       st
         sNewConstraints  = fNewConstraints st
     oldSt <- symbolicEnv
     let
       update :: (IncState -> IORef a) -> a -> IO ()
       update field value = modifyIncState oldSt field (const value)
     liftIO $
       do update rNewInps        sNewInps
          update rNewKinds       sNewKinds
          update rNewConsts      sNewConsts
          update rNewArrs        sNewArrs
          update rNewTbls        sNewTbls
          update rNewUIs         sNewUIs
          update rNewAsgns       sNewAsgns
          update rNewConstraints sNewConstraints

But this isn't working. I thought by creating pure data here the async would be easier but I'm still getting incorrect results or worse a Blocked on MVar signal. sbv does attempt synchronization which succeeds but then the threads die, for example:

[Debug] [Producer: 1] ==> After reset : fromList [("a",<symbolic> :: SBool),("two",<symbolic> :: SBool),("one",<symbolic> :: SBool)] @(vsmt-0.0.1-inplace:Solve Data/Solve.hs:76:9)
[Debug] Cache miss on : "b" @(vsmt-0.0.1-inplace:Solve Data/Solve.hs:76:9)
[FAIL] (declare-fun s3 () Bool)
[SYNC] Attempting to synchronize with tag: "terminating upon unexpected response (at: 2020-12-21 18:04:47.684253434 PST)"
[FIRE] (echo "terminating upon unexpected response (at: 2020-12-21 18:04:47.684253434 PST)")
[SYNC] Synchronization achieved using tag: "terminating upon unexpected response (at: 2020-12-21 18:04:47.684253434 PST)"
thread blocked indefinitely in an MVar operation

So I know this is way outside the normal use case of sbv but I was hoping you might have some thoughts on best practice. I had already tried to exploit the reader monad with mapSymbolicT and mapReaderT but it also resulted in a blocked thread. My hypothesis there was that the State data type is holding references (IORefs) and when a thread communicates these references are getting garbage collected before they're read, so by freezing I should avoid this but to no avail it seems.

Best,

Jeff

I'm a little confused by this. In particular, this line in the output:

[FAIL] (declare-fun s3 () Bool)

means SBV sent this line to the solver, but did not get back a success response. That can happen if z3 process has gotten into a funky state, or if it already died for some reason.

Maybe I should start with a simpler question: Do your threads have separate connections to a new instance of z3? If that's the case, you have to "replay" the entire interaction with the solver in each thread, no? Is that happening?

Or, perhaps these threads all talk to the one and the same z3 instance. If that's the case, I wouldn't count on this to work correctly at all, since I doubt you can have more than one pipe open with a process, I think.

But perhaps I'm misunderstanding the setup here completely.

Each thread has it's own private instance of z3. My attempts to freeze and unfreeze the sbv's state is an attempt to replay the entire interaction without having to actually replay the entire interaction.

So for example imagine only two threads each with their own z3 instance: z1 and z2. I want to pause an interaction on z1, capture the z1 sbv state, and then start from that pause point on z2.

So the naive way would be to re-compute the entire interaction that lead up to the pause point on z1, then replay that on z2, but because in this domain that computation can be pretty expensive (iterating over tens of thousands of variables, even though the sat problem is under-constrained) I want to capture the sbv state which was built up in z1 and then write the state on z2 to be identical to z1. So after the copy and write of the state there should be no difference between z1 and z2.

But my attempts to get this copy (freeze) and write (unfreeze) haven't worked because I receive the error you mention above. I assumed this was because modifyState and modifyIncState were not thread safe, so I altered them to use atomicModifyIORef' but this made no difference. So perhaps there is information which exists in z1 that is not being copied over to z2?

I'd be curious to know why you're getting:

[FAIL] (declare-fun s3 () Bool)

Add some debugging perhaps to see exactly what went on with the solver instance connected to the thread that issued this.

In addition, I don't think you can replicate the state of the solver unless you exactly replay all the commands. After each command you issue, z3 will internally update a whole bunch of its internal state, keep track of learned-lemmas etc; so I'm not sure if it would be possible to bring it back to the "exact" same state as the first one. A better idea might be to see if z3 exposes some sort of an API to "clone" itself. A quick stack-overflow search reveals some (not-that-helpful but can be a good starting point to dig into) answers:

https://stackoverflow.com/questions/36720288/duplicate-a-z3context/36721020#36721020 https://stackoverflow.com/questions/16516337/copying-z3-solver

Oh great pointers. I'll look into this and report back, it might be a decent addition to either Internals or Control modules.

I believe the error you point out is due to some specific code I wrote. I noticed I can incite the error if I try to copy the whole State in query mode, but if I only copy IncState in query mode then sbv happily continues which is expected behavior.

Closing this. I've abandoned this particular architecture. The z3 people don't provide a way to do this because references would become confused between threads so their recommended method is to "replay" the entire sat context, but we already implemented this strategy in PR #500 and PR #504, using the Symbolic and Query monads.

We could implement something very low level, or use the symbolic/query state to replay the solver context but I suspect this would be a pretty substantial effort for very little pay off. Just to support solvers other than z3 we would need to write ffi's and it just isn't reasonable for a low ticket item.

LeventErkok / sbv

Best way to copy solver state? #570