CNF testing

.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

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")
 
 
 

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!")