Radish alpha
H
HardenedBSD-pkg
rad:z3QDZAW2FAfuLvihrhiyDC9fAD8G9
HardenedBSD Package Manager
Radicle
Git
Commits › ead67db
Resolve UNSAT problems manually.
Vsevolod Stakhov committed 11 years ago
commit ead67db8da06837511bce5541901716a011cbca2
parent c28498b
3 files changed +49 -10
modified libpkg/pkg.h.in
@@ -466,7 +466,11 @@ typedef enum {
	/**

	 * A conflict between packages found

	 */
- 
	EPKG_CONFLICT
+ 
	EPKG_CONFLICT,
+ 
	/**
+ 
	 * Need to repeat operation
+ 
	 */
+ 
	EPKG_AGAIN

} pkg_error_t;



/**
@@ -1211,7 +1215,7 @@ int pkg_jobs_cudf_parse_output(struct pkg_jobs *j, FILE *f);
 * Solve a SAT problem

 * @return true if a problem is solvable

 */
- 
bool pkg_solve_sat_problem(struct pkg_solve_problem *problem);
+ 
int pkg_solve_sat_problem(struct pkg_solve_problem *problem);



/**

 * Convert package jobs to a SAT problem
modified libpkg/pkg_jobs.c
@@ -1527,6 +1527,7 @@ pkg_jobs_solve(struct pkg_jobs *j)
			waitpid(pchild, &pstatus, WNOHANG);

		}

		else {
+ 
again:

			pkg_jobs_universe_process_upgrade_chains(j);

			problem = pkg_solve_jobs_to_sat(j);

			if (problem != NULL) {
@@ -1546,13 +1547,20 @@ pkg_jobs_solve(struct pkg_jobs *j)
					waitpid(pchild, &pstatus, WNOHANG);

				}

				else {
- 
					if (!pkg_solve_sat_problem(problem)) {
+ 
					ret = pkg_solve_sat_problem(problem);
+ 
					if (ret == EPKG_FATAL) {

						pkg_emit_error("cannot solve job using SAT solver");

						ret = EPKG_FATAL;
+ 
						pkg_solve_problem_free(problem);

						j->solved = 0;

					}
+ 
					else if (ret == EPKG_AGAIN) {
+ 
						pkg_solve_problem_free(problem);
+ 
						goto again;
+ 
					}

					else {

						ret = pkg_solve_sat_to_jobs(problem);
+ 
						pkg_solve_problem_free(problem);

					}

				}

			}
@@ -1569,6 +1577,9 @@ pkg_jobs_solve(struct pkg_jobs *j)


	pkgdb_end_solver(j->db);
+ 
	if (ret != EPKG_OK)
+ 
		return (ret);
+ 


	pkg_jobs_apply_replacements(j);



	/* Check if we need to fetch and re-run the solver */
modified libpkg/pkg_solve.c
@@ -631,7 +631,7 @@ err:
	return (NULL);

}
- 
bool
+ 
int

pkg_solve_sat_problem(struct pkg_solve_problem *problem)

{

	struct pkg_solve_rule *rule;
@@ -670,19 +670,43 @@ pkg_solve_sat_problem(struct pkg_solve_problem *problem)
		const int *failed = picosat_failed_assumptions(problem->sat);

		struct sbuf *sb = sbuf_new_auto();
- 
		sbuf_printf(sb, "Cannot solve problem using SAT solver:\n");
+ 
		pkg_emit_error("Cannot solve problem using SAT solver:");



		do {

			struct pkg_solve_variable *var = &problem->variables[*failed - 1];
- 
			sbuf_printf(sb, "cannot %s package %s\n",
+
+ 
			sbuf_printf(sb, "cannot %s package %s, remove it from request [Y/n]: ",

				var->to_install ? "install" : "remove", var->uid);
+ 
			sbuf_finish(sb);
+
+ 
			if (pkg_emit_query_yesno(true, sbuf_data(sb))) {
+ 
				struct pkg_job_request *req;
+ 
				/* Remove this assumption and the corresponding request */
+ 
				if (var->to_install)
+ 
					HASH_FIND_PTR(problem->j->request_add, &var->unit, req);
+ 
				else
+ 
					HASH_FIND_PTR(problem->j->request_delete, &var->unit, req);
+ 
				if (req == NULL) {
+ 
					pkg_emit_error("cannot find %s in the request", var->uid);
+ 
					return (EPKG_FATAL);
+ 
				}
+
+ 
				if (var->to_install)
+ 
					HASH_DEL(problem->j->request_add, req);
+ 
				else
+ 
					HASH_DEL(problem->j->request_delete, req);
+ 
				sbuf_reset(sb);
+ 
			}
+ 
			else {
+ 
				sbuf_free(sb);
+ 
				return (EPKG_FATAL);
+ 
			}
+ 


		} while (*++failed);
- 
		sbuf_finish(sb);
- 
		pkg_emit_error(sbuf_data(sb));

		sbuf_free(sb);
- 
		return (false);
+ 
		return (EPKG_AGAIN);

	}



	/* Assign vars */
@@ -702,7 +726,7 @@ pkg_solve_sat_problem(struct pkg_solve_problem *problem)
			var->to_install ? "install" : "delete");

	}
- 
	return (true);
+ 
	return (EPKG_OK);

}



struct pkg_solve_ordered_variable {