Skip to content
Browse files

Compute a model for an inert set.

  • Loading branch information...
1 parent f4be024 commit 1aad572c6edd14b7510d3340ca81c25a1e490e8e @yav committed Oct 29, 2013
Showing with 49 additions and 1 deletion.
  1. +41 −1 src/Data/Integer/Presburger/Omega.hs
  2. +8 −0 src/Data/Integer/Presburger/Term.hs
View
42 src/Data/Integer/Presburger/Omega.hs
@@ -5,7 +5,7 @@ import Data.Integer.Presburger.Term
import Data.IntMap (IntMap)
import qualified Data.IntMap as Map
import Data.List(partition)
-import Data.Maybe(maybeToList)
+import Data.Maybe(maybeToList,fromMaybe)
import Control.Applicative
import Control.Monad
@@ -159,6 +159,46 @@ iSolved x t i =
stay (Bound _ bnd) = not (tHasVar x bnd)
+-- 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
+ 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
+
+
+iModel :: Inerts -> [(Name,Integer)]
+iModel i = goBounds [] (bounds i)
+ where
+ goBounds su mp =
+ case Map.maxViewWithKey mp of
+ Nothing -> goEqs su $ Map.toList $ solved i
+ Just ((x,(lbs0,ubs0)), mp1) ->
+ let lbs = [ Bound c (tLetNums su t) | Bound c t <- lbs0 ]
+ ubs = [ Bound c (tLetNums su t) | Bound c t <- ubs0 ]
+ sln = fromMaybe 0
+ $ mplus (iPickBounded Lower lbs) (iPickBounded Upper ubs)
+ in goBounds ((x,sln) : su) mp1
+
+ goEqs su [] = su
+ goEqs su ((x,t) : more) =
+ let t1 = tLetNums su t
+ vs = tVarList t1
+ su1 = [ (v,0) | v <- vs ] ++ (x,tConstPart t1) : su
+ in goEqs su1 more
--------------------------------------------------------------------------------
View
8 src/Data/Integer/Presburger/Term.hs
@@ -23,6 +23,8 @@ module Data.Integer.Presburger.Term
, tLetNum
, tLetNums
, tVars
+ , tVarList
+ , tConstPart
) where
import qualified Data.IntMap as Map
@@ -150,6 +152,9 @@ isConst (T n m)
| Map.null m = Just n
| otherwise = Nothing
+tConstPart :: Term -> Integer
+tConstPart (T n _) = n
+
-- | Returns: @Just (a, b, x)@ if the term is the form: @a + b * x@
tIsOneVar :: Term -> Maybe (Integer, Integer, Name)
tIsOneVar (T a m) = case Map.toList m of
@@ -174,6 +179,9 @@ tGetSimpleCoeff (T a m) =
tVars :: Term -> IntSet
tVars (T _ m) = Map.keysSet m
+tVarList :: Term -> [Name]
+tVarList (T _ m) = Map.keys m
+
-- | Try to factor-out a common consant (> 1) from a term.
-- For example, @2 + 4x@ becomes @2 * (1 + 2x)@.

0 comments on commit 1aad572

Please sign in to comment.
Something went wrong with that request. Please try again.