diff --git a/qlasskit/tools/py2bexp.py b/qlasskit/tools/py2bexp.py new file mode 100644 index 00000000..5e265788 --- /dev/null +++ b/qlasskit/tools/py2bexp.py @@ -0,0 +1,143 @@ +#!/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 +from sympy.logic.boolalg import to_anf, to_cnf, to_dnf, to_nnf + +import qlasskit +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 == "-": + return sys.stdin.read() + with open(input_file, "r") as file: + return file.read() + + +def convert_to_bool_expression(qlassf: QlassF, form: str): + combined_expr = sympy.And(*[expr[1] for expr in qlassf.expressions]) + + if form == "anf": + return to_anf(combined_expr) + elif form == "cnf": + return to_cnf(combined_expr, simplify=True) + elif form == "dnf": + return to_dnf(combined_expr, simplify=True) + elif form == "nnf": + return to_nnf(combined_expr, simplify=True) + return combined_expr # Default case if no specific form is requested + + +def convert_to_dimacs(expr): + clauses = 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, 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) + 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, args.form) + else: + print("No qlassf function found", file=sys.stderr) + + +if __name__ == "__main__": + main() 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 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..d3e7e1c0 100644 --- a/test/test_tools.py +++ b/test/test_tools.py @@ -1,22 +1,33 @@ -# 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 itertools import permutations +import sympy +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 + +import qlasskit from qlasskit.tools import utils -dummy = """ +dummy_script = """ from qlasskit import qlassf @qlassf @@ -24,11 +35,198 @@ 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, 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"]) + + def test_version(self): + result = self.run_command( + ["python", "-m", "qlasskit.tools.py2bexp", "--version"] + ) + 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] + ) + expr = sympy.parse_expr(result.stdout) + expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)") + self.assertTrue(expr.equals(expected)) + + def test_specific_entrypoint(self): + result = self.run_command( + [ + "python", + "-m", + "qlasskit.tools.py2bexp", + "-i", + self.temp_file.name, + "-e", + "a", + ] + ) + expr = sympy.parse_expr(result.stdout) + expected = sympy.parse_expr("~b") + self.assertTrue(expr.equals(expected)) + + def test_output_to_file(self): + with tempfile.NamedTemporaryFile(delete=False) as temp_output: + output_file = temp_output.name + try: + self.run_command( + [ + "python", + "-m", + "qlasskit.tools.py2bexp", + "-i", + self.temp_file.name, + "-o", + output_file, + ] + ) + with open(output_file, "r") as f: + content = f.read() + expr = sympy.parse_expr(content) + expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)") + self.assertTrue(expr.equals(expected)) + finally: + os.unlink(output_file) + + def test_dnf_form(self): + result = self.run_command( + [ + "python", + "-m", + "qlasskit.tools.py2bexp", + "-i", + self.temp_file.name, + "-f", + "dnf", + ] + ) + expr = sympy.parse_expr(result.stdout) + expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)") + self.assertTrue(is_dnf(result.stdout)) + self.assertTrue(expr.equals(expected)) + + def test_cnf_form(self): + result = self.run_command( + [ + "python", + "-m", + "qlasskit.tools.py2bexp", + "-i", + self.temp_file.name, + "-f", + "cnf", + ] + ) + expr = sympy.parse_expr(result.stdout) + expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)") + self.assertTrue(is_cnf(result.stdout)) + self.assertTrue(expr.equals(expected)) + + def test_nnf_form(self): + result = self.run_command( + [ + "python", + "-m", + "qlasskit.tools.py2bexp", + "-i", + self.temp_file.name, + "-f", + "nnf", + ] + ) + expr = sympy.parse_expr(result.stdout) + expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)") + self.assertTrue(is_nnf(result.stdout)) + self.assertTrue(expr.equals(expected)) + + def test_anf_form(self): + result = self.run_command( + [ + "python", + "-m", + "qlasskit.tools.py2bexp", + "-i", + self.temp_file.name, + "-f", + "anf", + ] + ) + expr = sympy.parse_expr(result.stdout) + expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)") + self.assertTrue(expr.equals(expected)) + # self.assertTrue(is_anf(result.stdout)) # This is not working + + def test_dimacs_format(self): + result = self.run_command( + [ + "python", + "-m", + "qlasskit.tools.py2bexp", + "-i", + self.temp_file.name, + "-f", + "cnf", + "-t", + "dimacs", + ] + ) + expr = load(result.stdout) + symbols = expr.free_symbols + + # 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_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 + ) + expr = sympy.parse_expr(result.stdout) + expected = sympy.parse_expr("(x | y | ~z) & (z | ~y)") + self.assertTrue(expr.equals(expected))