diff options
| -rw-r--r-- | Makefile | 16 | ||||
| -rw-r--r-- | conf.py | 4 | ||||
| -rw-r--r-- | scripts/solution.py | 17 |
3 files changed, 23 insertions, 14 deletions
@@ -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 @@ -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: |