#if 0

/**

 * Updates rules related to a single variable

 * @param var

 */

static void

pkg_solve_update_var_resolved (struct pkg_solve_variable *var)

{

	struct _pkg_solve_var_rule *rul;

	LL_FOREACH(var->rules, rul) {

		rul->rule->nresolved ++;

	}

}

static void

pkg_solve_undo_var_resolved (struct pkg_solve_variable *var)

{

	struct _pkg_solve_var_rule *rul;

	LL_FOREACH(var->rules, rul) {

		rul->rule->nresolved --;

	}

}

/**

 * Add variable to the implication graph

 * @param graph

 * @param var

 */

static void

pkg_solve_add_implication_graph(struct pkg_solve_impl_graph **graph,

	struct pkg_solve_variable *var)

{

	struct pkg_solve_impl_graph *it;

	it = malloc(sizeof(*it));

	if (it == NULL) {

		pkg_emit_errno("pkg_solve_add_implication_graph", "pkg_solve_impl_graph");

		return;

	}

	it->var = var;

	DL_APPEND(*graph, it);

}

/**

 * Propagate all units, must be called recursively

 * @param rules

 * @return true if there are units propagated

 */

static bool

pkg_solve_propagate_units(struct pkg_solve_problem *problem,

	struct pkg_solve_impl_graph **graph, bool top_level)

{

	struct pkg_solve_item *it, *unresolved = NULL;

	int solved_vars;

	struct _pkg_solve_var_rule *rul;

	struct pkg_solve_variable *var;

	bool ret;

	size_t i;

	do {

		solved_vars = 0;

		var = NULL;

		for (i = 0; i < problem->nvars; i ++) {

			var = &problem->variables[i];

check_again:

			/* Check for direct conflicts */

			LL_FOREACH(var->rules, rul) {

				unresolved = rul->rule;

				if (unresolved->nresolved == unresolved->nitems) {

					/* Check for direct conflict */

					ret = false;

					LL_FOREACH(unresolved, it) {

						if (it->var->resolved) {

							if (PKG_SOLVE_CHECK_ITEM(it)) {

								ret = true;

								break;

							}

						}

					}

					if (!ret) {

						if (top_level) {

							/*

							 * If it is top level propagation, then report that

							 * we have a conflicting clause there

							 */

							struct sbuf *err_msg = sbuf_new_auto();

							const char *pkg_name;

							int pkg_type;

							sbuf_printf(err_msg, "cannot resolve conflict between ");

							LL_FOREACH(unresolved, it) {

								pkg_get(it->var->unit->pkg, PKG_NAME, &pkg_name);

								pkg_type = it->var->unit->pkg->type;

								if (pkg_type == PKG_INSTALLED)

									sbuf_printf(err_msg, "local %s(want %s), ",

										pkg_name,

										it->var->to_install ? "keep" : "remove");

								else

									sbuf_printf(err_msg, "remote %s(want %s), ",

										pkg_name,

										it->var->to_install ? "install" : "ignore");

							}

							sbuf_finish(err_msg);

							pkg_emit_error("%splease resolve it manually", sbuf_data(err_msg));

							pkg_debug_print_rule(unresolved);

							sbuf_delete(err_msg);

						}

						return (false);

					}

					//pkg_debug(4, "resolved");

					//pkg_debug_print_rule(unresolved);

				}

			}

			LL_FOREACH(var->rules, rul) {

				unresolved = rul->rule;

				if (unresolved->nresolved == unresolved->nitems - 1) {

					//pkg_debug(4, "unit");

					//pkg_debug_print_rule(unresolved);

					/* Check for unit */

					ret = false;

					LL_FOREACH(unresolved, it) {

						if (it->var->resolved) {

							if (PKG_SOLVE_CHECK_ITEM(it)) {

								ret = true;

								break;

							}

						}

					}

					if (!ret) {

						/* This is a unit */

						int resolved = 0;

						LL_FOREACH(unresolved, it) {

							if (!it->var->resolved) {

								it->var->to_install = (!it->inverse);

								it->var->resolved = true;

								pkg_solve_update_var_resolved(it->var);

								pkg_debug(2, "propagate %s-%s(%d) to %s",

										it->var->uid, it->var->digest,

										it->var->priority,

										it->var->to_install ? "install" : "delete");

								pkg_debug_print_rule(unresolved);

								resolved ++;

								break;

							}

						}

						if (resolved == 0) {

							pkg_debug(4, "unit propagation conflict");

							pkg_debug_print_rule(unresolved);

							return (false);

						}

						solved_vars ++;

						/* We want to try propagating all clauses for a single variable */

						if (graph != NULL)

							pkg_solve_add_implication_graph(graph, it->var);

						goto check_again;

					}

				}

			}

		}

	} while (solved_vars > 0);

