atlas: SAT based package solver, WIP (#22027)

* atlas: SAT based package solver, WIP * progress * make tests green * progress * SAT: now works; enabled unit tests in versions.nim * Atlas: SAT: completed
2026-01-19 02:57:10 +00:00 · 2023-06-09 16:15:43 +02:00
parent 744a99d75c
commit 65c412e3f0
6 changed files with 856 additions and 100 deletions
--- a/atlas/atlas.nim
+++ b/atlas/atlas.nim
@@ -11,7 +11,7 @@

 import std / [parseopt, strutils, os, osproc, tables, sets, json, jsonutils,
  parsecfg, streams, terminal, strscans, hashes]
-import parse_requires, osutils, packagesjson, compiledpatterns
+import parse_requires, osutils, packagesjson, compiledpatterns, versions, sat

 from unicode import nil

@@ -65,6 +65,8 @@ Options:
                        corresponding Nim virtual environment
  --autoinit            auto initialize a workspace
  --colors=on|off       turn on|off colored output
+  --resolver=minver|semver|maxver
+                        which resolution algorithm to use, default is minver
  --showGraph           show the dependency graph
  --version             show the version
  --help                show this help
@@ -99,18 +101,23 @@ type
  SemVerField = enum
    major, minor, patch

+  ResolutionAlgorithm = enum
+    MinVer, SemVer, MaxVer
+
  Dependency = object
    name: PackageName
    url, commit: string
-    rel: DepRelation # "requires x < 1.0" is silly, but Nimble allows it so we have too.
+    query: VersionInterval
    self: int # position in the graph
    parents: seq[int] # why we need this dependency
    active: bool
+    algo: ResolutionAlgorithm
  DepGraph = object
    nodes: seq[Dependency]
    processed: Table[string, int] # the key is (url / commit)
    byName: Table[PackageName, seq[int]]
-    bestNimVersion: (int, int, int) # Nim is a special snowflake
+    availableVersions: Table[PackageName, seq[(string, Version)]] # sorted, latest version comes first
+    bestNimVersion: Version # Nim is a special snowflake

  LockFile = object # serialized as JSON so an object for extensibility
    items: OrderedTable[string, LockFileEntry]
@@ -133,6 +140,7 @@ type
    overrides: Patterns
    lockMode: LockMode
    lockFile: LockFile
+    defaultAlgo: ResolutionAlgorithm
    when MockupRun:
      step: int
      mockupSuccess: bool
@@ -143,7 +151,7 @@ proc `==`*(a, b: PackageName): bool {.borrow.}
 proc hash*(a: PackageName): Hash {.borrow.}

 const
-  InvalidCommit = "<invalid commit>"
+  InvalidCommit = "#head" #"<invalid commit>"
  ProduceTest = false

 type
@@ -178,7 +186,7 @@ proc nimbleExec(cmd: string; args: openArray[string]) =

 proc exec(c: var AtlasContext; cmd: Command; args: openArray[string]): (string, int) =
  when MockupRun:
-    assert TestLog[c.step].cmd == cmd, $(TestLog[c.step].cmd, cmd)
+    assert TestLog[c.step].cmd == cmd, $(TestLog[c.step].cmd, cmd, c.step)
    case cmd
    of GitDiff, GitTag, GitTags, GitLastTaggedRef, GitDescribe, GitRevParse, GitPush, GitPull, GitCurrentCommit:
      result = (TestLog[c.step].output, TestLog[c.step].exitCode)
@@ -224,12 +232,6 @@ proc extractRequiresInfo(c: var AtlasContext; nimbleFile: string): NimbleFileInf
  when ProduceTest:
    echo "nimble ", nimbleFile, " info ", result

-proc toDepRelation(s: string): DepRelation =
-  case s
-  of "<": strictlyLess
-  of ">": strictlyGreater
-  else: normal
-
 proc isCleanGit(c: var AtlasContext): string =
  result = ""
  let (outp, status) = exec(c, GitDiff, [])
@@ -292,29 +294,22 @@ proc getLastTaggedCommit(c: var AtlasContext): string =
    if lastTag.len != 0:
      result = lastTag

-proc versionToCommit(c: var AtlasContext; d: Dependency): string =
+proc collectTaggedVersions(c: var AtlasContext): seq[(string, Version)] =
  let (outp, status) = exec(c, GitTags, [])
  if status == 0:
-    var useNextOne = false
-    for line in splitLines(outp):
-      let commitsAndTags = strutils.splitWhitespace(line)
-      if commitsAndTags.len == 2:
-        case d.rel
-        of normal:
-          if commitsAndTags[1].sameVersionAs(d.commit):
-            return commitsAndTags[0]
-        of strictlyLess:
-          if d.commit == InvalidCommit:
-            return getLastTaggedCommit(c)
-          elif not commitsAndTags[1].sameVersionAs(d.commit):
-            return commitsAndTags[0]
-        of strictlyGreater:
-          if commitsAndTags[1].sameVersionAs(d.commit):
-            useNextOne = true
-          elif useNextOne:
-            return commitsAndTags[0]
+    result = parseTaggedVersions(outp)
+  else:
+    result = @[]

-  return ""
+proc versionToCommit(c: var AtlasContext; d: Dependency): string =
+  let allVersions = collectTaggedVersions(c)
+  case d.algo
+  of MinVer:
+    result = selectBestCommitMinVer(allVersions, d.query)
+  of SemVer:
+    result = selectBestCommitSemVer(allVersions, d.query)
+  of MaxVer:
+    result = selectBestCommitMaxVer(allVersions, d.query)

 proc shortToCommit(c: var AtlasContext; short: string): string =
  let (cc, status) = exec(c, GitRevParse, [short])
@@ -462,9 +457,8 @@ proc setupNimEnv(c: var AtlasContext; nimVersion: string)
 proc afterGraphActions(c: var AtlasContext; g: DepGraph) =
  if ShowGraph in c.flags:
    generateDepGraph c, g
-  if AutoEnv in c.flags and g.bestNimVersion != (0, 0, 0):
-    let v = $g.bestNimVersion[0] & "." & $g.bestNimVersion[1] & "." & $g.bestNimVersion[2]
-    setupNimEnv c, v
+  if AutoEnv in c.flags and g.bestNimVersion != Version"":
+    setupNimEnv c, g.bestNimVersion.string

 proc needsCommitLookup(commit: string): bool {.inline.} =
  '.' in commit or commit == InvalidCommit
@@ -575,35 +569,36 @@ proc addUnique[T](s: var seq[T]; elem: sink T) =
  if not s.contains(elem): s.add elem

 proc addUniqueDep(c: var AtlasContext; g: var DepGraph; parent: int;
-                  tokens: seq[string]) =
-  let pkgName = tokens[0]
+                  pkg: string; query: VersionInterval) =
+  let commit = versionKey(query)
  let oldErrors = c.errors
