From owner-freebsd-ports@freebsd.org Thu Nov 24 13:05:44 2016 Return-Path: Delivered-To: freebsd-ports@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id C385DC51865 for ; Thu, 24 Nov 2016 13:05:44 +0000 (UTC) (envelope-from hps@selasky.org) Received: from mailman.ysv.freebsd.org (unknown [127.0.1.3]) by mx1.freebsd.org (Postfix) with ESMTP id A687937C for ; Thu, 24 Nov 2016 13:05:44 +0000 (UTC) (envelope-from hps@selasky.org) Received: by mailman.ysv.freebsd.org (Postfix) id A5DD0C51862; Thu, 24 Nov 2016 13:05:44 +0000 (UTC) Delivered-To: ports@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id A54AAC51861; Thu, 24 Nov 2016 13:05:44 +0000 (UTC) (envelope-from hps@selasky.org) Received: from mail.turbocat.net (heidi.turbocat.net [88.198.202.214]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 4C88F37B; Thu, 24 Nov 2016 13:05:43 +0000 (UTC) (envelope-from hps@selasky.org) Received: from hps2016.home.selasky.org (unknown [62.141.129.119]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail.turbocat.net (Postfix) with ESMTPSA id 0F6181FE024; Thu, 24 Nov 2016 14:05:35 +0100 (CET) Subject: Re: Optimising generated rules for SAT solving (5/12 are duplicates) To: Vsevolod Stakhov , Ed Schouten References: <20150414200459.GE39658@ivaldir.etoilebsd.net> <20150421103454.GR1394@zxy.spb.ru> <5593D0AE.2010205@selasky.org> <416359ce-1dcd-1160-5c56-f120a0f6358f@selasky.org> <20160627115533.gqvdsmtzwnvrrfuo@ivaldir.etoilebsd.net> <0671148b-d7cd-f8ad-906d-a0baa1b98cf5@selasky.org> Cc: Baptiste Daroussin , Slawa Olhovchenkov , ports@freebsd.org, FreeBSD Current From: Hans Petter Selasky Message-ID: <9b0469bb-ab2b-4992-1d40-de748163f2c8@selasky.org> Date: Thu, 24 Nov 2016 14:05:18 +0100 User-Agent: Mozilla/5.0 (X11; FreeBSD amd64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0 MIME-Version: 1.0 In-Reply-To: Content-Type: multipart/mixed; boundary="------------6177813FFD2C97BC114024A6" X-BeenThere: freebsd-ports@freebsd.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Porting software to FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 24 Nov 2016 13:05:44 -0000 This is a multi-part message in MIME format. --------------6177813FFD2C97BC114024A6 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit On 11/24/16 13:13, Vsevolod Stakhov wrote: > On 23/11/2016 16:27, Ed Schouten wrote: >> Hi Hans, >> >> 2016-11-23 15:27 GMT+01:00 Hans Petter Selasky : >>> I've made a patch to hopefully optimise SAT solving in our pkg utility. >> >> Nice! Do you by any chance have any numbers that show the performance >> improvements made by this change? Assuming that the SAT solver of >> pkg(1) uses an algorithm similar to DPLL[1], a change like this would >> affect performance linearly. My guess is therefore that the running >> time is reduced by approximately 5/12. Is this correct? > > There won't be any improvement if you just remove duplicates from SAT > formula. This situation is handled by picosat internally and even for > naive DPLL there is no significant influence of duplicate KNF clauses: > once you've assumed all vars in some clause, you automatically resolve > all duplicates. > > Is there any real improvement of SAT solver speed with this patch? From > my experiences, SAT solving is negligible in terms of CPU time comparing > to other tasks performed by pkg. Hi, I added some code to measure the time for SAT solving. During my test run I'm seeing values in the range 8-10ms for both versions, so I consider that neglible. However, the unpatched version wants to reinstall 185 packages while the non-patched version wants to reinstall 1 package. That has a huge time influential. I'm not that familar with PKG that I can draw any conclusions from this. # Test1: echo "n" | /xxx/pkg/src/pkg-static upgrade --no-repo-update > b.txt # Test2: echo "n" | env PKG_NO_SORT=YES /xxx/pkg/src/pkg-static upgrade --no-repo-update > a.txt Please find the material attached including a debug version patch you can play with. --HPS --------------6177813FFD2C97BC114024A6 Content-Type: text/plain; charset=UTF-8; name="b.txt" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="b.txt" Checking for upgrades (748 candidates): .......... done Processing candidates (748 candidates): . done Skipped 3702 identical rules Reiterate SAT solving took 0s and 7370 usecs The following 52 package(s) will be affected (of 0 checked): Installed packages to be UPGRADED: xapian-core: 1.2.23,1 -> 1.2.24,1 webp: 0.5.0 -> 0.5.1_1 webkit2-gtk3: 2.8.5_6 -> 2.8.5_7 webkit-gtk2: 2.4.11_4 -> 2.4.11_5 vlc: 2.2.4_3,4 -> 2.2.4_4,4 trousers: 0.3.13_1 -> 0.3.14 tiff: 4.0.6_2 -> 4.0.7 thunderbird: 45.4.0_2 -> 45.5.0_1 sqlite3: 3.15.1 -> 3.15.1_1 spidermonkey170: 17.0.0_2 -> 17.0.0_3 soundtouch: 1.9.2 -> 1.9.2_1 raptor2: 2.0.15_4 -> 2.0.15_5 qt5-core: 5.6.2 -> 5.6.2_1 qt4-corelib: 4.8.7_5 -> 4.8.7_6 polkit: 0.113_1 -> 0.113_2 pciids: 20161029 -> 20161119 openimageio: 1.6.12_2 -> 1.6.12_3 openblas: 0.2.18_1,1 -> 0.2.18_2,1 openal-soft: 1.17.2 -> 1.17.2_1 libx264: 0.148.2708 -> 0.148.2708_1 libvpx: 1.6.0 -> 1.6.0_1 libvisio01: 0.1.5_3 -> 0.1.5_4 libreoffice: 5.2.3_2 -> 5.2.3_3 libpci: 3.5.1 -> 3.5.2 libmspub01: 0.1.2_4 -> 0.1.2_5 libfreehand: 0.1.1_3 -> 0.1.1_4 libe-book: 0.1.2_5 -> 0.1.2_6 libcdr01: 0.1.3_1 -> 0.1.3_2 lcms2: 2.7_2 -> 2.8 inkscape: 0.91_8 -> 0.91_9 icu: 57.1,1 -> 58.1,1 harfbuzz: 1.3.3 -> 1.3.3_1 gstreamer1-plugins: 1.8.0 -> 1.8.0_1 gstreamer-plugins: 0.10.36_6,3 -> 0.10.36_7,3 gstreamer: 0.10.36_4 -> 0.10.36_5 gnupg: 2.1.15 -> 2.1.16 glib: 2.46.2_3 -> 2.46.2_4 gcc: 4.8.5_2 -> 4.9.4 firefox: 50.0_2,1 -> 50.0_4,1 firebird25-client: 2.5.6_1 -> 2.5.6_2 ffmpeg: 2.8.8_5,1 -> 2.8.8_8,1 dejavu: 2.35 -> 2.37 chromium: 52.0.2743.116_2 -> 52.0.2743.116_4 boost-libs: 1.55.0_13 -> 1.55.0_14 blender: 2.77a -> 2.77a_1 belle-sip: 1.5.0 -> 1.5.0_1 bash: 4.4 -> 4.4.5 argyllcms: 1.7.0_1 -> 1.7.0_2 OpenEXR: 2.2.0_5 -> 2.2.0_6 ImageMagick: 6.9.5.10,1 -> 6.9.5.10_1,1 GraphicsMagick: 1.3.24,1 -> 1.3.24_1,1 Installed packages to be REINSTALLED: baresip-0.4.19 (options changed) Number of packages to be upgraded: 51 Number of packages to be reinstalled: 1 The process will require 19 MiB more space. 446 MiB to be downloaded. Proceed with this action? [y/N]: --------------6177813FFD2C97BC114024A6 Content-Type: text/plain; charset=UTF-8; name="a.txt" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="a.txt" Checking for upgrades (748 candidates): .......... done Processing candidates (748 candidates): . done Reiterate SAT solving took 0s and 5790 usecs The following 236 package(s) will be affected (of 0 checked): Installed packages to be UPGRADED: xapian-core: 1.2.23,1 -> 1.2.24,1 webp: 0.5.0 -> 0.5.1_1 webkit2-gtk3: 2.8.5_6 -> 2.8.5_7 webkit-gtk2: 2.4.11_4 -> 2.4.11_5 vlc: 2.2.4_3,4 -> 2.2.4_4,4 trousers: 0.3.13_1 -> 0.3.14 tiff: 4.0.6_2 -> 4.0.7 thunderbird: 45.4.0_2 -> 45.5.0_1 sqlite3: 3.15.1 -> 3.15.1_1 spidermonkey170: 17.0.0_2 -> 17.0.0_3 soundtouch: 1.9.2 -> 1.9.2_1 raptor2: 2.0.15_4 -> 2.0.15_5 qt5-core: 5.6.2 -> 5.6.2_1 qt4-corelib: 4.8.7_5 -> 4.8.7_6 polkit: 0.113_1 -> 0.113_2 pciids: 20161029 -> 20161119 openimageio: 1.6.12_2 -> 1.6.12_3 openblas: 0.2.18_1,1 -> 0.2.18_2,1 openal-soft: 1.17.2 -> 1.17.2_1 libx264: 0.148.2708 -> 0.148.2708_1 libvpx: 1.6.0 -> 1.6.0_1 libvisio01: 0.1.5_3 -> 0.1.5_4 libreoffice: 5.2.3_2 -> 5.2.3_3 libpci: 3.5.1 -> 3.5.2 libmspub01: 0.1.2_4 -> 0.1.2_5 libfreehand: 0.1.1_3 -> 0.1.1_4 libe-book: 0.1.2_5 -> 0.1.2_6 libcdr01: 0.1.3_1 -> 0.1.3_2 lcms2: 2.7_2 -> 2.8 inkscape: 0.91_8 -> 0.91_9 icu: 57.1,1 -> 58.1,1 harfbuzz: 1.3.3 -> 1.3.3_1 gstreamer1-plugins: 1.8.0 -> 1.8.0_1 gstreamer-plugins: 0.10.36_6,3 -> 0.10.36_7,3 gstreamer: 0.10.36_4 -> 0.10.36_5 gnupg: 2.1.15 -> 2.1.16 glib: 2.46.2_3 -> 2.46.2_4 gcc: 4.8.5_2 -> 4.9.4 firefox: 50.0_2,1 -> 50.0_4,1 firebird25-client: 2.5.6_1 -> 2.5.6_2 ffmpeg: 2.8.8_5,1 -> 2.8.8_8,1 dejavu: 2.35 -> 2.37 chromium: 52.0.2743.116_2 -> 52.0.2743.116_4 boost-libs: 1.55.0_13 -> 1.55.0_14 blender: 2.77a -> 2.77a_1 belle-sip: 1.5.0 -> 1.5.0_1 bash: 4.4 -> 4.4.5 argyllcms: 1.7.0_1 -> 1.7.0_2 OpenEXR: 2.2.0_5 -> 2.2.0_6 ImageMagick: 6.9.5.10,1 -> 6.9.5.10_1,1 GraphicsMagick: 1.3.24,1 -> 1.3.24_1,1 Installed packages to be REINSTALLED: yaml-cpp03-0.3.0 yajl-2.1.0 xvid-1.3.4,1 xcb-util-renderutil-0.3.9_1 xcb-util-keysyms-0.4.0_1 xcb-util-0.4.0_1,1 twolame-0.3.13_4 tpm-emulator-0.7.4_1 tinyxml-2.6.2_1 taglib-1.10 startup-notification-0.12_4 speexdsp-1.2.r3_1 speex-1.2.r2,1 speech-dispatcher-0.8.3_1 spandsp-0.0.6 snappy-1.1.3 serf-1.3.9_1 schroedinger-1.0.11_4 redland-1.0.17_4 readline-6.3.8 re2-20151101 rasqal-0.9.33 qt5-x11extras-5.6.2 qt5-widgets-5.6.2 python35-3.5.2 python27-2.7.12 popt-1.16_1 poppler-glib-0.46.0 poppler-0.46.0_2 pixman-0.34.0 perl5-5.24.1.r4 pcre-8.39 pangomm-2.36.0 pango-1.38.0_1 p11-kit-0.23.2 orc-0.4.25 opus-1.1.3 opensubdiv-3.0.5_2 openldap-client-2.4.44 openjpeg15-1.5.2_1 openjpeg-2.1.2_1 opencv2-core-2.4.13.1_1 opencolorio-1.0.9 opencollada-1.6.25 nss-3.27.1_1 nspr-4.13.1 npth-1.2 nettle-3.2 mythes-1.2.4 mpfr-3.1.5 mpc-1.0.3 lua52-5.2.4 libxslt-1.1.29 libxml2-2.9.4 libxcb-1.12 libwps-0.4.4 libwpg03-0.3.1 libwpd010-0.10.1 libwmf-0.2.8.4_15 libvorbis-1.3.5,3 libvdpau-1.1.1 libva-1.7.2 libv4l-1.6.3_2 libtheora-1.1.1_6 libtasn1-4.9 libsoup-2.52.2 libsndfile-1.0.27 libsigc++-2.4.1 libsecret-0.18.4 libsamplerate-0.1.9 librsvg2-2.40.16 librevenge-0.0.4_1 libpthread-stubs-0.3_6 libpciaccess-0.13.4 libpaper-1.1.24.4 libpagemaker-0.0.3 libogg-1.3.2_1,4 libodfgen01-0.1.6 libmwaw03-0.3.8 libmpeg2-0.5.1_6 libmatroska-1.4.5 libmad-0.15.1b_6 libltdl-2.4.6 liblqr-1-0.4.2 libidn-1.33_1 libiconv-1.14_9 libgltf-0.0.2_1 libglapi-11.2.2 libgcrypt-1.7.3 libfpx-1.3.1.4_1 libffi-3.2.1 libexttextcat-3.4.4 libevent2-2.0.22_1 libetonyek01-0.1.6,1 libepoxy-1.3.1 libedit-3.1.20150325_2,1 libdvdread-5.0.3 libdvdnav-5.0.3 libdvbpsi-1.3.0 libdrm-2.4.66,1 libdca-0.0.5_1 libcroco-0.6.11 libcmis-0.5.1 libcddb-1.3.2_4 libassuan-2.4.3 libantlr3c-3.4_1 libabw-0.1.1_1 liba52-0.7.4_3 libXxf86vm-1.1.4_1 libXvMC-1.0.10 libXv-1.0.11,1 libXtst-1.2.3 libXt-1.1.5,1 libXrender-0.9.10 libXrandr-1.5.1 libXmu-1.1.2_3,1 libXinerama-1.1.3_3,1 libXi-1.7.8,1 libXft-2.3.2_1 libXfixes-5.0.3 libXext-1.3.3_1,1 libXdmcp-1.1.2 libXdamage-1.1.4_3 libXcursor-1.1.14_3 libXcomposite-0.4.4_3,1 libXaw-1.0.13,2 libXau-1.0.8_3 libXScrnSaver-1.2.2_3 libX11-1.6.4,1 libSM-1.2.2_3,1 libIDL-0.8.14_2 libICE-1.0.9_1,1 libGLU-9.0.0_2 libGL-11.2.2 libEGL-11.2.2 jpeg-turbo-1.5.1 jbigkit-2.1_1 jasper-1.900.1_16 ilmbase-2.2.0 hyphen-2.8.8 hunspell-1.3.3 gtkspell-2.0.16_5 gtkmm24-2.24.4_2 gtk3-3.18.8_3 gtk2-2.24.29_2 gstreamer1-1.8.0 gsl-1.16_2 gnutls-3.4.16 gmp-5.1.3_3 glibmm-2.44.0,1 glew-1.13.0 giflib-5.1.4 gettext-runtime-0.19.8.1 gdk-pixbuf2-2.32.3_1 gconf2-3.2.6_4 gbm-11.2.2 freetype2-2.6.3 fontconfig-2.12.1,1 flac-1.3.1_2 fftw3-3.3.5 faad2-2.7_6,1 expat-2.2.0 espeak-1.48.04_1 enchant-1.6.0_5 dotconf-1.3_1 dbus-glib-0.104 dbus-1.8.20 db5-5.3.28_6 curl-7.51.0_1 cups-2.2.1 colord-1.2.11_1 clucene-2.3.3.4_7 cairomm-1.10.0_3 cairo-1.14.6_1,2 boehm-gc-7.6.0 bctoolbox-0.2.0 baresip-0.4.19 (options changed) avahi-app-0.6.31_5 atkmm-2.22.7 atk-2.18.0 at-spi2-atk-2.18.1 apr-1.5.2.1.5.4_2 alsa-lib-1.1.2 ORBit2-2.14.19_1 CoinMP-1.8.3 Number of packages to be upgraded: 51 Number of packages to be reinstalled: 185 The process will require 19 MiB more space. 491 MiB to be downloaded. Proceed with this action? [y/N]: --------------6177813FFD2C97BC114024A6 Content-Type: text/x-patch; name="0001-Optimise-SAT-solving.patch" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="0001-Optimise-SAT-solving.patch" >From 135812278d74a3dd632713885ba47daa05a2b175 Mon Sep 17 00:00:00 2001 From: Hans Petter Selasky Date: Thu, 24 Nov 2016 13:35:37 +0100 Subject: [PATCH] Optimise SAT solving. Signed-off-by: Hans Petter Selasky --- libpkg/pkg_solve.c | 317 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 315 insertions(+), 2 deletions(-) diff --git a/libpkg/pkg_solve.c b/libpkg/pkg_solve.c index 9cf08e2..d50281f 100644 --- a/libpkg/pkg_solve.c +++ b/libpkg/pkg_solve.c @@ -1074,8 +1074,299 @@ pkg_solve_set_initial_assumption(struct pkg_solve_problem *problem, } } -int -pkg_solve_sat_problem(struct pkg_solve_problem *problem) +static int +pkg_solve_item_compare(const void *ppa, const void *ppb) +{ + struct pkg_solve_item *ia = *(struct pkg_solve_item **)ppa; + struct pkg_solve_item *ib = *(struct pkg_solve_item **)ppb; + int va = ia->var->order * ia->inverse; + int vb = ib->var->order * ib->inverse; + + if (va > vb) + return (1); + else if (va < vb) + return (-1); + return (0); +} + +static int +pkg_solve_rule_compare(const void *ppa, const void *ppb) +{ + struct pkg_solve_rule *ra = *(struct pkg_solve_rule **)ppa; + struct pkg_solve_rule *rb = *(struct pkg_solve_rule **)ppb; + struct pkg_solve_item *ia; + struct pkg_solve_item *ib; + size_t na = 0; + size_t nb = 0; + + LL_FOREACH(ra->items, ia) + na++; + LL_FOREACH(rb->items, ib) + nb++; + + if (na > nb) + return (1); + else if (na < nb) + return (-1); + + ia = ra->items; + ib = rb->items; + while (ia != 0 && ib != 0) { + int va = ia->var->order * ia->inverse; + int vb = ib->var->order * ib->inverse; + if (va > vb) + return (1); + else if (va < vb) + return (-1); + ia = ia->next; + ib = ib->next; + } + return (0); +} + +static int +pkg_solve_sat_problem_sub(struct pkg_solve_problem *problem) +{ + struct pkg_solve_rule **rule_array; + struct pkg_solve_rule *rule; + struct pkg_solve_item *item; + int res, iter = 0; + size_t skipped = 0; + size_t i; + size_t n; + bool need_reiterate = false; + const int *failed = NULL; + int attempt = 0; + struct pkg_solve_variable *var; + + rule_array = (struct pkg_solve_rule **)calloc(kv_size(problem->rules), sizeof(void *)); + if (rule_array == NULL) + return (EPKG_FATAL); + + n = kv_size(problem->rules); + for (i = 0; i != n; i++) { + size_t j; + size_t k; + + rule = kv_A(problem->rules, i); + rule_array[i] = rule; + + j = 0; + LL_FOREACH(rule->items, item) + j++; + + struct pkg_solve_item *item_array[j]; + + j = 0; + LL_FOREACH(rule->items, item) + item_array[j++] = item; + + mergesort(item_array, j, sizeof(void *), pkg_solve_item_compare); + + rule->items = 0; + for (k = 0; k != j; k++) { + /* if items are identical, skip them */ + if (k != j - 1 && + pkg_solve_item_compare(item_array + k, item_array + k + 1) == 0) { + free(item_array[k]); + continue; + } + item_array[k]->next = rule->items; + rule->items = item_array[k]; + } + } + + mergesort(rule_array, n, sizeof(void *), pkg_solve_rule_compare); + + for (i = 0; i != n; i++) { + /* if rules are identical, skip them */ + if (i != n - 1 && + pkg_solve_rule_compare(rule_array + i, rule_array + i + 1) == 0) { + skipped++; + continue; + } + rule = rule_array[i]; + LL_FOREACH(rule->items, item) { + picosat_add(problem->sat, item->var->order * item->inverse); + } + + picosat_add(problem->sat, 0); + pkg_debug_print_rule(rule); + } + + for (i = 0; i != n; i++) { + /* if rules are identical, skip them */ + if (i != n - 1 && + pkg_solve_rule_compare(rule_array + i, rule_array + i + 1) == 0) + continue; + rule = rule_array[i]; + pkg_solve_set_initial_assumption(problem, rule); + } + + free(rule_array); + + pkg_emit_notice("Skipped %lld identical rules", (long long)skipped); + +reiterate: + pkg_emit_notice("Reiterate"); + + res = pkg_solve_picosat_iter(problem, iter); + + if (res != PICOSAT_SATISFIABLE) { + /* + * in case we cannot satisfy the problem it appears by + * experience that the culprit seems to always be the latest of + * listed in the failed assumptions. + * So try to remove them for the given problem. + * To avoid endless loop allow a maximum of 10 iterations no + * more + */ + failed = picosat_failed_assumptions(problem->sat); + attempt++; + + /* get the last failure */ + while (*failed) { + failed++; + } + failed--; + + if (attempt >= 10) { + pkg_emit_error("Cannot solve problem using SAT solver"); + UT_string *sb; + utstring_new(sb); + + while (*failed) { + var = &problem->variables[abs(*failed) - 1]; + for (i = 0; i < kv_size(problem->rules); i++) { + rule = kv_A(problem->rules, i); + + if (rule->reason != PKG_RULE_DEPEND) { + LL_FOREACH(rule->items, item) { + if (item->var == var) { + pkg_print_rule_buf(rule, sb); + utstring_printf(sb, "%c", '\n'); + break; + } + } + } + } + + utstring_printf(sb, "cannot %s package %s, remove it from request? ", + var->flags & PKG_VAR_INSTALL ? "install" : "remove", var->uid); + + if (pkg_emit_query_yesno(true, utstring_body(sb))) { + var->flags |= PKG_VAR_FAILED; + } + + failed++; + need_reiterate = true; + } + utstring_clear(sb); + } else { + pkg_emit_notice("Cannot solve problem using SAT solver, trying another plan"); + var = &problem->variables[abs(*failed) - 1]; + + var->flags |= PKG_VAR_FAILED; + + need_reiterate = true; + } + +#if 0 + failed = picosat_next_maximal_satisfiable_subset_of_assumptions(problem->sat); + + while (*failed) { + struct pkg_solve_variable *var = &problem->variables[*failed - 1]; + + pkg_emit_notice("var: %s", var->uid); + + failed ++; + } + + return (EPKG_AGAIN); +#endif + } + else { + + /* Assign vars */ + for (i = 0; i < problem->nvars; i ++) { + int val = picosat_deref(problem->sat, i + 1); + struct pkg_solve_variable *var = &problem->variables[i]; + + if (val > 0) + var->flags |= PKG_VAR_INSTALL; + else + var->flags &= ~PKG_VAR_INSTALL; + + pkg_debug(2, "decided %s %s-%s to %s", + var->unit->pkg->type == PKG_INSTALLED ? "local" : "remote", + var->uid, var->digest, + var->flags & PKG_VAR_INSTALL ? "install" : "delete"); + } + + /* Check for reiterations */ + if ((problem->j->type == PKG_JOBS_INSTALL || + problem->j->type == PKG_JOBS_UPGRADE) && iter == 0) { + for (i = 0; i < problem->nvars; i ++) { + bool failed_var = false; + struct pkg_solve_variable *var = &problem->variables[i], *cur; + + if (!(var->flags & PKG_VAR_INSTALL)) { + LL_FOREACH(var, cur) { + if (cur->flags & PKG_VAR_INSTALL) { + failed_var = false; + break; + } + else if (cur->unit->pkg->type == PKG_INSTALLED) { + failed_var = true; + } + } + } + + /* + * If we want to delete local packages on installation, do one more SAT + * iteration to ensure that we have no other choices + */ + if (failed_var) { + pkg_debug (1, "trying to delete local package %s-%s on install/upgrade," + " reiterate on SAT", + var->unit->pkg->name, var->unit->pkg->version); + need_reiterate = true; + + LL_FOREACH(var, cur) { + cur->flags |= PKG_VAR_FAILED; + } + } + } + } + } + + if (need_reiterate) { + iter ++; + + /* Restore top-level assumptions */ + for (i = 0; i < problem->nvars; i ++) { + struct pkg_solve_variable *var = &problem->variables[i]; + + if (var->flags & PKG_VAR_TOP) { + if (var->flags & PKG_VAR_FAILED) { + var->flags ^= PKG_VAR_INSTALL | PKG_VAR_FAILED; + } + + picosat_assume(problem->sat, var->order * + (var->flags & PKG_VAR_INSTALL ? 1 : -1)); + } + } + + need_reiterate = false; + + goto reiterate; + } + + return (EPKG_OK); +} + +static int +pkg_solve_sat_problem_old(struct pkg_solve_problem *problem) { struct pkg_solve_rule *rule; struct pkg_solve_item *item; @@ -1103,6 +1394,7 @@ pkg_solve_sat_problem(struct pkg_solve_problem *problem) } reiterate: + pkg_emit_notice("Reiterate"); res = pkg_solve_picosat_iter(problem, iter); @@ -1259,6 +1551,27 @@ reiterate: return (EPKG_OK); } +int +pkg_solve_sat_problem(struct pkg_solve_problem *problem) +{ + struct timeval tv0; + gettimeofday(&tv0, NULL); + int err; + + if (getenv("PKG_NO_SORT") != NULL) + err = pkg_solve_sat_problem_old(problem); + else + err = pkg_solve_sat_problem_sub(problem); + struct timeval tv1; + gettimeofday(&tv1, NULL); + + timersub(&tv1, &tv0, &tv1); + + pkg_emit_notice("SAT solving took %llds and %lld usecs", (long long)tv1.tv_sec, (long long)tv1.tv_usec); + + return (err); +} + void pkg_solve_dot_export(struct pkg_solve_problem *problem, FILE *file) { -- 2.10.1 --------------6177813FFD2C97BC114024A6--