google-styled docstrings

Author: paolomorettin

src/wmipa/core/assignmentconverter.py

@@ -11,17 +11,30 @@
 
 
 class AssignmentConverter:
-    """
-    This class is responsible of converting the pysmt assignments
-    returned by an enumerator into pairs <Polytope, Polynomial>.
-    """
+    """This class is responsible of converting the pysmt assignments returned by an enumerator into pairs <Polytope, Polynomial>."""
 
     def __init__(self, enumerator: "Enumerator") -> None:
+        """Default constructor.
+
+        Args:
+            enumerator: the enumerator instance
+        """
         self.enumerator = enumerator
 
     def convert(
         self, truth_assignment: dict[FNode, bool], domain: Collection[FNode]
     ) -> tuple[Polytope, Polynomial]:
+        """Converts a truth assignment (as returned by an Enumerator)
+        into a <Polytope, Polynomial> pair.
+
+        Args:
+            truth_assignment: mapping pysmt atoms to bool
+            domain: list of real variables in pysmt format
+
+        Returns:
+            A convex integration problem as a pair of instances of Polytope and Polynomial.
+            The two represent the convex integration bounds and integrand respectively.
+        """
 
         mgr = self.enumerator.env.formula_manager
 

src/wmipa/core/inequality.py

@@ -7,15 +7,26 @@
 
 
 class Inequality:
-    """Internal representations of inequalities in canonical form:
+    """Internal class for inequalities in the canonical form:
 
-    Polynomial {<,<=} 0
+        P {<,<=} 0
 
-    where Polynomial is also in canonical form.
+    where P is a degree 1 polynomial.
 
+    Attributes:
+        strict: boolean flag, true when the inequality is <
+        mgr: pysmt formula manager
+        polynomial: the Polynomial P
     """
 
     def __init__(self, expr: FNode, variables: Collection[FNode], env: Environment):
+        """Default constructor.
+
+        Args:
+            expr: the inequality in pysmt format
+            variables: the continuous integration domain
+            env: the pysmt environment
+        """
         if expr.is_le() or expr.is_lt():
             self.strict = expr.is_lt()
         else:
@@ -33,6 +44,11 @@ def __init__(self, expr: FNode, variables: Collection[FNode], env: Environment):
         assert self.polynomial.degree == 1
 
     def to_pysmt(self) -> FNode:
+        """Converts the inequality in pysmt format.
+
+        Returns:
+            Either a LT (less-than) or LE (less-or-equal-than) atom.
+        """
         op = self.mgr.LT if self.strict else self.mgr.LE
         return op(self.polynomial.to_pysmt(), self.mgr.Real(0))
 

src/wmipa/core/polynomial.py

@@ -12,14 +12,27 @@
 
 
 class Polynomial:
-    """Internal representation of a canonical polynomial.
+    """Internal class representing canonical polynomials.
     Implemented as a dict, having for each monomial: {key : coefficient}
     where key is a tuple encoding exponents of the ordered variables.
 
     E.g. {(2,0,1): 3} = "3 * x^2 * y^0 * z^1"
+
+    Attributes:
+        monomials: the monomial dictionary
+        variables: the continuous integration domain
+        ordered_keys: sorted list of monomial keys
+        mgr: the pysmt formula manager
     """
 
     def __init__(self, expr: FNode, variables: Collection[FNode], env: Environment):
+        """Default constructor.
+
+        Args:
+            expr: the polynomial in pysmt format
+            variables: the continuous integration domain
+            env: the pysmt environment
+        """
         self.monomials = PolynomialParser(variables).parse(expr)
         const_key = tuple(0 for _ in range(len(variables)))
         if const_key in self.monomials and self.monomials[const_key] == 0:
@@ -30,12 +43,17 @@ def __init__(self, expr: FNode, variables: Collection[FNode], env: Environment):
 
     @property
     def degree(self) -> int:
+        """Returns the degree of the polynomial."""
         if len(self.monomials) == 0:
             return 0
         else:
             return max(sum(exponents) for exponents in self.monomials)
 
     def to_numpy(self) -> Callable[[np.ndarray], np.ndarray]:
