summaryrefslogtreecommitdiff
path: root/abstract/varenv.ml
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-11 14:50:18 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-11 14:50:18 +0200
commitfd027ca593bdfb2d2db811730521b4f5d52c8593 (patch)
tree94982e74c74a480e9bafd235101d1934a330439e /abstract/varenv.ml
parent9ca8bcb35eb0385c8f9852045bb282c445bd6901 (diff)
downloadscade-analyzer-fd027ca593bdfb2d2db811730521b4f5d52c8593.tar.gz
scade-analyzer-fd027ca593bdfb2d2db811730521b4f5d52c8593.zip
Acceptable heuristic.
Diffstat (limited to 'abstract/varenv.ml')
-rw-r--r--abstract/varenv.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/abstract/varenv.ml b/abstract/varenv.ml
index 450bef3..4d6caca 100644
--- a/abstract/varenv.ml
+++ b/abstract/varenv.ml
@@ -256,6 +256,12 @@ let mk_varenv (rp : rooted_prog) f cl =
let ev_order = Hashtbl.create (List.length evars) in
List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
+ let enum_vars = List.sort
+ (fun (id1, _) (id2, _) ->
+ compare (Hashtbl.find ev_order id1) (Hashtbl.find ev_order id2))
+ enum_vars
+ in
+
Format.printf "Order for variables: @[<hov>[%a]@]@."
(print_list Formula_printer.print_id ", ") evars_ord;