func (f *T) Push(c Id) {
	cls := &f.clauses[c]
	cls.level++
	if cls.level >= len(f.ids) {
		f.ids = append(f.ids, []Id{})
	}
	f.ids[cls.level] = append(f.ids[cls.level], c)
}
Push pushes the clause `c` forward one level.
If `c` is at the max level `f.K()`, then
`c` is queued for the next `PushK`
package cnf
import (
	"fmt"
	"io"
	"sort"
	"github.com/go-air/gini"
	"github.com/go-air/gini/inter"
	"github.com/go-air/gini/z"
	"github.com/go-air/reach/iic/internal/lits"
)
const (
	sanitize = true
)
type T struct {
	clauses []clause  
	ids     [][]Id    
	occs    [][]Id    
	free    []Id
	sat     *gini.Gini  
	lits    *lits.T     
	rmHook  func(f *T, rm, by Id, K int)
}
func New(sat *gini.Gini, d *lits.T) *T {
	return &T{sat: sat, lits: d, clauses: make([]clause, 1, 1024)}
}
func (f *T) Add(ms []z.Lit, k int) Id {
	sort.Slice(ms, func(i, j int) bool {
		return ms[i] < ms[j]
	})
	if sanitize {
		for i := 1; i < len(ms); i++ {
			if ms[i] == ms[i-1] {
				panic("ErrSanitize")
			}
		}
	}
	cls := f.newClause()
	f.ids[k] = append(f.ids[k], cls.id)
	cls.ms = f.lits.Put(ms)
	cls.sig = lits.CalcSig(ms)
	cls.level = k
	cls.rm = false
	sat := f.sat
	for _, m := range ms {
		sat.Add(m)
	}
	cls.act = sat.Activate()
	return cls.id
}
func (f *T) String(c Id) string {
	return fmt.Sprintf("%s %v", c, f.Lits(c))
}
func (f *T) Lits(c Id) []z.Lit {
	cl := &f.clauses[c]
	return f.lits.Get(cl.ms)
}
func (f *T) Len(c Id) int {
	cl := &f.clauses[c]
	return f.lits.Len(cl.ms)
}
func (f *T) Level(c Id) int {
	cls := &f.clauses[c]
	return cls.level
}
func (f *T) ActLit(c Id) z.Lit {
	cls := &f.clauses[c]
	return cls.act
}
func (f *T) K() int {
	return len(f.ids) - 1
}
func (f *T) PushK() {
	f.ids = append(f.ids, []Id{})
}
func (f *T) NumClauses() int {
	return len(f.clauses) - len(f.free) - 1
}
func (f *T) LenK(k int) int {
	ttl := 0
	f.Forall(k, func(_ *T, _ Id) {
		ttl++
	})
	return ttl
}
func (f *T) SetRemoveHook(fn func(f *T, rm, by Id, K int)) {
	f.rmHook = fn
}
func (f *T) Forall(k int, fn func(f *T, cls Id)) {
	j := 0
	var cls *clause
	ids := f.ids[k]
	for _, id := range ids {
		cls = &f.clauses[id]
		if cls.rmd() || cls.level != k {
			continue
		}
		fn(f, id)
		ids[j] = id
		j++
	}
	f.ids[k] = ids[:j]
}