	return (true);

}

/**

 * Propagate pure clauses

 */

static bool

pkg_solve_propagate_pure(struct pkg_solve_problem *problem)

{

	struct pkg_solve_variable *var;

	struct _pkg_solve_var_rule *rul;

	struct pkg_solve_item *it;

	size_t i;

	var = NULL;

	for (i = 0; i < problem->nvars; i ++) {

		var = &problem->variables[i];

		if (var->nrules == 0) {

			/* This variable is independent and should not change its state */

			assert (var->rules == NULL);

			var->to_install = (var->unit->pkg->type == PKG_INSTALLED);

			var->resolved = true;

			pkg_debug(2, "leave %s %s-%s(%d) to %s",

					var->unit->pkg->type == PKG_INSTALLED ? "local" : "remote",

					var->uid, var->digest,

					var->priority, var->to_install ? "install" : "delete");

		}

		else {

			LL_FOREACH(var->rules, rul) {

				it = rul->rule;

				if (it->nitems == 1 && it->nresolved == 0) {

					it->var->to_install = (!it->inverse);

					it->var->resolved = true;

					pkg_debug(2, "requested %s-%s(%d) to %s",

							it->var->uid, it->var->digest,

							it->var->priority, it->var->to_install ? "install" : "delete");

					pkg_solve_update_var_resolved(it->var);

				}

			}

		}

	}

	return (true);

}

/*

 * For all variables in implication graph we reset their resolved values

 * Also we remove all variables propagated by this guess

 */

static void

pkg_solve_undo_guess(struct pkg_solve_impl_graph *graph)

{

	struct pkg_solve_impl_graph *cur, *tmp;

	DL_FOREACH_SAFE(graph, cur, tmp) {

		cur->var->resolved = false;

		pkg_solve_undo_var_resolved(cur->var);

		if (cur != graph)

			free(cur);

	}

	graph->next = NULL;

	graph->prev = graph;

}

/**

 * Try to solve sat problem

 * @param rules incoming rules to solve

 * @param nrules number of rules

 * @param nvars number of variables

 * @return

 */

bool

pkg_solve_sat_problem(struct pkg_solve_problem *problem)

{

	size_t i;

	struct pkg_solve_variable *var, *tvar;

	int64_t unresolved = 0, iters = 0;

	bool rc, backtrack = false, free_var;

	struct _solver_tree_elt {

		struct pkg_solve_variable *var;

		int guess;

		int inverses;

		struct pkg_solve_impl_graph *graph;

		struct _solver_tree_elt *prev, *next;

	} *solver_tree = NULL, *elt, *tmp;

	/* Obvious case */

	if (problem->rules_count == 0)

		return (true);

	/* Initially propagate explicit rules */

	pkg_solve_propagate_pure(problem);

	if (!pkg_solve_propagate_units(problem, NULL, true)) {

		pkg_emit_error("SAT: conflicting request, cannot solve");

		return (false);

	}

	/* Set initial guess */

	elt = solver_tree;

	/* DPLL Algorithm */

	var = NULL;

	for (i = 0; i < problem->nvars; i ++) {

		var = &problem->variables[i];

		if (!var->resolved) {

			if (backtrack) {

				/* Shift var back */

				var = tvar;

				backtrack = false;

				i --;

			}

			if (elt == NULL) {

				/* Add new element to the backtracking queue */

				elt = malloc(sizeof (*elt));

				if (elt == NULL) {

					pkg_emit_errno("malloc", "_solver_tree_elt");

					LL_FREE(solver_tree, free);

					return (false);

				}

				elt->inverses = 0;

				elt->var = var;

				elt->guess = -1;

				elt->graph = NULL;

				DL_APPEND(solver_tree, elt);

			}

			assert (var == elt->var);

			if (elt->guess == -1) {

				var->to_install = pkg_solve_initial_guess(problem, var);

				var->resolved = true;

			}

			else {

				/* For analyzed variables we can only inverse previous guess */

				var->to_install = !elt->guess;

				var->resolved = true;

				elt->inverses ++;

			}

			unresolved ++;

			free_var = elt->guess == -1;

			pkg_debug(3, "setting guess for %s variable %s(%s): %d(%d)",

				free_var ? "free" : "inversed", var->uid,

				var->unit->pkg->type == PKG_INSTALLED ? "l" : "r",

				var->to_install, elt->guess);

			/* Propagate units */

			pkg_solve_add_implication_graph(&elt->graph, var);

			rc = pkg_solve_propagate_units(problem, &elt->graph, false);

			if (!rc) {

				pkg_solve_undo_guess(elt->graph);

				if (free_var) {

					/* This is free variable, so we can assign true or false to it */

					var->to_install = !var->to_install;

					rc = pkg_solve_propagate_units(problem, &elt->graph, false);

				}

				else {

					rc = false;

				}

				if (!rc) {

					/* Need to backtrack */

					iters ++;

					if (elt->prev->next == NULL) {

						/* Cannot backtrack, UNSAT */

						pkg_debug(1, "problem is UNSAT problem after %d guesses", iters);

						LL_FREE(solver_tree, free);

						return (false);

					}

					pkg_debug(3, "backtrack from %s to %s", var->uid,

						elt->prev->var->uid);

					/* Set the current variable as free variable */

					elt->inverses = 0;

					free(elt->graph);

					elt->graph = NULL;

					elt->guess = -1;

					/* Go to the previous level */

					elt = elt->prev;

					tvar = elt->var;

					backtrack = true;

					continue;

				}

			}

			if (rc)

				pkg_solve_update_var_resolved(var);

			/* Assign the current guess */

			elt->guess = var->to_install;

			/* Move to the next elt */

			elt = elt->next;

		}

	}

	pkg_debug(1, "solved SAT problem in %d guesses", iters);

	DL_FOREACH_SAFE(solver_tree, elt, tmp) {

		LL_FREE(elt->graph, free);

		free(elt);

	}

	return (true);

}

