#!/usr/bin/env python3

import re, sys, os

# read gcov result and return a list of lines executed:
def parse_gcov_file (fname):
    lines=[]
    f=open(fname,"r")
 
    while True:
        l=f.readline().rstrip()
        m = re.search('^ *([0-9]+):  ([0-9]+):.*$', l)
        if m!=None:
            lines.append(int(m.group(2)))
        if len(l)==0:
            break

    f.close()
    return lines

max_test_n=0

# k=line, v=list of tests
lines={}

# k=tbl_entry, v=list of tests
tbl_entries={}

# enumerate all gcov-files:
for (dirpath, dirnames, filenames) in os.walk ("gcovs"):
    for fname in filenames:
        #print "c fname", fname
        fullfname="gcovs/"+fname
        test_n=int(fname.split(".")[0])
        max_test_n=max(max_test_n, test_n)
        tbl_entry=int(fname.split(".")[1])

        tbl_entries[tbl_entry]=tbl_entries.get(tbl_entry, [])+[test_n]

        lines_executed=parse_gcov_file (fullfname)

        for line in lines_executed:
            lines[line]=lines.get(line, [])+[test_n]

def list_to_CNF(l):
    return "10000 "+" ".join(map(str, l))+" 0"

print ("p wcnf "+str(max_test_n)+" "+str(len(tbl_entries)+len(lines)+max_test_n-1)+" 10000")

# hard clauses. each MUST be satisfied
# "test_1 OR test_2 OR ..." for table entry
print ("c tbl entries:")
for tbl_entry in tbl_entries:
    print ("c tbl_entry="+str(tbl_entry))
    print (list_to_CNF(tbl_entries[tbl_entry]))

print ("c lines:")
for line in lines:
    print ("c line=", str(line))
    print (list_to_CNF(lines[line]))

# soft clauses. as many should be satisfied (be False) as possible
for test_n in range(max_test_n):
    print ("1 -"+str(test_n+1)+" 0")