Rocket

https://mp.weixin.qq.com/s/CbBWdTlc_DESlUzd8KFcSg

 
介绍Term类各方法的实现。
 
 
 
1. prime
 
表示一个项是否是质项,即这个项是否被其他项包含。如项AB包含项ABC。
 
2. covers
 
 
this covers x,即项this包含项x,包含两点:
a. 项this包含的变量比项x少:x.mask &~ mask
b. 项this包含的变量的值与项x相同:(value ^ x.value) &~ mask
 
如包含ABC三变量的项:AB(value: 110, mask: 001),ABC(value: 111, mask: 000)
AB covers ABC: ((110 ^ 111) &~ 001) | (000 &~ 001) == 0
 
3. intersects
 
 
this intersects x,即项this与项x相交,也包含两点:
a. 项this与项x有共同的变量:~mask & ~x.mask
b. 且共同的变量值都相同:(value ^ x.value) & (~mask & ~x.mask)
 
4. equals
 
 
this equals that,即项this与项that相等,需要两者的value和mask都相等。
 
5. <
 
 
this < that,即项this小于项that,包含两种情况:
a. this的值小于that的值;
b. 值相等,但this.mask小于that.mask;
 
小于判断用于项之间的排序,并无特殊的意义。
 
6. similar
 
 
this similar x, 即项this与项x相似,包含三个条件:
a. mask相等:mask == x.mask
b. this.value > x.value
c. this和x的值只差一个变量(差值为2的幂):(diff & diff - 1) == 0
 
如:ABC(值为111) similar AB'C(值为101)。
 
7. merge
 
 
this merge x,需要this similar x,如ABC merge AB'C = AC,
a. 取出不同的变量:val bit = value - x.value
b. 把value中相应变量对应的位清0:value &~ bit
c. 把mask中相应变量对应的位置1:mask | bit
 
在合并生成的新项(Term)中,合并的变量对应的value位为0,对应的mask位为1,以表明这个变量在Term中不存在。
 
合并生成的新项是一个质项,而被合并的两项则不再是质项了。
 
原文地址:https://www.cnblogs.com/wjcdx/p/10295016.html