⚡ prune useless facts when solving.

fol/kb.py

@@ -1,13 +1,18 @@
+import random
 import fol
 
 
 class Kb:
     def __init__(self):
         self.base = []
+        self.existing = {}
+        self.prev = []
+        self.current = []
+
+        self.indexes = {}
         self.counter = fol.cnf.Counter()
 
     def make_f(self, h):
-
         f = h
         if type(f) is str:
             f = fol.p(f)
@@ -68,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
 
@@ -90,25 +104,39 @@ class Kb:
     def clause_in(self, clause, lst):
         for other in lst:
             same = clause.equals(other)
-
-            s = fol.unify(clause, other)
-            # same = s is not None
             if same:
                 return True
         return False
 
-    def tell(self, request):
-        req = self.make_f(request)
+    def add_req(self, req):
+        if len(req) == 1:
+            preds = []
+            for r in req:
+                preds.extend(r.find_by_name('PRED'))
+
+            for p in preds:
+                if p.value in self.indexes.keys():
+                    self.indexes[p.value].append(req)
+                else:
+                    self.indexes[p.value] = [req]
         self.check_request(req)
         self.base.append(req)
+        self.current.append(req)
 
-    def ask(self, request):
+    def tell(self, request):
+        req = self.make_f(request)
+        self.add_req(req)
+
+    def generate(self):
         while True:
-            n = len(self.base)
             self.update()
-            if n == len(self.base):
+            self.prev = [c for c in self.current]
+            self.current = []
+            if len(self.prev) == 0:
                 break
 
+    def ask(self, request):
+        self.generate()
         req = self.make_req(request)
         results = []
 
@@ -129,14 +157,36 @@ class Kb:
             conclusion = self.conclusion(rule)
             solution = []
             solutions = []
-            self.solve(rule, self.conds(rule), self.facts, solution, solutions)
+
+            preds = []
+            for cond in self.conds(rule):
+                preds.append(cond.value)
+            facts = []
+            for p in preds:
+                if p in self.indexes.keys():
+                    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
+
+            self.solve(rule, rules, facts, solution, solutions)
+
             for sol in solutions:
                 concl = conclusion.subst(sol)
-
-                if not self.exists(concl) and concl.depth() < 4:
-                    self.base.append([concl])
+                if not self.exists(concl):
+                    self.add_req([concl])
                     return
 
+    def is_rule_needed(self, rule, prev):
+        for f in prev:
+            for r in rule:
+                s = fol.unify(r, f[0])
+                if s is not None:
+                    return True
+        return False
+
     def merge_substs(self, substs):
         res = {}
         for s in substs:
@@ -154,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)
 

sine_patre.py

@@ -3,16 +3,34 @@ import fol
 if __name__ == '__main__':
     kb = fol.kb.Kb()
     try:
-        if False:
-            kb.tell('Est(ALICE, X0, S0)')
-            kb.tell('Proche(X0, X1)')
-            kb.tell('Proche(X1, X2)')
-            kb.tell('Proche(X2, X3)')
-            kb.tell('Proche(X3, X4)')
+        if True:
+            kb.tell('Est(ALICE, L0, S0)')
+            kb.tell('Proche(L0, L1)')
+            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]
+
+            if False:
+                print(f'{len(kb.base)}----------------')
+                [print(r) for r in kb.base]
+                print(f'{len(kb.base)}----------------')
+                print(answer)
+
+            if False:
+                for k, v in kb.indexes.items():
+                    print('--------', k, '--------')
+                    [print(p) for p in v]
+
         else:
             kb.tell('Friend(ALICE, BOB)')
             kb.tell('Friend(BOB, CLAIRE)')