Permalink
Browse files

Compute intervals based on a model

  • Loading branch information...
1 parent 43b4678 commit d954d92807386e9916f5f1d23945aca6cb4bc264 @yav committed Nov 8, 2013
Showing with 65 additions and 4 deletions.
  1. +65 −4 src/Data/Integer/SAT.hs
View
@@ -15,12 +15,14 @@ module Data.Integer.SAT
, assert
, Prop(..)
, Expr(..)
+ , BoundType(..)
+ , getExprBound
) where
import Data.IntMap (IntMap)
import qualified Data.IntMap as Map
import Data.List(partition)
-import Data.Maybe(maybeToList,fromMaybe)
+import Data.Maybe(maybeToList,fromMaybe,mapMaybe)
import Control.Applicative(Applicative(..), (<$>))
import Control.Monad(liftM,ap,MonadPlus(..),msum,guard)
import Text.PrettyPrint(Doc,(<+>), (<>), integer, hsep, text)
@@ -31,12 +33,12 @@ infix 4 :==, :/=, :<, :<=, :>, :>=
infixl 6 :+, :-
infixl 7 :*
-
--------------------------------------------------------------------------------
-- Solver interface
-- | A collection of propositions.
newtype PropSet = State (Answer RW)
+ deriving Show
-- | An empty collection of propositions.
noProps :: PropSet
@@ -57,6 +59,17 @@ checkSat (State m) = go m
go (One rw) = Just $ filter ((>= 0) . fst) $ iModel $ inerts rw
go (Choice m1 m2) = mplus (go m1) (go m2)
+-- | Computes bounds on the expression that are compatible with the model.
+-- Returns `Nothing` if the bound is not known.
+getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer
+getExprBound bt e (State s) =
+ do let S m = expr e
+ check (t,s1) = iTermBound bt t (inerts s1)
+ bs <- mapM check $ toList $ s >>= m
+ case bs of
+ [] -> Nothing
+ _ -> Just (maximum bs)
+
-- | The type of proposition.
data Prop = PTrue
@@ -204,7 +217,7 @@ ctLt t1 t2 = t1 |-| t2
ctEq :: Term -> Term -> Term
ctEq t1 t2 = t1 |-| t2
-data Bound = Bound Integer Term
+data Bound = Bound Integer Term -- ^ The integer is strictly positive
deriving Show
data BoundType = Lower | Upper
@@ -308,6 +321,46 @@ iPickBounded bt bs = go bs Nothing
in if r == 0 then q - 1 else q
+-- | The largest (resp. least) upper (resp. lower) bound on a term
+-- that will satisfy the model
+iTermBound :: BoundType -> Term -> Inerts -> Maybe Integer
+iTermBound bt (T k xs) is = do ks <- mapM summand (Map.toList xs)
+ return $ sum $ k : ks
+ where
+ summand (x,c) = fmap (c *) (iVarBound (newBt c) x is)
+ newBt c = if c > 0 then bt else case bt of
+ Lower -> Upper
+ Upper -> Lower
+
+
+-- | The largest (resp. least) upper (resp. lower) bound on a variable
+-- that will satisfy the model.
+iVarBound :: BoundType -> Name -> Inerts -> Maybe Integer
+iVarBound bt x is
+ | Just t <- Map.lookup x (solved is) = iTermBound bt t is
+
+iVarBound bt x is =
+ do both <- Map.lookup x (bounds is)
+ case mapMaybe fromBound (chooseBounds both) of
+ [] -> Nothing
+ bs -> return (combineBounds bs)
+ where
+ fromBound (Bound c t) = fmap (scaleBound c) (iTermBound bt t is)
+
+ combineBounds = case bt of
+ Upper -> minimum
+ Lower -> maximum
+
+ chooseBounds = case bt of
+ Upper -> snd
+ Lower -> fst
+
+ scaleBound c b = case bt of
+ Upper -> div (b-1) c
+ Lower -> div b c + 1
+
+
+
iModel :: Inerts -> [(Name,Integer)]
iModel i = goBounds [] (bounds i)
where
@@ -453,6 +506,14 @@ which is covered by the dark shadow.
data Answer a = None | One a | Choice (Answer a) (Answer a)
deriving Show
+toList :: Answer a -> [a]
+toList a = go a []
+ where
+ go (Choice xs ys) zs = go xs (go ys zs)
+ go (One x) xs = x : xs
+ go None xs = xs
+
+
instance Monad Answer where
return a = One a
fail _ = None
@@ -617,7 +678,7 @@ tLetNums xs t = foldr (\(x,i) t1 -> tLetNum x i t1) t xs
instance Show Term where
- showsPrec c t = showsPrec c (ppTerm t)
+ showsPrec c t = showsPrec c (show (ppTerm t))
ppTerm :: Term -> Doc
ppTerm (T k m) =

0 comments on commit d954d92

Please sign in to comment.