From c084f8185a2155d3eb6757a715d1978731b92314 Mon Sep 17 00:00:00 2001
From: Tom Vidal <tomvidal421@gmail.com>
Date: Tue, 11 Jun 2024 19:57:42 +0100
Subject: [PATCH 1/7] Add py2bexp CLI tool to convert qlassf functions to
 boolean expressions

- Implemented `py2bexp.py` in the `qlasskit/tools` package.
  - Added functionality to receive a Python script (file or stdin) as input and output boolean expressions.
  - Default input is stdin if not specified with `--input-file/-i`.
  - Default entrypoint function is the last qlassf defined if not specified with `--entrypoint/-e`.
  - Default output is stdout if not specified with `--output/-o`.
  - Added parameter `-f/--form` for specifying the expression form (anf, cnf, dnf, nnf).
  - Added parameter `-t/--format` for specifying the output format (sympy string or dimacs format for cnf).
  - Added `-h/--help` for usage and `-v/--version` for qlasskit version.

- Added unit tests in `test_tools.py` to verify functionality:
  - Tested help and version output.
  - Tested default behavior and specific entrypoint function handling.
  - Tested different expression forms (anf, cnf, dnf, nnf).
  - Verified DIMACS format output for CNF.
---
 qlasskit/tools/py2bexp.py | 133 ++++++++++++++++++++++++++++++++++++++
 setup.py                  |   5 ++
 test/test_tools.py        | 123 ++++++++++++++++++++++++++++++++---
 3 files changed, 253 insertions(+), 8 deletions(-)
 create mode 100644 qlasskit/tools/py2bexp.py

diff --git a/qlasskit/tools/py2bexp.py b/qlasskit/tools/py2bexp.py
new file mode 100644
index 00000000..c5e99c78
--- /dev/null
+++ b/qlasskit/tools/py2bexp.py
@@ -0,0 +1,133 @@
+#!/usr/bin/env python3
+
+# Copyright 2023-2024 Davide Gessa
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+import argparse
+import sys
+import sympy
+import qlasskit
+from qlasskit.qlassfun import QlassF
+from qlasskit.tools.utils import parse_str
+
+
+def read_input(input_file):
+    if input_file == "-":
+        return sys.stdin.read()
+    with open(input_file, "r") as file:
+        return file.read()
+
+
+def find_last_qlassf(qlassf_list):
+    return qlassf_list[-1][1] if qlassf_list else None
+
+
+def convert_to_bool_expression(qlassf: QlassF, form: str):
+    combined_expr = sympy.And(*[expr[1] for expr in qlassf.expressions])
+
+    if form == "anf":
+        return sympy.to_anf(combined_expr)
+    elif form == "cnf":
+        return sympy.to_cnf(combined_expr, simplify=True)
+    elif form == "dnf":
+        return sympy.to_dnf(combined_expr, simplify=True)
+    elif form == "nnf":
+        return sympy.to_nnf(combined_expr, simplify=True)
+    return combined_expr  # Default case if no specific form is requested
+
+
+def convert_to_dimacs(expr):
+    clauses = sympy.to_cnf(expr, simplify=True).args
+    if len(clauses) == 1 and isinstance(clauses[0], sympy.Symbol):
+        clauses = [clauses]
+
+    var_dict = {symbol: i + 1 for i, symbol in enumerate(expr.free_symbols)}
+    dimacs_clauses = []
+
+    for clause in clauses:
+        if isinstance(clause, sympy.Or):
+            clause_literals = clause.args
+        else:
+            clause_literals = [clause]
+
+        dimacs_clause = []
+        for lit in clause_literals:
+            if isinstance(lit, sympy.Not):
+                dimacs_clause.append(-var_dict[lit.args[0]])
+            else:
+                dimacs_clause.append(var_dict[lit])
+        dimacs_clauses.append(dimacs_clause)
+
+    num_vars = len(var_dict)
+    num_clauses = len(dimacs_clauses)
+    dimacs_str = f"p cnf {num_vars} {num_clauses}\n"
+    for clause in dimacs_clauses:
+        dimacs_str += " ".join(map(str, clause)) + " 0\n"
+    return dimacs_str
+
+
+def output_result(result, output_file, output_format):
+    if output_format == "dimacs":
+        result = convert_to_dimacs(result)
+    if output_file == "-":
+        print(result)
+    else:
+        with open(output_file, "w") as file:
+            file.write(str(result))
+
+
+def main():
+    parser = argparse.ArgumentParser(
+        description="Convert qlassf functions in a Python script to boolean expressions."
+    )
+    parser.add_argument(
+        "-i", "--input-file", default="-", help="Input file (default: stdin)"
+    )
+    parser.add_argument("-e", "--entrypoint", help="Entrypoint function name")
+    parser.add_argument(
+        "-o", "--output", default="-", help="Output file (default: stdout)"
+    )
+    parser.add_argument(
+        "-f",
+        "--form",
+        choices=["anf", "cnf", "dnf", "nnf"],
+        default="sympy",
+        help="Expression form (default: sympy)",
+    )
+    parser.add_argument(
+        "-t",
+        "--format",
+        choices=["sympy", "dimacs"],
+        default="sympy",
+        help="Output format (default: sympy)",
+    )
+    parser.add_argument(
+        "-v", "--version", action="version", version=f"qlasskit {qlasskit.__version__}"
+    )
+
+    args = parser.parse_args()
+
+    script = read_input(args.input_file)
+    qlassf_list = parse_str(script)
+
+    if args.entrypoint:
+        qlassf = next((f[1] for f in qlassf_list if f[0] == args.entrypoint), None)
+    else:
+        qlassf = find_last_qlassf(qlassf_list)
+
+    if qlassf:
+        bool_expr = convert_to_bool_expression(qlassf, args.form)
+        output_result(bool_expr, args.output, args.format)
+    else:
+        print("No qlassf function found", file=sys.stderr)
diff --git a/setup.py b/setup.py
index 46248e68..ab5712ec 100644
--- a/setup.py
+++ b/setup.py
@@ -61,4 +61,9 @@
         "Documentation": "https://dakk.github.io/qlasskit",
         "Source": "https://github.com/dakk/qlasskit",
     },
