import N3Engine, xml, Unify, UtilsN3, string, ToN3 class Proof: # verbose flag = trace verbose = 0 # extended flag = extended trace extended = 0 # a limitation of the number of steps of the engine loopLimit = 100 # flag to test if the limit is obtained limitFlag = 0 # flag for interactive testing interactive = 0 # unification instance unify = Unify.Unify() # utils instance utils = UtilsN3.Utils() # to n3 instance toN3 = ToN3.ToN3() # variable for testing newV = 1 newVerbose = 1 # an alternative consists of a goal list and a substitution that must # be combined with the substitution that was already found at that # point. # In Haskell: type Alt = ([XMLTree], Subst) # execute the proof1 funcion for every tripleset in the query # returns a list of lists def proof(self, semTree, semDic): query = semDic["query"] triplesets = query.getDirectChildrenByName("TripleSet") genSubstList = [] genTrace = xml.XmlTree("Trace") genCycleCounter = 0 for tripleset in triplesets: substList, trace, cycleCounter = ( self.proof1(semTree, semDic, tripleset)) genSubstList = genSubstList + [substList] genTrace.addTreeList(trace.children) genCycleCounter = genCycleCounter + cycleCounter return (genSubstList, genTrace, genCycleCounter) # The leightweight proof engine. # a proof has as input the database of clauses and a query # the output is a list of substitutions (one for each found solution) # and an XMLTree that contains information if the verbose flag is set. # the query is the initial goallist. # The database with the axiom-file and the query-file, the prefixes and variables # is a global variable and also the dictionary. def proof1(self, semTree, semDic, query): # altCounter counts the number of searches for alternatives self.altCounter = 0 # cycleCounter counts the number of unifications self.cycleCounter = 0 dbh = semDic["axioms"] self.db = dbh.getDirectChildrenByName("TripleSet") self.query = query.copy() query.printXml("") self.goals = [self.query] self.trace = xml.XmlTree("proof") self.substitutionList = [] # the alternative solutions self.subs = [] # current substitution self.stack = [] self.alts = ([], xml.XmlTree("Empty")) self.abortFlag = 0 self.oldGoals = [] self.altFlag = 1 self.level = 0 # the initial substitution level # one is added to this level for each unification round (get alternatives) # and one is subtracted for each backtrack. # The variables in the substitution are marked with this level. self.solve() self.choose() wait = "." while 1: while (not len(self.goals) == 0): if not self.verbose: self.trace.clearTree() if self.verbose: ch = xml.XmlTree("choose") self.trace.addTree(ch) # loop limitation; this is for testing. if (self.altCounter > self.loopLimit and self.limitFlag): return (self.substitutionList, self.trace, self.cycleCounter) test = 0 if test: if wait == ".": wait = "/" print wait else: wait = "." print wait self.solve() # try to unify if len(self.stack) == 0: break altList, altTrace = self.alts while (len(altList) == 0): if len(self.stack) == 0: break self.backtrack () # one step back; try an alternative # return to last choicepoint self.level = self.level - 1 altList, altTrace = self.alts self.choose() # choose an alternative # the goal list is empty; a solution has been found if len(self.stack) == 0: break self.oldGoals = [] self.abortFlag = 0 if (not self.abortFlag ): self.subs = self.unify.elimDoubleSubstitutions(self.subs) flag = 0 for subst in self.substitutionList: if self.unify.compareSubstitutions(subst, self.subs): self.unify.showSubstitution(subst) flag = 1 break if not flag: if self.interactive: print "Solution found !!!!!!!!!!!!!!!!!\n" print self.unify.showSubstitution(self.subs) self.substitutionList = self.substitutionList + [self.subs] self.abortFlag = 0 self.backtrack() # try to find another solution altList, altTrace = self.alts while len(altList) == 0: if len(self.stack) == 0: break self.backtrack () # one step back; try an alternative # return to last choicepoint self.level = self.level - 1 altList, altTrace = self.alts self.choose() # choose an alternative return (self.substitutionList, self.trace, self.cycleCounter) # when the goal list is empty and the stack is empty all solutions # have been found; if the goallist is empty but not the stack then # a backtrack will be done in search of further solutions. # parameters: trace, substitution, goals(query), stack, counter, database. # Returns a substitution list (one substi tution for each solution) # and the trace. def solve(self): # search a solution for the goal at the top of the goallist. # testing n permits to limit the number of loops when # the limitFlag is set. bool1 = len(self.goals) == 0 tr1 = xml.XmlTree("Results") if (bool1): if self.verbose: gEmpty = xml.XmlTree("solve goallist empty") tr1.addTree(gEmpty) self.trace.addTree(gEmpty) if self.interactive: #tr1.printXml("") print "Nr. of loops: " + `self.altCounter` raw_input("Push enter to continue\n" + "==========================\n\n") return else: self.altCounter = self.altCounter + 1 test = 0 if not test: if len(self.goals) == 0: return goal = self.goals[0] goal1 = goal.copy() goal1 = self.unify.applySubstitution( self.subs, goal1) if test: done = 0 # loop test while not done: if len(self.goals) == 0: return goal = self.goals[0] oldGoal = goal.copy() goal1 = goal.copy() goal1 = self.unify.applySubstitution( self.subs, goal1) bool3 = 0 # check if a goal comes back = loop for goal2 in self.oldGoals: goal3, oldLevel = goal2 if (oldLevel < self.level and self.compareTreesVars(goal1, goal3)): bool3 = 1 break if ( bool3): if self.verbose: stackTag = xml.XmlTree("stack") stackTag.content = self.showStack(self.stack) goalTag = xml.XmlTree("goal") goalTag.addTree(goal1) goalsTag = xml.XmlTree("goals") goalsTag.addTreeList(self.goals) aTree = xml.XmlTree("Abort!!!!!!") self.trace.addTree(stackTag) self.trace.addTree(goalTag) self.trace.addTree(goalsTag) self.trace.addTree(aTree) if self.interactive: tr1.addTree(goalTag) tr1.addTree(goalsTag) tr1.addTree(aTree) # tr1.printXml("") self.toN3.init() if tr1.name == "TripleSet": self.toN3.transTripleSet(tr1) else: self.toN3.transTriple(tr1) print "Repeating goal -- abort!!!!!" print ":goal = {" + self.toN3.n3Out + "}." print "Nr. of loops: " + `self.altCounter` raw_input("Push enter to continue\n" + "--------------------------\n\n") # loop detected; (recurring goal) # must do backtrack to before the first occurence of # the recurring goal; # other alts are on stack while self.level > oldLevel: if len(self.stack) == 0: return self.backtrack () # one step back; try an alternative # return to last choicepoint self.level = self.level - 1 self.choose() # choose an alternative done = 1 else: done = 1 self.oldGoals = self.oldGoals + [(goal1, self.level)] self.goals = self.goals[1:] self.level = self.level + 1 self.alts, self.altFlag = (self.getAlts(self.db, goal1, self.subs)) if not self.altFlag: self.abortFlag = 1 altList, altTrace = self.alts # test of loops test = 1 if test: altList1 = [] for alt in altList: treeList, subst = alt flag = 0 for tree in treeList: tree1 = tree.copy() tree1 = self.unify.applySubstitution( self.subs + subst, tree1) if self.compareTreesVars(tree1, goal1): flag = 1 break if not flag: altList1 = altList1 + [alt] self.alts = (altList1, altTrace) if self.newV: self.toN3.init() if goal1.name == "TripleSet": self.toN3.transTripleSet(goal1) else: self.toN3.transTriple(goal1) print ":goal = {" + self.toN3.n3Out + "}." if self.verbose: goalTag = xml.XmlTree("goal") goalTag.addTree(goal1) goalsTag = xml.XmlTree("goals") goalsTag.addTreeList(self.goals) solveTag = xml.XmlTree("solve") solveTag.addTree(goalTag) solveTag.addTree(goalsTag) failed = self.getFailedSubstitution(self.alts, self.subs, goal1) solveTag.addTree(failed) self.trace.addTree(solveTag) tr1.addTree(solveTag) altList, altTrace = self.alts if self.newVerbose: if not len(self.goals) == 0: print "List of goals to be proven:" for g in self.goals: self.toN3.init() if g.name == "TripleSet": self.toN3.transTripleSet(g) else: self.toN3.transTriple(g) print " :goal = {" + self.toN3.n3Out + "}." for child in altTrace.children: if child.name == "Substitution": subTs = child.children if not len(subTs) == 0: print "Substitution:" for subT in subTs: self.toN3.init() if subT.name == "TripleSet": self.toN3.transTripleSet(subT) else: self.toN3.transTriple(subT) print " :sub = {" + self.toN3.n3Out + "}." if child.name == "Alternatives": altTs = child.children if not len(altTs) == 0: for altT in altTs: print "Alternatives:" self.toN3.init() if altT.name == "TripleSet": self.toN3.transTripleSet(altT) else: self.toN3.transTriple(altT) print " :alt = {" + self.toN3.n3Out + "}." if self.interactive: tr1.addTree(altTrace) #tr1.printXml("") print "Nr. of loops: " + `self.altCounter` raw_input("Push enter to continue\n"+ "__________________________\n\n") def getFailedSubstitution(self, alts, subs, goal): altList, altTrace = alts if len(altList) == 0: t1 = xml.XmlTree("already_made_substitution") string = self.unify.showSubstitution(subs) t1.content = string t2 = xml.XmlTree("failed_substitution") t2.addTree(t1) t2.addTree(goal) return t2 else: return xml.XmlTree("Empty") # choose an alternative. # parameters are: the trace, a substitution, a goal list, the list of alternatives, the stack, # the counter and the database. Returned: a substitution list and a trace. def choose(self): # add the goals of the first alternative to the goallist # and combine the substitutions and try to solve; save the # previous goallist on the stack with the previous substitution # and the previous list of alternatives. # alts is a tuple: the tuple contains a list of # alternatives (= first element) and a trace tree( = second element) # The list of alternatives contains tuples: # The first element of each tuple contains a goal list # and the second element contains a substitution. # alts = (altsList, traceTree) # altsList =[(gl, subs), (...,...), ...] altList, altTrace = self.alts self.altLen = len(altList) if len(altList) == 0: return if self.extended and self.verbose: self.trace.addTree(altTrace) treeList, sub = altList[0] self.stack = [(self.subs, self.goals, altList[1:])] + self.stack self.subs = self.subs + sub self.goals = treeList + self.goals # If a goal fails then retrieve the last saved situation from # the stack. def backtrack (self): if self.verbose: bt = xml.XmlTree("backtrack") self.trace.addTree(bt) if self.interactive: tr1 = xml.XmlTree("backtrack") # backtrack to the last choice point. self.subs, self.goals, altsNT = self.stack[0] # if (not len(self.subs) == 0 and len(self.alts) == 0 and # not len(self.goals) == 0): # self.subsitutionList = self.substitutionList + [self.subs] self.alts = (altsNT, xml.XmlTree("Alts")) altList, altTrace = self.alts self.showAlts(altList) self.stack = self.stack[1:] # checks whether a goal in a goal list is grounded or not; if it is the goal is # eliminated. Returns the goal list without the grounded goals. def checkGrounded (self, goalList): if len(goalList) == 0: return [] else: goalList1 = [] for goal in goalList: tree1 = goal.getChildrenByName(goal, "Var", []) tree2 = goal.getChildrenByName(goal, "EVar", []) tree3 = goal.getChildrenByName(goal, "GVar", []) tree4 = goal.getChildrenByName(goal, "GEVar", []) if (len(tree1) == 0 and len(tree2) == 0 and len(tree3) == 0 and len(tree4) == 0): # goal is grounded; eliminate pass else: goalList1 = goalList1 + [goal] return goalList1 # get the list of matches of a triple with the heads in the database. # unify and rename the variables. # this is the kernel of the resolution engine. # The first parameter is the database; the second is the goal to unify; # The third parameter is the current substitution. # Output is a list of alternatives # consisting of pairs that contain a clause and a substitution: # type Alt = (XMLTree, Subst), and an XMLTree that contains trace data. # A goal is a tripleset. def getAlts(self, db, goal, subst): out1 = xml.XmlTree("Input triple for generation of above goals") if self.extended: out1.addTree(goal) if (len(db) == 0 or goal.type == "Empty"): return (([], out1),0) else: alts = [] bool1 = 0 traceOut = xml.XmlTree("Unification") for tripleset2 in db: self.cycleCounter = self.cycleCounter + 1 tripleset = tripleset2.copy() # optimisation possible self.renameTripleset(tripleset, self.level + 1) if not goal.name == "TripleSet": tripleset1 = xml.XmlTree("TripleSet") tripleset1.addTree(goal) goal = tripleset1 bool, subst1, tree, goals = (self.unify.unifyTwoTripleSets(goal, tripleset)) test = 1 if test: goalsCo = [] for goalC in goals: goalL = self.checkGrounded([goalC]) if len(goalL) == 0: pass else: goalsCo = goalsCo + [goalC] goals = goalsCo else: goals = self.checkGrounded(goals) if bool: bool1 = 1 out = xml.XmlTree("Substitution") if self.newVerbose: #verbose: out.addTree(goal) out.addTree(tripleset) out1 = xml.XmlTree("Alternatives") if self.newVerbose: #extended: out1.addTreeList(goals) traceOut.addTree(out) traceOut.addTree(out1) alts = alts + [(goals, subst1)] return ((alts, traceOut), bool1) # prefix the variables in a substitution with the current level # = depth of inferencing. def renameVariables(self, substitution): for subst in substitution: subst1, subst2 = subst bool = (subst1.name == "Var" or subst1.name == "EVar" or subst1.name == "GVar" or subst1.name == "GEVar") if bool: if (not self.utils.containsString("$_$", subst1.content)== "T"): subst1.content = `self.level` + "$_$" + subst1.content bool = (subst2.name == "Var" or subst2.name == "EVar" or subst2.name == "GVar" or subst2.name == "GEVar") if bool: if (not self.utils.containsString("$_$", subst2.content) == "T"): subst2.content = `self.level` + "$_$" + subst2.content return substitution # rename the variables in a tripleset def renameTripleset(self, tripleset, level): # optimisation possible vars = tripleset.getChildrenByName(tripleset,"Var", []) vars = vars + tripleset.getChildrenByName(tripleset,"EVar", []) vars = vars + tripleset.getChildrenByName(tripleset,"GVar", []) vars = vars + tripleset.getChildrenByName(tripleset,"GEVar", []) for var in vars: var.content = `level` + "$_$" + var.content # show the contents of the stack. # The stack is a list of triples. # Each triple contains: a substitution, a goal list + an alternative list. # The alternative list is a list of tuples (goal list, substitution). # return a string def showStack(self, stack): if len(stack) == 0: return "\nStack is empty.\n" else: dummy = xml.XmlTree("dummy") output = "Stack:\n\n" for entry in stack: output = output + "Stack entry:\n\n" subst, goalList, alts = entry output = (output + "Substitution: " + self.unify.showSubstitution(subst) + "\nGoals: " + dummy.toStringTreeList(goalList) + "\nAlts: \n" + self.showAlts(alts) + "\n") output = output + "\nEnd of stack.\n\n" return output # show an alternative list. def showAlts(self, altsList): if len(altsList) == 0: return "" else: output = "" for alt in altsList: output = output + "\nAlternative:\n" output = output + self.showAlt(alt) return output + "\nEnd of alternatives" # show an alternative. # an alternative consists of a tree list (a list of goals) and a substitution def showAlt(self, alt): goalList, subst = alt dummy = xml.XmlTree("dummy") return (dummy.toStringTreeList(goalList) + self.unify.showSubstitution(subst) + "\nEnd\n") # strip the level prefix of vars def stripVars(self, tree): # does this work ??? vars = tree.getChildrenByName(tree, "Var", []) vars = vars + tree.getChildrenByName(tree, "EVar", []) vars = vars + tree.getChildrenByName(tree, "GVar", []) vars = vars + tree.getChildrenByName(tree, "GEVar", []) for var in vars: (bool1, s1, rest1) = ( self.utils.parseUntilString(var.content, "$_$")) var.content = rest1[3:] # compare two trees; strip the level indication of the vars # this compares name, content and children def compareTreesVars (self, tree1, tree2): name1 = string.strip(tree1.name) name2 = string.strip(tree2.name) content1 = tree1.content content2 = tree2.content if (name1 == "Var" or name1 == "EVar" or name1 == "GVar" or name1 == "GEVar"): (bool1, s1, rest1) = ( self.utils.parseUntilString(content1, "$_$")) content1 = rest1[3:] if (name2 == "Var" or name2 == "EVar" or name2 == "GVar" or name2 == "GEVar"): (bool2, s2, rest2) = ( self.utils.parseUntilString(content2, "$_$")) content2 = rest2[3:] if (name1 == name2 and content1 == content2): children1 = tree1.children children2 = tree2.children flag = 0 for t1 in children1: flag1 = 0 for t2 in children2: if self.compareTreesVars(t1, t2): flag1 = 1 break if flag1 == 0: flag = 1 break if flag == 1: return 0 else: return 1 else: return 0