Merge branch 'clean-code' into main

CHANGES.rst

@@ -3,6 +3,28 @@
 CHANGES
 =======
 
+Version 2.0.4 - 2023-11-04
+--------------------------
+
+Deprecated
+^^^^^^^^^^
+
+- propnize() and reduce() have been deprecated and will be removed in v3.0.0.
+
+
+Changed
+^^^^^^^
+
+- Renamed propnize() to perform_boolean_encoding().
+- Renamed reduce() to reduce_formula().
+- Renamed class variable bipartite_order to partitioning_order.
+
+Cleaned
+^^^^^^^
+
+- Changed code so that partitioning_order is not accessed outside binop_batch().
+
+
 Version 2.0.3 - 2023-11-04
 --------------------------
 

docs/examples.rst

@@ -33,7 +33,7 @@ The CNF encoded from ``f`` is generated to ``f.cnf`` in
 
     st = GrSt(vertex_list, edge_list, encoding="edge", prefix="V")
     f = Fog.read("(~ edg(x1,x2)) & (~ edg(x1,x3)) & (~ edg(x2,x3)) & (~ x1=x2) & (~ x1=x3) & (~ x2=x3)")
-    g = op.propnize(f, st)
+    g = op.perform_boolean_encoding(f, st)
 
     tup  = tuple([st.compute_domain_constraint(v) \
                     for v in op.get_free_vars(f)])

docs/getting-started.rst

@@ -55,7 +55,7 @@ The encoding performed here is described in more details in
 
 .. code:: python
 
-    g = op.propnize(f, st)
+    g = op.perform_boolean_encoding(f, st)
     tup  = tuple([st.compute_domain_constraint(v) \
                     for v in op.get_free_vars(f)])
     mgr = Cnf( (g, ) + tup , st)

docs/howto-use-pygplib.rst

@@ -51,23 +51,23 @@ as being right associative, is recognized to be a different formula from
    fff = Fog.read("((~ edg(x1, x2)) & ((~ edg(x1, x3)) & (~ edg(x2, x3))))")
    assert f != fff
 
-Note: when the class variables ``bipartite_order`` of ``Prop`` class and  
+Note: when the class variables ``partitioning_order`` of ``Prop`` class and  
 ``Fog`` class are set ``True``, binary operations for these class objects 
 with equal priority are associated, recursively halving them.
 
 .. code:: python
 
-    Fog.bipartite_order = False
+    Fog.partitioning_order = False
     f = Fog.read("T & T & T & T")
     assert op.to_str(f) == "(((T & T) & T) & T)"
-    Fog.bipartite_order = True
+    Fog.partitioning_order = True
     f = Fog.read("T & T & T & T")
     assert op.to_str(f) == "((T & T) & (T & T))"
-    Fog.bipartite_order = False
+    Fog.partitioning_order = False
 
-Similarly, when ``Prop.bipartite_order`` is set ``True``, 
-``Prop`` objects computed by ``propnize()`` and ``compute_domain_constraint()`` 
-become syntactically different expressions.
+Similarly, when ``Prop.partitioning_order`` is set ``True``, 
+``Prop`` objects computed by ``perform_boolean_encoding()`` 
+and ``compute_domain_constraint()`` become syntactically different expressions.
 
 Name and Index of Symbol
 ^^^^^^^^^^^^^^^^^^^^^^^^
@@ -160,14 +160,14 @@ are listed below.
 -  ``print_formula(f, stream=out, fmt=type)`` prints out formula object in
    stream (stdout if not given) in human-readable format (fmt=“str”) or
    DOT format (fmt=“dot”).
--  ``reduce(f)`` returns the result reduced from ``f`` with equivalent
+-  ``reduce_formula(f)`` returns the result reduced from ``f`` with equivalent
    transformations to make it be as simple as possible.
 -  ``get_free_vars_and_consts(f)`` returns a tuple of all
    free variables and constants of ``f``.
 -  ``get_free_vars(f)`` returns a tuple of the indices of all free
    variables of ``f``.
