-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcnf_2_relaxed_wcnf.py
executable file
·137 lines (123 loc) · 6.26 KB
/
cnf_2_relaxed_wcnf.py
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
#!/usr/bin/python
#Title : cnf_2_relaxed_wcnf.py
#Usage : python cnf_2_relaxed_wcnf.py -h
#Author : pmorvalho
#Date : March 06, 2023
#Description : Given a CNF formula generated by CBMC, this script generates a WCNF. The soft clauses are the relaxation variables (bool) of the program that indicate if a given line is executed or not.
#Notes :
#Python Version : 3.8.5
# (C) Copyright 2023 Pedro Orvalho.
#==============================================================================
import argparse
from sys import argv
import sys
from helper import *
# the format of the string that correspond to relaxation variables in our C programs
relax_var_format="__l_"
# Weight we want to assign to the soft clauses in the generated WCNF formulae
SOFT_WEIGHT=1
# bits used for each bool
BITS_BOOL=8
def process_cnf(f):
# receives cnf
# returns
# wcnf header
# set of hard clauses already with the corresponding hard weight,
# the weight associated with the hard clauses
# the set of literals that correspond to each relaxation variable
# the list of comments of the cnf formula
lines = open(args.cnf, "r+").readlines()
hard_clauses = []
header = None
rv_literals = dict()
hard_weight = None
comts=[]
l_cmts=[]
rv_iterations=dict()
for l in lines:
if l[0] == 'p':
_, _, n_vars, n_clauses = l[:-1].split(" ")
hard_weight=int(n_clauses)*2
if not args.pwcnf:
header = "p wcnf {v} {c} {w}\n".format(v=n_vars,c=n_clauses,w=hard_weight)
else:
header = "p pwcnf {v} {c} {w} {p}\n".format(v=n_vars,c=n_clauses,w=hard_weight, p=(args.num_unroll+1) if args.num_unroll != None else 32)
elif l[0] == 'c':
if relax_var_format in l and "main::" in l:
n_var, lits = l.split("!")
n_var = n_var.split("::")[-1]
lits = lits[:-1].split()
ind, lits = lits[0], lits[1:]
ind = int(ind.split("#")[-1])
if n_var not in rv_literals.keys() or ind > rv_iterations[n_var]:
rv_literals[n_var] = [lits]
rv_iterations[n_var] = ind
l_cmts.insert(0, l)
# elif ind==args.num_unroll:
# print(ind)
# print(lits)
# rv_literals[n_var] = [lits]
# l_cmts.insert(0, l)
else:
comts.append(l)
else:
hard_clauses.append("{w} {r}".format(w=hard_weight, r=l))
return header, hard_clauses, hard_weight, rv_literals, sorted(l_cmts)+comts
def parser():
parser = argparse.ArgumentParser(prog='cnf_2_relaxed_wcnf.py', formatter_class=argparse.RawTextHelpFormatter)
parser.add_argument('-i', '--cnf', help='CNF formula generated by CBMC.')
parser.add_argument('-o', '--outfile', help='the path of the output file for the WCNF formula.')
parser.add_argument('-msi', '--map_stu_insts', nargs='?', help='Path to the mapping from instrumentalized-unrolled program statements to the original students\' instructions.')
parser.add_argument('-v', '--verbose', action='store_true', default=False, help='Prints debugging information.')
parser.add_argument('-s', '--sat', action='store_true', default=False, help='Generates a CNF formula, with all the relaxed variable assigned to true. This can be used to verify correct programs.')
parser.add_argument('-nu', '--num_unroll', type=int, help='Number of times each loop is going to be unrolled.')
parser.add_argument('-p', '--pwcnf', action='store_true', default=False, help='Generates a PWCNF formula. A WCNF formula with partitioning information. Each soft clause is assigned a parition number. Each program instruction is assigned to partition 2 (partition 1 is for hard clauses). Unless, the instruction is inside a loop, then it is assigned to a partition based on the number of interations of the loop.')
args = parser.parse_args(argv[1:])
return args
if __name__ == '__main__':
py_print=print
args = parser()
header, hard_clauses, hard_weight, rv_literals, comts = process_cnf(args.cnf)
if args.outfile is not None:
f_out=open(args.outfile, "w+")
print = lambda out_str : py_print(out_str, end="", file=f_out)
print(header)
map_stmts = load_dict(args.map_stu_insts) if args.map_stu_insts != None else None
for hc in hard_clauses:
if not args.pwcnf:
print(hc)
else:
print("1 {h}".format(h=hc))
for k in sorted(list(rv_literals.keys())):
if k not in map_stmts.keys():
continue
for lits in rv_literals[k]:
print("c {k} {l}\n".format(k=k, l=lits))
for l in range(len(lits)):
if lits[l] == "TRUE" or lits[l] == "FALSE":
continue
it = int((l+1) % BITS_BOOL)
if it != 0:
if not args.pwcnf:
print("{hw} -{l} 0\n".format(hw=hard_weight, l=lits[l]))
else:
print("1 {hw} -{l} 0\n".format(hw=hard_weight, l=lits[l]))
elif args.sat:
if not args.pwcnf:
print("{hw} {l} 0\n".format(hw=hard_weight, l=lits[l]))
else:
print("1 {hw} {l} 0\n".format(hw=hard_weight, l=lits[l]))
elif not args.pwcnf:
if map_stmts[k][1] != None:
print("{sw} {l} 0\n".format(sw=map_stmts[k][1] if map_stmts != None else SOFT_WEIGHT, l=lits[l]))
else:
print("{hw} {l} 0\n".format(hw=hard_weight, l=lits[l]))
else:
itt = int((l+1) / BITS_BOOL) % args.num_unroll if (l+1) > BITS_BOOL else 1
it = itt + 1 if itt > 0 else args.num_unroll + 1
print("{i} {sw} {l} 0\n".format(i=it, sw=map_stmts[k][1] if map_stmts != None else SOFT_WEIGHT, l=lits[l]))
#print("{sw} {l} 0\n".format(sw=k.split("_")[-1], l=lits[-1]))
print("c {k} done\n".format(k=k))
# for c in comts:
# print(c)
print = py_print