Add an AtMost cardinality constraint to the solver package.

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

@@ -3,40 +3,16 @@ package solver
 import (
 	"fmt"
 	"strings"
-)
-
-// constrainer is a reusable accumulator of constraint clause terms.
-type constrainer struct {
-	pos []Identifier
-	neg []Identifier
-}
-
-func (x *constrainer) Add(id Identifier) {
-	x.pos = append(x.pos, id)
-}
-
-func (x *constrainer) AddNot(id Identifier) {
-	x.neg = append(x.neg, id)
-}
 
-// Reset clears the receiver's internal state so that it can be
-// reused.
-func (x *constrainer) Reset() {
-	x.pos = x.pos[:0]
-	x.neg = x.neg[:0]
-}
-
-// Empty returns true if and only if the receiver has accumulated no
-// positive or negative terms.
-func (x *constrainer) Empty() bool {
-	return len(x.pos) == 0 && len(x.neg) == 0
-}
+	"github.com/irifrance/gini/logic"
+	"github.com/irifrance/gini/z"
+)
 
 // Constraint implementations limit the circumstances under which a
 // particular Installable can appear in a solution.
 type Constraint interface {
 	String(subject Identifier) string
-	apply(x *constrainer, subject Identifier)
+	apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit
 	order() []Identifier
 }
 
@@ -49,7 +25,8 @@ func (zeroConstraint) String(subject Identifier) string {
 	return ""
 }
 
