Permalink
Browse files

Bugfix: during normalization we dealt incorrectly with props of the f…

…orm "t < x"
  • Loading branch information...
1 parent 66a2db2 commit 0000754b7a919b826c965d2f170e1409ac65c0b7 @yav committed Apr 27, 2009
Showing with 14 additions and 3 deletions.
  1. +14 −3 src/Data/Integer/Presburger/Prop.hs
@@ -37,13 +37,24 @@ norm x p = case prop p of
Bin op t1 t2
| k1 == k2 -> Ind p { prop = Bin op t1' t2' }
| k1 > k2 -> Norm p { prop = CVarP (k1 - k2) (NBin op (t2' - t1')) }
- | otherwise -> Norm Prop { prop = CVarP (k2 - k1) (NBin op (t1' - t2'))
- , negated = if op == Equal then negated p
- else not (negated p)
+ | otherwise -> Norm Prop { prop = CVarP (k2 - k1) (NBin op' (t1' - t2'))
+ , negated = neg'
}
+
where (k1,t1') = split_term x t1 -- t1 = k1 * x + t1'
(k2,t2') = split_term x t2 -- t2 = k2 * x + t2'
+ (neg',op') = case op of
+ Equal -> (negated p, Equal)
+ LessThan -> (not (negated p), LessThanEqual)
+ LessThanEqual -> (not (negated p), LessThan)
+
+ -- a < t --> same
+ -- Not (a < t) --> same
+ -- t < a --> Not (a =< t)
+ -- Not (t < a) --> a =< t
+
+
Divides n t1
| k1 == 0 -> Ind p
| k1 > 0 -> Norm p { prop = CVarP k1 (NDivides n t1') }

0 comments on commit 0000754

Please sign in to comment.