ADD: API change stores one unique formula per model

All leaf formulae have to be instantiated with a model.
e.g. `P = Predicate("P", model=m)`
connective formulae automatically inherit the model from one of the children. All formulae nodes are automatically attached to the model graph. The model enforces unique naming for nodes attached to its graph.

- rename connective_str -> syntax
- rename node_structure -> node_syntax
- fix numbering convention of the nodes attached to the model
- fixed naming of nodes to enforce a unique node per model - based on the model syntax.

Signed-off-by: naweedkhan <naweed.khan@ibm.com>

lnn/_exceptions.py

@@ -43,11 +43,11 @@ class AssertBoundsType:
     Raised when bounds given in the incorrect type.
     """
 
-    def __init__(self, bounds: Union[Fact, tuple, torch.Tensor]):
+    def __init__(self, bounds: Union[bool, Fact, tuple, torch.Tensor]):
         options = [bool, Fact, World, tuple, torch.Tensor, float]
         if type(bounds) not in options:
             raise TypeError(
-                f"fact expected from [lnn.Fact, lnn.World, tuple, torch.Tensor] "
+                f"fact expected from [bool, lnn.Fact, lnn.World, tuple, torch.Tensor] "
                 f"received {bounds.__class__.__name__} {bounds}"
             )
 

lnn/_utils.py

@@ -4,8 +4,11 @@
 # SPDX-License-Identifier: Apache-2.0
 ##
 
-import time
+import importlib.resources
 import logging
+import logging.config
+import time
+import yaml
 from typing import Union, TypeVar, Tuple, List, Iterable
 
 from . import _exceptions
@@ -134,7 +137,7 @@ def unpack_checkpoints():
     result = list()
     for t in range(len(checkpoints) - 1):
         result.append(
-            (f"{checkpoints[t+1][1]}", checkpoints[t + 1][0] - checkpoints[t][0])
+            (f"{checkpoints[t + 1][1]}", checkpoints[t + 1][0] - checkpoints[t][0])
         )
     return result
 

lnn/model.py

@@ -105,7 +105,7 @@ def __init__(
         self.graph = nx.DiGraph()
         self.nodes = dict()
         self.node_names = dict()
-        self.node_structures = dict()
+        self.node_syntax = dict()
         self.num_formulae = 0
         self.name = name
         self.query = None
@@ -120,33 +120,27 @@ def __init__(
         self.logger = _utils.get_logger(flush=True)
         self.logger.info(f" {name} {datetime.datetime.now()} ".join(["*" * 22] * 2))
 
-    def __getitem__(
-        self, formula: Union[Formula, int]
-    ) -> Union[Formula, List[Formula]]:
+    def __getitem__(self, key: Union[Formula, int]) -> Union[Formula, List[Formula]]:
         r"""Returns a formula object from the model.
 
         If the formula is in the model, return the formula
             - for backward compatibility
-        if multiple formula exists in the model with the same structure,
+        if multiple formula exists in the model with the same syntax,
             return a list of all the relevant nodes
 
         """
-        if isinstance(formula, int):
-            return self.nodes[formula]
-        if formula.formula_number is not None and formula.formula_number in self.nodes:
-            return self.nodes[formula.formula_number]
-        if formula.structure in self.node_structures:
-            result = self.node_structures[formula.structure]
-            return (
-                result
-                if len(self.node_structures[formula.structure]) > 1
-                else result[0]
-            )
+        if isinstance(key, int):
+            return self.nodes[key]
+        if key.formula_number is not None and key.formula_number in self.nodes:
+            return self.nodes[key.formula_number]
+        if key.syntax in self.node_syntax:
+            return self.node_syntax[key.syntax]
 
     def __contains__(self, formula: Formula):
-        if formula.formula_number and formula.formula_number in self.nodes:
-            return True
-        return formula.structure in self.node_structures
+        if hasattr(formula, "formula_number"):
+            if formula.formula_number and formula.formula_number in self.nodes:
+                return True
+        return formula.syntax in self.node_syntax
 
     def set_query(self, formula: Formula, world=World.OPEN, converge=False):
         r"""Inserts a query node into the model and maintains a handle on the node.
@@ -267,18 +261,9 @@ def _add_knowledge(self, *formulae: Formula, world: World = None):
             self.graph.add_node(f)
             self.graph.add_edges_from(f.edge_list)
             self.num_formulae = f.set_formula_number(self.num_formulae) + 1