#endif

static void

pkg_debug_print_rule (struct pkg_solve_item *rule)

{

	struct pkg_solve_item *it;

	struct sbuf *sb;

	int64_t expectlevel;

	/* Avoid expensive printing if debug level is less than required */

	expectlevel = pkg_object_int(pkg_config_get("DEBUG_LEVEL"));

	if (expectlevel < 2)

		return;

	sb = sbuf_new_auto();

	sbuf_printf(sb, "%s", "rule: (");

	LL_FOREACH(rule, it) {

			sbuf_printf(sb, "%s%s%s%s", it->inverse < 0 ? "!" : "",

					it->var->uid,

					(it->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)",

					it->next ? " | " : ")");

	}

	sbuf_finish(sb);

	pkg_debug(2, "%s", sbuf_data(sb));

	sbuf_delete(sb);

}

/*

 * Set initial guess based on a variable passed

 */

static int

pkg_solve_initial_guess(struct pkg_solve_problem *problem,

		struct pkg_solve_variable *var)

{

	struct pkg_solve_variable *cur, *start, *local = NULL;

	unsigned vercnt = 0;

	bool force;

	force = problem->j->flags & PKG_FLAG_FORCE;

	/* Find start variable in the chain */

	start = var;

	while(start->prev->next != NULL)

		start = start->prev;

	LL_FOREACH(start, cur) {

		if (cur->unit->pkg->type == PKG_INSTALLED)

			local = cur;

		vercnt ++;

	}

	if (vercnt > 2 && local != NULL) {

		/* We need to find the largest version possible */

		struct pkg_solve_variable *selected = NULL;

		bool chosen = false;

		LL_FOREACH(start, cur) {

			if (selected != NULL && pkg_version_change_between(cur->unit->pkg,

				selected->unit->pkg) == PKG_UPGRADE) {

				selected = cur;

				chosen = true;

			}

			else if (selected == NULL) {

				selected = cur;

			}

		}

		/* If not chosen then pin repository */

		if (!chosen) {

			const ucl_object_t *an, *obj;

			pkg_get(local->unit->pkg, PKG_ANNOTATIONS, &obj);

			an = pkg_object_find(obj, "repository");

			if (an != NULL) {

				LL_FOREACH(start, cur) {

					const char *reponame;

					pkg_get(cur->unit->pkg, PKG_REPONAME, &reponame);

					if (reponame && strcmp(reponame, ucl_object_tostring(an)) == 0) {

						selected = cur;

						break;

					}

				}

			}

		}

		return (var == selected) ? 1 : -1;

	}

	else if (problem->j->type == PKG_JOBS_UPGRADE) {

		if (var->unit->pkg->type == PKG_INSTALLED) {

			/* For local packages assume true if we have no upgrade */

			if (var->unit->next == NULL && var->unit->prev == var->unit)

				return (1);

		}

		else {

			/* For remote packages we return true if they are upgrades for local ones */

			if (var->unit->next != NULL || var->unit->prev != var->unit)

				return (1);

		}

	}

	else {

		/* For all non-upgrade jobs be more conservative */

		if (var->unit->pkg->type == PKG_INSTALLED)

			return (1);

	}

	/* Otherwise set initial guess to false */

	return (-1);

}