Replace minisat with picosat

Picosat is distributed with this project.

3 files changed, 23 insertions, 14 deletions

diff --git a/Makefile b/Makefile
index 906a187..ce3c188 100644
--- a/Makefile
+++ b/Makefile
@@ -1,11 +1,11 @@
-.PHONY: all help parse_kconfig write_config build run test clean clean_linux clean_buildroot mlinux mbuildroot deflinux distclean_linux distclean_buildroot distclean
+.PHONY: all help parse_kconfig write_config build run test clean clean_linux clean_buildroot mlinux mbuildroot deflinux distclean_linux distclean_buildroot distclean picosat
 
 -include .conf.mk
 
 BENCHMARK_FILES := $(patsubst benchmark/%,scripts/buildroot/system/skeleton/usr/share/benchmark/%,$(shell find benchmark -type f))
 BENCHMARK_FOLDERS := $(shell dirname $(BENCHMARK_FILES))
 
-all: parse_kconfig write_config
+all: parse_kconfig write_config picosat
 
 help:
 	@echo "all         - Builds basic programs and prints message about next steps."
@@ -44,15 +44,16 @@ deflinux:
 test: $(INITRAM) parse_kconfig
 	scripts/test.py
 
-run: parse_kconfig write_config $(INITRAM)
+run: parse_kconfig write_config picosat $(INITRAM)
 	scripts/loop.py
 
 evaluate:
 	@ #TODO
 
 clean:
-	@$(MAKE) -C scripts/parse_kconfig/ clean
-	@$(MAKE) -C scripts/write_config/ clean
+	@$(MAKE) -C scripts/parse_kconfig clean
+	@$(MAKE) -C scripts/write_config clean
+	@if [ -e scripts/picosat-959/makefile ]; then $(MAKE) -C scripts/picosat-959 clean; fi
 	$(RM) -r build
 	$(RM) -r scripts/buildroot/system/skeleton/usr/share/benchmark
 	$(RM) $(INITRAM)
@@ -107,3 +108,8 @@ scripts/buildroot/system/skeleton/usr/bin/linux-conf-perf:
 $(BENCHMARK_FILES): $(BENCHMARK_FOLDERS)
 scripts/buildroot/system/skeleton/usr/share/benchmark/%: benchmark/%
 	cp $< $@
+
+picosat: scripts/picosat-959/picosat
+scripts/picosat-959/picosat:
+	cd scripts/picosat-959 && ./configure
+	$(MAKE) -C scripts/picosat-959
diff --git a/conf.py b/conf.py
index 833f64b..36e7487 100644
--- a/conf.py
+++ b/conf.py
@@ -6,7 +6,7 @@ ARCH = SRCARCH
 linux_make_args = ['-j8']
 novaboot_args = ['--qemu=qemu-system-x86_64']
 
-minisat_args = []
+picosat_args = []
 # Programs output show/hide
 parse_kconfig_output = False
 minisat_output = False
@@ -55,7 +55,7 @@ nbscript = 'scripts/nbscript'
 parse_kconfig = 'scripts/parse_kconfig/parse'
 write_config = 'scripts/write_config/write'
 novaboot = 'scripts/novaboot/novaboot'
-minisat = 'minisat'
+picosat = 'scripts/picosat-959/picosat'
 
 
 absroot = os.path.dirname(os.path.realpath(__file__))
diff --git a/scripts/solution.py b/scripts/solution.py
index 649e3d2..ee1c043 100644
--- a/scripts/solution.py
+++ b/scripts/solution.py
@@ -54,11 +54,12 @@ def generate():
 
 	# Execute minisat
 	if conf.minisat_output:
-		subprocess.call([conf.minisat, w_file.name, sf(conf.solution_file)]
-				+ conf.minisat_args)
+		subprocess.call([conf.picosat, w_file.name, '-o',
+			sf(conf.solution_file)] + conf.picosat_args)
 	else:
-		subprocess.call([conf.minisat, w_file.name, sf(conf.solution_file)]
-				+ conf.minisat_args, stdout=subprocess.DEVNULL)
+		subprocess.call([conf.picosat, w_file.name, '-o',
+			sf(conf.solution_file)] + conf.picosat_args,
+			stdout=subprocess.DEVNULL)
 
 	os.remove(w_file.name)
 
@@ -72,10 +73,13 @@ def apply():
 	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() == 'SAT':
+		if not f.readline().rstrip() == 's SATISFIABLE':
 			raise NoSolution()
-		solut = f.readline().split()
+		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
@@ -88,7 +92,6 @@ def apply():
 			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: