Skip to content

Commit 1260c13

Browse files
committed
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.
1 parent 1a55d77 commit 1260c13

File tree

7 files changed

+1265
-230
lines changed

7 files changed

+1265
-230
lines changed

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,6 +91,9 @@ func Prohibited() Constraint {
9191
type dependency []Identifier
9292

9393
func (constraint dependency) String(subject Identifier) string {
94+
if len(constraint) == 0 {
95+
return fmt.Sprintf("%s has a dependency without any candidates to satisfy it", subject)
96+
}
9497
s := make([]string, len(constraint))
9598
for i, each := range constraint {
9699
s[i] = string(each)

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -187,7 +187,7 @@ func (d *litMapping) Lits(dst []z.Lit) []z.Lit {
187187
return dst
188188
}
189189

190-
func (d *litMapping) Conflicts(g inter.S) []AppliedConstraint {
190+
func (d *litMapping) Conflicts(g inter.Assumable) []AppliedConstraint {
191191
whys := g.Why(nil)
192192
as := make([]AppliedConstraint, 0, len(whys))
193193
for _, why := range whys {
Lines changed: 219 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,219 @@
1+
package solver
2+
3+
import (
4+
"context"
5+
6+
"github.com/irifrance/gini/inter"
7+
"github.com/irifrance/gini/z"
8+
)
9+
10+
type choice struct {
11+
prev, next *choice
12+
index int // index of next unguessed literal
13+
candidates []z.Lit
14+
}
15+
16+
type guess struct {
17+
m z.Lit // if z.LitNull, this choice was satisfied by a previous assumption
18+
index int // index of guessed literal in candidates
19+
children int // number of choices introduced by making this guess
20+
candidates []z.Lit
21+
}
22+
23+
type search struct {
24+
s inter.S
25+
lits *litMapping
26+
assumptions map[z.Lit]struct{} // set of assumed lits - duplicates guess stack - for fast lookup
27+
guesses []guess // stack of assumed guesses
28+
headChoice, tailChoice *choice // deque of unmade choices
29+
heap []choice
30+
position int
31+
tracer Tracer
32+
result int
33+
buffer []z.Lit
34+
}
35+
36+
func (h *search) PushGuess() {
37+
c := h.PopChoiceFront()
38+
g := guess{
39+
m: z.LitNull,
40+
index: c.index,
41+
candidates: c.candidates,
42+
}
43+
if g.index < len(g.candidates) {
44+
g.m = g.candidates[g.index]
45+
}
46+
47+
// Check whether or not this choice can be satisfied by an
48+
// existing assumption.
49+
for _, m := range g.candidates {
50+
if _, ok := h.assumptions[m]; ok {
51+
g.m = z.LitNull
52+
break
53+
}
54+
}
55+
56+
h.guesses = append(h.guesses, g)
57+
if g.m == z.LitNull {
58+
return
59+
}
60+
61+
installable := h.lits.InstallableOf(g.m)
62+
for _, constraint := range installable.Constraints() {
63+
var ms []z.Lit
64+
for _, dependency := range constraint.order() {
65+
ms = append(ms, h.lits.LitOf(dependency))
66+
}
67+
if len(ms) > 0 {
68+
h.guesses[len(h.guesses)-1].children++
69+
h.PushChoiceBack(choice{candidates: ms})
70+
}
71+
}
72+
73+
if h.assumptions == nil {
74+
h.assumptions = make(map[z.Lit]struct{})
75+
}
76+
h.assumptions[g.m] = struct{}{}
77+
h.s.Assume(g.m)
78+
h.result, h.buffer = h.s.Test(h.buffer)
79+
}
80+
81+
func (h *search) PopGuess() {
82+
g := h.guesses[len(h.guesses)-1]
83+
h.guesses = h.guesses[:len(h.guesses)-1]
84+
if g.m != z.LitNull {
85+
delete(h.assumptions, g.m)
86+
h.result = h.s.Untest()
87+
}
88+
for g.children > 0 {
89+
g.children--
90+
h.PopChoiceBack()
91+
}
92+
c := choice{
93+
index: g.index,
94+
candidates: g.candidates,
95+
}
96+
if g.m != z.LitNull {
97+
c.index++
98+
}
99+
h.PushChoiceFront(c)
100+
}
101+
102+
func (h *search) PushChoiceFront(c choice) {
103+
if h.headChoice == nil {
104+
h.headChoice = &c
105+
h.tailChoice = &c
106+
return
107+
}
108+
h.headChoice.prev = &c
109+
c.next = h.headChoice
110+
h.headChoice = &c
111+
}
112+
113+
func (h *search) PopChoiceFront() choice {
114+
c := h.headChoice
115+
if c.next != nil {
116+
c.next.prev = nil
117+
} else {
118+
h.tailChoice = nil
119+
}
120+
h.headChoice = c.next
121+
return *c
122+
123+
}
124+
func (h *search) PushChoiceBack(c choice) {
125+
if h.tailChoice == nil {
126+
h.headChoice = &c
127+
h.tailChoice = &c
128+
return
129+
}
130+
h.tailChoice.next = &c
131+
c.prev = h.tailChoice
132+
h.tailChoice = &c
133+
}
134+
135+
func (h *search) PopChoiceBack() choice {
136+
c := h.tailChoice
137+
if c.prev != nil {
138+
c.prev.next = nil
139+
} else {
140+
h.headChoice = nil
141+
}
142+
h.tailChoice = c.prev
143+
return *c
144+
}
145+
146+
func (h *search) Result() int {
147+
return h.result
148+
}
149+
150+
func (h *search) Lits() []z.Lit {
151+
result := make([]z.Lit, 0, len(h.guesses))
152+
for _, g := range h.guesses {
153+
if g.m != z.LitNull {
154+
result = append(result, g.m)
155+
}
156+
}
157+
return result
158+
}
159+
160+
func (h *search) Do(ctx context.Context, anchors []z.Lit) (int, []z.Lit, map[z.Lit]struct{}) {
161+
for _, m := range anchors {
162+
h.PushChoiceBack(choice{candidates: []z.Lit{m}})
163+
}
164+
165+
for {
166+
// Need to have a definitive result once all choices
167+
// have been made to decide whether to end or
168+
// backtrack.
169+
if h.headChoice == nil && h.result == unknown {
170+
h.result = h.s.Solve()
171+
}
172+
173+
// Backtrack if possible, otherwise end.
174+
if h.result == unsatisfiable {
175+
h.tracer.Trace(h)
176+
if len(h.guesses) == 0 {
177+
break
178+
}
179+
h.PopGuess()
180+
continue
181+
}
182+
183+
// Satisfiable and no decisions left!
184+
if h.headChoice == nil {
185+
break
186+
}
187+
188+
// Possibly SAT, keep guessing.
189+
h.PushGuess()
190+
}
191+
192+
lits := h.Lits()
193+
set := make(map[z.Lit]struct{}, len(lits))
194+
for _, m := range lits {
195+
set[m] = struct{}{}
196+
}
197+
result := h.Result()
198+
199+
// Go back to the initial test scope.
200+
for len(h.guesses) > 0 {
201+
h.PopGuess()
202+
}
203+
204+
return result, lits, set
205+
}
206+
207+
func (h *search) Installables() []Installable {
208+
result := make([]Installable, 0, len(h.guesses))
209+
for _, g := range h.guesses {
210+
if g.m != z.LitNull {
211+
result = append(result, h.lits.InstallableOf(g.candidates[g.index]))
212+
}
213+
}
214+
return result
215+
}
216+
217+
func (h *search) Conflicts() []AppliedConstraint {
218+
return h.lits.Conflicts(h.s)
219+
}
Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
//go:generate go run github.com/maxbrunsfeld/counterfeiter/v6 -o zz_search_test.go ../../../../../vendor/github.com/irifrance/gini/inter S
2+
3+
package solver
4+
5+
import (
6+
"context"
7+
"testing"
8+
9+
"github.com/irifrance/gini/inter"
10+
"github.com/irifrance/gini/z"
11+
"github.com/stretchr/testify/assert"
12+
)
13+
14+
type TestScopeCounter struct {
15+
depth *int
16+
inter.S
17+
}
18+
19+
func (c *TestScopeCounter) Test(dst []z.Lit) (result int, out []z.Lit) {
20+
result, out = c.S.Test(dst)
21+
*c.depth++
22+
return
23+
}
24+
25+
func (c *TestScopeCounter) Untest() (result int) {
26+
result = c.S.Untest()
27+
*c.depth--
28+
return
29+
}
30+
31+
func TestSearch(t *testing.T) {
32+
type tc struct {
33+
Name string
34+
Installables []Installable
35+
TestReturns []int
36+
UntestReturns []int
37+
Result int
38+
Assumptions []Identifier
39+
}
40+
41+
for _, tt := range []tc{
42+
{
43+
Name: "children popped from back of deque when guess popped",
44+
Installables: []Installable{
45+
installable("a", Mandatory(), Dependency("c")),
46+
installable("b", Mandatory()),
47+
installable("c"),
48+
},
49+
TestReturns: []int{0, -1},
50+
UntestReturns: []int{-1, -1},
51+
Result: -1,
52+
Assumptions: nil,
53+
},
54+
{
55+
Name: "candidates exhausted",
56+
Installables: []Installable{
57+
installable("a", Mandatory(), Dependency("x")),
58+
installable("b", Mandatory(), Dependency("y")),
59+
installable("x"),
60+
installable("y"),
61+
},
62+
TestReturns: []int{0, 0, -1, 1},
63+
UntestReturns: []int{0},
64+
Result: 1,
65+
Assumptions: []Identifier{"a", "b", "y"},
66+
},
67+
} {
68+
t.Run(tt.Name, func(t *testing.T) {
69+
assert := assert.New(t)
70+
71+
var s FakeS
72+
for i, result := range tt.TestReturns {
73+
s.TestReturnsOnCall(i, result, nil)
74+
}
75+
for i, result := range tt.UntestReturns {
76+
s.UntestReturnsOnCall(i, result)
77+
}
78+
79+
var depth int
80+
counter := &TestScopeCounter{depth: &depth, S: &s}
81+
82+
lits := newLitMapping(tt.Installables)
83+
h := search{
84+
s: counter,
85+
lits: lits,
86+
tracer: DefaultTracer{},
87+
}
88+
89+
var anchors []z.Lit
90+
for _, id := range h.lits.MandatoryIdentifiers() {
91+
anchors = append(anchors, h.lits.LitOf(id))
92+
}
93+
94+
result, ms, _ := h.Do(context.Background(), anchors)
95+
96+
assert.Equal(tt.Result, result)
97+
var ids []Identifier
98+
for _, m := range ms {
99+
ids = append(ids, lits.InstallableOf(m).Identifier())
100+
}
101+
assert.Equal(tt.Assumptions, ids)
102+
assert.Equal(0, depth)
103+
})
104+
}
105+
}

0 commit comments

Comments
 (0)