1#!/usr/bin/env python3 2# -*- coding: utf-8 -*- 3 4# Copyright (C) 2014 Mate Soos 5# 6# This program is free software; you can redistribute it and/or 7# modify it under the terms of the GNU General Public License 8# as published by the Free Software Foundation; version 2 9# of the License. 10# 11# This program is distributed in the hope that it will be useful, 12# but WITHOUT ANY WARRANTY; without even the implied warranty of 13# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 14# GNU General Public License for more details. 15# 16# You should have received a copy of the GNU General Public License 17# along with this program; if not, write to the Free Software 18# Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 19# 02110-1301, USA. 20 21from __future__ import print_function 22import os 23import optparse 24import subprocess 25import time 26import gzip 27import threading 28import glob 29 30 31class PlainHelpFormatter(optparse.IndentedHelpFormatter): 32 33 def format_description(self, description): 34 if description: 35 return description + "\n" 36 else: 37 return "" 38 39usage = "usage: %prog [options] cryptominisat5-binary testfile(s)" 40desc = """Test solver against some problems 41""" 42 43parser = optparse.OptionParser(usage=usage, description=desc, 44 formatter=PlainHelpFormatter()) 45 46parser.add_option("--verbose", "-v", action="store_true", default=False, 47 dest="verbose", help="Print more output") 48parser.add_option("--threads", "-t", default=4, type=int, 49 dest="threads", help="Number of threads") 50parser.add_option("--minisat", type=str, 51 dest="minisat_exe", help="MiniSat location") 52parser.add_option("--cms", type=str, 53 dest="cms_exe", help="CryptoMiniSat location") 54 55 56(options, args) = parser.parse_args() 57print_lock = threading.Lock() 58todo_lock = threading.Lock() 59 60if len(args) < 1: 61 print("ERROR: You must call this script with at least one argument, a file to check") 62 exit(-1) 63 64 65def go_through_cnf(f): 66 for line in f: 67 line = line.decode('ascii').strip() 68 if len(line) == 0: 69 continue 70 if line[0] == "p": 71 line = line.split() 72 assert line[1].strip() == "cnf" 73 assert line[2].isdigit() 74 return int(line[2]) 75 76 assert False 77 78 79def find_num_vars(fname): 80 81 try: 82 with gzip.open(fname, 'rb') as f: 83 maxvar = go_through_cnf(f) 84 except IOError: 85 with open(fname, 'rb') as f: 86 maxvar = go_through_cnf(f) 87 88 return maxvar 89 90todo = [] 91exitnum = 0 92 93 94class MyThread(threading.Thread): 95 def __init__(self, threadID, extraopts): 96 threading.Thread.__init__(self) 97 self.threadID = threadID 98 self.extraopts = extraopts 99 100 def run(self): 101 global todo 102 global exitnum 103 while len(todo) > 0: 104 with todo_lock: 105 fname = todo[0] 106 todo = todo[1:] 107 108 if options.verbose: 109 with print_lock: 110 print("Thread %d pikced up %s" % (self.threadID, fname)) 111 112 ret = self.test_velim_one_file(fname) 113 114 with todo_lock: 115 exitnum |= ret 116 117 if options.verbose: 118 with print_lock: 119 print("Finished thread %d" % self.threadID) 120 121 def test_velim_one_file(self, fname): 122 orig_num_vars = find_num_vars(fname) 123 124 simp_fname = "simp.out-%d" % self.threadID 125 try: 126 os.unlink(simp_fname) 127 except: 128 pass 129 130 toprint = "" 131 132 toexec = [options.cms_exe, "--zero-exit-status", 133 "--preproc", "1", "--verb", "0"] 134 toexec.extend(self.extraopts) 135 toexec.extend([fname, simp_fname]) 136 137 toprint += "Executing: %s\n" % toexec 138 with print_lock: 139 print(toprint) 140 toprint = "" 141 142 start = time.time() 143 cms_out_fname = "cms-%s.out" % os.path.split(fname)[1] 144 try: 145 with open(cms_out_fname, "w") as f: 146 subprocess.check_call(" ".join(toexec), stdout=f, shell=True) 147 except subprocess.CalledProcessError: 148 toprint += "*** ERROR CryptoMiniSat errored out!\n" 149 with print_lock: 150 print(toprint) 151 exit(-1) 152 return -1 153 t_cms = time.time()-start 154 num_vars_after_cms_preproc = find_num_vars(simp_fname) 155 156 start = time.time() 157 toexec = [options.minisat_exe, fname] 158 toprint += "Executing: %s\n" % toexec 159 minisat_out_fname = "minisat_elim_data.out-%d" % self.threadID 160 try: 161 with open(minisat_out_fname, "w") as f: 162 subprocess.check_call(" ".join(toexec), stdout=f, shell=True) 163 except subprocess.CalledProcessError: 164 toprint += "** Minisat errored out...\n" 165 with print_lock: 166 print(toprint) 167 exit(-1) 168 return -1 169 t_msat = time.time()-start 170 171 var_elimed = None 172 num_vars_after_ms_preproc = None 173 with open(minisat_out_fname, "r") as f: 174 for line in f: 175 line = line.strip() 176 if "num-vars-eliminated" in line: 177 var_elimed = int(line.split()[1]) 178 if "num-free-vars" in line: 179 num_vars_after_ms_preproc = int(line.split()[1]) 180 181 assert var_elimed is not None, "Couldn't find var-elimed line, out: %s" % toprint 182 assert num_vars_after_ms_preproc is not None, "Couldn't find num-free-vars line, out: %s" % toprint 183 184 toprint += "-> orig num vars: %d\n" % orig_num_vars 185 toprint += "-> T-cms : %-4.2f free vars after: %-9d\n" % (t_cms, num_vars_after_cms_preproc) 186 toprint += "-> T-msat: %-4.2f free vars after: %-9d\n" % (t_msat, num_vars_after_ms_preproc) 187 diff = num_vars_after_cms_preproc - num_vars_after_ms_preproc 188 limit = float(orig_num_vars)*0.05 189 if diff < limit*8 and t_msat > t_cms*4 and t_msat > 20: 190 toprint += " * MiniSat didn't timeout, but we did, acceptable difference.\n" 191 with print_lock: 192 print(toprint) 193 return 0 194 195 if diff > limit: 196 toprint += "*** ERROR: No. vars difference %d is more than 5%% " % diff 197 toprint += "of original no. of vars, %d\n" % limit 198 with print_lock: 199 print(toprint) 200 return 1 201 202 toprint += "------------------[ thread %d ]------------------------" % self.threadID 203 204 with print_lock: 205 print(toprint) 206 207 return 0 208 209 210def test(extraopts): 211 global exitnum 212 exitnum = 0 213 global todo 214 assert os.path.isdir(args[0]) 215 path = os.path.join(args[0], '') 216 todo = glob.glob(path+"/*.cnf.gz") 217 218 threads = [] 219 for i in range(options.threads): 220 threads.append(MyThread(i, extraopts)) 221 222 for t in threads: 223 t.start() 224 225 for t in threads: 226 t.join() 227 228 if exitnum == 0: 229 print("ALL PASSED") 230 else: 231 print("SOME CHECKS FAILED") 232 233 return exitnum 234 235if __name__ == "__main__": 236 test(["--preschedule", "occ-bve,must-renumber"]) 237 if exitnum != 0: 238 exit(exitnum) 239