Z3: feedback (4 combinations)

src/LogicIR/Backend/QuickCheck/API.hs

 module LogicIR.Backend.QuickCheck.API (equivalentTo) where
 
-import Control.Arrow ((***))
-import Data.Map (Map)
-import qualified Data.Map.Lazy as M
-import Data.Maybe (fromJust, fromMaybe, isNothing)
+import           Control.Arrow                             ((***))
+import qualified Data.Map.Lazy                             as M
 import qualified LogicIR.Backend.QuickCheck.ModelGenerator as QC
-import LogicIR.Backend.QuickCheck.Test
-import LogicIR.Expr
-import LogicIR.Pretty (prettyLExpr)
-import Model
+import           LogicIR.Backend.QuickCheck.Test
+import           LogicIR.Expr                              hiding (b, r)
+import           LogicIR.Pretty                            (prettyLExpr)
+import           Model
 
 -- | Determine the equality of two method's pre/post conditions.
 equivalentTo :: LExpr -> LExpr -> IO Response
 equivalentTo lexpr lexpr' = do
     (eq, testModel) <- testEquality 1000 lexpr lexpr'
-    let feedback = NoFeedback -- TODO check implication (stronger + weaker)
+    let feedback = Feedback { pre = defFeedback -- TODO check which combinations are possible
+                            , post = defFeedback -- leave as is
+                            }
     if eq
     then return Equivalent
-    else return $ NotEquivalent (toZ3Model testModel) (feedback, NoFeedback)
+    else return $ NotEquivalent (toZ3Model testModel) feedback
 
 toZ3Model :: (QC.Model, QC.ArrayModel) -> Model
 toZ3Model (m, arrayM) =
@@ -29,6 +29,7 @@ toModelVal :: LExpr -> ModelVal
 toModelVal (LConst (CBool b)) = BoolVal b
 toModelVal (LConst (CInt  i)) = IntVal  $ toInteger i
 toModelVal (LConst (CReal r)) = RealVal r
+toModelVal _                  = error "toModelVal: invalid LExpr"
 
 toModelVals :: [LExpr] -> ModelVal
 toModelVals = ManyVal . map toModelVal

src/LogicIR/Backend/Z3/API.hs

@@ -8,14 +8,13 @@ import qualified Z3.Base  as Z3
 import           Z3.Monad hiding (Model)
 
 import           Control.Exception.Base (tryJust)
-import           Control.Monad          (forM, when)
+import           Control.Monad          (forM)
 import qualified Data.Map               as M
 import           Data.Maybe             (fromJust)
 import           Data.String
 
-import Control.Monad.Trans   (liftIO)
 import LogicIR.Backend.Z3.Z3
-import LogicIR.Expr          (LExpr, lnot, (.<==>), (.==>))
+import LogicIR.Expr          (LExpr, lnot, (.&&), (.<==>))
 import Model
 
 data Z3Response = Satisfiable Model | Unsatisfiable | Undecidable
