From: Michal Sojka <sojkam1@fel.cvut.cz>
Date: Sun, 25 Oct 2015 22:53:48 +0000 (+0100)
Subject: kconfig2sat: Preliminary support for generating pairs of "single-diff" configurations
X-Git-Url: http://rtime.felk.cvut.cz/gitweb/linux-conf-perf.git/commitdiff_plain/cf1496bc572e2d339b02186eac36f4413eda8453

kconfig2sat: Preliminary support for generating pairs of "single-diff" configurations

i.e. configurations which differ in just one option.
---

diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc
index f014419..aa68bd5 100644
--- a/kconfig2sat/kconfig2sat.cc
+++ b/kconfig2sat/kconfig2sat.cc
@@ -835,7 +835,52 @@ public:
 		}
 		fclose(f);
 	}
+	void write_dimacs_cnf_single(const char *cnf, const char *sym_name) {
+		FILE *f = fopen((string(cnf)+"-single-"+sym_name).c_str(), "w");
 
+		if (!f) {
+			perror(cnf);
+			exit(EXIT_FAILURE);
+		}
+
+		fprintf(f, "p cnf %d %lu\n", 2*literals.count(), 2*clauses.size() + 2*literals.count());
+
+		for (auto l: literals) {
+			if (l.sym)
+				fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
+			if (l.expr)
+				fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
+		}
+		for (auto clause: clauses) {
+			for (sat_id id: clause) {
+				assert(id != 0);
+				fprintf(f, "%d ", id);
+			}
+			fprintf(f, "0\n");
+
+			for (sat_id id: clause) {
+				fprintf(f, "%d ", id > 0 ? id + literals.count() : id - literals.count());
+			}
+			fprintf(f, "0\n");
+		}
+		fprintf(f, "c Equivalence\n");
+		for (auto l: literals) {
+			if (l.sym && strcmp(sym_name, l.sym->name) != 0) {
+				fprintf(f, "%d %d 0\n", -l.id(), l.id() + literals.count());
+				fprintf(f, "%d %d 0\n", -l.id() - literals.count(), l.id());
+			} else {
+				fprintf(f, "%d 0\n", +l.id());
+				fprintf(f, "%d 0\n", -l.id() - literals.count());
+			}
+		}
+		fclose(f);
+	}
+
+	void write_dimacs_cnf_all_single(const char *cnf) {
+		for (auto l: literals)
+			if (l.sym)
+				write_dimacs_cnf_single(cnf, l.sym->name);
+	}
 };
 
 int main(int argc, char **argv)
@@ -953,6 +998,8 @@ int main(int argc, char **argv)
 
 	if (cnf)
 		sat_data.write_dimacs_cnf(cnf);
+	if (cnf)
+		sat_data.write_dimacs_cnf_all_single(cnf);
 
 	return EXIT_SUCCESS;
 }