From 1f380c86193aae170247989fc549c58dd4a11cfc Mon Sep 17 00:00:00 2001 From: Spencer Killen Date: Wed, 29 Jun 2022 16:06:09 -0600 Subject: [PATCH] working from campus --- Makefile | 0 __pycache__/ontology.cpython-39.pyc | Bin 1096 -> 1298 bytes example.py | 30 ++++++++++ ontology.py | 15 +++-- programs/a.lp | 4 ++ programs/a.py | 1 + programs/b.lp | 2 + programs/b.py | 6 ++ propagator.py | 82 ++++++++++++++++++---------- tests.py | 20 +++++++ 10 files changed, 126 insertions(+), 34 deletions(-) create mode 100644 Makefile create mode 100644 example.py create mode 100644 programs/b.lp create mode 100644 programs/b.py create mode 100644 tests.py diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..e69de29 diff --git a/__pycache__/ontology.cpython-39.pyc b/__pycache__/ontology.cpython-39.pyc index 5253117280042373ac94fd1ee55b7e4c63c18945..e77b37255be579d868c6d7e19a4f2ab87de73aec 100644 GIT binary patch delta 677 zcmY*XyKWOf6utM(uCv~}j1@T>h)6?Y7cNpzAj?&nl*oc&8?^R}A!Kcb*$G0CQHn$& zG)Q4nQa}L`h)>`H_yjcK2lxx_jIBj%apugqkC}64e@5@)jck2A2L3+Z{1`UG^~UbG z;hhADIZQCc38gd?&|drFE|Ro`jSh{{*)UgD43x3qqv_FXdj0JSZk7-6qFduMy;(tn znT-o&o=j#^x37RkU3-H%PXwpQ?Hw9D2!5YT%L{ykfDWgGSQ;ZAeaN6zq_w{ z7cx##p{%ZeeER+je$j{9rj2#!m(VD_p#!ZVpsyQlsn(FafLtzxhGtC!9df?-qMKWb znl2$IHWHV))H{ckX^On;JUJSUxkxi*9}i@f|9S?xr%@bQ>yr-B9w7W5%`J>wjBEkn znmm#mp5O*qPA^E8NIfEYtYVU-zcjDT?1WWi_xhrDsyE0O0s#-?8s^YbmHg^#5RXnI z#kP2 Set[str]: atoms = atoms.intersection(DL_ATOMS) - sub_models = (model for model in models if atoms <= model) - first: set = next(sub_models, None) + sup_models = (model for model in models if atoms <= model) + first: set = next(sup_models, None) if first is None: return set() - return first.intersection(*sub_models) + return first.intersection(*sup_models) -def check(atoms: Set[str]) -> bool: +def check(atoms: Set[str]) -> Union[Set[str], None]: atoms = atoms.intersection(DL_ATOMS) - return atoms in models + if atoms not in models: + return None + sub_models = (model for model in models if model < atoms) + return atoms - atoms.intersection(*sub_models) diff --git a/programs/a.lp b/programs/a.lp index e69de29..b075e53 100644 --- a/programs/a.lp +++ b/programs/a.lp @@ -0,0 +1,4 @@ +a :- not b. +b :- not a. + + diff --git a/programs/a.py b/programs/a.py index ea92ebc..0e3a59b 100644 --- a/programs/a.py +++ b/programs/a.py @@ -1,5 +1,6 @@ "ab" ( +"", "a", "b", "ab", diff --git a/programs/b.lp b/programs/b.lp new file mode 100644 index 0000000..c655f1d --- /dev/null +++ b/programs/b.lp @@ -0,0 +1,2 @@ +a :- not b. +b :- not a. diff --git a/programs/b.py b/programs/b.py new file mode 100644 index 0000000..ea92ebc --- /dev/null +++ b/programs/b.py @@ -0,0 +1,6 @@ +"ab" +( +"a", +"b", +"ab", +) \ No newline at end of file diff --git a/propagator.py b/propagator.py index 6a91ee0..d9ae52b 100644 --- a/propagator.py +++ b/propagator.py @@ -1,7 +1,7 @@ from itertools import chain -from typing import Iterable, List, Set, Tuple +from typing import Iterable, Iterator, List, Set, Tuple import clingo -from more_itertools import partition +from more_itertools import partition, unique_everseen from clingo import ( PropagateControl, PropagateInit, @@ -10,7 +10,10 @@ from clingo import ( Assignment, Symbol, ) +from functools import partial +from sys import stderr +eprint = partial(print, file=stderr) """ API notes: @@ -51,12 +54,14 @@ class OntologyPropagator: # Could add these with additional rules, but I think that will change the semantics of the O atoms. # An ontology atom must be true if it's regular counterpart is also true # The opposite direction is already enforced by rules. - for theory_atom in self.theory_atoms_inv: - theory_lit = self.theory_atoms_inv[theory_atom] - symbolic_lit = self.symbolic_atoms_inv[theory_atom] + # for theory_atom in self.theory_atoms_inv: + # theory_lit = self.theory_atoms_inv[theory_atom] + # symbolic_lit = self.symbolic_atoms_inv[theory_atom] - # This is already implied if the symbolic and theory literals are the same - init.add_clause((-symbolic_lit, theory_lit)) + # # This is already implied if the symbolic and theory literals are the same + # init.add_clause((-symbolic_lit, theory_lit)) + + assert len(set(self.symbolic_atoms) & set(self.theory_atoms)) == 0 def truthy_atoms_text(self): return ( @@ -80,19 +85,19 @@ class OntologyPropagator: ) def print_nogood(self, nogood: Tuple[int, ...]): - print("adding nogood: ", end="") + eprint("adding nogood: ", end="") names = ( self.symbolic_atoms.get(abs(lit), self.theory_atoms.get(abs(lit))) for lit in nogood ) - print( + eprint( " ".join( f"(not {name})" if lit < 0 else f"({name})" for lit, name in zip(nogood, names) ) ) - def assign_nogood_true(self, pcontrol: PropagateControl, lits: Iterable[int]): + def assign_nogood(self, pcontrol: PropagateControl, lits: Iterable[int]): not_lits = set(-lit for lit in lits) assert len(not_lits) assignment = set(self.assignment_lits()) @@ -108,7 +113,7 @@ class OntologyPropagator: return (lit if is_pos else -lit for lit, is_pos in self.assignment.items()) def conflict(self, pcontrol: PropagateControl): - print("conflict: ", end="") + eprint("conflict: ", end="") self.print_assignment() pcontrol.add_nogood(self.assignment_lits()) @@ -120,10 +125,12 @@ class OntologyPropagator: in_atoms = set(self.truthy_atoms_text()) - print("made truthy: ", " ".join(in_atoms)) + eprint("made truthy: ", " ".join(in_atoms)) - out_atoms = set(self.atom_text_to_dl_atom(O.propagate(in_atoms))) + out_atoms = set(O.propagate(in_atoms)) + # This is sort of special in that regular atoms won't propagate their ontology counterparts. new_atoms = out_atoms - in_atoms + new_atoms = set(self.atom_text_to_dl_atom(new_atoms)) l = lambda atom: atom in self.assignment new_atoms, prev_new_atoms = map(tuple, partition(l, new_atoms)) @@ -131,11 +138,11 @@ class OntologyPropagator: if any(not self.assignment[atom] for atom in prev_new_atoms): self.conflict(pcontrol) elif len(new_atoms): - self.assign_nogood_true(pcontrol, new_atoms) + self.assign_nogood(pcontrol, new_atoms) else: return pcontrol.propagate() - print("propagate: ", end="") + eprint("propagate: ", end="") self.print_assignment() def undo(self, thread_id: int, assignment: Assignment, changes: List[int]): @@ -143,19 +150,38 @@ class OntologyPropagator: atom = abs(change) del self.assignment[atom] + def lits_to_text(self, lits: Iterable[int]) -> Iterable[str]: + return ( + self.symbolic_atoms.get(abs(lit), self.theory_atoms.get(abs(lit))) + for lit in lits + ) + def check(self, pcontrol: PropagateControl) -> None: - print("check: ", end="") + eprint("check: ", end="") self.print_assignment() in_atoms = set(self.truthy_atoms_text()) - if not O.check(in_atoms): + + shrink = O.check(in_atoms) + if shrink is None: self.conflict(pcontrol) + return + shrink = tuple(self.theory_atoms_inv[atom] for atom in shrink) + if any(self.assignment.get(abs(lit)) for lit in shrink): + self.conflict(pcontrol) + return + + eprint("shrink with: ", " ".join(self.lits_to_text(shrink))) + for lit in shrink: + self.assign_nogood(pcontrol, (-lit,)) + + def print_assignment(self): - print("assignment: ", end="") + eprint("assignment: ", end="") for lit in self.assignment: lit = -lit if not self.assignment[lit] else lit - print(self.solver_lit_text(lit), end=" ") - print() + eprint(self.solver_lit_text(lit), end=" ") + eprint() def is_theory_atom(self, lit: int): _, _, a = self.lookup_solver_lit(lit) @@ -204,11 +230,11 @@ def add_external_atoms(program: str) -> str: def solve(program: str, O_alphabet: Iterable[str], O_models: Iterable[Iterable[str]]): O.set_models(O_alphabet, O_models) program = add_external_atoms(program) - print("USING ONTOLOGY WITH ALPHABET AND MODELS:") - print(O_alphabet) - print(O_models) - print("USING PROGRAM:") - print(program) + eprint("USING ONTOLOGY WITH ALPHABET AND MODELS:") + eprint(O_alphabet) + eprint(O_models) + eprint("USING PROGRAM:") + eprint(program) control = clingo.Control(["0"]) propagator = OntologyPropagator() control.register_propagator(propagator) @@ -219,13 +245,13 @@ def solve(program: str, O_alphabet: Iterable[str], O_models: Iterable[Iterable[s with control.solve(yield_=True) as solve_handle: for model in solve_handle: - print("answer set:", model) + eprint("answer set:", model) answer_sets.append(str(model)) - print() + eprint() if len(answer_sets): print("ALL FINISHED, ALL ANSWER SETS:") - print(*answer_sets, sep="\n") + print(*unique_everseen(answer_sets), sep="\n") else: print("ALL DONE, NO ANSWER SETS") diff --git a/tests.py b/tests.py new file mode 100644 index 0000000..426ae83 --- /dev/null +++ b/tests.py @@ -0,0 +1,20 @@ +#!/usr/bin/env python3 + +from glob import glob +from os import system +from functools import partial +from sys import argv, stderr +from os.path import splitext + + +eprint = partial(print, file=stderr) + +if len(argv) >= 2 and argv[1] == "-a": + accept = True +else: + accept = False + +system("mkdir -p tests") + +for lp in glob("programs/*.lp"): + base = splitext(lp)[0]