Refactor solver preference searching.

This resolves a couple bugs in the solver's preference search. First,
multiple ordered constraints (i.e. Dependency) on a single
Installable are searched properly now. Second, the search will make a
selection for each dependency constraint in the solution, whereas
before it would bail as soon as it's known to be SAT.

Searching has also been refactored to be tested independently from
solving, with a fake of S.

Author: benluddy

pkg/controller/registry/resolver/solver/constraints.go

@@ -91,6 +91,9 @@ func Prohibited() Constraint {
 type dependency []Identifier
 
 func (constraint dependency) String(subject Identifier) string {
+	if len(constraint) == 0 {
+		return fmt.Sprintf("%s has a dependency without any candidates to satisfy it", subject)
+	}
 	s := make([]string, len(constraint))
 	for i, each := range constraint {
 		s[i] = string(each)

pkg/controller/registry/resolver/solver/lit_mapping.go

@@ -187,7 +187,7 @@ func (d *litMapping) Lits(dst []z.Lit) []z.Lit {
 	return dst
 }
 
-func (d *litMapping) Conflicts(g inter.S) []AppliedConstraint {
+func (d *litMapping) Conflicts(g inter.Assumable) []AppliedConstraint {
 	whys := g.Why(nil)
 	as := make([]AppliedConstraint, 0, len(whys))
 	for _, why := range whys {

pkg/controller/registry/resolver/solver/search.go

@@ -0,0 +1,219 @@
+package solver
+
+import (
+	"context"
+
+	"github.com/irifrance/gini/inter"
+	"github.com/irifrance/gini/z"
+)
+
+type choice struct {
+	prev, next *choice
+	index      int // index of next unguessed literal
+	candidates []z.Lit
+}
+
+type guess struct {
+	m          z.Lit // if z.LitNull, this choice was satisfied by a previous assumption
+	index      int   // index of guessed literal in candidates
+	children   int   // number of choices introduced by making this guess
+	candidates []z.Lit
+}
+
+type search struct {
+	s                      inter.S
+	lits                   *litMapping
+	assumptions            map[z.Lit]struct{} // set of assumed lits - duplicates guess stack - for fast lookup
+	guesses                []guess            // stack of assumed guesses
+	headChoice, tailChoice *choice            // deque of unmade choices
+	heap                   []choice
+	position               int
+	tracer                 Tracer
+	result                 int
+	buffer                 []z.Lit
+}
+
+func (h *search) PushGuess() {
+	c := h.PopChoiceFront()
+	g := guess{
+		m:          z.LitNull,
+		index:      c.index,
+		candidates: c.candidates,
+	}
+	if g.index < len(g.candidates) {
+		g.m = g.candidates[g.index]
+	}
+
+	// Check whether or not this choice can be satisfied by an
+	// existing assumption.
+	for _, m := range g.candidates {
+		if _, ok := h.assumptions[m]; ok {
+			g.m = z.LitNull
+			break
+		}
+	}
+
+	h.guesses = append(h.guesses, g)
+	if g.m == z.LitNull {
+		return
+	}
+
+	installable := h.lits.InstallableOf(g.m)
+	for _, constraint := range installable.Constraints() {
+		var ms []z.Lit
+		for _, dependency := range constraint.order() {
+			ms = append(ms, h.lits.LitOf(dependency))
+		}
+		if len(ms) > 0 {
+			h.guesses[len(h.guesses)-1].children++
+			h.PushChoiceBack(choice{candidates: ms})
+		}
+	}
+
+	if h.assumptions == nil {
+		h.assumptions = make(map[z.Lit]struct{})
+	}
+	h.assumptions[g.m] = struct{}{}
+	h.s.Assume(g.m)
+	h.result, h.buffer = h.s.Test(h.buffer)
+}
+
+func (h *search) PopGuess() {
+	g := h.guesses[len(h.guesses)-1]
+	h.guesses = h.guesses[:len(h.guesses)-1]
+	if g.m != z.LitNull {
+		delete(h.assumptions, g.m)
+		h.result = h.s.Untest()
+	}
+	for g.children > 0 {
+		g.children--
+		h.PopChoiceBack()
+	}
+	c := choice{
+		index:      g.index,
+		candidates: g.candidates,
+	}
+	if g.m != z.LitNull {
+		c.index++
+	}
+	h.PushChoiceFront(c)
+}
+
+func (h *search) PushChoiceFront(c choice) {
+	if h.headChoice == nil {
+		h.headChoice = &c
+		h.tailChoice = &c
+		return
+	}
+	h.headChoice.prev = &c
+	c.next = h.headChoice
+	h.headChoice = &c
+}
+
+func (h *search) PopChoiceFront() choice {
+	c := h.headChoice
+	if c.next != nil {
+		c.next.prev = nil
+	} else {
+		h.tailChoice = nil
+	}
+	h.headChoice = c.next
+	return *c
+
+}
+func (h *search) PushChoiceBack(c choice) {
+	if h.tailChoice == nil {
+		h.headChoice = &c
+		h.tailChoice = &c
+		return
+	}
+	h.tailChoice.next = &c
+	c.prev = h.tailChoice
+	h.tailChoice = &c
+}
+
+func (h *search) PopChoiceBack() choice {
+	c := h.tailChoice
+	if c.prev != nil {
+		c.prev.next = nil
+	} else {
+		h.headChoice = nil
+	}
+	h.tailChoice = c.prev
+	return *c
+}
+
+func (h *search) Result() int {
+	return h.result
+}
+
+func (h *search) Lits() []z.Lit {
+	result := make([]z.Lit, 0, len(h.guesses))
+	for _, g := range h.guesses {
+		if g.m != z.LitNull {
+			result = append(result, g.m)
+		}
+	}
+	return result
+}
+
+func (h *search) Do(ctx context.Context, anchors []z.Lit) (int, []z.Lit, map[z.Lit]struct{}) {
+	for _, m := range anchors {
+		h.PushChoiceBack(choice{candidates: []z.Lit{m}})
+	}
+
+	for {
+		// Need to have a definitive result once all choices
+		// have been made to decide whether to end or
+		// backtrack.
+		if h.headChoice == nil && h.result == unknown {
+			h.result = h.s.Solve()
+		}
+
+		// Backtrack if possible, otherwise end.
+		if h.result == unsatisfiable {
+			h.tracer.Trace(h)
+			if len(h.guesses) == 0 {
+				break
+			}
+			h.PopGuess()
+			continue
+		}
+
+		// Satisfiable and no decisions left!
+		if h.headChoice == nil {
+			break
+		}
+
+		// Possibly SAT, keep guessing.
+		h.PushGuess()
+	}
+
+	lits := h.Lits()
+	set := make(map[z.Lit]struct{}, len(lits))
+	for _, m := range lits {
+		set[m] = struct{}{}
+	}
+	result := h.Result()
+
+	// Go back to the initial test scope.
+	for len(h.guesses) > 0 {
+		h.PopGuess()
+	}
+
+	return result, lits, set
+}
+
+func (h *search) Installables() []Installable {
+	result := make([]Installable, 0, len(h.guesses))
+	for _, g := range h.guesses {
+		if g.m != z.LitNull {
+			result = append(result, h.lits.InstallableOf(g.candidates[g.index]))
+		}
+	}
+	return result
+}
+
+func (h *search) Conflicts() []AppliedConstraint {
+	return h.lits.Conflicts(h.s)
+}

pkg/controller/registry/resolver/solver/search_test.go

@@ -0,0 +1,105 @@
+//go:generate go run github.com/maxbrunsfeld/counterfeiter/v6 -o zz_search_test.go ../../../../../vendor/github.com/irifrance/gini/inter S
+
+package solver
+
+import (
+	"context"
+	"testing"
+
+	"github.com/irifrance/gini/inter"
+	"github.com/irifrance/gini/z"
+	"github.com/stretchr/testify/assert"
+)
+
+type TestScopeCounter struct {
+	depth *int
+	inter.S
+}
+
+func (c *TestScopeCounter) Test(dst []z.Lit) (result int, out []z.Lit) {
+	result, out = c.S.Test(dst)
+	*c.depth++
+	return
+}
+
+func (c *TestScopeCounter) Untest() (result int) {
+	result = c.S.Untest()
+	*c.depth--
+	return
+}
+
+func TestSearch(t *testing.T) {
+	type tc struct {
+		Name          string
+		Installables  []Installable
+		TestReturns   []int
+		UntestReturns []int
+		Result        int
+		Assumptions   []Identifier
+	}
+
+	for _, tt := range []tc{
+		{
+			Name: "children popped from back of deque when guess popped",
+			Installables: []Installable{
+				installable("a", Mandatory(), Dependency("c")),
+				installable("b", Mandatory()),
+				installable("c"),
+			},
+			TestReturns:   []int{0, -1},
+			UntestReturns: []int{-1, -1},
+			Result:        -1,
+			Assumptions:   nil,
+		},
+		{
+			Name: "candidates exhausted",
+			Installables: []Installable{
+				installable("a", Mandatory(), Dependency("x")),
+				installable("b", Mandatory(), Dependency("y")),
+				installable("x"),
+				installable("y"),
+			},
+			TestReturns:   []int{0, 0, -1, 1},
+			UntestReturns: []int{0},
+			Result:        1,
+			Assumptions:   []Identifier{"a", "b", "y"},
+		},
+	} {
+		t.Run(tt.Name, func(t *testing.T) {
+			assert := assert.New(t)
+
+			var s FakeS
+			for i, result := range tt.TestReturns {
+				s.TestReturnsOnCall(i, result, nil)
+			}
+			for i, result := range tt.UntestReturns {
+				s.UntestReturnsOnCall(i, result)
+			}
+
+			var depth int
+			counter := &TestScopeCounter{depth: &depth, S: &s}
+
+			lits := newLitMapping(tt.Installables)
+			h := search{
+				s:      counter,
+				lits:   lits,
+				tracer: DefaultTracer{},
+			}
+
+			var anchors []z.Lit
+			for _, id := range h.lits.MandatoryIdentifiers() {
+				anchors = append(anchors, h.lits.LitOf(id))
+			}
+
+			result, ms, _ := h.Do(context.Background(), anchors)
+
+			assert.Equal(tt.Result, result)
+			var ids []Identifier
+			for _, m := range ms {
+				ids = append(ids, lits.InstallableOf(m).Identifier())
+			}
+			assert.Equal(tt.Assumptions, ids)
+			assert.Equal(0, depth)
+		})
+	}
+}