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 <h...@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
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]: 
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]: 
>From 135812278d74a3dd632713885ba47daa05a2b175 Mon Sep 17 00:00:00 2001
From: Hans Petter Selasky <h...@selasky.org>
Date: Thu, 24 Nov 2016 13:35:37 +0100
Subject: [PATCH] Optimise SAT solving.

Signed-off-by: Hans Petter Selasky <h...@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

_______________________________________________
freebsd-ports@freebsd.org mailing list
https://lists.freebsd.org/mailman/listinfo/freebsd-ports
To unsubscribe, send any mail to "freebsd-ports-unsubscr...@freebsd.org"

Reply via email to