@@ -27,18 +26,19 @@ equivalentTo l l' = do
   equiv <- checkZ3 $ lnot (l .<==> l')
   case equiv of
     Satisfiable m -> do
-      feedback <- do
-        stronger <- checkZ3 $ lnot (l .==> l')
-        case stronger of
-          Unsatisfiable -> return Stronger
-          _ -> do
-            weaker <- checkZ3 $ lnot (l' .==> l)
-            case weaker of
-              Unsatisfiable -> return Weaker
-              _             -> return NoFeedback
-      return $ NotEquivalent m (feedback, NoFeedback)
+      res <- sequence $ checkZ3 <$>
+        [l .&& l', l .&& lnot l', lnot l .&& l', lnot l .&& lnot l']
+      let feedback = mkFeedback $ toBool <$> res
+      return $ NotEquivalent m Feedback {pre = feedback, post = defFeedback}
     Unsatisfiable -> return Equivalent
     Undecidable -> return Undefined
+  where
+    mkFeedback :: [Bool] -> SingleFeedback
+    mkFeedback [b1, b2, b3, b4] = (b1, b2, b3, b4)
+    mkFeedback _                = defFeedback
+    toBool :: Z3Response -> Bool
+    toBool (Satisfiable _) = True
+    toBool _               = False
 
 -- | Checks the validity of a logical statement.
 checkZ3 :: LExpr -> IO Z3Response

src/Model.hs

@@ -16,18 +16,30 @@ import qualified Text.Parsec.Token    as Tokens
 import LogicIR.ParserUtils
 
 -- | Feedback type.
-data Feedback = Stronger   -- A ==> B
-              | Weaker     -- A <== B
-              | NoFeedback -- A ??? B
-                deriving (Eq, Show, Generic)
+type SingleFeedback = ( Bool -- T-T
+                      , Bool -- T-F
+                      , Bool -- F-T
+                      , Bool -- F-F
+                      )
+
+defFeedback :: SingleFeedback
+defFeedback = (False, False, False, False)
+
+data Feedback = Feedback
+  { pre  :: SingleFeedback
+  , post :: SingleFeedback
+  } deriving (Eq, Show, Generic)
+
+defFeedback' :: Feedback
+defFeedback' = Feedback { pre = defFeedback, post = defFeedback }
 
 -- | Response type.
 data Response = Equivalent
-              | NotEquivalent Model (Feedback, Feedback)
+              | NotEquivalent Model Feedback
               | ErrorResponse String
               | Undefined
               | Timeout
-                deriving (Eq, Show)
+              deriving (Eq, Show)
 
 (<>) :: Response -> Response -> Response
 ErrorResponse e        <> _                       = ErrorResponse e
@@ -35,7 +47,7 @@ _                      <> ErrorResponse e         = ErrorResponse e
 Timeout                <> _                       = Timeout
 Undefined              <> _                       = Undefined
 Equivalent             <> r                       = r
-NotEquivalent s (f, _) <> NotEquivalent _ (f', _) = NotEquivalent s (f, f')
+NotEquivalent s (Feedback pre' _) <> NotEquivalent _ (Feedback _ post') = NotEquivalent s (Feedback pre' post')
 r                      <> _                       = r
 
 -- | Model type.
@@ -49,8 +61,8 @@ type Model = M.Map String ModelVal
 
 emptyModel :: Model
 emptyModel = M.empty
-emptyFeedback :: (Feedback, Feedback)
-emptyFeedback = (NoFeedback, NoFeedback)
+-- emptyFeedback :: (Feedback, Feedback)
+-- emptyFeedback = (NoFeedback, NoFeedback)
 
 -- | Pretty-printing.
 instance Show ModelVal where

src/Server.hs

+{-# OPTIONS_GHC -fno-warn-orphans #-}
 {-# LANGUAGE DataKinds             #-}
 {-# LANGUAGE DeriveGeneric         #-}
 {-# LANGUAGE FlexibleInstances     #-}
@@ -8,18 +9,17 @@
 {-# LANGUAGE TypeFamilies          #-}
 {-# LANGUAGE TypeOperators         #-}
 {-# LANGUAGE UndecidableInstances  #-}
-{-# OPTIONS_GHC -fno-warn-orphans #-}
 module Server (runApi) where
 
-import Control.Monad.Trans (liftIO)
-import Data.Aeson
-import Data.ByteString.Lazy (ByteString)
-import Data.List.Split (splitOn)
-import qualified Data.Map as Map
-import Data.Proxy
-import Data.Text.Lazy (pack)
-import Data.Text.Lazy.Encoding (encodeUtf8)
-import Data.Vector (fromList)
+import           Control.Monad.Trans     (liftIO)
+import           Data.Aeson
+import           Data.ByteString.Lazy    (ByteString)
+import           Data.List.Split         (splitOn)
+import qualified Data.Map                as Map
+import           Data.Proxy
+import           Data.Text.Lazy          (pack)
+import           Data.Text.Lazy.Encoding (encodeUtf8)
+import           Data.Vector             (fromList)
 
 import GHC.Generics
 import System.IO
@@ -30,11 +30,11 @@ import Network.Wai.Handler.Warp
 import Servant
 import Servant.Docs
 
-import Data.Swagger hiding (port)
+import Data.Swagger       hiding (port)
 import Servant.Swagger
 import Servant.Swagger.UI
 
-import API (Mode (..), ParseMode (..), compareSpec)
+import API   (Mode (..), ParseMode (..), compareSpec)
 import Model
 
 -- | Data types.
@@ -52,7 +52,7 @@ data ApiResponse = ApiResponse
   { responseType :: ApiResponseType
   , model        :: Maybe Model
   , err          :: Maybe String
-  , feedback     :: Maybe (Feedback, Feedback)
+  , feedback     :: Maybe Feedback
   }
   deriving (Eq, Show, Generic)
 instance ToJSON Feedback
@@ -65,6 +65,7 @@ instance ToJSON ModelVal where
   toJSON (ManyVal vs) = Array $ fromList $ map toJSON vs
 
 -- | Default API response.
+defResp :: ApiResponse
 defResp = ApiResponse { responseType = Undef
                       , model = Nothing
                       , err = Nothing
@@ -118,7 +119,7 @@ instance ToSample ApiResponse where
       , ("i", IntVal 10)
       ]
     , err = Nothing
-    , feedback = Just (NoFeedback, Stronger)
+    , feedback = Just $ Feedback (True, True, False, True) (False, True, True, False)
     }
 
 docsBS :: ByteString

test/TEquivalenceClasses.hs

@@ -17,10 +17,10 @@ testEquiv :: Response -> String -> String -> String -> Assertion
 testEquiv b src s s' = do
   res <- hSilence [stdout, stderr] $ compareSpec Debug File (src, s) (src, s')
   (case res of
-    NotEquivalent _ _ -> NotEquivalent emptyModel emptyFeedback
+    NotEquivalent _ _ -> NotEquivalent emptyModel defFeedback'
     x               -> x) @?= b
 (.==) = testEquiv Equivalent
-(.!=) = testEquiv $ NotEquivalent emptyModel emptyFeedback
+(.!=) = testEquiv $ NotEquivalent emptyModel defFeedback'
 
 genEquivTests edslSrc =
   let methodIds = unsafePerformIO (hSilence [stdout, stderr] $ parseMethodIds edslSrc)

test/TExamples.hs

@@ -13,10 +13,10 @@ testEquiv :: Response -> String -> String -> Assertion
 testEquiv b s s' = do
   res <- hSilence [stdout, stderr] $ compareSpec Release File (src, s) (src, s')
   (case res of
-    NotEquivalent _ _ -> NotEquivalent emptyModel emptyFeedback
+    NotEquivalent _ _ -> NotEquivalent emptyModel defFeedback'
     x                 -> x) @?= b
 (.==) = testEquiv Equivalent
-(.!=) = testEquiv $ NotEquivalent emptyModel emptyFeedback
+(.!=) = testEquiv $ NotEquivalent emptyModel defFeedback'
 (.??) = testEquiv Timeout
 
 examples =

test/TFeedback.hs

@@ -16,12 +16,13 @@ testEquiv b s s' = do
   (case res of
     NotEquivalent _ f -> NotEquivalent emptyModel f
     x                 -> x) @?= b
-(!!=) s s' f = testEquiv (NotEquivalent emptyModel (f, NoFeedback)) s s'
+(!!=) s s' f = testEquiv (NotEquivalent emptyModel (Feedback f defFeedback)) s s'
 
 feedbackTests =
-  [ ("true /\\ x:int == 1" !!= "false \\/ x:int >= 1") Stronger
-  , ("true /\\ x:int >= 1" !!= "false \\/ x:int == 1") Weaker
-  , ("x:int == 1 /\\ y:int == 1" !!= "x:int == 2 /\\ y:int == 1") NoFeedback
-  , ("x:[int][0] != 0 /\\ x:[int][1] != 0"
-      !!= "x:[int][0] != 0 \\/ x:[int][1] != 0") Stronger
+  [ ("true /\\ x:int == 1" !!= "false \\/ x:int >= 1") (True, False, True, True)
+  , ("true /\\ x:int >= 1" !!= "false \\/ x:int == 1") (True, True, False, True)
+  , ("x:int == 1 /\\ y:int == 1" !!= "x:int == 2 /\\ y:int == 1")
+      (False, True, True, True)
+  , ("x:[int][0] != 0 /\\ x:[int][1] != 0" !!= "x:[int][0] != 0 \\/ x:[int][1] != 0")
+      (True, False, True, True)
   ]