]> rtime.felk.cvut.cz Git - linux-conf-perf.git/commit
projects / linux-conf-perf.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cf1496b) | patch
kconfig2sat: Fix single-diff problem generation
authorMichal Sojka <sojkam1@fel.cvut.cz>
Mon, 26 Oct 2015 08:19:35 +0000 (09:19 +0100)
committerMichal Sojka <sojkam1@fel.cvut.cz>
Mon, 26 Oct 2015 08:19:35 +0000 (09:19 +0100)
commit79d9948def604018321e9a98bfda2777d16a69a3
tree1b443df7a809a8aa5e08d996956d9481947e777ftree | snapshot
parentcf1496bc572e2d339b02186eac36f4413eda8453commit | diff
kconfig2sat: Fix single-diff problem generation

We must generate equivalence clauses only for symbol literals. Expression
literals may have different value depending on the "single" variable
symbol.

Therefore, we learn SatLiterals to count the number of symbols so that we
can easily construct the p-line in DIMACS file.
kconfig2sat/kconfig2sat.cc diff | blob | history
Automated overhead analysis of Linux configuration options