1. Nathan Howell
  2. z3-haskell

Commits

Nathan Howell  committed a3a0da6

Add debug functions to dump the context and model as strings

  • Participants
  • Parent commits 6bc8685
  • Branches default

Comments (0)

Files changed (4)

File Z3/Base.hs

View file
  • Ignore whitespace
 
     -- * Models
     , eval
+    , showModel
+    , showContext
 
     -- * Constraints
     , assertCnstr
                                                  m <- mkModel c z3m
                                                  return $ Sat m
 
+showModel :: Context -> Model -> IO String
+showModel (Context fpc) (Model pm) =
+  withForeignPtr fpc $ \ pc ->
+    z3_model_to_string pc pm >>= peekCString
+ 
+showContext :: Context -> IO String
+showContext (Context fpc) =
+  withForeignPtr fpc $ \ pc ->
+    z3_context_to_string pc >>= peekCString
+
 -- | Check whether the given logical context is consistent or not.
 --
 -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03>

File Z3/Base/C.hsc

View file
  • Ignore whitespace
 foreign import ccall unsafe "Z3_del_model"
     z3_del_model :: Ptr Z3_context -> Ptr Z3_model -> IO ()
 
+foreign import ccall unsafe "Z3_model_to_string"
+    z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO CString
+
+foreign import ccall unsafe "Z3_context_to_string"
+    z3_context_to_string :: Ptr Z3_context -> IO CString
+
 
 -- TODO From section 'Constraints' on.

File Z3/Lang/Monad.hs

View file
  • Ignore whitespace
     , mkIte
     , pop
     , push
+    , showContext
+    , showModel
 
     -- * Satisfiability result
     , Base.Result(..)
 getModel :: Z3 (Base.Result Base.Model)
 getModel = liftZ3Op Base.getModel
 
+showModel :: Z3 (Base.Result String)
+showModel = do
+  c <- gets context
+  mm <- getModel
+  case mm of
+    Base.Sat m -> liftZ3 . liftM Base.Sat $ Base.showModel c m
+    Base.Unsat -> return Base.Unsat
+    Base.Undef -> return Base.Undef
+
+showContext :: Z3 String
+showContext = do
+  c <- gets context
+  liftZ3 $ Base.showContext c
+
 getValue :: Base.Z3Type a => Base.AST a -> Z3 a
 getValue = liftZ3Op2 Base.getValue
 

File Z3/Lang/Prelude.hs

View file
  • Ignore whitespace
     , let_
     , check
     , checkModel
+    , showContext
+    , showModel
     , push, pop
 
     -- * Expressions