Translation of RSF-Files into DIMACS Format

This section specifies the translation of RSF files into DIMACS files.

Translation of Tristate Variables

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 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 exactly one variable will be selected:

• In Boolean formula:

  VARIABLE=n XOR VARIABLE=value1 XOR ... XOR VARIABLE=valueN
  

• In DIMACS:

  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)
  ...
  VARIABLE=n OR VARIABLE=value1 OR ... OR VARIABLE=valueN
  

All combinations of 2 negated variables + 1 constraint were all variables are used in a positive combination.

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.

Translation of Choices

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

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)
  

Translation of depends Constraints

Each variable can have multiple depends statements, specifying when the variable can be configured. The variable must remain unconfigured (in case of a Boolean or Tristate variable, it must be set to n), if none of the depends statements is fulfilled. Conditions will be translated as follows:

1. One Condition:
   • In RSF:

     depends Variable Condition
     

   • In Boolean formula:

     Not(Condition) implies Not(Variable)
     

   • In DIMACS:

     Condition or Not(Variable)
     

2. Multiple Conditions
   • In RSF:

     depends Variable Condition1
     depends Variable Condition2
     

   • In Boolean formula:

     Not(Condition1) and Not(Condition2) implies Not(Variable)
     

   • In DIMACS:

     Condition1 or Condition2 or Not(Variable)
     

3. Variable depends of Tristate
   • In RSF:

     depends VARIABLE TRISTATE_VAR
     

   • In Boolean formula:

     Not(TRISTATE_VAR) and Not(TRISTATE_VAR_MODULE) implies Not(VARIABLE)
     

   • In DIMACS:

     TRISTATE_VAR or TRISTATE_VAR_MODULE or Not(VARIABLE)
     

4. Tristate variable depends of Condition
   • In RSF:

     depends TRISTATE_VAR CONDITION
     

   • In Boolean formula:

     Not(CONDITION) implies Not(TRISTATE_VAR)
     Not(CONDITION) implies Not(TRISTATE_VAR_MODULE)
     

   • In DIMACS:

     CONDITION or Not(TRISTATE_VAR)
     CONDITION or Not(TRISTATE_VAR_MODULE_VAR)
     

Translation of ItemSelects Constraints

The ​KConfig specification defines select statements as follows:

reverse dependencies: "select" <symbol> ["if" <expr>]

While normal dependencies reduce the upper limit of a symbol (see below), reverse dependencies can be used to force a lower limit of another symbol. The value of the current menu symbol is used as the minimal value <symbol> can be set to. If <symbol> is selected multiple times, the limit is set to the largest selection. Reverse dependencies can only be used with boolean or tristate symbols.

1. Translation of Boolean ItemSelect statements:
   • In RSF:

     ItemSelects BOOLEAN_VAR OTHER_VAR CONDITION
     

   • In Boolean formula:

     (BOOLEAN_VAR and CONDITION) implies OTHER_VAR
     

   • In DIMACS:

     Not(BOOLEAN_VAR) or Not(CONDITION) or OTHER_VAR
     

2. Translation of Tristate ItemSelect statements:
   • In RSF:

     ItemSelects TRISTATE_VAR OTHER_VAR CONDITION
     

   • In Boolean formula:

     (TRISTATE_VAR and CONDITION) implies OTHER_VAR
     (TRISTATE_VAR_MODULE and CONDITION) implies OTHER_VAR_MODULE
     

   • In DIMACS:

     Not(TRISTATE_VAR) or Not(CONDITION) or OTHER_VAR
     Not(TRISTATE_VAR_MODULE) or Not(CONDITION) or OTHER_VAR_MODULE