WIP SAT solver integration fixes nim-lang#1162

src/nimble.nim

@@ -20,7 +20,8 @@ import nimblepkg/packageinfotypes, nimblepkg/packageinfo, nimblepkg/version,
        nimblepkg/nimscriptwrapper, nimblepkg/developfile, nimblepkg/paths,
        nimblepkg/nimbledatafile, nimblepkg/packagemetadatafile,
        nimblepkg/displaymessages, nimblepkg/sha1hashes, nimblepkg/syncfile,
-       nimblepkg/deps
+       nimblepkg/deps, nimblepkg/nimblesat
+import sat, satvars
 
 const
   nimblePathsFileName* = "nimble.paths"
@@ -92,9 +93,21 @@ proc processFreeDependencies(pkgInfo: PackageInfo,
   ## during build phase.
   assert not pkgInfo.isMinimal,
          "processFreeDependencies needs pkgInfo.requires"
-
+         
   var pkgList {.global.}: seq[PackageInfo]
-  once: pkgList = initPkgList(pkgInfo, options)
+  once: 
+    pkgList = initPkgList(pkgInfo, options)
+    #At this point we have all the installed packages
+    #If we can solve them all here, we just do it and call it a day. 
+    let allPackages = pkgList.mapIt(it.basicInfo)
+    if requirements.areRequirementsWithinPackages(allPackages):
+      let form = toFormular(requirements, allPackages)      
+      var s = createSolution(form.f)
+      if satisfiable(form.f, s):
+        for pkg in pkgList:
+          result.incl pkg
+        return result
+
   display("Verifying", "dependencies for $1@$2" %
           [pkgInfo.basicInfo.name, $pkgInfo.basicInfo.version],
           priority = HighPriority)

src/nimblepkg/nimblesat.nim

@@ -0,0 +1,54 @@
+import std/tables
+import sat, satvars #Notice this two files eventually will be a package. They are copied (untouch) from atlas
+import version, packageinfotypes
+
+type  
+  SatVarInfo* = object # attached information for a SAT variable
+    pkg: string
+    version: Version
+    index: int
+
+  Form* = object
+    f*: Formular
+    mapping: Table[VarId, SatVarInfo]
+    idgen: int32
+
+proc toFormular*(requirements: seq[PkgTuple], allPackages: seq[PackageBasicInfo]): Form =
+  var b = Builder()
+  var idgen: int32 = 0
+  var mapping = initTable[VarId, SatVarInfo]()
+  b.openOpr(AndForm)
+
+  for (pkgName, constraint) in requirements:
+    b.openOpr(ExactlyOneOfForm)
+    for pkg in allPackages:
+      if pkg.name != pkgName: continue
+      if pkg.version.withinRange(constraint):
+        let vid = VarId(idgen)
+        b.add(newVar(vid))
+        mapping[vid] = SatVarInfo(pkg: pkgName, version: pkg.version, index: idgen)
+        inc idgen
+    b.closeOpr()  
+
+  b.closeOpr()
+  Form(f: b.toForm(), mapping: mapping, idgen: idgen)
+
+proc getPackageVersions*(form: Form, s: var Solution): Table[string, Version] =
+  let m = maxVariable(form.f)
+  result = initTable[string, Version]()
+  for i in 0..<m:
+    let varId = VarId(i)
+    if isTrue(s, varId):
+      if varId in form.mapping:
+        let info = form.mapping[varId]
+        result[info.pkg] = info.version
+
+proc areRequirementsWithinPackages*(requirements: seq[PkgTuple], allPackages: seq[PackageBasicInfo]): bool = 
+  var found = 0
+  for (pkgName, constraint) in requirements:
+    for pgk in allPackages:
+      if pkgName == pgk.name and pgk.version.withinRange(constraint):
+        inc found
+        break
+  found == requirements.len
+