: → kaie819:另外，想請教程式中nodeMove的問題，是不是沒有node就不能 04/29 00:05
: → kaie819:做move，例如tautology，所以move前必須自己檢查嗎？ 04/29 00:09
: → kaie819:像如果next state(Y)沒node，這樣要移到current state(X) 04/29 00:12
: → kaie819:似乎就會出現`thisLevel >= fromLevel'的assertion fail 04/29 00:13
Let me copy the source code of the function BddNode::nodeMove() here

所以沒有 node (tautology) 的確是會 crash... 請檢查一下再呼叫此 function.

我不太懂nodeMove這個function...所有大於fromlevel的level都會搬動的意思嗎？也就是這個function只呼叫一次？

是的，一次搬到定位。就是用在將 X 搬到 Y 或是 Y 搬到 X