Hi Daniel,
First of all: Sorry for the delay in getting back to you and thank you
so much for looking at my code and the detailed bug report! You are
definitely right: there is a bug.
You've pointed out that if A and B are tristates, then "B depends on
A" has the following "truth table":
+---+---+-------------------+
| A | B | B -> A satisfied? |
+---+---+-------------------+
| n | n | 1 |
| y | n | 1 |
| m | n | 1 |
+---+---+-------------------+
| n | y | 0 |
| y | y | 1 |
| m | y | 0 |
+---+---+-------------------+
| n | m | 0 |
| y | m | 1 |
| m | m | 1 |
+---+---+-------------------+
In particular, in the current implementation, (A=m, B=y) appears to
satisfy "B depends on A", which it shouldn't according to the table.
In my code, the "depends on" constraints are encoded by
build_prompt_visibility_clauses() and expr_to_bool_expr():
static bool build_prompt_visibility_clauses(struct property *prop)
{
struct bool_expr *e[2];
...
/* visible.expr is a conjunction of the menu's dependencies
* (parent menus' "depends on", this menu' "depends on", and the
* "if" part of the prompt). Which is exactly what we need.
*
* For choices, it is a conjunction of the choice block symbol
* and the choice's "depends on". */
if (prop->visible.expr) {
expr_to_bool_expr(prop->sym, prop->visible.expr, e);
} else {
e[0] = bool_const(true);
e[1] = bool_const(false);
}
/* Prompts are visible if and only if
* - the menu is visible ("depends on", etc.)
* - the prompt's dependencies are satisfied (the "if" part) */
assert(prop->sat_variable <= nr_sat_variables);
t1 = bool_eq_put(bool_var(prop->sat_variable), e[0]);
bool_put(e[1]);
...
}
In our example, 'prop' is the prompt for B and 'prop->visible.expr' is
the expression "A".
The function encodes: (B is y or m) iff (A is y or m). Which is a
weaker statement that what we really wanted. Let's set up a Karnaugh
map for the table above:
\zw|
xy\ | 00 01 11 10
----+------------
00 | 1 - 0 0
01 | - - - -
11 | 1 - 1 0
10 | 1 - 1 1
(with x=A_y, y=A_m, z=B_y, w=B_m in the format of kconfig-sat.txt)
So this would make... (¬B_y) ∨ (A_y ∧ B_m) ∨ (A_y ∧ ¬A_m)
Quick verification with a Python script:
n = ('n', 0, 0)
y = ('y', 1, 0)
m = ('m', 1, 1)
for B_kc, B_y, B_m in (n, y, m):
for A_kc, A_y, A_m in (n, y, m):
sat = (not B_y) or (A_y and B_m) or (A_y and not A_m)
print A_kc, B_kc, int(sat)
print '-----'
$ python truthtable.py
n n 1
y n 1
m n 1
-----
n y 0
y y 1
m y 0
-----
n m 0
y m 1
m m 1
This prints the same table as we had above, so that means the (new)
encoding/expressions should be correct.
I haven't checked if this actually gives the same result as
transforming (B depends on A) into (!B or A) in tristate logic and
then encoding that with propositional logic, but I suspect that it
does. That would be a little bit simpler, I guess.
Actually fixing satconf.c is not very straightforward: I've assumed
that "prompt visibility" only needs 1 variable and is sufficient to
encode dependencies, but it seems like what we really want to encode
is for each prompt, what is the maximal value that it allows the
symbol to have (which would need 2 variables per prompt). Then, when
actually determining the value of a symbol, it would have to take a
max() over all its prompts (so that if one prompt is y and another
prompt is m -- for the same symbol -- then the result would be the
maximum over all the prompts' values).
If what I said so far is not very clear, consider this modified example:
config MODULES
bool "Enable loadable module support"
option modules
config A
tristate "A prompt"
config B
tristate "B prompt"
config C
tristate "C prompt 1"
depends on A
config C
tristate "C prompt 2"
depends on B
Here, you can set A=y and B=m and C can be either y or m. So the
dependency doesn't restrict the value of C directly, just the value of
the prompt (which is then used together with all the other prompts for
the same symbol to determine the final value of C).
I'll give fixing satconf.c a shot -- if my head doesn't explode ;-)
Again, thanks for the report!
Vegard