From faf6af02db9584b529dbcd07191a5ef85c29f1d7 Mon Sep 17 00:00:00 2001 From: Hao Zhang Date: Fri, 2 Jan 2026 19:49:21 +0800 Subject: [PATCH] Add kele example to ddss. feat: add relationship examples and main execution script feat: add arithmetic example and support in main.py Update the new interface. Cancel pending tasks. Update arithmetic structure to support typed literals. Refactor arithmetic with helper functions for better structure extraction. Support +, -, *, / and Int/Float types in arithmetic. Sync arithmetic support and loop optimizations to examples. Add a geometry example Add TypeScript implementation of arithmetic example. refactor: update examples main calls to match new signatures feat: add complex geometry examples 1-10 (excluding 8) Update engine name to chain. --- examples/arithmetic_example.dsp | 9 + examples/geometry_for_wo_tool_complex_1.dsp | 97 ++++++++ examples/geometry_for_wo_tool_complex_10.dsp | 68 ++++++ examples/geometry_for_wo_tool_complex_2.dsp | 45 ++++ examples/geometry_for_wo_tool_complex_3.dsp | 78 ++++++ examples/geometry_for_wo_tool_complex_4.dsp | 37 +++ examples/geometry_for_wo_tool_complex_5.dsp | 30 +++ examples/geometry_for_wo_tool_complex_6.dsp | 35 +++ examples/geometry_for_wo_tool_complex_7.dsp | 35 +++ examples/geometry_for_wo_tool_complex_8.dsp | 29 +++ examples/geometry_for_wo_tool_complex_9.dsp | 86 +++++++ examples/main.py | 200 +++++++++++++++ examples/main.ts | 241 +++++++++++++++++++ examples/relationship.dsp | 17 ++ examples/relationship_quick_start.dsp | 9 + 15 files changed, 1016 insertions(+) create mode 100644 examples/arithmetic_example.dsp create mode 100644 examples/geometry_for_wo_tool_complex_1.dsp create mode 100644 examples/geometry_for_wo_tool_complex_10.dsp create mode 100644 examples/geometry_for_wo_tool_complex_2.dsp create mode 100644 examples/geometry_for_wo_tool_complex_3.dsp create mode 100644 examples/geometry_for_wo_tool_complex_4.dsp create mode 100644 examples/geometry_for_wo_tool_complex_5.dsp create mode 100644 examples/geometry_for_wo_tool_complex_6.dsp create mode 100644 examples/geometry_for_wo_tool_complex_7.dsp create mode 100644 examples/geometry_for_wo_tool_complex_8.dsp create mode 100644 examples/geometry_for_wo_tool_complex_9.dsp create mode 100644 examples/main.py create mode 100644 examples/main.ts create mode 100644 examples/relationship.dsp create mode 100644 examples/relationship_quick_start.dsp diff --git a/examples/arithmetic_example.dsp b/examples/arithmetic_example.dsp new file mode 100644 index 0000000..916beb0 --- /dev/null +++ b/examples/arithmetic_example.dsp @@ -0,0 +1,9 @@ +// 初始事实：定义数字 1 和 2 存在 +Exist(Literal(1) :: Int) +Exist(Literal(2) :: Int) + +// 规则：如果 X 存在，Y 存在，且 X + Y = W，则 W 也存在 +Exist(Literal(`X) :: Int), Exist(Literal(`Y) :: Int), Literal(`X) :: Int + Literal(`Y) :: Int == Literal(`W) :: Int => Exist(Literal(`W) :: Int) + +// 查询：数字 5 是否存在？ +Exist(Literal(5) :: Int) => Query() diff --git a/examples/geometry_for_wo_tool_complex_1.dsp b/examples/geometry_for_wo_tool_complex_1.dsp new file mode 100644 index 0000000..01d5eb3 --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_1.dsp @@ -0,0 +1,97 @@ +// 初始事实 +Collinear(F, A, C) +Collinear(F, E, B) +Collinear(D, B, G) +Collinear(A, G, C) +Collinear(D, B, H) +Collinear(I, A, D) +Collinear(E, I, C) +Collinear(E, J, B) +Length(K, A) == Length(K, F) +Length(K, F) == Length(K, J) +Length(L, F) == Length(L, G) +Length(L, B) == Length(L, F) +Length(M, G) == Length(M, H) +Length(M, C) == Length(M, G) +Length(N, D) == Length(N, H) +Length(N, H) == Length(N, I) +Length(O, E) == Length(O, I) +Length(O, I) == Length(O, J) +Length(K, P) == Length(K, F) +Length(L, P) == Length(L, F) +Length(M, Q) == Length(M, G) +Length(L, Q) == Length(L, G) +Length(N, R) == Length(N, H) +Length(M, R) == Length(M, H) +Length(K, T) == Length(K, J) +Length(O, T) == Length(O, J) +Length(O, S) == Length(O, I) + +// R1: KA=KF & KF=KJ & KT=KJ => F,A,J,T 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P4), Length(`P1, `P5) == Length(`P1, `P4) => Cyclic(`P3, `P2, `P4, `P5) + +// R2: F,A,J,T 共圆 & KA=KF & KP=KF & KF=KJ => A,F,P,T 共圆 +Cyclic(`P1, `P2, `P3, `P4), Length(`P5, `P2) == Length(`P5, `P1), Length(`P5, `P6) == Length(`P5, `P1), Length(`P5, `P1) == Length(`P5, `P3) => Cyclic(`P2, `P1, `P6, `P4) + +// R3: ND=NH & NR=NH & NH=NI => D,I,R,H 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P5) => Cyclic(`P2, `P5, `P4, `P3) + +// R4: D,I,R,H 共圆 => ∠DHR=∠DIR +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P4, `P3) == Degree(`P1, `P2, `P3) + +// R5: MG=MH & MR=MH & MC=MG => H,C,R,G 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P2) => Cyclic(`P3, `P5, `P4, `P2) + +// R6: H,C,R,G 共圆 => ∠HGC=∠HRC +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P4, `P2) == Degree(`P1, `P3, `P2) + +// R7: I,A,D共线 & ∠DHR=∠DIR & D,B,H共线 & ∠HGC=∠HRC & D,B,G共线 & A,G,C共线 => ∠ACR=∠AIR +Collinear(`P1, `P2, `P3), Degree(`P3, `P4, `P5) == Degree(`P3, `P1, `P5), Collinear(`P3, `P6, `P4), Degree(`P4, `P7, `P8) == Degree(`P4, `P5, `P8), Collinear(`P3, `P6, `P7), Collinear(`P2, `P7, `P8) => Degree(`P2, `P8, `P5) == Degree(`P2, `P1, `P5) + +// R8: ∠ACR=∠AIR => A,I,R,C 共圆 +Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3) => Cyclic(`P1, `P4, `P3, `P2) + +// R9: OE=OI & OI=OJ & OT=OJ & OS=OI => E,I,J,T 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P4), Length(`P1, `P5) == Length(`P1, `P4), Length(`P1, `P6) == Length(`P1, `P3) => Cyclic(`P2, `P3, `P5, `P5) + +// R11: E,I,J,T 共圆 => ∠JTI=∠JEI +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P2, `P4) == Degree(`P3, `P1, `P2) + +// R12: F,A,J,T 共圆 => ∠AFJ=∠ATJ +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P2, `P1, `P3) == Degree(`P2, `P4, `P3) + +// R13: E,I,C共线 & ∠JTI=∠JEI & E,J,B共线 & ∠AFJ=∠ATJ & F,A,C共线 & F,E,B共线 => ∠CAT=∠CIT +Collinear(`P1, `P2, `P3), Degree(`P4, `P2, `P8) == Degree(`P4, `P1, `P2), Collinear(`P1, `P4, `P6), Degree(`P7, `P5, `P4) == Degree(`P7, `P8, `P4), Collinear(`P5, `P7, `P3), Collinear(`P5, `P1, `P6) => Degree(`P3, `P7, `P8) == Degree(`P3, `P2, `P8) + +// R14: ∠CAT=∠CIT => A,I,T,C 共圆 +Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3) => Cyclic(`P2, `P4, `P3, `P1) + +// R15: A,I,R,C 共圆 & A,I,T,C 共圆 => A,C,T,R 共圆 +Cyclic(`P1, `P2, `P3, `P4), Cyclic(`P1, `P2, `P5, `P4) => Cyclic(`P1, `P4, `P5, `P3) + +// R16: ∠AFP=∠ATP & F,A,C共线 & ∠CAT=∠CRT => ∠CRT=∠FPT +Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3), Collinear(`P2, `P1, `P5), Degree(`P5, `P1, `P4) == Degree(`P5, `P6, `P4) => Degree(`P5, `P6, `P4) == Degree(`P2, `P3, `P4) + +// R17: H,C,R,G 共圆 & MG=MH & MQ=MG & MC=MG => C,R,G,Q 共圆 +Cyclic(`P1, `P2, `P3, `P4), Length(`P5, `P4) == Length(`P5, `P1), Length(`P5, `P6) == Length(`P5, `P4), Length(`P5, `P2) == Length(`P5, `P4) => Cyclic(`P2, `P3, `P4, `P6) + +// R18: Q,G,C,R 共圆 => ∠QGC=∠QRC +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3) + +// R19: LP=LF & LF=LG & LQ=LG & LB=LF => F,Q,P,G 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P4), Length(`P1, `P5) == Length(`P1, `P4), Length(`P1, `P6) == Length(`P1, `P3) => Cyclic(`P3, `P5, `P2, `P4) + +// R20: F,Q,P,G 共圆 => ∠FPQ=∠FGQ +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P3, `P2) == Degree(`P1, `P4, `P2) + +// R21: ∠QGC=∠QRC & A,G,C共线 & ∠FPQ=∠FGQ & F,A,C共线 => ∠FPQ=∠CRQ +Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3), Collinear(`P6, `P2, `P3), Degree(`P5, `P7, `P1) == Degree(`P5, `P2, `P1), Collinear(`P5, `P6, `P3) => Degree(`P5, `P7, `P1) == Degree(`P3, `P4, `P1) + +// R22: ∠CRT=∠FPT & ∠FPQ=∠CRQ => ∠TPQ=∠TRQ +Degree(`P1, `P2, `P3) == Degree(`P4, `P5, `P3), Degree(`P4, `P5, `P6) == Degree(`P1, `P2, `P6) => Degree(`P3, `P5, `P6) == Degree(`P3, `P2, `P6) + +// R23: ∠TPQ=∠TRQ => Q,P,R,T 共圆 +Degree(`P3, `P5, `P6) == Degree(`P3, `P2, `P6) => Cyclic(`P6, `P5, `P2, `P3) + +// 查询：A,I,T,C 是否共圆？ +Cyclic(A, I, T, C) => Query() diff --git a/examples/geometry_for_wo_tool_complex_10.dsp b/examples/geometry_for_wo_tool_complex_10.dsp new file mode 100644 index 0000000..c778479 --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_10.dsp @@ -0,0 +1,68 @@ +// 初始事实 +Collinear(B, A, C) +Collinear(G, I, E) +Length(B, A) == Length(B, C) +Length(D, A) == Length(D, B) +Length(D, E) == Length(D, B) +Length(F, B) == Length(F, C) +Length(F, E) == Length(F, B) +Length(F, G) == Length(F, B) +Length(D, I) == Length(D, B) +Perp(A, G, A, D) + +// R1: FB = FC & FG = FB & FE = FB ⇒ F 是 △CGE 的外心 +Length(`P1, `P5) == Length(`P1, `P2), Length(`P1, `P3) == Length(`P1, `P5), Length(`P1, `P4) == Length(`P1, `P5) => Circumcenter(`P1, `P2, `P3, `P4) + +// R2: FB = FC & FG = FB & FE = FB ⇒ G,B,E,C 共圆 +Length(`P1, `P3) == Length(`P1, `P5), Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3) => Cyclic(`P2, `P3, `P4, `P5) + +// R3: G,B,E,C 共圆 ⇒ ∠ECB = ∠EGB +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P4, `P2) == Degree(`P3, `P1, `P2) + +// R4: G,B,E,C 共圆 ⇒ ∠EBC = ∠EGC +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P2, `P4) == Degree(`P3, `P1, `P4) + +// R5: DA = DB & DI = DB & DE = DB ⇒ I,B,E,A 共圆 +Length(`P1, `P5) == Length(`P1, `P3), Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3) => Cyclic(`P2, `P3, `P4, `P5) + +// R6: I,B,E,A 共圆 ⇒ ∠IEB = ∠IAB +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P3, `P2) == Degree(`P1, `P4, `P2) + +// R7: B,A,C共线 & ∠EBC = ∠EGC & ∠IEB = ∠IAB & G,I,E共线 ⇒ ∠BAI = ∠ACG +Collinear(`P1, `P2, `P3), Degree(`P4, `P1, `P3) == Degree(`P4, `P5, `P3), Degree(`P6, `P4, `P1) == Degree(`P6, `P2, `P1), Collinear(`P5, `P6, `P4) => Degree(`P1, `P2, `P6) == Degree(`P2, `P3, `P5) + +// R8: DA = DB & DI = DB ⇒ D 是 △ABI 的外心 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3) => Circumcenter(`P1, `P2, `P3, `P4) + +// R9: D是△ABI的外心 & AG ⟂ AD ⇒ ∠BAG = ∠BIA +Circumcenter(`P1, `P2, `P3, `P4), Perp(`P2, `P5, `P2, `P1) => Degree(`P3, `P2, `P5) == Degree(`P3, `P4, `P2) + +// R10: B,A,C 共线 & ∠BIA = ∠BAG ⇒ ∠BIA = ∠CAG +Collinear(`P1, `P2, `P3), Degree(`P1, `P4, `P2) == Degree(`P1, `P2, `P5) => Degree(`P1, `P4, `P2) == Degree(`P3, `P2, `P5) + +// R11: ∠BAI = ∠ACG & ∠BIA = ∠CAG => AB:CG = AI:CA +Degree(`P1, `P2, `P4) == Degree(`P2, `P3, `P5), Degree(`P1, `P4, `P2) == Degree(`P3, `P2, `P5) => Ratio(`P2, `P1, `P3, `P5) == Ratio(`P2, `P4, `P3, `P2) + +// R12: AB:CG = AI:CA & BA = BC => BC:GC = IA:CA +Ratio(`P2, `P1, `P3, `P5) == Ratio(`P2, `P4, `P3, `P2), Length(`P1, `P2) == Length(`P1, `P3) => Ratio(`P1, `P3, `P5, `P3) == Ratio(`P4, `P2, `P3, `P2) + +// R13: B,A,C 共线 & ∠EBC = ∠EGC & ∠IEB = ∠IAB & G,I,E 共线 => ∠BCG = ∠CAI +Collinear(`P1, `P2, `P3), Degree(`P6, `P1, `P3) == Degree(`P6, `P5, `P3), Degree(`P4, `P6, `P1) == Degree(`P4, `P2, `P1), Collinear(`P5, `P4, `P6) => Degree(`P1, `P3, `P5) == Degree(`P3, `P2, `P4) + +// R14: BC:GC = IA:CA & ∠BCG = ∠CAI => ∠CBG = ∠CIA +Ratio(`P1, `P3, `P5, `P3) == Ratio(`P4, `P2, `P3, `P2), Degree(`P1, `P3, `P5) == Degree(`P3, `P2, `P4) => Degree(`P3, `P1, `P5) == Degree(`P3, `P4, `P2) + +// R15: B,A,C 共线 & ∠EBC = ∠EGC & ∠IEB = ∠IAB & G,I,E 共线 => ∠(IA-BC) = ∠GCB +Collinear(`P1, `P2, `P3), Degree(`P6, `P1, `P3) == Degree(`P6, `P5, `P3), Degree(`P4, `P6, `P1) == Degree(`P4, `P2, `P1), Collinear(`P5, `P4, `P6) => Angle(`P4, `P2, `P1, `P3) == Degree(`P5, `P3, `P1) + +// R16: ∠(IA-BC) = ∠GCB => IA ∥ GC +Angle(`P4, `P2, `P1, `P3) == Degree(`P5, `P3, `P1) => Para(`P4, `P2, `P5, `P3) + +// R17: ∠ECB = ∠EGB & B,A,C 共线 & ∠CBG = ∠CIA & IA ∥ CG => ∠ICG = ∠CEG +Degree(`P6, `P3, `P1) == Degree(`P6, `P5, `P1), Collinear(`P1, `P2, `P3), Degree(`P3, `P1, `P5) == Degree(`P3, `P4, `P2), Para(`P4, `P2, `P5, `P3) => Degree(`P4, `P3, `P5) == Degree(`P3, `P6, `P5) + +// R18: F is the circumcenter of CGE & ∠ICG = ∠CEG ⇒ CF ⟂ CI +Circumcenter(`P1, `P2, `P3, `P4), Degree(`P5, `P2, `P3) == Degree(`P2, `P4, `P3) => Perp(`P2, `P1, `P2, `P5) + +// 查询：CF ⟂ CI？ +Perp(C, F, C, I) => Query() diff --git a/examples/geometry_for_wo_tool_complex_2.dsp b/examples/geometry_for_wo_tool_complex_2.dsp new file mode 100644 index 0000000..f05cff5 --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_2.dsp @@ -0,0 +1,45 @@ +// 初始事实 +Collinear(B, C, A) +Collinear(B, D, F) +Collinear(E, A, G) +Collinear(C, G, F) +Collinear(B, E, H) +Collinear(C, H, F) +Collinear(C, I, F) +Collinear(D, I, A) +Para(A, E, B, D) +Para(B, E, A, D) +Length(C, A) == Length(C, B) + +// R1: B,D,F 共线 & E,A,G 共线 & AE ∥ BD => DF ∥ AG +Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P6), Para(`P5, `P4, `P1, `P2) => Para(`P2, `P3, `P5, `P6) + +// R2: C,I,F 共线 & C,G,F 共线 => I,F,G 共线 +Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3) => Collinear(`P2, `P3, `P4) + +// R3: DF ∥ AG & I,F,G 共线 & D,I,A 共线 => IF/IG = FD/GA +Para(`P1, `P2, `P3, `P4), Collinear(`P5, `P2, `P4), Collinear(`P1, `P5, `P3) => Ratio(`P5, `P2, `P5, `P4) == Ratio(`P2, `P1, `P4, `P3) + +// R4: B,D,F 共线 & E,A,G 共线 & AE ∥ BD => BF ∥ AG +Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P6), Para(`P5, `P4, `P1, `P2) => Para(`P1, `P3, `P5, `P6) + +// R5: BF ∥ AG & B,C,A 共线 & C,G,F 共线 => CB/CA = BF/AG +Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P5, `P3), Collinear(`P5, `P4, `P2) => Ratio(`P5, `P1, `P5, `P3) == Ratio(`P1, `P2, `P3, `P4) + +// R6: B,E,H 共线 & D,I,A 共线 & BE ∥ AD => BH ∥ DI +Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P6), Para(`P1, `P2, `P6, `P4) => Para(`P1, `P3, `P4, `P5) + +// R7: C,I,F 共线 & C,H,F 共线 => F,H,I 共线 +Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3) => Collinear(`P3, `P4, `P2) + +// R8: BH ∥ DI & B,D,F 共线 & F,H,I 共线 => BF/DF = HF/IF +Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P3, `P5), Collinear(`P5, `P2, `P4) => Ratio(`P1, `P5, `P3, `P5) == Ratio(`P2, `P5, `P4, `P5) + +// R9: IF:IG=FD:GA & CB:CA=BF:AG & CA=CB & BF:DF=HF:IF => HF:IF=IG:IF +Ratio(`P1, `P2, `P1, `P3) == Ratio(`P2, `P4, `P3, `P5), Ratio(`P6, `P7, `P6, `P5) == Ratio(`P7, `P2, `P5, `P3), Length(`P6, `P5) == Length(`P6, `P7), Ratio(`P7, `P2, `P4, `P2) == Ratio(`P8, `P2, `P1, `P2) => Ratio(`P8, `P2, `P1, `P2) == Ratio(`P1, `P3, `P1, `P2) + +// R10: HF:IF = IG:IF => HF = IG +Ratio(`P1, `P2, `P3, `P2) == Ratio(`P3, `P4, `P3, `P2) => Length(`P1, `P2) == Length(`P3, `P4) + +// 查询：HF 是否等于 IG？ +Length(H, F) == Length(I, G) => Query() diff --git a/examples/geometry_for_wo_tool_complex_3.dsp b/examples/geometry_for_wo_tool_complex_3.dsp new file mode 100644 index 0000000..62624e4 --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_3.dsp @@ -0,0 +1,78 @@ +// 初始事实 +Collinear(B, E, C) +Collinear(A, D, E) +Collinear(A, F, C) +Collinear(B, D, F) +Collinear(B, I, C) +Collinear(A, G, B) +Collinear(G, D, C) +Collinear(A, H, C) +Collinear(D, I, C) +Collinear(B, J, F) +Para(B, H, E, F) +Para(E, I, A, B) +Para(J, E, A, C) +Intro(A) +Intro(B) +Intro(C) +Intro(D) +Intro(E) +Intro(F) +Intro(G) +Intro(H) +Intro(I) +Intro(J) + +// R1: A,B,G 共线 & EI ∥ AB => BG ∥ EI +Collinear(`P1, `P3, `P2), Para(`P4, `P5, `P1, `P2) => Para(`P2, `P3, `P4, `P5) + +// R2: D,I,C 共线 & G,D,C 共线 => C,G,I 共线 +Collinear(`P1, `P2, `P3), Collinear(`P4, `P1, `P3) => Collinear(`P3, `P4, `P2) + +// R3: D,I,C 共线 & G,D,C 共线 => D,G,I 共线 +Collinear(`P1, `P2, `P3), Collinear(`P4, `P1, `P3) => Collinear(`P1, `P4, `P2) + +// R4: BG ∥ EI & B,E,C 共线 & C,G,I 共线 => BC:EC = BG:IE +Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P3, `P5), Collinear(`P5, `P2, `P4) => Ratio(`P1, `P5, `P3, `P5) == Ratio(`P1, `P2, `P4, `P3) + +// R5: A,H,C 共线 & A,F,C 共线 => C,H,F 共线 +Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3) => Collinear(`P3, `P2, `P4) + +// R6: BH ∥ EF & B,E,C 共线 & C,H,F 共线 => BC:EC = BH:EF +Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P3, `P5), Collinear(`P5, `P2, `P4) => Ratio(`P1, `P5, `P3, `P5) == Ratio(`P1, `P2, `P3, `P4) + +// R7: A,H,C 共线 & A,F,C 共线 & BH ∥ EF & AC ∥ EJ => ∠BHF = ∠FEJ +Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3), Para(`P5, `P2, `P6, `P4), Para(`P7, `P6, `P1, `P3) => Degree(`P5, `P2, `P4) == Degree(`P4, `P6, `P7) + +// R8: B,D,F 共线 & A,H,C 共线 & A,F,C 共线 & B,J,F 共线 & AC ∥ EJ => ∠BFH = ∠FJE +Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P6), Collinear(`P4, `P3, `P6), Collinear(`P1, `P7, `P3), Para(`P7, `P8, `P4, `P6) => Degree(`P1, `P3, `P5) == Degree(`P3, `P7, `P8) + +// R9: ∠BHF = ∠FEJ & ∠BFH = ∠FJE => BH:EF = HF:JE +Degree(`P1, `P2, `P3) == Degree(`P3, `P4, `P5), Degree(`P1, `P3, `P2) == Degree(`P3, `P5, `P4) => Ratio(`P1, `P2, `P4, `P3) == Ratio(`P2, `P3, `P5, `P4) + +// R10: 传递性推导 +Ratio(`P1, `P2, `P3, `P2) == Ratio(`P1, `P4, `P5, `P3), Ratio(`P1, `P2, `P3, `P2) == Ratio(`P1, `P6, `P3, `P7), Ratio(`P1, `P6, `P3, `P7) == Ratio(`P6, `P7, `P8, `P3) => Ratio(`P6, `P7, `P8, `P3) == Ratio(`P1, `P4, `P5, `P3) + +// R11: A,G,B 共线 & EI ∥ AB => AG ∥ EI +Collinear(`P1, `P2, `P3), Para(`P4, `P5, `P1, `P3) => Para(`P1, `P2, `P4, `P5) + +// R12: AG ∥ EI & A,D,E 共线 & G,D,I 共线 => DE:AD = IE:AG +Para(`P1, `P2, `P3, `P4), Collinear(`P1, `P5, `P3), Collinear(`P2, `P5, `P4) => Ratio(`P5, `P3, `P1, `P5) == Ratio(`P4, `P3, `P1, `P2) + +// R13: A,C,F 共线 & EJ ∥ AC => JE ∥ FA +Collinear(`P1, `P3, `P2), Para(`P4, `P5, `P1, `P2) => Para(`P4, `P5, `P3, `P1) + +// R14: B,J,F 共线 & B,D,F 共线 => D,J,F 共线 +Collinear(`P1, `P2, `P3), Collinear(`P1, `P4, `P3) => Collinear(`P4, `P2, `P3) + +// R15: JE ∥ FA & A,D,E 共线 & D,J,F 共线 => DE:AD = JE:AF +Para(`P1, `P2, `P3, `P4), Collinear(`P4, `P5, `P2), Collinear(`P5, `P1, `P3) => Ratio(`P5, `P2, `P4, `P5) == Ratio(`P1, `P2, `P4, `P3) + +// R16: 传递性推导 +Ratio(`P1, `P2, `P3, `P1) == Ratio(`P4, `P2, `P3, `P5), Ratio(`P1, `P2, `P3, `P1) == Ratio(`P6, `P2, `P3, `P7) => Ratio(`P6, `P2, `P3, `P7) == Ratio(`P4, `P2, `P3, `P5) + +// R17: 传递性推导 +Ratio(`P1, `P2, `P3, `P4) == Ratio(`P5, `P6, `P7, `P4), Ratio(`P3, `P4, `P8, `P2) == Ratio(`P7, `P4, `P8, `P6) => Ratio(`P1, `P2, `P8, `P2) == Ratio(`P5, `P6, `P8, `P6) + +// 查询：HF/AF = BG/AG ? +Ratio(H, F, A, F) == Ratio(B, G, A, G) => Query() diff --git a/examples/geometry_for_wo_tool_complex_4.dsp b/examples/geometry_for_wo_tool_complex_4.dsp new file mode 100644 index 0000000..ec4a568 --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_4.dsp @@ -0,0 +1,37 @@ +// 初始事实 +Collinear(A, B, E) +Collinear(G, C, E) +Collinear(G, A, D) +Collinear(H, C, E) +Perp(B, C, A, D) +Perp(C, E, A, B) +Length(F, A) == Length(F, C) +Length(F, A) == Length(F, B) +Length(F, H) == Length(F, C) + +// R1: G,C,E 共线 & A,B,E 共线 & H,C,E 共线 & CE ⟂ AB ⇒ ∠GEA = ∠AEH +Collinear(`P1, `P2, `P3), Collinear(`P4, `P5, `P3), Collinear(`P6, `P2, `P3), Perp(`P2, `P3, `P4, `P5) => Degree(`P1, `P3, `P4) == Degree(`P4, `P3, `P6) + +// R2: FA = FC & FH = FC & FA = FB ⇒ H,A,B,C 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P2) == Length(`P1, `P5) => Cyclic(`P4, `P2, `P5, `P3) + +// R3: H,A,B,C 共圆 ⇒ ∠HAB = ∠HCB +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3) + +// R4: G,A,D 共线 & BC ⟂ AD ⇒ CB ⟂ GA +Collinear(`P1, `P2, `P3), Perp(`P4, `P5, `P2, `P3) => Perp(`P5, `P4, `P1, `P2) + +// R5: H,C,E 共线 & G,C,E 共线 & CE ⟂ AB ⇒ AB ⟂ GH +Collinear(`P1, `P2, `P3), Collinear(`P4, `P2, `P3), Perp(`P2, `P3, `P5, `P6) => Perp(`P5, `P6, `P4, `P1) + +// R6: CB ⟂ GA & AB ⟂ GH ⇒ ∠(CB-GH) = ∠GAB +Perp(`P1, `P2, `P3, `P4), Perp(`P4, `P2, `P3, `P5) => Angle(`P1, `P2, `P3, `P5) == Degree(`P3, `P4, `P2) + +// R7: G,A,D共线 & A,B,E共线 & ∠HAB=∠HCB & H,C,E共线 & ∠(CB-GH)=∠GAB & G,C,E共线 ⇒ ∠GAE=∠EAH +Collinear(`P1, `P2, `P3), Collinear(`P2, `P4, `P5), Degree(`P6, `P2, `P4) == Degree(`P6, `P7, `P4), Collinear(`P6, `P7, `P5), Angle(`P7, `P4, `P1, `P6) == Degree(`P1, `P2, `P4), Collinear(`P1, `P7, `P5) => Degree(`P1, `P2, `P5) == Degree(`P6, `P2, `P5) + +// R8: ∠GEA = ∠AEH & ∠GAE = ∠EAH ⇒ EG = EH +Degree(`P1, `P2, `P3) == Degree(`P4, `P2, `P3), Degree(`P1, `P3, `P2) == Degree(`P4, `P3, `P2) => Length(`P2, `P1) == Length(`P2, `P4) + +// 查询：EG 是否等于 EH？ +Length(E, G) == Length(E, H) => Query() diff --git a/examples/geometry_for_wo_tool_complex_5.dsp b/examples/geometry_for_wo_tool_complex_5.dsp new file mode 100644 index 0000000..42f21c4 --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_5.dsp @@ -0,0 +1,30 @@ +// 初始事实 +Collinear(D, F, C) +Collinear(F, B, E) +Perp(F, H, F, G) +Length(A, C) == Length(A, B) +Length(A, D) == Length(A, B) +Length(A, E) == Length(A, B) +Length(G, F) == Length(G, B) +Length(G, D) == Length(G, F) + +// 规则 R1: AD=AB, AE=AB, AC=AB => D,B,E,C 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P3) => Cyclic(`P2, `P3, `P4, `P5) + +// 规则 R2: 四点共圆 => 圆周角相等 ∠EBD = ∠ECD +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P2, `P1) == Degree(`P3, `P4, `P1) + +// 规则 R3: GF=GB, GD=GF => G 是 △FBD 的外心 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2) => Circumcenter(`P1, `P2, `P3, `P4) + +// 规则 R4: 外心 + 垂直关系 => 弦切角性质 ∠HFB = ∠FDB +Circumcenter(`P1, `P2, `P3, `P4), Perp(`P2, `P5, `P2, `P1) => Degree(`P5, `P2, `P3) == Degree(`P2, `P4, `P3) + +// 规则 R5: 综合共线与角度相等推导角度关系 ∠HFD = Angle(EC, DF) +Collinear(`P1, `P2, `P3), Degree(`P4, `P5, `P1) == Degree(`P4, `P3, `P1), Degree(`P6, `P2, `P5) == Degree(`P2, `P1, `P5), Collinear(`P2, `P5, `P4) => Degree(`P6, `P2, `P1) == Angle(`P4, `P3, `P1, `P2) + +// 规则 R6: 角度相等 => FH ∥ EC +Degree(`P1, `P2, `P3) == Angle(`P4, `P5, `P3, `P2) => Para(`P2, `P1, `P4, `P5) + +// 查询：FH 是否平行于 EC？ +Para(F, H, E, C) => Query() diff --git a/examples/geometry_for_wo_tool_complex_6.dsp b/examples/geometry_for_wo_tool_complex_6.dsp new file mode 100644 index 0000000..3b3ef49 --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_6.dsp @@ -0,0 +1,35 @@ +// 初始事实 +Collinear(F, A, C) +Collinear(F, B, E) +Collinear(A, G, B) +Collinear(G, H, E) +Perp(E, F, A, C) +Perp(E, G, A, B) +Length(D, A) == Length(D, B) +Length(D, B) == Length(D, C) +Length(D, E) == Length(D, A) +Length(D, H) == Length(D, E) + +// R1: A,G,B共线 & F,A,C共线 & EF⟂AC & EG⟂AB ⇒ ∠EGA = ∠EFA +Collinear(`P1, `P2, `P3), Collinear(`P4, `P1, `P5), Perp(`P6, `P4, `P1, `P5), Perp(`P6, `P2, `P1, `P3) => Degree(`P6, `P2, `P1) == Degree(`P6, `P4, `P1) + +// R2: ∠EGA = ∠EFA ⇒ F,A,G,E 共圆 +Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3) => Cyclic(`P4, `P3, `P2, `P1) + +// R3: F,A,G,E 共圆 ⇒ ∠FAE = ∠FGE +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P2, `P4) == Degree(`P1, `P3, `P4) + +// R4: DA=DB & DE=DA & DH=DE & DB=DC ⇒ A,C,H,E 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2), Length(`P1, `P5) == Length(`P1, `P4), Length(`P1, `P3) == Length(`P1, `P6) => Cyclic(`P2, `P6, `P5, `P4) + +// R5: A,C,H,E 共圆 ⇒ ∠ACH = ∠AEH +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3) + +// R6: G,H,E共线 & ∠FAE=∠FGE & F,A,C共线 & ∠ACH=∠AEH ⇒ ∠CHG=∠FGH +Collinear(`P1, `P2, `P3), Degree(`P4, `P5, `P3) == Degree(`P4, `P1, `P3), Collinear(`P4, `P5, `P6), Degree(`P5, `P6, `P2) == Degree(`P5, `P3, `P2) => Degree(`P6, `P2, `P1) == Degree(`P4, `P1, `P2) + +// R7: ∠CHG = ∠FGH ⇒ HC ∥ FG +Degree(`P1, `P2, `P3) == Degree(`P4, `P3, `P2) => Para(`P2, `P1, `P4, `P3) + +// 查询：HC 是否平行于 FG？ +Para(H, C, F, G) => Query() diff --git a/examples/geometry_for_wo_tool_complex_7.dsp b/examples/geometry_for_wo_tool_complex_7.dsp new file mode 100644 index 0000000..482adb5 --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_7.dsp @@ -0,0 +1,35 @@ +// 初始事实 +Para(E, D, B, C) +Para(G, D, C, F) +Length(A, C) == Length(A, B) +Length(A, D) == Length(A, B) +Length(A, E) == Length(A, B) +Length(A, F) == Length(A, B) +Length(A, G) == Length(A, B) + +// R1: AD = AB & AF = AB & AE = AB & AC = AB ⇒ F,D,E,C 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P3), Length(`P1, `P6) == Length(`P1, `P3) => Cyclic(`P4, `P2, `P5, `P6) + +// R2: AF=AB & AG=AB & AE=AB & AD=AB & AC=AB ⇒ G,E,B,C 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P3), Length(`P1, `P6) == Length(`P1, `P3), Length(`P1, `P7) == Length(`P1, `P3) => Cyclic(`P4, `P5, `P3, `P7) + +// R3: G,E,B,C 共圆 ⇒ ∠BGE = ∠BCE +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P3, `P1, `P2) == Degree(`P3, `P4, `P2) + +// R4: F,D,E,C 共圆 ⇒ ∠DFC = ∠DEC +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P2, `P1, `P4) == Degree(`P2, `P3, `P4) + +// R5: AF=AB & AG=AB & AE=AB & AD=AB & AC=AB ⇒ G,F,D,E 共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P5) == Length(`P1, `P3), Length(`P1, `P6) == Length(`P1, `P3), Length(`P1, `P7) == Length(`P1, `P3) => Cyclic(`P4, `P2, `P6, `P5) + +// R6: G,F,D,E 共圆 ⇒ ∠GDF = ∠GEF +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P1, `P3, `P2) == Degree(`P1, `P4, `P2) + +// R7: ∠BGE=∠BCE & ∠DFC=∠DEC & DE∥BC & ∠GDF=∠GEF & DG∥CF ⇒ ∠FEG = ∠BGE +Degree(`P1, `P2, `P3) == Degree(`P1, `P4, `P3), Degree(`P5, `P6, `P4) == Degree(`P5, `P3, `P4), Para(`P5, `P3, `P1, `P4), Degree(`P2, `P5, `P6) == Degree(`P2, `P3, `P6), Para(`P5, `P2, `P4, `P6) => Degree(`P6, `P3, `P2) == Degree(`P1, `P2, `P3) + +// R8: ∠FEG = ∠BGE ⇒ FE ∥ GB +Degree(`P1, `P2, `P3) == Degree(`P4, `P3, `P2) => Para(`P1, `P2, `P3, `P4) + +// 查询：FE 是否平行于 GB？ +Para(F, E, G, B) => Query() diff --git a/examples/geometry_for_wo_tool_complex_8.dsp b/examples/geometry_for_wo_tool_complex_8.dsp new file mode 100644 index 0000000..fd3a737 --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_8.dsp @@ -0,0 +1,29 @@ +// 初始事实 +Collinear(D, B, H) +Length(C, A) == Length(C, B) +Length(C, D) == Length(C, A) +Length(C, F) == Length(C, A) +Length(F, C) == Length(F, D) +Length(C, G) == Length(C, A) +Length(G, C) == Length(G, D) + +// 规则 R1: 如果 CF=CA, CG=CA, CA=CB, CE=CA, CD=CA，则 B, G, F, D 四点共圆 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P3), Length(`P1, `P3) == Length(`P1, `P5), Length(`P1, `P6) == Length(`P1, `P3), Length(`P1, `P7) == Length(`P1, `P3) => Cyclic(`P5, `P4, `P2, `P7) + +// 规则 R2: 四点共圆引出的圆周角相等：∠DBG = ∠DFG +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P2, `P3, `P1) == Degree(`P2, `P4, `P1) + +// 规则 R3: 四点共圆引出的圆周角相等：∠FGD = ∠FBD +Cyclic(`P1, `P2, `P3, `P4) => Degree(`P4, `P1, `P2) == Degree(`P4, `P3, `P2) + +// 规则 R4: 通过边长相等推导：GC=GD, CG=CA, CF=CA, FC=FD => DF=DG +Length(`P1, `P2) == Length(`P1, `P3), Length(`P2, `P1) == Length(`P2, `P4), Length(`P2, `P5) == Length(`P2, `P4), Length(`P5, `P2) == Length(`P5, `P3) => Length(`P3, `P5) == Length(`P3, `P1) + +// 规则 R5: 等腰三角形推导底角相等：DF=DG => ∠DFG = ∠FGD +Length(`P1, `P2) == Length(`P1, `P3) => Degree(`P1, `P2, `P3) == Degree(`P2, `P3, `P1) + +// 规则 R6: 综合共线与角度相等推导角平分关系：∠FBH = ∠HBG +Collinear(`P1, `P2, `P3), Degree(`P1, `P2, `P4) == Degree(`P1, `P5, `P4), Degree(`P1, `P5, `P4) == Degree(`P5, `P4, `P1), Degree(`P5, `P4, `P1) == Degree(`P5, `P2, `P1) => Degree(`P5, `P2, `P3) == Degree(`P3, `P2, `P4) + +// 查询：∠FBH 是否等于 ∠HBG？ +Degree(F, B, H) == Degree(H, B, G) => Query() diff --git a/examples/geometry_for_wo_tool_complex_9.dsp b/examples/geometry_for_wo_tool_complex_9.dsp new file mode 100644 index 0000000..f8ea58a --- /dev/null +++ b/examples/geometry_for_wo_tool_complex_9.dsp @@ -0,0 +1,86 @@ +// 初始事实 +Collinear(C, F, A) +Collinear(G, B, C) +Collinear(H, D, G) +Collinear(E, H, C) +Collinear(D, F, I) +Collinear(E, C, I) +Collinear(E, C, J) +Collinear(E, K, C) +Perp(F, J, C, E) +Perp(C, E, K, G) +Length(D, B) == Length(D, C) +Length(D, A) == Length(D, B) +Length(D, E) == Length(D, A) +Length(E, A) == Length(E, B) +Length(F, C) == Length(F, A) +Length(G, C) == Length(G, B) + +// R1: DB = DC & GC = GB ⇒ BC ⟂ DG +Length(`P1, `P2) == Length(`P1, `P3), Length(`P4, `P3) == Length(`P4, `P2) => Perp(`P2, `P3, `P1, `P4) + +// R2: DB = DC & DA = DB ⇒ DA = DC +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2) => Length(`P1, `P4) == Length(`P1, `P3) + +// R3: DA = DC & FC = FA ⇒ AC ⟂ DF +Length(`P1, `P2) == Length(`P1, `P3), Length(`P4, `P3) == Length(`P4, `P2) => Perp(`P2, `P3, `P1, `P4) + +// R4: C,F,A共线 & D,F,I共线 & H,D,G共线 & G,B,C共线 & BC⟂DG & AC⟂DF ⇒ ∠CFI = ∠HGC +Collinear(`P1, `P2, `P3), Collinear(`P4, `P2, `P5), Collinear(`P6, `P4, `P7), Collinear(`P7, `P8, `P1), Perp(`P8, `P1, `P4, `P7), Perp(`P3, `P1, `P4, `P2) => Degree(`P1, `P2, `P5) == Degree(`P6, `P7, `P1) + +// R5: DA=DB & DE=DA & DB=DC ⇒ D 是 △EBC 的外心 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2), Length(`P1, `P3) == Length(`P1, `P5) => Circumcenter(`P1, `P4, `P3, `P5) + +// R6: DA=DB & DE=DA & DB=DC ⇒ D 是 △EAC 的外心 +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2), Length(`P1, `P3) == Length(`P1, `P5) => Circumcenter(`P1, `P4, `P2, `P5) + +// R7: DA=DB & DE=DA & DB=DC ⇒ DC = DE +Length(`P1, `P2) == Length(`P1, `P3), Length(`P1, `P4) == Length(`P1, `P2), Length(`P1, `P3) == Length(`P1, `P5) => Length(`P1, `P5) == Length(`P1, `P4) + +// R8: G,B,C共线 & GC=GB ⇒ G是CB的中点 +Collinear(`P1, `P2, `P3), Length(`P1, `P3) == Length(`P1, `P2) => Midpoint(`P1, `P3, `P2) + +// R9: D是△EBC的外心 & G是CB的中点 ⇒ ∠DBE = ∠(DG-CE) +Circumcenter(`P1, `P2, `P3, `P4), Midpoint(`P5, `P4, `P3) => Degree(`P1, `P3, `P2) == Angle(`P1, `P5, `P4, `P2) + +// R10: DA = DB & EA = EB ⇒ ∠DBE = ∠EAD +Length(`P1, `P2) == Length(`P1, `P3), Length(`P4, `P2) == Length(`P4, `P3) => Degree(`P1, `P3, `P4) == Degree(`P4, `P2, `P1) + +// R11: C,F,A共线 & FC=FA ⇒ F是CA的中点 +Collinear(`P1, `P2, `P3), Length(`P2, `P1) == Length(`P2, `P3) => Midpoint(`P2, `P1, `P3) + +// R12: D是△EAC的外心 & F是CA的中点 ⇒ ∠EAD = ∠(CE-DF) +Circumcenter(`P1, `P2, `P3, `P4), Midpoint(`P5, `P4, `P3) => Degree(`P2, `P3, `P1) == Angle(`P4, `P2, `P1, `P5) + +// R13: ∠CFI=∠HGC & ∠CIF=∠GHC ⇒ IC:HC = IF:HG +Degree(`P2, `P4, `P1) == Degree(`P3, `P5, `P2), Degree(`P2, `P1, `P4) == Degree(`P5, `P3, `P2) => Ratio(`P1, `P2, `P3, `P2) == Ratio(`P1, `P4, `P3, `P5) + +// R15: D,F,I共线 & DF⟂AC ⇒ IF⟂CA +Collinear(`P1, `P2, `P3), Perp(`P4, `P5, `P1, `P2) => Perp(`P3, `P2, `P5, `P4) + +// R16: F是CA的中点 & IF⟂CA ⇒ IC = IA +Midpoint(`P1, `P2, `P3), Perp(`P4, `P1, `P2, `P3) => Length(`P4, `P2) == Length(`P4, `P3) + +// R19: ∠GKH=∠IJF & ∠GHK=∠JIF ⇒ GK:FJ = GH:FI +Degree(`P1, `P2, `P3) == Degree(`P4, `P5, `P6), Degree(`P1, `P3, `P2) == Degree(`P5, `P4, `P6) => Ratio(`P1, `P2, `P6, `P5) == Ratio(`P1, `P3, `P6, `P4) + +// R21: DC = DE ⇒ ∠DCE = ∠CED +Length(`P1, `P2) == Length(`P1, `P3) => Degree(`P1, `P2, `P3) == Degree(`P2, `P3, `P1) + +// R22: E,H,C共线 & E,C,I共线 & ∠DCE=∠CED ⇒ ∠DCH = ∠IED +Collinear(`P1, `P2, `P3), Collinear(`P1, `P3, `P4), Degree(`P5, `P3, `P1) == Degree(`P3, `P1, `P5) => Degree(`P5, `P3, `P2) == Degree(`P4, `P1, `P5) + +// R23: ∠DHC=∠EID & ∠DCH=∠IED ⇒ CD:ED = CH:EI +Degree(`P1, `P2, `P3) == Degree(`P4, `P5, `P1), Degree(`P1, `P3, `P2) == Degree(`P5, `P4, `P1) => Ratio(`P3, `P1, `P4, `P1) == Ratio(`P3, `P2, `P4, `P5) + +// R25: E,H,C共线 & E,C,I共线 & ∠DEC=∠ECD ⇒ ∠DEH = ∠ICD +Collinear(`P2, `P4, `P3), Collinear(`P2, `P3, `P5), Degree(`P1, `P3, `P2) == Degree(`P3, `P2, `P1) => Degree(`P1, `P2, `P4) == Degree(`P5, `P3, `P1) + +// R26: ∠DHE=∠CID & ∠DEH=∠ICD ⇒ ED:CD = EH:CI +Degree(`P1, `P2, `P3) == Degree(`P4, `P5, `P1), Degree(`P1, `P3, `P2) == Degree(`P5, `P4, `P1) => Ratio(`P3, `P1, `P4, `P1) == Ratio(`P3, `P2, `P4, `P5) + +// R27: GK:FJ = EI:EH +Ratio(`P1, `P2, `P3, `P2) == Ratio(`P1, `P4, `P3, `P5), Length(`P1, `P2) == Length(`P1, `P6), Ratio(`P5, `P7, `P4, `P8) == Ratio(`P5, `P3, `P4, `P1), Ratio(`P2, `P9, `P10, `P9) == Ratio(`P2, `P3, `P10, `P1), Length(`P9, `P2) == Length(`P9, `P10), Ratio(`P10, `P9, `P2, `P9) == Ratio(`P10, `P3, `P2, `P1) => Ratio(`P5, `P7, `P4, `P8) == Ratio(`P10, `P1, `P10, `P3) + +// 查询：GK:FJ 是否等于 EI:EH +Ratio(G, K, F, J) == Ratio(E, I, E, H) => Query() diff --git a/examples/main.py b/examples/main.py new file mode 100644 index 0000000..6f44048 --- /dev/null +++ b/examples/main.py @@ -0,0 +1,200 @@ +import sys +import asyncio +import tempfile +import pathlib +from sqlalchemy import select +from apyds import Rule, List, Variable, Term, Item +from apyds_bnf import parse, unparse +from ddss.orm import initialize_database, insert_or_ignore, Facts, Ideas +from ddss.chain import main as ds +from ddss.egg import main as egg +from ddss.utility import str_rule_get_str_idea + + +def extract_binary_from_term(term: Term) -> tuple[Item, Term, Term] | None: + t = term.term + if isinstance(t, List) and len(t) == 4 and str(t[0]) == "binary": + if isinstance(t[1].term, Item): + return t[1].term, t[2], t[3] + return None + + +def extract_equality_from_rule(rule: Rule) -> tuple[Term, Term] | None: + if len(rule) != 0: + return None + res = extract_binary_from_term(rule.conclusion) + if res and str(res[0]) == "==": + return res[1], res[2] + return None + + +def extract_literal_from_term(term: Term) -> tuple[Item | Variable, Item] | None: + res = extract_binary_from_term(term) + if res and str(res[0]) == "::": + lhs, rhs = res[1].term, res[2].term + if isinstance(lhs, List) and isinstance(rhs, Item): + if len(lhs) == 3 and str(lhs[0]) == "function" and str(lhs[1]) == "Literal": + if isinstance(lhs[2].term, Item | Variable): + return lhs[2].term, rhs + return None + + +async def arithmetic(session): + ops = { + "+": lambda a, b: a + b, + "-": lambda a, b: a - b, + "*": lambda a, b: a * b, + "/": lambda a, b: a / b if b != 0 else None, + } + types_map = {"Int": int, "Float": float} + + try: + max_idea = -1 + + while True: + async with session() as sess: + pool: list[Rule] = [] + for i in await sess.scalars(select(Ideas).where(Ideas.id > max_idea)): + max_idea = max(max_idea, i.id) + pool.append(Rule(i.data)) + + for rule in pool: + if eq := extract_equality_from_rule(rule): + lhs_term, rhs_term = eq + + for side in [("lhs", lhs_term, rhs_term), ("rhs", rhs_term, lhs_term)]: + label, bin_expr, val_expr = side + if bin_res := extract_binary_from_term(bin_expr): + op_str = str(bin_res[0]) + if ( + (func := ops.get(op_str)) + and (v1_lit := extract_literal_from_term(bin_res[1])) + and (v2_lit := extract_literal_from_term(bin_res[2])) + and (v_res_lit := extract_literal_from_term(val_expr)) + ): + val1, type1 = v1_lit + val2, type2 = v2_lit + val_res, type_res = v_res_lit + val1_str = str(val1) + val2_str = str(val2) + type_str = str(type_res) + + if ( + isinstance(val1, Item) + and isinstance(val2, Item) + and isinstance(val_res, Variable) + and type1 == type2 == type_res + and (conv := types_map.get(type_str)) + ): + a = conv(val1_str) + b = conv(val2_str) + res = func(a, b) + + if res is None: + continue + + v1_str = f"(binary :: (function Literal {val1_str}) {type_str})" + v2_str = f"(binary :: (function Literal {val2_str}) {type_str})" + res_str = f"(binary :: (function Literal {res}) {type_str})" + + if label == "lhs": + fact = f"(binary == (binary {op_str} {v1_str} {v2_str}) {res_str})" + else: + fact = f"(binary == {res_str} (binary {op_str} {v1_str} {v2_str}))" + + await insert_or_ignore(sess, Facts, str(Rule(fact))) + + await sess.commit() + + await asyncio.sleep(0) + except asyncio.CancelledError: + pass + + +async def output(session): + try: + max_fact = -1 + max_idea = -1 + + while True: + async with session() as sess: + for i in await sess.scalars(select(Ideas).where(Ideas.id > max_idea)): + max_idea = max(max_idea, i.id) + print("idea:", unparse(i.data)) + for i in await sess.scalars(select(Facts).where(Facts.id > max_fact)): + max_fact = max(max_fact, i.id) + print("fact:", unparse(i.data)) + + rule = Rule(i.data) + if len(rule) == 0: + term = rule.conclusion.term + if isinstance(term, List): + if len(term) >= 2 and str(term[0]) == "function" and str(term[1]) == "Query": + print("status:", unparse(i.data)) + raise asyncio.CancelledError() + await sess.commit() + + await asyncio.sleep(0) + except asyncio.CancelledError: + pass + + +async def load(session, file_name): + async with session() as sess: + for line in open(file_name, "rt", encoding="utf-8"): + data = line.strip() + if data == "": + continue + if data.startswith("//"): + continue + + try: + ds = parse(data) + except Exception as e: + print(f"error: {e}") + continue + + await insert_or_ignore(sess, Facts, ds) + if idea := str_rule_get_str_idea(ds): + await insert_or_ignore(sess, Ideas, idea) + await sess.commit() + + +async def run(addr: str, file_name: str) -> None: + engine, session = await initialize_database(addr) + + try: + await load(session, file_name) + tasks = [ + asyncio.create_task(ds(session)), + asyncio.create_task(egg(session)), + asyncio.create_task(output(session)), + asyncio.create_task(arithmetic(session)), + ] + done, pending = await asyncio.wait( + tasks, + return_when=asyncio.FIRST_COMPLETED, + ) + for task in pending: + task.cancel() + for task in pending: + try: + await task + except asyncio.CancelledError: + pass + except asyncio.CancelledError: + pass + finally: + await engine.dispose() + + +def main() -> None: + tmpdir = tempfile.TemporaryDirectory(prefix="ddss-") + path = pathlib.Path(tmpdir.name) / "ddss.db" + addr = f"sqlite+aiosqlite:///{path.as_posix()}" + file_name = sys.argv[1] + asyncio.run(run(addr, file_name)) + + +if __name__ == "__main__": + main() diff --git a/examples/main.ts b/examples/main.ts new file mode 100644 index 0000000..c0afb86 --- /dev/null +++ b/examples/main.ts @@ -0,0 +1,241 @@ +import * as fs from "node:fs"; +import * as path from "node:path"; +import * as os from "node:os"; +import { Op, type Sequelize } from "sequelize"; +import { Rule, List, Variable, type Term, Item } from "atsds"; +import { parse, unparse } from "atsds-bnf"; +import { Fact, Idea, initializeDatabase, insertOrIgnore } from "../ddss/orm.ts"; +import { main as ds } from "../ddss/chain.ts"; +import { main as egg } from "../ddss/egg.ts"; +import { strRuleGetStrIdea } from "../ddss/utility.ts"; + +function extractBinaryFromTerm(term: Term): [Item, Term, Term] | null { + const t = term.term(); + if (t instanceof List && t.length() === 4 && t.getitem(0).toString() === "binary") { + const opTerm = t.getitem(1).term(); + if (opTerm instanceof Item) { + return [opTerm, t.getitem(2), t.getitem(3)]; + } + } + return null; +} + +function extractEqualityFromRule(rule: Rule): [Term, Term] | null { + if (rule.length() !== 0) { + return null; + } + const res = extractBinaryFromTerm(rule.conclusion()); + if (res && res[0].toString() === "==") { + return [res[1], res[2]]; + } + return null; +} + +function extractLiteralFromTerm(term: Term): [Item | Variable, Item] | null { + const res = extractBinaryFromTerm(term); + if (res && res[0].toString() === "::") { + const lhs = res[1].term(); + const rhs = res[2].term(); + if (lhs instanceof List && rhs instanceof Item) { + if ( + lhs.length() === 3 && + lhs.getitem(0).toString() === "function" && + lhs.getitem(1).toString() === "Literal" + ) { + const val = lhs.getitem(2).term(); + if (val instanceof Item || val instanceof Variable) { + return [val, rhs]; + } + } + } + } + return null; +} + +async function arithmetic() { + const ops: Record number | null> = { + "+": (a, b) => a + b, + "-": (a, b) => a - b, + "*": (a, b) => a * b, + "/": (a, b) => (b !== 0 ? a / b : null), + }; + + const typesMap: Record number> = { + Int: (v) => Number.parseInt(v, 10), + Float: (v) => Number.parseFloat(v), + }; + + let maxIdea = -1; + + while (true) { + const newIdeas = await Idea.findAll({ + where: { id: { [Op.gt]: maxIdea } }, + }); + + for (const idea of newIdeas) { + maxIdea = Math.max(maxIdea, idea.id); + const rule = new Rule(idea.data); + const eq = extractEqualityFromRule(rule); + if (!eq) continue; + + const [lhsTerm, rhsTerm] = eq; + const sides: Array<["lhs" | "rhs", Term, Term]> = [ + ["lhs", lhsTerm, rhsTerm], + ["rhs", rhsTerm, lhsTerm], + ]; + + for (const [label, binExpr, valExpr] of sides) { + const binRes = extractBinaryFromTerm(binExpr); + if (binRes) { + const opStr = binRes[0].toString(); + const func = ops[opStr]; + if (func) { + const v1Lit = extractLiteralFromTerm(binRes[1]); + const v2Lit = extractLiteralFromTerm(binRes[2]); + const vResLit = extractLiteralFromTerm(valExpr); + + if (v1Lit && v2Lit && vResLit) { + const [val1, type1] = v1Lit; + const [val2, type2] = v2Lit; + const [valRes, typeRes] = vResLit; + + const val1Str = val1.toString(); + const val2Str = val2.toString(); + const typeStr = typeRes.toString(); + + if ( + val1 instanceof Item && + val2 instanceof Item && + valRes instanceof Variable && + type1.toString() === type2.toString() && + type1.toString() === typeRes.toString() + ) { + const conv = typesMap[typeStr]; + if (conv) { + const a = conv(val1Str); + const b = conv(val2Str); + const res = func(a, b); + + if (res !== null) { + const v1Str = `(binary :: (function Literal ${val1Str}) ${typeStr})`; + const v2Str = `(binary :: (function Literal ${val2Str}) ${typeStr})`; + const resStr = `(binary :: (function Literal ${res}) ${typeStr})`; + + let factStr: string; + if (label === "lhs") { + factStr = `(binary == (binary ${opStr} ${v1Str} ${v2Str}) ${resStr})`; + } else { + factStr = `(binary == ${resStr} (binary ${opStr} ${v1Str} ${v2Str}))`; + } + + await insertOrIgnore(Fact, new Rule(factStr).toString()); + } + } + } + } + } + } + } + } + + await new Promise((resolve) => setTimeout(resolve, 0)); + } +} + +async function output(abortController: AbortController) { + let maxFact = -1; + let maxIdea = -1; + + while (true) { + const newIdeas = await Idea.findAll({ + where: { id: { [Op.gt]: maxIdea } }, + }); + for (const idea of newIdeas) { + maxIdea = Math.max(maxIdea, idea.id); + console.log("idea:", unparse(idea.data)); + } + + const newFacts = await Fact.findAll({ + where: { id: { [Op.gt]: maxFact } }, + }); + for (const fact of newFacts) { + maxFact = Math.max(maxFact, fact.id); + console.log("fact:", unparse(fact.data)); + + const rule = new Rule(fact.data); + if (rule.length() === 0) { + const term = rule.conclusion().term(); + if ( + term instanceof List && + term.length() >= 2 && + term.getitem(0).toString() === "function" && + term.getitem(1).toString() === "Query" + ) { + console.log("status:", unparse(fact.data)); + abortController.abort(); + return; + } + } + } + + await new Promise((resolve) => setTimeout(resolve, 0)); + } +} + +async function load(fileName: string) { + const content = fs.readFileSync(fileName, "utf-8"); + const lines = content.split("\n"); + + for (const line of lines) { + const data = line.trim(); + if (data === "" || data.startsWith("//")) continue; + + try { + const dsStr = parse(data); + await insertOrIgnore(Fact, dsStr); + const idea = strRuleGetStrIdea(dsStr); + if (idea) { + await insertOrIgnore(Idea, idea); + } + } catch (e) { + console.error(`error: ${(e as Error).message}`); + } + } +} + +async function run(addr: string, fileName: string) { + const sequelize = await initializeDatabase(addr); + const abortController = new AbortController(); + + try { + await load(fileName); + await Promise.race([ + ds(sequelize), + egg(sequelize), + output(abortController), + arithmetic(), + new Promise((_, reject) => { + abortController.signal.addEventListener("abort", () => reject(new Error("Abort"))); + }), + ]).catch((e) => { + if (e.message !== "Abort") throw e; + }); + } finally { + await sequelize.close(); + } +} + +function main() { + const fileName = process.argv[2]; + if (!fileName) { + console.error("Please provide a dsp file"); + process.exit(1); + } + const tmpDir = fs.mkdtempSync(path.join(os.tmpdir(), "ddss-")); + const dbPath = path.join(tmpDir, "ddss.sqlite"); + const addr = `sqlite://${dbPath}`; + + run(addr, fileName).catch(console.error); +} + +main(); diff --git a/examples/relationship.dsp b/examples/relationship.dsp new file mode 100644 index 0000000..6a0ea35 --- /dev/null +++ b/examples/relationship.dsp @@ -0,0 +1,17 @@ +// 初始事实 +Father(Alice, Bob) // Alice 是 Bob 的父亲（此处沿用代码逻辑） +Brother(Bob, Carie) // Bob 是 Carie 的兄弟 +Brother(Mark, Dick) // Mark 是 Dick 的兄弟 +Father(Mark, Bob) // Mark 是 Bob 的父亲 + +// 规则 R1: 如果 X 是 Y 的父亲且 Y 是 Z 的兄弟，则 X 是 Z 的叔伯 +Father(`X, `Y), Brother(`Y, `Z) => Uncle(`X, `Z) + +// 规则 R2: 如果 X 和 Y 都是 Z 的父亲，则 X 和 Y 是同胞 +Father(`X, `Z), Father(`Y, `Z) => Sibling(`X, `Y) + +// 规则 R3: 如果 X 是 Z 的叔伯且 X 与 Y 是同胞，则 Y 也是 Z 的叔伯 +Uncle(`X, `Z), Sibling(`X, `Y) => Uncle(`Y, `Z) + +// 查询：Mark 是谁的叔伯？ +Uncle(Mark, `X) => Query(`X) diff --git a/examples/relationship_quick_start.dsp b/examples/relationship_quick_start.dsp new file mode 100644 index 0000000..a3a4064 --- /dev/null +++ b/examples/relationship_quick_start.dsp @@ -0,0 +1,9 @@ +// 初始事实：定义父母关系 +Parent(Alice, Bob) +Parent(Bob, Carie) + +// 规则：如果 X 是 Y 的父母，且 Y 是 Z 的父母，则 X 是 Z 的祖父母 +Parent(`X, `Y), Parent(`Y, `Z) => GrandParent(`X, `Z) + +// 查询：寻找 Alice 的所有孙辈 +GrandParent(Alice, `X) => Query(`X)