diff options
| author | herbelin | 2002-01-18 16:50:32 +0000 |
|---|---|---|
| committer | herbelin | 2002-01-18 16:50:32 +0000 |
| commit | b690cf1a76d33afc878ba9a51de414560209e8e8 (patch) | |
| tree | 79865e212174fe71205969df8d8d280191214797 | |
| parent | 07fa62e2c1b7045eb8d845e76d1d7e0b6fce0760 (diff) | |
Bug MERGE_EQ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2416 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rwxr-xr-x | contrib/omega/omega.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml index 6d78494a22..23236bc3cc 100755 --- a/contrib/omega/omega.ml +++ b/contrib/omega/omega.ml @@ -225,6 +225,9 @@ let map_eq_afine f e = let negate_eq = map_eq_afine (fun x -> -x) +let opposite x y = + map_eq_linear (fun x -> - x) x.body = y.body & x.constant = y.constant + let rec sum p0 p1 = match (p0,p1) with | ([], l) -> l | (l, []) -> l | (((x1::l1) as l1'), ((x2::l2) as l2')) -> @@ -406,7 +409,7 @@ let redundancy_elimination system = let accu_ineq = ref [] in iter (fun p0 p1 -> match (p0,p1) with - | (e, (Some x, Some y)) when x.constant = -y.constant -> + | (e, (Some x, Some y)) when opposite x y -> let id=new_id () in add_event (MERGE_EQ(id,x,y.id)); push {id=id; kind=EQUA; body=x.body; constant=x.constant} accu_eq |