+        """Returns the polynomial as a callable function.
+
+        This function can be used to evaluate a numpy array.
+        """
         return lambda x: np.sum(
             np.array(
                 [k * np.prod(np.pow(x, e), axis=1) for e, k in self.monomials.items()]
@@ -44,7 +62,7 @@ def to_numpy(self) -> Callable[[np.ndarray], np.ndarray]:
         )
 
     def to_pysmt(self) -> FNode:
-
+        """Returns the polynomial in pysmt format."""
         if len(self.monomials) == 0:
             return self.mgr.Real(0)
 
@@ -156,7 +174,7 @@ def _sum_polys(mono_first: Monomials, mono_second: Monomials) -> Monomials:
 
     @staticmethod
     def _multiply_polys(mono_first: Monomials, mono_second: Monomials) -> Monomials:
-        """Multiply two polynomials represented as monomial dictionaries."""
+        """Multiplies two polynomials represented as monomial dictionaries."""
         result = {}
         n = (
             len(next(iter(mono_first.keys())))
@@ -178,7 +196,7 @@ def _multiply_polys(mono_first: Monomials, mono_second: Monomials) -> Monomials:
 
     @classmethod
     def _expand_power(cls, base_poly: Monomials, exp_val: int) -> Monomials:
-        """Expand (polynomial)^n by repeated multiplication."""
+        """Expands (polynomial)^n by repeated multiplication."""
         if exp_val == 0:
             n = len(next(iter(base_poly.keys())))
             return {tuple(0 for _ in range(n)): 1}

src/wmipa/core/polytope.py

@@ -8,17 +8,28 @@
 
 
 class Polytope:
-    """Internal data structure for H-polytopes."""
+    """Internal class for convex H-polytopes.
+
+    Attributes:
+        inequalities: list of wmipa.core.Inequality
+        N: the number of variables
+    """
 
     def __init__(
         self,
         expressions: Collection[FNode],
         variables: Collection[FNode],
         env: Environment,
     ):
+        """Default constructor for a H-polytope defined on an ordered list of variables (the continuous integration domain).
+
+        Args:
+           expressions: list of linear inequalities in pysmt format
+           variables: the continuous integration domain
+           env: the pysmt environment
+        """
         self.inequalities = [Inequality(e, variables, env) for e in expressions]
         self.N = len(variables)
-        self.H = len(expressions)
         self.mgr = env.formula_manager
 
     def to_pysmt(self) -> FNode:
@@ -28,8 +39,15 @@ def to_pysmt(self) -> FNode:
         return self.mgr.And(*map(lambda x: x.to_pysmt(), self.inequalities))
 
     def to_numpy(self) -> tuple[np.ndarray, np.ndarray]:
-        """Returns two numpy arrays A, b encoding the polytope.
-        (Non-)Strictness information is discarded."""
+        """Converts the polytope to a pair of numpy arrays.
+
+        Note: information on the strictness of each inequality is discarded.
+
+        Returns:
+            Two numpy arrays A, b encoding the polytope
+
+              A x {<=/<} b
+        """
         A, b = [], []
         const_key = tuple(0 for _ in range(self.N))
         key = lambda i: tuple(1 if j == i else 0 for j in range(self.N))

src/wmipa/core/utils.py

@@ -1,9 +1,4 @@
-"""This module implements some useful methods used throughout the code.
-
-Credits: least common multiple code by J.F. Sebastian
-    (http://stackoverflow.com/a/147539)
-
-"""
+"""This module implements some useful methods used throughout the code."""
 
 from collections import defaultdict
 from typing import Any
@@ -17,20 +12,24 @@
 
 
 def is_atom(node: FNode) -> bool:
+    """Returns true iff node is a propositional or theory atom."""
     return node.is_symbol(BOOL) or node.is_theory_relation()
 
 
 def is_literal(node: FNode) -> bool:
+    """Returns true iff node is an atom or its negation."""
     return is_atom(node) or (node.is_not() and is_atom(node.arg(0)))
 
 
 def is_clause(formula: FNode) -> bool:
+    """Returns true iff formula is a disjuction of literals."""
     return is_literal(formula) or (
         formula.is_or() and all(is_literal(lit) for lit in formula.args())
     )
 
 
 def is_cnf(formula: FNode) -> bool:
+    """Returns true iff formula is in Conjunctive Normal Form."""
     return is_clause(formula) or (
         formula.is_and() and all(is_clause(c) for c in formula.args())
     )
@@ -40,7 +39,6 @@ class LiteralNormalizer:
     """A helper class for normalizing literals. This class is useful
     whenever literals involving algebraic atoms are manipulated by an
     external procedure, such as an SMT-based enumerator.
-
     """
 
     def __init__(self, env: Environment):
@@ -60,35 +58,34 @@ def _normalize(self, literal: FNode) -> FNode:
             self._cache[literal] = normalized_literal
         return self._cache[literal]
 
-    def normalize(self, phi: FNode, remember_alias: bool = False) -> tuple[FNode, bool]:
-        """Return a normalized representation of a literal.
+    def normalize(self, literal: FNode, remember_alias: bool = False) -> tuple[FNode, bool]:
+        """Normalizes 'literal', possibly storing original formula in the alias dictionary.
 
         Args:
-            phi (FNode): The formula to normalize.
-            remember_alias (bool): If True, the original formula is remembered to be an alias of its normalized version.
+            literal: the literal in pysmt format
+            remember_alias: store 'literal' as an alias (def: False)
 
         Returns:
-            FNode: The normalized formula.
-            bool: True if the formula was negated, False otherwise.
+            A normalized atom plus a Boolean that indicates if the normalized literal was negative.
         """
-        normalized_phi = self._normalize(phi)
-        negated = False
-        if normalized_phi.is_not():
-            normalized_phi = normalized_phi.arg(0)
-            negated = True
+        normalized_literal = self._normalize(literal)
+        negative = False
+        if normalized_literal.is_not():
+            normalized_literal = normalized_literal.arg(0)
+            negative = True
         if remember_alias:
-            self._known_aliases[normalized_phi].add((phi, negated))
-        return normalized_phi, negated
+            self._known_aliases[normalized_literal].add((literal, negative))
+        return normalized_literal, negative
 
     def known_aliases(self, literal: FNode) -> set[tuple[FNode, bool]]:
-        """Return the set of known aliases of the literal.
-
-        Args:
-            literal (FNode): The literal to check.
+        """Maps back a normalized atom into the original ones (multiple literals might map into the same normalized literal).
 
         Returns:
-            set(tuple(FNode, bool)): The set of known aliases of the literal. Each alias is a tuple containing the
-                normalized literal and a boolean indicating whether the alias is negated.
+            The set of known aliases for a normalized (positive) 'literal'.
+
+            Each alias is a tuple containing:
+            - the original literal
+            - the Boolean flag 'negative'
         """
         if literal not in self._known_aliases:
             known_aliases_str = "\n".join(str(x) for x in self._known_aliases.keys())