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

Changed the monad in the Omega Test equality stuff to StateT Maybe rather than State, and fixed some bugs in the Omega Test

Browse Source
This commit is contained in:
Neil Brown 2007-12-12 13:57:44 +00:00
parent e34ebc67ea
commit c46580fbda
1 changed files with 17 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
transformations/ArrayUsageCheck.hs
View File

@ -67,15 +67,15 @@ type EqualityProblem = [EqualityConstraintEquation]
type InequalityConstraintEquation = Array CoeffIndex Integer type InequalityConstraintEquation = Array CoeffIndex Integer
type InequalityProblem = [InequalityConstraintEquation] type InequalityProblem = [InequalityConstraintEquation]
type StIneq = State InequalityProblem type StIneq = StateT InequalityProblem Maybe
solveConstraints :: EqualityProblem -> InequalityProblem -> Maybe InequalityProblem solveConstraints :: EqualityProblem -> InequalityProblem -> Maybe InequalityProblem
solveConstraints p ineq solveConstraints p ineq
= case normalise p of = case normalise p of
Nothing -> Nothing Nothing -> Nothing
Just p' -> case (runState (solve p') ineq) of Just p' -> case (runStateT (solve p') ineq) of
(Nothing,_) -> Nothing Nothing -> Nothing
(_,s) -> Just s Just (_,s) -> Just s
where where
normalise :: EqualityProblem -> Maybe EqualityProblem normalise :: EqualityProblem -> Maybe EqualityProblem
normalise = mapM normalise' --Note the mapM; if any calls to normalise' fail, so will normalise normalise = mapM normalise' --Note the mapM; if any calls to normalise' fail, so will normalise
@ -84,12 +84,9 @@ solveConstraints p ineq
normalise' e = let g = foldl1 gcd (elems e) in normalise' e = let g = foldl1 gcd (elems e) in
if (((e ! 0) `mod` g) /= 0) then Nothing else Just $ amap (\x -> x `div` g) e if (((e ! 0) `mod` g) /= 0) then Nothing else Just $ amap (\x -> x `div` g) e
solve :: EqualityProblem -> StIneq (Maybe EqualityProblem) solve :: EqualityProblem -> StIneq EqualityProblem
solve [] = return $ Just [] solve [] = return []
solve p = do mp <- solveUnits p >>* (checkFalsifiable . removeRedundant) solve p = (solveUnits p >>* removeRedundant) >>= liftF checkFalsifiable >>= solveNext >>= solve
case mp of
Nothing -> return Nothing
Just p' -> solveNext p' >>= solve
checkForUnit :: EqualityConstraintEquation -> Maybe CoeffIndex checkForUnit :: EqualityConstraintEquation -> Maybe CoeffIndex
-- checkForUnit [_] = Nothing -- checkForUnit [_] = Nothing
@ -127,7 +124,7 @@ solveConstraints p ineq
negateOthers match (ind,val) = if match == ind then 0 else negate val negateOthers match (ind,val) = if match == ind then 0 else negate val
findSmallestAbsCoeff :: EqualityConstraintEquation -> CoeffIndex findSmallestAbsCoeff :: EqualityConstraintEquation -> CoeffIndex
findSmallestAbsCoeff = fst. minimumBy (cmpAbsSnd) . tail . assocs findSmallestAbsCoeff = fst. minimumBy (cmpAbsSnd) . filter ((/= 0) . snd) . tail . assocs
where where
cmpAbsSnd :: (a,Integer) -> (a,Integer) -> Ordering cmpAbsSnd :: (a,Integer) -> (a,Integer) -> Ordering
cmpAbsSnd (_,x) (_,y) = compare (abs x) (abs y) cmpAbsSnd (_,x) (_,y) = compare (abs x) (abs y)
@ -135,14 +132,20 @@ solveConstraints p ineq
solveNext :: EqualityProblem -> StIneq EqualityProblem solveNext :: EqualityProblem -> StIneq EqualityProblem
solveNext [] = return [] solveNext [] = return []
solveNext (e:es) = -- We transform the kth variable into sigma, effectively solveNext (e:es) = -- We transform the kth variable into sigma, effectively
-- So a_k becomes -|a_k|, and all other constraints are transformed appropriately -- So once we have x_k = ... (in terms of sigma) we add a_k * RHS
modify (map change) >> return (map change (e:es)) -- to all other equations, AFTER zeroing the a_k coefficient (so
-- that the multiple of sigma is added on properly)
modifyM_ (normalise . map alterEquation) >> (lift $ (normalise . map alterEquation) (e:es))
where where
change = changeAllButOneDifferent (k,-(abs a_k)) transform alterEquation :: EqualityConstraintEquation -> EqualityConstraintEquation
alterEquation eq = arrayZipWith (+) (eq // [(k,0)]) (amap (\x -> x * (eq ! k)) x_k_eq)
k = findSmallestAbsCoeff e k = findSmallestAbsCoeff e
a_k = e ! k a_k = e ! k
m = (abs a_k) + 1 m = (abs a_k) + 1
sign_a_k = signum a_k
x_k_eq = changeAllButOneDifferent (k,(- sign_a_k) * m) (\a_i -> sign_a_k * (a_i `mymod` m)) e
transform :: Integer -> Integer transform :: Integer -> Integer
transform a_i = (floordivplushalf a_i m) + (mymod a_i m) transform a_i = (floordivplushalf a_i m) + (mymod a_i m)