Merge tag 'for_v5.3-rc1' of git://git.kernel.org/pub/scm/linux/kernel/git/jack/linux-fs
[sfrench/cifs-2.6.git] / Documentation / kbuild / kconfig-language.rst
1 ================
2 Kconfig Language
3 ================
4
5 Introduction
6 ------------
7
8 The configuration database is a collection of configuration options
9 organized in a tree structure::
10
11         +- Code maturity level options
12         |  +- Prompt for development and/or incomplete code/drivers
13         +- General setup
14         |  +- Networking support
15         |  +- System V IPC
16         |  +- BSD Process Accounting
17         |  +- Sysctl support
18         +- Loadable module support
19         |  +- Enable loadable module support
20         |     +- Set version information on all module symbols
21         |     +- Kernel module loader
22         +- ...
23
24 Every entry has its own dependencies. These dependencies are used
25 to determine the visibility of an entry. Any child entry is only
26 visible if its parent entry is also visible.
27
28 Menu entries
29 ------------
30
31 Most entries define a config option; all other entries help to organize
32 them. A single configuration option is defined like this::
33
34   config MODVERSIONS
35         bool "Set version information on all module symbols"
36         depends on MODULES
37         help
38           Usually, modules have to be recompiled whenever you switch to a new
39           kernel.  ...
40
41 Every line starts with a key word and can be followed by multiple
42 arguments.  "config" starts a new config entry. The following lines
43 define attributes for this config option. Attributes can be the type of
44 the config option, input prompt, dependencies, help text and default
45 values. A config option can be defined multiple times with the same
46 name, but every definition can have only a single input prompt and the
47 type must not conflict.
48
49 Menu attributes
50 ---------------
51
52 A menu entry can have a number of attributes. Not all of them are
53 applicable everywhere (see syntax).
54
55 - type definition: "bool"/"tristate"/"string"/"hex"/"int"
56   Every config option must have a type. There are only two basic types:
57   tristate and string; the other types are based on these two. The type
58   definition optionally accepts an input prompt, so these two examples
59   are equivalent::
60
61         bool "Networking support"
62
63   and::
64
65         bool
66         prompt "Networking support"
67
68 - input prompt: "prompt" <prompt> ["if" <expr>]
69   Every menu entry can have at most one prompt, which is used to display
70   to the user. Optionally dependencies only for this prompt can be added
71   with "if".
72
73 - default value: "default" <expr> ["if" <expr>]
74   A config option can have any number of default values. If multiple
75   default values are visible, only the first defined one is active.
76   Default values are not limited to the menu entry where they are
77   defined. This means the default can be defined somewhere else or be
78   overridden by an earlier definition.
79   The default value is only assigned to the config symbol if no other
80   value was set by the user (via the input prompt above). If an input
81   prompt is visible the default value is presented to the user and can
82   be overridden by him.
83   Optionally, dependencies only for this default value can be added with
84   "if".
85
86  The default value deliberately defaults to 'n' in order to avoid bloating the
87  build. With few exceptions, new config options should not change this. The
88  intent is for "make oldconfig" to add as little as possible to the config from
89  release to release.
90
91  Note:
92         Things that merit "default y/m" include:
93
94         a) A new Kconfig option for something that used to always be built
95            should be "default y".
96
97         b) A new gatekeeping Kconfig option that hides/shows other Kconfig
98            options (but does not generate any code of its own), should be
99            "default y" so people will see those other options.
100
101         c) Sub-driver behavior or similar options for a driver that is
102            "default n". This allows you to provide sane defaults.
103
104         d) Hardware or infrastructure that everybody expects, such as CONFIG_NET
105            or CONFIG_BLOCK. These are rare exceptions.
106
107 - type definition + default value::
108
109         "def_bool"/"def_tristate" <expr> ["if" <expr>]
110
111   This is a shorthand notation for a type definition plus a value.
112   Optionally dependencies for this default value can be added with "if".
113
114 - dependencies: "depends on" <expr>
115   This defines a dependency for this menu entry. If multiple
116   dependencies are defined, they are connected with '&&'. Dependencies
117   are applied to all other options within this menu entry (which also
118   accept an "if" expression), so these two examples are equivalent::
119
120         bool "foo" if BAR
121         default y if BAR
122
123   and::
124
125         depends on BAR
126         bool "foo"
127         default y
128
129 - reverse dependencies: "select" <symbol> ["if" <expr>]
130   While normal dependencies reduce the upper limit of a symbol (see
131   below), reverse dependencies can be used to force a lower limit of
132   another symbol. The value of the current menu symbol is used as the
133   minimal value <symbol> can be set to. If <symbol> is selected multiple
134   times, the limit is set to the largest selection.
135   Reverse dependencies can only be used with boolean or tristate
136   symbols.
137
138   Note:
139         select should be used with care. select will force
140         a symbol to a value without visiting the dependencies.
141         By abusing select you are able to select a symbol FOO even
142         if FOO depends on BAR that is not set.
143         In general use select only for non-visible symbols
144         (no prompts anywhere) and for symbols with no dependencies.
145         That will limit the usefulness but on the other hand avoid
146         the illegal configurations all over.
147
148 - weak reverse dependencies: "imply" <symbol> ["if" <expr>]
149   This is similar to "select" as it enforces a lower limit on another
150   symbol except that the "implied" symbol's value may still be set to n
151   from a direct dependency or with a visible prompt.
152
153   Given the following example::
154
155     config FOO
156         tristate
157         imply BAZ
158
159     config BAZ
160         tristate
161         depends on BAR
162
163   The following values are possible:
164
165         ===             ===             =============   ==============
166         FOO             BAR             BAZ's default   choice for BAZ
167         ===             ===             =============   ==============
168         n               y               n               N/m/y
169         m               y               m               M/y/n
170         y               y               y               Y/n
171         y               n               *               N
172         ===             ===             =============   ==============
173
174   This is useful e.g. with multiple drivers that want to indicate their
175   ability to hook into a secondary subsystem while allowing the user to
176   configure that subsystem out without also having to unset these drivers.
177
178 - limiting menu display: "visible if" <expr>
179   This attribute is only applicable to menu blocks, if the condition is
180   false, the menu block is not displayed to the user (the symbols
181   contained there can still be selected by other symbols, though). It is
182   similar to a conditional "prompt" attribute for individual menu
183   entries. Default value of "visible" is true.
184
185 - numerical ranges: "range" <symbol> <symbol> ["if" <expr>]
186   This allows to limit the range of possible input values for int
187   and hex symbols. The user can only input a value which is larger than
188   or equal to the first symbol and smaller than or equal to the second
189   symbol.
190
191 - help text: "help" or "---help---"
192   This defines a help text. The end of the help text is determined by
193   the indentation level, this means it ends at the first line which has
194   a smaller indentation than the first line of the help text.
195   "---help---" and "help" do not differ in behaviour, "---help---" is
196   used to help visually separate configuration logic from help within
197   the file as an aid to developers.
198
199 - misc options: "option" <symbol>[=<value>]
200   Various less common options can be defined via this option syntax,
201   which can modify the behaviour of the menu entry and its config
202   symbol. These options are currently possible:
203
204   - "defconfig_list"
205     This declares a list of default entries which can be used when
206     looking for the default configuration (which is used when the main
207     .config doesn't exists yet.)
208
209   - "modules"
210     This declares the symbol to be used as the MODULES symbol, which
211     enables the third modular state for all config symbols.
212     At most one symbol may have the "modules" option set.
213
214   - "allnoconfig_y"
215     This declares the symbol as one that should have the value y when
216     using "allnoconfig". Used for symbols that hide other symbols.
217
218 Menu dependencies
219 -----------------
220
221 Dependencies define the visibility of a menu entry and can also reduce
222 the input range of tristate symbols. The tristate logic used in the
223 expressions uses one more state than normal boolean logic to express the
224 module state. Dependency expressions have the following syntax::
225
226   <expr> ::= <symbol>                           (1)
227            <symbol> '=' <symbol>                (2)
228            <symbol> '!=' <symbol>               (3)
229            <symbol1> '<' <symbol2>              (4)
230            <symbol1> '>' <symbol2>              (4)
231            <symbol1> '<=' <symbol2>             (4)
232            <symbol1> '>=' <symbol2>             (4)
233            '(' <expr> ')'                       (5)
234            '!' <expr>                           (6)
235            <expr> '&&' <expr>                   (7)
236            <expr> '||' <expr>                   (8)
237
238 Expressions are listed in decreasing order of precedence.
239
240 (1) Convert the symbol into an expression. Boolean and tristate symbols
241     are simply converted into the respective expression values. All
242     other symbol types result in 'n'.
243 (2) If the values of both symbols are equal, it returns 'y',
244     otherwise 'n'.
245 (3) If the values of both symbols are equal, it returns 'n',
246     otherwise 'y'.
247 (4) If value of <symbol1> is respectively lower, greater, lower-or-equal,
248     or greater-or-equal than value of <symbol2>, it returns 'y',
249     otherwise 'n'.
250 (5) Returns the value of the expression. Used to override precedence.
251 (6) Returns the result of (2-/expr/).
252 (7) Returns the result of min(/expr/, /expr/).
253 (8) Returns the result of max(/expr/, /expr/).
254
255 An expression can have a value of 'n', 'm' or 'y' (or 0, 1, 2
256 respectively for calculations). A menu entry becomes visible when its
257 expression evaluates to 'm' or 'y'.
258
259 There are two types of symbols: constant and non-constant symbols.
260 Non-constant symbols are the most common ones and are defined with the
261 'config' statement. Non-constant symbols consist entirely of alphanumeric
262 characters or underscores.
263 Constant symbols are only part of expressions. Constant symbols are
264 always surrounded by single or double quotes. Within the quote, any
265 other character is allowed and the quotes can be escaped using '\'.
266
267 Menu structure
268 --------------
269
270 The position of a menu entry in the tree is determined in two ways. First
271 it can be specified explicitly::
272
273   menu "Network device support"
274         depends on NET
275
276   config NETDEVICES
277         ...
278
279   endmenu
280
281 All entries within the "menu" ... "endmenu" block become a submenu of
282 "Network device support". All subentries inherit the dependencies from
283 the menu entry, e.g. this means the dependency "NET" is added to the
284 dependency list of the config option NETDEVICES.
285
286 The other way to generate the menu structure is done by analyzing the
287 dependencies. If a menu entry somehow depends on the previous entry, it
288 can be made a submenu of it. First, the previous (parent) symbol must
289 be part of the dependency list and then one of these two conditions
290 must be true:
291
292 - the child entry must become invisible, if the parent is set to 'n'
293 - the child entry must only be visible, if the parent is visible::
294
295     config MODULES
296         bool "Enable loadable module support"
297
298     config MODVERSIONS
299         bool "Set version information on all module symbols"
300         depends on MODULES
301
302     comment "module support disabled"
303         depends on !MODULES
304
305 MODVERSIONS directly depends on MODULES, this means it's only visible if
306 MODULES is different from 'n'. The comment on the other hand is only
307 visible when MODULES is set to 'n'.
308
309
310 Kconfig syntax
311 --------------
312
313 The configuration file describes a series of menu entries, where every
314 line starts with a keyword (except help texts). The following keywords
315 end a menu entry:
316
317 - config
318 - menuconfig
319 - choice/endchoice
320 - comment
321 - menu/endmenu
322 - if/endif
323 - source
324
325 The first five also start the definition of a menu entry.
326
327 config::
328         "config" <symbol>
329         <config options>
330
331 This defines a config symbol <symbol> and accepts any of above
332 attributes as options.
333
334 menuconfig::
335         "menuconfig" <symbol>
336         <config options>
337
338 This is similar to the simple config entry above, but it also gives a
339 hint to front ends, that all suboptions should be displayed as a
340 separate list of options. To make sure all the suboptions will really
341 show up under the menuconfig entry and not outside of it, every item
342 from the <config options> list must depend on the menuconfig symbol.
343 In practice, this is achieved by using one of the next two constructs::
344
345   (1):
346   menuconfig M
347   if M
348       config C1
349       config C2
350   endif
351
352   (2):
353   menuconfig M
354   config C1
355       depends on M
356   config C2
357       depends on M
358
359 In the following examples (3) and (4), C1 and C2 still have the M
360 dependency, but will not appear under menuconfig M anymore, because
361 of C0, which doesn't depend on M::
362
363   (3):
364   menuconfig M
365       config C0
366   if M
367       config C1
368       config C2
369   endif
370
371   (4):
372   menuconfig M
373   config C0
374   config C1
375       depends on M
376   config C2
377       depends on M
378
379 choices::
380
381         "choice" [symbol]
382         <choice options>
383         <choice block>
384         "endchoice"
385
386 This defines a choice group and accepts any of the above attributes as
387 options. A choice can only be of type bool or tristate.  If no type is
388 specified for a choice, its type will be determined by the type of
389 the first choice element in the group or remain unknown if none of the
390 choice elements have a type specified, as well.
391
392 While a boolean choice only allows a single config entry to be
393 selected, a tristate choice also allows any number of config entries
394 to be set to 'm'. This can be used if multiple drivers for a single
395 hardware exists and only a single driver can be compiled/loaded into
396 the kernel, but all drivers can be compiled as modules.
397
398 A choice accepts another option "optional", which allows to set the
399 choice to 'n' and no entry needs to be selected.
400 If no [symbol] is associated with a choice, then you can not have multiple
401 definitions of that choice. If a [symbol] is associated to the choice,
402 then you may define the same choice (i.e. with the same entries) in another
403 place.
404
405 comment::
406
407         "comment" <prompt>
408         <comment options>
409
410 This defines a comment which is displayed to the user during the
411 configuration process and is also echoed to the output files. The only
412 possible options are dependencies.
413
414 menu::
415
416         "menu" <prompt>
417         <menu options>
418         <menu block>
419         "endmenu"
420
421 This defines a menu block, see "Menu structure" above for more
422 information. The only possible options are dependencies and "visible"
423 attributes.
424
425 if::
426
427         "if" <expr>
428         <if block>
429         "endif"
430
431 This defines an if block. The dependency expression <expr> is appended
432 to all enclosed menu entries.
433
434 source::
435
436         "source" <prompt>
437
438 This reads the specified configuration file. This file is always parsed.
439
440 mainmenu::
441
442         "mainmenu" <prompt>
443
444 This sets the config program's title bar if the config program chooses
445 to use it. It should be placed at the top of the configuration, before any
446 other statement.
447
448 '#' Kconfig source file comment:
449
450 An unquoted '#' character anywhere in a source file line indicates
451 the beginning of a source file comment.  The remainder of that line
452 is a comment.
453
454
455 Kconfig hints
456 -------------
457 This is a collection of Kconfig tips, most of which aren't obvious at
458 first glance and most of which have become idioms in several Kconfig
459 files.
460
461 Adding common features and make the usage configurable
462 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
463 It is a common idiom to implement a feature/functionality that are
464 relevant for some architectures but not all.
465 The recommended way to do so is to use a config variable named HAVE_*
466 that is defined in a common Kconfig file and selected by the relevant
467 architectures.
468 An example is the generic IOMAP functionality.
469
470 We would in lib/Kconfig see::
471
472   # Generic IOMAP is used to ...
473   config HAVE_GENERIC_IOMAP
474
475   config GENERIC_IOMAP
476         depends on HAVE_GENERIC_IOMAP && FOO
477
478 And in lib/Makefile we would see::
479
480         obj-$(CONFIG_GENERIC_IOMAP) += iomap.o
481
482 For each architecture using the generic IOMAP functionality we would see::
483
484   config X86
485         select ...
486         select HAVE_GENERIC_IOMAP
487         select ...
488
489 Note: we use the existing config option and avoid creating a new
490 config variable to select HAVE_GENERIC_IOMAP.
491
492 Note: the use of the internal config variable HAVE_GENERIC_IOMAP, it is
493 introduced to overcome the limitation of select which will force a
494 config option to 'y' no matter the dependencies.
495 The dependencies are moved to the symbol GENERIC_IOMAP and we avoid the
496 situation where select forces a symbol equals to 'y'.
497
498 Adding features that need compiler support
499 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
500
501 There are several features that need compiler support. The recommended way
502 to describe the dependency on the compiler feature is to use "depends on"
503 followed by a test macro::
504
505   config STACKPROTECTOR
506         bool "Stack Protector buffer overflow detection"
507         depends on $(cc-option,-fstack-protector)
508         ...
509
510 If you need to expose a compiler capability to makefiles and/or C source files,
511 `CC_HAS_` is the recommended prefix for the config option::
512
513   config CC_HAS_STACKPROTECTOR_NONE
514         def_bool $(cc-option,-fno-stack-protector)
515
516 Build as module only
517 ~~~~~~~~~~~~~~~~~~~~
518 To restrict a component build to module-only, qualify its config symbol
519 with "depends on m".  E.g.::
520
521   config FOO
522         depends on BAR && m
523
524 limits FOO to module (=m) or disabled (=n).
525
526 Kconfig recursive dependency limitations
527 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
528
529 If you've hit the Kconfig error: "recursive dependency detected" you've run
530 into a recursive dependency issue with Kconfig, a recursive dependency can be
531 summarized as a circular dependency. The kconfig tools need to ensure that
532 Kconfig files comply with specified configuration requirements. In order to do
533 that kconfig must determine the values that are possible for all Kconfig
534 symbols, this is currently not possible if there is a circular relation
535 between two or more Kconfig symbols. For more details refer to the "Simple
536 Kconfig recursive issue" subsection below. Kconfig does not do recursive
537 dependency resolution; this has a few implications for Kconfig file writers.
538 We'll first explain why this issues exists and then provide an example
539 technical limitation which this brings upon Kconfig developers. Eager
540 developers wishing to try to address this limitation should read the next
541 subsections.
542
543 Simple Kconfig recursive issue
544 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
545
546 Read: Documentation/kbuild/Kconfig.recursion-issue-01
547
548 Test with::
549
550   make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-01 allnoconfig
551
552 Cumulative Kconfig recursive issue
553 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
554
555 Read: Documentation/kbuild/Kconfig.recursion-issue-02
556
557 Test with::
558
559   make KBUILD_KCONFIG=Documentation/kbuild/Kconfig.recursion-issue-02 allnoconfig
560
561 Practical solutions to kconfig recursive issue
562 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
563
564 Developers who run into the recursive Kconfig issue have two options
565 at their disposal. We document them below and also provide a list of
566 historical issues resolved through these different solutions.
567
568   a) Remove any superfluous "select FOO" or "depends on FOO"
569   b) Match dependency semantics:
570
571         b1) Swap all "select FOO" to "depends on FOO" or,
572
573         b2) Swap all "depends on FOO" to "select FOO"
574
575 The resolution to a) can be tested with the sample Kconfig file
576 Documentation/kbuild/Kconfig.recursion-issue-01 through the removal
577 of the "select CORE" from CORE_BELL_A_ADVANCED as that is implicit already
578 since CORE_BELL_A depends on CORE. At times it may not be possible to remove
579 some dependency criteria, for such cases you can work with solution b).
580
581 The two different resolutions for b) can be tested in the sample Kconfig file
582 Documentation/kbuild/Kconfig.recursion-issue-02.
583
584 Below is a list of examples of prior fixes for these types of recursive issues;
585 all errors appear to involve one or more select's and one or more "depends on".
586
587 ============    ===================================
588 commit          fix
589 ============    ===================================
590 06b718c01208    select A -> depends on A
591 c22eacfe82f9    depends on A -> depends on B
592 6a91e854442c    select A -> depends on A
593 118c565a8f2e    select A -> select B
594 f004e5594705    select A -> depends on A
595 c7861f37b4c6    depends on A -> (null)
596 80c69915e5fb    select A -> (null)              (1)
597 c2218e26c0d0    select A -> depends on A        (1)
598 d6ae99d04e1c    select A -> depends on A
599 95ca19cf8cbf    select A -> depends on A
600 8f057d7bca54    depends on A -> (null)
601 8f057d7bca54    depends on A -> select A
602 a0701f04846e    select A -> depends on A
603 0c8b92f7f259    depends on A -> (null)
604 e4e9e0540928    select A -> depends on A        (2)
605 7453ea886e87    depends on A > (null)           (1)
606 7b1fff7e4fdf    select A -> depends on A
607 86c747d2a4f0    select A -> depends on A
608 d9f9ab51e55e    select A -> depends on A
609 0c51a4d8abd6    depends on A -> select A        (3)
610 e98062ed6dc4    select A -> depends on A        (3)
611 91e5d284a7f1    select A -> (null)
612 ============    ===================================
613
614 (1) Partial (or no) quote of error.
615 (2) That seems to be the gist of that fix.
616 (3) Same error.
617
618 Future kconfig work
619 ~~~~~~~~~~~~~~~~~~~
620
621 Work on kconfig is welcomed on both areas of clarifying semantics and on
622 evaluating the use of a full SAT solver for it. A full SAT solver can be
623 desirable to enable more complex dependency mappings and / or queries,
624 for instance on possible use case for a SAT solver could be that of handling
625 the current known recursive dependency issues. It is not known if this would
626 address such issues but such evaluation is desirable. If support for a full SAT
627 solver proves too complex or that it cannot address recursive dependency issues
628 Kconfig should have at least clear and well defined semantics which also
629 addresses and documents limitations or requirements such as the ones dealing
630 with recursive dependencies.
631
632 Further work on both of these areas is welcomed on Kconfig. We elaborate
633 on both of these in the next two subsections.
634
635 Semantics of Kconfig
636 ~~~~~~~~~~~~~~~~~~~~
637
638 The use of Kconfig is broad, Linux is now only one of Kconfig's users:
639 one study has completed a broad analysis of Kconfig use in 12 projects [0]_.
640 Despite its widespread use, and although this document does a reasonable job
641 in documenting basic Kconfig syntax a more precise definition of Kconfig
642 semantics is welcomed. One project deduced Kconfig semantics through
643 the use of the xconfig configurator [1]_. Work should be done to confirm if
644 the deduced semantics matches our intended Kconfig design goals.
645
646 Having well defined semantics can be useful for tools for practical
647 evaluation of depenencies, for instance one such use known case was work to
648 express in boolean abstraction of the inferred semantics of Kconfig to
649 translate Kconfig logic into boolean formulas and run a SAT solver on this to
650 find dead code / features (always inactive), 114 dead features were found in
651 Linux using this methodology [1]_ (Section 8: Threats to validity).
652
653 Confirming this could prove useful as Kconfig stands as one of the the leading
654 industrial variability modeling languages [1]_ [2]_. Its study would help
655 evaluate practical uses of such languages, their use was only theoretical
656 and real world requirements were not well understood. As it stands though
657 only reverse engineering techniques have been used to deduce semantics from
658 variability modeling languages such as Kconfig [3]_.
659
660 .. [0] http://www.eng.uwaterloo.ca/~shshe/kconfig_semantics.pdf
661 .. [1] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
662 .. [2] http://gsd.uwaterloo.ca/sites/default/files/ase241-berger_0.pdf
663 .. [3] http://gsd.uwaterloo.ca/sites/default/files/icse2011.pdf
664
665 Full SAT solver for Kconfig
666 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
667
668 Although SAT solvers [4]_ haven't yet been used by Kconfig directly, as noted
669 in the previous subsection, work has been done however to express in boolean
670 abstraction the inferred semantics of Kconfig to translate Kconfig logic into
671 boolean formulas and run a SAT solver on it [5]_. Another known related project
672 is CADOS [6]_ (former VAMOS [7]_) and the tools, mainly undertaker [8]_, which
673 has been introduced first with [9]_.  The basic concept of undertaker is to
674 exract variability models from Kconfig, and put them together with a
675 propositional formula extracted from CPP #ifdefs and build-rules into a SAT
676 solver in order to find dead code, dead files, and dead symbols. If using a SAT
677 solver is desirable on Kconfig one approach would be to evaluate repurposing
678 such efforts somehow on Kconfig. There is enough interest from mentors of
679 existing projects to not only help advise how to integrate this work upstream
680 but also help maintain it long term. Interested developers should visit:
681
682 http://kernelnewbies.org/KernelProjects/kconfig-sat
683
684 .. [4] http://www.cs.cornell.edu/~sabhar/chapters/SATSolvers-KR-Handbook.pdf
685 .. [5] http://gsd.uwaterloo.ca/sites/default/files/vm-2013-berger.pdf
686 .. [6] https://cados.cs.fau.de
687 .. [7] https://vamos.cs.fau.de
688 .. [8] https://undertaker.cs.fau.de
689 .. [9] https://www4.cs.fau.de/Publications/2011/tartler_11_eurosys.pdf