parse.org

* verifier status
| verifier-status     | verifier-result | drat         | drat_final             | cake            |   n | unique confs | names                                                     |
|---------------------+-----------------+--------------+------------------------+-----------------+-----+--------------+-----------------------------------------------------------|
| complete            | --              | NOPROOF      | None                   | OutOfHeap       | 112 |            8 | [..]                                                      |
| complete            | --              | NOPROOF      | None                   | parse_problem   |   1 |            1 | ['SLIME__default-no-drup']                                |
| complete            | --              | NOPROOF      | None                   | timeout         | 889 |            8 | [..]                                                      |
| complete            | ERROR           | ERROR        | commentLongetThan65536 | formally_failed |   4 |            1 | ['optsat_m20__default']                                   |
| complete            | NOT_VERIFIED    | NOT_VERIFIED | Enc                    | OutOfHeap       |  22 |            2 | ['Riss__NOUNSAT_proof-fixed', 'Riss__default_proof']      |
| complete            | NOT_VERIFIED    | NOT_VERIFIED | Enc                    | formally_failed | 207 |            2 | ['Riss__NOUNSAT_proof-fixed', 'Riss__default_proof']      |
| complete            | NOT_VERIFIED    | NOT_VERIFIED | None                   | formally_failed |   1 |            1 | ['optsat_m20__default']                                   |
| complete            | NOT_VERIFIED    | NOT_VERIFIED | RATcfoapp              | formally_failed |  55 |            2 | ['glucose-3.0-inprocess__default', 'optsat_m20__default'] |
| complete            | NOT_VERIFIED    | NOT_VERIFIED | ccbnd                  | formally_failed |   2 |            1 | ['optsat_m20__default']                                   |
| timeout (cpu)       | --              | None         | None                   | None            |  15 |           11 | [..]                                                      |
| timeout (wallclock) | --              | None         | None                   | None            |  75 |           33 | [..]                                                      |
* pandas
#+begin_src python :results output raw
<<imports>>
d = pd.read_csv("results.csv")

d['n'] = d['solver'] + '__' + d['configuration'] # confs
d = d[d['result'].isin(['SAT', 'UNSAT'])]

# remove disqualified
f = d[d['verifier-result'].isin(['SAT-INCORRECT', 'UNSAT-INCORRECT',])]['n'].unique()
d = d[~d['n'].isin(f)]

# I understand those
d = d[~(d['verifier-result'].isin(['SAT-VERIFIED', 'UNSAT-VERIFIED',]))]

d = d[['verifier-status', 'verifier-result', 'drat', 'drat_final', 'cake', 'n']]
d = d.drop_duplicates() # remove to count instances and not confs
d = d.groupby(['verifier-status', 'verifier-result', 'drat', 'drat_final', 'cake'])
d = d.count().reset_index()
# d = d.agg(list).reset_index()
org(d, True)
#+end_src