scripts/sat_solution.py

   1 #!/bin/python3
   2 import os
   3 import sys
   4 import tempfile
   5 import subprocess
   6 from conf import conf
   7
   8 if not os.path.isfile(conf.rules_file):
   9         print("Error: Rules are not generated yet, or wrong build_folder.\nCheck existence of " + rules_file, file=sys.stderr)
  10         sys.exit(1)
  11
  12
  13 #w_file = tempfile.NamedTemporaryFile(delete=False)
  14 w_file = open('bld', 'w')
  15 # Join files to one single file
  16 lines = set()
  17 for ln in open(conf.rules_file, 'r'):
  18         if ln not in lines:
  19                 lines.add(ln)
  20 if os.path.isfile(conf.solved_file):
  21         for ln in open(conf.solved_file, 'r'):
  22                 if ln not in lines:
  23                         lines.add(ln)
  24 if os.path.isfile(conf.required_file):
  25         for ln in open(conf.required_file, 'r'):
  26                 if ln not in lines:
  27                         lines.add(ln)
  28
  29 with open(conf.symbol_map_file) as f:
  30         for var_num, l in enumerate(f):
  31                 pass
  32         var_num += 1
  33 lines_count = len(lines)
  34
  35 first_line = "p cnf " + str(var_num) + " " + str(lines_count)
  36 w_file.write(first_line + '\n')
  37 for ln in lines:
  38         w_file.write(ln)
  39
  40 w_file.close()
  41
  42 print("temp file: " + w_file.name)
  43 print("Output: " + conf.solution_file)
  44 subprocess.call(['minisat', w_file.name, conf.solution_file])
  45
  46 #os.remove(w_file.name)