Commits

Scott West committed 4319ab7

Eval a Z3 script with given context and solver
This is useful if you want to maintain the context/solver externally,
for example if you want to push/pop and return again to the caller.
#changelog #z3monad #addition

Edited-by: Iago Abal <mail@iagoabal.eu>

  • Participants
  • Parent commits 97b74d4

Comments (0)

Files changed (1)

   , Logic(..)
   , evalZ3
   , evalZ3With
+  , evalZ3WithEnv
 
   -- * Types
   , Symbol
   , App
   , Pattern
   , Model
+  , Base.Context
   , FuncInterp
   , FuncEntry
   , FuncModel(..)
+  , Base.Solver
 
   -- ** Satisfiability result
   , Result(..)
 evalZ3 :: Z3 a -> IO a
 evalZ3 = evalZ3With Nothing stdOpts
 
+-- | Eval a Z3 script with a given context and solver.
+evalZ3WithEnv :: Base.Context
+              -> Base.Solver
+              -> Z3 a
+              -> IO a
+evalZ3WithEnv ctx slv (Z3 s) =
+  runReaderT s (Z3Env (Just slv) ctx)
+
 ---------------------------------------------------------------------
 -- Contexts