From 4e2a6b5219f469c4b05628a0133340ba2fa2d807 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Karel=20Ko=C4=8D=C3=AD?= <cynerd@email.cz>
Date: Thu, 7 May 2015 13:25:04 +0200
Subject: Add implementation of  hash indexing of configurations

---
 scripts/solution.py | 108 +++++++++++++++++++++++++++++-----------------------
 1 file changed, 61 insertions(+), 47 deletions(-)

(limited to 'scripts/solution.py')

diff --git a/scripts/solution.py b/scripts/solution.py
index 8e02324..f9f605b 100644
--- a/scripts/solution.py
+++ b/scripts/solution.py
@@ -2,6 +2,7 @@ import os
 import sys
 import tempfile
 import subprocess
+import time
 
 import utils
 from conf import conf
@@ -16,7 +17,7 @@ def generate():
 	if not os.path.isfile(sf(conf.rules_file)):
 		raise exceptions.MissingFile(conf.rules_file,"Run parse_kconfig.")
 
-	if sys.path.isfile(sf(conf.solution_file)) and conf.gen_all_solution_oninit:
+	if os.path.isfile(sf(conf.solution_file)) and conf.gen_all_solution_oninit:
 		raise exceptions.SolutionGenerated()
 
 	w_file = tempfile.NamedTemporaryFile(delete=False)
@@ -50,56 +51,69 @@ def generate():
 	w_file.close()
 
 	# Execute picosat
-	picosat_cmd = [conf.picosat, w_file.name]
-	picosat_cmd += ['-o', sf(conf.solution_file)]
+	try:
+		os.mkdir(sf(conf.log_folder))
+	except OSError:
+		pass
+
+	picosat_cmd = [sf(conf.picosat), w_file.name]
 	if (conf.gen_all_solution_oninit):
 		picosat_cmd += ['--all']
-	if conf.picosat_output:
-		subprocess.call(picosat_cmd)
-	else:
-		subprocess.call(picosat_cmd, stdout=subprocess.DEVNULL)
+
+	satprc = subprocess.Popen(picosat_cmd, stdout = subprocess.PIPE)
+	with open(os.path.join(sf(conf.log_folder), "picosat.log"), 'a') as f:
+		f.write("::" + time.strftime("%y-%m-%d-%H-%M-%S") + "::\n")
+		solut = []
+		for linen in satprc.stdout:
+			line = linen.decode(sys.getdefaultencoding())
+			f.write(line)
+			if conf.picosat_output:
+				print(line, end="")
+			if line[0] == 's':
+				if line.rstrip() == 's SATISFIABLE':
+					try:
+						solut.remove(0)
+						with open(sf(conf.config_map_file), 'a') as fm:
+							fm.write(str(utils.hash_config(solut)) + ':')
+							for sl in solut:
+								fm.write(str(sl) + ' ')
+							fm.write('\n')
+						with open(sf(conf.solved_file), 'a') as fs:
+							for sl in solut:
+								fs.write(str(-1 * sl) + ' ')
+							fs.write('\n')
+					except ValueError:
+						pass
+					solut = []
+				else:
+					os.remove(w_file.name)
+					raise exceptions.NoSolution()
+			elif line[0] == 'v':
+				for sl in line[2:].split():
+					solut.append(int(sl))
 
 	os.remove(w_file.name)
 
 def apply():
 	"""Apply generated solution to kernel source.
 	"""
-	# Check if solution_file exist
-	if not os.path.isfile(sf(conf.solution_file)):
-		raise Exception("Solution file is missing. Run sat_solution and check existence of " + sf(conf.solution_file))
-	
 	utils.build_symbol_map() # Ensure smap existence
 
-	# Read solution if satisfiable
-	solut = []
-	with open(sf(conf.solution_file), 'r') as f:
-		if not f.readline().rstrip() == 's SATISFIABLE':
-			raise NoSolution()
-		for line in f:
-			if line[0] == 'v':
-				solut += line[2:].split()
-	solut.remove('0') # Remove 0 at the end 
-
-	# Write solution to output_confs file
-	with open(sf(conf.output_confs), 'a') as f:
-		iteration = 0
-		with open(sf(conf.iteration_file)) as ff:
-			iteration = int(ff.readline())
-		f.write(str(iteration) + ':')
-		for txt in solut:
-			f.write(txt + ' ')
-		f.write('\n')
-
-	# Write negotation solution to solver_file
-	with open(sf(conf.solved_file), 'a') as f:
-		for txt in solut:
-			if txt[0] == '-':
-				ntx = ""
-				txt = txt[1:]
-			else:
-				ntx = "-"
-			f.write( ntx + txt + " ")
-		f.write("\n")
+	solved = set()
+	solution = []
+	if os.path.isfile(sf(config_solved_file)):
+		with open(sf(conf.config_solved_file)) as f:
+			for ln in f:
+				solved.add(ln.strip())
+
+	with open(sf(conf.config_map_file)) as f:
+			while True:
+				w = f.readline().split(sep=':')
+				if not w[0] in solved:
+					solution = utils.config_strtoint(w[1])
+					break;
+	if not solution:
+		raise exceptions.NoApplicableSolution()
 
 	# Load variable count
 	with open(sf(conf.symbol_map_file)) as f:
@@ -108,18 +122,18 @@ def apply():
 		var_num += 1
 	# Write solution to .config file in linux source folder
 	with open(sf(conf.linux_dot_config), 'w') as f:
-		for txt in solut:
-			if txt[0] == '-':
+		for s in solution:
+			if s < 0:
 				nt = True
-				txt = txt[1:]
+				s *= -1
 			else:
 				nt = False
-			if int(txt) >= var_num:
+			if s >= var_num:
 				break;
-			if 'NONAMEGEN' in utils.smap[txt]: # ignore generated names
+			if 'NONAMEGEN' in utils.smap[s]: # ignore generated names
 				continue
 
-			f.write('CONFIG_' + utils.smap[txt] + '=')
+			f.write('CONFIG_' + utils.smap[s] + '=')
 			if not nt:
 				f.write('y')
 			else:
-- 
cgit v1.2.3