Re: pkg SAT_SOLVER bugs
On Tue, Jun 28, 2016 at 05:52:32PM +0200, Hans Petter Selasky wrote: > On 06/27/16 13:55, Baptiste Daroussin wrote: > > On Mon, Jun 27, 2016 at 12:38:02PM +0200, Hans Petter Selasky wrote: > > > Hi, > > > > > > I found some bugs in PKG with regard to the SAT_SOLVER environment > > > variable. > > > Please find patch attached :-) > > > > > > Issues fixed: > > > 1) No need to use hash table when generating SAT rules for external > > > solver. > > > Variables are already in a linear array. Fix encoding and decoding of SAT > > > data. > > > 2) Endless variable loop caused pkg to crash. > > > 3) it->inverse was checked for non-zero, while it should actually be > > > checked > > > for -1 only. SAT rules produces were all negative. > > > > > > How to verify: > > > > > > make -C /usr/ports/math/picosat all install clean > > > > > > env SAT_SOLVER=picosat pkg upgrade > > > > > > --HPS > > > > Thank you I will look into shortly > > > > Hi Baptiste, > > Are you handling this one or do you want me to create an issue at github. > Thank you! > I am handling it BTW not that picosat is the one we use internally already :D Best regards Bapt signature.asc Description: PGP signature
Re: pkg SAT_SOLVER bugs
On 27/06/2016 8:38 PM, Hans Petter Selasky wrote: > Hi, > > I found some bugs in PKG with regard to the SAT_SOLVER environment > variable. Please find patch attached :-) > > Issues fixed: > 1) No need to use hash table when generating SAT rules for external > solver. Variables are already in a linear array. Fix encoding and > decoding of SAT data. > 2) Endless variable loop caused pkg to crash. > 3) it->inverse was checked for non-zero, while it should actually be > checked for -1 only. SAT rules produces were all negative. > > How to verify: > > make -C /usr/ports/math/picosat all install clean > > env SAT_SOLVER=picosat pkg upgrade > > --HPS > Heads-up: Have just updated picosat to its latest version, enjoy! ___ freebsd-current@freebsd.org mailing list https://lists.freebsd.org/mailman/listinfo/freebsd-current To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"
Re: pkg SAT_SOLVER bugs
On 06/27/16 13:55, Baptiste Daroussin wrote: On Mon, Jun 27, 2016 at 12:38:02PM +0200, Hans Petter Selasky wrote: Hi, I found some bugs in PKG with regard to the SAT_SOLVER environment variable. Please find patch attached :-) Issues fixed: 1) No need to use hash table when generating SAT rules for external solver. Variables are already in a linear array. Fix encoding and decoding of SAT data. 2) Endless variable loop caused pkg to crash. 3) it->inverse was checked for non-zero, while it should actually be checked for -1 only. SAT rules produces were all negative. How to verify: make -C /usr/ports/math/picosat all install clean env SAT_SOLVER=picosat pkg upgrade --HPS Thank you I will look into shortly Hi Baptiste, Are you handling this one or do you want me to create an issue at github. Thank you! --HPS ___ freebsd-current@freebsd.org mailing list https://lists.freebsd.org/mailman/listinfo/freebsd-current To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"
Re: pkg SAT_SOLVER bugs
On Mon, Jun 27, 2016 at 12:38:02PM +0200, Hans Petter Selasky wrote: > Hi, > > I found some bugs in PKG with regard to the SAT_SOLVER environment variable. > Please find patch attached :-) > > Issues fixed: > 1) No need to use hash table when generating SAT rules for external solver. > Variables are already in a linear array. Fix encoding and decoding of SAT > data. > 2) Endless variable loop caused pkg to crash. > 3) it->inverse was checked for non-zero, while it should actually be checked > for -1 only. SAT rules produces were all negative. > > How to verify: > > make -C /usr/ports/math/picosat all install clean > > env SAT_SOLVER=picosat pkg upgrade > > --HPS Thank you I will look into shortly Best regards, Bapt signature.asc Description: PGP signature
Re: pkg SAT_SOLVER bugs
On 27/06/2016 8:38 PM, Hans Petter Selasky wrote: > Hi, > > I found some bugs in PKG with regard to the SAT_SOLVER environment > variable. Please find patch attached :-) Nice! Can you report upstream @ https://github.com/freebsd/pkg if you haven't already > Issues fixed: > 1) No need to use hash table when generating SAT rules for external > solver. Variables are already in a linear array. Fix encoding and > decoding of SAT data. > 2) Endless variable loop caused pkg to crash. > 3) it->inverse was checked for non-zero, while it should actually be > checked for -1 only. SAT rules produces were all negative. > > How to verify: > > make -C /usr/ports/math/picosat all install clean > > env SAT_SOLVER=picosat pkg upgrade > > --HPS ___ freebsd-current@freebsd.org mailing list https://lists.freebsd.org/mailman/listinfo/freebsd-current To unsubscribe, send any mail to "freebsd-current-unsubscr...@freebsd.org"
pkg SAT_SOLVER bugs
Hi,
I found some bugs in PKG with regard to the SAT_SOLVER environment
variable. Please find patch attached :-)
Issues fixed:
1) No need to use hash table when generating SAT rules for external
solver. Variables are already in a linear array. Fix encoding and
decoding of SAT data.
2) Endless variable loop caused pkg to crash.
3) it->inverse was checked for non-zero, while it should actually be
checked for -1 only. SAT rules produces were all negative.
How to verify:
make -C /usr/ports/math/picosat all install clean
env SAT_SOLVER=picosat pkg upgrade
--HPS
--- ./work/pkg-1.8.99.6/libpkg/pkg_solve.c.orig 2016-06-27 10:32:46.11981 +0200
+++ ./work/pkg-1.8.99.6/libpkg/pkg_solve.c 2016-06-27 12:28:07.901757000 +0200
@@ -118,8 +118,6 @@
#define PKG_SOLVE_CHECK_ITEM(item)\
((item)->var->to_install ^ (item)->inverse)
-#define PKG_SOLVE_VAR_NEXT(a, e) ((e) == NULL ? [0] : (e + 1))
-
/*
* Utilities to convert jobs to SAT rule
*/
@@ -1302,45 +1300,23 @@
fprintf(file, "}\n");
}
-struct pkg_solve_ordered_variable {
- struct pkg_solve_variable *var;
- int order;
- UT_hash_handle hh;
-};
-
int
pkg_solve_dimacs_export(struct pkg_solve_problem *problem, FILE *f)
{
- struct pkg_solve_ordered_variable *ordered_variables = NULL, *nord;
- struct pkg_solve_variable *var;
struct pkg_solve_rule *rule;
struct pkg_solve_item *it;
- int cur_ord = 1;
-
- /* Order variables */
- var = NULL;
- while ((var = PKG_SOLVE_VAR_NEXT(problem->variables, var))) {
- nord = calloc(1, sizeof(struct pkg_solve_ordered_variable));
- nord->order = cur_ord ++;
- nord->var = var;
- HASH_ADD_PTR(ordered_variables, var, nord);
- }
fprintf(f, "p cnf %d %zu\n", (int)problem->nvars, kv_size(problem->rules));
for (unsigned int i = 0; i < kv_size(problem->rules); i++) {
rule = kv_A(problem->rules, i);
LL_FOREACH(rule->items, it) {
- HASH_FIND_PTR(ordered_variables, >var, nord);
- if (nord != NULL) {
-fprintf(f, "%s%d ", (it->inverse ? "-" : ""), nord->order);
- }
+ size_t order = it->var - problem->variables;
+ if (order < problem->nvars)
+fprintf(f, "%ld ", (long)((order + 1) * it->inverse));
}
fprintf(f, "0\n");
}
-
- HASH_FREE(ordered_variables, free);
-
return (EPKG_OK);
}
@@ -1443,26 +1419,42 @@
return (EPKG_OK);
}
+static bool
+pkg_solve_parse_sat_output_store(struct pkg_solve_problem *problem, const char *var_str)
+{
+ struct pkg_solve_variable *var;
+ ssize_t order;
+
+ order = strtol(var_str, NULL, 10);
+ if (order == 0)
+ return (true);
+ if (order < 0) {
+ /* negative value means false */
+ order = - order - 1;
+ if ((size_t)order < problem->nvars) {
+ var = problem->variables + order;
+ var->flags &= ~PKG_VAR_INSTALL;
+ }
+ } else {
+ /* positive value means true */
+ order = order - 1;
+ if ((size_t)order < problem->nvars) {
+ var = problem->variables + order;
+ var->flags |= PKG_VAR_INSTALL;
+ }
+ }
+ return (false);
+}
+
int
pkg_solve_parse_sat_output(FILE *f, struct pkg_solve_problem *problem)
{
- struct pkg_solve_ordered_variable *ordered_variables = NULL, *nord;
- struct pkg_solve_variable *var;
- int cur_ord = 1, ret = EPKG_OK;
+ int ret = EPKG_OK;
char *line = NULL, *var_str, *begin;
size_t linecap = 0;
ssize_t linelen;
bool got_sat = false, done = false;
- /* Order variables */
- var = NULL;
- while ((var = PKG_SOLVE_VAR_NEXT(problem->variables, var))) {
- nord = calloc(1, sizeof(struct pkg_solve_ordered_variable));
- nord->order = cur_ord ++;
- nord->var = var;
- HASH_ADD_INT(ordered_variables, order, nord);
- }
-
while ((linelen = getline(, , f)) > 0) {
if (strncmp(line, "SAT", 3) == 0) {
got_sat = true;
@@ -1474,22 +1466,8 @@
/* Skip unexpected lines */
if (var_str == NULL || (!isdigit(*var_str) && *var_str != '-'))
continue;
-cur_ord = 0;
-cur_ord = abs((int)strtol(var_str, NULL, 10));
-if (cur_ord == 0) {
+if (pkg_solve_parse_sat_output_store(problem, var_str))
done = true;
- break;
-}
-
-HASH_FIND_INT(ordered_variables, _ord, nord);
-if (nord != NULL) {
- if (*var_str == '-') {
- nord->var->flags &= ~PKG_VAR_INSTALL;
- }
- else {
- nord->var->flags |= PKG_VAR_INSTALL;
- }
-}
} while (begin != NULL);
}
else if (strncmp(line, "v ", 2) == 0) {
@@ -1499,23 +1477,8 @@
/* Skip unexpected lines */
if (var_str == NULL || (!isdigit(*var_str) && *var_str != '-'))
continue;
-cur_ord = 0;
-cur_ord = abs((int)strtol(var_str, NULL, 10));
-if (cur_ord == 0) {
+if (pkg_solve_parse_sat_output_store(problem, var_str))
done = true;
- break;
-}
-
-HASH_FIND_INT(ordered_variables, _ord, nord);
-
-if (nord != NULL) {
- if (*var_str == '-') {
- nord->var->flags &= ~PKG_VAR_INSTALL;
- }
- else {
- nord->var->flags |= PKG_VAR_INSTALL;
- }
-}
} while (begin != NULL);
}
else {
@@ -1531,7 +1494,6 @@
ret = EPKG_FATAL;
}
-
