close #15

src/SimpleFormulaChecker.hs

@@ -87,13 +87,18 @@ isEquivalent ast1' ast2' = evalZ3 z3
          return r
 
 -- Function that shows a human-readable model and also highlights potential inconsistencies.
+-- Sorry for the code, it is quite awful...
 showRelevantModel :: Z3Model -> IO ()
 showRelevantModel model = do
   putStrLn $ show $ M.toList modelClean
   mapM_ (putStrLn . prettyModelVal) $ fromKeys (consts ++ arrays)
-  where modelMap = M.fromList model
+  where modelMap :: M.Map String ModelVal
+        modelMap = M.fromList model
+        modelClean :: M.Map String ModelVal
         modelClean = M.filterWithKey (\k _ -> all (\e -> e /= '!') k) $ M.map modelCleanFunc modelMap
+        fromKeys :: [String] -> [(String, ModelVal)]
         fromKeys = map (\k -> let v = M.findWithDefault defaultArray k modelClean in (k, v))
+        defaultArray :: ModelVal
         defaultArray = ArrayFunc [InstElse (-1000000000000000)] -- nullTest2
         -- Pretty print the model value
         prettyModelVal :: (String, ModelVal) -> String
@@ -103,7 +108,9 @@ showRelevantModel model = do
             where (BoolVal aNull) = M.findWithDefault (BoolVal False) (k ++ "?null") modelClean
                   (IntVal aLength) = M.findWithDefault (IntVal (-1)) (k ++ "?length") modelClean
                   [InstElse elseVal] = filter (not . isInst) a
+                  arrKv :: [(Int, Int)]
                   arrKv = filter (\(k, v) -> v /= elseVal) (sort (map (\(InstInt k v) -> (k, v)) (filter isInst a)))
+                  isInst :: FuncInst -> Bool
                   isInst (InstInt _ v) = True
                   isInst _ = False
                   isValidArray :: Bool
@@ -111,10 +118,11 @@ showRelevantModel model = do
                       where minIndex = minimum indices
                             maxIndex = maximum indices
                             indices  = map fst arrKv
-                  -- TODO: this does not appear to be correct yet
-                  asdf = M.fromList arrKv
+                  arrMap :: M.Map Int Int
+                  arrMap = M.fromList arrKv
                   buildArray :: Int -> [Int]
-                  buildArray i = if aLength == 0 then [] else (M.findWithDefault elseVal i asdf : if i + 1 == aLength || i + 1 > 100 then [] else buildArray (i + 1))
+                  buildArray i = if aLength == 0 then [] else (M.findWithDefault elseVal i arrMap : if i + 1 == aLength || i + 1 > 100 then [] else buildArray (i + 1))
+                  final :: String
                   final = if aNull
                              then if (aLength /= -1) || (length arrKv /= 0)
                                      then "1: INVALID" -- nullTest1, nullTest3, nullTest4
@@ -130,9 +138,9 @@ showRelevantModel model = do
         modelCleanFunc (ArrayRef s) = let Just v = M.lookup s modelMap in v
         modelCleanFunc (ArrayAsConst n) = ArrayFunc [InstElse (cropInt32 n)]
         modelCleanFunc (ArrayFunc v) = ArrayFunc (map funcInstClean v)
-        funcInstClean :: FuncInst -> FuncInst
-        funcInstClean (InstInt k v) = InstInt (cropInt32 k) (cropInt32 v)
-        funcInstClean (InstElse v) = InstElse (cropInt32 v)
+            where funcInstClean :: FuncInst -> FuncInst
+                  funcInstClean (InstInt k v) = InstInt (cropInt32 k) (cropInt32 v)
+                  funcInstClean (InstElse v) = InstElse (cropInt32 v)
         -- Crop an Integer to an Int32
         cropInt32 :: Int -> Int
         cropInt32 n = fromIntegral (fromIntegral n :: Int32) :: Int
@@ -181,7 +189,7 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
     (result, model) <- isEquivalent ast1 ast2
     case result of
        Unsat -> putStrLn "formulas are equivalent!"
-       Undef -> putStrLn "unable to decide the satisfiablity (TODO: use QuickCheck)"
+       Undef -> putStrLn "unable to decide the satisfiablity (TODO: use QuickCheck)" -- this should happen on timeout, but the Z3 library does not function properly...
        Sat   -> do
                 putStrLn "formulas are NOT equivalent, model:"
                 case model of
@@ -226,4 +234,4 @@ sort2 = compareSpec (edslSrc, "sorted1") (edslSrc, "sorted2")
 sort3 = compareSpec (edslSrc, "sorted1") (edslSrc, "sorted3")
 sort4 = compareSpec (edslSrc, "test2") (edslSrc, "sorted3")
 sort5 = compareSpec (edslSrc, "sorted3") (edslSrc, "sorted4")
-sort6 = compareSpec (edslSrc, "sorted1") (edslSrc, "sorted4") -- does not terminate
\ No newline at end of file
+sort6 = compareSpec (edslSrc, "sorted1") (edslSrc, "sorted4") -- does not terminate (TODO: should time out, but this does not work)
\ No newline at end of file