suzanne.soy/tock-mirror
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fixed a bug where the non-pruned version of the inequalities were being used in fmElimination; the Omega Test now functions properly

Browse Source
This commit is contained in:
Neil Brown 2008-01-09 17:14:15 +00:00
parent 524275cd9f
commit 26bd792e61
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
transformations/ArrayUsageCheck.hs
View File

@ -596,20 +596,20 @@ fmElimination vm ineq = fmElimination' vm (presentItems ineq) ineq
case listToMaybe $ filter (flip isExactProjection ineqsPruned) indexes of
-- If there is an exact projection (real shadow = dark shadow), eliminate that
-- variable, and therefore just recurse to process this shadow:
Just ex -> fmElimination' vm' (indexes \\ [ex]) (getRealShadow ex ineqs)
Just ex -> fmElimination' vm' (indexes \\ [ex]) (getRealShadow ex ineqsPruned)
Nothing ->
-- Otherwise, check the real shadow first:
case fmElimination' vm' ixs (getRealShadow ix ineqs) of
case fmElimination' vm' ixs (getRealShadow ix ineqsPruned) of
-- No solution to the real shadow means no solution to the problem:
Nothing -> Nothing
-- Check the dark shadow:
Just vm'' -> case fmElimination' vm'' ixs (getDarkShadow ix ineqs) of
Just vm'' -> case fmElimination' vm'' ixs (getDarkShadow ix ineqsPruned) of
-- Solution to the dark shadow means there is a solution to the problem:
Just vm''' -> return vm'''
-- Solution to real but not to dark; we must brute force the problem.
-- If we find any solutions during the brute-forcing, we have our solution.
-- Otherwise there is no solution
Nothing -> listToMaybe $ mapMaybe (uncurry $ solveProblem' vm'') $ getBruteForceProblems ix ineqs
Nothing -> listToMaybe $ mapMaybe (uncurry $ solveProblem' vm'') $ getBruteForceProblems ix ineqsPruned
-- Prunes the inequalities. If any equalities arise, those are processed, so
-- that the return is only inequalities