putting back a function to calculate the wlp of a method and check its satisfiability.

src/Javawlp/API.hs

@@ -6,6 +6,7 @@ module Javawlp.API where
 import Language.Java.Syntax
 import Language.Java.Parser
 import Language.Java.Pretty
+import Z3.Monad
 
 import Javawlp.Engine.WLP
 import Javawlp.Engine.Types
@@ -77,9 +78,23 @@ printWlp sourcePath methodName postCond = do
   let q = post_ postCond
   p <- wlpMethod defaultConf typeEnv decls (Ident methodName) q
   putStrLn $ showMethodWlp methodName q p
+  let (result,model) = unsafeIsSatisfiable (extendEnv typeEnv decls (Ident methodName)) decls p
+  case result of
+     Unsat -> putStrLn "** The wlp is UNSATISFIABLE."
+     Undef -> putStrLn "** Unable to decide the wlp's satisfiablity."
+     _     -> do
+              putStrLn "** The wlp is SATISFIABLE."
+              case model of
+                Just m -> do { putStrLn "** Model:" ; s <- evalZ3 (modelToString m) ; putStrLn s }
+                _      -> return ()
+                
 
 showMethodWlp :: String -> Exp -> Exp -> String
 showMethodWlp methodName postCond wlp = 
-       "wlp of " ++ methodName ++ " over " ++ prettyPrint postCond
+       "** wlp of " ++ methodName ++ " over " ++ prettyPrint postCond
                  ++ " is "
                  ++ prettyPrint wlp
+                 
+                 
+                 
+

src/Javawlp/Engine/Verifier.hs

@@ -30,6 +30,22 @@ isFalse env decls e =
             Unsat -> return True
             _     -> return False
         
+-- | Check if a formula is satisfiable, and if so, return the model for it as well.
+-- The result is a pair (r,m) where r is either Sat, Unsat, or Undef. If r is Sat,
+-- then m is Just v where v a model witnessing the satisfiability of the input
+-- formula. Else m is Nothing.
+--            
+unsafeIsSatisfiable :: TypeEnv -> [TypeDecl] -> Exp -> (Result, Maybe Model)
+unsafeIsSatisfiable env decls e = unsafePerformIO $ evalZ3 z3
+    where
+    z3 = do
+         ast <- foldExp expAssertAlgebra e env decls
+         assert ast
+         r <- solverCheckAndGetModel
+         solverReset
+         return r  
+
+        
 -- | Unsafe version of isTrue
 unsafeIsTrue :: TypeEnv -> [TypeDecl] -> Exp -> Bool
 unsafeIsTrue env decls = unsafePerformIO . evalZ3 . isTrue env decls