# yav/presburger

### Subversion checkout URL

You can clone with HTTPS or Subversion.

Remove old implementation.

```We may want to resurrect this later, as it supports arbitrary nesting
of quantifiers.```
commit b3aaf5bb93897fea4f054c720afa3042b977bc23 1 parent 40b33d9
authored
194 src/Data/Integer/Presburger.hs
 @@ -1,194 +0,0 @@ -{-# LANGUAGE Safe #-} -{-# LANGUAGE FlexibleInstances #-} -module Data.Integer.Presburger - ( Formula - , bool, true, false, (/\), (\/), (==>), (<==>), neg, ite, divides - , (|==|), (|/=|), (|<|), (|<=|), (|>|), (|>=|) - , letDivMod - , nat - , forAll, bForAll, exists, bExists - - , Term - , (|*|), tITE - - , isTrue - ) where - -import qualified Data.Integer.Presburger.Term as T -import qualified Data.Integer.Presburger.Formula as A -import qualified Data.Integer.Presburger.Exists as E - -infixr 1 ==> -infixr 2 \/ -infixr 3 /\ -infix 4 |==|, |/=|, |<|, |<=|, |>|, |>=| - --- | First-order formulas -data Formula = F Int A.Formula -- ^ The Int is the largest bound var in body - -instance Show Formula where - showsPrec p (F _ x) = showsPrec p x - -data Term = T T.Term - | ITE Formula Term Term - deriving Show -instance Num Term where - fromInteger n = T (fromInteger n) - (+) = tBin (+) - (-) = tBin (-) - (*) = tBin (*) - abs x = tITE (x |>=| 0) x (negate x) - signum x = tITE (x |<| 0) (-1) (tITE (x |>| 0) 1 0) - --- For lifting binary operations -tBin :: (T.Term -> T.Term -> T.Term) -> Term -> Term -> Term -tBin f (T x) (T y) = T (f x y) -tBin f (ITE p t1 t2) t = ITE p (tBin f t1 t) (tBin f t2 t) -tBin f t (ITE p t1 t2) = ITE p (tBin f t t1) (tBin f t t2) - --- | A constant formula. -bool :: Bool -> Formula -bool b = F 0 \$ A.fAtom \$ A.mkBool b - --- | A true statement. -true :: Formula -true = bool True - --- | A false statement. -false :: Formula -false = bool False - --- | Conjunction. -(/\) :: Formula -> Formula -> Formula -F x p /\ F y q = F (max x y) (A.fConn A.And p q) - --- | Disjunction. -(\/) :: Formula -> Formula -> Formula -F x p \/ F y q = F (max x y) (A.fConn A.Or p q) - --- | Implication. -(==>) :: Formula -> Formula -> Formula -p ==> q = neg p \/ q - -(<==>) :: Formula -> Formula -> Formula -p <==> q = (p ==> q) /\ (q ==> p) - --- | Negation. -neg :: Formula -> Formula -neg (F x fo) = F x (A.fNeg fo) - --- | If-then-else. -ite :: Formula -> Formula -> Formula -> Formula -ite p t e = (p /\ t) \/ (neg p /\ e) - --- | Multiple a term by a constant -(|*|) :: Integer -> Term -> Term -k |*| T t = T (k T.|*| t) -k |*| ITE f t1 t2 = ITE f (k |*| t1) (k |*| t2) - --- | If-then-else term -tITE :: Formula -> Term -> Term -> Term -tITE = ITE - --- | Assert that terms are the same. -(|==|) :: Term -> Term -> Formula -t1 |==| t2 = atom A.Eq t1 t2 - --- | Assert that the first term is strictly smaller. -(|<|) :: Term -> Term -> Formula -t1 |<| t2 = atom A.Lt t1 t2 - --- | Assert that the first term is smaller than or equal to the second one. -(|<=|) :: Term -> Term -> Formula -t1 |<=| t2 = atom A.Leq t1 t2 - --- | Assert that terms are different. -(|/=|) :: Term -> Term -> Formula -t1 |/=| t2 = neg (t1 |==| t2) - --- | Assert that the first term is strictly greater than the second. -(|>|) :: Term -> Term -> Formula -t1 |>| t2 = neg (t1 |<=| t2) - --- | Assert that the first term is greater than or equal to the second. -(|>=|) :: Term -> Term -> Formula -t1 |>=| t2 = neg (t1 |<| t2) - -atom :: A.PredS -> Term -> Term -> Formula -atom op (T t1) (T t2) = F 0 \$ A.fAtom \$ A.mkAtom A.Pos op lhs rhs - where (lhs,rhs) = T.tSplit (t2 - t1) -atom op (ITE f t1 t2) t = ite f (atom op t1 t) (atom op t2 t) -atom op t (ITE f t1 t2) = ite f (atom op t t1) (atom op t t2) - --- | Assert that the given integer divides the term. -divides :: Integer -> Term -> Formula -divides 0 t = t |==| 0 -divides m (T t) = F 0 \$ A.fAtom \$ A.mkDiv A.Pos (abs m) t -divides m (ITE f t1 t2) = ite f (divides m t1) (divides m t2) - -{- | Simluate division and reminder. -@letDivMod t m \$ \q r -> p@ asserts that when we divide @t@ by @m@ -we get quotiont @q@ and reminder @r@, and also `p` holds. -} - -letDivMod :: Term -> Integer -> (Term -> Term -> Formula) -> Formula -letDivMod t m p = exists \$ \q r -> - 0 |<=| r /\ r |<| fromInteger m /\ m |*| q + r |==| t /\ p q r - - -class Quantifiable t where - quantify :: ([Term] -> Formula -> Formula) -- This is used to tweak the - -- final formula to negate (forall) - -- and assertions about domain - -> t -> Formula - -instance Quantifiable Bool where - quantify f k = f [] (bool k) - -instance Quantifiable Formula where - quantify f k = f [] k - -instance Quantifiable t => Quantifiable (Term -> t) where - quantify f p = F name \$ E.exists [name] body - where - F mx body = quantify (\xs -> f (term:xs)) \$ p term - term = T \$ T.tVar name - name = 1 + mx - --- | WARNING: mixing evaluation with formula construction --- may lead to capture! --- > test = exists \$ \x -> bool \$ isTrue \$ forAll \$ \y -> x |==| y -exists :: Quantifiable formula => (Term -> formula) -> Formula -exists p = quantify (\_ -> id) p - -bExists :: Quantifiable formula => (Term -> Formula) -> - (Term -> formula) -> Formula -bExists dom p = quantify (\ts f -> foldr (/\) f (map dom ts)) p - -forAll :: Quantifiable formula => (Term -> formula) -> Formula -forAll p = neg \$ quantify (\_ -> neg) p - -bForAll :: Quantifiable formula => (Term -> Formula) - -> (Term -> formula) -> Formula -bForAll dom p = neg \$ quantify (\ts f -> neg \$ foldr (==>) f (map dom ts)) p - --- | Assert that a term is a natural number -nat :: Term -> Formula -nat x = 0 |<=| x - --------------------------------------------------------------------------------- -isTrue :: Formula -> Bool -isTrue (F _ fo0) = go fo0 - where - go fo = case A.isBool =<< A.isFAtom fo of - Just x -> x - Nothing -> - case A.isFConn fo of - Just (c, f1, f2) -> case c of - A.And -> go f1 && go f2 - A.Or -> go f1 || go f2 - _ -> error "Unexpected free variables in term" - - - - -
148 src/Data/Integer/Presburger/Div.hs
 @@ -1,148 +0,0 @@ -{-# LANGUAGE Safe #-} -{-# LANGUAGE BangPatterns #-} -module Data.Integer.Presburger.Div (Solution, DivCt, solve, instTerm) where - -import Data.Integer.Presburger.Term -import Data.List(partition) - -{- | The extended Euclid's algorithm. -It computes the GCD of two numbres as a linear combination of the inputs. -If @gcd a b = (d, s, t)@, then @d@ is the GCD of a and b, -and @d = s * a + t * b@. -} -gcdE :: Integer -> Integer -> (Integer, Integer, Integer) -gcdE u v = let (d,p,q) = go 1 0 0 1 (abs u) (abs v) - in (d, signum u * p, signum v * q) - - where - go !s2 !s1 !t2 !t1 !a !b - | b == 0 = (a, s2, t2) - | otherwise = let (q,r) = divMod a b - in go s1 (next q s2 s1) t1 (next q t2 t1) b r - - next q a2 a1 = a2 - q * a1 - - --- | A solution assigns value to the variables in such a way that --- all constraints are satisified. -type Solution = [ (Name,Integer) ] - --- | A divisibility constraint. -type DivCt = (Integer, Term) - -{- | Given a bunch of upper bounds on some variables, and a collection -of divisibilty constraints, compute the possible values for the variables. -We are only interested in values between 1 and the upper bound (inclusive). -} - -solve :: [(Name, Integer)] -> [DivCt] -> [[(Name, Integer)]] -solve xs cs = solve' xs cs - - -solve' :: [(Name, Integer)] -> [DivCt] -> [[(Name, Integer)]] -solve' vs [] = go vs - where - go ((x,u) : rest) = [ (x,v) : su | su <- go rest, v <- [ 1 .. u ] ] - go [] = [ [] ] - -solve' [] cs - | all ok cs = [ [] ] - | otherwise = [] - where - ok (m,t) = let Just b = isConst t - in mod b m == 0 - -solve' ((x,u) : vars) cs - | null cs_this = [ (x,v) : su | su <- solve' vars cs, v <- [ 1 .. u ] ] - | otherwise = [ (x,v) : su | su <- solve' vars rest, v <- soln su ] - where - (cs_this, cs_more) = partition ((/= 0) . tCoeff x . snd) cs - - ((m,t),rest0) = joinCts x cs_this - rest = cs_more ++ rest0 - - soln su = let (a,t1) = tSplitVar x (instTerm su t) - Just b = isConst t1 - in solveDiv u m a b - - - -instTerm :: Solution -> Term -> Term -instTerm [] ty = ty -instTerm ((y,n) : more) ty = instTerm more (tLetNum y n ty) - -{- | Join a (non-empty) list of constraints into a single constraint -involvong the variable, and a bunch of other constraints that do not. -} -joinCts :: Name -> [DivCt] -> (DivCt, [DivCt]) -joinCts x cs = go cs [] - where - go (c1 : c2 : more) others = let (cX, other) = joinCts2 x c1 c2 - in go (cX : more) (other : others) - go [c1] others = (c1, others) - go _ _ = error "JoinCts: []" - - -{- Given two constraints involving a variable, @x@, combine them into a -single constraint on that variable and another one that does not mention it. - -The first component of the result mentions @x@ but the second does not. --} -joinCts2 :: Name -> DivCt -> DivCt -> (DivCt, DivCt) -joinCts2 x (m, t1) (n, t2) = - let (a,b) = tSplitVar x t1 - (a',b') = tSplitVar x t2 - (d,p,q) = gcdE (a * n) (a' * m) - in ( ( m * n, d |*| tVar x + (p * n) |*| b + (q * m) |*| b' ) - , ( d, a' |*| b - a |*| b' ) - ) - - - -{- | The solutions for @m | (a * x + b)@, where @x `elem` [ 1 .. u ]@. -We assume that @m > 0@. - -The solutions are of the form: - -> do let (d,p,_) = gcdE a m -> guard (mod b d == 0) -> [ (-p) * div b d + t * div m d | t <- all_integers ] - -Note the @div m d@ is always positive, so we start from an initial -value computed from the lower bound, 1, and then keep incrementing -until we exceed the upper bound. --} -solveDiv :: Integer -> Integer -> Integer -> Integer -> [Integer] -solveDiv u m a b - | d == 0 = error ("SOLVEDIV 0: " ++ show (m,a,b)) - | r1 == 0 = takeWhile (<= u) \$ iterate (step +) \$ t0 * step - extra - | otherwise = [] - where - (d,p,_) = gcdE a m - (k1,r1) = divMod b d - step = div m d - extra = p * k1 - t0 = case divMod (1 + extra) step of - (q,r) -> if r == 0 then q else q + 1 - -_checkSolveDiv :: Integer -> Integer -> Integer -> Integer -> - Maybe ([Integer],[Integer]) -_checkSolveDiv u m a b = - if proposed == correct then Nothing else Just (correct,proposed) - where - correct = [ x | x <- [ 1 .. u ], (a * x + b) `mod` m == 0 ] - proposed = solveDiv u m a b - - - -_checkSolve :: [(Name,Integer)] -> [DivCt] -> Bool -_checkSolve xs cts = all valid slns && all (`elem` slns) allSlns - where - slns = solve xs cts - - valid sln = all (checkCt sln) cts - - checkCt su (m,t) = case isConst (instTerm su t) of - Just k | mod k m == 0 -> True - _ -> False - - allSlns = filter valid (solve xs []) - -
379 src/Data/Integer/Presburger/Exists.hs
 @@ -1,379 +0,0 @@ -{-# LANGUAGE Safe #-} -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE ViewPatterns #-} -{-# LANGUAGE PatternGuards #-} -module Data.Integer.Presburger.Exists(exists,existsTop) where - -import Data.Integer.Presburger.Term -import Data.Integer.Presburger.Formula -import Data.Integer.Presburger.Div(DivCt,solve) -import Data.Maybe(mapMaybe) -import Control.Monad(guard) - -{-| A type used while eliminating the quantifier for a variable. -The atoms are normalized so that the variable is on its own and has -coefficient 1. -} -data CtFo = Fo Formula -- ^ The varibale does not appear here - | CtConnF !Conn CtFo CtFo -- ^ Connective - | CtAtomF Ct -- ^ Normalized atom - -{-| Note that it is important that the 'Integer' in 'DivCt' is lazy, -so that we generate the constraint in a single pass. -} -data Ct = AtomCt Pol PredS Name Term -- ^ @x `op` t@ - | DivCt Pol Integer Name Term -- ^ @k | (x + t)@ - -{- | Construct formulas so that parts that do not mention the quantified -variabele float to the front. -} -ctConn :: Conn -> CtFo -> CtFo -> CtFo -ctConn c (Fo lf) (CtConnF c' (Fo rf) rest) - | c == c' = CtConnF c (Fo (fConn c lf rf)) rest - --- Quantifiers commute -ctConn c (CtConnF c' (Fo lf) rest) (Fo rf) - | c == c' = CtConnF c (Fo (fConn c lf rf)) rest - -ctConn c (CtConnF c' (Fo lf) rest) (CtConnF c'' (Fo rf) rest') - | c == c' && c == c'' = CtConnF c (Fo (fConn c lf rf)) - (CtConnF c rest rest') - -ctConn c lf rf@(Fo _) = CtConnF c rf lf - -ctConn c lf rf = CtConnF c lf rf - - - - --- | Collect all constraints in a constraint-formula. -getCts :: CtFo -> [Ct] -> [Ct] -getCts ctfo more = - case ctfo of - Fo _ -> more - CtConnF _ f1 f2 -> getCts f1 (getCts f2 more) - CtAtomF ct -> ct : more - --- | Convert a constraint-formula back into a normal formula. -ctAtoms :: (Ct -> Atom) -> CtFo -> Formula -ctAtoms f ctfo = - case ctfo of - Fo fo -> fo - CtConnF c f1 f2 -> fConn c (ctAtoms f f1) (ctAtoms f f2) - CtAtomF ct -> fAtom (f ct) - - - - -{- | Transform an atom so that the variable is on the LHS with coefficient 1. -If the variable is not mentioned in the atom, then it is left unchanged, -and we return 'Nothing'. Otherwise, we update the LCMs of coeffieicnts -and compute a normalized constraint. -} - --- 5 * x = 10 --- x = 2 - -aCt :: Name -> -- ^ Variable. - Integer -> -- ^ LCM of all coefficients for the variable (LAZY). - Integer -> -- ^ Partial LCM of coefficients. - Atom -> -- ^ Constraint to be normalizied. - Maybe (Integer, Ct) - -- ^ (Updated LCM of coefficients, constraint) - --- Does it occur on the left? -aCt x lcmCoeffFinal lcmCoeff (isAtom -> Just (pol,op,lhs,rhs)) - | k /= 0 = Just ( lcm k lcmCoeff - , AtomCt pol op x (div lcmCoeffFinal k |*| (rhs - lRest)) - ) - where - (k, lRest) = tSplitVar x lhs - --- Does it occur on the right? -aCt x lcmCoeffFinal lcmCoeff (isAtom -> Just (pol,op,lhs,rhs)) - | k /= 0 = Just ( lcm k lcmCoeff - , AtomCt newP newOp x (div lcmCoeffFinal k |*| (lhs - rRest)) - ) - where - (k, rRest) = tSplitVar x rhs - - -- Because we are moving the variable to the LHS, we need to update - -- the operations. - (newP,newOp) = case pol of - Pos -> - case op of - Eq -> (Pos,Eq) -- same - Lt -> (Neg,Leq) -- < becomes > - Leq -> (Neg,Lt) -- <= becomes >= - Neg -> - case op of - Eq -> (Neg,Eq) -- same - Lt -> (Pos,Leq) -- >= becomes <= - Leq -> (Pos,Lt) -- > becomes < - --- Does it occur in a divisibility constraint? --- m | (k * x + t) <=> abs (sc * m) | (sc * k * x + sc * t) --- where sc * k = lcmCoeffFinal -aCt x lcmCoeffFinal lcmCoeff (isDiv -> Just (p,m,t)) - | k /= 0 = let sc = div lcmCoeffFinal k - m1 = abs (m * sc) - in Just ( lcm lcmCoeff k - , DivCt p m1 x (sc |*| rest) - ) - where (k,rest) = tSplitVar x t - --- It does not occur anywhere. -aCt _ _ _ _ = Nothing - - -{-| Normalize a formula with respect to a particular variable. -In the resulting formula, the variable (technically, a new variable with -the same name) has coefficient 1. -Example: @2x > 5 --> x > 10@ - -As a result we return: - * the LCM of all coefficients of the variables, - * Parts of the formula that do not mention the variable are - tagged with 'Fo'. --} -aCts :: Name -> Formula -> (Integer, CtFo) -aCts x form = ( lcmCoeffFinal - , ctConn And foFinal (CtAtomF \$ DivCt Pos lcmCoeffFinal x 0) - ) - where - (lcmCoeffFinal,foFinal) = go True 1 form - - go _ lcmCoeff f - | Just a <- isFAtom f = - case aCt x lcmCoeffFinal lcmCoeff a of -- RECURSION: cf lcmCoeffFinal - Just (lcmCoeff', ct) -> (lcmCoeff', CtAtomF ct) - Nothing -> (lcmCoeff, Fo f) - - go _ lcmCoeff f - | ~(Just (c,l,r)) <- isFConn f = - case go (c == Or) lcmCoeff l of - (lcmCoeff1, l') -> - case go (c == Or) lcmCoeff1 r of - (lcmCoeff2, r') -> - case (l',r') of - (Fo _,Fo _) -> (lcmCoeff, Fo f) - _ -> (lcmCoeff2, ctConn c l' r') - - -computeDelta :: CtFo -> (Integer, CtFo) -computeDelta = go True 1 - where - - {- The boolean paramter to 'go' indicates if we should try the equality - optimization. We implement this in `tryEqOpt` which flattens - a conjunction and looks for equalities. If we don't find any equalities, - we go back to the `go` function, but now we disable the optimization, - to avoid an infinite loop. The optimization is autmoatically re-enabled - when we go under a disjunction. - -} - - - go opt !lcmDiv fo = - case fo of - CtAtomF (DivCt _ m _ _) -> (lcm m lcmDiv, fo) - CtConnF And f1 f2 | opt -> tryEqOpt lcmDiv f1 [f2] [] - CtConnF c f1 f2 -> let (lcmDiv1, f1') = go (c == Or) lcmDiv f1 - (lcmDiv2, f2') = go (c == Or) lcmDiv1 f2 - - in (lcmDiv2, ctConn c f1' f2') - Fo _ -> (lcmDiv, fo) - CtAtomF _ -> (lcmDiv, fo) - - {- The Equality Optmization - - We look for pattrens of the form: `x = t /\ P`. - When we spot this pattern, we can continue with: `x = t /\ P (t/x)`. - - The benfit of this is that now `P` does not mention `x`, which results - in less work when eliminating quantifiers (e.g., `lcmDiv` will be smaller). -} - - tryEqOpt d fo@(CtAtomF (AtomCt Pos Eq _ t)) todo done = - (d, case todo ++ done of - [] -> fo - more -> CtConnF And (Fo \$ foldr1 (fConn And) - (map (addDef t) more)) fo) - - tryEqOpt d (CtConnF And f1 f2) todo done = tryEqOpt d f1 (f2 : todo) done - tryEqOpt d f (f1 : todo) done = tryEqOpt d f1 todo (f : done) - tryEqOpt d f [] done = go False d (foldr (CtConnF And) f done) - - addDef t ctfo = ctAtoms (letAtom t) ctfo - --- | Given some constraints, collect the upper/lower bound restrictions on --- them. We have a strategy that can use either the lower bounds or the --- upper bounds. However, we need to perform a check for each separate --- bound, so we are interested in the shorter list. This is what the sum --- is for: 'Left': there were fewer lower bounds, 'Right': fewer upper bounds -getBounds :: [Ct] -> Either [Term] [Term] -getBounds = go (0::Int) [] [] - where - go !d !ls !us (AtomCt pol op _ rhs : more) = - case (pol,op) of - (Pos,Lt ) -> go (d+1) ls (rhs : us) more - (Neg,Leq) -> go (d-1) (rhs : ls) us more - (Pos,Leq) -> go (d+1) ls (rhs + 1 : us) more - (Neg,Lt ) -> go (d-1) (rhs - 1 : ls) us more - (Pos,Eq ) -> go d (rhs - 1 : ls) (rhs + 1 : us) more - (Neg,Eq ) -> go d (rhs : ls) (rhs : us) more - - go d ls us (DivCt {} : more) = go d ls us more - go d ls us [] = if d >= 0 then Left ls else Right us - - --- | Case when variable gets arbitrarily small. -fNegInfAtom :: Term -> Ct -> Atom -fNegInfAtom _ (AtomCt pol op _ _) = mkBool \$ evalPol pol \$ case op of - Eq -> False - Lt -> True - Leq -> True -fNegInfAtom j (DivCt pol m _ t) = mkDiv pol m (j + t) - - --- | Case when variable gets arbitrarily large. -posInfAtom :: Term -> Ct -> Atom -posInfAtom _ (AtomCt pol _ _ _) = mkBool \$ case pol of - Pos -> False -- eq,lt,leq:all False - Neg -> True -- fNegations are true -posInfAtom j (DivCt p m _ t) = mkDiv p m (j + t) - --- | Replace the variable in a constraint with the given term. -letAtom :: Term -> Ct -> Atom -letAtom b (AtomCt pol op _ rhs) = mkAtom pol op newLhs newRhs - where (newLhs,newRhs) = tSplit (rhs - b) -letAtom b (DivCt p m _ t) = mkDiv p m (b + t) - - -ex :: Name -> Formula -> Formula -ex x fo - | Just (Or, f1, f2) <- isFConn fo = fConn Or (ex x f1) (ex x f2) - | otherwise = - case ctFo of - Fo f -> f -- Did not mention variable, nothing to do. - _ -> - case getBounds (getCts ctFo []) of - Left lowerBounds -> - fConns Or \$ - [ ctAtoms (fNegInfAtom (fromInteger j)) ctFo - | j <- [ 1 .. delta ] ] - ++ - [ ctAtoms (letAtom (j |+| b)) ctFo - | j <- [ 1 .. delta ], b <- lowerBounds ] - - Right upperBounds -> - fConns Or \$ - [ ctAtoms (posInfAtom (fromInteger (negate j))) ctFo - | j <- [ 1 .. delta ] ] - ++ - [ ctAtoms (letAtom (negate j |+| a)) ctFo - | j <- [ 1 .. delta ], a <- upperBounds ] - where - (_coeff, ctFo0) = aCts x fo - (delta, ctFo) = computeDelta ctFo0 - -exists :: [Name] -> Formula -> Formula -exists xs f = foldr ex f xs - - -example = fAtom \$ mkAtom Pos Eq (3 |*| tVar 1) (5 |*| tVar 2) - --- 3 * x = 5 * y --- x = 5 * y /\ 3 | x --- x = 5 * y /\ 3 | 5 * y --- { x = 5 * y } 3 | 5 * y - - -{- | We use this for outermost quantifiers, which assumes no free variables -in the formula. -} -existsTop :: [Name] -> Formula -> [ Soln ] -existsTop [] fo = if isTrue fo then [ [] ] else [] -existsTop xs fo - | Just (Or, f1, f2) <- isFConn fo = existsTop xs f1 ++ existsTop xs f2 -existsTop xs fo = concat \$ map expandTopFo \$ foldr exTops [TopFo [] fo] xs - -data Val a = InfDown | Num a | InfUp deriving Show -type Soln = [ (Name,Val Integer) ] -data TopFo = TopFo [(Name,Integer,Val Term,Integer)] Formula - deriving Show - -expandTopFo :: TopFo -> [ Soln ] -expandTopFo (TopFo ds0 fo) = mapMaybe useSu \$ solve ds \$ findDivCts fo - where - ds = [ (x,d) | (x,d,_,_) <- ds0 ] - useSu su = do guard (isTrue (fLetNums su fo)) - return [ (x, mkT su s t) | (x,_,t,s) <- ds0 ] - - - mkT _ _ InfDown = InfDown - mkT _ _ InfUp = InfUp - mkT su s (Num t) = - let t1 = tLetNums su t - in case isConst t1 of - Just v -> Num (div v s) - Nothing -> error ("expantTopFo: Free variables in" ++ show t1) - --- F_neg (j) = F(j - L * delta) - --- x == t = False --- x /= t = True - - - -isTrue :: Formula -> Bool -isTrue fo = - case isBool =<< isFAtom fo of - Just x -> x - Nothing -> - case isFConn fo of - Just (c, f1, f2) -> case c of - And -> isTrue f1 && isTrue f2 - Or -> isTrue f1 || isTrue f2 - _ -> error "Unexpected free variables in term" - - - - - -findDivCts :: Formula -> [DivCt] -findDivCts = mapMaybe isDivCt . splitConn And - where isDivCt fo = do a <- isFAtom fo - (Pos,m,t) <- isDiv a - return (m,t) - - -exTops :: Name -> [TopFo] -> [TopFo] -exTops x = concatMap (exTop x) - -exTop :: Name -> TopFo -> [TopFo] -exTop x it@(TopFo ds fo) = - case ctFo of - Fo _ -> [it] -- Did not mention variable, nothing to do. - _ -> map topFo \$ - case getBounds (getCts ctFo []) of - Left lowerBounds -> - (InfDown, ctAtoms (fNegInfAtom \$ tVar x') ctFo) - : [ (Num te, ctAtoms (letAtom te) ctFo) | b <- lowerBounds - , let te = tVar x' + b ] - - Right upperBounds -> - (InfUp, ctAtoms (posInfAtom \$ negate (tVar x')) ctFo) - : [ (Num te, ctAtoms (letAtom te) ctFo) | a <- upperBounds - , let te = a - tVar x' ] - where - (coeff, ctFo0) = aCts x fo - (delta, ctFo) = computeDelta ctFo0 - topFo (te,f) = TopFo ((x',delta,te,coeff) : ds) f - - x' = negate x - - -instance Show Ct where - showsPrec p = showsPrec p . toAtom -instance Show CtFo where - showsPrec p = showsPrec p . ctAtoms toAtom - -toAtom :: Ct -> Atom -toAtom (AtomCt p op x t) = mkAtom p op (tVar x) t -toAtom (DivCt p m x t) = mkDiv p m (tVar x + t) - -
240 src/Data/Integer/Presburger/Formula.hs
 @@ -1,240 +0,0 @@ -{-# LANGUAGE Safe #-} -module Data.Integer.Presburger.Formula - ( Formula - , fConn - , fConns - , fAtom - , fLet - , fLetNums - , fNeg - , Conn(..) - , Pol(..) - , PredS(..) - , Atom - , mkAtom - , mkDiv - , mkBool - , isFConn, isFAtom, splitConn - , isAtom, isDiv, isBool - , evalPol - ) - where - -import Data.Integer.Presburger.Term - (Term, Name, PP(..), pp, tLet, tLetNums, tSplit, isConst) - -import Text.PrettyPrint -import Control.Monad(liftM2) - --- | Formulas. -data Formula = AtomF Atom - | ConnF !Conn Formula Formula - --- | Connectives. -data Conn = And | Or - deriving (Show, Eq) - - --- | Basic propositions. -data Atom = Atom !Pol !PredS Term Term -- ^ Comparisons - | Div !Pol !Integer Term -- ^ Divisibility assertions - | Bool !Bool -- ^ Constants - deriving Eq - --- | Polarity of atoms. -data Pol = Pos -- ^ Normal atom. - | Neg -- ^ Negated atom. - deriving (Eq, Show) - --- | Binary predicate symbols. -data PredS = Eq | Lt | Leq - deriving (Eq, Show) - --------------------------------------------------------------------------------- --- Patterns - -isFAtom :: Formula -> Maybe Atom -isFAtom (AtomF a) = Just a -isFAtom _ = Nothing - -isFConn :: Formula -> Maybe (Conn, Formula, Formula) -isFConn (ConnF c p q) = Just (c,p,q) -isFConn _ = Nothing - --- | Split a formula into its conjuncts. Always returns at least one element. -splitConn :: Conn -> Formula -> [Formula] -splitConn c0 f0 = go f0 [] - where - go (ConnF c f1 f2) more | c == c0 = go f1 (go f2 more) - go f more = f : more - - - --------------------------------------------------------------------------------- --- Smart constructors. - -fConns :: Conn -> [Formula] -> Formula -fConns And [] = fAtom \$ mkBool True -fConns Or [] = fAtom \$ mkBool False -fConns c fs = foldr1 (fConn c) fs - -fConn :: Conn -> Formula -> Formula -> Formula - --- NOTE: Here we only simply True/False when it appears in the first argument. --- This memory leaks where we have to fullly evaluate both sub-formulas --- before we know the top-most connective in the formula. -fConn And f1@(AtomF (Bool False)) _ = f1 -fConn And (AtomF (Bool True)) f2 = f2 - -fConn Or f1@(AtomF (Bool True)) _ = f1 -fConn Or (AtomF (Bool False)) f2 = f2 - -fConn c f1 f2 = ConnF c f1 f2 - -fAtom :: Atom -> Formula -fAtom = AtomF - -fNeg :: Formula -> Formula -fNeg (ConnF c f1 f2) = ConnF (negC c) (fNeg f1) (fNeg f2) - where - negC And = Or - negC Or = And - -fNeg (AtomF a) = AtomF (negA a) - where - negP Pos = Neg - negP Neg = Pos - - negA (Bool b) = Bool (not b) - negA (Atom pol op t1 t2) = Atom (negP pol) op t1 t2 - negA (Div pol m t) = Div (negP pol) m t - - -fLetNums :: [(Name,Integer)] -> Formula -> Formula -fLetNums su fo = - case fo of - ConnF c f1 f2 -> fConn c (fLetNums su f1) (fLetNums su f2) - AtomF a -> - case a of - Atom p s t1 t2 -> - let (lhs,rhs) = tSplit \$ tLetNums su \$ t2 - t1 - in AtomF (mkAtom p s lhs rhs) - Div p m t1 -> AtomF (mkDiv p m (tLetNums su t1)) - Bool _ -> fo - -fLet :: Name -> Term -> Formula -> Formula -fLet x t fo = - case fo of - ConnF c f1 f2 -> fConn c (fLet x t f1) (fLet x t f2) - AtomF a -> - case a of - Atom p s t1 t2 -> - let (lhs,rhs) = tSplit \$ tLet x t \$ t2 - t1 - in AtomF (mkAtom p s lhs rhs) - Div p m t1 -> AtomF (mkDiv p m (tLet x t t1)) - Bool _ -> fo - - -mkAtom :: Pol -> PredS -> Term -> Term -> Atom -mkAtom p s t1 t2 = - let a = Atom p s t1 t2 - in case evalAtom a of - Just b -> Bool b - Nothing -> a - -mkDiv :: Pol -> Integer -> Term -> Atom -mkDiv p m t = - let a = Div p m t - in case evalAtom a of - Just b -> Bool b - Nothing -> a - -mkBool :: Bool -> Atom -mkBool = Bool - -isAtom :: Atom -> Maybe (Pol, PredS, Term, Term) -isAtom (Atom p s x y) = Just (p,s,x,y) -isAtom _ = Nothing - -isDiv :: Atom -> Maybe (Pol, Integer, Term) -isDiv (Div p m t) = Just (p,m,t) -isDiv _ = Nothing - -isBool :: Atom -> Maybe Bool -isBool (Bool a) = Just a -isBool _ = Nothing - - --------------------------------------------------------------------------------- --- Evaluation. - -evalAtom :: Atom -> Maybe Bool -evalAtom (Div p m t) = evalPolMb p \$ - if m == 1 then Just True - else do x <- isConst t - return (mod x m == 0) -evalAtom (Bool b) = Just b -evalAtom (Atom pol op lhs rhs) = - evalPolMb pol \$ - case op of - Lt -> liftM2 (<) (isConst lhs) (isConst rhs) - Leq -> liftM2 (<=) (isConst lhs) (isConst rhs) - Eq -> liftM2 (==) (isConst lhs) (isConst rhs) - -evalPolMb :: Pol -> Maybe Bool -> Maybe Bool -evalPolMb p mb = fmap (evalPol p) mb - -evalPol :: Pol -> Bool -> Bool -evalPol Pos x = x -evalPol Neg x = not x - - - - --------------------------------------------------------------------------------- --- Pretty printing. - -instance Show Atom where - showsPrec p a cs = show (ppPrec p a) ++ cs - -instance PP Atom where - ppPrec _ (Atom pol op lhs rhs) = char '"' <> - pp lhs <+> text o <+> pp rhs <> char '"' - where o = case pol of - Pos -> - case op of - Lt -> "<" - Leq -> "<=" - Eq -> "==" - Neg -> - case op of - Leq -> ">" - Lt -> ">=" - Eq -> "/=" - - ppPrec _ (Bool x) = text (if x then "True" else "False") - - ppPrec _ (Div p x t) = ppPol p - \$ char '"' <> integer x <+> text "|" <+> pp t <> char '"' - - where ppPol Pos d = d - ppPol Neg d = text "Not" <+> parens d - -instance Show Formula where - showsPrec p f = showsPrec p (toFF f) - --- For printing -data FF = FF Conn [FF] | FFAtom Atom - deriving Show - -toFF :: Formula -> FF -toFF fo = - case fo of - AtomF a -> FFAtom a - ConnF c _ _ -> FF c \$ map toFF \$ gather c fo [] - where - gather c (ConnF c' f1 f2) more - | c == c' = gather c f1 (gather c f2 more) - gather _ f more = f : more - -
555 src/Data/Integer/Presburger/Omega.hs