presburger 0.1 → 0.2

raw patch · 2 files changed

+9/−3 lines, 2 files

Files

• presburger.cabal +1/−1
• src/Data/Integer/Presburger.hs +8/−2

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

@@ -79,8 +79,14 @@  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+1)))+  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@@ -114,7 +120,7 @@  type Name           = Int --- | @split_term x (n * x + t1) = (n,t1)+-- | @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)