--  ``propnize(f, st)`` returns an equivalent propositional formula of
-   first-order formula ``f``, given graph structure. 
+-  ``perform_boolean_encoding(f, st)`` returns an equivalent propositional 
+   formula of first-order formula ``f``, given graph structure. 
    **Note: since this method performs quantifier elimination, 
    it would take much time and space if a
    formula contains quantifiers and a graph is large.**
@@ -181,16 +181,16 @@ are listed below.
 
 As mentioned, we assume that a graph has no loop, and hence the formula
 written as ``edg(x, x)`` is unsatisfiable.
-The formula is evaluated to false constant by ``op.reduce()`` just like
+The formula is evaluated to false constant by ``op.reduce_formula()`` just like
 ``eval()`` does in arithmetic expression.
 
 .. code:: python
 
    f = Fog.read("edg(x, x)")
    assert f != Fog.true_const() 
-   assert op.reduce(f) == Fog.false_const()
+   assert op.reduce_formula(f) == Fog.false_const()
 
-However, ``op.reduce()`` only performs a few equivalent transformations 
+However, ``op.reduce_formula()`` only performs a few equivalent transformations 
 and the resulted formula not always becomes irreducible, as demonstrated 
 in the following code block.
 
@@ -358,7 +358,7 @@ It is then converted to a tuple of propositional formulas
 
     f = Fog.read("(~ edg(x1,x2)) & (~ edg(x1,x3)) & (~ edg(x2,x3))")
 
-    g = op.propnize(f, st)
+    g = op.perform_boolean_encoding(f, st)
     tup  = tuple([st.compute_domain_constraint(v) \
                     for v in op.get_free_vars(f)])
 

examples/bmc.py

