1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
|
#!/usr/bin/env python3
# -*- coding: utf-8 -*-
# Copyright (C) 2009-2020 Authors of CryptoMiniSat, see AUTHORS file
#
# This program is free software; you can redistribute it and/or
# modify it under the terms of the GNU General Public License
# as published by the Free Software Foundation; version 2
# of the License.
#
# This program is distributed in the hope that it will be useful,
# but WITHOUT ANY WARRANTY; without even the implied warranty of
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
# GNU General Public License for more details.
#
# You should have received a copy of the GNU General Public License
# along with this program; if not, write to the Free Software
# Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
# 02110-1301, USA.
from __future__ import with_statement # Required in 2.5
from __future__ import print_function
import random
def shuffle_cnf(fname1, fname2, seed):
random.seed(int(seed))
with open(fname1, "r") as f1:
headers = []
lines = []
for line in f1:
line = line.strip()
if len(line) > 1 and line[0] == 'p':
headers.append(line)
else:
lines.append(line)
random.shuffle(lines)
with open(fname2, "w") as f2:
for line in headers:
f2.write(line+"\n")
for line in lines:
f2.write(line+"\n")
def get_max_var_from_clause(line):
maxvar = 0
# strip leading 'x'
line2 = line.strip()
if len(line2) > 0 and line2[0] == 'x':
line2 = line2[1:]
for lit in line2.split():
num = 0
try:
num = int(lit)
except ValueError:
print("line '%s' contains a non-integer variable" % line2)
maxvar = max(maxvar, abs(num))
return maxvar
class debuglib:
@staticmethod
def generate_random_assumps(maxvar):
assumps = ""
num = 0
varsInside = set()
# Half of the time, no assumptions at all
if random.randint(0, 1) == 1:
return assumps
# use a distribution so that few will be in assumps
while (num < maxvar and random.randint(0, 4) > 0):
# get a var that is not already inside the assumps
thisVar = random.randint(1, maxvar)
tries = 0
while (thisVar in varsInside):
thisVar = random.randint(1, maxvar)
tries += 1
# too many tries, don't waste time
if tries > 100:
return assumps
varsInside.add(thisVar)
# random sign
num += 1
if random.randint(0, 1):
thisVar *= -1
assumps += "%d " % thisVar
return assumps
@staticmethod
def file_len_no_comment(fname):
i = 0
with open(fname) as f:
for l in f:
# ignore comments and empty lines and header
if not l or l[0] == "c" or l[0] == "p":
continue
i += 1
return i
@staticmethod
def main(fname1, fname2):
# approx number of solve()-s to add
if random.randint(0, 1) == 1:
num_to_add = random.randint(0, 10)
else:
num_to_add = 0
# based on length and number of solve()-s to add, intersperse
# file with ::solve()
file_len = debuglib.file_len_no_comment(fname1)
if num_to_add > 0:
nextToAdd = random.randint(1, int(file_len / num_to_add) + 1)
else:
nextToAdd = file_len + 1
fin = open(fname1, "r")
fout = open(fname2, "w")
at = 0
maxvar = 0
for line in fin:
line = line.strip()
# ignore comments (but write them out)
if not line or line[0] == "c" or line[0] == 'p':
fout.write(line + '\n')
continue
at += 1
if at >= nextToAdd:
assumps = debuglib.generate_random_assumps(maxvar)
if random.choice([True, False]):
fout.write("c Solver::solve( %s )\n" % assumps)
elif random.choice([True, False]):
fout.write("c Solver::simplify( %s )\n" % assumps)
else:
fout.write("c Solver::simplify( %s )\n" % assumps)
fout.write("c Solver::solve( %s )\n" % assumps)
nextToAdd = at + \
random.randint(1, int(file_len / num_to_add) + 1)
# calculate max variable
maxvar = max(maxvar, get_max_var_from_clause(line))
# copy line over
fout.write(line + '\n')
fout.close()
fin.close()
def intersperse(fname1, fname2, seed):
random.seed(int(seed))
debuglib.main(fname1, fname2)
|