+    entry_points={
+        "console_scripts": [
+            "py2bexp=qlasskit.tools.py2bexp:main",
+        ]
+    },
 )
diff --git a/test/test_tools.py b/test/test_tools.py
index 0e969ea7..25c0eed2 100644
--- a/test/test_tools.py
+++ b/test/test_tools.py
@@ -1,22 +1,25 @@
-# Copyright 2023-204 Davide Gessa
-
+# Copyright 2023-2024 Davide Gessa
+#
 # Licensed under the Apache License, Version 2.0 (the "License");
 # you may not use this file except in compliance with the License.
 # You may obtain a copy of the License at
-
+#
 # http://www.apache.org/licenses/LICENSE-2.0
-
+#
 # Unless required by applicable law or agreed to in writing, software
 # distributed under the License is distributed on an "AS IS" BASIS,
 # WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 # See the License for the specific language governing permissions and
 # limitations under the License.
 
+import os
+import subprocess
+import tempfile
 import unittest
 
 from qlasskit.tools import utils
 
-dummy = """
+dummy_script = """
 from qlasskit import qlassf
 
 @qlassf
@@ -24,11 +27,115 @@ def a(b: bool) -> bool:
     return not b
 
 @qlassf
-def c(b: bool) -> bool:
-    return b
+def c(x: bool, y: bool, z: bool) -> bool:
+    return (x or y or not z) and (not y or z)
 """
 
 
 class TestTools_utils(unittest.TestCase):
     def test_parse_str(self):
-        print(utils.parse_str(dummy))
+        print(utils.parse_str(dummy_script))
+
+
+class TestPy2Bexp(unittest.TestCase):
+    def setUp(self):
+        # Create a temporary file to hold the dummy script
+        self.temp_file = tempfile.NamedTemporaryFile(delete=False, suffix=".py")
+        self.temp_file.write(dummy_script.encode())
+        self.temp_file.close()
+
+    def tearDown(self):
+        # Remove the temporary file
+        os.unlink(self.temp_file.name)
+
+    def run_command(self, args, input=None):
+        result = subprocess.run(args, input=input, capture_output=True, text=True)
+        if result.stderr:
+            print(f"Error: {result.stderr}")
+        return result
+
+    def test_help(self):
+        result = self.run_command(["py2bexp", "--help"])
+        print(result.stdout)
+
+    def test_version(self):
+        result = self.run_command(["py2bexp", "--version"])
+        print(result.stdout)
+
+    def test_output_to_stdout(self):
+        result = self.run_command(["py2bexp", "-i", self.temp_file.name])
+        print(result.stdout)
+
+    def test_specific_entrypoint(self):
+        result = self.run_command(
+            [
+                "py2bexp",
+                "-i",
+                self.temp_file.name,
+                "-e",
+                "a",
+            ]
+        )
+        print(result.stdout)
+        self.assertIn("~b", result.stdout)  # For function a(b)
+
+    def test_output_to_file(self):
+        with tempfile.NamedTemporaryFile(delete=False) as temp_output:
+            output_file = temp_output.name
+        try:
+            self.run_command(
+                [
+                    "py2bexp",
+                    "-i",
+                    self.temp_file.name,
+                    "-o",
+                    output_file,
+                ]
+            )
+            with open(output_file, "r") as f:
+                content = f.read()
+                print(content)
+        finally:
+            os.unlink(output_file)
+
+    def test_dnf_form(self):
+        result = self.run_command(
+            [
+                "py2bexp",
+                "-i",
+                self.temp_file.name,
+                "-f",
+                "dnf",
+            ]
+        )
+        print(result.stdout)
+
+    def test_cnf_form(self):
+        result = self.run_command(
+            [
+                "py2bexp",
+                "-i",
+                self.temp_file.name,
+                "-f",
+                "cnf",
+            ]
+        )
+        print(result.stdout)
+
+    def test_dimacs_format(self):
+        result = self.run_command(
+            [
+                "py2bexp",
+                "-i",
+                self.temp_file.name,
+                "-f",
+                "cnf",
+                "-t",
+                "dimacs",
+            ]
+        )
+        print(result.stdout)
+
+    def test_stdin_input(self):
+        result = self.run_command(["py2bexp"], input=dummy_script)
+        print(result.stdout)

From ac43b5112771657cc07e982d06cfa29878a1e01b Mon Sep 17 00:00:00 2001
From: Tom Vidal <tomvidal421@gmail.com>
Date: Tue, 11 Jun 2024 20:32:47 +0100
Subject: [PATCH 2/7] Fix unit tests

---
 qlasskit/tools/py2bexp.py |  6 ++++++
 test/test_tools.py        | 34 +++++++++++++++++++++++++---------
 2 files changed, 31 insertions(+), 9 deletions(-)

diff --git a/qlasskit/tools/py2bexp.py b/qlasskit/tools/py2bexp.py
index c5e99c78..45337a92 100644
--- a/qlasskit/tools/py2bexp.py
+++ b/qlasskit/tools/py2bexp.py
@@ -16,7 +16,9 @@
 
 import argparse
 import sys
+
 import sympy
+
 import qlasskit
 from qlasskit.qlassfun import QlassF
 from qlasskit.tools.utils import parse_str
@@ -131,3 +133,7 @@ def main():
         output_result(bool_expr, args.output, args.format)
     else:
         print("No qlassf function found", file=sys.stderr)
+
+
+if __name__ == "__main__":
+    main()
diff --git a/test/test_tools.py b/test/test_tools.py
index 25c0eed2..ecfdcfbc 100644
--- a/test/test_tools.py
+++ b/test/test_tools.py
@@ -55,21 +55,27 @@ def run_command(self, args, input=None):
         return result
 
     def test_help(self):
-        result = self.run_command(["py2bexp", "--help"])
+        result = self.run_command(["python", "-m", "qlasskit.tools.py2bexp", "--help"])
         print(result.stdout)
 
     def test_version(self):
-        result = self.run_command(["py2bexp", "--version"])
+        result = self.run_command(
+            ["python", "-m", "qlasskit.tools.py2bexp", "--version"]
+        )
         print(result.stdout)
 
     def test_output_to_stdout(self):
-        result = self.run_command(["py2bexp", "-i", self.temp_file.name])
+        result = self.run_command(
+            ["python", "-m", "qlasskit.tools.py2bexp", "-i", self.temp_file.name]
+        )
         print(result.stdout)
 
     def test_specific_entrypoint(self):
         result = self.run_command(
             [
-                "py2bexp",
+                "python",
+                "-m",
+                "qlasskit.tools.py2bexp",
                 "-i",
                 self.temp_file.name,
                 "-e",
@@ -85,7 +91,9 @@ def test_output_to_file(self):
         try:
             self.run_command(
                 [
-                    "py2bexp",
+                    "python",
+                    "-m",
+                    "qlasskit.tools.py2bexp",
                     "-i",
                     self.temp_file.name,
                     "-o",
@@ -101,7 +109,9 @@ def test_output_to_file(self):
     def test_dnf_form(self):
         result = self.run_command(
             [
-                "py2bexp",
+                "python",
+                "-m",
+                "qlasskit.tools.py2bexp",
                 "-i",
                 self.temp_file.name,
                 "-f",
@@ -113,7 +123,9 @@ def test_dnf_form(self):
     def test_cnf_form(self):
         result = self.run_command(
             [
-                "py2bexp",
+                "python",
+                "-m",
+                "qlasskit.tools.py2bexp",
                 "-i",
                 self.temp_file.name,
                 "-f",
@@ -125,7 +137,9 @@ def test_cnf_form(self):
     def test_dimacs_format(self):
         result = self.run_command(
             [
-                "py2bexp",
+                "python",
+                "-m",
+                "qlasskit.tools.py2bexp",
                 "-i",
                 self.temp_file.name,
                 "-f",
@@ -137,5 +151,7 @@ def test_dimacs_format(self):
         print(result.stdout)
 
     def test_stdin_input(self):
-        result = self.run_command(["py2bexp"], input=dummy_script)
+        result = self.run_command(
+            ["python", "-m", "qlasskit.tools.py2bexp"], input=dummy_script
+        )
         print(result.stdout)

From 6c9c7f9dd4744d02c3c2072f7f341e5239be0a6d Mon Sep 17 00:00:00 2001
From: Tom Vidal <tomvidal421@gmail.com>
Date: Tue, 11 Jun 2024 23:15:07 +0100
Subject: [PATCH 3/7] Add assertions in unit tests

- Added satisfactory assertions for all the unit tests except two (in test_anf_form, is_anf returns an error... ; Haven't found a satisfactory way to test the dimacs format)
- Modify py2bexp.py to use sympy logic functions directly instead of sympy.to_anf, sympy.to_cnf, sympy.to_dnf, sympy.to_nnf functions
- Refactor output_result function in py2bexp.py to handle DIMACS format only for CNF expressions
---
 qlasskit/tools/py2bexp.py | 20 ++++++---
 test/test_tools.py        | 89 ++++++++++++++++++++++++++++++++++++---
 2 files changed, 95 insertions(+), 14 deletions(-)

diff --git a/qlasskit/tools/py2bexp.py b/qlasskit/tools/py2bexp.py
index 45337a92..68101136 100644
--- a/qlasskit/tools/py2bexp.py
+++ b/qlasskit/tools/py2bexp.py
@@ -18,6 +18,7 @@
 import sys
 
 import sympy
+from sympy.logic.boolalg import to_anf, to_cnf, to_dnf, to_nnf
 
 import qlasskit
 from qlasskit.qlassfun import QlassF
@@ -39,18 +40,18 @@ def convert_to_bool_expression(qlassf: QlassF, form: str):
     combined_expr = sympy.And(*[expr[1] for expr in qlassf.expressions])
 
     if form == "anf":
-        return sympy.to_anf(combined_expr)
+        return to_anf(combined_expr)
     elif form == "cnf":
-        return sympy.to_cnf(combined_expr, simplify=True)
+        return to_cnf(combined_expr, simplify=True)
     elif form == "dnf":
-        return sympy.to_dnf(combined_expr, simplify=True)
+        return to_dnf(combined_expr, simplify=True)
     elif form == "nnf":
-        return sympy.to_nnf(combined_expr, simplify=True)
+        return to_nnf(combined_expr, simplify=True)
     return combined_expr  # Default case if no specific form is requested
 
 
 def convert_to_dimacs(expr):
-    clauses = sympy.to_cnf(expr, simplify=True).args
+    clauses = to_cnf(expr, simplify=True).args
     if len(clauses) == 1 and isinstance(clauses[0], sympy.Symbol):
         clauses = [clauses]
 
@@ -79,8 +80,13 @@ def convert_to_dimacs(expr):
     return dimacs_str
 
 
-def output_result(result, output_file, output_format):
+def output_result(result, output_file, output_format, form):
     if output_format == "dimacs":
+        if form != "cnf":
+            print(
+                "Warning: DIMACS format is only supported for CNF form. Converting to CNF."
+            )
+            result = to_cnf(result, simplify=True)
         result = convert_to_dimacs(result)
     if output_file == "-":
         print(result)
@@ -130,7 +136,7 @@ def main():
 
     if qlassf:
         bool_expr = convert_to_bool_expression(qlassf, args.form)
-        output_result(bool_expr, args.output, args.format)
+        output_result(bool_expr, args.output, args.format, args.form)
     else:
         print("No qlassf function found", file=sys.stderr)
 
diff --git a/test/test_tools.py b/test/test_tools.py
index ecfdcfbc..5b74a7c9 100644
--- a/test/test_tools.py
+++ b/test/test_tools.py
@@ -17,6 +17,11 @@
 import tempfile
 import unittest
 
+import sympy
+from sympy.logic.boolalg import is_anf, is_cnf, is_dnf, is_nnf
+from sympy.logic.utilities.dimacs import load
+
+import qlasskit
 from qlasskit.tools import utils
 
 dummy_script = """
