f46824e Add DIMACS exporter of a SAT problem. — HardenedBSD-pkg

rad:z3QDZAW2FAfuLvihrhiyDC9fAD8G9

HardenedBSD Package Manager

Add DIMACS exporter of a SAT problem.

Vsevolod Stakhov committed 12 years ago

commit f46824e23c95e22580c2979c9013728d6eaee4a0
parent 8a4a7e9

3 files changed +57 -0

modified libpkg/pkg.h.in

@@ -1178,6 +1178,12 @@ bool pkg_solve_sat_problem(struct pkg_solve_problem *problem);

 struct pkg_solve_problem * pkg_solve_jobs_to_sat(struct pkg_jobs *j);
 /**
  * Export sat problem to the DIMACS format
  * @return error code
  */
 int pkg_solve_dimacs_export(struct pkg_solve_problem *problem, FILE *f);
 /**
  * Free a SAT problem structure
  */
 void pkg_solve_problem_free(struct pkg_solve_problem *problem);

modified libpkg/pkg_jobs.c

@@ -927,6 +927,7 @@ pkg_jobs_solve(struct pkg_jobs *j)

 {
 	bool dry_run = false, cudf = false;
 	int ret;
 	struct pkg_solve_problem *problem;
 	if ((j->flags & PKG_FLAG_DRY_RUN) == PKG_FLAG_DRY_RUN)
 		dry_run = true;

@@ -959,6 +960,10 @@ pkg_jobs_solve(struct pkg_jobs *j)

 		if (pkg_config_bool(PKG_CONFIG_CUDF_SOLVER, &cudf) == EPKG_OK && cudf) {
 			ret = pkg_jobs_cudf_emit_file(j, j->type, stderr, j->db);
 		}
 		problem = pkg_solve_jobs_to_sat(j);
 		if (problem != NULL) {
 			pkg_solve_dimacs_export(problem, stderr);
 		}
 	}
 	return (ret);
 }

modified libpkg/pkg_solve.c

@@ -62,6 +62,7 @@ struct pkg_solve_rule {

 };
 struct pkg_solve_problem {
 	unsigned int rules_count;
 	struct pkg_solve_rule *rules;
 	struct pkg_solve_variable *variables;
 };

@@ -428,6 +429,7 @@ pkg_solve_add_pkg_rule(struct pkg_jobs *j, struct pkg_solve_problem *problem,

 			}
 			LL_PREPEND(problem->rules, rule);
 			problem->rules_count ++;
 		}
 		/* Go through all conflicts */

@@ -464,6 +466,7 @@ pkg_solve_add_pkg_rule(struct pkg_jobs *j, struct pkg_solve_problem *problem,

 				LL_PREPEND(rule->items, it);
 				LL_PREPEND(problem->rules, rule);
 				problem->rules_count ++;
 			}
 		}

@@ -496,6 +499,7 @@ pkg_solve_add_pkg_rule(struct pkg_jobs *j, struct pkg_solve_problem *problem,

 					LL_PREPEND(rule->items, it);
 					LL_PREPEND(problem->rules, rule);
 					problem->rules_count ++;
 				}
 			}
 		}

@@ -553,6 +557,7 @@ pkg_solve_jobs_to_sat(struct pkg_jobs *j)

 		/* Requests are unary rules */
 		LL_PREPEND(rule->items, it);
 		LL_PREPEND(problem->rules, rule);
 		problem->rules_count ++;
 	}
 	HASH_ITER(hh, j->request_delete, jreq, jtmp) {
 		rule = NULL;

@@ -577,6 +582,7 @@ pkg_solve_jobs_to_sat(struct pkg_jobs *j)

 		/* Requests are unary rules */
 		LL_PREPEND(rule->items, it);
 		LL_PREPEND(problem->rules, rule);
 		problem->rules_count ++;
 	}
 	/* Parse universe */

@@ -623,3 +629,43 @@ err:

 		pkg_solve_rule_free(rule);
 	return (NULL);
 }
 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, *vtmp;
 	struct pkg_solve_rule *rule;
 	struct pkg_solve_item *it;
 	int cur_ord = 1;
 	/* Order variables */
 	HASH_ITER(hd, problem->variables, var, vtmp) {
 		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 %d\n", HASH_CNT(hd, problem->variables), problem->rules_count);
 	LL_FOREACH(problem->rules, rule) {
 		LL_FOREACH(rule->items, it) {
 			HASH_FIND_PTR(ordered_variables, it->var, nord);
 			if (nord != NULL) {
 				fprintf(f, "%s%d ", (it->inverse ? "-" : ""), nord->order);
 			}
 		}
 		fprintf(f, "0\n");
 	}
 	HASH_FREE(ordered_variables, pkg_solve_ordered_variable, free);
 	return (EPKG_OK);
 }