Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We鈥檒l occasionally send you account related emails.

Already on GitHub? Sign in to your account

馃尡 Update the internal solver before exporting #164

Merged
merged 1 commit into from
Dec 4, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 2 additions & 11 deletions internal/solver/bench_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -68,20 +68,11 @@ var BenchmarkInput = func() []deppy.Variable {

func BenchmarkSolve(b *testing.B) {
for i := 0; i < b.N; i++ {
s, err := NewSolver(WithInput(BenchmarkInput))
s, err := New()
if err != nil {
b.Fatalf("failed to initialize solver: %s", err)
}
_, err = s.Solve()
if err != nil {
b.Fatalf("failed to initialize solver: %s", err)
}
}
}

func BenchmarkNewInput(b *testing.B) {
for i := 0; i < b.N; i++ {
_, err := NewSolver(WithInput(BenchmarkInput))
_, err = s.Solve(BenchmarkInput)
if err != nil {
b.Fatalf("failed to initialize solver: %s", err)
}
Expand Down
4 changes: 1 addition & 3 deletions internal/solver/search.go
Original file line number Diff line number Diff line change
@@ -1,8 +1,6 @@
package solver

import (
"context"

"github.com/go-air/gini/inter"
"github.com/go-air/gini/z"

Expand Down Expand Up @@ -157,7 +155,7 @@ func (h *search) Lits() []z.Lit {
return result
}

func (h *search) Do(_ context.Context, anchors []z.Lit) (int, []z.Lit, map[z.Lit]struct{}) {
func (h *search) Do(anchors []z.Lit) (int, []z.Lit, map[z.Lit]struct{}) {
for _, m := range anchors {
h.PushChoiceBack(choice{candidates: []z.Lit{m}})
}
Expand Down
3 changes: 1 addition & 2 deletions internal/solver/search_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
package solver

import (
"context"
"testing"

"github.com/go-air/gini/inter"
Expand Down Expand Up @@ -96,7 +95,7 @@ func TestSearch(t *testing.T) {
anchors = append(anchors, h.lits.LitOf(id))
}

result, ms, _ := h.Do(context.Background(), anchors)
result, ms, _ := h.Do(anchors)

assert.Equal(tt.Result, result)
var ids []deppy.Identifier
Expand Down
100 changes: 40 additions & 60 deletions internal/solver/solve.go
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
package solver

import (
"context"
"errors"
"fmt"

Expand All @@ -12,17 +11,8 @@ import (
"github.com/operator-framework/deppy/pkg/deppy"
)

var ErrIncomplete = errors.New("cancelled before a solution could be found")

type Solver interface {
Solve() ([]deppy.Variable, error)
}

type solver struct {
g inter.S
litMap *litMapping
type Solver struct {
tracer deppy.Tracer
buffer []z.Lit
}

const (
Expand All @@ -33,81 +23,87 @@ const (

// Solve takes a slice containing all Variables and returns a slice
// containing only those Variables that were selected for
// installation. If no solution is possible, or if the provided
// Context times out or is cancelled, an error is returned.
func (s *solver) Solve() ([]deppy.Variable, error) {
result, err := s.solve()
// installation. If no solution is possible an error is returned.
func (s *Solver) Solve(input []deppy.Variable) ([]deppy.Variable, error) {
giniSolver := gini.New()
litMap, err := newLitMapping(input)
if err != nil {
return nil, err
}

result, err := s.solve(giniSolver, litMap)

// This likely indicates a bug, so discard whatever
// return values were produced.
if derr := s.litMap.Error(); derr != nil {
if derr := litMap.Error(); derr != nil {
return nil, derr
}

return result, err
}

func (s *solver) solve() ([]deppy.Variable, error) {
func (s *Solver) solve(giniSolver inter.S, litMap *litMapping) ([]deppy.Variable, error) {
// teach all constraints to the solver
s.litMap.AddConstraints(s.g)
litMap.AddConstraints(giniSolver)

// collect literals of all mandatory variables to assume as a baseline
anchors := s.litMap.AnchorIdentifiers()
anchors := litMap.AnchorIdentifiers()
assumptions := make([]z.Lit, len(anchors))
for i := range anchors {
assumptions[i] = s.litMap.LitOf(anchors[i])
assumptions[i] = litMap.LitOf(anchors[i])
}

// assume that all constraints hold
s.litMap.AssumeConstraints(s.g)
s.g.Assume(assumptions...)
litMap.AssumeConstraints(giniSolver)
giniSolver.Assume(assumptions...)

var buffer []z.Lit
var aset map[z.Lit]struct{}
// push a new test scope with the baseline assumptions, to prevent them from being cleared during search
outcome, _ := s.g.Test(nil)
outcome, _ := giniSolver.Test(nil)
if outcome != satisfiable && outcome != unsatisfiable {
// searcher for solutions in input Order, so that preferences
// can be taken into acount (i.e. prefer one catalog to another)
outcome, assumptions, aset = (&search{s: s.g, lits: s.litMap, tracer: s.tracer}).Do(context.Background(), assumptions)
// can be taken into account (i.e. prefer one catalog to another)
outcome, assumptions, aset = (&search{s: giniSolver, lits: litMap, tracer: s.tracer}).Do(assumptions)
ncdc marked this conversation as resolved.
Show resolved Hide resolved
}
switch outcome {
case satisfiable:
s.buffer = s.litMap.Lits(s.buffer)
buffer = litMap.Lits(buffer)
var extras, excluded []z.Lit
for _, m := range s.buffer {
for _, m := range buffer {
if _, ok := aset[m]; ok {
continue
}
if !s.g.Value(m) {
if !giniSolver.Value(m) {
excluded = append(excluded, m.Not())
continue
}
extras = append(extras, m)
}
s.g.Untest()
cs := s.litMap.CardinalityConstrainer(s.g, extras)
s.g.Assume(assumptions...)
s.g.Assume(excluded...)
s.litMap.AssumeConstraints(s.g)
_, s.buffer = s.g.Test(s.buffer)
giniSolver.Untest()
cs := litMap.CardinalityConstrainer(giniSolver, extras)
giniSolver.Assume(assumptions...)
giniSolver.Assume(excluded...)
litMap.AssumeConstraints(giniSolver)
giniSolver.Test(nil)
for w := 0; w <= cs.N(); w++ {
s.g.Assume(cs.Leq(w))
if s.g.Solve() == satisfiable {
return s.litMap.Variables(s.g), nil
giniSolver.Assume(cs.Leq(w))
if giniSolver.Solve() == satisfiable {
return litMap.Variables(giniSolver), nil
}
}
// Something is wrong if we can't find a model anymore
// after optimizing for cardinality.
return nil, fmt.Errorf("unexpected internal error")
case unsatisfiable:
return nil, deppy.NotSatisfiable(s.litMap.Conflicts(s.g))
return nil, deppy.NotSatisfiable(litMap.Conflicts(giniSolver))
}

return nil, ErrIncomplete
return nil, errors.New("cancelled before a solution could be found")
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it possible to get here?

Copy link
Member Author

@m1kola m1kola Dec 4, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure. My guess is that Deppy used to accept context for some reason (maybe somehow related to entity sources). So this is probably a leftover from the times where some call coud be cancelled.

I did a bit of code archaeology with a goal to find out the origin of this on Friday, but without any results. I decided to leave this error for now, but removed exported ErrIncomplete. I think for the scope of this PR it is good enough. But I will dig deeper into this (will create an issue to track this). Edit: see #167

}

func NewSolver(options ...Option) (Solver, error) {
s := solver{g: gini.New()}
func New(options ...Option) (*Solver, error) {
s := Solver{}
for _, option := range append(options, defaults...) {
if err := option(&s); err != nil {
return nil, err
Expand All @@ -116,33 +112,17 @@ func NewSolver(options ...Option) (Solver, error) {
return &s, nil
}

type Option func(s *solver) error

func WithInput(input []deppy.Variable) Option {
return func(s *solver) error {
var err error
s.litMap, err = newLitMapping(input)
return err
}
}
type Option func(s *Solver) error

func WithTracer(t deppy.Tracer) Option {
return func(s *solver) error {
return func(s *Solver) error {
s.tracer = t
return nil
}
}

var defaults = []Option{
func(s *solver) error {
if s.litMap == nil {
var err error
s.litMap, err = newLitMapping(nil)
return err
}
return nil
},
func(s *solver) error {
func(s *Solver) error {
if s.tracer == nil {
s.tracer = DefaultTracer{}
}
Expand Down
12 changes: 8 additions & 4 deletions internal/solver/solve_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ import (
"testing"

"github.com/stretchr/testify/assert"
"github.com/stretchr/testify/require"

"github.com/operator-framework/deppy/pkg/deppy/constraint"

Expand Down Expand Up @@ -290,12 +291,12 @@ func TestSolve(t *testing.T) {
assert := assert.New(t)

var traces bytes.Buffer
s, err := NewSolver(WithInput(tt.Variables), WithTracer(LoggingTracer{Writer: &traces}))
s, err := New(WithTracer(LoggingTracer{Writer: &traces}))
if err != nil {
t.Fatalf("failed to initialize solver: %s", err)
}

installed, err := s.Solve()
installed, err := s.Solve(tt.Variables)

var ids []deppy.Identifier
for _, variable := range installed {
Expand All @@ -312,9 +313,12 @@ func TestSolve(t *testing.T) {
}

func TestDuplicateIdentifier(t *testing.T) {
_, err := NewSolver(WithInput([]deppy.Variable{
s, err := New()
require.NoError(t, err)

_, err = s.Solve([]deppy.Variable{
variable("a"),
variable("a"),
}))
})
assert.Equal(t, DuplicateIdentifier("a"), err)
}
4 changes: 2 additions & 2 deletions pkg/deppy/solver/solver.go
Original file line number Diff line number Diff line change
Expand Up @@ -46,12 +46,12 @@ func NewDeppySolver() *DeppySolver {
}

func (d DeppySolver) Solve(vars []deppy.Variable) (*Solution, error) {
satSolver, err := solver.NewSolver(solver.WithInput(vars))
satSolver, err := solver.New()
if err != nil {
return nil, err
}

selection, err := satSolver.Solve()
selection, err := satSolver.Solve(vars)
if err != nil && !errors.As(err, &deppy.NotSatisfiable{}) {
return nil, err
}
Expand Down