documentation cleanup + unroll Len/MaxLen

logic/c.go

@@ -150,23 +150,20 @@ func (p *C) CnfSince(dst inter.Adder, mark []int8, roots ...z.Lit) ([]int8, int)
 	return mark, ttl
 }
 
-// Len returns the length of C, the number of
-// internal nodes used to represent C.
+// Len returns the length of C, the number of internal nodes used to represent
+// C.
 func (c *C) Len() int {
 	return len(c.nodes)
 }
 
-// At returns the i'th element.  Elements from
-// 0..Len(c) are in topological order:  if i < j
-// then c.At(j) is not reachable from c.At(i)
-// via the edge relation defined by c.Ins().
-// All elements are positive literals.
+// At returns the i'th element.  Elements from 0..Len(c) are in topological
+// order:  if i < j then c.At(j) is not reachable from c.At(i) via the edge
+// relation defined by c.Ins().  All elements are positive literals.
 //
-// One variable for internal use, with index 1, is created when
-// c is created.  All other variables created by NewIn, And, ...
-// are created in sequence starting with index 2.  Internal
-// variables may be created by c.  c.Len() - 1 is the maximal
-// index of a variable.
+// One variable for internal use, with index 1, is created when c is created.
+// All other variables created by NewIn, And, ...  are created in sequence
+// starting with index 2.  Internal variables may be created by c.  c.Len() - 1
+// is the maximal index of a variable.
 //
 // Hence, the implementation of At(i) is simply z.Var(i).Pos().
 func (c *C) At(i int) z.Lit {

logic/s.go

@@ -94,9 +94,15 @@ func (s *S) Init(latch z.Lit) z.Lit {
 	return s.nodes[v].a
 }
 
-func (s *S) SetInit(latch, nxt z.Lit) {
+// SetInit sets the initial state of 'latch' to 'nxt'.  'nxt' should be either
+// z.LitNull, s.T, or s.F.  If it is not, SetInit panics.  If 'latch' is not
+// a latch, then subsequent operations on s are undefined.
+func (s *S) SetInit(latch, init z.Lit) {
+	if init != s.F && init != s.T && init != z.LitNull {
+		panic("invalid initial value")
+	}
 	v := latch.Var()
-	s.nodes[v].a = nxt
+	s.nodes[v].a = init
 }
 
 // type of node type

logic/unroll.go

@@ -22,6 +22,27 @@ func NewUnroll(s *S) *Unroll {
 	return u
 }
 
+// Len returns the length of the unrolling for literal m.
+func (u *Unroll) Len(m z.Lit) int {
+	v := m.Var()
+	return len(u.dmap[v])
+}
+
+// MaxLen returns the maximum length of any literal in
+// the unrolling.
+func (u *Unroll) MaxLen() int {
+	ns := u.S.nodes
+	max := 0
+	for i := 1; i < len(ns); i++ {
+		v := z.Var(i)
+		n := len(u.dmap[v])
+		if n > max {
+			max = n
+		}
+	}
+	return max
+}
+
 // At returns the value of literal m from sequential circuit
 // u.S at time/depth d as a literal in u.C
 //