diff --git a/.github/workflows/generate.yml b/.github/workflows/generate.yml index d1e708f..a65ac35 100644 --- a/.github/workflows/generate.yml +++ b/.github/workflows/generate.yml @@ -46,7 +46,7 @@ jobs: steps: - uses: actions/checkout@v4 - name: Install iverilog - run: sudo apt install iverilog + run: sudo apt install iverilog minisat - name: Set up Python 3.x uses: actions/setup-python@v5 with: @@ -123,7 +123,7 @@ jobs: needs: build strategy: matrix: - python-version: [ '3.7', '3.8', '3.9', '3.10', '3.11' ] + python-version: [ '3.9', '3.10', '3.11', '3.12' ] name: Python ${{ matrix.python-version }} test steps: - uses: actions/checkout@v4 @@ -132,7 +132,7 @@ jobs: with: python-version: ${{ matrix.python-version }} architecture: x64 - - run: python -m pip install numpy pytest + - run: python -m pip install numpy pytest minisat - name: Run pytest run: | pytest diff --git a/ariths_gen/core/arithmetic_circuits/general_circuit.py b/ariths_gen/core/arithmetic_circuits/general_circuit.py index e09fdf5..5f0b677 100644 --- a/ariths_gen/core/arithmetic_circuits/general_circuit.py +++ b/ariths_gen/core/arithmetic_circuits/general_circuit.py @@ -7,7 +7,7 @@ from ariths_gen.wire_components import ( Wire, Bus ) -from typing import Dict +from typing import Dict, List, Tuple import inspect import copy from io import StringIO @@ -860,26 +860,15 @@ class GeneralCircuit(): file_object.write(self.get_triplets_cgp()) file_object.write(self.get_outputs_cgp()) - - # Generating flat C code representation of circuit - def get_cnf_code_flat(self, file_object): - """Generates flat C code representation of corresponding arithmetic circuit. - - Args: - file_object (TextIOWrapper): Destination file object where circuit's representation will be written to. + def get_simplified_circuits(self) -> Tuple[List[Wire], List[object]]: """ - assert self.out.N == 1, f"CNF generation only supports single output, not {self.out.N}" + Generates simplified circuit representation with only active outputs and their corresponding input wires and logic gates. + + Returns: + Tuple[List[Wire], List[object]]: List of input wires and list of logic gates. + """ - self.cnf_vars = {} - self.cnf_varid = 1 - self.cnf_has_const = False - self.cnf_var_comments = {} - - for i in self.inputs: - for j in range(i.N): - self.get_cnfvar(i[j], create=True) - - # hash array for gate outputs + # hash array for gate outputs hash_outputs = {} for i, g in enumerate(self.circuit_gates): assert g.out not in hash_outputs, f"Gate {g} has multiple outputs" @@ -910,12 +899,46 @@ class GeneralCircuit(): print(hash_outputs) + + inputs = [] + for i in self.inputs: + for j in range(i.N): + if i[j].name in active_outputs: + inputs.append(i[j]) + + gates = [] + for g in self.circuit_gates: + if g.out.name in active_outputs: + gates.append(g) + + return inputs, gates + + # Generating flat C code representation of circuit + def get_cnf_code_flat(self, file_object): + """Generates flat C code representation of corresponding arithmetic circuit. + + Args: + file_object (TextIOWrapper): Destination file object where circuit's representation will be written to. + """ + assert self.out.N == 1, f"CNF generation only supports single output, not {self.out.N}" + + self.cnf_vars = {} + self.cnf_varid = 1 + self.cnf_has_const = False + self.cnf_var_comments = {} + + + active_inputs, active_gates = self.get_simplified_circuits() + + for i in self.inputs: + for j in range(i.N): + self.get_cnfvar(i[j], create=True) + + #file_object.write(self.get_includes_c()) #file_object.write(self.get_prototype_c()) allcnfs = [] - for g in self.circuit_gates: - if g.out.name not in active_outputs: - continue + for g in active_gates: allcnfs += g.get_cnf_clause(self) allcnfs.append([self.get_cnfvar(self.out[0])]) @@ -929,7 +952,7 @@ class GeneralCircuit(): file_object.write("c varmap={}\n".format(json.dumps(self.cnf_var_comments))) for c in allcnfs: - file_object.write(" ".join(map(str, c)) + "\n") + file_object.write(" ".join(map(str, c + [0])) + "\n") diff --git a/tests/test_cnf.py b/tests/test_cnf.py new file mode 100644 index 0000000..c2f4149 --- /dev/null +++ b/tests/test_cnf.py @@ -0,0 +1,104 @@ +import os +import sys + +# Add the parent directory to the system path +DIR_PATH = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, os.path.join(DIR_PATH, '..')) +import re + +import numpy as np +import math +from io import StringIO +import tempfile + +from ariths_gen.core.cgp_circuit import UnsignedCGPCircuit +from ariths_gen.core.arithmetic_circuits.general_circuit import GeneralCircuit + +class minisat_runner: + def __init__(self, circuit : GeneralCircuit): + # create tmp name in temporary directory with unique name + with tempfile.NamedTemporaryFile(delete=True, suffix=".cnf", dir="/tmp") as tmp_file: + self.cnf_file = tmp_file.name + + # create cnf file + circuit.get_cnf_code_flat(open(self.cnf_file, "w")) + + self.output = StringIO() + self.run_minisat() + + def run_minisat(self): + with tempfile.NamedTemporaryFile(delete=True, suffix=".out", dir="/tmp") as tmp_file: + self.output = tmp_file + self.retval = os.system(f"minisat {self.cnf_file} > {self.output.name}") + + self.output.seek(0) + self.output = self.output.read().decode() + return self.retval + + def get_output(self): + return self.output + + def get_results(self): + """ parses results in format + +============================[ Problem Statistics ]============================= +| | +| Number of variables: 6 | +| Number of clauses: 6 | +| Parse time: 0.00 s | +| Eliminated clauses: 0.00 Mb | +| Simplification time: 0.00 s | +| | +============================[ Search Statistics ]============================== +| Conflicts | ORIGINAL | LEARNT | Progress | +| | Vars Clauses Literals | Limit Clauses Lit/Cl | | +=============================================================================== +=============================================================================== +restarts : 1 +conflicts : 0 (0 /sec) +decisions : 1 (0.00 % random) (545 /sec) +propagations : 4 (2181 /sec) +conflict literals : 0 (-nan % deleted) +Memory used : 11.00 MB +CPU time : 0.001834 s + +SATISFIABLE + """ + ret = {"simplification": False} + for line in self.output.split("\n"): + if "SATISFIABLE" in line: + ret["SATISFIABLE"] = True + if "UNSATISFIABLE" in line: + ret["SATISFIABLE"] = False + if "Solved by simplification" in line: + ret["simplification"] = True + + if g := re.match(r".*Number of variables:\s+(\d+)", line): + ret["variables"] = int(g.groups()[0]) + if g := re.match(r".*Number of clauses:\s+(\d+)", line): + ret["clauses"] = int(g.groups()[0]) + if g := re.match(r"\s*conflicts\s*:\s*(\d+)", line): + ret["conflicts"] = int(g.groups()[0]) + if g := re.match(r"\s*decisions\s*:\s*(\d+)", line): + ret["decisions"] = int(g.groups()[0]) + + return ret + + +def test_cnf_minisat(): + # check optimization + # a AND (NOT a) + circ = UnsignedCGPCircuit("{4,1,1,8,2,1,0}([6]2,0,1)([7]2,6,2)([8]2,5,2)([9]8,7,4)([10]8,7,2)([11]3,5,2)([12]11,10,4)([13]11,10,2)(7)", [4]) + #circ = UnsignedCGPCircuit("{4,1,1,8,2,1,0}([6]2,3,2)([7]2,6,2)([8]2,5,2)([9]8,7,4)([10]8,7,2)([11]3,5,2)([12]11,10,4)([13]11,10,2)(7)", [4]) + runner = minisat_runner(circ) + #print(runner.get_output()) + #print(runner.get_results()) + res = runner.get_results() + assert res["simplification"] + assert res["clauses"] == 0 + assert not res["SATISFIABLE"] + + +if __name__ == "__main__": + test_cnf_minisat() + print("CNF Python tests were successful!")