Edit on GitHub

pytact.scripts.lemma_size

Calculate the number of proof state refinements in each lemmas proof.

View Source

 1"""Calculate the number of proof state refinements in each lemmas proof."""
 2
 3from pathlib import Path
 4import sys
 5from pytact.data_reader import data_reader, Original
 6
 7def main():
 8    dataset_path = Path(sys.argv[1]).resolve()
 9    with data_reader(dataset_path) as data:
10        for f in data.values():
11            for d in f.definitions():
12                if not isinstance(d.status, Original):
13                    continue
14                if proof := d.proof:
15                    count = 0
16                    for step in proof:
17                        for outcome in step.outcomes:
18                            count += 1
19                    print(f"{d.name}\t{count}")
20
21if __name__ == "__main__":
22    exit(main())

def main(): View Source

 8def main():
 9    dataset_path = Path(sys.argv[1]).resolve()
10    with data_reader(dataset_path) as data:
11        for f in data.values():
12            for d in f.definitions():
13                if not isinstance(d.status, Original):
14                    continue
15                if proof := d.proof:
16                    count = 0
17                    for step in proof:
18                        for outcome in step.outcomes:
19                            count += 1
20                    print(f"{d.name}\t{count}")