@@ -48,11 +53,19 @@ def tearDown(self):
         # Remove the temporary file
         os.unlink(self.temp_file.name)
 
-    def run_command(self, args, input=None):
-        result = subprocess.run(args, input=input, capture_output=True, text=True)
-        if result.stderr:
-            print(f"Error: {result.stderr}")
-        return result
+    def run_command(self, args, stdin_input=None):
+        try:
+            result = subprocess.run(
+                args, input=stdin_input, capture_output=True, text=True, check=True
+            )
+            return result
+        except subprocess.CalledProcessError as e:
+            print(
+                f"Command '{' '.join(e.cmd)}' returned non-zero exit status {e.returncode}"
+            )
+            print(f"Standard output:\n{e.stdout}")
+            print(f"Standard error:\n{e.stderr}")
+            raise
 
     def test_help(self):
         result = self.run_command(["python", "-m", "qlasskit.tools.py2bexp", "--help"])
@@ -63,12 +76,16 @@ def test_version(self):
             ["python", "-m", "qlasskit.tools.py2bexp", "--version"]
         )
         print(result.stdout)
+        assert result.stdout == f"qlasskit {qlasskit.__version__}\n"
 
     def test_output_to_stdout(self):
         result = self.run_command(
             ["python", "-m", "qlasskit.tools.py2bexp", "-i", self.temp_file.name]
         )
         print(result.stdout)
