feat(ldfi2): add iff formula and clean up z3_same

src/ldfi2/src/Ldfi/Prop.hs

@@ -18,6 +18,7 @@ data FormulaF var
   | And [FormulaF var]
   | Or [FormulaF var]
   | Neg (FormulaF var)
+  | FormulaF var :<-> FormulaF var
   | TT
   | FF
   | Var var
@@ -32,13 +33,14 @@ genFormula env 0 = QC.oneof
   , Var <$> QC.elements env
   ]
 genFormula env size =
-  QC.oneof [ genFormula env 0
-           , Neg <$> genFormula env (size - 1)
-           , QC.elements [(:&&), (:||)] <*> genFormula env (size `div` 2) <*> genFormula env (size `div` 2)
-           , do
-               n <- QC.choose (0, size `div` 2)
-               QC.elements [And, Or] <*> QC.vectorOf n (genFormula env (size `div` 4))
-           ]
+  QC.oneof
+    [ genFormula env 0
+    , Neg <$> genFormula env (size - 1)
+    , QC.elements [(:&&), (:||)] <*> genFormula env (size `div` 2) <*> genFormula env (size `div` 2)
+    , do
+        n <- QC.choose (0, size `div` 2)
+        QC.elements [And, Or] <*> QC.vectorOf n (genFormula env (size `div` 4))
+    ]
 
 instance QC.Arbitrary v => QC.Arbitrary (FormulaF v) where
   arbitrary = do
@@ -58,6 +60,7 @@ simplify1 (And [])    = TT
 simplify1 (And [f])   = f
 simplify1 (And fs)    = And (map simplify1 fs)
 simplify1 (Neg f)     = Neg (simplify1 f)
+simplify1 (l :<-> r)  = simplify1 l :<-> simplify1 r
 simplify1 f           = f
 
 -- simplify (TT :&& r)     = simplify r

src/ldfi2/src/Ldfi/Sat.hs

@@ -3,6 +3,7 @@ module Ldfi.Sat where
 import Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
+import GHC.Stack (HasCallStack)
 import Z3.Monad
 
 import Ldfi.Prop
@@ -30,6 +31,10 @@ translate env f0 = case f0 of
     fs' <- mapM (translate env) fs
     mkOr fs'
   Neg f -> mkNot =<< translate env f
+  l :<-> r -> do
+    l' <- translate env l
+    r' <- translate env r
+    mkIff l' r'
   TT    -> mkTrue
   FF    -> mkFalse
   Var v -> return (env Map.! v)
@@ -41,7 +46,7 @@ oldSolve m =  do
   (result, _mModel) <- getModel
   return result
 
-z3Solve :: Formula -> IO Solution
+z3Solve :: HasCallStack => Formula -> IO Solution
 z3Solve f = evalZ3 $ do
   let vs = Set.toList (getVars f)
   vs' <- mapM mkFreshBoolVar vs

src/ldfi2/src/Ldfi/Solver.hs

@@ -8,6 +8,7 @@ import Ldfi.Prop
 -- * Solver
 
 data Solution = NoSolution | Solution (Map String Bool)
+  deriving Show
 
 data Solver m = Solver
   { solve :: Formula -> m Solution }

src/ldfi2/test/LdfiTest.hs

@@ -1,16 +1,14 @@
 module LdfiTest where
 
-import qualified Data.Map as Map
-import qualified Data.Set as Set
 import Test.HUnit
 import qualified Test.QuickCheck as QC
-import Z3.Monad
 
 import Ldfi
 import Ldfi.FailureSpec
 import Ldfi.Prop
 import Ldfi.Sat
 import Ldfi.Traces
+import Ldfi.Solver
 
 ------------------------------------------------------------------------
 
@@ -21,25 +19,15 @@ emptyFailureSpec = FailureSpec
   , endOfTime = 0
   }
 
-data WasSame = Same | NotSame (Maybe String) | Dunno
+data WasSame = Same | NotSame (Maybe String)
   deriving Show
 
 z3_same :: Formula -> Formula -> IO WasSame
 z3_same l r = do
-  result <- evalZ3 . oldSolve $ do
-    -- we could also check that the variables are the same.. but then
-    -- we would also need to check we don't have silly things like (x \/ ~x)
-    let vs = Set.toList (getVars l `Set.union` getVars r)
-    vs' <- mapM mkFreshBoolVar vs
-    let env = Map.fromList (zip vs vs')
-    lf <- translate env l
-    rf <- translate env r
-    mkNot =<< mkIff lf rf
-  pure $ case result of
-    Sat  -> NotSame Nothing -- TODO(stevan): Maybe we can give a better
-                            -- counterexample here?
-    Unsat  -> Same
-    Undef -> Dunno
+  sol <- z3Solve (Neg (l :<-> r))
+  pure $ case sol of
+    Solution assignment -> NotSame (Just (show assignment))
+    NoSolution          -> Same
 
 shouldBe :: Formula -> Formula -> Assertion
 shouldBe actual expected = do
@@ -49,8 +37,6 @@ shouldBe actual expected = do
     NotSame modString -> assertFailure msg
       where msg = "expected: " ++ show expected ++ "\n but got: " ++ show actual ++
               "\n model: " ++ show modString
-    Dunno -> assertFailure msg
-      where msg = "z3 returns Undef"
 
 ------------------------------------------------------------------------
 -- Sanity checks for z3_same