From 11c5175617a8700cc38385029577a5fd768f9a35 Mon Sep 17 00:00:00 2001
From: Mikalai Radchuk <mradchuk@redhat.com>
Date: Tue, 14 Nov 2023 17:17:26 +0000
Subject: [PATCH] Ensure solver output is deterministic

Signed-off-by: Mikalai Radchuk <mradchuk@redhat.com>
---
 internal/solver/lit_mapping.go | 16 ++++++----
 internal/solver/solve_test.go  | 58 ++++++----------------------------
 2 files changed, 19 insertions(+), 55 deletions(-)

diff --git a/internal/solver/lit_mapping.go b/internal/solver/lit_mapping.go
index 64ff27c..fe79200 100644
--- a/internal/solver/lit_mapping.go
+++ b/internal/solver/lit_mapping.go
@@ -27,12 +27,13 @@ func (inconsistentLitMapping) Error() string {
 // Solve (Constraints, Variables, etc.) and the variables that
 // appear in the SAT formula.
 type litMapping struct {
-	inorder     []deppy.Variable
-	variables   map[z.Lit]deppy.Variable
-	lits        map[deppy.Identifier]z.Lit
-	constraints map[z.Lit]deppy.AppliedConstraint
-	c           *logic.C
-	errs        inconsistentLitMapping
+	inorder            []deppy.Variable
+	variables          map[z.Lit]deppy.Variable
+	lits               map[deppy.Identifier]z.Lit
+	constraints        map[z.Lit]deppy.AppliedConstraint
+	constraintsInOrder []z.Lit
+	c                  *logic.C
+	errs               inconsistentLitMapping
 }
 
 // newLitMapping returns a new litMapping with its state initialized based on
@@ -72,6 +73,7 @@ func newLitMapping(variables []deppy.Variable) (*litMapping, error) {
 				Variable:   variable,
 				Constraint: constraint,
 			}
+			d.constraintsInOrder = append(d.constraintsInOrder, m)
 		}
 	}
 
@@ -142,7 +144,7 @@ func (d *litMapping) AddConstraints(g inter.S) {
 }
 
 func (d *litMapping) AssumeConstraints(s inter.S) {
-	for m := range d.constraints {
+	for _, m := range d.constraintsInOrder {
 		s.Assume(m)
 	}
 }
diff --git a/internal/solver/solve_test.go b/internal/solver/solve_test.go
index 7625a3e..4f49ff6 100644
--- a/internal/solver/solve_test.go
+++ b/internal/solver/solve_test.go
@@ -3,10 +3,7 @@ package solver
 import (
 	"bytes"
 	"context"
-	"errors"
 	"fmt"
-	"reflect"
-	"sort"
 	"testing"
 
 	"github.com/stretchr/testify/assert"
@@ -117,11 +114,11 @@ func TestSolve(t *testing.T) {
 			Error: deppy.NotSatisfiable{
 				{
 					Variable:   variable("a", constraint.Mandatory(), constraint.Prohibited()),
-					Constraint: constraint.Mandatory(),
+					Constraint: constraint.Prohibited(),
 				},
 				{
 					Variable:   variable("a", constraint.Mandatory(), constraint.Prohibited()),
-					Constraint: constraint.Prohibited(),
+					Constraint: constraint.Mandatory(),
 				},
 			},
 		},
@@ -186,16 +183,16 @@ func TestSolve(t *testing.T) {
 			},
 			Error: deppy.NotSatisfiable{
 				{
-					Variable:   variable("a", constraint.Mandatory()),
-					Constraint: constraint.Mandatory(),
+					Variable:   variable("b", constraint.Mandatory(), constraint.Conflict("a")),
+					Constraint: constraint.Conflict("a"),
 				},
 				{
 					Variable:   variable("b", constraint.Mandatory(), constraint.Conflict("a")),
 					Constraint: constraint.Mandatory(),
 				},
 				{
-					Variable:   variable("b", constraint.Mandatory(), constraint.Conflict("a")),
-					Constraint: constraint.Conflict("a"),
+					Variable:   variable("a", constraint.Mandatory()),
+					Constraint: constraint.Mandatory(),
 				},
 			},
 		},
@@ -218,16 +215,16 @@ func TestSolve(t *testing.T) {
 			},
 			Error: deppy.NotSatisfiable{
 				{
-					Variable:   variable("a", constraint.Mandatory(), constraint.Dependency("x", "y"), constraint.AtMost(1, "x", "y")),
-					Constraint: constraint.AtMost(1, "x", "y"),
+					Variable:   variable("y", constraint.Mandatory()),
+					Constraint: constraint.Mandatory(),
 				},
 				{
 					Variable:   variable("x", constraint.Mandatory()),
 					Constraint: constraint.Mandatory(),
 				},
 				{
-					Variable:   variable("y", constraint.Mandatory()),
-					Constraint: constraint.Mandatory(),
+					Variable:   variable("a", constraint.Mandatory(), constraint.Dependency("x", "y"), constraint.AtMost(1, "x", "y")),
+					Constraint: constraint.AtMost(1, "x", "y"),
 				},
 			},
 		},
@@ -301,41 +298,6 @@ func TestSolve(t *testing.T) {
 
 			installed, err := s.Solve(context.TODO())
 
-			if installed != nil {
-				sort.SliceStable(installed, func(i, j int) bool {
-					return installed[i].Identifier() < installed[j].Identifier()
-				})
-			}
-
-			// Failed constraints are sorted in lexically
-			// increasing Order of the identifier of the
-			// constraint's variable, with ties broken
-			// in favor of the constraint that appears
-			// earliest in the variable's list of
-			// constraints.
-			var ns deppy.NotSatisfiable
-			if errors.As(err, &ns) {
-				sort.SliceStable(ns, func(i, j int) bool {
-					if ns[i].Variable.Identifier() != ns[j].Variable.Identifier() {
-						return ns[i].Variable.Identifier() < ns[j].Variable.Identifier()
-					}
-					var x, y int
-					for ii, c := range ns[i].Variable.Constraints() {
-						if reflect.DeepEqual(c, ns[i].Constraint) {
-							x = ii
-							break
-						}
-					}
-					for ij, c := range ns[j].Variable.Constraints() {
-						if reflect.DeepEqual(c, ns[j].Constraint) {
-							y = ij
-							break
-						}
-					}
-					return x < y
-				})
-			}
-
 			var ids []deppy.Identifier
 			for _, variable := range installed {
 				ids = append(ids, variable.Identifier())