From 85a82310f73ddf212c297505248a59e0898b1204 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Karel=20Ko=C4=8D=C3=AD?= Date: Tue, 5 May 2015 17:41:23 +0200 Subject: Replace minisat with picosat Picosat is distributed with this project. --- scripts/solution.py | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) (limited to 'scripts') 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: -- cgit v1.2.3