-  let url = toUrl(c, pkgName)
+  let url = toUrl(c, pkg)
  if oldErrors != c.errors:
-    warn c, toName(pkgName), "cannot resolve package name"
+    warn c, toName(pkg), "cannot resolve package name"
  else:
-    let key = url / tokens[2]
+    let key = url / commit
    if g.processed.hasKey(key):
      g.nodes[g.processed[key]].parents.addUnique parent
    else:
      let self = g.nodes.len
-      g.byName.mgetOrPut(toName(pkgName), @[]).add self
+      g.byName.mgetOrPut(toName(pkg), @[]).add self
      g.processed[key] = self
      if c.lockMode == useLock:
-        if c.lockfile.items.contains(pkgName):
-          g.nodes.add Dependency(name: toName(pkgName),
-                              url: c.lockfile.items[pkgName].url,
-                              commit: c.lockfile.items[pkgName].commit,
-                              rel: normal,
-                              self: self,
-                              parents: @[parent])
+        if c.lockfile.items.contains(pkg):
+          g.nodes.add Dependency(name: toName(pkg),
+                                 url: c.lockfile.items[pkg].url,
+                                 commit: c.lockfile.items[pkg].commit,
+                                 self: self,
+                                 parents: @[parent],
+                                 algo: c.defaultAlgo)
        else:
-          error c, toName(pkgName), "package is not listed in the lock file"
+          error c, toName(pkg), "package is not listed in the lock file"
      else:
-        g.nodes.add Dependency(name: toName(pkgName), url: url, commit: tokens[2],
-                               rel: toDepRelation(tokens[1]),
+        g.nodes.add Dependency(name: toName(pkg), url: url, commit: commit,
                               self: self,
-                               parents: @[parent])
+                               query: query,
+                               parents: @[parent],
+                               algo: c.defaultAlgo)

 template toDestDir(p: PackageName): string = p.string

@@ -612,11 +607,9 @@ proc readLockFile(filename: string): LockFile =
  let jsonTree = parseJson(jsonAsStr)
  result = to(jsonTree, LockFile)

-proc rememberNimVersion(g: var DepGraph; tokens: seq[string]) =
-  if tokens[1] in ["==", ">="]:
-    var v = (0, 0, 0)
-    if scanf(tokens[2], "$i.$i.$i", v[0], v[1], v[2]):
-      if v > g.bestNimVersion: g.bestNimVersion = v
+proc rememberNimVersion(g: var DepGraph; q: VersionInterval) =
+  let v = extractGeQuery(q)
+  if v != Version"" and v > g.bestNimVersion: g.bestNimVersion = v

 proc collectDeps(c: var AtlasContext; g: var DepGraph; parent: int;
                 dep: Dependency; nimbleFile: string): CfgPath =