+        expr = sympy.parse_expr(result.stdout)
+        expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
+        assert expr.equals(expected)
 
     def test_specific_entrypoint(self):
         result = self.run_command(
@@ -83,7 +100,9 @@ def test_specific_entrypoint(self):
             ]
         )
         print(result.stdout)
-        self.assertIn("~b", result.stdout)  # For function a(b)
+        expr = sympy.parse_expr(result.stdout)
+        expected = sympy.parse_expr("~b")
+        assert expr.equals(expected)
 
     def test_output_to_file(self):
         with tempfile.NamedTemporaryFile(delete=False) as temp_output:
@@ -103,6 +122,9 @@ def test_output_to_file(self):
             with open(output_file, "r") as f:
                 content = f.read()
                 print(content)
+                expr = sympy.parse_expr(content)
+                expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
+                assert expr.equals(expected)
         finally:
             os.unlink(output_file)
 
@@ -119,6 +141,10 @@ def test_dnf_form(self):
             ]
         )
         print(result.stdout)
+        expr = sympy.parse_expr(result.stdout)
+        expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
+        assert expr.equals(expected)
+        assert is_dnf(result.stdout)
 
     def test_cnf_form(self):
         result = self.run_command(
@@ -133,6 +159,47 @@ def test_cnf_form(self):
             ]
         )
         print(result.stdout)
+        expr = sympy.parse_expr(result.stdout)
+        expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
+        assert expr.equals(expected)
+        assert is_cnf(result.stdout)
+
+    def test_nnf_form(self):
+        result = self.run_command(
+            [
+                "python",
+                "-m",
+                "qlasskit.tools.py2bexp",
+                "-i",
+                self.temp_file.name,
+                "-f",
+                "nnf",
+            ]
+        )
+        print(result.stdout)
+        expr = sympy.parse_expr(result.stdout)
+        expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
+        assert expr.equals(expected)
+        assert is_nnf(result.stdout)
+
+    def test_anf_form(self):
+        result = self.run_command(
+            [
+                "python",
+                "-m",
+                "qlasskit.tools.py2bexp",
+                "-i",
+                self.temp_file.name,
+                "-f",
+                "anf",
+            ]
+        )
+        print(result.stdout)
+        expr = sympy.parse_expr(result.stdout)
+        print(expr)
+        expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
+        assert expr.equals(expected)
+        # assert is_anf(result.stdout) # This is not working
 
     def test_dimacs_format(self):
         result = self.run_command(
@@ -149,9 +216,17 @@ def test_dimacs_format(self):
             ]
         )
         print(result.stdout)
+        expr = load(result.stdout)
+        print(expr)
+        # expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
+        # assert expr.equals(expected)
+        self.assertIn("p cnf 3 2", result.stdout)
 
     def test_stdin_input(self):
         result = self.run_command(
-            ["python", "-m", "qlasskit.tools.py2bexp"], input=dummy_script
+            ["python", "-m", "qlasskit.tools.py2bexp"], stdin_input=dummy_script
         )
         print(result.stdout)
