presburger 1.0 → 1.1

raw patch · 2 files changed

+13/−18 lines, 2 files

Files

• presburger.cabal +1/−1
• src/Data/Integer/SAT.hs +12/−17

@@ -1,5 +1,5 @@ Name:           presburger-Version:        1.0+Version:        1.1 License:        BSD3 License-file:   LICENSE Author:         Iavor S. Diatchki

@@ -261,7 +261,7 @@     -- Each bound @(c,t)@ in the second list asserts that @c * x < t@    , solved :: NameMap Term-    -- ^ Definitions for resolved variabless.+    -- ^ Definitions for resolved variables.     -- These form an idempotent substitution.   } deriving Show @@ -283,7 +283,7 @@ -- --    * Assumes substitution has already been applied. -----    * The kciked-out constraints are NOT rewritten, this happens+--    * The kicked-out constraints are NOT rewritten, this happens --      when they get inserted in the work queue.  iSolved :: Name -> Term -> Inerts -> ([Term], Inerts)@@ -324,22 +324,17 @@ -- Given a list of lower (resp. upper) bounds, compute the least (resp. largest) -- value that satisfies them all. iPickBounded :: BoundType -> [Bound] -> Maybe Integer-iPickBounded bt bs = go bs Nothing+iPickBounded _ [] = Nothing+iPickBounded bt bs =+  do xs <- mapM (normBound bt) bs+     return $ case bt of+                Lower -> maximum xs + 1+                Upper -> minimum xs - 1   where-  go [] mb = mb-  go (Bound c t : more) mb =-    do k <- isConst t-       let t1 = maybe k (combine k) mb-       go more $ Just $ compute t1 c--  combine = case bt of-              Lower -> max-              Upper -> min--  compute v c = case bt of-                  Lower -> div v c + 1-                  Upper -> let (q,r) = divMod v c-                           in if r == 0 then q - 1 else q+  normBound Lower (Bound c t) = do k <- isConst t+                                   return (div (k + c - 1) c)+  normBound Upper (Bound c t) = do k <- isConst t+                                   return (div k c)   -- | The largest (resp. least) upper (resp. lower) bound on a term