alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

[buddy] Add a default_deleter for bddPair

Browse source 
* src/bddx.h (std::default_deleter<bddPair>): Here.
This commit is contained in:
Alexandre Duret-Lutz 2022-10-25 11:52:03 +02:00
parent 0ba6949f7d
commit 0ecc870a0e
1 changed files with 6 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

6
buddy/src/bddx.h
View file

@ -501,6 +501,7 @@ BUDDY_API_VAR const BDD bddtrue;
*************************************************************************/ *************************************************************************/
#ifdef CPLUSPLUS #ifdef CPLUSPLUS
#include <iostream> #include <iostream>
#include <memory>
/*=== User BDD class ===================================================*/ /*=== User BDD class ===================================================*/
@ -1092,6 +1093,11 @@ inline bddxfalse bdd_false(void)
{ return bddxfalse(); } { return bddxfalse(); }
template<>
struct std::default_delete<bddPair> {
void operator()(bddPair *p) const { bdd_freepair(p); };
};
/*=== Iostream printing ================================================*/ /*=== Iostream printing ================================================*/
class BUDDY_API bdd_ioformat class BUDDY_API bdd_ioformat