From: Michal Sojka <sojkam1@fel.cvut.cz>
Date: Mon, 26 Oct 2015 08:19:35 +0000 (+0100)
Subject: kconfig2sat: Fix single-diff problem generation
X-Git-Url: http://rtime.felk.cvut.cz/gitweb/linux-conf-perf.git/commitdiff_plain/79d9948def604018321e9a98bfda2777d16a69a3

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.
---

diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc
index aa68bd5..5108642 100644
--- a/kconfig2sat/kconfig2sat.cc
+++ b/kconfig2sat/kconfig2sat.cc
@@ -296,12 +296,25 @@ struct SatExpr {
 
 class SatLiterals : protected vector<struct SatLiteral>
 {
+	unsigned _symbols = 0;
 public:
 	using vector<struct SatLiteral>::begin;
 	using vector<struct SatLiteral>::end;
-	using vector<struct SatLiteral>::push_back;
+
 	SatLiterals() { reserve(20000); }
+	SatLiteral &add(struct symbol *sym) {
+		sym->lcp.id = count() + 1;
+		push_back(SatLiteral(sym));
+		_symbols++;
+		return last();
+	}
+	SatLiteral &add(struct expr *e) {
+		e->lcp.id = count() + 1;
+		push_back(SatLiteral(e));
+		return last();
+	}
 	int count() const { return size(); }
+	int symbols() const { return _symbols; }
 	const SatLiteral &operator[](size_type i) const { return at(i-1); }
 	SatLiteral &last() { return *(--end()); }
 	bool test_set_dot_printed(struct symbol *sym) const {
@@ -585,19 +598,17 @@ public:
 	}
 
 	const SatLiteral &add_literal(struct symbol *sym) {
-		sym->lcp.id = literals.count() + 1;
-		literals.push_back(SatLiteral(sym));
+		SatLiteral &l = literals.add(sym);
 		if (dot)
-			dot->literal(literals.last());
-		return literals.last();
+			dot->literal(l);
+		return l;
 	}
 
 	const SatLiteral &add_literal(struct expr *e) {
-		e->lcp.id = literals.count() + 1;
-		literals.push_back(SatLiteral(e));
+		SatLiteral &l = literals.add(e);
 		if (dot)
-			dot->literal(literals.last());
-		return literals.last();
+			dot->literal(l);
+		return l;
 	}
 
 	void symbols2literals() {
@@ -822,9 +833,9 @@ public:
 
 		for (auto l: literals) {
 			if (l.sym)
-				fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
+				fprintf(f, "c SYM %d %s\n", l.id(), l.sym->name);
 			if (l.expr)
-				fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
+				fprintf(f, "c EXPR %d %s\n", l.id(), expr_to_string(l.expr).get());
 		}
 		for (auto clause: clauses) {
 			for (sat_id id: clause) {
@@ -843,13 +854,16 @@ public:
 			exit(EXIT_FAILURE);
 		}
 
-		fprintf(f, "p cnf %d %lu\n", 2*literals.count(), 2*clauses.size() + 2*literals.count());
+		fprintf(f, "p cnf %d %lu\n", 2*literals.count(), 2*clauses.size() + 2*literals.symbols());
 
 		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());
+				fprintf(f, "c SYM %d,%d %s\n", l.id(), l.id() + literals.count(), l.sym->name);
+			if (l.expr) {
+				struct gstr gs = str_new();
+				expr_gstr_print(l.expr, &gs);
+				fprintf(f, "c EXPR %d,%d %s\n", l.id(), l.id() + literals.count(), str_get(&gs));
+			}
 		}
 		for (auto clause: clauses) {
 			for (sat_id id: clause) {
@@ -865,7 +879,9 @@ public:
 		}
 		fprintf(f, "c Equivalence\n");
 		for (auto l: literals) {
-			if (l.sym && strcmp(sym_name, l.sym->name) != 0) {
+			if (!l.sym)
+				continue;
+			if (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 {