-        for node in self.graph.nodes:
-            if node.structure in self.node_structures:
-                if node not in self.node_structures[node.structure]:
-                    self.node_structures[node.structure].append(node)
-            else:
-                self.node_structures.update({node.structure: [node]})
-            if node.name in self.node_names:
-                if node not in self.node_names[node.name]:
-                    self.node_names[node.name].append(node)
-            else:
-                self.node_names.update({node.name: [node]})
-            self.nodes[node.formula_number] = node
+            self.node_syntax.update({f.syntax: f})
+            self.node_names.update({f.name: f})
+            self.nodes[f.formula_number] = f
 
         if world:
             for f in formulae:
@@ -746,8 +731,8 @@ def plot_graph(
                 [
                     (node, node.formula_number)
                     if formula_number
-                    else (node, node.connective_str)
-                    if hasattr(node, "connective_str")
+                    else (node, node.symbol)
+                    if hasattr(node, "symbol")
                     else (node, node.name)
                     for node in self.graph
                 ]

lnn/symbolic/logic/binary_neuron.py

@@ -68,7 +68,7 @@ class Implies(_BinaryNeuron):
     """
 
     def __init__(self, lhs: Formula, rhs: Formula, **kwds):
-        self.connective_str = "→"
+        self.symbol = kwds.get("symbol", "→")
         kwds.setdefault("activation", {})
         kwds["activation"].setdefault("bias_learning", True)
         super().__init__(lhs, rhs, **kwds)
@@ -114,7 +114,7 @@ class Iff(_BinaryNeuron):
     """
 
     def __init__(self, lhs: Formula, rhs: Formula, **kwds):
-        self.connective_str = "∧"
+        self.symbol = "∧"
         self.Imp1, self.Imp2 = Implies(lhs, rhs, **kwds), Implies(rhs, lhs, **kwds)
         super().__init__(self.Imp1, self.Imp2, **kwds)
         self.func = self.neuron.activation("And", direction=Direction.UPWARD)

lnn/symbolic/logic/formula.py

@@ -39,9 +39,33 @@ def _isinstance(obj, class_str) -> bool:
 class Formula(ABC):
     r"""Symbolic container for a generic formula."""
 
+    def __new__(cls, *args, **kwds):
+        instance = super(Formula, cls).__new__(cls)
+        instance.__init__(*args, **kwds)
+        return instance._add_to_model()
+
     def __init__(
-        self, *formulae: "Formula", name: Optional[str] = "", arity: int = None, **kwds
+        self,
+        *formulae: "Formula",
+        name: Optional[str] = "",
+        syntax: str = None,
+        arity: int = None,
+        **kwds,
     ):
+        # placeholder for neural variables and functions
+        self.initialised = True
+        self.neuron = None
+        self.func = None
+        self.func_inv = None
+        if not hasattr(self, "formula_number"):
+            self.formula_number = None
+        if not hasattr(self, "operands_by_number"):
+            self.operands_by_number = list()
+        self.congruent_nodes = list()
+
+        # debugging
+        self.logger = _utils.get_logger()
+
         # construct edge and operand list for each formula
         self.edge_list = list()
         self.operands: List[Formula] = list()
@@ -52,28 +76,31 @@ def __init__(
         # inherit propositional, variables, and graphs
         self.propositional: bool = kwds.get("propositional")
         self.variables: Tuple[Variable, ...] = kwds.get("variables")
-        self._inherit_from_subformulae(*formulae)
+        if not _isinstance(self, "_LeafFormula"):
+            self._inherit_from_subformulae(*formulae)
 
         # formula naming
-        if _isinstance(self, "_LeafFormula"):
-            self.structure: str = name
-            self.name: str = name
-        else:
-            self.structure: str = self._formula_structure(True)
-            self.name: str = (
-                name if name else self._formula_structure(True, lambda x: x.name)
-            )
+        self.name = name if name else ""
+        if syntax:
+            self.syntax = syntax
+            if not name:
+                self.name = syntax
+        if not self.name or not syntax:
+            self.syntax = self._formula_syntax()
+            self.name = name if name else self._formula_syntax(lambda x: x.name)
 
         # formula grounding table maps grounded objects to table rows
         self.grounding_table = None if self.propositional else dict()
 
-        # placeholder for neural variables and functions
-        self.neuron = None
-        self.func = None
-        self.func_inv = None
-        self.formula_number = None
-        self.operands_by_number = list()
-        self.congruent_nodes = list()
+    def _add_to_model(self):
+        r"""Inherits model from operands and insert the formula into the model."""
+        if not hasattr(self, "model"):
+            self.model = self.operands[0].model
+        if self not in self.model:
+            self.model.add_knowledge(self)
+            return self
+        else:
+            return self.model[self]
 
     ##
     # External function definitions
@@ -381,6 +408,7 @@ def print(
         self,
         header_len: int = 50,
         roundoff: int = 5,
+        state: bool = False,
         params: bool = False,
         grads: bool = False,
         numbering: bool = False,
@@ -441,17 +469,20 @@ def round_bounds(grounding=None):
         else:
             params = ""
         number = (
-            f"{self.formula_number} {self.operands_by_number}: "
-            if self.formula_number is not None and numbering
+            f"{self.formula_number}"
+            f"{' ' + str(self.operands_by_number) if self.operands_by_number else ''}: "
+            if numbering and self.formula_number is not None
             else ""
         )
 
         # print propositional node - single bounds
+        J = self.neuron.J if hasattr(self.neuron, "J") else ""
         if self.propositional:
             states = (
                 f"{header:<{header_len}} "
-                f"{self.state().name:>13} "
-                f"{round_bounds()}\n"
+                f"{self.state().name if state else '':>14} "
+                f"{round_bounds()}"
+                f"{f'  J: {J}' if J and str(self.neuron) == 'J()' else ''}\n"
                 f"{params}"
             )
             print(f"{number}{states}")
@@ -465,7 +496,7 @@ def round_bounds(grounding=None):
                     [
                         (
                             f"{state_wrapper(g):{header_len}} "
-                            f"{self.state(g).name:>13} "
+                            f"{self.state(g).name if state else '':>14} "
                             f"{round_bounds(g)}\n"
                         )
                         for g in self.grounding_table
@@ -700,13 +731,11 @@ def __str__(self) -> str:
         return self.name
 
     def __eq__(self, other):
-        eq_condition = (self.structure == other.structure) and (
-            self.neuron == other.neuron
-        )
+        eq_condition = (self.syntax == other.syntax) and (self.neuron == other.neuron)
         return eq_condition
 
     def __hash__(self):
-        return hash(self.structure)
+        return hash(self.syntax)
 
     def _add_groundings(self, *groundings: tuple[str]):
         r"""Adds missing groundings to `grounding_table` for those not yet stored.
@@ -739,10 +768,10 @@ def _add_groundings(self, *groundings: tuple[str]):
             {g: table_rows[i] for i, g in enumerate(missing_groundings)}
         )
 
-    def _formula_structure(self, as_int, get_str=lambda x: x.structure) -> str:
+    def _formula_syntax(self, get_str=lambda x: x.syntax, as_str: bool = True) -> str:
         r"""Determine a name for input formula(e)."""
 
-        def subformula_structure(
+        def subformula_syntax(
             subformula: Formula,
             operator: str = None,
             subformula_vars: Tuple = None,
@@ -780,7 +809,7 @@ def subformula_structure(
                     + _utils.list_to_str(
                         [
                             root_var_remap[v]
-                            if not as_int
+                            if as_str
                             else subformula.unique_var_map[root_var_remap[v]]
                             if _isinstance(subformula, "_Quantifier")
                             else self.unique_var_map[root_var_remap[v]]
@@ -799,19 +828,19 @@ def subformula_structure(
                 if _isinstance(f, "Predicate")
                 else f"{f.name}"
                 if _isinstance(f, "Proposition")
-                else f"{f.structure}"
+                else f"{f.syntax}"
                 if _isinstance(f, "_Quantifier")
                 else (
                     "("
-                    + subformula_structure(
-                        f, f.connective_str, subformula.var_remap[i], root_var_remap
+                    + subformula_syntax(
+                        f, f.symbol, subformula.var_remap[i], root_var_remap
                     )
                     + ")"
                 )
                 if _isinstance(f, "_ConnectiveNeuron")
                 else (
-                    f"{f.connective_str}"
-                    + subformula_structure(
+                    f"{f.symbol}"
+                    + subformula_syntax(
                         f, None, subformula.var_remap[i], root_var_remap
                     )
                 )
@@ -825,25 +854,18 @@ def subformula_structure(
             quantified_idxs = _utils.list_to_str(
                 [self.unique_var_map[v] for v in self.variables], ","
             )
-            return (
-                f"({self.connective_str}{quantified_idxs}, "
-                f"{subformula_structure(self)})"
-            )
+            return f"({self.symbol}{quantified_idxs}, " f"{subformula_syntax(self)})"
 
         elif _isinstance(self, "Not"):
             return (
-                f"{self.connective_str}{get_str(self.operands[0])}"
+                f"{self.symbol}{get_str(self.operands[0])}"
                 if self.propositional
-                else f"{self.connective_str}{subformula_structure(self)}"
+                else f"{self.symbol}{subformula_syntax(self)}"
             )
         return (
-            (
-                "("
-                + f" {self.connective_str} ".join([get_str(f) for f in self.operands])
-                + ")"
-            )
+            ("(" + f" {self.symbol} ".join([get_str(f) for f in self.operands]) + ")")
             if self.propositional
-            else f"({subformula_structure(self, self.connective_str)})"
+            else f"({subformula_syntax(self, self.symbol)})"
         )
 
     @staticmethod