diff options
| author | letouzey | 2006-03-23 22:45:45 +0000 |
|---|---|---|
| committer | letouzey | 2006-03-23 22:45:45 +0000 |
| commit | f07866cd76ef06501da987084217d2206fc2ffc3 (patch) | |
| tree | 1f7738e6a23d073efcae43b377c634555572d692 /contrib/omega | |
| parent | de8e041c0c9ced8f91e934255de6a925bdcd9d0a (diff) | |
correctifs de bug pour romega:
1) dans refl_omega, on donnait a OmegaSolver un generateur de numero
d'equations new_eq_id qui pouvait clasher avec les numeros d'equations
initiaux créés avec new_omega_id.
=>
on sépare en deux compteurs, un pour les equations omegas, l'autre
pour les variables omegas. On en profite pour reinitialiser ces
compteurs à chaque session romega, histoire que romega devienne
reproductible.
2) dans omega.ml, le role de new_eq_id et new_var_id etait interverti
à un endroit.
ATTENTION: ceci peut changer le comportement d'omega. Surveiller le
resultat du prochain bench nocturne.
3) dans ReflOmegaCore.v, on ne traitait pas le cas d'une implication
dans une hypothese lors du recalcul final.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8657 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/omega')
| -rw-r--r-- | contrib/omega/omega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml index 69e57ca42e..fd774c16d0 100644 --- a/contrib/omega/omega.ml +++ b/contrib/omega/omega.ml @@ -512,7 +512,7 @@ let product new_eq_id dark_shadow low high = accu high) [] low -let fourier_motzkin (_,new_eq_id,print_var) dark_shadow system = +let fourier_motzkin (new_eq_id,_,print_var) dark_shadow system = let v = select_variable system in let (ineq_out, ineq_low,ineq_high) = classify v system in let expanded = ineq_out @ product new_eq_id dark_shadow ineq_low ineq_high in |