+        expr = sympy.parse_expr(result.stdout)
+        expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
+        assert expr.equals(expected)

From 922c06d9a30caece0e6135c3af17816270e766f7 Mon Sep 17 00:00:00 2001
From: Tom Vidal <tomvidal421@gmail.com>
Date: Tue, 11 Jun 2024 23:15:50 +0100
Subject: [PATCH 4/7] Comment unused import

---
 test/test_tools.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/test/test_tools.py b/test/test_tools.py
index 5b74a7c9..80520237 100644
--- a/test/test_tools.py
+++ b/test/test_tools.py
@@ -18,7 +18,9 @@
 import unittest
 
 import sympy
-from sympy.logic.boolalg import is_anf, is_cnf, is_dnf, is_nnf
+from sympy.logic.boolalg import is_cnf, is_dnf, is_nnf
+
+# from sympy.logic.boolalg import to_anf
 from sympy.logic.utilities.dimacs import load
 
 import qlasskit

From 7544f82c6a3f3cb3bf35930bdb663f573cbde896 Mon Sep 17 00:00:00 2001
From: Tom Vidal <tomvidal421@gmail.com>
Date: Tue, 11 Jun 2024 23:47:33 +0100
Subject: [PATCH 5/7] Correct dimacs unit test

As the order of the symbols when converting to DIMACS is not guaranteed, and all the permutations of the names of the symbols give equivalent expressions, the test compares to all the possible permutations of the 3 symbols.
---
 test/test_tools.py | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/test/test_tools.py b/test/test_tools.py
index 80520237..b2fe750c 100644
--- a/test/test_tools.py
+++ b/test/test_tools.py
@@ -18,7 +18,7 @@
 import unittest
 
 import sympy
-from sympy.logic.boolalg import is_cnf, is_dnf, is_nnf
+from sympy.logic.boolalg import And, Not, Or, is_cnf, is_dnf, is_nnf
 
 # from sympy.logic.boolalg import to_anf
 from sympy.logic.utilities.dimacs import load
@@ -219,9 +219,24 @@ def test_dimacs_format(self):
         )
         print(result.stdout)
         expr = load(result.stdout)
-        print(expr)
-        # expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
-        # assert expr.equals(expected)
+        symbols = expr.free_symbols
+        x, y, z = symbols
+        expected1 = And(Or(x, y, Not(z)), Or(z, Not(y)))
+        expected2 = And(Or(y, z, Not(x)), Or(x, Not(z)))
+        expected3 = And(Or(z, x, Not(y)), Or(y, Not(x)))
+        expected4 = And(Or(x, z, Not(y)), Or(y, Not(z)))
+        expected5 = And(Or(y, x, Not(z)), Or(z, Not(x)))
+        expected6 = And(Or(z, y, Not(x)), Or(x, Not(y)))
+        # The result should be one of the 6 permutations of the expected expressions
+        # because the order of the symbols in the DIMACS format is not guaranteed
+        assert (
+            expr.equals(expected1)
+            or expr.equals(expected2)
+            or expr.equals(expected3)
+            or expr.equals(expected4)
+            or expr.equals(expected5)
+            or expr.equals(expected6)
+        )
         self.assertIn("p cnf 3 2", result.stdout)
 
     def test_stdin_input(self):

