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

@@ -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,
+-- | Given a list of replicators, and a set of background knowledge for each
--- checks if there are any solutions for a combination of the normal replicator
+-- access inside the replicator, checks if there are any solutions for a
--- constraints, and the given background knowledge.
+-- combination of the normal replicator constraints, and the given background
--- Returns Nothing if no solutions, a String with a counter-example if there are solutions
+-- knowledge (pairing each set against each other, applying one set to the replicator,
-findRepSolutions :: (CSMR m, MonadIO m) => [(A.Name, A.Replicator)] -> BK -> m (Maybe String)
+-- and the other to the mirror of the replicator).
-findRepSolutions reps bk = case makeEquations (addReps $ ParItems $ map (\x -> SeqItems [(bk, [x], [])]) $
+--
-          [A.ExprVariable (A.nameMeta n) $ A.Variable (A.nameMeta n) n
+-- Returns Nothing if no solutions, a String with a counter-example if there
-                      | (n, _) <- reps]) maxInt of
+-- 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