diff --git a/AutoFormalization/proof/autoformalize.py b/AutoFormalization/proof/autoformalize.py index d435532..4238ab6 100644 --- a/AutoFormalization/proof/autoformalize.py +++ b/AutoFormalization/proof/autoformalize.py @@ -10,7 +10,9 @@ def preceding_propositions(idx): - with open("AutoFormalization/proof/book_propositions.json", "r", encoding="utf-8") as f: + with open( + "AutoFormalization/proof/book_propositions.json", "r", encoding="utf-8" + ) as f: propositions = json.load(f) pre_props = [] for i in range(1, idx): diff --git a/AutoFormalization/statement/evaluate.py b/AutoFormalization/statement/evaluate.py index a54417e..2a6ed68 100644 --- a/AutoFormalization/statement/evaluate.py +++ b/AutoFormalization/statement/evaluate.py @@ -6,6 +6,7 @@ from E3.checker import Checker from E3.utils import ROOT_DIR + def main(): parser = argparse.ArgumentParser() parser.add_argument( @@ -32,14 +33,9 @@ def main(): ) parser.add_argument( "--mode", - choices=[ - "bvars", - "skipApprox", - "onlyApprox", - "full" - ], + choices=["bvars", "skipApprox", "onlyApprox", "full"], default="skipApprox", - help="E3 checker mode" + help="E3 checker mode", ) parser.add_argument( "--reasoning", @@ -112,7 +108,7 @@ def main(): cnt += 1 except Exception as e: print(e) - continue + continue print(f"cnt: {cnt}, tot: {tot}, acc: {(cnt/tot)*100:.2f}%") diff --git a/E3/Engine/choosePerms.py b/E3/Engine/choosePerms.py index b5f44ac..a56a0b3 100644 --- a/E3/Engine/choosePerms.py +++ b/E3/Engine/choosePerms.py @@ -6,13 +6,16 @@ from dataclasses import dataclass, field from collections import Counter + def is_permutation(list1, list2): return Counter(list1) == Counter(list2) + SHORTCIRCUIT_THRESHOLD = 4000000 SHORTCIRCUIT_SAMPLE_THRESHOLD = 0.88 SHORTCIRCUIT_SAMPLE_CUTOFF = 50 + class QuantifierData: points: list[str] lines: list[str] @@ -23,8 +26,14 @@ def __init__(self, points, lines, circles): self.lines = lines self.circles = circles -def has_permutation(x:QuantifierData,y:QuantifierData): - return is_permutation(x.points, y.points) and is_permutation(x.lines, y.lines) and is_permutation (x.circles, y.circles) + +def has_permutation(x: QuantifierData, y: QuantifierData): + return ( + is_permutation(x.points, y.points) + and is_permutation(x.lines, y.lines) + and is_permutation(x.circles, y.circles) + ) + class PropData: univNames: QuantifierData @@ -33,12 +42,22 @@ class PropData: def __init__(self, univNames, existNames): self.univNames = univNames self.existNames = existNames - - def asList(self): - return self.univNames.points + self.univNames.lines + self.univNames.circles + self.existNames.points + self.existNames.lines + self.existNames.circles -def has_match(x : PropData, y : PropData): - return has_permutation(x.univNames,y.univNames) and has_permutation(x.existNames, y.existNames) + def asList(self): + return ( + self.univNames.points + + self.univNames.lines + + self.univNames.circles + + self.existNames.points + + self.existNames.lines + + self.existNames.circles + ) + + +def has_match(x: PropData, y: PropData): + return has_permutation(x.univNames, y.univNames) and has_permutation( + x.existNames, y.existNames + ) class PermutationStruct: @@ -75,7 +94,7 @@ class NameMap: sim: float def __eq__(self, other) -> bool: - self.name==other.name + self.name == other.name def readNames(data): @@ -115,7 +134,8 @@ def checkPerm(names, target, reference, guarded): def checkAndInsert(heap, name, N): - if name in heap: return () + if name in heap: + return () if len(heap) < N: heapq.heappush(heap, name) else: @@ -155,24 +175,30 @@ def choosePermutations( nonempty_names = [] - - if not univ.noPoints(): nonempty_names+=[univ.pointPerms] - if not univ.noLines(): nonempty_names+=[univ.linePerms] - if not univ.noCircles(): nonempty_names+=[univ.circlePerms] - if not exist.noPoints(): nonempty_names+=[exist.pointPerms] - if not exist.noLines(): nonempty_names+=[exist.linePerms] - if not exist.noCircles(): nonempty_names+=[exist.circlePerms] - + if not univ.noPoints(): + nonempty_names += [univ.pointPerms] + if not univ.noLines(): + nonempty_names += [univ.linePerms] + if not univ.noCircles(): + nonempty_names += [univ.circlePerms] + if not exist.noPoints(): + nonempty_names += [exist.pointPerms] + if not exist.noLines(): + nonempty_names += [exist.linePerms] + if not exist.noCircles(): + nonempty_names += [exist.circlePerms] ceiling = 1 for x in nonempty_names: ceiling *= ceiling * len(x) - if ceiling > SHORTCIRCUIT_THRESHOLD : + if ceiling > SHORTCIRCUIT_THRESHOLD: short_circuiting = True - if has_match(ground,remove_all_guards(test)): + if has_match(ground, remove_all_guards(test)): print("match found") - sim = checkPerm(ground.asList(), target, reference, replaceGuards(ground.asList())) + sim = checkPerm( + ground.asList(), target, reference, replaceGuards(ground.asList()) + ) checkAndInsert(permHeap, NameMap(ground.asList(), sim), N) for uPoints, uLines, uCircles, ePoints, eLines, eCircles in allCombs: @@ -180,9 +206,9 @@ def choosePermutations( sim = checkPerm(asList, target, reference, perm) x = NameMap(perm, sim) checkAndInsert(permHeap, x, N) - if (short_circuiting and sim > SHORTCIRCUIT_SAMPLE_THRESHOLD): + if short_circuiting and sim > SHORTCIRCUIT_SAMPLE_THRESHOLD: seen_sc += 1 - if (short_circuiting and seen_sc >= SHORTCIRCUIT_SAMPLE_CUTOFF): + if short_circuiting and seen_sc >= SHORTCIRCUIT_SAMPLE_CUTOFF: return permHeap, asList return permHeap, asList @@ -190,13 +216,24 @@ def choosePermutations( def removeGuards(data): return list(map(lambda x: x.replace("grd_", ""), data)) + def replaceGuards(data): - return list(map(lambda x : "grd_"+x,data)) + return list(map(lambda x: "grd_" + x, data)) + def remove_all_guards(x: PropData): - univ = QuantifierData(removeGuards(x.univNames.points), removeGuards(x.univNames.lines), removeGuards(x.univNames.circles)) - exist = QuantifierData(removeGuards(x.existNames.points), removeGuards(x.existNames.lines), removeGuards(x.existNames.circles)) - return PropData(univ,exist) + univ = QuantifierData( + removeGuards(x.univNames.points), + removeGuards(x.univNames.lines), + removeGuards(x.univNames.circles), + ) + exist = QuantifierData( + removeGuards(x.existNames.points), + removeGuards(x.existNames.lines), + removeGuards(x.existNames.circles), + ) + return PropData(univ, exist) + def main(): @@ -229,6 +266,6 @@ def main(): with open(args.outFile, "w") as file: json.dump(dict, file) + if __name__ == "__main__": main() - diff --git a/README.md b/README.md index 5e92cea..a15d6eb 100644 --- a/README.md +++ b/README.md @@ -67,6 +67,8 @@ Optionally, you can: 1. Run `lake -R -Kenv=dev build SystemE:docs` to build the documentation 1. View the auto-generated documentation locally at ./lake/build/doc, e.g., using `python -mhttp.server` +If you have problems building the project, [Dockerfile](./Dockerfile) and [scripts/build.sh](./scripts/build.sh) may serve as useful references. + ## The Formal System E diff --git a/scripts/build.sh b/scripts/build.sh index 9622d01..52c19a7 100644 --- a/scripts/build.sh +++ b/scripts/build.sh @@ -1,4 +1,5 @@ #!/bin/bash +# This script was designed to run on GitHub Codespaces. # Install elan. curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y @@ -18,6 +19,7 @@ cd ../.. pip install smt-portfolio +# Build the Lean project. lake script run check lake exe cache get lake build SystemE Book UniGeo E3 \ No newline at end of file