apt-solver-z3.cc

/*
 * SPDX-License-Identifier: GPL-2.0-or-later
 *
 * Copyright (C) 2021 Julian Andres Klode <jak@jak-linux.org>
 *
 * Some portions included below are taken from the dummy apt solver, and hence
 * share its copyright owners.
 *
 */

#include <apt-pkg/cachefile.h>
#include <apt-pkg/error.h>
#include <apt-pkg/init.h>
#include <apt-pkg/pkgsystem.h>
#include <apt-pkg/strutl.h>
#include <numeric>
#include <unordered_map>
#include <z3++.h>

struct ProblemTranslator
{
   z3::context context;
   z3::optimize solver;
   pkgDepCache *cache;

   std::unordered_map<pkgCache::Package *, z3::expr> packages;
   std::unordered_map<pkgCache::Version *, z3::expr> versions;
   std::unordered_map<std::string, pkgCache::PkgIterator> rpackages;
   std::unordered_map<std::string, pkgCache::VerIterator> rversions;

   ProblemTranslator(pkgDepCache *cache) : context(), solver(context), cache(cache){};

   void translateInstalled()
   {
      for (auto pkg = cache->PkgBegin(); not pkg.end(); pkg++)
      {
	 if ((*cache)[pkg].Install())
	 {
	    translatePackage(pkg);
	    auto v = translateVersion(pkgCache::VerIterator(*cache, (*cache)[pkg].InstallVer));
	    std::cerr << "Adding " << v << std::endl;
	    solver.add(v);
	 }
	 else if ((*cache)[pkg].Delete())
	 {
	    solver.add(!translatePackage(pkg));
	 }
	 else if (pkg->CurrentVer && ((*cache)[pkg].Flags & pkgCache::Flag::Auto) == 0)
	 {
	    solver.add(translatePackage(pkg));
	 }
      }
   }

   z3::expr translatePackage(pkgCache::PkgIterator pkg)
   {
      if (auto found = packages.find(pkg); found != packages.end())
	 return found->second;

      auto name = pkg.FullName();
      auto expr = context.bool_const(name.c_str());

      packages.insert({pkg, expr});
      rpackages.insert({name, pkg});

      z3::expr_vector versions(context);
      if (pkg->CurrentVer)
      {
	 versions.push_back(translateVersion(pkg.CurrentVer()));
	 solver.add_soft(versions[versions.size() - 1], 1);
      }

      if (auto cand = cache->GetCandidateVersion(pkg); not cand.end() && cand->ID != pkg.CurrentVer()->ID)
      {
	 versions.push_back(translateVersion(cand));
	 solver.add_soft(!versions[versions.size() - 1], 1);
      }

      if (versions.empty())
      {
	 solver.add(!expr);
      }
      else
      {
	 // If package is installed, either version must be installed, and vice versa
	 solver.add(expr == z3::atleast(versions, 1));
	 // only one version may be installed
	 solver.add(z3::atmost(versions, 1));
      }

      return expr;
   }

   z3::expr translateVersion(pkgCache::VerIterator ver)
   {
      if (auto found = versions.find(ver); found != versions.end())
	 return found->second;
      auto name = ver.ParentPkg().FullName() + "=" + (ver.VerStr());
      auto expr = context.bool_const(name.c_str());

      versions.insert({ver, expr});
      rversions.insert({name, ver});

      translateDependencies(expr, ver.DependsList());

      return expr;
   }

   //
   z3::expr *maybeTranslateVersion(pkgCache::VerIterator ver)
   {
      translatePackage(ver.ParentPkg());
      if (auto found = versions.find(ver); found != versions.end())
	 return &found->second;
      return nullptr;
   }

