m4lvin / hascacbdd Goto Github PK

Problematic lines around here:

It seems that the original CacBdd does not provide a function to count the nodes of a BDD.

Ugly workaround which does not improve performance: Provide an Ord instance and use nubOrd instead of nub.

Ideally showGraph should "just work" in different environments:

• Linux with -Tx11
• macOS
• gitpod
• github codespaces
• when runing inside VS code or codium, write to PDF and open in editor

Currently too much in Data.HasCacBDD.Visuals is hard-coded, for example "/usr/bin/dot"

See ghc-proposals/ghc-proposals#440.

For consistency it might be good to also rename exists.

Instead of installing CacBDD to /usr/local/cacbdd we should pack everything into a single Haskell package that can be installed without sudo, just using cabal or stack. See https://github.com/davidcock/cudd where this has been done for CUDD.

see http://kailesu.net/CacBDD/

see https://hspec.github.io/

This is coming from jrclogic/SMCDEL#35, but is not specific to SMCDEL.

On a Mac M1 stack test fails with a segmentation fault.

We can run it with lldb as follows

• stack test
• find the tests executable somewhere in .stack-work/...
• run lldb .stack-work/whatever/the/path/is/tests
• inside (lldb) now run

We then get:

Examples
  Creating BDDs
    top == Top [ ]Declaring One and Zero
Done with One and Zero
Process 84341 stopped
* thread #5, name = 'ghc_worker', stop reason = EXC_BAD_ACCESS (code=1, address=0x68)
    frame #0: 0x000000010102b9fc tests`XBDDManager::BddOne(this=0x0000000102306ca0) at BDDNode.h:99:41
   96       ~XBDDManager(){ delete mgr; }
   97       void Clear(int varCnt){ mgr->Clear(varCnt); }
   98
-> 99       BDD  BddOne(){ return BDD(mgr, mgr->One);}
   100      BDD  BddZero(){ return BDD(mgr, mgr->Zero);}
   101      BDD  BddVar(int varIndex){ return BDD(mgr, varIndex); }
   102      BDD  Ite(const BDD &f, const BDD &g, const BDD &h){ return BDD(mgr, mgr->ite(f.node, g.node, h.node)); };
(lldb)

where "One" is underlined in line 99.

Moving mgr from private to public (which should not be necessary) delays the problem into the body of BDD(mgr, mgr->One) at BDDNode.cpp:48 and then there gives a EXC_BAD_ACCESS error too.

Notably, the C++ example cd cpp && make -f OriginalMakefile && ./t does work fine and not have these problems.

Ideas for further debugging:

• can we trigger the bug when only using C-to-C++ and not Haskell-to-C-to-C++ ?

Further information to collect:

• compiler versions used on mac os