2024-04-28 16:23:47 +00:00
|
|
|
import fol
|
|
|
|
|
|
|
|
|
|
|
|
class Kb:
|
|
|
|
def __init__(self):
|
|
|
|
self.base = []
|
2024-04-29 21:15:06 +00:00
|
|
|
self.indexes = {}
|
2024-04-28 16:23:47 +00:00
|
|
|
self.counter = fol.cnf.Counter()
|
|
|
|
|
|
|
|
def make_f(self, h):
|
|
|
|
f = h
|
|
|
|
if type(f) is str:
|
|
|
|
f = fol.p(f)
|
|
|
|
self.counter.begin()
|
|
|
|
f = fol.cnf.cnf(f, self.counter)
|
|
|
|
|
|
|
|
if f.name == 'OR':
|
|
|
|
f = f.list_of('OR')
|
|
|
|
else:
|
|
|
|
f = [f]
|
|
|
|
|
|
|
|
return f
|
|
|
|
|
|
|
|
def make_req(self, h):
|
|
|
|
f = h
|
|
|
|
if type(f) is str:
|
|
|
|
f = fol.p(f)
|
|
|
|
|
|
|
|
if f.name == 'OR':
|
|
|
|
f = f.list_of('OR')
|
|
|
|
else:
|
|
|
|
f = [f]
|
|
|
|
|
|
|
|
return f
|
|
|
|
|
|
|
|
def check_request(self, request):
|
|
|
|
for r in request:
|
|
|
|
if r.name not in ['NOT', 'PRED']:
|
|
|
|
raise Exception(f'invalid statement {repr(r)}')
|
|
|
|
|
|
|
|
def conds(self, statement):
|
|
|
|
result = []
|
|
|
|
for f in statement:
|
|
|
|
if f.name == 'NOT':
|
|
|
|
result.append(f.children[0])
|
|
|
|
return result
|
|
|
|
|
|
|
|
def conclusion(self, statement):
|
|
|
|
for f in statement:
|
|
|
|
if f.name != 'NOT':
|
|
|
|
return f
|
|
|
|
return None
|
|
|
|
|
|
|
|
@property
|
|
|
|
def rules(self):
|
|
|
|
res = []
|
|
|
|
for r in self.base:
|
|
|
|
if len(r) > 1:
|
|
|
|
res.append(r)
|
|
|
|
return res
|
|
|
|
|
|
|
|
@property
|
|
|
|
def facts(self):
|
|
|
|
res = []
|
|
|
|
for r in self.base:
|
|
|
|
if len(r) == 1:
|
|
|
|
res.append(r[0])
|
|
|
|
return res
|
|
|
|
|
|
|
|
def exists(self, f):
|
|
|
|
for g in self.base:
|
2024-04-28 22:43:24 +00:00
|
|
|
if self.clause_equals([f], g):
|
2024-04-28 16:23:47 +00:00
|
|
|
return True
|
|
|
|
return False
|
|
|
|
|
|
|
|
def clause_equals(self, left, right):
|
|
|
|
if len(left) != len(right):
|
|
|
|
return False
|
|
|
|
|
|
|
|
for element in left:
|
|
|
|
if not self.clause_in(element, right):
|
|
|
|
return False
|
|
|
|
|
|
|
|
for element in right:
|
|
|
|
if not self.clause_in(element, left):
|
|
|
|
return False
|
|
|
|
|
|
|
|
return True
|
|
|
|
|
|
|
|
def clause_in(self, clause, lst):
|
|
|
|
for other in lst:
|
2024-04-28 22:43:24 +00:00
|
|
|
same = clause.equals(other)
|
2024-04-28 16:23:47 +00:00
|
|
|
if same:
|
|
|
|
return True
|
|
|
|
return False
|
|
|
|
|
2024-04-29 21:15:06 +00:00
|
|
|
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]
|
2024-04-28 16:23:47 +00:00
|
|
|
self.check_request(req)
|
|
|
|
self.base.append(req)
|
|
|
|
|
2024-04-29 21:15:06 +00:00
|
|
|
def tell(self, request):
|
|
|
|
req = self.make_f(request)
|
|
|
|
self.add_req(req)
|
|
|
|
|
2024-04-28 16:23:47 +00:00
|
|
|
def ask(self, request):
|
2024-04-28 22:43:24 +00:00
|
|
|
while True:
|
2024-04-28 16:23:47 +00:00
|
|
|
n = len(self.base)
|
|
|
|
self.update()
|
|
|
|
if n == len(self.base):
|
|
|
|
break
|
|
|
|
|
|
|
|
req = self.make_req(request)
|
|
|
|
results = []
|
|
|
|
|
|
|
|
for f in self.base:
|
|
|
|
s = fol.unify(f, req)
|
|
|
|
if s is not None:
|
2024-04-28 22:43:24 +00:00
|
|
|
ok = True
|
|
|
|
for k in s.keys():
|
|
|
|
if len(s[k].find_by_name('VAR')) > 0:
|
|
|
|
ok = False
|
|
|
|
if ok:
|
|
|
|
results.append(s)
|
2024-04-28 16:23:47 +00:00
|
|
|
|
|
|
|
return results
|
|
|
|
|
|
|
|
def update(self):
|
|
|
|
for rule in self.rules:
|
|
|
|
conclusion = self.conclusion(rule)
|
|
|
|
solution = []
|
|
|
|
solutions = []
|
2024-04-29 21:15:06 +00:00
|
|
|
|
|
|
|
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]
|
|
|
|
|
|
|
|
self.solve(rule, self.conds(rule), facts, solution, solutions)
|
|
|
|
|
2024-04-28 16:23:47 +00:00
|
|
|
for sol in solutions:
|
|
|
|
concl = conclusion.subst(sol)
|
2024-04-29 21:15:06 +00:00
|
|
|
if concl.depth() < 8 and not self.exists(concl):
|
|
|
|
self.add_req([concl])
|
2024-04-28 16:23:47 +00:00
|
|
|
return
|
|
|
|
|
|
|
|
def merge_substs(self, substs):
|
|
|
|
res = {}
|
|
|
|
for s in substs:
|
|
|
|
for k in s.keys():
|
|
|
|
if k in res.keys() and not res[k].equals(s[k]):
|
|
|
|
return None
|
|
|
|
res[k] = s[k]
|
|
|
|
return res
|
|
|
|
|
|
|
|
def solve(self, rule, conds, facts, solution, solutions):
|
|
|
|
if len(conds) == 0:
|
|
|
|
substs = []
|
|
|
|
|
|
|
|
for sol in solution:
|
|
|
|
s = fol.unify(sol[0], sol[1])
|
|
|
|
if s is not None:
|
|
|
|
substs.append(s)
|
|
|
|
|
|
|
|
s = self.merge_substs(substs)
|
|
|
|
|
|
|
|
if s is not None:
|
|
|
|
solutions.append(s)
|
|
|
|
return
|
|
|
|
|
|
|
|
for cond in conds:
|
|
|
|
for fact in facts:
|
|
|
|
solution.append((cond, fact))
|
|
|
|
|
|
|
|
self.solve(
|
|
|
|
rule,
|
|
|
|
[c for c in conds if c != cond],
|
|
|
|
[f for f in facts if f != fact],
|
|
|
|
solution,
|
|
|
|
solutions
|
|
|
|
)
|
|
|
|
|
|
|
|
solution.pop()
|