   void translateDependencies(z3::expr source, pkgCache::DepIterator dep)
   {
      {
	 for (; !dep.end(); dep++)
	    switch (dep->Type)
	    {
	    case pkgCache::Dep::Recommends:
	       continue;
	    case pkgCache::Dep::Depends:
	    case pkgCache::Dep::PreDepends:
	    {
	       z3::expr_vector versions(context);
	       for (;; dep++)
	       {
		  std::unique_ptr<pkgCache::Version *[]> targets(dep.AllTargets());
		  for (int i = 0; targets[i] != nullptr; i++)
		  {
		     auto ver = maybeTranslateVersion(pkgCache::VerIterator(cache->GetCache(), targets[i]));
		     if (ver != nullptr)
			versions.push_back(*ver);
		  }
		  if ((dep->CompareOp & pkgCache::Dep::Or) == 0)
		     break;
	       }

	       if (versions.empty())
		  solver.add(!source);
	       else
		  solver.add(z3::implies(source, z3::atleast(versions, 1)));
	       break;
	    }
	    case pkgCache::Dep::DpkgBreaks:
	    case pkgCache::Dep::Conflicts:
	    {
	       z3::expr_vector versions(context);
	       std::unique_ptr<pkgCache::Version *[]> targets(dep.AllTargets());
	       versions.push_back(source);
	       for (int i = 0; targets[i] != nullptr; i++)
	       {
		  auto ver = maybeTranslateVersion(pkgCache::VerIterator(cache->GetCache(), targets[i]));
		  if (ver != nullptr)
		     versions.push_back(*ver);
	       }
	       solver.add(z3::atmost(versions, 1));
	    }
	    }
      }
   }
};
#if 0
int main(int argc, char *argv[])
{
   pkgCacheFile cache;
   pkgInitConfig(*_config);
   pkgInitSystem(*_config, _system);

   if (!cache.Open(nullptr, false))
      return _error->DumpErrors(), 1;

   ProblemTranslator tr(cache);
   std::cout << "BEGIN TRANSLATE\n";
   tr.translateInstalled();
   std::cout << "END TRANSLATE\n";
   //   std::cout << tr.solver;
   std::cout << "BEGIN CHECK\n";
   std::cout << tr.solver.check();
   auto model = tr.solver.get_model();
   std::cout << "END CHECK\n";

   for (size_t i = 0; i < model.num_consts(); i++) {
      auto decl = model.get_const_decl(i);
      if (decl.name().str().find("=") == std::string::npos)
	 continue;
      auto ver = tr.rversions[decl.name().str()];
      auto pkg = ver.ParentPkg();
      auto inst = model.get_const_interp(decl).is_true();

      if (inst && not pkg->CurrentVer)
	 std::cout << "Install " << pkg.Name() << " " << ver.VerStr() << std::endl;
      else if (inst &&  pkg->CurrentVer && pkg.CurrentVer()->ID != ver->ID)
	 std::cout << "Upgrade " << pkg.Name() << " " << pkg.CurrentVer().VerStr() << " -> " << ver.VerStr() << std::endl;
      else if (not inst &&  pkg->CurrentVer && pkg.CurrentVer()->ID == ver->ID)
	 std::cout << "Delete " << pkg.Name() << " " << pkg.CurrentVer().VerStr() << "(" << ver.VerStr() << ")" << std::endl;


   }
}
#else

// -*- mode: cpp; mode: fold -*-
// Description								/*{{{*/
/* #####################################################################

   cover around the internal solver to be able to run it like an external

   ##################################################################### */
/*}}}*/
// Include Files							/*{{{*/
#include <apt-pkg/algorithms.h>
#include <apt-pkg/cachefile.h>
#include <apt-pkg/cacheset.h>
#include <apt-pkg/cmndline.h>
#include <apt-pkg/configuration.h>
#include <apt-pkg/depcache.h>
#include <apt-pkg/edsp.h>
#include <apt-pkg/error.h>
#include <apt-pkg/fileutl.h>
#include <apt-pkg/init.h>
#include <apt-pkg/pkgcache.h>
#include <apt-pkg/pkgsystem.h>
#include <apt-pkg/strutl.h>
#include <apt-pkg/upgrade.h>

#include <chrono>
#include <cstdio>
#include <iostream>
#include <list>
#include <sstream>
#include <string>
#include <stdlib.h>
#include <string.h>
#include <unistd.h>

/*}}}*/

