diff --git a/src/Data/Integer/OldPresburger.hs b/src/Data/Integer/OldPresburger.hs new file mode 100644 index 0000000..2abcd6e --- /dev/null +++ b/src/Data/Integer/OldPresburger.hs @@ -0,0 +1,673 @@ +{-| This module implements Cooper's algorithm for deciding + first order formulas over integers with addition. + +Based on the paper: + * author: D.C.Cooper + * title: "Theorem Proving in Arithmetic without Multiplication" + * year: 1972 +-} +module Data.Integer.OldPresburger + ( check, simplify, Formula(..), Term, (.*), is_constant + , PP(..) + ) where + + +import qualified Data.IntMap as Map +import Data.Maybe(fromMaybe) +import Data.List(nub,foldl') +import Control.Monad(mplus,guard) +import Prelude hiding (LT,EQ) + +import Text.PrettyPrint.HughesPJ + + +-- | Check if a formula is true. +check :: Formula -> Bool +check f = eval_form (pre (True,0) f) + +simplify :: Formula -> Formula +simplify f = invert (pre (True,0) f) + +-- Sugar ----------------------------------------------------------------------- + + +infixl 3 :/\: +infixl 2 :\/: +infixr 1 :=>: + +infix 4 :<:, :<=:, :>:, :>=:, :=:, :/=:, :| + + +-- Forst-oreder formulas for Presburger arithmetic. +data Formula = Formula :/\: Formula + | Formula :\/: Formula + | Formula :=>: Formula + | Not Formula + | Exists (Term -> Formula) + | Forall (Term -> Formula) + | TRUE + | FALSE + | Term :<: Term + | Term :>: Term + | Term :<=: Term + | Term :>=: Term + | Term :=: Term + | Term :/=: Term + | Integer :| Term + +pre :: (Bool,Int) -> Formula -> Form +pre n form = case form of + f1 :/\: f2 -> and' (pre n f1) (pre n f2) + f1 :\/: f2 -> or' (pre n f1) (pre n f2) + f1 :=>: f2 -> pre n (Not f1 :\/: f2) + Exists f -> pre_ex (top,x + 1) [x] (f (var x)) + where (top,x) = n + Forall f -> pre n (Not (Exists (Not . f))) + TRUE -> tt' + FALSE -> ff' + t1 :<: t2 -> lt' t1 t2 + t1 :>: t2 -> lt' t2 t1 + t1 :<=: t2 -> leq' t1 t2 + t1 :>=: t2 -> leq' t2 t1 + t1 :=: t2 -> eq' t1 t2 + t1 :/=: t2 -> neq' t1 t2 + k :| t -> divs' k t + Not form1 -> case form1 of + Not f -> pre n f + Forall f -> pre n (Exists (Not . f)) + _ -> not' (pre n form1) + +pre_ex :: (Bool,Int) -> [Name] -> Formula -> Form +pre_ex (top,n) xs form = case form of + Exists f -> pre_ex (top,n+1) (n:xs) (f (var n)) + f1 :\/: f2 -> or' (pre_ex (top,n) xs f1) (pre_ex (top,n) xs f2) + Not form1 -> + case form1 of + Not form2 -> pre_ex (top,n) xs form2 + Forall f -> pre_ex (top,n) xs (Exists (Not . f)) + p :/\: q -> pre_ex (top,n) xs (Not p :\/: Not q) + _ -> exists_many top xs (pre (False,n) form) + _ -> exists_many top xs (pre (False,n) form) + +invert :: Form -> Formula +invert form = case form of + Conn And f1 f2 -> invert f1 :/\: invert f2 + Conn Or f1 f2 -> invert f1 :\/: invert f2 + Prop prop -> case prop of + Pred FF True :> [] -> FALSE + Pred FF False :> [] -> TRUE + Pred LT True :> [t1,t2] -> t1 :<: t2 + Pred LT False :> [t1,t2] -> t1 :>=: t2 + Pred LEQ True :> [t1,t2] -> t1 :<=: t2 + Pred LEQ False :> [t1,t2] -> t1 :>: t2 + Pred EQ True :> [t1,t2] -> t1 :=: t2 + Pred EQ False :> [t1,t2] -> t1 :/=: t2 + Pred (Divs n) True :> [t] -> n :| t + Pred (Divs n) False :> [t] -> Not (n :| t) + _ -> error "(bug) Type error in 'invert'" + + +-- Terms ---------------------------------------------------------------------- + +-- | Terms of Presburger arithmetic. +-- Term are created by using the 'Num' class. +-- WARNING: Presburger arithmetic only supports multiplication +-- by a constant, trying to create invalid terms will result +-- in a run-time error. A more type-safe alternative is to +-- use the '(.*)' operator. +data Term = Term (Map.IntMap Integer) Integer + + +type Name = Int + +-- | @split_term x (n * x + t1) = (n,t1)@ +-- @x@ does not occur in @t1@ +split_term :: Name -> Term -> (Integer,Term) +split_term x (Term m n) = (fromMaybe 0 c, Term m1 n) + where (c,m1) = Map.updateLookupWithKey (\_ _ -> Nothing) x m + +var :: Name -> Term +var x = Term (Map.singleton x 1) 0 + +num :: Integer -> Term +num n = Term Map.empty n + + +-------------------------------------------------------------------------------- + +instance Eq Term where + t1 == t2 = is_constant (t1 - t2) == Just 0 + +instance Num Term where + fromInteger n = Term Map.empty n + + Term m1 n1 + Term m2 n2 = Term (Map.unionWith (+) m1 m2) (n1 + n2) + + negate (Term m n) = Term (Map.map negate m) (negate n) + + t1 * t2 = case fmap (.* t2) (is_constant t1) `mplus` + fmap (.* t1) (is_constant t2) of + Just t -> t + Nothing -> error $ unlines [ "[(*) @ Term] Non-linear product:" + , " *** " ++ show t1 + , " *** " ++ show t2 + ] + signum t = case is_constant t of + Just n -> num (signum n) + Nothing -> error $ unlines [ "[signum @ Term]: Non-constant:" + , " *** " ++ show t + ] + + abs t = case is_constant t of + Just n -> num (abs n) + Nothing -> error $ unlines [ "[abs @ Term]: Non-constant:" + , " *** " ++ show t + ] + + +-- | Check if a term is a constant (i.e., contains no variables). +-- If so, then we return the constant, otherwise we return 'Nothing'. +is_constant :: Term -> Maybe Integer +is_constant (Term m n) = guard (all (0 ==) (Map.elems m)) >> return n + +(.*) :: Integer -> Term -> Term +0 .* _ = 0 +1 .* t = t +k .* Term m n = Term (Map.map (k *) m) (k * n) + + +-- Formulas -------------------------------------------------------------------- + +data PredSym = FF | LT | LEQ | EQ | Divs Integer {- +ve -} +data Pred = Pred PredSym Bool -- Bool: positive (i.e. non-negated)? +data Prop = Pred :> [Term] +data Conn = And | Or deriving Eq +data Form = Conn Conn Form Form | Prop Prop + +abs_form :: Form -> ([Prop],[Prop] -> Form) +abs_form fo = let (ps,skel) = loop [] fo + in (reverse ps, fst . skel) + where loop ps (Conn c p q) = + let (ps1,f1) = loop ps p + (ps2,f2) = loop ps1 q + in (ps2, \fs -> let (p1,fs1) = f1 fs + (p2,fs2) = f2 fs1 + in (Conn c p1 p2, fs2)) + loop ps (Prop p) = (p:ps, \(f:fs) -> (Prop f,fs)) + + +not' :: Form -> Form +not' (Conn c t1 t2) = Conn (not_conn c) (not' t1) (not' t2) +not' (Prop p) = Prop (not_prop p) + +ff' :: Form +ff' = Prop $ Pred FF True :>[] + +tt' :: Form +tt' = Prop $ Pred FF False :>[] + +lt' :: Term -> Term -> Form +lt' t1 t2 = Prop $ Pred LT True :> [t1,t2] + +leq' :: Term -> Term -> Form +leq' t1 t2 = Prop $ Pred LEQ True :> [t1,t2] + +eq' :: Term -> Term -> Form +eq' t1 t2 = Prop $ Pred EQ True :> [t1,t2] + +neq' :: Term -> Term -> Form +neq' t1 t2 = Prop $ Pred EQ False :> [t1,t2] + +and' :: Form -> Form -> Form +and' p q = Conn And p q + +or' :: Form -> Form -> Form +or' p q = Conn Or p q + +divs' :: Integer -> Term -> Form +divs' n t = Prop $ Pred (Divs n) True :> [t] + +ors' :: [Form] -> Form +ors' [] = ff' +ors' xs = foldr1 or' xs + +not_conn :: Conn -> Conn +not_conn And = Or +not_conn Or = And + +not_prop :: Prop -> Prop +not_prop (f :> ts) = not_pred f :> ts + +not_pred :: Pred -> Pred +not_pred (Pred p pos) = Pred p (not pos) + + + +-- Eliminating existential quantifiers ----------------------------------------- + +data NormProp = Ind Prop + | L Pred Term + +norm2 :: Name -> Integer -> Pred -> Term -> Term -> (Integer,NormProp) +norm2 x final_k p t1 t2 + | k1 == k2 = (1, Ind (p :> [t1',t2'])) + | k1 > k2 = (abs k, L p t) + | otherwise = (abs k, L p' t) + + where (k1,t1') = split_term x t1 + (k2,t2') = split_term x t2 + + k = k1 - k2 + t = (final_k `div` k) .* (t2' - t1') -- only used when k /= 0 + + p' = case p of + Pred LT b -> Pred LEQ (not b) + Pred LEQ b -> Pred LT (not b) + _ -> p + +norm1 :: Name -> Integer -> Pred -> Term -> (Integer,NormProp) +norm1 x final_k p@(Pred (Divs d) b) t + | k == 0 = (1, Ind (p :> [t])) + | otherwise = (abs k, L ps (l .* t')) + + where (k,t') = split_term x t + l = final_k `div` k + ps = Pred (Divs (d * abs l)) b + +norm1 _ _ _ _ = error "(bug) norm1 applied to a non-unary operator" + + +norm_prop :: Name -> Integer -> Prop -> (Integer,NormProp) +norm_prop _ _ p@(_ :> []) = (1,Ind p) +norm_prop x final_k (p :> [t]) = norm1 x final_k p t +norm_prop x final_k (p :> [t1,t2]) = norm2 x final_k p t1 t2 +norm_prop _ _ _ = error "(bug) norm_prop on arity > 2" + +-- The integer is "length as - length bs" +a_b_sets :: (Integer,[Term],[Term]) -> NormProp -> (Integer,[Term],[Term]) +a_b_sets (o,as,bs) p = case p of + Ind _ -> (o,as,bs) + + L (Pred op True) t -> + case op of + LT -> (1 + o , t : as, bs) + LEQ -> (1 + o , (t+1) : as, bs) + EQ -> (o , (t+1) : as, (t-1) : bs) + _ -> (o , as, bs) + + L (Pred op False) t -> + case op of + LT -> (o - 1 , as, (t-1) : bs) + LEQ -> (o - 1 , as, t : bs) + EQ -> (o , t : as, t : bs) + _ -> (o , as, bs) + + +analyze_props :: Name -> [Prop] -> ( [NormProp] + , Integer -- scale + , Integer -- bound + , Either [Term] [Term] -- A set or B set + ) +analyze_props x ps = (ps1, final_k, bnd, if o < 0 then Left as else Right bs) + where (ks,ps1) = unzip $ map (norm_prop x final_k) ps + final_k = lcms ks + (o,as,bs) = foldl' a_b_sets (0,[],[]) ps1 + bnd = lcms (final_k : [ d | L (Pred (Divs d) _) _ <- ps1 ]) + +from_bool :: Bool -> Prop +from_bool True = Pred FF False :> [] +from_bool False = Pred FF True :> [] + +neg_inf :: NormProp -> Term -> Prop +neg_inf prop t = case prop of + Ind p -> p + L ps@(Pred op pos) t1 -> case op of + LT -> from_bool pos + LEQ -> from_bool pos + EQ -> from_bool (not pos) + Divs {} -> ps :> [t + t1] + FF -> error "(bug) FF in NormPred" + +pos_inf :: NormProp -> Term -> Prop +pos_inf prop t = case prop of + Ind p -> p + L ps@(Pred op pos) t1 -> case op of + LT -> from_bool (not pos) + LEQ -> from_bool (not pos) + EQ -> from_bool (not pos) + Divs {} -> ps :> [t + t1] + FF -> error "(bug) FF in NormPred" + +normal :: NormProp -> Term -> Prop +normal prop t = case prop of + Ind p -> p + L ps@(Pred (Divs {}) _) t1 -> ps :> [t + t1] + L ps t1 -> ps :> [t,t1] + + +data Ex = Ex [(Name,Integer)] + [Constraint] + [Prop] + +exists_many :: Bool -> [Name] -> Form -> Form +exists_many top xs f = ors' + $ map exp_f + $ foldr (concatMap . ex_step) [Ex [] [] ps] (nub xs) + where (ps,skel) = abs_form f + exp_f = if top then expand_top skel else expand skel + + +ex_step :: Name -> Ex -> [Ex] +ex_step x (Ex xs ds ps) = case as_or_bs of + Left as -> + ( let arg = negate (var x) + in Ex ((x,d) : xs) (constr arg) (map (`pos_inf` arg) ps1) + ) : [ let arg = a - var x + in Ex ((x,d) : xs) (constr arg) (map (`normal` arg) ps1) | a <- as ] + + Right bs -> + ( let arg = var x + in Ex ((x,d) : xs) (constr arg) (map (`neg_inf` arg) ps1) + ) : [ let arg = b + var x + in Ex ((x,d) : xs) (constr arg) (map (`normal` arg) ps1) | b <- bs ] + + where (ps1,k,d',as_or_bs) = analyze_props x ps + d = lcms (d' : map fst ds) + constr t = if k == 1 then ds else (k,t) : ds + + +expand_top :: ([Prop] -> Form) -> Ex -> Form +expand_top skel (Ex xs ds ps) = + ors' [ skel (map (subst_prop env) ps) | env <- elim xs ds ] + +expand :: ([Prop] -> Form) -> Ex -> Form +expand skel (Ex xs ds ps) = + ors' [ foldr and' (skel (map (subst_prop env) ps)) (map (`ctr` env) ds) + | env <- envs xs ] + + where envs [] = [ Map.empty ] + envs ((x,bnd):qs) = [ Map.insert x v env + | env <- envs qs, v <- [ 1 .. bnd ] ] + + ctr (k,t) env = Prop (Pred (Divs k) True :> [ subst_term env t ]) + + + +type Env = Map.IntMap Integer + +subst_prop :: Env -> Prop -> Prop +subst_prop env (p :> ts) = p :> map (subst_term env) ts + +subst_term :: Env -> Term -> Term +subst_term env (Term m n) = + let (xs,vs) = unzip $ Map.toList $ Map.intersectionWith (*) env m + in Term (foldl' (flip Map.delete) m xs) (foldl' (+) n vs) + + + + +-- Evaluation ------------------------------------------------------------------ + +-- The meanings of formulas. +eval_form :: Form -> Bool +eval_form (Conn c p q) = eval_conn c (eval_form p) (eval_form q) +eval_form (Prop p) = eval_prop p + +-- The meanings of connectives. +eval_conn :: Conn -> Bool -> Bool -> Bool +eval_conn And = (&&) +eval_conn Or = (||) + +-- The meanings of atomic propositions. +eval_prop :: Prop -> Bool +eval_prop (Pred p pos :> ts) = if pos then res else not res + where res = eval_pred p (map eval_term ts) + +-- The meanings of predicate symbols. +eval_pred :: PredSym -> [Integer] -> Bool +eval_pred p ts = case (p,ts) of + (FF, []) -> False + (Divs d, [k]) -> divides d k + (LT, [x,y]) -> x < y + (LEQ, [x,y]) -> x <= y + (EQ, [x,y]) -> x == y + _ -> error "Type error" + +-- We define: "d | a" as "exists y. d * y = a" +divides :: Integral a => a -> a -> Bool +0 `divides` 0 = True +0 `divides` _ = False +x `divides` y = mod y x == 0 + +-- The meaning of a term with no free variables. +-- NOTE: We do not check that there are no free variables. +eval_term :: Term -> Integer +eval_term (Term _ k) = k + +-- The meaning of a term with free variables +eval_term_env :: Term -> Env -> Integer +eval_term_env (Term m k) env = sum (k : map eval_var (Map.toList m)) + where eval_var (x,c) = case Map.lookup x env of + Nothing -> error "free var" + Just v -> c * v +-------------------------------------------------------------------------------- + + +-- Solving divides constraints ------------------------------------------------- +-- See the paper's appendix. + + +-- | let (p,q,r) = extended_gcd x y +-- in (x * p + y * q = r) && (gcd x y = r) +extended_gcd :: Integral a => a -> a -> (a,a,a) +extended_gcd arg1 arg2 = loop arg1 arg2 0 1 1 0 + where loop a b x lastx y lasty + | b /= 0 = let (q,b') = divMod a b + x' = lastx - q * x + y' = lasty - q * y + in x' `seq` y' `seq` loop b b' x' x y' y + | otherwise = (lastx,lasty,a) + + +type Constraint = (Integer,Term) +type VarConstraint = (Integer,Integer,Term) + +-- m | (x * a1 + b1) /\ (n | x * a2 + b2) +theorem1 :: VarConstraint -> VarConstraint -> (VarConstraint, Constraint) +theorem1 (m,a1,b1) (n,a2,b2) = (new_x, new_other) + where new_x = (m * n, d, (p*n) .* b1 + (q * m) .* b2) + new_other = (d, a2 .* b1 - a1 .* b2) + + (p,q,d) = extended_gcd (a1 * n) (a2 * m) + +-- solutions for x in [1 .. bnd] of: m | x * a + b +theorem2 :: Integer -> (Integer,Integer,Integer) -> [Integer] +theorem2 bnd (m,a,b) + | r == 0 = [ t * k - c | t <- [ lower .. upper ] ] + | otherwise = [] + where k = div m d + c = p * qu + (p,_,d) = extended_gcd a m + (qu,r) = divMod b d + + (lower',r1) = divMod (1 + c) k + lower = if r1 == 0 then lower' else lower' + 1 -- hmm + upper = div (bnd + c) k + + -- lower and upper: + -- t * k - c = 1 --> t = (1 + c) / k + -- t * k - c = bnd --> t = (bnd + c) / k + + + + +elim :: [(Name,Integer)] -> [Constraint] -> [ Env ] +elim [] ts = if all chk ts then [ Map.empty ] else [] + where chk (x,t) = divides x (eval_term t) +elim ((x,bnd):xs) cs = do env <- elim xs cs1 + v <- case mb of + Nothing -> [ 1 .. bnd ] + Just (a,b,t) -> + theorem2 bnd (a,b,eval_term_env t env) + return (Map.insert x v env) + + where (mb,cs1) = elim_var x cs + + + + +elim_var :: Name -> [Constraint] -> (Maybe VarConstraint, [Constraint]) +elim_var x cs = case foldl' part ([],[]) cs of + ([], have_not) -> (Nothing, have_not) + (h : hs, have_not) -> let (c,hn) = step h hs have_not + in (Just c,hn) + where part s@(have,have_not) c@(m,t) + | m == 1 = s + | a == 0 = (have , c:have_not) + | otherwise = ((m,a,b):have, have_not) + where (a,b) = split_term x t + + step :: VarConstraint -> [VarConstraint] -> [Constraint] + -> (VarConstraint,[Constraint]) + step h [] ns = (h,ns) + step h (h1:hs) ns = step h2 hs (n : ns) + where (h2,n) = theorem1 h h1 + +-- Misc ----------------------------------------------------------------------- + +lcms :: Integral a => [a] -> a +lcms xs = foldr lcm 1 xs + + +-- Pretty Printing ------------------------------------------------------------- + +class PP a where + pp :: a -> Doc + + +var_name :: Name -> String +var_name x = let (a,b) = divMod x 26 + rest = if a == 0 then "" else show a + in toEnum (97 + b) : rest + +instance Show Term where show x = show (pp x) +instance PP Term where + pp (Term m k) | isEmpty vars = text (show k) + | k == 0 = vars + | k > 0 = vars <+> char '+' <+> text (show k) + | otherwise = vars <+> char '-' <+> text (show $ abs k) + where ppvar (x,n) = sign <+> co <+> text (var_name x) + where (sign,co) + | n == -1 = (char '-', empty) + | n < 0 = (char '-', text (show (abs n)) <+> char '*') + | n == 1 = (char '+', empty) + | otherwise = (char '+', text (show n) <+> char '*') + first_var (x,1) = text (var_name x) + first_var (x,-1) = char '-' <> text (var_name x) + first_var (x,n) = text (show n) <+> char '*' <+> text (var_name x) + + vars = case filter ((/= 0) . snd) (Map.toList m) of + [] -> empty + v : vs -> first_var v <+> hsep (map ppvar vs) + + +-- 4: wrap term, not +-- 3: wrap and +-- 2: wrap or +-- 1: wrap implies, quantifiers +instance PP Formula where + pp = pp1 0 -- ' 0 0 + where + pp1 :: Int -> Formula -> Doc + pp1 p form = case form of + _ :/\: _ -> hang (text "/\\") 2 (loop form) + where loop (f1 :/\: f2) = loop f1 $$ loop f2 + loop f = pp f + + _ :\/: _ -> hang (text "\\/") 2 (loop form) + where loop (f1 :\/: f2) = loop f1 $$ loop f2 + loop f = pp f + + _ -> pp' 0 p form + + + + pp' :: Int -> Name -> Formula -> Doc + pp' n p form = case form of + f1 :/\: f2 | n < 3 -> pp' 2 p f1 <+> text "/\\" <+> pp' 2 p f2 + f1 :\/: f2 | n < 2 -> pp' 1 p f1 <+> text "\\/" <+> pp' 1 p f2 + f1 :=>: f2 | n < 1 -> pp' 1 p f1 <+> text "=>" <+> pp' 0 p f2 + Not f | n < 4 -> text "Not" <+> pp' 4 p f + Exists {} | n < 1 -> pp_ex (text "exists") p form + where pp_ex d q (Exists g) = pp_ex (d <+> text (var_name q)) + (q+1) (g (var q)) + pp_ex d q g = d <> text "." <+> pp' 0 q g + + Forall {} | n < 1 -> pp_ex (text "forall") p form + where pp_ex d q (Forall g) = pp_ex (d <+> text (var_name q)) + (q+1) (g (var q)) + pp_ex d q g = d <> text "." <+> pp' 0 q g + TRUE -> text "true" + FALSE -> text "false" + t1 :<: t2 | n < 4 -> pp t1 <+> text "<" <+> pp t2 + t1 :>: t2 | n < 4 -> pp t1 <+> text ">" <+> pp t2 + t1 :<=: t2 | n < 4 -> pp t1 <+> text "<=" <+> pp t2 + t1 :>=: t2 | n < 4 -> pp t1 <+> text ">=" <+> pp t2 + t1 :=: t2 | n < 4 -> pp t1 <+> text "=" <+> pp t2 + t1 :/=: t2 | n < 4 -> pp t1 <+> text "/=" <+> pp t2 + k :| t1 | n < 4 -> text (show k) <+> text "|" <+> pp t1 + _ -> parens (pp' 0 p form) + +instance Show Formula where show = show . pp + + + +instance PP PredSym where + pp p = case p of + FF -> text "false" + LT -> text "<" + LEQ -> text "<=" + EQ -> text "===" + Divs n -> text (show n) <+> text "|" + +instance PP Pred where + pp (Pred p True) = pp p + pp (Pred p False) = case p of + FF -> text "true" + LT -> text ">=" + LEQ -> text ">" + EQ -> text "=/=" + Divs n -> text (show n) <+> text "/|" + +instance Show Prop where show = show . pp +instance PP Prop where + pp (p :> [t1,t2]) = pp t1 <+> pp p <+> pp t2 + pp (p :> ts) = pp p <+> hsep (map pp ts) + + +instance PP Conn where + pp And = text "/\\" + pp Or = text "\\/" + +instance PP Form where + pp me@(Conn c _ _) = hang (pp c) 2 (vcat $ map pp $ jn me []) + where jn (Conn c1 p1 q1) fs | c == c1 = jn p1 (jn q1 fs) + jn f fs = f : fs + pp (Prop p) = pp p + +instance PP NormProp where + pp (Ind p) = pp p + pp (L p@(Pred (Divs {}) _) t) = pp p <+> text "_ +" <+> pp t + pp (L p t) = text "_" <+> pp p <+> pp t + +instance Show NormProp where show = show . pp + +instance PP Ex where + pp (Ex xs ps ss) = hang (text "OR" <+> hsep (map quant xs)) 2 + ( text "!" <+> hsep (map (parens . divs) ps) + $$ vcat (map pp ss) + ) + where quant (x,n) = parens $ text (var_name x) <> colon <> text (show n) + divs (x,t) = text (show x) <+> text "|" <+> pp t + + diff --git a/src/Data/Integer/Presburger.hs b/src/Data/Integer/Presburger.hs index bff4642..f8a272f 100644 --- a/src/Data/Integer/Presburger.hs +++ b/src/Data/Integer/Presburger.hs @@ -6,668 +6,6 @@ Based on the paper: * title: "Theorem Proving in Arithmetic without Multiplication" * year: 1972 -} -module Data.Integer.Presburger - ( check, simplify, Formula(..), Term, (.*), is_constant - , PP(..) - ) where - - -import qualified Data.IntMap as Map -import Data.Maybe(fromMaybe) -import Data.List(nub,foldl') -import Control.Monad(mplus,guard) -import Prelude hiding (LT,EQ) - -import Text.PrettyPrint.HughesPJ - - --- | Check if a formula is true. -check :: Formula -> Bool -check f = eval_form (pre (True,0) f) - -simplify :: Formula -> Formula -simplify f = invert (pre (True,0) f) - --- Sugar ----------------------------------------------------------------------- - - -infixl 3 :/\: -infixl 2 :\/: -infixr 1 :=>: - -infix 4 :<:, :<=:, :>:, :>=:, :=:, :/=:, :| - - --- Forst-oreder formulas for Presburger arithmetic. -data Formula = Formula :/\: Formula - | Formula :\/: Formula - | Formula :=>: Formula - | Not Formula - | Exists (Term -> Formula) - | Forall (Term -> Formula) - | TRUE - | FALSE - | Term :<: Term - | Term :>: Term - | Term :<=: Term - | Term :>=: Term - | Term :=: Term - | Term :/=: Term - | Integer :| Term - -pre :: (Bool,Int) -> Formula -> Form -pre n form = case form of - f1 :/\: f2 -> and' (pre n f1) (pre n f2) - f1 :\/: f2 -> or' (pre n f1) (pre n f2) - f1 :=>: f2 -> pre n (Not f1 :\/: f2) - Exists f -> pre_ex (top,x + 1) [x] (f (var x)) - where (top,x) = n - Forall f -> pre n (Not (Exists (Not . f))) - TRUE -> tt' - FALSE -> ff' - t1 :<: t2 -> lt' t1 t2 - t1 :>: t2 -> lt' t2 t1 - t1 :<=: t2 -> leq' t1 t2 - t1 :>=: t2 -> leq' t2 t1 - t1 :=: t2 -> eq' t1 t2 - t1 :/=: t2 -> neq' t1 t2 - k :| t -> divs' k t - Not form1 -> case form1 of - Not f -> pre n f - Forall f -> pre n (Exists (Not . f)) - _ -> not' (pre n form1) - -pre_ex :: (Bool,Int) -> [Name] -> Formula -> Form -pre_ex (top,n) xs form = case form of - Exists f -> pre_ex (top,n+1) (n:xs) (f (var n)) - f1 :\/: f2 -> or' (pre_ex (top,n) xs f1) (pre_ex (top,n) xs f2) - Not form1 -> - case form1 of - Not form2 -> pre_ex (top,n) xs form2 - Forall f -> pre_ex (top,n) xs (Exists (Not . f)) - p :/\: q -> pre_ex (top,n) xs (Not p :\/: Not q) - _ -> exists_many top xs (pre (False,n) form) - _ -> exists_many top xs (pre (False,n) form) - -invert :: Form -> Formula -invert form = case form of - Conn And f1 f2 -> invert f1 :/\: invert f2 - Conn Or f1 f2 -> invert f1 :\/: invert f2 - Prop prop -> case prop of - Pred FF True :> [] -> FALSE - Pred FF False :> [] -> TRUE - Pred LT True :> [t1,t2] -> t1 :<: t2 - Pred LT False :> [t1,t2] -> t1 :>=: t2 - Pred LEQ True :> [t1,t2] -> t1 :<=: t2 - Pred LEQ False :> [t1,t2] -> t1 :>: t2 - Pred EQ True :> [t1,t2] -> t1 :=: t2 - Pred EQ False :> [t1,t2] -> t1 :/=: t2 - Pred (Divs n) True :> [t] -> n :| t - Pred (Divs n) False :> [t] -> Not (n :| t) - _ -> error "(bug) Type error in 'invert'" - - --- Terms ---------------------------------------------------------------------- - --- | Terms of Presburger arithmetic. --- Term are created by using the 'Num' class. --- WARNING: Presburger arithmetic only supports multiplication --- by a constant, trying to create invalid terms will result --- in a run-time error. A more type-safe alternative is to --- use the '(.*)' operator. -data Term = Term (Map.IntMap Integer) Integer - - -type Name = Int - --- | @split_term x (n * x + t1) = (n,t1)@ --- @x@ does not occur in @t1@ -split_term :: Name -> Term -> (Integer,Term) -split_term x (Term m n) = (fromMaybe 0 c, Term m1 n) - where (c,m1) = Map.updateLookupWithKey (\_ _ -> Nothing) x m - -var :: Name -> Term -var x = Term (Map.singleton x 1) 0 - -num :: Integer -> Term -num n = Term Map.empty n - - --------------------------------------------------------------------------------- - -instance Eq Term where - t1 == t2 = is_constant (t1 - t2) == Just 0 - -instance Num Term where - fromInteger n = Term Map.empty n - - Term m1 n1 + Term m2 n2 = Term (Map.unionWith (+) m1 m2) (n1 + n2) - - negate (Term m n) = Term (Map.map negate m) (negate n) - - t1 * t2 = case fmap (.* t2) (is_constant t1) `mplus` - fmap (.* t1) (is_constant t2) of - Just t -> t - Nothing -> error $ unlines [ "[(*) @ Term] Non-linear product:" - , " *** " ++ show t1 - , " *** " ++ show t2 - ] - signum t = case is_constant t of - Just n -> num (signum n) - Nothing -> error $ unlines [ "[signum @ Term]: Non-constant:" - , " *** " ++ show t - ] - - abs t = case is_constant t of - Just n -> num (abs n) - Nothing -> error $ unlines [ "[abs @ Term]: Non-constant:" - , " *** " ++ show t - ] - - --- | Check if a term is a constant (i.e., contains no variables). --- If so, then we return the constant, otherwise we return 'Nothing'. -is_constant :: Term -> Maybe Integer -is_constant (Term m n) = guard (all (0 ==) (Map.elems m)) >> return n - -(.*) :: Integer -> Term -> Term -0 .* _ = 0 -1 .* t = t -k .* Term m n = Term (Map.map (k *) m) (k * n) - - --- Formulas -------------------------------------------------------------------- - -data PredSym = FF | LT | LEQ | EQ | Divs Integer {- +ve -} -data Pred = Pred PredSym Bool -- Bool: positive (i.e. non-negated)? -data Prop = Pred :> [Term] -data Conn = And | Or deriving Eq -data Form = Conn Conn Form Form | Prop Prop - -abs_form :: Form -> ([Prop],[Prop] -> Form) -abs_form fo = let (ps,skel) = loop [] fo - in (reverse ps, fst . skel) - where loop ps (Conn c p q) = - let (ps1,f1) = loop ps p - (ps2,f2) = loop ps1 q - in (ps2, \fs -> let (p1,fs1) = f1 fs - (p2,fs2) = f2 fs1 - in (Conn c p1 p2, fs2)) - loop ps (Prop p) = (p:ps, \(f:fs) -> (Prop f,fs)) - - -not' :: Form -> Form -not' (Conn c t1 t2) = Conn (not_conn c) (not' t1) (not' t2) -not' (Prop p) = Prop (not_prop p) - -ff' :: Form -ff' = Prop $ Pred FF True :>[] - -tt' :: Form -tt' = Prop $ Pred FF False :>[] - -lt' :: Term -> Term -> Form -lt' t1 t2 = Prop $ Pred LT True :> [t1,t2] - -leq' :: Term -> Term -> Form -leq' t1 t2 = Prop $ Pred LEQ True :> [t1,t2] - -eq' :: Term -> Term -> Form -eq' t1 t2 = Prop $ Pred EQ True :> [t1,t2] - -neq' :: Term -> Term -> Form -neq' t1 t2 = Prop $ Pred EQ False :> [t1,t2] - -and' :: Form -> Form -> Form -and' p q = Conn And p q - -or' :: Form -> Form -> Form -or' p q = Conn Or p q - -divs' :: Integer -> Term -> Form -divs' n t = Prop $ Pred (Divs n) True :> [t] - -ors' :: [Form] -> Form -ors' [] = ff' -ors' xs = foldr1 or' xs - -not_conn :: Conn -> Conn -not_conn And = Or -not_conn Or = And - -not_prop :: Prop -> Prop -not_prop (f :> ts) = not_pred f :> ts - -not_pred :: Pred -> Pred -not_pred (Pred p pos) = Pred p (not pos) - - - --- Eliminating existential quantifiers ----------------------------------------- - -data NormProp = Ind Prop - | L Pred Term - -norm2 :: Name -> Integer -> Pred -> Term -> Term -> (Integer,NormProp) -norm2 x final_k p t1 t2 - | k1 == k2 = (1, Ind (p :> [t1',t2'])) - | k1 > k2 = (abs k, L p t) - | otherwise = (abs k, L p' t) - - where (k1,t1') = split_term x t1 - (k2,t2') = split_term x t2 - - k = k1 - k2 - t = (final_k `div` k) .* (t2' - t1') -- only used when k /= 0 - - p' = case p of - Pred LT b -> Pred LEQ (not b) - Pred LEQ b -> Pred LT (not b) - _ -> p - -norm1 :: Name -> Integer -> Pred -> Term -> (Integer,NormProp) -norm1 x final_k p@(Pred (Divs d) b) t - | k == 0 = (1, Ind (p :> [t])) - | otherwise = (abs k, L ps (l .* t')) - - where (k,t') = split_term x t - l = final_k `div` k - ps = Pred (Divs (d * abs l)) b - -norm1 _ _ _ _ = error "(bug) norm1 applied to a non-unary operator" - - -norm_prop :: Name -> Integer -> Prop -> (Integer,NormProp) -norm_prop _ _ p@(_ :> []) = (1,Ind p) -norm_prop x final_k (p :> [t]) = norm1 x final_k p t -norm_prop x final_k (p :> [t1,t2]) = norm2 x final_k p t1 t2 -norm_prop _ _ _ = error "(bug) norm_prop on arity > 2" - --- The integer is "length as - length bs" -a_b_sets :: (Integer,[Term],[Term]) -> NormProp -> (Integer,[Term],[Term]) -a_b_sets (o,as,bs) p = case p of - Ind _ -> (o,as,bs) - - L (Pred op True) t -> - case op of - LT -> (1 + o , t : as, bs) - LEQ -> (1 + o , (t+1) : as, bs) - EQ -> (o , (t+1) : as, (t-1) : bs) - _ -> (o , as, bs) - - L (Pred op False) t -> - case op of - LT -> (o - 1 , as, (t-1) : bs) - LEQ -> (o - 1 , as, t : bs) - EQ -> (o , t : as, t : bs) - _ -> (o , as, bs) - - -analyze_props :: Name -> [Prop] -> ( [NormProp] - , Integer -- scale - , Integer -- bound - , Either [Term] [Term] -- A set or B set - ) -analyze_props x ps = (ps1, final_k, bnd, if o < 0 then Left as else Right bs) - where (ks,ps1) = unzip $ map (norm_prop x final_k) ps - final_k = lcms ks - (o,as,bs) = foldl' a_b_sets (0,[],[]) ps1 - bnd = lcms (final_k : [ d | L (Pred (Divs d) _) _ <- ps1 ]) - -from_bool :: Bool -> Prop -from_bool True = Pred FF False :> [] -from_bool False = Pred FF True :> [] - -neg_inf :: NormProp -> Term -> Prop -neg_inf prop t = case prop of - Ind p -> p - L ps@(Pred op pos) t1 -> case op of - LT -> from_bool pos - LEQ -> from_bool pos - EQ -> from_bool (not pos) - Divs {} -> ps :> [t + t1] - FF -> error "(bug) FF in NormPred" - -pos_inf :: NormProp -> Term -> Prop -pos_inf prop t = case prop of - Ind p -> p - L ps@(Pred op pos) t1 -> case op of - LT -> from_bool (not pos) - LEQ -> from_bool (not pos) - EQ -> from_bool (not pos) - Divs {} -> ps :> [t + t1] - FF -> error "(bug) FF in NormPred" - -normal :: NormProp -> Term -> Prop -normal prop t = case prop of - Ind p -> p - L ps@(Pred (Divs {}) _) t1 -> ps :> [t + t1] - L ps t1 -> ps :> [t,t1] - - -data Ex = Ex [(Name,Integer)] - [Constraint] - [Prop] - -exists_many :: Bool -> [Name] -> Form -> Form -exists_many top xs f = ors' - $ map exp_f - $ foldr (concatMap . ex_step) [Ex [] [] ps] (nub xs) - where (ps,skel) = abs_form f - exp_f = if top then expand_top skel else expand skel - - -ex_step :: Name -> Ex -> [Ex] -ex_step x (Ex xs ds ps) = case as_or_bs of - Left as -> - ( let arg = negate (var x) - in Ex ((x,d) : xs) (constr arg) (map (`pos_inf` arg) ps1) - ) : [ let arg = a - var x - in Ex ((x,d) : xs) (constr arg) (map (`normal` arg) ps1) | a <- as ] - - Right bs -> - ( let arg = var x - in Ex ((x,d) : xs) (constr arg) (map (`neg_inf` arg) ps1) - ) : [ let arg = b + var x - in Ex ((x,d) : xs) (constr arg) (map (`normal` arg) ps1) | b <- bs ] - - where (ps1,k,d',as_or_bs) = analyze_props x ps - d = lcms (d' : map fst ds) - constr t = if k == 1 then ds else (k,t) : ds - - -expand_top :: ([Prop] -> Form) -> Ex -> Form -expand_top skel (Ex xs ds ps) = - ors' [ skel (map (subst_prop env) ps) | env <- elim xs ds ] - -expand :: ([Prop] -> Form) -> Ex -> Form -expand skel (Ex xs ds ps) = - ors' [ foldr and' (skel (map (subst_prop env) ps)) (map (`ctr` env) ds) - | env <- envs xs ] - - where envs [] = [ Map.empty ] - envs ((x,bnd):qs) = [ Map.insert x v env - | env <- envs qs, v <- [ 1 .. bnd ] ] - - ctr (k,t) env = Prop (Pred (Divs k) True :> [ subst_term env t ]) - - - -type Env = Map.IntMap Integer - -subst_prop :: Env -> Prop -> Prop -subst_prop env (p :> ts) = p :> map (subst_term env) ts - -subst_term :: Env -> Term -> Term -subst_term env (Term m n) = - let (xs,vs) = unzip $ Map.toList $ Map.intersectionWith (*) env m - in Term (foldl' (flip Map.delete) m xs) (foldl' (+) n vs) - - - - --- Evaluation ------------------------------------------------------------------ - --- The meanings of formulas. -eval_form :: Form -> Bool -eval_form (Conn c p q) = eval_conn c (eval_form p) (eval_form q) -eval_form (Prop p) = eval_prop p - --- The meanings of connectives. -eval_conn :: Conn -> Bool -> Bool -> Bool -eval_conn And = (&&) -eval_conn Or = (||) - --- The meanings of atomic propositions. -eval_prop :: Prop -> Bool -eval_prop (Pred p pos :> ts) = if pos then res else not res - where res = eval_pred p (map eval_term ts) - --- The meanings of predicate symbols. -eval_pred :: PredSym -> [Integer] -> Bool -eval_pred p ts = case (p,ts) of - (FF, []) -> False - (Divs d, [k]) -> divides d k - (LT, [x,y]) -> x < y - (LEQ, [x,y]) -> x <= y - (EQ, [x,y]) -> x == y - _ -> error "Type error" - --- We define: "d | a" as "exists y. d * y = a" -divides :: Integral a => a -> a -> Bool -0 `divides` 0 = True -0 `divides` _ = False -x `divides` y = mod y x == 0 - --- The meaning of a term with no free variables. --- NOTE: We do not check that there are no free variables. -eval_term :: Term -> Integer -eval_term (Term _ k) = k - --- The meaning of a term with free variables -eval_term_env :: Term -> Env -> Integer -eval_term_env (Term m k) env = sum (k : map eval_var (Map.toList m)) - where eval_var (x,c) = case Map.lookup x env of - Nothing -> error "free var" - Just v -> c * v --------------------------------------------------------------------------------- - - --- Solving divides constraints ------------------------------------------------- --- See the paper's appendix. - - --- | let (p,q,r) = extended_gcd x y --- in (x * p + y * q = r) && (gcd x y = r) -extended_gcd :: Integral a => a -> a -> (a,a,a) -extended_gcd arg1 arg2 = loop arg1 arg2 0 1 1 0 - where loop a b x lastx y lasty - | b /= 0 = let (q,b') = divMod a b - x' = lastx - q * x - y' = lasty - q * y - in x' `seq` y' `seq` loop b b' x' x y' y - | otherwise = (lastx,lasty,a) - - -type Constraint = (Integer,Term) -type VarConstraint = (Integer,Integer,Term) - --- m | (x * a1 + b1) /\ (n | x * a2 + b2) -theorem1 :: VarConstraint -> VarConstraint -> (VarConstraint, Constraint) -theorem1 (m,a1,b1) (n,a2,b2) = (new_x, new_other) - where new_x = (m * n, d, (p*n) .* b1 + (q * m) .* b2) - new_other = (d, a2 .* b1 - a1 .* b2) - - (p,q,d) = extended_gcd (a1 * n) (a2 * m) - --- solutions for x in [1 .. bnd] of: m | x * a + b -theorem2 :: Integer -> (Integer,Integer,Integer) -> [Integer] -theorem2 bnd (m,a,b) - | r == 0 = [ t * k - c | t <- [ lower .. upper ] ] - | otherwise = [] - where k = div m d - c = p * qu - (p,_,d) = extended_gcd a m - (qu,r) = divMod b d - - (lower',r1) = divMod (1 + c) k - lower = if r1 == 0 then lower' else lower' + 1 -- hmm - upper = div (bnd + c) k - - -- lower and upper: - -- t * k - c = 1 --> t = (1 + c) / k - -- t * k - c = bnd --> t = (bnd + c) / k - - - - -elim :: [(Name,Integer)] -> [Constraint] -> [ Env ] -elim [] ts = if all chk ts then [ Map.empty ] else [] - where chk (x,t) = divides x (eval_term t) -elim ((x,bnd):xs) cs = do env <- elim xs cs1 - v <- case mb of - Nothing -> [ 1 .. bnd ] - Just (a,b,t) -> - theorem2 bnd (a,b,eval_term_env t env) - return (Map.insert x v env) - - where (mb,cs1) = elim_var x cs - - - - -elim_var :: Name -> [Constraint] -> (Maybe VarConstraint, [Constraint]) -elim_var x cs = case foldl' part ([],[]) cs of - ([], have_not) -> (Nothing, have_not) - (h : hs, have_not) -> let (c,hn) = step h hs have_not - in (Just c,hn) - where part s@(have,have_not) c@(m,t) - | m == 1 = s - | a == 0 = (have , c:have_not) - | otherwise = ((m,a,b):have, have_not) - where (a,b) = split_term x t - - step :: VarConstraint -> [VarConstraint] -> [Constraint] - -> (VarConstraint,[Constraint]) - step h [] ns = (h,ns) - step h (h1:hs) ns = step h2 hs (n : ns) - where (h2,n) = theorem1 h h1 - --- Misc ----------------------------------------------------------------------- - -lcms :: Integral a => [a] -> a -lcms xs = foldr lcm 1 xs - - --- Pretty Printing ------------------------------------------------------------- - -class PP a where - pp :: a -> Doc - - -var_name :: Name -> String -var_name x = let (a,b) = divMod x 26 - rest = if a == 0 then "" else show a - in toEnum (97 + b) : rest - -instance Show Term where show x = show (pp x) -instance PP Term where - pp (Term m k) | isEmpty vars = text (show k) - | k == 0 = vars - | k > 0 = vars <+> char '+' <+> text (show k) - | otherwise = vars <+> char '-' <+> text (show $ abs k) - where ppvar (x,n) = sign <+> co <+> text (var_name x) - where (sign,co) - | n == -1 = (char '-', empty) - | n < 0 = (char '-', text (show (abs n)) <+> char '*') - | n == 1 = (char '+', empty) - | otherwise = (char '+', text (show n) <+> char '*') - first_var (x,1) = text (var_name x) - first_var (x,-1) = char '-' <> text (var_name x) - first_var (x,n) = text (show n) <+> char '*' <+> text (var_name x) - - vars = case filter ((/= 0) . snd) (Map.toList m) of - [] -> empty - v : vs -> first_var v <+> hsep (map ppvar vs) - - --- 4: wrap term, not --- 3: wrap and --- 2: wrap or --- 1: wrap implies, quantifiers -instance PP Formula where - pp = pp1 0 -- ' 0 0 - where - pp1 :: Int -> Formula -> Doc - pp1 p form = case form of - _ :/\: _ -> hang (text "/\\") 2 (loop form) - where loop (f1 :/\: f2) = loop f1 $$ loop f2 - loop f = pp f - - _ :\/: _ -> hang (text "\\/") 2 (loop form) - where loop (f1 :\/: f2) = loop f1 $$ loop f2 - loop f = pp f - - _ -> pp' 0 p form - - - - pp' :: Int -> Name -> Formula -> Doc - pp' n p form = case form of - f1 :/\: f2 | n < 3 -> pp' 2 p f1 <+> text "/\\" <+> pp' 2 p f2 - f1 :\/: f2 | n < 2 -> pp' 1 p f1 <+> text "\\/" <+> pp' 1 p f2 - f1 :=>: f2 | n < 1 -> pp' 1 p f1 <+> text "=>" <+> pp' 0 p f2 - Not f | n < 4 -> text "Not" <+> pp' 4 p f - Exists {} | n < 1 -> pp_ex (text "exists") p form - where pp_ex d q (Exists g) = pp_ex (d <+> text (var_name q)) - (q+1) (g (var q)) - pp_ex d q g = d <> text "." <+> pp' 0 q g - - Forall {} | n < 1 -> pp_ex (text "forall") p form - where pp_ex d q (Forall g) = pp_ex (d <+> text (var_name q)) - (q+1) (g (var q)) - pp_ex d q g = d <> text "." <+> pp' 0 q g - TRUE -> text "true" - FALSE -> text "false" - t1 :<: t2 | n < 4 -> pp t1 <+> text "<" <+> pp t2 - t1 :>: t2 | n < 4 -> pp t1 <+> text ">" <+> pp t2 - t1 :<=: t2 | n < 4 -> pp t1 <+> text "<=" <+> pp t2 - t1 :>=: t2 | n < 4 -> pp t1 <+> text ">=" <+> pp t2 - t1 :=: t2 | n < 4 -> pp t1 <+> text "=" <+> pp t2 - t1 :/=: t2 | n < 4 -> pp t1 <+> text "/=" <+> pp t2 - k :| t1 | n < 4 -> text (show k) <+> text "|" <+> pp t1 - _ -> parens (pp' 0 p form) - -instance Show Formula where show = show . pp - - - -instance PP PredSym where - pp p = case p of - FF -> text "false" - LT -> text "<" - LEQ -> text "<=" - EQ -> text "===" - Divs n -> text (show n) <+> text "|" - -instance PP Pred where - pp (Pred p True) = pp p - pp (Pred p False) = case p of - FF -> text "true" - LT -> text ">=" - LEQ -> text ">" - EQ -> text "=/=" - Divs n -> text (show n) <+> text "/|" - -instance Show Prop where show = show . pp -instance PP Prop where - pp (p :> [t1,t2]) = pp t1 <+> pp p <+> pp t2 - pp (p :> ts) = pp p <+> hsep (map pp ts) - - -instance PP Conn where - pp And = text "/\\" - pp Or = text "\\/" - -instance PP Form where - pp me@(Conn c _ _) = hang (pp c) 2 (vcat $ map pp $ jn me []) - where jn (Conn c1 p1 q1) fs | c == c1 = jn p1 (jn q1 fs) - jn f fs = f : fs - pp (Prop p) = pp p - -instance PP NormProp where - pp (Ind p) = pp p - pp (L p@(Pred (Divs {}) _) t) = pp p <+> text "_ +" <+> pp t - pp (L p t) = text "_" <+> pp p <+> pp t - -instance Show NormProp where show = show . pp - -instance PP Ex where - pp (Ex xs ps ss) = hang (text "OR" <+> hsep (map quant xs)) 2 - ( text "!" <+> hsep (map (parens . divs) ps) - $$ vcat (map pp ss) - ) - where quant (x,n) = parens $ text (var_name x) <> colon <> text (show n) - divs (x,t) = text (show x) <+> text "|" <+> pp t - - +module Data.Integer.Presburger (module X) where + +import Data.Integer.Presburger.HOAS as X \ No newline at end of file