-
-
Save mtensor/d824b8462535d9b2c690008d2db243a0 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| from z3 import * | |
| class ParseError(Exception): | |
| pass | |
| class FancyDefaultDict(dict): | |
| def __init__(self, fn): | |
| super(FancyDefaultDict, self).__init__() | |
| self.fn = fn | |
| def __missing__(self, key): | |
| res = self[key] = self.fn(key) | |
| return res | |
| class Env: | |
| def __init__(self): | |
| self.people = FancyDefaultDict( lambda personName: Const(personName, Person) ) | |
| self.s = Solver() | |
| self.s.set(unsat_core=True) | |
| Person = DeclareSort('Person') | |
| self.Person = Person | |
| # ancestor(x, y) -> ancestor of x is y | |
| ancestor = Function('ancestor', Person, Person, BoolSort()) | |
| # anti-reflexitivity | |
| x = Const('x', Person) | |
| y = Const('y', Person) | |
| z = Const('z', Person) | |
| self.x = x | |
| self.y = y | |
| self.z = z | |
| #new stuff | |
| grand = Function('grand', Person, Person, BoolSort()) | |
| #grand is short for grandchild | |
| inv_grand = Function('inv_grand', Person, Person, BoolSort()) | |
| child = Function('child', Person, Person, BoolSort()) | |
| inv_child = Function('inv_child', Person, Person, BoolSort()) | |
| sibling = Function('sibling', Person, Person, BoolSort()) | |
| in_law = Function('in_law', Person, Person, BoolSort()) | |
| inv_in_law = Function('inv_in_law', Person, Person, BoolSort()) | |
| #uncle | |
| un = Function('un', Person, Person, BoolSort()) | |
| inv_un = Function('inv_un', Person, Person, BoolSort()) | |
| SO = Function('SO', Person, Person, BoolSort()) | |
| #relations: | |
| self.s.add(ForAll([x, y, z], Implies(And(child(x, z), child(z, y)), | |
| grand(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(SO(x, z), grand(z, y)), | |
| grand(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(grand(x, z), sibling(z, y)), | |
| grand(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(inv_child(x, z), inv_child(z, y)), | |
| inv_grand(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(sibling(x, z), inv_grand(z, y)), | |
| inv_grand(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(child(x, z), sibling(z, y)), | |
| child(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(SO(x, z), child(z, y)), | |
| child(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(sibling(x, z), inv_child(z, y)), | |
| inv_child(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(child(x, z), inv_grand(z, y)), | |
| inv_child(x, y)))) | |
| # self.s.add(ForAll([x, y, z], Implies(And(child(x, z), inv_un(z, y)), | |
| # sibling(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(x != y, inv_child(x, z), child(z, y)), | |
| sibling(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(child(x, z), SO(z, y)), | |
| in_law(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(SO(x, z), inv_child(z, y)), | |
| inv_in_law(x, y)))) | |
| #terminology for uncle is backwards: un(x,y) -> uncle of y is x | |
| self.s.add(ForAll([x, y, z], Implies(And(sibling(x, z), child(z, y)), | |
| un(x, y)))) | |
| self.s.add(ForAll([x, y, z], Implies(And(inv_child(x, z), sibling(z, y)), | |
| inv_un(x, y)))) | |
| #inverses: | |
| self.s.add(ForAll([x, y], child(x, y) == inv_child(y, x) )) | |
| self.s.add(ForAll([x, y], inv_in_law(x, y) == in_law(y,x))) | |
| self.s.add(ForAll([x, y], inv_grand(x, y) == grand(y,x))) | |
| self.s.add(ForAll([x, y], inv_un(x, y) == un(y, x))) | |
| #symmetric ones: | |
| #self.s.add(ForAll([x, y], Implies(And(sibling(x, y), x != y), sibling(y,x)))) | |
| self.s.add(ForAll([x, y], Implies(sibling(x, y), sibling(y, x)))) | |
| self.s.add(ForAll([x, y], SO(y, x) == SO(x, y))) | |
| #what is an ancestor? | |
| self.s.add(ForAll([x, y], Implies( child(x, y), ancestor(y,x) ))) | |
| self.s.add(ForAll([x, y], Implies( grand(x, y), ancestor(y,x) ))) | |
| #sibling is transitive: | |
| self.s.add(ForAll([x, y, z], Implies(And(x!=z, sibling(x, y), sibling(y, z)), | |
| sibling(x, z)))) | |
| #1 you can't be your own ancestor | |
| self.s.add(ForAll([x, y], Implies(ancestor(x, y), Not(ancestor(y, x))))) | |
| # ancestor transitivity | |
| self.s.add(ForAll([x, y, z], Implies(And(ancestor(x, y), ancestor(y, z)), | |
| ancestor(x, z)))) #fine | |
| #2 you can't be your own sibling - need to change rule above | |
| self.s.add(ForAll(x, Not(sibling(x, x)))) | |
| #inverse of uncle | |
| self.s.add(ForAll([x, y], Implies(un(x, y), Exists(z, And(sibling(x, z), child(z, y)) )))) | |
| #inverse of sibling | |
| self.s.add(ForAll([x, y], Implies(sibling(x, y), Exists(z, And(child(z, x), child(z, y)) )))) | |
| #parents cant be uncles: | |
| self.s.add(ForAll([x, y], Implies(inv_un(x, y), Not(inv_child(x, y))) )) | |
| self.s.add(ForAll([x, y], Implies(inv_child(x, y), Not(inv_un(x, y))) )) | |
| self.s.push() | |
| self.rels = {rel.name(): rel for rel in [ancestor, | |
| grand, inv_grand, child, inv_child, sibling, in_law, inv_in_law, un, inv_un, SO]} #TODO | |
| #extra names for use of parser | |
| self.rels['spouse'] = SO | |
| self.rels['husband'] = SO | |
| self.rels['wife'] = SO | |
| self.rels['parent'] = inv_child | |
| self.rels['grandchild'] = grand | |
| self.rels['granddaughter'] = grand | |
| self.rels['grandson'] = grand | |
| self.rels['grandparent'] = inv_grand | |
| self.rels['grandmother'] = inv_grand | |
| self.rels['grandfather'] = inv_grand | |
| self.rels['father'] = self.rels['parent'] | |
| self.rels['mother'] = self.rels['parent'] | |
| self.rels['uncle'] = inv_un | |
| self.rels['aunt'] = inv_un | |
| self.rels['nephew'] = un | |
| self.rels['niece'] = un | |
| self.rels['sister'] = sibling | |
| self.rels['brother'] = sibling | |
| self.rels['friend'] = None | |
| self.rels['dog'] = None | |
| self.rels['pet'] = None | |
| self.rels['cousin'] = None | |
| self.rels['daughter'] = child | |
| self.rels['son'] = child | |
| self.rels['daughter in law'] = in_law | |
| self.rels['son in law'] = in_law | |
| self.rels['mother in law'] = inv_in_law | |
| self.rels['father in law'] = inv_in_law | |
| self.rels['mother-in-law'] = inv_in_law | |
| self.rels['father-in-law'] = inv_in_law | |
| self.rels['daughter-in-law'] = in_law | |
| self.rels['son-in-law'] = in_law | |
| def buildConstraint(self, string): | |
| return constraint | |
| def parseConstraint(self, string): | |
| #for now, assuming string is rel(p1, p2) | |
| if len(string.strip().split('(')) != 2: raise ParseError | |
| command, rest = string.strip().split('(') | |
| if command not in self.rels: return None | |
| if self.rels[command] is None: return None | |
| p1Name, p2Name = rest[:-1].split(', ') | |
| fn = self.rels[command] | |
| constraint = fn(self.people[p1Name], self.people[p2Name]) | |
| return constraint | |
| def checkConstraint(self, const_string): | |
| if const_string == "None": return self.s.check() | |
| if "; " in const_string: | |
| for constStr in const_string.split("; "): | |
| if constStr is "None": continue | |
| try: | |
| c = self.parseConstraint(constStr) | |
| except ParseError: | |
| print("parse error") | |
| continue | |
| if c is not None: self.s.add(c) | |
| return self.s.check() | |
| try: | |
| constraint = self.parseConstraint(const_string) | |
| except ParseError: | |
| print("parse error") | |
| return self.s.check() | |
| if constraint is None: return self.s.check() | |
| self.s.add(constraint) | |
| return self.s.check() | |
| def removeLast(self): | |
| self.s.pop() | |
| def findRelations(self, p1Name, p2Name): | |
| #for each relation, check if it CAN be SAT | |
| d = {} | |
| assert self.s.check().r == 1 | |
| for name, fn in self.rels.items(): | |
| self.s.push() | |
| self.s.add(fn(self.people[p1Name], self.people[p2Name])) | |
| d[name] = self.s.check().r == 1 | |
| self.s.pop() | |
| return d | |
| def findNecessaryRelations(self, p1Name, p2Name): | |
| #for each relation, check if it MUST be SAT | |
| d = {} | |
| assert self.s.check().r == 1 | |
| for name, fn in self.rels.items(): | |
| self.s.push() | |
| self.s.add(Not(fn(self.people[p1Name], self.people[p2Name]))) | |
| d[name] = self.s.check().r == -1 | |
| self.s.pop() | |
| return d | |
| def checkNecessaryConstraint(self, const_string): | |
| #TODO idk about pushing and pulling or whatever | |
| print("TODO: push/pull") | |
| constraint = self.parseConstraint(const_string) | |
| self.s.add(Not(constraint)) | |
| return self.s.check() | |
| def convertFromNL(self, nl_string): | |
| if nl_string == "None": return nl_string | |
| assert nl_string[-1] == "." | |
| nl_string = nl_string[:-1] | |
| if ". " in nl_string: | |
| cs = "" | |
| for constStr in nl_string.split(". "): | |
| c = self.convertFromNL(constStr+".") | |
| if c == "None": continue | |
| if cs is "": cs+= c #don't put semicolon for first one | |
| else: cs += "; " + c | |
| return cs | |
| # const1str, const2str = nl_string.split(". ") | |
| # c1 = self.convertFromNL(const1str+".") | |
| # c2 = self.convertFromNL(const2str+".") | |
| # if c2 == "None": return c1 | |
| # if c1 == "None": return c2 | |
| # return c1 + "; " + c2 | |
| if not " is " in nl_string: | |
| print("error parsing") | |
| return "None" | |
| if not "'s " in nl_string: | |
| print("error parsing") | |
| return "None" | |
| p1, rest = nl_string.split(" is ") | |
| if not len(rest.split("'s ")) == 2: return "None" | |
| p2, rel = rest.split("'s ") | |
| return f"{rel}({p2}, {p1})" | |
| if __name__ == '__main__': | |
| e = Env() | |
| print(e.s.check()) | |
| #for string in ['ancestor(bob, joe)', 'ancestor(joe, bob)','ancestor(joe, kevin)']: | |
| #for string in ['child(bob, joe)', 'child(joe, bob)','child(joe, kevin)', 'child(kevin, bob)', | |
| #for string in ['grand(m, m)','child(joe, kevin)', 'child(kevin, joe)', 'sibling(kevin, timmy)', 'inv_un(beth, tom)','sibling(beth, tom)', 'inv_un(jake, tom)', 'SO(jake, beth)', 'SO(jake, tom)', 'SO(jake, bob)']: | |
| for string in ['uncle(Marie, Robert)', 'father(Marie, Robert)']: | |
| sat = e.checkConstraint(string) | |
| print(string) | |
| if sat.r > 0: | |
| print("SEEMS OKAY") | |
| e.s.push() | |
| else: | |
| print(e.s.unsat_core()) | |
| assert FALSE, print("INCONSISTENT SET OF CONSTRAINTS") | |
| e.removeLast() | |
| e.s.push() | |
| print() | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment