diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-26 19:20:47 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-26 19:20:47 +0200 |
| commit | 4445158c58756a315dbbbf5773fc691dd61b61f1 (patch) | |
| tree | 8104ccc88b757002a2437b42cad489901588a75f /plugins/omega | |
| parent | 06aa7498415ca98a795219a2b1460e812b6bafc6 (diff) | |
| parent | 9bf766d4f66727a638ed2662099d090b5a72200a (diff) | |
Merge PR#666: romega revisited : no more normalization trace, cleaned-up resolution trace
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/omega.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index 334b03de1..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 } @@ -587,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 |