diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 8b2367339..94d1855fb 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -54,7 +54,6 @@ misc_HEADERS = \ satsolver.hh \ timer.hh \ tmpfile.hh \ - unique_ptr.hh \ version.hh noinst_LTLIBRARIES = libmisc.la diff --git a/src/misc/unique_ptr.hh b/src/misc/unique_ptr.hh deleted file mode 100644 index 61fc02741..000000000 --- a/src/misc/unique_ptr.hh +++ /dev/null @@ -1,88 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#ifndef SPOT_MISC_UNIQUE_PTR_HH -# define SPOT_MISC_UNIQUE_PTR_HH - -namespace spot -{ - /// \brief Take ownership of a pointer at its construction, and - /// destroy it at the end of the scope. - template - class unique_ptr - { - typedef T* pointer; - typedef const T* const_pointer; - public: - unique_ptr(pointer ptr) - : ptr_(ptr) - { - } - - ~unique_ptr() - { - delete ptr_; - } - - operator pointer() - { - return ptr_; - } - - pointer - operator->() - { - return ptr_; - } - - const_pointer - operator->() const - { - return ptr_; - } - - private: - pointer ptr_; - - // This copy gives the ownership of the pointer to the new copy. - // Can only be used by make_unique. - unique_ptr(const unique_ptr& up) - { - unique_ptr& non_const_up = const_cast(up); - ptr_ = non_const_up.ptr_; - non_const_up.ptr_ = 0; - } - - // Allow `make_unique' to have an access to the private copy. - template friend unique_ptr make_unique(V* ptr); - - unique_ptr& operator=(const unique_ptr&); - }; - - - /// \brief Change a pointer into a unique_ptr. - template - inline unique_ptr make_unique(T* ptr) - { - return unique_ptr(ptr); - } -} - - -#endif // !SPOT_MISC_UNIQUE_PTR_HH diff --git a/src/tgbaalgos/simulation.cc b/src/tgbaalgos/simulation.cc index c2c884d3d..dee758b3e 100644 --- a/src/tgbaalgos/simulation.cc +++ b/src/tgbaalgos/simulation.cc @@ -26,7 +26,6 @@ #include "simulation.hh" #include "priv/acccompl.hh" #include "misc/minato.hh" -#include "misc/unique_ptr.hh" #include "tgba/bddprint.hh" #include "tgbaalgos/reachiter.hh" #include "tgbaalgos/sccfilter.hh" @@ -1599,25 +1598,28 @@ namespace spot { prev = next; direct_simulation simul(res); - tgba* maybe_res = simul.run(); + tgba* after_simulation = simul.run(); if (res != t) delete res; if (simul.result_is_deterministic()) { - res = maybe_res; + res = after_simulation; break; } - unique_ptr after_simulation(maybe_res); direct_simulation cosimul(after_simulation); - unique_ptr after_cosimulation(cosimul.run()); + tgba* after_cosimulation = cosimul.run(); next = cosimul.get_stat(); + + delete after_simulation; + if (Sba) res = scc_filter_states(after_cosimulation); else res = scc_filter(after_cosimulation, false); + delete after_cosimulation; } while (prev != next); return res; @@ -1663,15 +1665,18 @@ namespace spot { prev = next; - unique_ptr after_simulation(dont_care_simulation(res, limit)); + tgba* after_simulation = dont_care_simulation(res, limit); if (res != t) delete res; direct_simulation cosimul(after_simulation); - unique_ptr after_cosimulation(cosimul.run()); + tgba* after_cosimulation = cosimul.run(); + delete after_simulation; + next = cosimul.get_stat(); res = scc_filter(after_cosimulation, true); + delete after_cosimulation; } while (prev != next); diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 7ab4c93a0..6c52e4f2b 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -58,7 +58,6 @@ #include "tgbaalgos/gtec/gtec.hh" #include "eltlparse/public.hh" #include "misc/timer.hh" -#include "misc/unique_ptr.hh" #include "tgbaalgos/stats.hh" #include "tgbaalgos/scc.hh" #include "tgbaalgos/emptiness_stats.hh" @@ -1789,12 +1788,12 @@ main(int argc, char** argv) // It is possible that we have applied other // operations to the automaton since its initial // degeneralization. Let's degeneralize again! - spot::unique_ptr - s(spot::degeneralize(a, - degen_reset, - degen_order, - degen_cache)); + spot::tgba* s = spot::degeneralize(a, + degen_reset, + degen_order, + degen_cache); spot::never_claim_reachable(std::cout, s, f, spin_comments); + delete s; } break; } @@ -1997,9 +1996,10 @@ main(int argc, char** argv) } else if (graph_run_tgba_opt) { - spot::unique_ptr - ar(spot::tgba_run_to_tgba(a, run)); + spot::tgba* ar = + spot::tgba_run_to_tgba(a, run); spot::dotty_reachable(std::cout, ar, false); + delete ar; } else {