diff options
Diffstat (limited to 'plugins/omega/omega.ml')
| -rw-r--r-- | plugins/omega/omega.ml | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index bd991a955..2a018fa3f 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -96,7 +96,7 @@ type afine = { type state_action = { st_new_eq : afine; - st_def : afine; + st_def : afine; (* /!\ this represents [st_def = st_var] *) st_orig : afine; st_coef : bigint; st_var : int } @@ -330,11 +330,13 @@ let omega_mod a b = a - b * floor_div (two * a + b) (two * b) let banerjee_step (new_eq_id,new_var_id,print_var) original l1 l2 = let e = original.body in let sigma = new_var_id () in + if e == [] then begin + display_system print_var [original] ; failwith "TL" + end; let smallest,var = - try - List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p)) - (abs (List.hd e).c, (List.hd e).v) (List.tl e) - with Failure "tl" -> display_system print_var [original] ; failwith "TL" in + List.fold_left (fun (v,p) c -> if v >? (abs c.c) then abs c.c,c.v else (v,p)) + (abs (List.hd e).c, (List.hd e).v) (List.tl e) + in let m = smallest + one in let new_eq = { constant = omega_mod original.constant m; @@ -585,10 +587,6 @@ let rec depend relie_on accu = function end | [] -> relie_on, accu -let solve (new_eq_id,new_eq_var,print_var) system = - try let _ = simplify new_eq_id false system in failwith "no contradiction" - with UNSOLVABLE -> display_action print_var (snd (depend [] [] (history ()))) - let negation (eqs,ineqs) = let diseq,_ = List.partition (fun e -> e.kind = DISE) ineqs in let normal = function |