Date: Thu, 24 Nov 2016 14:05:18 +0100 From: Hans Petter Selasky <hps@selasky.org> To: Vsevolod Stakhov <vsevolod@highsecure.ru>, Ed Schouten <ed@nuxi.nl> Cc: Baptiste Daroussin <bapt@freebsd.org>, Slawa Olhovchenkov <slw@zxy.spb.ru>, ports@freebsd.org, FreeBSD Current <freebsd-current@freebsd.org> Subject: Re: Optimising generated rules for SAT solving (5/12 are duplicates) Message-ID: <9b0469bb-ab2b-4992-1d40-de748163f2c8@selasky.org> In-Reply-To: <d786cde5-89af-cb14-c42e-cc649cb32bdb@highsecure.ru> 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> <cbc964a7-5f90-6ea1-630d-414de68867b1@selasky.org> <CABh_MKm7LAtQzp9KEBpaRZWQQHnsUtNFiKVSVF70-wj4GmytuA@mail.gmail.com> <d786cde5-89af-cb14-c42e-cc649cb32bdb@highsecure.ru>
next in thread | previous in thread | raw e-mail | index | archive | help
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 <hps@selasky.org>:
>>> 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 <hps@selasky.org>
Date: Thu, 24 Nov 2016 13:35:37 +0100
Subject: [PATCH] Optimise SAT solving.
Signed-off-by: Hans Petter Selasky <hps@selasky.org>
---
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--
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?9b0469bb-ab2b-4992-1d40-de748163f2c8>