From 116dd25881df91f97a826c114085bb7d51d240d1 Mon Sep 17 00:00:00 2001
From: bog <bog@gozmail.net>
Date: Wed, 1 May 2024 23:38:10 +0200
Subject: [PATCH] :zap: prune useless facts when solving.

---
 fol/kb.py     | 20 +++++++++++++++-----
 sine_patre.py |  6 +++++-
 2 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/fol/kb.py b/fol/kb.py
index 98acd44..362ab47 100644
--- a/fol/kb.py
+++ b/fol/kb.py
@@ -1,10 +1,11 @@
+import random
 import fol
 
 
 class Kb:
     def __init__(self):
         self.base = []
-
+        self.existing = {}
         self.prev = []
         self.current = []
 
@@ -72,8 +73,17 @@ class Kb:
         return res
 
     def exists(self, f):
-        for g in self.base:
+        if str(f) in self.existing.keys():
+            return True
+
+        facts = self.base
+
+        if f.value in self.indexes.keys():
+            facts = self.indexes[f.value]
+
+        for g in facts:
             if self.clause_equals([f], g):
+                self.existing[str(f)] = True
                 return True
         return False
 
@@ -157,9 +167,7 @@ class Kb:
                     facts.extend(self.indexes[p])
 
             facts = [f[0] for f in facts]
-
             rules = self.conds(rule)
-
             if not self.is_rule_needed(rules, self.prev):
                 continue
 
@@ -167,7 +175,7 @@ class Kb:
 
             for sol in solutions:
                 concl = conclusion.subst(sol)
-                if concl.depth() < 8 and not self.exists(concl):
+                if not self.exists(concl):
                     self.add_req([concl])
                     return
 
@@ -196,6 +204,8 @@ class Kb:
                 s = fol.unify(sol[0], sol[1])
                 if s is not None:
                     substs.append(s)
+                else:
+                    return
 
             s = self.merge_substs(substs)
 
diff --git a/sine_patre.py b/sine_patre.py
index e6940d5..b7a4a3b 100644
--- a/sine_patre.py
+++ b/sine_patre.py
@@ -9,9 +9,13 @@ if __name__ == '__main__':
             kb.tell('Proche(L1, L2)')
             kb.tell('Proche(L2, L3)')
             kb.tell('Proche(L3, L4)')
+            kb.tell('Proche(L4, L5)')
+            kb.tell('Proche(L5, L6)')
+            kb.tell('Proche(L6, L7)')
             kb.tell('(Est(ALICE, x, s) & Proche(x, y)) -> Poss(go(x, y), s)')
             kb.tell('Poss(go(x, y), s) -> Est(ALICE, y, do(go(x, y), s))')
-            answer = kb.ask('Est(ALICE, x, y)')
+
+            answer = kb.ask('Est(ALICE, place, situation)')
 
             print(answer)
             # [print(k) for k in kb.base]