From 6805980d419dcbcd5a51dbc4176af838faececa9 Mon Sep 17 00:00:00 2001
From: Tom Vidal <tomvidal421@gmail.com>
Date: Wed, 12 Jun 2024 10:28:24 +0100
Subject: [PATCH 6/7] Clean test_tools.py

Removed prints from unit test.
Used itertools to handle permutations for the DIMACS test.
---
 test/test_tools.py | 67 +++++++++++++++++-----------------------------
 1 file changed, 25 insertions(+), 42 deletions(-)

diff --git a/test/test_tools.py b/test/test_tools.py
index b2fe750c..d3e7e1c0 100644
--- a/test/test_tools.py
+++ b/test/test_tools.py
@@ -16,6 +16,7 @@
 import subprocess
 import tempfile
 import unittest
+from itertools import permutations
 
 import sympy
 from sympy.logic.boolalg import And, Not, Or, is_cnf, is_dnf, is_nnf
@@ -69,25 +70,22 @@ def run_command(self, args, stdin_input=None):
             print(f"Standard error:\n{e.stderr}")
             raise
 
-    def test_help(self):
-        result = self.run_command(["python", "-m", "qlasskit.tools.py2bexp", "--help"])
-        print(result.stdout)
+    # def test_help(self):
+    #     result = self.run_command(["python", "-m", "qlasskit.tools.py2bexp", "--help"])
 
     def test_version(self):
         result = self.run_command(
             ["python", "-m", "qlasskit.tools.py2bexp", "--version"]
         )
-        print(result.stdout)
-        assert result.stdout == f"qlasskit {qlasskit.__version__}\n"
+        self.assertTrue(result.stdout == f"qlasskit {qlasskit.__version__}\n")
 
     def test_output_to_stdout(self):
         result = self.run_command(
             ["python", "-m", "qlasskit.tools.py2bexp", "-i", self.temp_file.name]
         )
-        print(result.stdout)
         expr = sympy.parse_expr(result.stdout)
         expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
-        assert expr.equals(expected)
+        self.assertTrue(expr.equals(expected))
 
     def test_specific_entrypoint(self):
         result = self.run_command(
@@ -101,10 +99,9 @@ def test_specific_entrypoint(self):
                 "a",
             ]
         )
-        print(result.stdout)
         expr = sympy.parse_expr(result.stdout)
         expected = sympy.parse_expr("~b")
-        assert expr.equals(expected)
+        self.assertTrue(expr.equals(expected))
 
     def test_output_to_file(self):
         with tempfile.NamedTemporaryFile(delete=False) as temp_output:
@@ -123,10 +120,9 @@ def test_output_to_file(self):
             )
             with open(output_file, "r") as f:
                 content = f.read()
-                print(content)
                 expr = sympy.parse_expr(content)
                 expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
-                assert expr.equals(expected)
+                self.assertTrue(expr.equals(expected))
         finally:
             os.unlink(output_file)
 
@@ -142,11 +138,10 @@ def test_dnf_form(self):
                 "dnf",
             ]
         )
-        print(result.stdout)
         expr = sympy.parse_expr(result.stdout)
         expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
-        assert expr.equals(expected)
-        assert is_dnf(result.stdout)
+        self.assertTrue(is_dnf(result.stdout))
+        self.assertTrue(expr.equals(expected))
 
     def test_cnf_form(self):
         result = self.run_command(
@@ -160,11 +155,10 @@ def test_cnf_form(self):
                 "cnf",
             ]
         )
-        print(result.stdout)
         expr = sympy.parse_expr(result.stdout)
         expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
-        assert expr.equals(expected)
-        assert is_cnf(result.stdout)
+        self.assertTrue(is_cnf(result.stdout))
+        self.assertTrue(expr.equals(expected))
 
     def test_nnf_form(self):
         result = self.run_command(
@@ -178,11 +172,10 @@ def test_nnf_form(self):
                 "nnf",
             ]
         )
-        print(result.stdout)
         expr = sympy.parse_expr(result.stdout)
         expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
-        assert expr.equals(expected)
-        assert is_nnf(result.stdout)
+        self.assertTrue(is_nnf(result.stdout))
+        self.assertTrue(expr.equals(expected))
 
     def test_anf_form(self):
         result = self.run_command(
@@ -196,12 +189,10 @@ def test_anf_form(self):
                 "anf",
             ]
         )
