Radish alpha
H
HardenedBSD Package Manager
Radicle
Git (anonymous pull)
Log in to clone via SSH
Add ability to parse the output of SAT solvers.
Vsevolod Stakhov committed 12 years ago
commit be8625029bce66854950e2e06d91ced0491512be
parent 2a73b920467bfd5f9c484f4cdbdc84cc1b8ff123
2 files changed +66 -0
modified libpkg/pkg.h.in
@@ -1192,6 +1192,12 @@ int pkg_solve_dimacs_export(struct pkg_solve_problem *problem, FILE *f);
int pkg_solve_sat_to_jobs(struct pkg_solve_problem *problem, struct pkg_jobs *j);

/**
+
 * Parse SAT solver output and convert it to jobs
+
 * @return error code
+
 */
+
int pkg_parse_sat_output(FILE *f, struct pkg_solve_problem *problem, struct pkg_jobs *j);
+

+
/**
 * Free a SAT problem structure
 */
void pkg_solve_problem_free(struct pkg_solve_problem *problem);
modified libpkg/pkg_solve.c
@@ -32,7 +32,10 @@
#include <libutil.h>
#include <stdbool.h>
#include <stdlib.h>
+
#define _WITH_GETLINE
+
#include <stdio.h>
#include <string.h>
+
#include <ctype.h>

#include "pkg.h"
#include "private/event.h"
@@ -699,3 +702,60 @@ pkg_solve_sat_to_jobs(struct pkg_solve_problem *problem, struct pkg_jobs *j)

	return (EPKG_OK);
}
+

+
int
+
pkg_parse_sat_output(FILE *f, struct pkg_solve_problem *problem, struct pkg_jobs *j)
+
{
+
	struct pkg_solve_ordered_variable *ordered_variables = NULL, *nord;
+
	struct pkg_solve_variable *var, *vtmp;
+
	int cur_ord = 1, ret = EPKG_OK;
+
	char *line = NULL, *var_str, *begin;
+
	size_t linecap = 0;
+
	ssize_t linelen;
+
	bool got_sat = false;
+

+
	/* Order variables */
+
	HASH_ITER(hd, problem->variables_by_digest, var, vtmp) {
+
		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(&line, &linecap, f)) > 0) {
+
		if (strncmp (line, "SAT", 3) == 0) {
+
			got_sat = true;
+
		}
+
		else if (got_sat) {
+
			begin = line;
+
			do {
+
				var_str = strsep(&begin, " \t");
+
				/* Skip unexpected lines */
+
				if (var_str == NULL || (!isdigit(*var_str) && *var_str != '-'))
+
					continue;
+
				cur_ord = 0;
+
				cur_ord = abs(strtol(var_str, NULL, 10));
+
				if (cur_ord == 0)
+
					break;
+

+
				HASH_FIND_INT(ordered_variables, &cur_ord, nord);
+
				if (nord != NULL) {
+
					nord->var->resolved = true;
+
					nord->var->to_install = (*var_str != '-');
+
				}
+
			} while (begin != NULL);
+
		}
+
		else {
+
			pkg_emit_error("got invalid line from SAT solver: %s", line);
+
			ret = EPKG_FATAL;
+
			goto end;
+
		}
+
	}
+

+
	ret = pkg_solve_sat_to_jobs(problem, j);
+
end:
+
	HASH_FREE(ordered_variables, pkg_solve_ordered_variable, free);
+
	if (line != NULL)
+
		free(line);
+
	return (ret);
+
}