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