-        print(result.stdout)
         expr = sympy.parse_expr(result.stdout)
-        print(expr)
         expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
-        assert expr.equals(expected)
-        # assert is_anf(result.stdout) # This is not working
+        self.assertTrue(expr.equals(expected))
+        # self.assertTrue(is_anf(result.stdout)) # This is not working
 
     def test_dimacs_format(self):
         result = self.run_command(
@@ -217,33 +208,25 @@ def test_dimacs_format(self):
                 "dimacs",
             ]
         )
-        print(result.stdout)
         expr = load(result.stdout)
         symbols = expr.free_symbols
-        x, y, z = symbols
-        expected1 = And(Or(x, y, Not(z)), Or(z, Not(y)))
-        expected2 = And(Or(y, z, Not(x)), Or(x, Not(z)))
-        expected3 = And(Or(z, x, Not(y)), Or(y, Not(x)))
-        expected4 = And(Or(x, z, Not(y)), Or(y, Not(z)))
-        expected5 = And(Or(y, x, Not(z)), Or(z, Not(x)))
-        expected6 = And(Or(z, y, Not(x)), Or(x, Not(y)))
+
         # The result should be one of the 6 permutations of the expected expressions
         # because the order of the symbols in the DIMACS format is not guaranteed
-        assert (
-            expr.equals(expected1)
-            or expr.equals(expected2)
-            or expr.equals(expected3)
-            or expr.equals(expected4)
-            or expr.equals(expected5)
-            or expr.equals(expected6)
-        )
+        assert_val = False
+        for sl in permutations(symbols):
+            exp = And(Or(sl[0], sl[1], Not(sl[2])), Or(sl[2], Not(sl[1])))
+            if expr.equals(exp):
+                assert_val = True
+                break
+
+        self.assertTrue(assert_val)
         self.assertIn("p cnf 3 2", result.stdout)
 
     def test_stdin_input(self):
         result = self.run_command(
             ["python", "-m", "qlasskit.tools.py2bexp"], stdin_input=dummy_script
         )
-        print(result.stdout)
         expr = sympy.parse_expr(result.stdout)
         expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)")
-        assert expr.equals(expected)
+        self.assertTrue(expr.equals(expected))

From 40ab93c36487f4f26af2117048b6893c2b10d685 Mon Sep 17 00:00:00 2001
From: Tom Vidal <tomvidal421@gmail.com>
Date: Wed, 12 Jun 2024 10:39:15 +0100
Subject: [PATCH 7/7] Moved `find_last_qlassf` function to `tools.py`

---
 qlasskit/tools/py2bexp.py |  6 ++----
 qlasskit/tools/tools.py   | 17 +++++++++++++++++
 2 files changed, 19 insertions(+), 4 deletions(-)
 create mode 100644 qlasskit/tools/tools.py

diff --git a/qlasskit/tools/py2bexp.py b/qlasskit/tools/py2bexp.py
index 68101136..5e265788 100644
--- a/qlasskit/tools/py2bexp.py
+++ b/qlasskit/tools/py2bexp.py
@@ -24,6 +24,8 @@
 from qlasskit.qlassfun import QlassF
 from qlasskit.tools.utils import parse_str
 
+from .tools import find_last_qlassf
+
 
 def read_input(input_file):
     if input_file == "-":
@@ -32,10 +34,6 @@ def read_input(input_file):
         return file.read()
 
 
-def find_last_qlassf(qlassf_list):
-    return qlassf_list[-1][1] if qlassf_list else None
-
-
 def convert_to_bool_expression(qlassf: QlassF, form: str):
     combined_expr = sympy.And(*[expr[1] for expr in qlassf.expressions])
 
diff --git a/qlasskit/tools/tools.py b/qlasskit/tools/tools.py
new file mode 100644
index 00000000..3d9f7916
--- /dev/null
+++ b/qlasskit/tools/tools.py
@@ -0,0 +1,17 @@
+# Copyright 2023-2024 Davide Gessa
+#
+# Licensed under the Apache License, Version 2.0 (the "License");
+# you may not use this file except in compliance with the License.
+# You may obtain a copy of the License at
+#
+#     http://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS,
+# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+# See the License for the specific language governing permissions and
+# limitations under the License.
+
+
+def find_last_qlassf(qlassf_list):
+    return qlassf_list[-1][1] if qlassf_list else None