memo about weaver

[shnarazk]

これが最終稿

• weave (ci): overwrite both refs
• reweave (ci, wi, wj): unlink a ref, swap lits, then link the ref, ただしwi = wj ならfree listに繋ぐ
• unweave (ci, wi): unlink a ref (これはfree listへの回収ではない。部分的切り離しに相当）

Combination of them

• to kill a clause (= add to free list), unweave then reweave to FREE_LIT
• to add a new clause, just weave
• to propagate, just reweave
• to fetch a clause from free list, just reweave from FREE_LIT

another simple but not-optimal solution

• weave (ci, wi): overwrite a ref
• unweave (ci, wi): unlink a ref

Combination of them

• to kill a clause (= add to free list), unweave, unweave, then weave to FREE_LIT
• to add a new clause, weave and weave
• to propagate, unweave, swap two lots, then weave
• to fetch a clause from free list, unweave from FREE_LIT then weave

weaveしている感があまりない。unweave weaveに対してショートカットがあるべき。