-func (zeroConstraint) apply(x *constrainer, subject Identifier) {
+func (zeroConstraint) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
+	return z.LitNull
 }
 
 func (zeroConstraint) order() []Identifier {
@@ -71,15 +48,15 @@ func (a AppliedConstraint) String() string {
 
 type mandatory struct{}
 
-func (c mandatory) String(subject Identifier) string {
+func (constraint mandatory) String(subject Identifier) string {
 	return fmt.Sprintf("%s is mandatory", subject)
 }
 
-func (c mandatory) apply(x *constrainer, subject Identifier) {
-	x.Add(subject)
+func (constraint mandatory) apply(_ *logic.C, lm *litMapping, subject Identifier) z.Lit {
+	return lm.LitOf(subject)
 }
 
-func (c mandatory) order() []Identifier {
+func (constraint mandatory) order() []Identifier {
 	return nil
 }
 
@@ -91,15 +68,15 @@ func Mandatory() Constraint {
 
 type prohibited struct{}
 
-func (c prohibited) String(subject Identifier) string {
+func (constraint prohibited) String(subject Identifier) string {
 	return fmt.Sprintf("%s is prohibited", subject)
 }
 
-func (c prohibited) apply(x *constrainer, subject Identifier) {
-	x.AddNot(subject)
+func (constraint prohibited) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
+	return lm.LitOf(subject).Not()
 }
 
-func (c prohibited) order() []Identifier {
+func (constraint prohibited) order() []Identifier {
 	return nil
 }
 
@@ -113,26 +90,24 @@ func Prohibited() Constraint {
 
 type dependency []Identifier
 
-func (c dependency) String(subject Identifier) string {
-	s := make([]string, len(c))
-	for i, each := range c {
+func (constraint dependency) String(subject Identifier) string {
+	s := make([]string, len(constraint))
+	for i, each := range constraint {
 		s[i] = string(each)
 	}
 	return fmt.Sprintf("%s requires at least one of %s", subject, strings.Join(s, ", "))
 }
 
-func (c dependency) apply(x *constrainer, subject Identifier) {
-	if len(c) == 0 {
-		return
-	}
-	x.AddNot(subject)
-	for _, each := range c {
-		x.Add(each)
+func (constraint dependency) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
+	m := lm.LitOf(subject).Not()
+	for _, each := range constraint {
+		m = c.Or(m, lm.LitOf(each))
 	}
+	return m
 }
 
-func (c dependency) order() []Identifier {
-	return []Identifier(c)
+func (constraint dependency) order() []Identifier {
+	return constraint
 }
 
 // Dependency returns a Constraint that will only permit solutions
@@ -146,16 +121,15 @@ func Dependency(ids ...Identifier) Constraint {
 
 type conflict Identifier
 
-func (c conflict) String(subject Identifier) string {
-	return fmt.Sprintf("%s conflicts with %s", subject, c)
+func (constraint conflict) String(subject Identifier) string {
+	return fmt.Sprintf("%s conflicts with %s", subject, constraint)
 }
 
-func (c conflict) apply(x *constrainer, subject Identifier) {
-	x.AddNot(subject)
-	x.AddNot(Identifier(c))
+func (constraint conflict) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
+	return c.Or(lm.LitOf(subject).Not(), lm.LitOf(Identifier(constraint)).Not())
 }
 
-func (c conflict) order() []Identifier {
+func (constraint conflict) order() []Identifier {
 	return nil
 }
 
@@ -165,3 +139,38 @@ func (c conflict) order() []Identifier {
 func Conflict(id Identifier) Constraint {
 	return conflict(id)
 }
+
+type leq struct {
+	ids []Identifier
+	n   int
+}
+
+func (constraint leq) String(subject Identifier) string {
+	s := make([]string, len(constraint.ids))
+	for i, each := range constraint.ids {
+		s[i] = string(each)
+	}
+	return fmt.Sprintf("%s permits at most %d of %s", subject, constraint.n, strings.Join(s, ", "))
+}
+
+func (constraint leq) apply(c *logic.C, lm *litMapping, subject Identifier) z.Lit {
+	ms := make([]z.Lit, len(constraint.ids))
+	for i, each := range constraint.ids {
+		ms[i] = lm.LitOf(each)
+	}
+	return c.CardSort(ms).Leq(constraint.n)
+}
+
+func (constraint leq) order() []Identifier {
+	return nil
+}
+
+// AtMost returns a Constraint that forbids solutions that contain
+// more than n of the Installables identified by the given
+// Identifiers.
+func AtMost(n int, ids ...Identifier) Constraint {
+	return leq{
+		ids: ids,
+		n:   n,
+	}
+}

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

@@ -1,87 +1,11 @@
 package solver
 
 import (
-	"sort"
 	"testing"
 
 	"github.com/stretchr/testify/assert"
 )
 
-func TestConstraints(t *testing.T) {
-	type tc struct {
-		Name       string
-		Constraint Constraint
-		Subject    Identifier
-		Expected   constrainer
-	}
-
-	for _, tt := range []tc{
-		{
-			Name:       "mandatory",
-			Constraint: Mandatory(),
-			Subject:    "a",
-			Expected: constrainer{
-				pos: []Identifier{"a"},
-			},
-		},
-		{
-			Name:       "prohibited",
-			Constraint: Prohibited(),
-			Subject:    "a",
-			Expected: constrainer{
-				neg: []Identifier{"a"},
-			},
-		},
-		{
-			Name:       "empty dependency",
-			Constraint: Dependency(),
-			Subject:    "a",
-			Expected:   constrainer{},
-		},
-		{
-			Name:       "single dependency",
-			Constraint: Dependency("b"),
-			Subject:    "a",
-			Expected: constrainer{
-				pos: []Identifier{"b"},
-				neg: []Identifier{"a"},
-			},
-		},
-		{
-			Name:       "multiple dependency",
-			Constraint: Dependency("x", "y", "z"),
-			Subject:    "a",
-			Expected: constrainer{
-				pos: []Identifier{"x", "y", "z"},
-				neg: []Identifier{"a"},
-			},
-		},
-		{
-			Name:       "conflict",
-			Constraint: Conflict("b"),
-			Subject:    "a",
-			Expected: constrainer{
-				neg: []Identifier{"a", "b"},
-			},
-		},
-	} {
-		t.Run(tt.Name, func(t *testing.T) {
-			var x constrainer
-			tt.Constraint.apply(&x, tt.Subject)
-
-			// Literals in lexically increasing order:
-			sort.Slice(x.pos, func(i, j int) bool {
-				return x.pos[i] < x.pos[j]
-			})
-			sort.Slice(x.neg, func(i, j int) bool {
-				return x.neg[i] < x.neg[j]
-			})
-
-			assert.Equal(t, tt.Expected, x)
-		})
-	}
-}
-
 func TestOrder(t *testing.T) {
 	type tc struct {
 		Name       string

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

@@ -48,27 +48,16 @@ func newLitMapping(installables []Installable) *litMapping {
 		d.installables[im] = installable
 	}
 
-	var x constrainer
 	for _, installable := range installables {
 		for _, constraint := range installable.Constraints() {
-			x.Reset()
-			constraint.apply(&x, installable.Identifier())
-			if x.Empty() {
+			m := constraint.apply(d.c, &d, installable.Identifier())
+			if m == z.LitNull {
 				// This constraint doesn't have a
 				// useful representation in the SAT
 				// inputs.
 				continue
 			}
 
-			d.buf = d.buf[:0]
-			for _, p := range x.pos {
-				d.buf = append(d.buf, d.LitOf(p))
-			}
-			for _, n := range x.neg {
-				d.buf = append(d.buf, d.LitOf(n).Not())
-			}
-			m := d.c.Ors(d.buf...)
-
 			d.constraints[m] = AppliedConstraint{
 				Installable: installable,
 				Constraint:  constraint,

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

@@ -227,6 +227,42 @@ func TestSolve(t *testing.T) {
 				installable("y"),
 			},
 		},
+		{
+			Name: "cardinality constraint prevents resolution",
+			Installables: []Installable{
+				installable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")),
+				installable("x", Mandatory()),
+				installable("y", Mandatory()),
+			},
+			Error: NotSatisfiable{
+				{
+					Installable: installable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")),
+					Constraint:  AtMost(1, "x", "y"),
+				},
+				{
+					Installable: installable("x", Mandatory()),
+					Constraint:  Mandatory(),
+				},
+				{
+					Installable: installable("y", Mandatory()),
+					Constraint:  Mandatory(),
+				},
+			},
+		},
+		{
+			Name: "cardinality constraint forces alternative",
+			Installables: []Installable{
+				installable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")),
+				installable("b", Mandatory(), Dependency("y")),
+				installable("x"),
+				installable("y"),
+			},
+			Installed: []Installable{
+				installable("a", Mandatory(), Dependency("x", "y"), AtMost(1, "x", "y")),
+				installable("b", Mandatory(), Dependency("y")),
+				installable("y"),
+			},
+		},
 		{
 			Name: "two dependencies satisfied by one installable",
 			Installables: []Installable{