Edit on GitHub

pytact.scripts.analyze_oracle

Script used to analyze which proofs the oracle was unable to reproduce and why.

 1"""Script used to analyze which proofs the oracle was unable to reproduce and
 2why."""
 3
 4from pathlib import Path
 5import sys
 6from pytact.data_reader import data_reader, Original
 7
 8def main():
 9    benchfile = sys.argv[2]
10    unsolved_bench = set()
11    with open(benchfile, 'r') as f:
12        for line in f.readlines():
13            spl = line.split('\t')
14            if len(spl) <= 3:
15                unsolved_bench.add(spl[1])
16
17    dataset_path = Path(sys.argv[1]).resolve()
18    with data_reader(dataset_path) as data:
19        for datafile in data.values():
20            if datafile.filename.parts[0] != 'coq-tactician-stdlib.dev':
21                continue
22            for d in datafile.definitions():
23                if not isinstance(d.status, Original):
24                    continue
25                if not d.name in unsolved_bench:
26                    continue
27                if proof := d.proof:
28
29                    unknown = False
30                    for step in proof:
31                        if step.tactic is None:
32                            unknown = True
33                    if unknown:
34                        continue
35
36                    arg_unknown = False
37                    for step in proof:
38                        for outcome in step.outcomes:
39                            for arg in outcome.tactic_arguments:
40                                if arg is None:
41                                    arg_unknown = True
42                    if arg_unknown:
43                        continue
44
45                    term = False
46                    for step in proof:
47                        if step.tactic.text != step.tactic.interm_text:
48                            term = True
49                    if term:
50                        continue
51
52                    tactics = { step.tactic.ident for step in proof }
53                    for ancestor in d.global_context():
54                        if a_proof := ancestor.proof:
55                            for step in a_proof:
56                                if step.tactic is not None:
57                                    tactics.discard(step.tactic.ident)
58                    if tactics:
59                        continue
60
61                    count = 0
62                    for step in proof:
63                        for outcome in step.outcomes:
64                            count += 1
65                    print(f"{count}\t{d.name}")
66
67if __name__ == "__main__":
68    exit(main())
def main(): 
 9def main():
10    benchfile = sys.argv[2]
11    unsolved_bench = set()
12    with open(benchfile, 'r') as f:
13        for line in f.readlines():
14            spl = line.split('\t')
15            if len(spl) <= 3:
16                unsolved_bench.add(spl[1])
17
18    dataset_path = Path(sys.argv[1]).resolve()
19    with data_reader(dataset_path) as data:
20        for datafile in data.values():
21            if datafile.filename.parts[0] != 'coq-tactician-stdlib.dev':
22                continue
23            for d in datafile.definitions():
24                if not isinstance(d.status, Original):
25                    continue
26                if not d.name in unsolved_bench:
27                    continue
28                if proof := d.proof:
29
30                    unknown = False
31                    for step in proof:
32                        if step.tactic is None:
33                            unknown = True
34                    if unknown:
35                        continue
36
37                    arg_unknown = False
38                    for step in proof:
39                        for outcome in step.outcomes:
40                            for arg in outcome.tactic_arguments:
41                                if arg is None:
42                                    arg_unknown = True
43                    if arg_unknown:
44                        continue
45
46                    term = False
47                    for step in proof:
48                        if step.tactic.text != step.tactic.interm_text:
49                            term = True
50                    if term:
51                        continue
52
53                    tactics = { step.tactic.ident for step in proof }
54                    for ancestor in d.global_context():
55                        if a_proof := ancestor.proof:
56                            for step in a_proof:
57                                if step.tactic is not None:
58                                    tactics.discard(step.tactic.ident)
59                    if tactics:
60                        continue
61
62                    count = 0
63                    for step in proof:
64                        for outcome in step.outcomes:
65                            count += 1
66                    print(f"{count}\t{d.name}")