Replace minisat with picosat

[linux-conf-perf.git] / scripts / solution.py

diff --git a/scripts/solution.py b/scripts/solution.py
index 649e3d204bdcf6bd0bdca6a5e9946f07aaea6d94..ee1c04300de99216bd10439159a5929d8c99cf09 100644 (file)
--- 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: