: → 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