From 99c1b607de84cfa13c8e37fbbb450c5da3658e05 Mon Sep 17 00:00:00 2001 From: Felix Abecassis Date: Fri, 26 Mar 2010 17:31:58 +0100 Subject: [PATCH] * src/tgbaalgos/minimize.cc: Now use register_anonymous_variables. --- ChangeLog | 4 ++++ src/tgbaalgos/minimize.cc | 7 ++++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/ChangeLog b/ChangeLog index 9f02e272c..a9d0d0448 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2010-03-26 Felix Abecassis + + * src/tgbaalgos/minimize.cc: Now use register_anonymous_variables. + 2010-03-20 Felix Abecassis Small fixes. diff --git a/src/tgbaalgos/minimize.cc b/src/tgbaalgos/minimize.cc index cd81f11e4..93b42fdb3 100644 --- a/src/tgbaalgos/minimize.cc +++ b/src/tgbaalgos/minimize.cc @@ -143,10 +143,14 @@ namespace spot hash_set* final = new hash_set; hash_set* non_final = new hash_set; hash_map state_set_map; + bdd_dict* dict = det_a->get_dict(); std::list::iterator li; for (li = acc_list.begin(); li != acc_list.end(); ++li) final->insert(*li); init_sets(det_a, *final, *non_final, state_set_map); + // Size of det_a + unsigned size = final->size() + non_final->size(); + unsigned bdd_offset = dict->register_anonymous_variables(size, det_a); hash_set* final_copy = new hash_set(*final); if (final->size() > 1) todo.push(final); @@ -178,7 +182,7 @@ namespace spot const state* dst = si->current_state(); unsigned dst_set = state_set_map[dst]; delete dst; - f |= (bdd_ithvar(dst_set) & si->current_condition()); + f |= (bdd_ithvar(bdd_offset + dst_set) & si->current_condition()); } delete si; bdd_states_map::iterator bsi; @@ -227,6 +231,7 @@ namespace spot // Build the result. tgba_explicit_number* res = build_result(det_a, done, final_copy); + dict->unregister_variable(bdd_offset, det_a); // Free all the allocated memory. delete final_copy; hash_map::iterator hit;