Translation of RSF-Files into DIMACS Format
This section specifies the translation of RSF files into DIMACS files.
Table of Contents
Translation of Boolean and Tristate Variables
When evaluating KConfig each variable is assigned a value; possible values are:
- 0: The variable is not selected (constant symbol: 'n')
- 1: The variable is selected as a module (constant symbol: 'm')
- 2: The variable is permanently selected (constant symbol: 'y')
Boolean variables can only have the values 0 or 2. They are translated as a single boolean variable with their name.
- In RSF:
Item VARIABLE boolean
- Meaning:
| VARIABLE | Explanation |
| 0 | VARIABLE is permanently deselected ('n' was selected) |
| 1 | VARIABLE is permanently selected ('y' was selected) |
Tristate variables will be translated into 2 variables. This translation shall be equal to the translation of Undertaker or KConfigReader:
- One variable declaring whether the related KConfig variable is permanently selected
- One variable declaring whether the related KConfig variable is selected as a module.
- Only one of these variables can be selected at the same time.
The translation will be done as follows:
- In RSF:
Item VARIABLE tristate
- In DIMACS:
Not(VARIABLE) or Not(VARIABLE_MODULE)
- Meaning:
| VARIABLE | VARIABLE_MODULE | Explanation |
| 0 | 0 | VARIABLE is permanently deselected ('n' was selected) |
| 1 | 0 | VARIABLE is permanently selected ('y' was selected) |
| 0 | 1 | VARIABLE is selected as a module ('m' was selected) |
| 1 | 1 | Illegal state |
Translation of Depends Constraints
A depends statement specifies the maximum possible selection for a variable. The constraint is evaluated in "integer logic", with "or" being "max", "and" being "min" and "not" being "2-".
- In RSF:
depends Variable Condition
Variable is Boolean
- In Boolean formula:
Not(Condition) implies Not(Variable)
- In DIMACS:
Condition or Not(Variable)
If Condition contains tristate variables, then the version that decides whether they are permanently selected is used. This is because if the tristate is selected as a module, the value would be 1. Since depends specifies the maximum possible value for the variable, for boolean variables the only possible solution would be 0.
If Condition contains variables that are neither boolean nor tristate (i.e. integer, hex, string or unknown) they are treated as false (i.e. 'n').
Variable is Tristate
- In Boolean formula:
Not(Condition) implies Not(Variable) Not(Condition) implies Not(Variable_MODULE)
- In DIMACS:
Condition or Not(Variable) Condition or Not(Variable_MODULE)
If Condition contains tristate variables, then the version that decides whether they are permanently selected is used when parsing the Condition for the first constraint. This is because the Condition must evaluate to 2 in "integer logic", when Variable is selected as 2. When parsing the Condition for the second constraint, (VAR or VAR_MODULE) is used for module variables. This is because the Condition must evaluate to 2 or 1, when Variable is selected as 1(since depends specifies the maximum possible selection).
If Conditions contains 'm' (i.e. the constant symbol for "1"), it is treated as false for the first constraint and as true for the second constraint. Moreover, since the negation is handled as "2-" in "integer logic", NOT('m') equals 'm' (2-1 = 1).
If Condition contains variables that are neither boolean nor tristate (i.e. integer, hex, string or unknown) they are treated as false (i.e. 'n').
Translation of ItemSelects Constraints
The ItemSelects statement specifies the minimum possible selection for a variable, if the specified condition is true. The constraint is evaluated in "integer logic", with "or" being "max", "and" being "min" and "not" being "2-".
- In RSF:
ItemSelects Variable OtherVariable Condition
Variable is Boolean
- In Boolean formula:
(Variable and Condition) implies OtherVariable
- In DIMACS:
Not(Variable) or Not(Condition) or OtherVariable
If the Condition is true and Variable is true (i.e. 'y'), then OtherVariable must be true (i.e. 'y'). If OtherVariable is a tristate, 'y' means "permanently selected".
Variable is Tristate
- In Boolean formula:
(Variable and Condition) implies OtherVariable (Variable_MODULE and Condition) implies (OtherVariable or OtherVariable_MODULE)
- In DIMACS:
Not(Variable) or Not(Condition) or OtherVariable Not(Variable_MODULE) or Not(Condition) or (OtherVariable or OtherVariable_MODULE)
If the Condition is true and Variable is true (i.e. 'y'), then OtherVariable must be true (i.e. 'y').
If the Condition is true and Variable is selected as module (i.e. 'm'), then OtherVariable must be selected as module ('m') or permanently selected ('y'). Thus, if OtherVariable boolean, it can only be permanently selected; the " or OtherVariable_MODULE" part is omitted in this case.
Translation of Choices
TODO: review A choice can be treated as an Enumeration. The KConfig specification defines a choice as follows:
choices:
"choice" [symbol]
<choice options>
<choice block>
"endchoice"
This defines a choice group and accepts any of the above attributes as options. A choice can only be of type bool or tristate, while a boolean choice only allows a single config entry to be selected, a tristate choice also allows any number of config entries to be set to 'm'. This can be used if multiple drivers for a single hardware exists and only a single driver can be compiled/loaded into the kernel, but all drivers can be compiled as modules.
A choice accepts another option "optional", which allows to set the choice to 'n' and no entry needs to be selected. If no [symbol] is associated with a choice, then you can not have multiple definitions of that choice. If a [symbol] is associated to the choice, then you may define the same choice (ie. with the same entries) in another place.
Translation of Boolean Choices
If a boolean choice is selected, exactly one of the related ChoiceItems has to be selected. For each ChoiceItems the individual conditions has to be considered. A Choice with n ChoiceItems Item1 - ItemN must be translated as follows (conditions are not considered here):
- In RSF:
Choice CHOICE ChoiceItem Item1 CHOICE ... ChoiceItem ItemN CHOICE
- In Boolean formula:
CHOICE implies (Item1 or Item2 or ... or ItemN) Not(CHOICE) implies Not(Item1) Not(CHOICE) implies Not(Item2) ... Not(CHOICE) implies Not(ItemN) Item1 xor Item2 Item1 xor Item3 ... Item1 xor ItemN Item2 xor Item3 ... ItemN-1 xor ItemN
- In DIMACS:
Not(CHOICE) or Item1 or Item2 or ... or ItemN CHOICE or Not(Item1) CHOICE or Not(Item2) ... CHOICE or Not(ItemN) Not(Item1) or Not(Item2) Not(Item1) or Not(Item3) ... Not(Item1) or Not(ItemN) Not(Item2) or Not(Item3) ... Not(ItemN-1) or Not(ItemN)
Further, a Choice can be empty if none of the depends constraints of the individual ChoiceItems is fulfilled. In KConfig this situation is ok. A new "depends" condition must be created to avoid the creation an unsatisfiable model:
depends CHOICE (dependsOf(CHOICE) && (dependsOf(Item1) || dependsOf(Item2) ... dependsOf(ItemN))
dependsOf(CHOICE) can be omitted, if CHOICE has no depends.
Translation of Tristate Choices
TODO: review A Tristate Choice can be selected as permanently selected ('y') or as a module ('m').
- If the Choice is permanently selected ('y'), exactly one of its ChoiceItems must also be permanently selected ('y').
- If the Choice is selected as a module ('m'), an arbitrary number (0 - n) of ChoiceItems can also be selected as modules ('m'). The permanently selection of ChoiceItems ('y') is not allowed.
The translation of Tristate Choices includes the translation of Boolean Choices (for the 'y' part). Additional constraints are needed to model the constraints for the modules:
- In RSF:
Choice CHOICE ChoiceItem Item1 CHOICE ... ChoiceItem ItemN CHOICE
- In Boolean formula (only the module part):
Not(CHOICE_MODULE) implies Not(Item1_MODULE) Not(CHOICE_MODULE) implies Not(Item2_MODULE) ... Not(CHOICE_MODULE) implies Not(ItemN_MODULE) CHOICE implies Not(Item1_MODULE) CHOICE implies Not(Item2_MODULE) ... CHOICE implies Not(ItemN_MODULE) CHOICE_MODULE implies Not(Item1) CHOICE_MODULE implies Not(Item2) ... CHOICE_MODULE implies Not(ItemN)
- In RSF (only the module part):
CHOICE_MODULE or Not(Item1_MODULE) CHOICE_MODULE or Not(Item2_MODULE) ... CHOICE_MODULE or Not(ItemN_MODULE) Not(CHOICE) or Not(Item1_MODULE) Not(CHOICE) or Not(Item2_MODULE) ... Not(CHOICE) or Not(ItemN_MODULE) Not(CHOICE_MODULE) or Not(Item1) Not(CHOICE_MODULE) or Not(Item2) ... Not(CHOICE_MODULE) or Not(ItemN)
Defaults and prompts
Each variable can have multiple default values. The user may overwrite this value, if the variable is visible. Thus, default values must be used as constraints for variables which are not visible.
- Translation of defaults with prompts
No constraint must be crated, if a variable has a default value and a (permanent visible) prompt.
- Translation of defaults with no prompts
For variables with a default but no prompt, a constraint must be created.
- In RSF:
Default VARIABLE VALUE CONDITION1 Prompt VARIABLE CONDITION2
- In Boolean formula:
(Not(CONDITION2) and CONDITION1) implies VARIABLE=VALUE
- In DIMACS:
CONDITION2 or Not(CONDITION1) or VARIABLE=VALUE
Translation of String, Integer, Hex Variables
Concrete Values
For String, Integer, and Hex variables we list all used values as different variables in the following form:
VARIABLE=<value>
For a not configured variable (or an empty String) a variable in the following form will be created:
VARIABLE=n
Further, constraints must ensure that at most one variable will be selected:
- In DIMACS/Boolean formula:
Not(VARIABLE=n) OR Not(VARIABLE=value1) Not(VARIABLE=n) OR Not(VARIABLE=value2) ... Not(VARIABLE=n) OR Not(VARIABLE=valueN) Not(VARIABLE=value1) OR Not(VARIABLE=value2) ... Not(VARIABLE=value1) OR Not(VARIABLE=valueN)
All combinations of 2 negated variables.
Ranges
Ranges of Integers/Hex variables will not be considered. Since KConfig supports only == and != comparisons, only values used in constraints will be translated to DIMACS.
Unused Variables
If a variable is not used, this variable must be deselected (selection 'n'). A variable is not used if there exist a condition where the variable is not visible, has no prompt, and will not be selected by another variable.
This creation of additional parameters should be optional.