hkernel.go

// Copyright (c) 2021 Silvano DAL ZILIO
//
// MIT License

// +build !buddy

package rudd

import (
	"log"
	"math"
	"runtime"
	"sync/atomic"
)

// Retnode is a kernel function of the BDD package. Use it at your own risk.
// Retnode returns a valid node from the value returned by a call to Makenode.
func (b *tables) Retnode(n int) Node {
	if n < 0 || n > len(b.nodes) {
		if _DEBUG {
			log.Panicf("b.retnode(%d) not valid\n", n)
		}
		return nil
	}
	if n == 0 {
		return bddzero
	}
	if n == 1 {
		return bddone
	}
	x := n
	if b.nodes[n].refcou < _MAXREFCOUNT {
		b.nodes[n].refcou++
		runtime.SetFinalizer(&x, b.nodefinalizer)
		if _DEBUG {
			atomic.AddUint64(&(b.setfinalizers), 1)
			if _LOGLEVEL > 2 {
				log.Printf("inc refcou %d\n", n)
			}
		}
	}
	return &x
}

func (b *tables) makenode(level int32, low int, high int, refstack []int) (int, error) {
	if _DEBUG {
		b.uniqueAccess++
	}
	// check whether children are equal, in which case we can skip the node
	if low == high {
		return low, nil
	}
	// otherwise try to find an existing node using the unique table
	if res, ok := b.nodehash(level, low, high); ok {
		if _DEBUG {
			b.uniqueHit++
		}
		return res, nil
	}
	if _DEBUG {
		b.uniqueMiss++
	}
	// If no existing node, we build one. If there is no available spot
	// (b.freepos == 0), we try garbage collection and, as a last resort,
	// resizing the BDD list.
	var err error
	if b.freepos == 0 {
		// We garbage collect unused nodes to try and find spare space.
		b.gbc(refstack)
		err = errReset
		// We also test if we are under the threshold for resising.
		if (b.freenum*100)/len(b.nodes) <= b.minfreenodes {
			err = b.noderesize()
			if err != errResize {
				return -1, errMemory
			}
		}
		// Panic if we still have no free positions after all this
		if b.freepos == 0 {
			// b.seterror("Unable to resize BDD")
			return -1, errMemory
		}
	}
	// We can now build the new node in the first available spot
	b.produced++
	return b.setnode(level, low, high, 0), err
}

func (b *tables) gbc(refstack []int) {
	if _LOGLEVEL > 0 {
		log.Println("starting GC")
	}

	// runtime.GC()

	// we append the current stats to the GC history
	if _DEBUG {
		b.gcstat.history = append(b.gcstat.history, gcpoint{
			nodes:            len(b.nodes),
			freenodes:        b.freenum,
			setfinalizers:    int(b.gcstat.setfinalizers),
			calledfinalizers: int(b.gcstat.calledfinalizers),
		})
		if _LOGLEVEL > 0 {
			log.Printf("runtime.GC() reclaimed %d references\n", b.gcstat.calledfinalizers)
		}
		b.gcstat.setfinalizers = 0
		b.gcstat.calledfinalizers = 0
	} else {
		b.gcstat.history = append(b.gcstat.history, gcpoint{
			nodes:     len(b.nodes),
			freenodes: b.freenum,
		})
	}
	// we mark the nodes in the refstack to avoid collecting them
	for _, r := range refstack {
		b.markrec(int(r))
	}
	// we also protect nodes with a positive refcount (and therefore also the
	// ones with a MAXREFCOUNT, such has variables)
	for k := range b.nodes {
		if b.nodes[k].refcou > 0 {
			b.markrec(k)
		}
	}
	b.freepos = 0
	b.freenum = 0
	// we do a pass through the nodes list to void the unmarked nodes. After
	// finishing this pass, b.freepos points to the first free position in
	// b.nodes, or it is 0 if we found none.
	for n := len(b.nodes) - 1; n > 1; n-- {
		if b.ismarked(n) && (b.nodes[n].low != -1) {
			b.unmarknode(n)
		} else {
			b.delnode(b.nodes[n])
			b.nodes[n].low = -1
			b.nodes[n].high = b.freepos
			b.freepos = n
			b.freenum++
		}
	}
	// we also invalidate the caches
	// b.cachereset()
	if _LOGLEVEL > 0 {
		log.Printf("end GC; freenum: %d\n", b.freenum)
	}
}

func (b *tables) noderesize() error {
	if _LOGLEVEL > 0 {
		log.Printf("start resize: %d\n", len(b.nodes))
	}
	// if b.error != nil {
	// 	b.seterror("Error before resizing; %s", b.error)
	// 	return b.error
	// }
	oldsize := len(b.nodes)
	nodesize := len(b.nodes)
	if (oldsize >= b.maxnodesize) && (b.maxnodesize > 0) {
		// b.seterror("Cannot resize BDD, already at max capacity (%d nodes)", b.maxnodesize)
		return errMemory
	}
	if oldsize > (math.MaxInt32 >> 1) {
		nodesize = math.MaxInt32 - 1
	} else {
		nodesize = nodesize << 1
	}
	if b.maxnodeincrease > 0 && nodesize > (oldsize+b.maxnodeincrease) {
		nodesize = oldsize + b.maxnodeincrease
	}
	if (nodesize > b.maxnodesize) && (b.maxnodesize > 0) {
		nodesize = b.maxnodesize
	}
	if nodesize <= oldsize {
		// b.seterror("Unable to grow size of BDD (%d nodes)", nodesize)
		return errMemory
	}

	tmp := b.nodes
	b.nodes = make([]huddnode, nodesize)
	copy(b.nodes, tmp)

	for n := oldsize; n < nodesize; n++ {
		b.nodes[n].refcou = 0
		b.nodes[n].level = 0
		b.nodes[n].low = -1
		b.nodes[n].high = n + 1
	}
	b.nodes[nodesize-1].high = b.freepos
	b.freepos = oldsize
	b.freenum += (nodesize - oldsize)

	// b.cacheresize(len(b.nodes))

	if _LOGLEVEL > 0 {
		log.Printf("end resize: %d\n", len(b.nodes))
	}

	return errResize
}

func (b *tables) markrec(n int) {
	if n < 2 || b.ismarked(n) || (b.nodes[n].low == -1) {
		return
	}
	b.marknode(n)
	b.markrec(b.nodes[n].low)
	b.markrec(b.nodes[n].high)
}

func (b *tables) unmarkall() {
	for k, v := range b.nodes {
		if k < 2 || !b.ismarked(k) || (v.low == -1) {
			continue
		}
		b.unmarknode(k)
	}
}