From 99a9a6e6a1c659b6ca563f61bdb262877f6982f0 Mon Sep 17 00:00:00 2001 From: Spencer Killen Date: Mon, 27 Jun 2022 17:26:35 -0600 Subject: [PATCH] stash --- .vscode/settings.json | 3 +- __pycache__/ontology.cpython-39.pyc | Bin 0 -> 791 bytes ontology.py | 1 + propagator.py | 95 +++++++++++++++++++++------- 4 files changed, 75 insertions(+), 24 deletions(-) create mode 100644 __pycache__/ontology.cpython-39.pyc diff --git a/.vscode/settings.json b/.vscode/settings.json index afb940f..e4a1c31 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,3 +1,4 @@ { - "discord.enabled": true + "discord.enabled": true, + "python.formatting.provider": "black" } \ No newline at end of file diff --git a/__pycache__/ontology.cpython-39.pyc b/__pycache__/ontology.cpython-39.pyc new file mode 100644 index 0000000000000000000000000000000000000000..2f92e0e31c2d0d95750745d922778a38e761ee3b GIT binary patch literal 791 zcmZ8gy^a$x5T5b=+$Q8Ch!B6`1-7^Z3Cbt}aU}$#Ac{!nv{^epm(4n7J3!E;%1Io} zJpl!XDvv-%%LCB3rJ|;zf$=6p9G2#@XLkI}=NWCXzh4DfU%r0se?x%p&iQwFK{QpKyRZCcI-`uyg1I0!4TeHpspAjQcz|^?Q5UcvQwhzDKbNkGc?7 zeh@3fXuYm5ZCA@;VzF;AjhPJ+Bd6MiN|?FIQbJHaTbT0Stb`ckmVl$dR+t z$go3L;S!BkAcqxOvVw7#gSuz@6?CCs$57xoono(Zfu3#Y@6xVs5ft#EzQi+1pP*s| zJ_m#oBJ08$J8K}ZtZ~N%Q^`fPMitT(RU!BlH(yCL(X%8Kx|wFX8th~Bm|F2HeqAtuc T(RT8+`wMDb_}llZ>_+ql&|0Y! literal 0 HcmV?d00001 diff --git a/ontology.py b/ontology.py index 960b4ed..4ef5a7b 100644 --- a/ontology.py +++ b/ontology.py @@ -17,3 +17,4 @@ def propagate(atoms: Set[str]) -> Set[str]: def check(atoms: Set[str]) -> bool: atoms = atoms.intersection(DL_ATOMS) return atoms in models + diff --git a/propagator.py b/propagator.py index 97fbaeb..fbd250c 100644 --- a/propagator.py +++ b/propagator.py @@ -1,9 +1,29 @@ from copy import deepcopy from itertools import chain -from operator import itemgetter +from operator import getitem from typing import Iterable, List, Tuple +from functools import partial import clingo -from clingo import PropagateControl, PropagateInit, PropagateControl, PropagatorCheckMode, Assignment, Symbol, Control, TheoryAtom +from clingo import ( + PropagateControl, + PropagateInit, + PropagateControl, + PropagatorCheckMode, + Assignment, + Symbol, + Control, + TheoryAtom, +) + + +""" +API notes: +add_clause is disjunctive +add_nogood is conjunctive + +defined appear in a rule head +No way to strict atoms except through adding nogoods/clauses? +""" import ontology as O @@ -11,7 +31,7 @@ import ontology as O class Ontology: def init(self, init: PropagateInit) -> None: init.check_mode = PropagatorCheckMode.Total - + self.assignment = dict() self.symbolic_atoms = { @@ -22,37 +42,68 @@ class Ontology: init.solver_literal(atom.literal): atom.elements[0].terms[0].name for atom in init.theory_atoms } - self.symbolic_atoms_inv = { v: k for k, v in self.symbolic_atoms.items() } - self.theory_atoms_inv = { v: k for k, v in self.theory_atoms.items() } - + self.symbolic_atoms_inv = {v: k for k, v in self.symbolic_atoms.items()} + self.theory_atoms_inv = {v: k for k, v in self.theory_atoms.items()} # Might only need to watch just theory atoms / just symbol atoms but for now - # watching everything is easier + # watching everything is easier for lit in chain(self.symbolic_atoms, self.theory_atoms): init.add_watch(lit) + # 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] + + init.add_clause((-symbolic_lit, theory_lit)) def truthy_atoms_text(self): - return (str(self.lookup_solver_lit(atom)[0]) for atom in self.assignment if self.assignment[atom]) + return ( + str(self.lookup_solver_lit(atom)[0]) + for atom in self.assignment + if self.assignment[atom] + ) def atom_text_to_dl_atom(self, atoms: Iterable[str]) -> Iterable[int]: - return map(self.theory_atoms.get, atoms) + return ( + lit + for atom in atoms + if (lit := self.theory_atoms_inv.get(atom)) is not None + ) def falsey_atoms_text(self): - return (str(self.lookup_solver_lit(atom)[0]) for atom in self.assignment if not self.assignment[atom]) + return ( + str(self.lookup_solver_lit(atom)[0]) + for atom in self.assignment + if not self.assignment[atom] + ) + + def assign_nogood_true(self, pcontrol: PropagateControl, lits: Iterable[int]): + not_lits = (-lit for lit in lits) + assignment = ( + lit if is_pos else -lit + for lit, is_pos in chain( + self.symbolic_atoms.items(), self.theory_atoms.items() + ) + ) + pcontrol.add_nogood(chain(assignment, not_lits)) def propagate(self, pcontrol: PropagateControl, changes) -> None: + print("propagate: ", end="") + self.print_assignment() for change in changes: atom = abs(change) assert atom not in self.assignment self.assignment[atom] = change >= 0 - + in_atoms = set(self.truthy_atoms_text()) - out_atoms = self.atom_text_to_dl_atom(O.propagate()) + out_atoms = set(self.atom_text_to_dl_atom(O.propagate(in_atoms))) new_atoms = out_atoms - in_atoms - new_lits = self.atom_text_to_dl_atom(new_atoms) - + self.assign_nogood_true(pcontrol, new_atoms) + pcontrol.propagate() def undo(self, thread_id: int, assignment: Assignment, changes: List[int]): for change in changes: @@ -60,9 +111,9 @@ class Ontology: del self.assignment[atom] def check(self, pcontrol: PropagateControl) -> None: + print("check: ", end="") self.print_assignment() - def print_assignment(self): print("assignment: ", end="") for lit in self.assignment: @@ -82,7 +133,6 @@ class Ontology: neg = "not " if is_neg else "" return f"({theory}{neg}{symbol})" - def lookup_solver_lit(self, lit: int) -> Tuple[Symbol, bool, bool]: atom = abs(lit) if (atom_symb := self.symbolic_atoms.get(atom, None)) is not None: @@ -92,10 +142,9 @@ class Ontology: return None, False, False -program=""" +program = """ a :- not b. b :- not a. -c :- not d. """ # Need to ground program before we can look up symbolic atoms and @@ -103,7 +152,7 @@ c :- not d. # So we parse and ground and then revert back to text then reparse def add_external_atoms(program: str) -> str: control = clingo.Control(["0"]) - control.add("base", [], program) + control.add("base", [], program.replace("\n", "")) control.ground([("base", [])]) theory_grammar = """ @@ -111,15 +160,16 @@ def add_external_atoms(program: str) -> str: kterm {- : 0, unary }; &o/0 : kterm, any }. - """ +""" external_atoms = "\n".join( - f"{atom} :- &o{{{atom}}}." for atom in - (str(atom.symbol) for atom in control.symbolic_atoms) + f"{atom} :- &o{{{atom}}}." + for atom in (str(atom.symbol) for atom in control.symbolic_atoms) ) return theory_grammar + program + external_atoms program = add_external_atoms(program) +print(program) control = clingo.Control(["0"]) propagator = Ontology() control.register_propagator(propagator) @@ -133,4 +183,3 @@ control.ground([("base", [])]) with control.solve(yield_=True) as solve_handle: for model in solve_handle: print("answer set:", model) -