Tag 0.8.13

This reverts commit 2b23016a51.

cmd/build.go

@@ -15,9 +15,11 @@
 package cmd
 
 import (
+	"fmt"
 	"io/ioutil"
 	"os"
 
+	"github.com/ghodss/yaml"
 	helpers "github.com/mudler/luet/cmd/helpers"
 	"github.com/mudler/luet/pkg/compiler"
 	"github.com/mudler/luet/pkg/compiler/backend"
@@ -83,7 +85,13 @@ var buildCmd = &cobra.Command{
 		full, _ := cmd.Flags().GetBool("full")
 		skip, _ := cmd.Flags().GetBool("skip-if-metadata-exists")
 		concurrent, _ := cmd.Flags().GetBool("solver-concurrent")
+		var results Results
 
+		out, _ := cmd.Flags().GetString("output")
+		if out != "terminal" {
+			LuetCfg.GetLogging().SetLogLevel("error")
+		}
+		pretend, _ := cmd.Flags().GetBool("pretend")
 		compilerSpecs := compiler.NewLuetCompilationspecs()
 		var compilerBackend compiler.CompilerBackend
 		var db pkg.PackageDatabase
@@ -205,9 +213,58 @@ var buildCmd = &cobra.Command{
 		if revdeps {
 			artifact, errs = luetCompiler.CompileWithReverseDeps(privileged, compilerSpecs)
 
+		} else if pretend {
+			toCalculate := []compiler.CompilationSpec{}
+			if full {
+				var err error
+				toCalculate, err = luetCompiler.ComputeMinimumCompilableSet(compilerSpecs.All()...)
+				if err != nil {
+					errs = append(errs, err)
+				}
+			} else {
+				toCalculate = compilerSpecs.All()
+			}
+
+			for _, sp := range toCalculate {
+				packs, err := luetCompiler.ComputeDepTree(sp)
+				if err != nil {
+					errs = append(errs, err)
+				}
+				for _, p := range packs {
+					results.Packages = append(results.Packages,
+						PackageResult{
+							Name:       p.Package.GetName(),
+							Version:    p.Package.GetVersion(),
+							Category:   p.Package.GetCategory(),
+							Repository: "",
+							Hidden:     p.Package.IsHidden(),
+							Target:     sp.GetPackage().HumanReadableString(),
+						})
+				}
+			}
+
+			y, err := yaml.Marshal(results)
+			if err != nil {
+				fmt.Printf("err: %v\n", err)
+				return
+			}
+			switch out {
+			case "yaml":
+				fmt.Println(string(y))
+			case "json":
+				j2, err := yaml.YAMLToJSON(y)
+				if err != nil {
+					fmt.Printf("err: %v\n", err)
+					return
+				}
+				fmt.Println(string(j2))
+			case "terminal":
+				for _, p := range results.Packages {
+					Info(p.String())
+				}
+			}
 		} else {
 			artifact, errs = luetCompiler.CompileParallel(privileged, compilerSpecs)
-
 		}
 		if len(errs) != 0 {
 			for _, e := range errs {
@@ -252,5 +309,9 @@ func init() {
 	buildCmd.Flags().Int("solver-attempts", 9000, "Solver maximum attempts")
 	buildCmd.Flags().Bool("solver-concurrent", false, "Use concurrent solver (experimental)")
 
+	buildCmd.Flags().Bool("pretend", false, "Just print what packages will be compiled")
+
+	buildCmd.Flags().StringP("output", "o", "terminal", "Output format ( Defaults: terminal, available: json,yaml )")
+
 	RootCmd.AddCommand(buildCmd)
 }

cmd/root.go

@@ -38,7 +38,7 @@ var Verbose bool
 var LockedCommands = []string{"install", "uninstall", "upgrade"}
 
 const (
-	LuetCLIVersion = "0.8.11"
+	LuetCLIVersion = "0.8.13"
 	LuetEnvPrefix  = "LUET"
 )
 

cmd/search.go

@@ -32,6 +32,7 @@ type PackageResult struct {
 	Category   string `json:"category"`
 	Version    string `json:"version"`
 	Repository string `json:"repository"`
+	Target     string `json:"target"`
 	Hidden     bool   `json:"hidden"`
 }
 
@@ -39,6 +40,10 @@ type Results struct {
 	Packages []PackageResult `json:"packages"`
 }
 
+func (r PackageResult) String() string {
+	return fmt.Sprintf("%s/%s-%s required for %s", r.Category, r.Name, r.Version, r.Target)
+}
+
 var searchCmd = &cobra.Command{
 	Use:     "search <term>",
 	Short:   "Search packages",

contrib/config/get_luet_root.sh

@@ -0,0 +1,33 @@
+#!/bin/bash
+set -ex
+export LUET_NOLOCK=true
+
+LUET_VERSION=0.8.6
+LUET_ROOTFS=${LUET_ROOTFS:-/}
+LUET_DATABASE_PATH=${LUET_DATABASE_PATH:-/}
+LUET_DATABASE_ENGINE=${LUET_DATABASE_ENGINE:-boltdb}
+LUET_CONFIG_PROTECT=${LUET_CONFIG_PROTECT:-0}
+
+wget -q https://github.com/mudler/luet/releases/download/0.8.6/luet-0.8.6-linux-amd64 -O luet
+chmod +x luet
+
+mkdir -p /etc/luet/repos.conf.d || true
+if [ "${LUET_CONFIG_PROTECT}" = "1" ] ; then
+  mkdir -p /etc/luet/config.protect.d || true
+  wget -q  https://raw.githubusercontent.com/mudler/luet/master/contrib/config/config.protect.d/01_etc.yml.example -O /etc/luet/config.protect.d/01_etc.yml
+fi
+wget -q https://raw.githubusercontent.com/mocaccinoOS/repository-index/master/packages/mocaccino-repository-index/mocaccino-repository-index.yml -O /etc/luet/repos.conf.d/mocaccino-repository-index.yml
+
+cat > /etc/luet/luet.yaml <<EOF
+general:
+  debug: false
+system:
+  rootfs: ${LUET_ROOTFS}
+  database_path: "${LUET_DATABASE_PATH}"
+  database_engine: "${LUET_DATABASE_ENGINE}"
+EOF
+
+./luet install repository/luet repository/mocaccino-repository-index
+./luet install system/luet system/luet-extensions
+
+rm -rf luet

go.mod

@@ -25,6 +25,7 @@ require (
 	github.com/moby/sys/mount v0.1.1-0.20200320164225-6154f11e6840 // indirect
 	github.com/mudler/cobra-extensions v0.0.0-20200612154940-31a47105fe3d
 	github.com/mudler/docker-companion v0.4.6-0.20200418093252-41846f112d87
+	github.com/mudler/topsort v0.0.0-20201103161459-db5c7901c290
 	github.com/onsi/ginkgo v1.12.1
 	github.com/onsi/gomega v1.10.0
 	github.com/otiai10/copy v1.2.1-0.20200916181228-26f84a0b1578
@@ -33,7 +34,6 @@ require (
 	github.com/pkg/errors v0.9.1
 	github.com/spf13/cobra v1.0.0
 	github.com/spf13/viper v1.6.3
-	github.com/stevenle/topsort v0.0.0-20130922064739-8130c1d7596b
 	go.etcd.io/bbolt v1.3.4
 	go.uber.org/atomic v1.5.1 // indirect
 	go.uber.org/multierr v1.4.0 // indirect

go.sum

@@ -504,6 +504,8 @@ github.com/mudler/cobra-extensions v0.0.0-20200612154940-31a47105fe3d h1:fKh+rvw
 github.com/mudler/cobra-extensions v0.0.0-20200612154940-31a47105fe3d/go.mod h1:puRUWSwyecW2V355tKncwPVPRAjQBduPsFjG0mrV/Nw=
 github.com/mudler/docker-companion v0.4.6-0.20200418093252-41846f112d87 h1:mGz7T8KvmHH0gLWPI5tQne8xl2cO3T8wrrb6Aa16Jxo=
 github.com/mudler/docker-companion v0.4.6-0.20200418093252-41846f112d87/go.mod h1:1w4zI1LYXDeiUXqedPcrT5eQJnmKR6dbg5iJMgSIP/Y=
+github.com/mudler/topsort v0.0.0-20201103161459-db5c7901c290 h1:426hFyXMpXeqIeGJn2cGAW9ogvM2Jf+Jv23gtVPvBLM=
+github.com/mudler/topsort v0.0.0-20201103161459-db5c7901c290/go.mod h1:uP5BBgFxq2wNWo7n1vnY5SSbgL0WDshVJrOO12tZ/lA=
 github.com/munnerz/goautoneg v0.0.0-20120707110453-a547fc61f48d/go.mod h1:+n7T8mK8HuQTcFwEeznm/DIxMOiR9yIdICNftLE1DvQ=
 github.com/munnerz/goautoneg v0.0.0-20191010083416-a7dc8b61c822/go.mod h1:+n7T8mK8HuQTcFwEeznm/DIxMOiR9yIdICNftLE1DvQ=
 github.com/mwitkow/go-conntrack v0.0.0-20161129095857-cc309e4a2223/go.mod h1:qRWi+5nqEBWmkhHvq77mSJWrCKwh8bxhgT7d/eI7P4U=
@@ -699,8 +701,6 @@ github.com/spf13/viper v1.3.2/go.mod h1:ZiWeW+zYFKm7srdB9IoDzzZXaJaI5eL9QjNiN/DM
 github.com/spf13/viper v1.4.0/go.mod h1:PTJ7Z/lr49W6bUbkmS1V3by4uWynFiR9p7+dSq/yZzE=
 github.com/spf13/viper v1.6.3 h1:pDDu1OyEDTKzpJwdq4TiuLyMsUgRa/BT5cn5O62NoHs=
 github.com/spf13/viper v1.6.3/go.mod h1:jUMtyi0/lB5yZH/FjyGAoH7IMNrIhlBf6pXZmbMDvzw=
-github.com/stevenle/topsort v0.0.0-20130922064739-8130c1d7596b h1:wJSBFlabo96ySlmSX0a02WAPyGxagzTo9c5sk3sHP3E=
-github.com/stevenle/topsort v0.0.0-20130922064739-8130c1d7596b/go.mod h1:YIyOMT17IKD8FbLO8RfCJZd2qAZiOnIfuYePIeESwWc=
 github.com/streadway/amqp v0.0.0-20190404075320-75d898a42a94/go.mod h1:AZpEONHx3DKn8O/DFsRAY58/XVQiIPMTMB1SddzLXVw=
 github.com/streadway/amqp v0.0.0-20190827072141-edfb9018d271/go.mod h1:AZpEONHx3DKn8O/DFsRAY58/XVQiIPMTMB1SddzLXVw=
 github.com/streadway/handy v0.0.0-20190108123426-d5acb3125c2a/go.mod h1:qNTQ5P5JnDBl6z3cMAg/SywNDC5ABu5ApDIw6lUbRmI=

pkg/installer/installer.go

@@ -359,30 +359,39 @@ func (l *LuetInstaller) install(syncedRepos Repositories, cp pkg.Packages, s *Sy
 	var solution solver.PackagesAssertions
 
 	if !l.Options.NoDeps {
+		Info(":deciduous_tree: Computing installation, hang tight")
 		solv := solver.NewResolver(solver.Options{Type: l.Options.SolverOptions.Implementation, Concurrency: l.Options.Concurrency}, s.Database, allRepos, pkg.NewInMemoryDatabase(false), l.Options.SolverOptions.Resolver())
 		solution, err = solv.Install(p)
+		/// TODO: PackageAssertions needs to be a map[fingerprint]pack so lookup is in O(1)
 		if err != nil && !l.Options.Force {
 			return errors.Wrap(err, "Failed solving solution for package")
 		}
+		Info(":deciduous_tree: Finished calculating dependencies")
 		// Gathers things to install
+		Info(":deciduous_tree: Checking for packages already installed, and prepare for installation")
 		for _, assertion := range solution {
 			if assertion.Value {
+				if _, err := s.Database.FindPackage(assertion.Package); err == nil {
+					// skip matching if it is installed already
+					continue
+				}
 				packagesToInstall = append(packagesToInstall, assertion.Package)
 			}
 		}
 	} else if !l.Options.OnlyDeps {
 		for _, currentPack := range p {
+			if _, err := s.Database.FindPackage(currentPack); err == nil {
+				// skip matching if it is installed already
+				continue
+			}
 			packagesToInstall = append(packagesToInstall, currentPack)
 		}
 	}
-	Info(":deciduous_tree: Finding packages to install")
+	Info(":deciduous_tree: Finding packages to install from :cloud:")
 	// Gathers things to install
 	for _, currentPack := range packagesToInstall {
 		// Check if package is already installed.
-		if _, err := s.Database.FindPackage(currentPack); err == nil {
-			// skip matching if it is installed already
-			continue
-		}
+
 		matches := syncedRepos.PackageMatches(pkg.Packages{currentPack})
 		if len(matches) == 0 {
 			return errors.New("Failed matching solutions against repository for " + currentPack.HumanReadableString() + " where are definitions coming from?!")
@@ -618,9 +627,28 @@ func (l *LuetInstaller) uninstall(p pkg.Package, s *System) error {
 			continue
 		}
 
-		err := os.Remove(target)
+		fi, err := os.Lstat(target)
 		if err != nil {
-			Warning("Failed removing file (not present in the system target ?)", target)
+			Warning("File not present in the system target ?", target, err.Error())
+			if err = os.Remove(target); err != nil {
+				Warning("Failed removing file", target, err.Error())
+			}
+			continue
+		}
+		switch mode := fi.Mode(); {
+		case mode.IsDir():
+			files, err := ioutil.ReadDir(target)
+			if err != nil {
+				Warning("Failed reading folder", target, err.Error())
+			}
+			if len(files) != 0 {
+				Warning("Preserving not-empty folder", target, err.Error())
+				continue
+			}
+		}
+
+		if err = os.Remove(target); err != nil {
+			Warning("Failed removing file (not present in the system target ?)", target, err.Error())
 		}
 	}
 	err = s.Database.RemovePackageFiles(p)

pkg/package/database_boltdb.go

@@ -374,6 +374,11 @@ func (db *BoltDatabase) FindPackages(p Package) (Packages, error) {
 
 // FindPackageVersions return the list of the packages beloging to cat/name
 func (db *BoltDatabase) FindPackageVersions(p Package) (Packages, error) {
+	// Provides: Treat as the replaced package here
+	if provided, err := db.getProvide(p); err == nil {
+		p = provided
+	}
+
 	var versionsInWorld []Package
 	for _, w := range db.World() {
 		if w.GetName() != p.GetName() || w.GetCategory() != p.GetCategory() {

pkg/package/database_mem.go

@@ -225,6 +225,11 @@ func (db *InMemoryDatabase) FindPackage(p Package) (Package, error) {
 
 // FindPackages return the list of the packages beloging to cat/name
 func (db *InMemoryDatabase) FindPackageVersions(p Package) (Packages, error) {
+	// Provides: Treat as the replaced package here
+	if provided, err := db.getProvide(p); err == nil {
+		p = provided
+	}
+
 	versions, ok := db.CacheNoVersion[p.GetPackageName()]
 	if !ok {
 		return nil, errors.New("No versions found for package")

pkg/solver/benchmark_test.go

@@ -17,10 +17,12 @@ package solver_test
 
 import (
 	"fmt"
+	"io/ioutil"
 	"os"
 	"strconv"
 
 	pkg "github.com/mudler/luet/pkg/package"
+	"github.com/mudler/luet/tests/helpers"
 	. "github.com/onsi/ginkgo"
 	. "github.com/onsi/gomega"
 
@@ -144,13 +146,17 @@ var _ = Describe("Solver Benchmarks", func() {
 	Context("Complex data sets - Parallel Upgrades", func() {
 		BeforeEach(func() {
 			db = pkg.NewInMemoryDatabase(false)
-			dbInstalled = pkg.NewInMemoryDatabase(false)
+			//	dbInstalled = pkg.NewInMemoryDatabase(false)
 			dbDefinitions = pkg.NewInMemoryDatabase(false)
 			s = NewSolver(Options{Type: ParallelSimple, Concurrency: 100}, dbInstalled, dbDefinitions, db)
 			if os.Getenv("BENCHMARK_TESTS") != "true" {
 				Skip("BENCHMARK_TESTS not enabled")
 			}
+			tmpfile, _ := ioutil.TempFile(os.TempDir(), "tests")
+			defer os.Remove(tmpfile.Name()) // clean up
+			dbInstalled = pkg.NewBoltDatabase(tmpfile.Name())
 		})
+
 		Measure("it should be fast in resolution from a 10000*8 dataset", func(b Benchmarker) {
 			runtime := b.Time("runtime", func() {
 				for i := 2; i < 10000; i++ {
@@ -206,6 +212,48 @@ var _ = Describe("Solver Benchmarks", func() {
 			Ω(runtime.Seconds()).Should(BeNumerically("<", 70), "Install() shouldn't take too long.")
 		}, 1)
 
+		Measure("it should be fast in installation with 12000 packages installed and 2000*8 available", func(b Benchmarker) {
+			runtime := b.Time("runtime", func() {
+				for i := 0; i < 2000; i++ {
+					C := pkg.NewPackage("C", strconv.Itoa(i), []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
+					E := pkg.NewPackage("E", strconv.Itoa(i), []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
+					F := pkg.NewPackage("F", strconv.Itoa(i), []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
+					G := pkg.NewPackage("G", strconv.Itoa(i), []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
+					H := pkg.NewPackage("H", strconv.Itoa(i), []*pkg.DefaultPackage{G}, []*pkg.DefaultPackage{})
+					D := pkg.NewPackage("D", strconv.Itoa(i), []*pkg.DefaultPackage{H}, []*pkg.DefaultPackage{})
+					B := pkg.NewPackage("B", strconv.Itoa(i), []*pkg.DefaultPackage{D}, []*pkg.DefaultPackage{})
+					A := pkg.NewPackage("A", strconv.Itoa(i), []*pkg.DefaultPackage{B}, []*pkg.DefaultPackage{})
+					for _, p := range []pkg.Package{A, B, C, D, E, F, G} {
+						_, err := dbDefinitions.CreatePackage(p)
+						Expect(err).ToNot(HaveOccurred())
+					}
+					fmt.Println("Creating package, run", i)
+				}
+
+				for i := 0; i < 12000; i++ {
+					x := helpers.RandomPackage()
+					_, err := dbInstalled.CreatePackage(x)
+					Expect(err).ToNot(HaveOccurred())
+				}
+
+				G := pkg.NewPackage("G", strconv.Itoa(50000), []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
+				H := pkg.NewPackage("H", strconv.Itoa(50000), []*pkg.DefaultPackage{G}, []*pkg.DefaultPackage{})
+				D := pkg.NewPackage("D", strconv.Itoa(50000), []*pkg.DefaultPackage{H}, []*pkg.DefaultPackage{})
+				B := pkg.NewPackage("B", strconv.Itoa(50000), []*pkg.DefaultPackage{D}, []*pkg.DefaultPackage{})
+				A := pkg.NewPackage("A", strconv.Itoa(50000), []*pkg.DefaultPackage{B}, []*pkg.DefaultPackage{})
+
+				ass, err := s.Install([]pkg.Package{A})
+				Expect(err).ToNot(HaveOccurred())
+
+				Expect(ass).To(ContainElement(PackageAssert{Package: pkg.NewPackage("A", "50000", []*pkg.DefaultPackage{B}, []*pkg.DefaultPackage{}), Value: true}))
+				//Expect(ass).To(Equal(5))
+				//	Expect(len(solution)).To(Equal(6))
+
+			})
+
+			Ω(runtime.Seconds()).Should(BeNumerically("<", 70), "Install() shouldn't take too long.")
+		}, 1)
+
 		PMeasure("it should be fast in resolution from a 50000 dataset with upgrade universe", func(b Benchmarker) {
 			runtime := b.Time("runtime", func() {
 				for i := 0; i < 2; i++ {

pkg/solver/decoder.go

@@ -22,9 +22,9 @@ import (
 	"unicode"
 
 	pkg "github.com/mudler/luet/pkg/package"
+	"github.com/mudler/topsort"
 	toposort "github.com/philopon/go-toposort"
 	"github.com/pkg/errors"
-	"github.com/stevenle/topsort"
 )
 
 type PackagesAssertions []PackageAssert
@@ -181,7 +181,7 @@ func (assertions PackagesAssertions) Order(definitiondb pkg.PackageDatabase, fin
 			}
 			// Expand also here, as we need to order them (or instead the solver should give back the dep correctly?)
 			graph.AddEdge(currentPkg.GetFingerPrint(), requiredDef.GetFingerPrint())
-			added[requiredDef.GetFingerPrint()] = nil
+			added[requiredDef.GetFingerPrint()] = true
 		}
 	}
 	result, err := graph.TopSort(fingerprint)

pkg/solver/decoder_test.go

@@ -388,5 +388,37 @@ var _ = Describe("Decoder", func() {
 
 			Expect(solution4.Drop(Y).AssertionHash()).To(Equal(solution4.HashFrom(Y)))
 		})
+		for index := 0; index < 300; index++ { // Just to make sure we don't have false positives
+
+			It("Always same solution", func() {
+
+				X := pkg.NewPackage("X", "", []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
+				Y := pkg.NewPackage("Y", "", []*pkg.DefaultPackage{X}, []*pkg.DefaultPackage{})
+				Z := pkg.NewPackage("Z", "", []*pkg.DefaultPackage{X}, []*pkg.DefaultPackage{})
+				W := pkg.NewPackage("W", "", []*pkg.DefaultPackage{Z, Y}, []*pkg.DefaultPackage{})
+
+				for _, p := range []pkg.Package{X, Y, Z} {
+					_, err := dbDefinitions.CreatePackage(p)
+					Expect(err).ToNot(HaveOccurred())
+				}
+
+				for _, p := range []pkg.Package{} {
+					_, err := dbInstalled.CreatePackage(p)
+					Expect(err).ToNot(HaveOccurred())
+				}
+
+				solution, err := s.Install([]pkg.Package{W})
+				Expect(err).ToNot(HaveOccurred())
+
+				orderW, err := solution.Order(dbDefinitions, W.GetFingerPrint())
+				Expect(err).ToNot(HaveOccurred())
+				Expect(orderW[0].Package.GetName()).To(Equal("X"))
+				Expect(orderW[1].Package.GetName()).To(Equal("Y"))
+				Expect(orderW[2].Package.GetName()).To(Equal("Z"))
+				Expect(orderW[3].Package.GetName()).To(Equal("W"))
+			})
+
+		}
+
 	})
 })

pkg/solver/parallel.go

@@ -556,10 +556,11 @@ func (s *Parallel) Upgrade(checkconflicts, full bool) (pkg.Packages, PackagesAss
 
 	toUninstall := pkg.Packages{}
 	toInstall := pkg.Packages{}
-	availableCache := map[string]pkg.Packages{}
+
+	// we do this in memory so we take into account of provides
+	universe := pkg.NewInMemoryDatabase(false)
 	for _, p := range s.DefinitionDatabase.World() {
-		// Each one, should be expanded
-		availableCache[p.GetName()+p.GetCategory()] = append(availableCache[p.GetName()+p.GetCategory()], p)
+		universe.CreatePackage(p)
 	}
 
 	installedcopy := pkg.NewInMemoryDatabase(false)
@@ -575,10 +576,10 @@ func (s *Parallel) Upgrade(checkconflicts, full bool) (pkg.Packages, PackagesAss
 			defer wg.Done()
 			for p := range c {
 				installedcopy.CreatePackage(p)
-				packages, ok := availableCache[p.GetName()+p.GetCategory()]
-				if ok && len(packages) != 0 {
+				packages, err := universe.FindPackageVersions(p)
+				if err == nil && len(packages) != 0 {
 					best := packages.Best(nil)
-					if best.GetVersion() != p.GetVersion() {
+					if !best.Matches(p) {
 						results <- []pkg.Package{p, best}
 					}
 				}

pkg/solver/solver.go

@@ -489,20 +489,20 @@ func (s *Solver) Upgrade(checkconflicts, full bool) (pkg.Packages, PackagesAsser
 	toUninstall := pkg.Packages{}
 	toInstall := pkg.Packages{}
 
-	availableCache := map[string]pkg.Packages{}
+	// we do this in memory so we take into account of provides
+	universe := pkg.NewInMemoryDatabase(false)
 	for _, p := range s.DefinitionDatabase.World() {
-		// Each one, should be expanded
-		availableCache[p.GetName()+p.GetCategory()] = append(availableCache[p.GetName()+p.GetCategory()], p)
+		universe.CreatePackage(p)
 	}
 
 	installedcopy := pkg.NewInMemoryDatabase(false)
 
 	for _, p := range s.InstalledDatabase.World() {
 		installedcopy.CreatePackage(p)
-		packages, ok := availableCache[p.GetName()+p.GetCategory()]
-		if ok && len(packages) != 0 {
+		packages, err := universe.FindPackageVersions(p)
+		if err == nil && len(packages) != 0 {
 			best := packages.Best(nil)
-			if best.GetVersion() != p.GetVersion() {
+			if !best.Matches(p) {
 				toUninstall = append(toUninstall, p)
 				toInstall = append(toInstall, best)
 			}

pkg/solver/solver_test.go

@@ -1209,7 +1209,6 @@ var _ = Describe("Solver", func() {
 		})
 	})
 	Context("Upgrades", func() {
-
 		C := pkg.NewPackage("c", "1.5", []*pkg.DefaultPackage{&pkg.DefaultPackage{Name: "a", Version: ">=1.0", Category: "test"}}, []*pkg.DefaultPackage{})
 		C.SetCategory("test")
 		B := pkg.NewPackage("b", "1.0", []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
@@ -1219,6 +1218,17 @@ var _ = Describe("Solver", func() {
 		A1 := pkg.NewPackage("a", "1.2", []*pkg.DefaultPackage{&pkg.DefaultPackage{Name: "b", Version: "1.0", Category: "test"}}, []*pkg.DefaultPackage{})
 		A1.SetCategory("test")
 
+		BeforeEach(func() {
+			C = pkg.NewPackage("c", "1.5", []*pkg.DefaultPackage{&pkg.DefaultPackage{Name: "a", Version: ">=1.0", Category: "test"}}, []*pkg.DefaultPackage{})
+			C.SetCategory("test")
+			B = pkg.NewPackage("b", "1.0", []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
+			B.SetCategory("test")
+			A = pkg.NewPackage("a", "1.1", []*pkg.DefaultPackage{&pkg.DefaultPackage{Name: "b", Version: "1.0", Category: "test"}}, []*pkg.DefaultPackage{})
+			A.SetCategory("test")
+			A1 = pkg.NewPackage("a", "1.2", []*pkg.DefaultPackage{&pkg.DefaultPackage{Name: "b", Version: "1.0", Category: "test"}}, []*pkg.DefaultPackage{})
+			A1.SetCategory("test")
+		})
+
 		It("upgrades correctly", func() {
 			for _, p := range []pkg.Package{A1, B, C} {
 				_, err := dbDefinitions.CreatePackage(p)
@@ -1240,7 +1250,31 @@ var _ = Describe("Solver", func() {
 			Expect(solution).To(ContainElement(PackageAssert{Package: B, Value: true}))
 			Expect(solution).To(ContainElement(PackageAssert{Package: C, Value: false}))
 			Expect(len(solution)).To(Equal(3))
+		})
 
+		It("upgrades correctly with provides", func() {
+			B.SetProvides([]*pkg.DefaultPackage{&pkg.DefaultPackage{Name: "a", Version: ">=0", Category: "test"}, &pkg.DefaultPackage{Name: "c", Version: ">=0", Category: "test"}})
+
+			for _, p := range []pkg.Package{A1, B} {
+				_, err := dbDefinitions.CreatePackage(p)
+				Expect(err).ToNot(HaveOccurred())
+			}
+
+			for _, p := range []pkg.Package{A, C} {
+				_, err := dbInstalled.CreatePackage(p)
+				Expect(err).ToNot(HaveOccurred())
+			}
+			uninstall, solution, err := s.Upgrade(true, true)
+			Expect(err).ToNot(HaveOccurred())
+
+			Expect(len(uninstall)).To(Equal(2))
+			Expect(uninstall[1].GetName()).To(Equal("c"))
+			Expect(uninstall[1].GetVersion()).To(Equal("1.5"))
+			Expect(uninstall[0].GetName()).To(Equal("a"))
+			Expect(uninstall[0].GetVersion()).To(Equal("1.1"))
+
+			Expect(solution).To(ContainElement(PackageAssert{Package: B, Value: true}))
+			Expect(len(solution)).To(Equal(1))
 		})
 
 		It("UpgradeUniverse upgrades correctly", func() {

tests/helpers/package.go

@@ -0,0 +1,31 @@
+package helpers
+
+import (
+	"math/rand"
+	"strconv"
+	"time"
+
+	pkg "github.com/mudler/luet/pkg/package"
+)
+
+const charset = "abcdefghijklmnopqrstuvwxyz" +
+	"ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789"
+
+var seededRand *rand.Rand = rand.New(
+	rand.NewSource(time.Now().UnixNano()))
+
+func StringWithCharset(length int, charset string) string {
+	b := make([]byte, length)
+	for i := range b {
+		b[i] = charset[seededRand.Intn(len(charset))]
+	}
+	return string(b)
+}
+
+func String(length int) string {
+	return StringWithCharset(length, charset)
+}
+
+func RandomPackage() pkg.Package {
+	return pkg.NewPackage(String(5), strconv.Itoa(rand.Intn(100)), []*pkg.DefaultPackage{}, []*pkg.DefaultPackage{})
+}

vendor/github.com/crillab/gophersat/bf/bf.go

@@ -230,6 +230,8 @@ func (a and) String() string {
 }
 
 func (a and) Eval(model map[string]bool) (res bool) {
+	res = true
+
 	for i, s := range a {
 		b := s.Eval(model)
 		if i == 0 {

vendor/github.com/crillab/gophersat/solver/learn.go

@@ -29,7 +29,7 @@ func (s *Solver) addClauseLits(confl *Clause, lvl decLevel, met, metLvl []bool,
 		if abs(s.model[v]) == lvl {
 			metLvl[v] = true
 			nbLvl++
-		} else if abs(s.model[v]) != 1 {
+		} else {
 			*lits = append(*lits, l)
 		}
 	}
@@ -39,8 +39,9 @@ func (s *Solver) addClauseLits(confl *Clause, lvl decLevel, met, metLvl []bool,
 var bufLits = make([]Lit, 10000) // Buffer for lits in learnClause. Used to reduce allocations.
 
 // learnClause creates a conflict clause and returns either:
-// the clause itself, if its len is at least 2.
-// a nil clause and a unit literal, if its len is exactly 1.
+// - the clause itself, if its len is at least 2,
+// - a nil clause and a unit literal, if its len is exactly 1,
+// - a nil clause and -1, if the empty clause was learned.
 func (s *Solver) learnClause(confl *Clause, lvl decLevel) (learned *Clause, unit Lit) {
 	s.clauseBumpActivity(confl)
 	lits := bufLits[:1]             // Not 0: make room for asserting literal
@@ -58,6 +59,10 @@ func (s *Solver) learnClause(confl *Clause, lvl decLevel) (learned *Clause, unit
 			ptr--
 		}
 		v := s.trail[ptr].Var()
+		if s.assumptions[v] {
+			// Now we only have assumed lits: this is a top-level conflict
+			return nil, -1
+		}
 		ptr--
 		nbLvl--
 		if reason := s.reason[v]; reason != nil {
@@ -65,7 +70,7 @@ func (s *Solver) learnClause(confl *Clause, lvl decLevel) (learned *Clause, unit
 			for i := 0; i < reason.Len(); i++ {
 				lit := reason.Get(i)
 				if v2 := lit.Var(); !met[v2] {
-					if s.litStatus(lit) != Unsat {
+					if s.litStatus(lit) != Unsat { // In clauses where cardinality > 1, some lits might be true in the conflict clause: ignore them
 						continue
 					}
 					met[v2] = true
@@ -73,7 +78,7 @@ func (s *Solver) learnClause(confl *Clause, lvl decLevel) (learned *Clause, unit
 					if abs(s.model[v2]) == lvl {
 						metLvl[v2] = true
 						nbLvl++
-					} else if abs(s.model[v2]) != 1 {
+					} else {
 						lits = append(lits, lit)
 					}
 				}
@@ -109,7 +114,7 @@ func (s *Solver) minimizeLearned(met []bool, learned []Lit) int {
 		} else {
 			for k := 0; k < reason.Len(); k++ {
 				lit := reason.Get(k)
-				if !met[lit.Var()] && abs(s.model[lit.Var()]) > 1 {
+				if !met[lit.Var()] /*&& abs(s.model[lit.Var()]) > 1*/ {
 					learned[sz] = learned[i]
 					sz++
 					break

vendor/github.com/crillab/gophersat/solver/parser.go

@@ -12,11 +12,25 @@ import (
 // The argument is supposed to be a well-formed CNF.
 func ParseSlice(cnf [][]int) *Problem {
 	var pb Problem
+	pb.parseSlice(cnf)
+	return &pb
+}
+
+// ParseSliceNb parse a slice of slice of lits and returns the equivalent problem.
+// The argument is supposed to be a well-formed CNF.
+// The number of vars is provided because clauses might be added to it later.
+func ParseSliceNb(cnf [][]int, nbVars int) *Problem {
+	pb := Problem{NbVars: nbVars}
+	pb.parseSlice(cnf)
+	return &pb
+}
+
+func (pb *Problem) parseSlice(cnf [][]int) {
 	for _, line := range cnf {
 		switch len(line) {
 		case 0:
 			pb.Status = Unsat
-			return &pb
+			return
 		case 1:
 			if line[0] == 0 {
 				panic("null unit clause")
@@ -31,7 +45,7 @@ func ParseSlice(cnf [][]int) *Problem {
 			lits := make([]Lit, len(line))
 			for j, val := range line {
 				if val == 0 {
-					panic("null literal in clause %q")
+					panic(fmt.Sprintf("null literal in clause %v", lits))
 				}
 				lits[j] = IntToLit(int32(val))
 				if v := int(lits[j].Var()); v >= pb.NbVars {
@@ -52,11 +66,10 @@ func ParseSlice(cnf [][]int) *Problem {
 			}
 		} else if pb.Model[v] > 0 != unit.IsPositive() {
 			pb.Status = Unsat
-			return &pb
+			return
 		}
 	}
 	pb.simplify2()
-	return &pb
 }
 
 func isSpace(b byte) bool {

vendor/github.com/crillab/gophersat/solver/problem.go

@@ -97,26 +97,6 @@ func (pb *Problem) updateStatus(nbClauses int) {
 	}
 }
 
-func (pb *Problem) simplify() {
-	idxClauses := make([][]int, pb.NbVars*2) // For each lit, indexes of clauses it appears in
-	removed := make([]bool, len(pb.Clauses)) // Clauses that have to be removed
-	for i := range pb.Clauses {
-		pb.simplifyClause(i, idxClauses, removed)
-		if pb.Status == Unsat {
-			return
-		}
-	}
-	for i := 0; i < len(pb.Units); i++ {
-		lit := pb.Units[i]
-		neg := lit.Negation()
-		clauses := idxClauses[neg]
-		for j := range clauses {
-			pb.simplifyClause(j, idxClauses, removed)
-		}
-	}
-	pb.rmClauses(removed)
-}
-
 func (pb *Problem) simplifyClause(idx int, idxClauses [][]int, removed []bool) {
 	c := pb.Clauses[idx]
 	k := 0

vendor/github.com/crillab/gophersat/solver/solver.go

@@ -54,15 +54,18 @@ func (m Model) String() string {
 
 // A Solver solves a given problem. It is the main data structure.
 type Solver struct {
-	Verbose   bool // Indicates whether the solver should display information during solving or not. False by default
-	nbVars    int
-	status    Status
-	wl        watcherList
-	trail     []Lit     // Current assignment stack
-	model     Model     // 0 means unbound, other value is a binding
-	lastModel Model     // Placeholder for last model found, useful when looking for several models
-	activity  []float64 // How often each var is involved in conflicts
-	polarity  []bool    // Preferred sign for each var
+	Verbose     bool        // Indicates whether the solver should display information during solving or not. False by default
+	Certified   bool        // Indicates whether a certificate should be generated during solving or not, using the RUP notation. This is useful to prove UNSAT instances. False by default.
+	CertChan    chan string // Indicates where to write the certificate. If Certified is true but CertChan is nil, the certificate will be written on stdout.
+	nbVars      int
+	status      Status
+	wl          watcherList
+	trail       []Lit     // Current assignment stack
+	model       Model     // 0 means unbound, other value is a binding
+	lastModel   Model     // Placeholder for last model found, useful when looking for several models
+	activity    []float64 // How often each var is involved in conflicts
+	polarity    []bool    // Preferred sign for each var
+	assumptions []bool    // True iff the var's binding is assumed
 	// For each var, clause considered when it was unified
 	// If the var is not bound yet, or if it was bound by a decision, value is nil.
 	reason          []*Clause
@@ -73,7 +76,7 @@ type Solver struct {
 	Stats           Stats   // Statistics about the solving process.
 	minLits         []Lit   // Lits to minimize if the problem was an optimization problem.
 	minWeights      []int   // Weight of each lit to minimize if the problem was an optimization problem.
-	asumptions      []Lit   // Literals that are, ideally, true. Useful when trying to minimize a function.
+	hypothesis      []Lit   // Literals that are, ideally, true. Useful when trying to minimize a function.
 	localNbRestarts int     // How many restarts since Solve() was called?
 	varDecay        float64 // On each var decay, how much the varInc should be decayed
 	trailBuf        []int   // A buffer while cleaning bindings
@@ -94,19 +97,20 @@ func New(problem *Problem) *Solver {
 	}
 
 	s := &Solver{
-		nbVars:     nbVars,
-		status:     problem.Status,
-		trail:      make([]Lit, len(problem.Units), trailCap),
-		model:      problem.Model,
-		activity:   make([]float64, nbVars),
-		polarity:   make([]bool, nbVars),
-		reason:     make([]*Clause, nbVars),
-		varInc:     1.0,
-		clauseInc:  1.0,
-		minLits:    problem.minLits,
-		minWeights: problem.minWeights,
-		varDecay:   defaultVarDecay,
-		trailBuf:   make([]int, nbVars),
+		nbVars:      nbVars,
+		status:      problem.Status,
+		trail:       make([]Lit, len(problem.Units), trailCap),
+		model:       problem.Model,
+		activity:    make([]float64, nbVars),
+		polarity:    make([]bool, nbVars),
+		assumptions: make([]bool, nbVars),
+		reason:      make([]*Clause, nbVars),
+		varInc:      1.0,
+		clauseInc:   1.0,
+		minLits:     problem.minLits,
+		minWeights:  problem.minWeights,
+		varDecay:    defaultVarDecay,
+		trailBuf:    make([]int, nbVars),
 	}
 	s.resetOptimPolarity()
 	s.initOptimActivity()
@@ -322,26 +326,11 @@ func (s *Solver) rebuildOrderHeap() {
 	s.varQueue.build(ints)
 }
 
-// satClause returns true iff c is satisfied by a literal assigned at top level.
-func (s *Solver) satClause(c *Clause) bool {
-	if c.Len() == 2 || c.Cardinality() != 1 || c.PseudoBoolean() {
-		// TODO improve this, but it will be ok since we only call this function for removing useless clauses.
-		return false
-	}
-	for i := 0; i < c.Len(); i++ {
-		lit := c.Get(i)
-		assign := s.model[lit.Var()]
-		if assign == 1 && lit.IsPositive() || assign == -1 && !lit.IsPositive() {
-			return true
-		}
-	}
-	return false
-}
-
 // propagate binds the given lit, propagates it and searches for a solution,
 // until it is found or a restart is needed.
 func (s *Solver) propagateAndSearch(lit Lit, lvl decLevel) Status {
 	for lit != -1 {
+		// log.Printf("picked %d at lvl %d", lit.Int(), lvl)
 		if conflict := s.unifyLiteral(lit, lvl); conflict == nil { // Pick new branch or restart
 			if s.lbdStats.mustRestart() {
 				s.lbdStats.clear()
@@ -363,15 +352,17 @@ func (s *Solver) propagateAndSearch(lit Lit, lvl decLevel) Status {
 			s.lbdStats.addConflict(len(s.trail))
 			learnt, unit := s.learnClause(conflict, lvl)
 			if learnt == nil { // Unit clause was learned: this lit is known for sure
+				if unit == -1 || (abs(s.model[unit.Var()]) == 1 && s.litStatus(unit) == Unsat) { // Top-level conflict
+					return s.setUnsat()
+				}
 				s.Stats.NbUnitLearned++
 				s.lbdStats.addLbd(1)
 				s.cleanupBindings(1)
+				s.addLearnedUnit(unit)
 				s.model[unit.Var()] = lvlToSignedLvl(unit, 1)
 				if conflict = s.unifyLiteral(unit, 1); conflict != nil { // top-level conflict
-					s.status = Unsat
-					return Unsat
+					return s.setUnsat()
 				}
-				// s.rmSatClauses()
 				s.rebuildOrderHeap()
 				lit = s.chooseLit()
 				lvl = 2
@@ -392,6 +383,19 @@ func (s *Solver) propagateAndSearch(lit Lit, lvl decLevel) Status {
 	return Sat
 }
 
+// Sets the status to unsat and do cleanup tasks.
+func (s *Solver) setUnsat() Status {
+	if s.Certified {
+		if s.CertChan == nil {
+			fmt.Printf("0\n")
+		} else {
+			s.CertChan <- "0"
+		}
+	}
+	s.status = Unsat
+	return Unsat
+}
+
 // Searches until a restart is needed.
 func (s *Solver) search() Status {
 	s.localNbRestarts++
@@ -455,6 +459,28 @@ func (s *Solver) Solve() Status {
 	return s.status
 }
 
+// Assume adds unit literals to the solver.
+// This is useful when calling the solver several times, e.g to keep it "hot" while removing clauses.
+func (s *Solver) Assume(lits []Lit) Status {
+	s.cleanupBindings(0)
+	s.trail = s.trail[:0]
+	s.assumptions = make([]bool, s.nbVars)
+
+	for _, lit := range lits {
+
+		s.addLearnedUnit(lit)
+		s.assumptions[lit.Var()] = true
+		s.trail = append(s.trail, lit)
+	}
+	s.status = Indet
+	if confl := s.propagate(0, 1); confl != nil {
+		// Conflict after unit propagation
+		s.status = Unsat
+		return s.status
+	}
+	return s.status
+}
+
 // Enumerate returns the total number of models for the given problems.
 // if "models" is non-nil, it will write models on it as soon as it discovers them.
 // models will be closed at the end of the method.
@@ -474,10 +500,11 @@ func (s *Solver) Enumerate(models chan []bool, stop chan struct{}) int {
 			}
 		}
 		if s.status == Sat {
-			nb++
+			copy(s.lastModel, s.model)
 			if models != nil {
-				copy(s.lastModel, s.model)
-				models <- s.Model()
+				nb += s.addCurrentModels(models)
+			} else {
+				nb += s.countCurrentModels()
 			}
 			s.status = Indet
 			lits := s.decisionLits()
@@ -543,7 +570,8 @@ func (s *Solver) CountModels() int {
 			}
 		}
 		if s.status == Sat {
-			nb++
+			s.lastModel = s.model
+			nb += s.countCurrentModels()
 			if s.Verbose {
 				fmt.Printf("c found %d model(s)\n", nb)
 			}
@@ -695,6 +723,52 @@ func (s *Solver) Model() []bool {
 	return res
 }
 
+// addCurrentModels is called when a model was found.
+// It returns the total number of models from this point, and sends all models on ch.
+// The number can be different of 1 if there are unbound variables.
+// For instance, if there are 4 variables in the problem and only 1, 3 and 4 are bound,
+// there are actually 2 models currently: one with 2 set to true, the other with 2 set to false.
+func (s *Solver) addCurrentModels(ch chan []bool) int {
+	unbound := make([]int, 0, s.nbVars) // indices of unbound variables
+	var nb uint64 = 1                   // total number of models found
+	model := make([]bool, s.nbVars)     // partial model
+	for i, lvl := range s.lastModel {
+		if lvl == 0 {
+			unbound = append(unbound, i)
+			nb *= 2
+		} else {
+			model[i] = lvl > 0
+		}
+	}
+	for i := uint64(0); i < nb; i++ {
+		for j := range unbound {
+			mask := uint64(1 << j)
+			cur := i & mask
+			idx := unbound[j]
+			model[idx] = cur != 0
+		}
+		model2 := make([]bool, len(model))
+		copy(model2, model)
+		ch <- model2
+	}
+	return int(nb)
+}
+
+// countCurrentModels is called when a model was found.
+// It returns the total number of models from this point.
+// The number can be different of 1 if there are unbound variables.
+// For instance, if there are 4 variables in the problem and only 1, 3 and 4 are bound,
+// there are actually 2 models currently: one with 2 set to true, the other with 2 set to false.
+func (s *Solver) countCurrentModels() int {
+	var nb uint64 = 1 // total number of models found
+	for _, lvl := range s.lastModel {
+		if lvl == 0 {
+			nb *= 2
+		}
+	}
+	return int(nb)
+}
+
 // Optimal returns the optimal solution, if any.
 // If results is non-nil, all solutions will be written to it.
 // In any case, results will be closed at the end of the call.
@@ -731,13 +805,13 @@ func (s *Solver) Optimal(results chan Result, stop chan struct{}) (res Result) {
 			maxCost += w
 		}
 	}
-	s.asumptions = make([]Lit, len(s.minLits))
+	s.hypothesis = make([]Lit, len(s.minLits))
 	for i, lit := range s.minLits {
-		s.asumptions[i] = lit.Negation()
+		s.hypothesis[i] = lit.Negation()
 	}
 	weights := make([]int, len(s.minWeights))
 	copy(weights, s.minWeights)
-	sort.Sort(wLits{lits: s.asumptions, weights: weights})
+	sort.Sort(wLits{lits: s.hypothesis, weights: weights})
 	s.lastModel = make(Model, len(s.model))
 	var cost int
 	for status == Sat {
@@ -766,7 +840,7 @@ func (s *Solver) Optimal(results chan Result, stop chan struct{}) (res Result) {
 		// Add a constraint incrementing current best cost
 		lits2 := make([]Lit, len(s.minLits))
 		weights2 := make([]int, len(s.minWeights))
-		copy(lits2, s.asumptions)
+		copy(lits2, s.hypothesis)
 		copy(weights2, weights)
 		s.AppendClause(NewPBClause(lits2, weights2, maxCost-cost+1))
 		s.rebuildOrderHeap()
@@ -796,13 +870,13 @@ func (s *Solver) Minimize() int {
 			maxCost += w
 		}
 	}
-	s.asumptions = make([]Lit, len(s.minLits))
+	s.hypothesis = make([]Lit, len(s.minLits))
 	for i, lit := range s.minLits {
-		s.asumptions[i] = lit.Negation()
+		s.hypothesis[i] = lit.Negation()
 	}
 	weights := make([]int, len(s.minWeights))
 	copy(weights, s.minWeights)
-	sort.Sort(wLits{lits: s.asumptions, weights: weights})
+	sort.Sort(wLits{lits: s.hypothesis, weights: weights})
 	s.lastModel = make(Model, len(s.model))
 	var cost int
 	for status == Sat {
@@ -826,7 +900,7 @@ func (s *Solver) Minimize() int {
 		// Add a constraint incrementing current best cost
 		lits2 := make([]Lit, len(s.minLits))
 		weights2 := make([]int, len(s.minWeights))
-		copy(lits2, s.asumptions)
+		copy(lits2, s.hypothesis)
 		copy(weights2, weights)
 		s.AppendClause(NewPBClause(lits2, weights2, maxCost-cost+1))
 		s.rebuildOrderHeap()
@@ -835,7 +909,7 @@ func (s *Solver) Minimize() int {
 	return cost
 }
 
-// functions to sort asumptions for pseudo-boolean minimization clause.
+// functions to sort hypothesis for pseudo-boolean minimization clause.
 type wLits struct {
 	lits    []Lit
 	weights []int

vendor/github.com/crillab/gophersat/solver/types.go

@@ -42,6 +42,17 @@ type Var int32
 // Thus the CNF literal -3 is encoded as 2 * (3-1) + 1 = 5.
 type Lit int32
 
+// IntsToLits converts a list of CNF literals to a []Lit.
+// This is a helper function as the same result can be achieved by calling
+// IntToLit several times.
+func IntsToLits(vals ...int32) []Lit {
+	res := make([]Lit, len(vals))
+	for i, val := range vals {
+		res[i] = IntToLit(val)
+	}
+	return res
+}
+
 // IntToLit converts a CNF literal to a Lit.
 func IntToLit(i int32) Lit {
 	if i < 0 {

vendor/github.com/crillab/gophersat/solver/watcher.go

@@ -1,6 +1,9 @@
 package solver
 
-import "sort"
+import (
+	"fmt"
+	"sort"
+)
 
 type watcher struct {
 	other  Lit // Another lit from the clause
@@ -153,6 +156,26 @@ func (s *Solver) addLearned(c *Clause) {
 	s.wl.learned = append(s.wl.learned, c)
 	s.watchClause(c)
 	s.clauseBumpActivity(c)
+	if s.Certified {
+		if s.CertChan == nil {
+			fmt.Printf("%s\n", c.CNF())
+		} else {
+			s.CertChan <- c.CNF()
+		}
+	}
+}
+
+// Adds the given unit literal to the model at the top level.
+func (s *Solver) addLearnedUnit(unit Lit) {
+
+	s.model[unit.Var()] = lvlToSignedLvl(unit, 1)
+	if s.Certified {
+		if s.CertChan == nil {
+			fmt.Printf("%d 0\n", unit.Int())
+		} else {
+			s.CertChan <- fmt.Sprintf("%d 0", unit.Int())
+		}
+	}
 }
 
 // If l is negative, -lvl is returned. Else, lvl is returned.

vendor/github.com/mudler/topsort/topsort.go

@@ -16,6 +16,7 @@ package topsort
 
 import (
 	"fmt"
+	"sort"
 	"strings"
 )
 
@@ -98,6 +99,7 @@ func (n node) edges() []string {
 	for k := range n {
 		keys = append(keys, k)
 	}
+	sort.Strings(keys)
 	return keys
 }
 

vendor/modules.txt

@@ -59,7 +59,7 @@ github.com/containerd/continuity/syscallx
 github.com/containerd/continuity/sysx
 # github.com/cpuguy83/go-md2man/v2 v2.0.0
 github.com/cpuguy83/go-md2man/v2/md2man
-# github.com/crillab/gophersat v1.1.9-0.20200211102949-9a8bf7f2f0a3
+# github.com/crillab/gophersat v1.3.2-0.20201023142334-3fc2ac466765
 github.com/crillab/gophersat/bf
 github.com/crillab/gophersat/solver
 # github.com/cyphar/filepath-securejoin v0.2.2
@@ -211,6 +211,8 @@ github.com/morikuni/aec
 github.com/mudler/cobra-extensions
 # github.com/mudler/docker-companion v0.4.6-0.20200418093252-41846f112d87
 github.com/mudler/docker-companion/api
+# github.com/mudler/topsort v0.0.0-20201103161459-db5c7901c290
+github.com/mudler/topsort
 # github.com/nxadm/tail v1.4.4
 github.com/nxadm/tail
 github.com/nxadm/tail/ratelimiter
@@ -303,8 +305,6 @@ github.com/spf13/jwalterweatherman
 github.com/spf13/pflag
 # github.com/spf13/viper v1.6.3
 github.com/spf13/viper
-# github.com/stevenle/topsort v0.0.0-20130922064739-8130c1d7596b
-github.com/stevenle/topsort
 # github.com/subosito/gotenv v1.2.0
 github.com/subosito/gotenv
 # github.com/urfave/cli v1.22.1