@@ -181,13 +181,13 @@ def __init__(
             else:
                 raise Exception(f"trans_type={trans_type} is undefined")
 
-        self._prop_ini = op.propnize(ini_expr, self.st)
+        self._prop_ini = op.perform_boolean_encoding(ini_expr, self.st)
         """propositional formula of initial state"""
-        self._prop_fin = op.propnize(fin_expr, self.st)
+        self._prop_fin = op.perform_boolean_encoding(fin_expr, self.st)
         """propositional formula of final state"""
-        self._prop_state = op.propnize(state_expr, self.st)
+        self._prop_state = op.perform_boolean_encoding(state_expr, self.st)
         """propositional formula of each state"""
-        self._prop_trans = op.propnize(trans_expr, self.st)
+        self._prop_trans = op.perform_boolean_encoding(trans_expr, self.st)
         """propositional formula of transition relations of adjacent states"""
 
         self._state_size = self._nof_free_vars * st.code_length
@@ -286,10 +286,10 @@ def generate_cnf(
             self._curr_vars, ini_expr, fin_expr, self.st
         )
         if ini_expr is not None:
-            self._prop_ini = op.propnize(ini_expr, self.st)
+            self._prop_ini = op.perform_boolean_encoding(ini_expr, self.st)
 
         if fin_expr is not None:
-            self._prop_fin = op.propnize(fin_expr, self.st)
+            self._prop_fin = op.perform_boolean_encoding(fin_expr, self.st)
 
         self._total_state_size = self._state_size * (bound + 1)
         self.nvar = self._total_state_size

pygplib/absexpr.py

@@ -64,8 +64,8 @@ class AbsExpr:
     """
 
     _unique_table = {}
-    bipartite_order = False
-    """enables bipartite order of applying operations"""
+    partitioning_order = False
+    """changes order of applying binary operations (see binop_batch())"""
 
     # Tag-related Variables and Methods
     _ATOM_TAGS = ()
@@ -177,7 +177,8 @@ def gen_key(self) -> str:
         """
         return type(self)._to_key(self._tag, self._left, self._right, self._aux)
 
-    def compute_nnf_step(self, negated: bool, s: list[list], t: list[list]) -> None:
+    def compute_nnf_step(self, negated: bool, s: list[list], t: list[list])\
+        -> None:
         """Performs NNF compuation for this object."""
         assert False, f"{self.gen_key()}"
 
@@ -186,7 +187,7 @@ def compute_cnf_step(self, igen: IndexGen, \
         """Performs CNF compuation for this object."""
         assert False, f"{self.gen_key()}"
 
-    def reduce_step(self, assoc: dict, st: BaseRelSt) -> None:
+    def reduce_formula_step(self, assoc: dict, st: BaseRelSt) -> None:
         """Performs reduce compuation for this object."""
         assert False, f"{self.gen_key()}"
 

pygplib/absfo.py

@@ -201,7 +201,7 @@ def substitute_step(self, y: int, x: int, assoc: dict) -> None:
 
         assert False
 
-    def reduce_step(self, assoc: dict, st: BaseRelSt) -> None:
+    def reduce_formula_step(self, assoc: dict, st: BaseRelSt) -> None:
         """Performs reduce compuation for this object."""
 
         if self.is_forall_term():
@@ -248,7 +248,7 @@ def reduce_step(self, assoc: dict, st: BaseRelSt) -> None:
             assoc[id(self)] = type(self).exists(g, bvar)
             return
 
-        super().reduce_step(assoc, st)
+        super().reduce_formula_step(assoc, st)
 
     def make_str_pre_step(self) -> str:
         """Makes string in prefix order for this object."""

pygplib/absneg.py

@@ -116,7 +116,7 @@ def compute_cnf_step(self, igen: IndexGen, \
         ), "compute_cnf_step() assumes reduced formulas"
         super().compute_cnf_step(igen, assoc, cnf)
 
-    def reduce_step(self, assoc: dict, st: BaseRelSt) -> None:
+    def reduce_formula_step(self, assoc: dict, st: BaseRelSt) -> None:
         """Performs reduce computation for this object."""
         if self.is_neg_term():
             g = assoc[id(self.get_operand(1))]
@@ -131,7 +131,7 @@ def reduce_step(self, assoc: dict, st: BaseRelSt) -> None:
         if self.is_true_atom() or self.is_false_atom():
             assoc[id(self)] = self
             return
-        super().reduce_step(assoc, st)
+        super().reduce_formula_step(assoc, st)
 
     def make_str_pre_step(self) -> str:
         """Makes string in prefix order for this object."""

pygplib/absprop.py

@@ -1,5 +1,8 @@
 """Class of propositional logic with true and false and no variable"""
 
+import warnings
+import functools
+
 from .absexpr import AbsExpr
 from .absexpr import IndexGen
 from .absneg  import AbsNeg
@@ -111,16 +114,22 @@ def binop(cls, tag: str, left: AbsExpr, right: AbsExpr) -> AbsExpr:
 
     @classmethod
     def binop_batch(cls, tag: str, expr_li: list) -> AbsExpr:
-        """Gets the formula obtained from a list of formulas by recursively
-        applying operation to the left and the right halves of the list.
+        """Gets the formula obtained from a list of formulas by applying
+        operations.
+
+        If partitioning_order is set True, operations are recusively applied 
+        by partitioning operands into the left and the right halves.
+        Otherwise, operations are iteratively applied in a left-associative way. 
 
         Args:
             tag:    tag of AND or OR operation
             expr_li:   list of operands
         """
+        if tag not in [cls.get_land_tag(), cls.get_lor_tag()]:
+            raise Exception(\
+                f"Operation specified by {tag} cannot be done in batch.")
         if len(expr_li) == 0:
             raise ValueError("Expression list is empty.")
-        assert tag in [cls.get_land_tag(), cls.get_lor_tag()]
 
         def binop_batch_rec(tag: str, expr_li: list, begin: int, end: int) -> AbsExpr:
             assert begin < end
@@ -137,7 +146,11 @@ def binop_batch_rec(tag: str, expr_li: list, begin: int, end: int) -> AbsExpr:
             right = binop_batch_rec(tag, expr_li, mid, end)
             return type(left).binop(tag, left, right)
 
-        return binop_batch_rec(tag, expr_li, 0, len(expr_li))
+        if cls.partitioning_order:
+            res = binop_batch_rec(tag, expr_li, 0, len(expr_li))
+        else:
+            res = functools.reduce(lambda x,y: cls.binop(tag, x,y), expr_li)
+        return res
 
     @classmethod
     def bitwise_binop(cls, tag: str, left_li: list, right_li: list) -> AbsExpr:
@@ -263,7 +276,7 @@ def compute_cnf_step(self, igen: IndexGen, \
         ), "compute_cnf_step() assumes reduced formulas"
         super().compute_cnf_step(igen, assoc, cnf)
 
-    def reduce_step(self, assoc: dict, st: BaseRelSt) -> None:
+    def reduce_formula_step(self, assoc: dict, st: BaseRelSt) -> None:
         """Performs reduce computation for this object."""
         if self.is_land_term():
             left = assoc[id(self.get_operand(1))]
@@ -319,7 +332,7 @@ def reduce_step(self, assoc: dict, st: BaseRelSt) -> None:
             assoc[id(self)] = type(self).lor(left, right)
             return
 
-        super().reduce_step(assoc, st)
+        super().reduce_formula_step(assoc, st)
 
     def make_str_pre_step(self) -> str:
         """Makes string in prefix order for this object."""

pygplib/ecc.py

@@ -69,7 +69,7 @@ def _select_uncovered_edge(self, U: list, variant: str = "r"):
             i = random.randint(0,len(U)-1)
             return U[i][0], U[i][1]
         else:
-            raise Exception(f"variant {variant} not yet implemented")
+            raise Exception(f"NotImplementedError: variant {variant}")
 
     def _extract_node(self, P: set, Q: list, variant: str = "r")\
         -> int:
@@ -90,7 +90,7 @@ def _extract_node(self, P: set, Q: list, variant: str = "r")\
             pos = random.randint(0,len(P)-1)
             return list(P)[pos]
         else:
-            raise Exception(f"variant {variant} not yet implemented")
+            raise Exception(f"NotImplementedError: variant {variant}")
 
     def _find_clique_covering(self, u: int, v:int, U: list, \
         variant: str = "r") -> tuple:
@@ -166,7 +166,7 @@ def _select_unseparated_edge(self, U: list, variant: str = "r"):
             i = random.randint(0,len(U)-1)
             return U[i][0], U[i][1]
         else:
-            raise Exception(f"variant {variant} not yet implemented")
+            raise Exception(f"NotImplementedError: variant {variant}")
 
     def _find_clique_separating(self, u: int, v:int, U: list, \
         variant: str = "r") -> tuple:

pygplib/fog.py

@@ -1,6 +1,6 @@
 """Class of first-order logic of graphs"""
 
-import functools
+import warnings
 
 import pyparsing as pp
 # Enables "packrat" parsing, which speedup parsing.
@@ -182,7 +182,7 @@ def get_free_vars_and_consts_pre_step(
 
         super().get_free_vars_and_consts_pre_step(bound_vars, free_vars)
 
-    def reduce_step(self, assoc: dict, st: BaseRelSt) -> None:
+    def reduce_formula_step(self, assoc: dict, st: BaseRelSt) -> None:
         """Performs reduce computatoin for this object."""
 
         if self.is_edg_atom():
@@ -215,11 +215,10 @@ def reduce_step(self, assoc: dict, st: BaseRelSt) -> None:
             assoc[id(self)] = self
             return
 
-        super().reduce_step(assoc, st)
-
-    def propnize_step(self, assoc: dict, st: BaseRelSt) -> None:
-        """Performs propositionalization for this object."""
+        super().reduce_formula_step(assoc, st)
 
+    def perform_boolean_encoding_step(self, assoc: dict, st: BaseRelSt) -> None:
+        """Performs Boolean encoding for this object."""
         if self.is_edg_atom():
             atom = [self.get_atom_value(1), self.get_atom_value(2)]
             if atom[0] == atom[1]:
@@ -440,13 +439,13 @@ def action_qfop(string, location, tokens):
                     ANDOP,
                     2,
                     pp.opAssoc.LEFT,
-                    action_binop_batch if cls.bipartite_order else action_binop,
+                    action_binop_batch,
                 ),
                 (
                     OROP,
                     2,
                     pp.opAssoc.LEFT,
-                    action_binop_batch if cls.bipartite_order else action_binop,
+                    action_binop_batch,
                 ),
                 (IMPLIESOP, 2, pp.opAssoc.LEFT, action_binop),
                 (IFFOP, 2, pp.opAssoc.LEFT, action_binop),