From 3701154a1b238b7d71a0e0189e3baabb4ac128b7 Mon Sep 17 00:00:00 2001
From: Neil Brown <neil@twistedsquare.com>
Date: Sat, 7 Feb 2009 19:07:10 +0000
Subject: [PATCH] Fixed findRepSolutions to work properly

Previously, it was taking one lot of BK at a time, then checking to see if i and i' could overlap (i.e. i and i' were the array indexes to check), which of course they never could.  It now takes a list of BK to pair up against each other, and asks if 0 can overlap with 0, which it can as long as there is a solution to the replicators.
---
 checks/ArrayUsageCheck.hs | 32 ++++++++++++++++++++++----------
 1 file changed, 22 insertions(+), 10 deletions(-)

diff --git a/checks/ArrayUsageCheck.hs b/checks/ArrayUsageCheck.hs
index 8629e16..f142563 100644
--- a/checks/ArrayUsageCheck.hs
+++ b/checks/ArrayUsageCheck.hs
@@ -58,19 +58,31 @@ import Utils
 type BK = [Map.Map Var [BackgroundKnowledge]]
 type BK' = [Map.Map Var (EqualityProblem, InequalityProblem)]
 
--- | Given a list of replicators, and some background knowledge,
--- checks if there are any solutions for a combination of the normal replicator
--- constraints, and the given background knowledge.
--- Returns Nothing if no solutions, a String with a counter-example if there are solutions
-findRepSolutions :: (CSMR m, MonadIO m) => [(A.Name, A.Replicator)] -> BK -> m (Maybe String)
-findRepSolutions reps bk = case makeEquations (addReps $ ParItems $ map (\x -> SeqItems [(bk, [x], [])]) $
-          [A.ExprVariable (A.nameMeta n) $ A.Variable (A.nameMeta n) n
-                      | (n, _) <- reps]) maxInt of
+-- | Given a list of replicators, and a set of background knowledge for each
+-- access inside the replicator, checks if there are any solutions for a
+-- combination of the normal replicator constraints, and the given background
+-- knowledge (pairing each set against each other, applying one set to the replicator,
+-- and the other to the mirror of the replicator).
+--
+-- Returns Nothing if no solutions, a String with a counter-example if there
+-- are solutions
+findRepSolutions :: (CSMR m, MonadIO m) => [(A.Name, A.Replicator)] -> [BK] -> m (Maybe String)
+findRepSolutions reps bks
+  -- To get the right comparison, we create a SeqItems with all the accesses
+  -- Because they are inside a PAR replicator, they will all get compared to each
+  -- other with one set of BK applied to i and one applied to i', but they will
+  -- never be compared to each other just with the constraints on i (which is not
+  -- what we are checking here).  We set the dummy array accesses to all be zero,
+  -- which means they can overlap -- but only if there is also a solution to the
+  -- replicator background knowledge, which is what this function is trying to
+  -- determine.
+  = case makeEquations (addReps $ SeqItems [(bk, [makeConstant emptyMeta 0], [])
+                                           | bk <- bks]) maxInt of
             Right problems -> do
               probs <- formatProblems [(vm, prob) | (_,vm,prob) <- problems]
               case mapMaybe solve problems of
                 [] -> return Nothing -- No solutions, safe
-                xs -> liftM (Just . concat) $ mapM format xs
+                xs -> liftM (Just . unlines) $ mapM format xs
             res -> error $ "Unexpected reachability result"
   where
     maxInt = makeConstant emptyMeta $ fromInteger $ toInteger (maxBound :: Int32)
@@ -144,7 +156,7 @@ checkArrayUsage (m,p) = mapM_ (checkIndexes m) $ Map.toList $
                      do sol <- formatSolution varMapping (getCounterEqs vm)
                         cx <- showCode (fst lx)
                         cy <- showCode (fst ly)
---                        liftIO $ putStrLn $ "Found solution for problem: " ++ prob
+--                        liftIO $ putStrLn $ "Found solution for problem: " ++ probs
 --                         ++ show p
 --                        liftIO $ putStrLn $ "Succeeded on problem: " ++ prob
 --                        allProbs <- concatMapM (\(_,_,p) -> formatProblem varMapping p >>* (++ "\n#\n")) problems