cex-kc/util.py at main · whoami730/cex-kc · GitHub

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
BNAME = "Benchmark Name"
VORDER = "Variable Ordering"
HASH = "Hash"

BNAME_FIELD = "-b"
VORDER_FIELD = "-v"
OUTFOLDR_FIELD = "--out"
TIMEOUT_FIELD = "-t"
UNATE_FIELD = "-u"
FASTCNF_FIELD = "-f"
DYNORDER_FIELD = "-o"
BOOL_FIELDS = [UNATE_FIELD,"-s",DYNORDER_FIELD,FASTCNF_FIELD]
VAL_FIELDS = [ "-c", "-r", "-d", TIMEOUT_FIELD, "--unateTimeout"]
NON_BOOL_FIELDS = [BNAME_FIELD, VORDER_FIELD] + VAL_FIELDS
CONFIG_FIELDS = BOOL_FIELDS + VAL_FIELDS
FIELDS = [BNAME_FIELD, VORDER_FIELD] + CONFIG_FIELDS + [HASH]
# name, order, booleans, values

INIT_UN = "Initial unates"
FIN_UN = "Final unates"
PHASE_CNT = "Phase Count"
TOT_OUTPUTS = "Total outputs without unate"
FIXED_OUTPUTS = "Outputs fixed"
NUM_CEX = "Number of cex"
TOT_TIME = "Time taken"
ERR = "ERROR"

RESULTS = ["Initial size", "Final size", INIT_UN, FIN_UN, PHASE_CNT, "Number of iterations", NUM_CEX, FIXED_OUTPUTS, TOT_OUTPUTS, TOT_TIME, "repairTime", "conflictCnfTime", "satSolvingTime", "unateTime", "compressTime", "rectifyCnfTime", "rectifyUnsatCoreTime", "overallCnfTime", ERR]

# ["Benchmark", "VarOrder", "unate?","shannon?", "dynamic?", "fastCNF?"]
HEADER = FIELDS + RESULTS

ALLUNATES = "allUnates"
NOCONFU = "noConflictsWithUnates"
NOCONF = "noConflicts"
NOU = "noUnates"
OTHER = "others"
ERROR = "error"
FIXEDCONF = "fixedConflicts"
SOMEU = "someUnates"

FILENAMES = [ALLUNATES, NOCONFU, NOCONF, NOU, OTHER, ERROR, FIXEDCONF, SOMEU]

IS_SOLVED = "isSolved"

# row maps directly to HEADER
def process(D: dict, outputs: list, error: bool) :
    # U in the end signifies Unate, no U means No Unate case
    row = [D[k] for k in FIELDS] + outputs
    bname, vorder, hash = D[BNAME_FIELD], D[VORDER_FIELD], D[HASH]
    def isSolved():
        return not error and (int(row[HEADER.index(FIXED_OUTPUTS)]) == int(row[HEADER.index(TOT_OUTPUTS)]))
    def isAllU():
        return int(row[HEADER.index(TOT_OUTPUTS)]) == 0 and isSolved()
    def isNoConfU():
        return (UNATE_FIELD in row) and (int(row[HEADER.index(NUM_CEX)]) == 0) and isSolved()
    def isNoConf():
        return (UNATE_FIELD not in row) and (int(row[HEADER.index(NUM_CEX)]) == 0) and isSolved()
    def isNoU():
        # fully solved but had no unates
        return (UNATE_FIELD in row) and (int(row[HEADER.index(FIN_UN)]) == 0) and isSolved()

    d = dict()
    if (error):
        d[ERROR] = True
    else:
        if isAllU():
            d[ALLUNATES] = True
        if isNoConfU():
            d[NOCONFU] = True
        if isNoConf():
            d[NOCONF] = True
        if isNoU():
            d[NOU] = True
        if (len(d) == 0) and isSolved():
            d[OTHER] = True

    for k in [BNAME_FIELD, VORDER_FIELD, HASH]:
        D.pop(k)

    d_all = dict({BNAME: bname, VORDER: vorder, HASH: hash, "config": D, IS_SOLVED: isSolved(), "results": dict(zip(RESULTS, outputs)), "files": d})

    return row, bname, hash, d, d_all