Changes between Version 10 and Version 11 of Specification/RSF2DIMACS


Ignore:
Timestamp:
Sep 25, 2014, 8:05:12 AM (10 years ago)
Author:
elshar
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Specification/RSF2DIMACS

    v10 v11  
    2424 
    2525== Translation of String, Integer, Hex Variables == 
     26=== Concrete Values === 
     27For String, Integer, and Hex variables we list all used values as different variables in the following form: 
     28{{{ 
     29VARIABLE=<value> 
     30}}} 
     31For a not configured variable (or an empty String) a variable in the following form will be created: 
     32{{{ 
     33VARIABLE=n 
     34}}} 
     35Further, constraints must ensure that exactly one variable will be selected: 
     36* In Boolean formula: 
     37{{{ 
     38VARIABLE=n XOR VARIABLE=value1 XOR ... XOR VARIABLE=valueN 
     39}}} 
     40* In DIMACS: 
     41{{{ 
     42Not(VARIABLE=n) OR Not(VARIABLE=value1) 
     43Not(VARIABLE=n) OR (VARIABLE=value2) 
     44... 
     45Not(VARIABLE=n) OR (VARIABLE=valueN) 
     46Not(VARIABLE=value1) OR (VARIABLE=value2) 
     47... 
     48Not(VARIABLE=value1) OR (VARIABLE=valueN) 
     49... 
     50VARIABLE=n OR VARIABLE=value1 OR ... OR VARIABLE=valueN 
     51}}} 
     52All combinations of 2 negated variables + 1 constraint were all variables are used in a positive combination. 
    2653=== Ranges === 
    2754Ranges of !Integers/Hex variables will not be considered. Since KConfig supports only == and != comparisons, only values used in constraints will be translated to DIMACS.