static bool ShowHelp(CommandLine &) /*{{{*/
{
   std::cout << ("Usage: apt-internal-solver\n"
		 "\n"
		 "apt-internal-solver is an interface to use the current internal\n"
		 "resolver for the APT family like an external one, for debugging or\n"
		 "the like.\n");
   return true;
}
/*}}}*/
APT_NORETURN static void DIE(std::string const &message)
{ /*{{{*/
   std::cerr << "ERROR: " << message << std::endl;
   _error->DumpErrors(std::cerr);
   exit(EXIT_FAILURE);
}
/*}}}*/
static bool WriteSolution(pkgDepCache &Cache, FileFd &output) /*{{{*/
{
   bool Okay = output.Failed() == false;
   for (pkgCache::PkgIterator Pkg = Cache.PkgBegin(); Pkg.end() == false && (Okay); ++Pkg)
   {
      std::string action;
      if (Cache[Pkg].Delete() == true)
	 Okay &= EDSP::WriteSolutionStanza(output, "Remove", Pkg.CurrentVer());
      else if (Cache[Pkg].NewInstall() == true || Cache[Pkg].Upgrade() == true)
	 Okay &= EDSP::WriteSolutionStanza(output, "Install", Cache.GetCandidateVersion(Pkg));
      else if (Cache[Pkg].Garbage == true)
	 Okay &= EDSP::WriteSolutionStanza(output, "Autoremove", Pkg.CurrentVer());
   }
   return Okay;
}
/*}}}*/
int main(int argc, const char *argv[]) /*{{{*/
{
   if (pkgInitConfig(*_config) == false)
      DIE("System could not be initialized!");

   // we really don't need anything
   DropPrivileges();

   // Deal with stdout not being a tty
   if (!isatty(STDOUT_FILENO) && _config->FindI("quiet", -1) == -1)
      _config->Set("quiet", "1");

   if (_config->FindI("quiet", 0) < 1)
      _config->Set("Debug::EDSP::WriteSolution", true);

   _config->Set("APT::System", "Debian APT solver interface");
   _config->Set("APT::Solver", "internal");
   _config->Set("edsp::scenario", "/nonexistent/stdin");
   _config->Clear("Dir::Log");
   FileFd output;
   if (output.OpenDescriptor(STDOUT_FILENO, FileFd::WriteOnly | FileFd::BufferedWrite, true) == false)
      DIE("stdout couldn't be opened");
   int const input = STDIN_FILENO;
   SetNonBlock(input, false);

   EDSP::WriteProgress(0, "Start up solver…", output);

   if (pkgInitSystem(*_config, _system) == false)
      DIE("System could not be initialized!");

   EDSP::WriteProgress(1, "Read request…", output);

   if (WaitFd(input, false, 5) == false)
      DIE("WAIT timed out in the resolver");

   std::list<std::string> install, remove;
   unsigned int flags;
   if (EDSP::ReadRequest(input, install, remove, flags) == false)
      DIE("Parsing the request failed!");

   EDSP::WriteProgress(5, "Read scenario…", output);

   pkgCacheFile CacheFile;
   if (CacheFile.Open(NULL, false) == false)
      DIE("Failed to open CacheFile!");

   EDSP::WriteProgress(50, "Apply request on scenario…", output);

   if (EDSP::ApplyRequest(install, remove, CacheFile) == false)
      DIE("Failed to apply request to depcache!");

   EDSP::WriteProgress(60, "Call problemresolver on current scenario…", output);

   std::chrono::steady_clock::time_point start = std::chrono::steady_clock::now();

   ProblemTranslator tr(CacheFile);
   tr.translateInstalled();
   std::cerr << "RESULT " << tr.solver.check() << std::endl;
   auto model = tr.solver.get_model();

   {
      pkgDepCache::ActionGroup ag(CacheFile);
      for (size_t i = 0; i < model.num_consts(); i++)
      {
	 auto decl = model.get_const_decl(i);
	 auto inst = model.get_const_interp(decl).is_true();

	 if (decl.name().str().find("=") == std::string::npos)
	 {
	    auto pkg = tr.rpackages[decl.name().str()];
	    if (!inst)
	       CacheFile->MarkDelete(pkg);

	    continue;
	 }
	 auto ver = tr.rversions[decl.name().str()];
	 auto pkg = ver.ParentPkg();

	 if (inst)
	 {
	    CacheFile->SetCandidateVersion(ver);
	    CacheFile->MarkInstall(pkg, false);
	    CacheFile->MarkProtected(pkg);
	 }
      }
   }
   std::chrono::steady_clock::time_point end = std::chrono::steady_clock::now();

   std::cerr << "Time difference = " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << " ms" << std::endl;
   EDSP::WriteProgress(95, "Write solution…", output);

   if (WriteSolution(CacheFile, output) == false)
      DIE("Failed to output the solution!");

   EDSP::WriteProgress(100, "Done", output);

   return 0;
}
/*}}}*/
#endif