@@ -625,26 +618,18 @@ proc collectDeps(c: var AtlasContext; g: var DepGraph; parent: int;
  assert nimbleFile != ""
  let nimbleInfo = extractRequiresInfo(c, nimbleFile)
  for r in nimbleInfo.requires:
-    var tokens: seq[string] = @[]
-    for token in tokenizeRequires(r):
-      tokens.add token
-    if tokens.len == 1:
-      # nimx uses dependencies like 'requires "sdl2"'.
-      # Via this hack we map them to the first tagged release.
-      # (See the `isStrictlySmallerThan` logic.)
-      tokens.add "<"
-      tokens.add InvalidCommit
-    elif tokens.len == 2 and tokens[1].startsWith("#"):
-      # Dependencies can also look like 'requires "sdl2#head"
-      var commit = tokens[1][1 .. ^1]
-      tokens[1] = "=="
-      tokens.add commit
-
-    if tokens.len >= 3:
-      if cmpIgnoreCase(tokens[0], "nim") != 0:
-        c.addUniqueDep g, parent, tokens
+    var i = 0
+    while i < r.len and r[i] notin {'#', '<', '=', '>'} + Whitespace: inc i
+    let pkgName = r.substr(0, i-1)
+    var err = pkgName.len == 0
+    let query = parseVersionInterval(r, i, err)
+    if err:
+      error c, toName(nimbleFile), "invalid 'requires' syntax: " & r
+    else:
+      if cmpIgnoreCase(pkgName, "nim") != 0:
+        c.addUniqueDep g, parent, pkgName, query
      else:
-        rememberNimVersion g, tokens
+        rememberNimVersion g, query
  result = CfgPath(toDestDir(dep.name) / nimbleInfo.srcDir)

 proc collectNewDeps(c: var AtlasContext; g: var DepGraph; parent: int;
@@ -665,22 +650,101 @@ proc copyFromDisk(c: var AtlasContext; w: Dependency) =
  writeFile destDir / ThisVersion, w.commit
  #echo "WRITTEN ", destDir / ThisVersion

-proc isNewerVersion(a, b: string): bool =
-  # only used for testing purposes.
-  if a == InvalidCommit or b == InvalidCommit:
-    return true
-  var amajor, aminor, apatch, bmajor, bminor, bpatch: int
-  if scanf(a, "$i.$i.$i", amajor, aminor, apatch):
-    assert scanf(b, "$i.$i.$i", bmajor, bminor, bpatch)
-    result = (amajor, aminor, apatch) > (bmajor, bminor, bpatch)
-  else:
-    assert scanf(a, "$i.$i", amajor, aminor)
-    assert scanf(b, "$i.$i", bmajor, bminor)
-    result = (amajor, aminor) > (bmajor, bminor)
-
 proc isLaterCommit(destDir, version: string): bool =
  let oldVersion = try: readFile(destDir / ThisVersion).strip except: "0.0"
-  result = isNewerVersion(version, oldVersion)
+  if isValidVersion(oldVersion) and isValidVersion(version):
+    result = Version(oldVersion) < Version(version)
+  else:
+    result = true
+
+proc collectAvailableVersions(c: var AtlasContext; g: var DepGraph; w: Dependency) =
+  when MockupRun:
+    # don't cache when doing the MockupRun:
+    g.availableVersions[w.name] = collectTaggedVersions(c)
+  else:
+    if not g.availableVersions.hasKey(w.name):
+      g.availableVersions[w.name] = collectTaggedVersions(c)
+
+proc resolve(c: var AtlasContext; g: var DepGraph) =
+  var b = sat.Builder()
+  b.openOpr(AndForm)
+  # Root must true:
+  b.add newVar(VarId 0)
+
+  assert g.nodes.len > 0
+  assert g.nodes[0].active
+  # Implications:
+  for i in 0..<g.nodes.len:
+    if g.nodes[i].active:
+      for j in g.nodes[i].parents:
+        # "parent has a dependency on x" is translated to:
+        # "parent implies x" which is "not parent or x"
+        if j >= 0:
+          b.openOpr(OrForm)
+          b.openOpr(NotForm)
+          b.add newVar(VarId j)
+          b.closeOpr
+          b.add newVar(VarId i)
+          b.closeOpr
+  var idgen = 0
+  var mapping: seq[(string, string, Version)] = @[]
+  # Version selection:
+  for i in 0..<g.nodes.len:
+    if g.nodes[i].active:
+      # A -> (exactly one of: A1, A2, A3)
+      b.openOpr(OrForm)
+      b.openOpr(NotForm)
+      b.add newVar(VarId i)
+      b.closeOpr
+      b.openOpr(ExactlyOneOfForm)
+
+      let av {.cursor.} = g.availableVersions[g.nodes[i].name]
+      var q = g.nodes[i].query
+      if g.nodes[i].algo == SemVer: q = toSemVer(q)
+      if g.nodes[i].algo == MinVer:
+        for j in countup(0, av.len-1):
+          if q.matches(av[j][1]):
+            mapping.add (g.nodes[i].name.string, av[j][0], av[j][1])
+            b.add newVar(VarId(idgen + g.nodes.len))
+            inc idgen
+      else:
+        for j in countdown(av.len-1, 0):
+          if q.matches(av[j][1]):
+            mapping.add (g.nodes[i].name.string, av[j][0], av[j][1])
+            b.add newVar(VarId(idgen + g.nodes.len))
+            inc idgen
+
+      b.closeOpr # ExactlyOneOfForm
+      b.closeOpr # OrForm
+  b.closeOpr()
+  let f = toForm(b)
+  var s = newSeq[BindingKind](idgen)
+  if satisfiable(f, s):
+    for i in g.nodes.len..<s.len:
+      if s[i] == setToTrue:
+        let destDir = mapping[i - g.nodes.len][0]
+        let dir = selectDir(c.workspace / destDir, c.depsDir / destDir)
+        withDir c, dir:
+          checkoutGitCommit(c, toName(destDir), mapping[i - g.nodes.len][1])
+    when false:
+      echo "selecting: "
+      for i in g.nodes.len..<s.len:
+        if s[i] == setToTrue:
+          echo "[x] ", mapping[i - g.nodes.len]
+        else:
+          echo "[ ] ", mapping[i - g.nodes.len]
+      echo f
+  else:
+    error c, toName(c.workspace), "version conflict; for more information use --showGraph"
+    var usedVersions = initCountTable[string]()
+    for i in g.nodes.len..<s.len:
+      if s[i] == setToTrue:
+        usedVersions.inc mapping[i - g.nodes.len][0]
+    for i in g.nodes.len..<s.len:
+      if s[i] == setToTrue:
+        let counter = usedVersions.getOrDefault(mapping[i - g.nodes.len][0])
+        if counter > 0:
+          error c, toName(mapping[i - g.nodes.len][0]), $mapping[i - g.nodes.len][2] & " required"

 proc traverseLoop(c: var AtlasContext; g: var DepGraph; startIsDep: bool): seq[CfgPath] =
  if c.lockMode == useLock:
@@ -694,7 +758,8 @@ proc traverseLoop(c: var AtlasContext; g: var DepGraph; startIsDep: bool): seq[C
    let destDir = toDestDir(w.name)
    let oldErrors = c.errors

-    if not dirExists(c.workspace / destDir) and not dirExists(c.depsDir / destDir):
+    let dir = selectDir(c.workspace / destDir, c.depsDir / destDir)
+    if not dirExists(dir):
      withDir c, (if i != 0 or startIsDep: c.depsDir else: c.workspace):
        if w.url.startsWith(FileProtocol):
          copyFromDisk c, w
@@ -702,10 +767,16 @@ proc traverseLoop(c: var AtlasContext; g: var DepGraph; startIsDep: bool): seq[C
          let err = cloneUrl(c, w.url, destDir, false)
          if err != "":
            error c, w.name, err
+          elif w.algo != MinVer:
+            collectAvailableVersions c, g, w
+    elif w.algo != MinVer:
+      withDir c, dir:
+        collectAvailableVersions c, g, w
+
    # assume this is the selected version, it might get overwritten later:
    selectNode c, g, w
    if oldErrors == c.errors:
-      if KeepCommits notin c.flags:
+      if KeepCommits notin c.flags and w.algo == MinVer:
        if not w.url.startsWith(FileProtocol):
          checkoutCommit(c, g, w)
        else:
@@ -719,20 +790,27 @@ proc traverseLoop(c: var AtlasContext; g: var DepGraph; startIsDep: bool): seq[C
      result.addUnique collectNewDeps(c, g, i, w)
    inc i

+  if g.availableVersions.len > 0:
+    resolve c, g
  if c.lockMode == genLock:
    writeFile c.currentDir / LockFileName, toJson(c.lockFile).pretty

+proc createGraph(c: var AtlasContext; start, url: string): DepGraph =
+  result = DepGraph(nodes: @[Dependency(name: toName(start), url: url, commit: "", self: 0,
+                                       algo: c.defaultAlgo)])
+  result.byName.mgetOrPut(toName(start), @[]).add 0
+
 proc traverse(c: var AtlasContext; start: string; startIsDep: bool): seq[CfgPath] =
  # returns the list of paths for the nim.cfg file.
  let url = toUrl(c, start)
-  var g = DepGraph(nodes: @[Dependency(name: toName(start), url: url, commit: "", self: 0)])
-  g.byName.mgetOrPut(toName(start), @[]).add 0
+  var g = createGraph(c, start, url)

  if url == "":
    error c, toName(start), "cannot resolve package name"
    return

  c.projectDir = c.workspace / toDestDir(g.nodes[0].name)
+
  result = traverseLoop(c, g, startIsDep)
  afterGraphActions c, g

@@ -793,7 +871,8 @@ proc installDependencies(c: var AtlasContext; nimbleFile: string; startIsDep: bo
  # 2. install deps from .nimble
  var g = DepGraph(nodes: @[])
  let (_, pkgname, _) = splitFile(nimbleFile)
-  let dep = Dependency(name: toName(pkgname), url: "", commit: "", self: 0)
+  let dep = Dependency(name: toName(pkgname), url: "", commit: "", self: 0,
+                       algo: c.defaultAlgo)
  discard collectDeps(c, g, -1, dep, nimbleFile)
  let paths = traverseLoop(c, g, startIsDep)
  patchNimCfg(c, paths, if CfgHere in c.flags: c.currentDir else: findSrcDir(c))
@@ -936,6 +1015,11 @@ proc readConfig(c: var AtlasContext) =
        c.depsDir = absoluteDepsDir(c.workspace, e.value)
      of "overrides":
        parseOverridesFile(c, e.value)
+      of "resolver":
+        try:
+          c.defaultAlgo = parseEnum[ResolutionAlgorithm](e.value)
+        except ValueError:
+          warn c, toName(configFile), "ignored unknown resolver: " & e.key
      else:
        warn c, toName(configFile), "ignored unknown setting: " & e.key
    of cfgOption:
@@ -1007,7 +1091,9 @@ proc setupNimEnv(c: var AtlasContext; nimVersion: string) =
  withDir c, c.workspace / nimDest:
    let nimExe = "bin" / "nim".addFileExt(ExeExt)
    copyFileWithPermissions nimExe0, nimExe
-    let dep = Dependency(name: toName(nimDest), rel: normal, commit: nimVersion, self: 0)
+    let dep = Dependency(name: toName(nimDest), commit: nimVersion, self: 0,
+                         algo: c.defaultAlgo,
+                         query: createQueryEq(if nimVersion.isDevel: Version"#head" else: Version(nimVersion)))
    if not nimVersion.isDevel:
      let commit = versionToCommit(c, dep)
      if commit.len == 0:
@@ -1056,7 +1142,8 @@ proc listOutdated(c: var AtlasContext; dir: string) =
                # git merge-base --is-ancestor <commit> <commit>
                let (cc, status) = exec(c, GitMergeBase, [currentCommit, latestVersion])
                let mergeBase = strutils.strip(cc)
-                #echo f, " I'm at ", currentCommit, " release is at ", latestVersion, " merge base is ", mergeBase
+                #if mergeBase != latestVersion:
+                #  echo f, " I'm at ", currentCommit, " release is at ", latestVersion, " merge base is ", mergeBase
                if status == 0 and mergeBase == currentCommit:
                  let v = extractVersion gitDescribeRefTag(c, latestVersion)
                  if v.len > 0:
@@ -1141,6 +1228,11 @@ proc main =
        of "off": c.flags.incl NoColors
        of "on": c.flags.excl NoColors
        else: writeHelp()
+      of "resolver":
+        try:
+          c.defaultAlgo = parseEnum[ResolutionAlgorithm](val)
+        except ValueError:
+          quit "unknown resolver: " & val
      else: writeHelp()
    of cmdEnd: assert false, "cannot happen"

--- a/atlas/sat.nim
+++ b/atlas/sat.nim
@@ -0,0 +1,313 @@
+## SAT solver
+## (c) 2021 Andreas Rumpf
+## Based on explanations and Haskell code from
+## https://andrew.gibiansky.com/blog/verification/writing-a-sat-solver/
+
+## Formulars as packed ASTs, no pointers no cry. Solves formulars with many
+## thousands of variables in no time.
+
+type
+  FormKind* = enum
+    FalseForm, TrueForm, VarForm, NotForm, AndForm, OrForm, ExactlyOneOfForm # roughly 8 so the last 3 bits
+  BaseType = int32
+  Atom = distinct BaseType
+  VarId* = distinct BaseType
+  Formular* = seq[Atom] # linear storage
+
+proc `==`*(a, b: VarId): bool {.borrow.}
+
+const
+  KindBits = 3
+  KindMask = 0b111
+
+template kind(a: Atom): FormKind = FormKind(BaseType(a) and KindMask)
+template intVal(a: Atom): BaseType = BaseType(a) shr KindBits
+
+proc newVar*(val: VarId): Atom {.inline.} =
+  Atom((BaseType(val) shl KindBits) or BaseType(VarForm))
+
+proc newOperation(k: FormKind; val: BaseType): Atom {.inline.} =
+  Atom((val shl KindBits) or BaseType(k))
+
+proc trueLit(): Atom {.inline.} = Atom(TrueForm)
+proc falseLit(): Atom {.inline.} = Atom(FalseForm)
+
+proc lit(k: FormKind): Atom {.inline.} = Atom(k)
+
+when false:
+  proc isTrueLit(a: Atom): bool {.inline.} = a.kind == TrueForm
+  proc isFalseLit(a: Atom): bool {.inline.} = a.kind == FalseForm
+
+proc varId(a: Atom): VarId =
+  assert a.kind == VarForm
+  result = VarId(BaseType(a) shr KindBits)
+
+type
+  PatchPos = distinct int
+  FormPos = distinct int
+
+proc prepare(dest: var Formular; source: Formular; sourcePos: FormPos): PatchPos =
+  result = PatchPos dest.len
+  dest.add source[sourcePos.int]
+
+proc patch(f: var Formular; pos: PatchPos) =
+  let pos = pos.int
+  let k = f[pos].kind
+  assert k > VarForm
+  let distance = int32(f.len - pos)
+  f[pos] = newOperation(k, distance)
+
+proc nextChild(f: Formular; pos: var int) {.inline.} =
+  let x = f[int pos]
+  pos += (if x.kind <= VarForm: 1 else: int(intVal(x)))
+
+iterator sonsReadonly(f: Formular; n: FormPos): FormPos =
+  var pos = n.int
+  assert f[pos].kind > VarForm
+  let last = pos + f[pos].intVal
+  inc pos
+  while pos < last:
+    yield FormPos pos
+    nextChild f, pos
+
+iterator sons(dest: var Formular; source: Formular; n: FormPos): FormPos =
+  let patchPos = prepare(dest, source, n)
+  for x in sonsReadonly(source, n): yield x
+  patch dest, patchPos
+
+# String representation
+
+proc toString(dest: var string; f: Formular; n: FormPos) =
+  assert n.int >= 0
+  assert n.int < f.len
+  case f[n.int].kind
+  of FalseForm: dest.add 'F'
+  of TrueForm: dest.add 'T'
+  of VarForm:
+    dest.add 'v'
+    dest.addInt varId(f[n.int]).int
+  else:
+    case f[n.int].kind
+    of AndForm:
+      dest.add "(&"
+    of OrForm:
+      dest.add "(|"
+    of ExactlyOneOfForm:
+      dest.add "(1=="
+    of NotForm:
+      dest.add "(~"
+    else: assert false, "cannot happen"
+    for child in sonsReadonly(f, n):
+      toString(dest, f, child)
+      dest.add ' '
+    dest[^1] = ')'
+
+proc `$`*(f: Formular): string =
+  assert f.len > 0
+  toString(result, f, FormPos 0)
+
+type
+  Builder* = object
+    f: Formular
+    toPatch: seq[PatchPos]
+
+proc isEmpty*(b: Builder): bool {.inline.} =
+  b.f.len == 0 or b.f.len == 1 and b.f[0].kind in {NotForm, AndForm, OrForm, ExactlyOneOfForm}
+
+proc openOpr*(b: var Builder; k: FormKind) =
+  b.toPatch.add PatchPos b.f.len
+  b.f.add newOperation(k, 0)
+
+proc add*(b: var Builder; a: Atom) =
+  b.f.add a
+
+proc closeOpr*(b: var Builder) =
+  patch(b.f, b.toPatch.pop())
+
+proc toForm*(b: var Builder): Formular =
+  assert b.toPatch.len == 0, "missing `closeOpr` calls"
+  result = move b.f
+
+# Code from the blog translated into Nim and into our representation
+
+const
+  NoVar = VarId(-1)
+
+proc freeVariable(f: Formular): VarId =
+  ## returns NoVar if there is no free variable.
+  for i in 0..<f.len:
+    if f[i].kind == VarForm: return varId(f[i])
+  return NoVar
+
+type
+  BindingKind* = enum
+    dontCare,
+    setToFalse,
+    setToTrue
+  Solution* = seq[BindingKind]
+
+proc simplify(dest: var Formular; source: Formular; n: FormPos; sol: Solution): FormKind =
+  ## Returns either a Const constructor or a simplified expression;
+  ## if the result is not a Const constructor, it guarantees that there
+  ## are no Const constructors in the source tree further down.
+  let s = source[n.int]
+  result = s.kind
+  case result
+  of FalseForm, TrueForm:
+    # nothing interesting to do:
+    dest.add s
+  of VarForm:
+    let v = varId(s).int
+    if v < sol.len:
+      case sol[v]
+      of dontCare:
+        dest.add s
+      of setToFalse:
+        dest.add falseLit()
+        result = FalseForm
+      of setToTrue:
+        dest.add trueLit()
+        result = TrueForm
+    else:
+      dest.add s
+  of NotForm:
+    let oldLen = dest.len
+    var inner: FormKind
+    for child in sons(dest, source, n):
+      inner = simplify(dest, source, child, sol)
+    if inner in {FalseForm, TrueForm}:
+      setLen dest, oldLen
+      result = (if inner == FalseForm: TrueForm else: FalseForm)
+      dest.add lit(result)
+  of AndForm, OrForm:
+    let (tForm, fForm) = if result == AndForm: (TrueForm, FalseForm)
+                         else:                 (FalseForm, TrueForm)
+
+    let initialLen = dest.len
+    var childCount = 0
+    for child in sons(dest, source, n):
+      let oldLen = dest.len
+
+      let inner = simplify(dest, source, child, sol)
+      # ignore 'and T' or 'or F' subexpressions:
+      if inner == tForm:
+        setLen dest, oldLen
+      elif inner == fForm:
+        # 'and F' is always false and 'or T' is always true:
+        result = fForm
+        break
+      else:
+        inc childCount
+
+    if result == fForm:
+      setLen dest, initialLen
+      dest.add lit(result)
+    elif childCount == 1:
+      for i in initialLen..<dest.len-1:
+        dest[i] = dest[i+1]
+      setLen dest, dest.len-1
+      result = dest[initialLen].kind
+    elif childCount == 0:
+      # that means all subexpressions where ignored:
+      setLen dest, initialLen
+      result = tForm
+      dest.add lit(result)
+  of ExactlyOneOfForm:
+    let initialLen = dest.len
+    var childCount = 0
+    var couldEval = 0
+    for child in sons(dest, source, n):
+      let oldLen = dest.len
+
+      let inner = simplify(dest, source, child, sol)
+      # ignore 'exactlyOneOf F' subexpressions:
+      if inner == FalseForm:
+        setLen dest, oldLen
+      else:
+        if inner == TrueForm:
+          inc couldEval
+        inc childCount
+
+    if couldEval == childCount:
+      setLen dest, initialLen
+      if couldEval != 1:
+        dest.add lit FalseForm
+      else:
+        dest.add lit TrueForm
+    elif childCount == 1:
+      for i in initialLen..<dest.len-1:
+        dest[i] = dest[i+1]
+      setLen dest, dest.len-1
+      result = dest[initialLen].kind
+
+proc satisfiable*(f: Formular; s: var Solution): bool =
+  let v = freeVariable(f)
+  if v == NoVar:
+    result = f[0].kind == TrueForm
+  else:
+    result = false
+    # We have a variable to guess.
+    # Construct the two guesses.
+    # Return whether either one of them works.
+    if v.int >= s.len: s.setLen v.int+1
+    # try `setToFalse` first so that we don't end up with unnecessary dependencies:
+    s[v.int] = setToFalse
+
+    var falseGuess: Formular
+    let res = simplify(falseGuess, f, FormPos 0, s)
+
+    if res == TrueForm:
+      result = true
+    else:
+      result = satisfiable(falseGuess, s)
+      if not result:
+        s[v.int] = setToTrue
+
+        var trueGuess: Formular
+        let res = simplify(trueGuess, f, FormPos 0, s)
+
+        if res == TrueForm:
+          result = true
+        else:
+          result = satisfiable(trueGuess, s)
+          if not result:
+            # heuristic that provides a solution that comes closest to the "real" conflict:
+            s[v.int] = if trueGuess.len <= falseGuess.len: setToFalse else: setToTrue
+
+when isMainModule:
+  proc main =
+    var b: Builder
+    b.openOpr(AndForm)
+
+    b.openOpr(OrForm)
+    b.add newVar(VarId 1)
+    b.add newVar(VarId 2)
+    b.add newVar(VarId 3)
+    b.add newVar(VarId 4)
+    b.closeOpr
+
+    b.openOpr(ExactlyOneOfForm)
+    b.add newVar(VarId 5)
+    b.add newVar(VarId 6)
+    b.add newVar(VarId 7)
+
+    #b.openOpr(NotForm)
+    b.add newVar(VarId 8)
+    #b.closeOpr
+    b.closeOpr
+
+    b.add newVar(VarId 5)
+    b.add newVar(VarId 6)
+    b.closeOpr
+
+    let f = toForm(b)
+    echo "original: "
+    echo f
+
+    var s: Solution
+    echo satisfiable(f, s)
+    echo "solution"
+    for i in 0..<s.len:
+      echo "v", i, " ", s[i]
+
+  main()
--- a/atlas/tester.nim
+++ b/atlas/tester.nim
@@ -3,6 +3,9 @@
 import std / [strutils, os, sequtils]
 from std/private/gitutils import diffFiles

+if execShellCmd("nim c -r atlas/versions.nim") != 0:
+  quit("FAILURE: unit tests in atlas/versions.nim failed")
+
 var failures = 0

 when defined(develop):
--- a/atlas/tests/ws_conflict/expected/atlas.lock
+++ b/atlas/tests/ws_conflict/expected/atlas.lock
@@ -2,7 +2,7 @@
  "items": {
    "apkg": {
      "url": "file://./source/apkg",
-      "commit": "<invalid commit>"
+      "commit": "#head"
    },
    "bpkg": {
      "url": "file://./source/bpkg",
--- a/atlas/tests/ws_conflict/expected/deps.dot
+++ b/atlas/tests/ws_conflict/expected/deps.dot
@@ -1,11 +1,11 @@
 digraph deps {
-"file://./source/apkg/<invalid commit>" [label=""];
+"file://./source/apkg/#head" [label=""];
 "file://./source/bpkg/1.0" [label=""];
 "file://./source/cpkg/1.0" [label="unused"];
 "file://./source/cpkg/2.0" [label=""];
 "file://./source/dpkg/1.0" [label=""];
-"file://./source/apkg/<invalid commit>" -> "file://./source/bpkg/1.0";
-"file://./source/apkg/<invalid commit>" -> "file://./source/cpkg/1.0";
+"file://./source/apkg/#head" -> "file://./source/bpkg/1.0";
+"file://./source/apkg/#head" -> "file://./source/cpkg/1.0";
 "file://./source/bpkg/1.0" -> "file://./source/cpkg/2.0";
 "file://./source/cpkg/2.0" -> "file://./source/dpkg/1.0";
 }
--- a/atlas/versions.nim
+++ b/atlas/versions.nim
@@ -0,0 +1,348 @@
+#
+#           Atlas Package Cloner
+#        (c) Copyright 2021 Andreas Rumpf
+#
+#    See the file "copying.txt", included in this
+#    distribution, for details about the copyright.
+#
+
+import std / [strutils, parseutils, algorithm]
+
+type
+  Version* = distinct string
+
+  VersionRelation* = enum
+    verGe, # >= V -- Equal or later
+    verGt, # > V
+    verLe, # <= V -- Equal or earlier
+    verLt, # < V
+    verEq, # V
+    verAny, # *
+    verSpecial # #head
+
+  VersionReq* = object
+    r: VersionRelation
+    v: Version
+
+  VersionInterval* = object
+    a: VersionReq
+    b: VersionReq
+    isInterval: bool
+
+template versionKey*(i: VersionInterval): string = i.a.v.string
+
+proc createQueryEq*(v: Version): VersionInterval =
+  VersionInterval(a: VersionReq(r: verEq, v: v))
+
+proc extractGeQuery*(i: VersionInterval): Version =
+  if i.a.r in {verGe, verGt, verEq}:
+    result = i.a.v
+  else:
+    result = Version""
+
+proc `$`*(v: Version): string {.borrow.}
+
+proc isSpecial(v: Version): bool =
+  result = v.string.len > 0 and v.string[0] == '#'
+
+proc isValidVersion*(v: string): bool {.inline.} =
+  result = v.len > 0 and v[0] in {'#'} + Digits
+
+proc isHead(v: Version): bool {.inline.} = cmpIgnoreCase(v.string, "#head") == 0
+
+template next(l, p, s: untyped) =
+  if l > 0:
+    inc p, l
+    if p < s.len and s[p] == '.':
+      inc p
+    else:
+      p = s.len
+  else:
+    p = s.len
+
+proc lt(a, b: string): bool {.inline.} =
+  var i = 0
+  var j = 0
+  while i < a.len or j < b.len:
+    var x = 0
+    let l1 = parseSaturatedNatural(a, x, i)
+
+    var y = 0
+    let l2 = parseSaturatedNatural(b, y, j)
+
+    if x < y:
+      return true
+    elif x == y:
+      discard "continue"
+    else:
+      return false
+    next l1, i, a
+    next l2, j, b
+
+  result = false
+
+proc `<`*(a, b: Version): bool =
+  # Handling for special versions such as "#head" or "#branch".
+  if a.isSpecial or b.isSpecial:
+    if a.isHead: return false
+    if b.isHead: return true
+    # any order will do as long as the "sort" operation moves #thing
+    # to the bottom:
+    if a.isSpecial and b.isSpecial:
+      return a.string < b.string
+  return lt(a.string, b.string)
+
+proc eq(a, b: string): bool {.inline.} =
+  var i = 0
+  var j = 0
+  while i < a.len or j < b.len:
+    var x = 0
+    let l1 = parseSaturatedNatural(a, x, i)
+
+    var y = 0
+    let l2 = parseSaturatedNatural(b, y, j)
+
+    if x == y:
+      discard "continue"
+    else:
+      return false
+    next l1, i, a
+    next l2, j, b
+
+  result = true
+
+proc `==`*(a, b: Version): bool =
+  if a.isSpecial or b.isSpecial:
+    result = a.string == b.string
+  else:
+    result = eq(a.string, b.string)
+
+proc parseVer(s: string; start: var int): Version =
+  if start < s.len and s[start] == '#':
+    var i = start
+    while i < s.len and s[i] notin Whitespace: inc i
+    result = Version s.substr(start, i-1)
+    start = i
+  elif start < s.len and s[start] in Digits:
+    var i = start
+    while i < s.len and s[i] in Digits+{'.'}: inc i
+    result = Version s.substr(start, i-1)
+    start = i
+  else:
+    result = Version""
+
+proc parseVersion*(s: string; start: int): Version =
+  var i = start
+  result = parseVer(s, i)
+
+proc parseSuffix(s: string; start: int; result: var VersionInterval; err: var bool) =
+  # >= 1.5 & <= 1.8
+  #        ^ we are here
+  var i = start
+  while i < s.len and s[i] in Whitespace: inc i
+  # Nimble doesn't use the syntax `>= 1.5, < 1.6` but we do:
+  if i < s.len and s[i] in {'&', ','}:
+    inc i
+    while i < s.len and s[i] in Whitespace: inc i
+    if s[i] == '<':
+      inc i
+      var r = verLt
+      if s[i] == '=':
+        inc i
+        r = verLe
+      while i < s.len and s[i] in Whitespace: inc i
+      result.b = VersionReq(r: r, v: parseVer(s, i))
+      result.isInterval = true
+      while i < s.len and s[i] in Whitespace: inc i
+      # we must have parsed everything:
+      if i < s.len:
+        err = true
+
+proc parseVersionInterval*(s: string; start: int; err: var bool): VersionInterval =
+  var i = start
+  while i < s.len and s[i] in Whitespace: inc i
+  result = VersionInterval(a: VersionReq(r: verAny, v: Version""))
+  if i < s.len:
+    case s[i]
+    of '*': result = VersionInterval(a: VersionReq(r: verAny, v: Version""))
+    of '#', '0'..'9':
+      result = VersionInterval(a: VersionReq(r: verEq, v: parseVer(s, i)))
+      if result.a.v.isHead: result.a.r = verAny
+      err = i < s.len
+    of '=':
+      inc i
+      if i < s.len and s[i] == '=': inc i
+      while i < s.len and s[i] in Whitespace: inc i
+      result = VersionInterval(a: VersionReq(r: verEq, v: parseVer(s, i)))
+      err = i < s.len
+    of '<':
+      inc i
+      var r = verLt
+      if i < s.len and s[i] == '=':
+        r = verLe
+        inc i
+      while i < s.len and s[i] in Whitespace: inc i
+      result = VersionInterval(a: VersionReq(r: r, v: parseVer(s, i)))
+      parseSuffix(s, i, result, err)
+    of '>':
+      inc i
+      var r = verGt
+      if i < s.len and s[i] == '=':
+        r = verGe
+        inc i
+      while i < s.len and s[i] in Whitespace: inc i
+      result = VersionInterval(a: VersionReq(r: r, v: parseVer(s, i)))
+      parseSuffix(s, i, result, err)
+    else:
+      err = true
+  else:
+    result = VersionInterval(a: VersionReq(r: verAny, v: Version"#head"))
+
+proc parseTaggedVersions*(outp: string): seq[(string, Version)] =
+  result = @[]
+  for line in splitLines(outp):
+    if not line.endsWith("^{}"):
+      var i = 0
+      while i < line.len and line[i] notin Whitespace: inc i
+      let commitEnd = i
+      while i < line.len and line[i] in Whitespace: inc i
+      while i < line.len and line[i] notin Digits: inc i
+      let v = parseVersion(line, i)
+      if v != Version(""):
+        result.add (line.substr(0, commitEnd-1), v)
+  result.sort proc (a, b: (string, Version)): int =
+    (if a[1] < b[1]: 1
+    elif a[1] == b[1]: 0
+    else: -1)
+
+proc matches(pattern: VersionReq; v: Version): bool =
+  case pattern.r
+  of verGe:
+    result = pattern.v < v or pattern.v == v
+  of verGt:
+    result = pattern.v < v
+  of verLe:
+    result = v < pattern.v or pattern.v == v
+  of verLt:
+    result = v < pattern.v
+  of verEq, verSpecial:
+    result = pattern.v == v
+  of verAny:
+    result = true
+
+proc matches*(pattern: VersionInterval; v: Version): bool =
+  if pattern.isInterval:
+    result = matches(pattern.a, v) and matches(pattern.b, v)
+  else:
+    result = matches(pattern.a, v)
+
+proc selectBestCommitMinVer*(data: openArray[(string, Version)]; elem: VersionInterval): string =
+  for i in countdown(data.len-1, 0):
+    if elem.matches(data[i][1]):
+      return data[i][0]
+  return ""
+
+proc selectBestCommitMaxVer*(data: openArray[(string, Version)]; elem: VersionInterval): string =
+  for i in countup(0, data.len-1):
+    if elem.matches(data[i][1]): return data[i][0]
+  return ""
+
+proc toSemVer*(i: VersionInterval): VersionInterval =
+  result = i
+  if not result.isInterval and result.a.r in {verGe, verGt}:
+    var major = 0
+    let l1 = parseSaturatedNatural(result.a.v.string, major, 0)
+    if l1 > 0:
+      result.isInterval = true
+      result.b = VersionReq(r: verLt, v: Version($(major+1)))
+
+proc selectBestCommitSemVer*(data: openArray[(string, Version)]; elem: VersionInterval): string =
+  result = selectBestCommitMaxVer(data, elem.toSemVer)
+
+when isMainModule:
+  template v(x): untyped = Version(x)
+
+  assert v"1.0" < v"1.0.1"
+  assert v"1.0" < v"1.1"
+  assert v"1.2.3" < v"1.2.4"
+  assert v"2.0.0" < v"2.0.0.1"
+  assert v"2.0.0" < v"20.0"
+  assert not (v"1.10.0" < v"1.2.0")
+  assert v"1.0" < v"#head"
+  assert v"#branch" < v"#head"
+  assert v"#branch" < v"1.0"
+  assert not (v"#head" < v"#head")
+  assert not (v"#head" < v"10.0")
+
+  const lines = """
+24870f48c40da2146ce12ff1e675e6e7b9748355 1.6.12
+b54236aaee2fc90200cb3a4e7070820ced9ce605 1.6.10
+f06dc8ee3baf8f64cce67a28a6e6e8a8cd9bf04b 1.6.8
+2f85924354af35278a801079b7ff3f8805ff1f5a 1.6.6
+007bf1cb52eac412bc88b3ca2283127ad578ec04 1.6.4
+ee18eda86eef2db0a49788bf0fc8e35996ba7f0d 1.6.2
+1a2a82e94269741b0d8ba012994dd85a53f36f2d 1.6.0
+074f7159752b0da5306bdedb3a4e0470af1f85c0 1.4.8
+4eb05ebab2b4d8b0cd00b19a72af35a2d767819a 1.4.6
+944c8e6d04a044611ed723391272f3c86781eadd 1.4.4
+cd090a6151b452b99d65c5173400d4685916f970 1.4.2
+01dd8c7a959adac4aa4d73abdf62cbc53ffed11b 1.4.0
+1420d508dc4a3e51137647926d4db2f3fa62f43c 1.2.18
+726e3bb1ffc6bacfaab0a0abf0209640acbac807 1.2.16
+80d2206e68cd74020f61e23065c7a22376af8de5 1.2.14
+ddfe3905964fe3db33d7798c6c6c4a493cbda6a3 1.2.12
+6d914b7e6edc29c3b8ab8c0e255bd3622bc58bba 1.2.10
+0d1a9f5933eab686ab3b527b36d0cebd3949a503 1.2.8
+a5a0a9e3cb14e79d572ba377b6116053fc621f6d 1.2.6
+f9829089b36806ac0129c421bf601cbb30c2842c 1.2.4
+8b03d39fd387f6a59c97c2acdec2518f0b18a230 1.2.2
+a8a4725850c443158f9cab38eae3e54a78a523fb 1.2.0
+8b5888e0545ee3d931b7dd45d15a1d8f3d6426ef 1.0.10
+7282e53cad6664d09e8c9efd0d7f263521eda238 1.0.8
+283a4137b6868f1c5bbf0dd9c36d850d086fa007 1.0.6
+e826ff9b48af376fdc65ba22f7aa1c56dc169b94 1.0.4
+4c33037ef9d01905130b22a37ddb13748e27bb7c 1.0.2
+0b6866c0dc48b5ba06a4ce57758932fbc71fe4c2 1.0.0
+a202715d182ce6c47e19b3202e0c4011bece65d8 0.20.2
+8ea451196bd8d77b3592b8b34e7a2c49eed784c9 0.20.0
+1b512cc259b262d06143c4b34d20ebe220d7fb5c 0.19.6
+be22a1f4e04b0fec14f7a668cbaf4e6d0be313cb 0.19.4
+5cbc7f6322de8460cc4d395ed0df6486ae68004e 0.19.2
+79934561e8dde609332239fbc8b410633e490c61 0.19.0
+9c53787087e36b1c38ffd670a077903640d988a8 0.18.0
+a713ffd346c376cc30f8cc13efaee7be1b8dfab9 0.17.2
+2084650f7bf6f0db6003920f085e1a86f1ea2d11 0.17.0
+f7f68de78e9f286b704304836ed8f20d65acc906 0.16.0
+48bd4d72c45f0f0202a0ab5ad9d851b05d363988 0.15.2
+dbee7d55bc107b2624ecb6acde7cabe4cb3f5de4 0.15.0
+0a4854a0b7bcef184f060632f756f83454e9f9de 0.14.2
+5333f2e4cb073f9102f30aacc7b894c279393318 0.14.0
+7e50c5b56d5b5b7b96e56b6c7ab5e104124ae81b 0.13.0
+49bce0ebe941aafe19314438fb724c081ae891aa 0.12.0
+70789ef9c8c4a0541ba24927f2d99e106a6fe6cc 0.11.2
+79cc0cc6e501c8984aeb5b217a274877ec5726bc 0.11.0
+46d829f65086b487c08d522b8d0d3ad36f9a2197 0.10.2
+9354d3de2e1ecc1747d6c42fbfa209fb824837c0 0.9.6
+6bf5b3d78c97ce4212e2dd4cf827d40800650c48 0.9.4
+220d35d9e19b0eae9e7cd1f1cac6e77e798dbc72 0.9.2
+7a70058005c6c76c92addd5fc21b9706717c75e3 0.9.0
+32b4192b3f0771af11e9d850046e5f3dd42a9a5f 0.8.14
+"""
+
+  proc p(s: string): VersionInterval =
+    var err = false
+    result = parseVersionInterval(s, 0, err)
+    assert not err
+
+  let tags = parseTaggedVersions(lines)
+  let query = p">= 1.2 & < 1.4"
+  assert selectBestCommitMinVer(tags, query) == "a8a4725850c443158f9cab38eae3e54a78a523fb"
+
+  let query2 = p">= 1.2 & < 1.4"
+  assert selectBestCommitMaxVer(tags, query2) == "1420d508dc4a3e51137647926d4db2f3fa62f43c"
+
+  let query3 = p">= 0.20.0"
+  assert selectBestCommitSemVer(tags, query3) == "a202715d182ce6c47e19b3202e0c4011bece65d8"
+
+  let query4 = p"#head"
+  assert selectBestCommitSemVer(tags, query4) == "24870f48c40da2146ce12ff1e675e6e7b9748355"