From b7764cd7c621425d6ba36fd8e8d7e27c2a7768b7 Mon Sep 17 00:00:00 2001 From: Vojta Date: Wed, 15 Jan 2025 11:42:36 +0100 Subject: [PATCH] cnf implementation --- .../arithmetic_circuits/general_circuit.py | 103 ++++++++++++++++++ .../logic_gate_circuits/logic_gate_circuit.py | 3 + .../logic_gates/logic_gates.py | 69 +++++++++++- 3 files changed, 173 insertions(+), 2 deletions(-) diff --git a/ariths_gen/core/arithmetic_circuits/general_circuit.py b/ariths_gen/core/arithmetic_circuits/general_circuit.py index 95d3f31..e09fdf5 100644 --- a/ariths_gen/core/arithmetic_circuits/general_circuit.py +++ b/ariths_gen/core/arithmetic_circuits/general_circuit.py @@ -1,3 +1,4 @@ +import json from ariths_gen.core.logic_gate_circuits.logic_gate_circuit import ( OneInputLogicGate, TwoInputLogicGate @@ -11,6 +12,8 @@ import inspect import copy from io import StringIO +from ariths_gen.wire_components.wires import ConstantWireValue0, ConstantWireValue1 + class GeneralCircuit(): """Class represents a general circuit and ensures its generation to various representations. @@ -856,3 +859,103 @@ class GeneralCircuit(): file_object.write(self.get_parameters_cgp()) 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. + """ + 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 = {} + + for i in self.inputs: + for j in range(i.N): + self.get_cnfvar(i[j], create=True) + + # 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" + hash_outputs[g.out] = (i, g) + + + active_outputs = set() + + # set ouput active + for i in range(self.out.N): + active_outputs.add(self.out[i].name) + + print(active_outputs) + # for all gates back + for g in reversed(self.circuit_gates): + if g.out.name in active_outputs: + # set output active + active_outputs.add(g.a.name) + if hasattr(g, "b"): + active_outputs.add(g.b.name) + if hasattr(g, "c"): + active_outputs += (g.c.name) + print("Setting active output", g.out, " for gate ", g) + + + print("active outputs", active_outputs) + + print(hash_outputs) + + + #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 + allcnfs += g.get_cnf_clause(self) + + allcnfs.append([self.get_cnfvar(self.out[0])]) + const1 = ConstantWireValue1() + if str(const1) in self.cnf_vars: + allcnfs.append([self.get_cnfvar(const1)]) + + + # header p cnf + file_object.write(f"p cnf {self.cnf_varid-1} {len(allcnfs)}\n") + + 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") + + + + def get_cnfvar(self, wire : Wire, create = False): + wireid = str(wire) + if wireid in self.cnf_vars: + assert not create, f"Wire {wireid} already found in CNF vars for {wire}" + elif wire.is_const(): + # create FALSE variable + print("Creating new CNF var for constant wires", wire, " id ", wireid) + self.cnf_vars[str(ConstantWireValue0())] = -self.cnf_varid + self.cnf_vars[str(ConstantWireValue1())] = self.cnf_varid + self.cnf_var_comments[self.cnf_varid] = True + + + self.cnf_varid += 1 + else: + assert create, f"Wire {wireid} not found in CNF vars" + print("Creating new CNF var for wire", wire, " id ", wireid) + self.cnf_var_comments[self.cnf_varid] = wire.name + self.cnf_vars[wireid] = self.cnf_varid + self.cnf_varid += 1 + return self.cnf_vars[wireid] + + def set_cnfvar(self, wire : Wire, value : int): + """ for buffers and inverters """ + wireid = str(wire) + assert not wireid in self.cnf_vars, f"Wire {wireid} already found in CNF vars for {wire}" + self.cnf_vars[wireid] = value \ No newline at end of file diff --git a/ariths_gen/core/logic_gate_circuits/logic_gate_circuit.py b/ariths_gen/core/logic_gate_circuits/logic_gate_circuit.py index 76c122d..f635d91 100644 --- a/ariths_gen/core/logic_gate_circuits/logic_gate_circuit.py +++ b/ariths_gen/core/logic_gate_circuits/logic_gate_circuit.py @@ -500,6 +500,9 @@ class TwoInputLogicGate(): file_object.write(self.get_parameters_cgp()) file_object.write(self.get_gate_triplet_cgp()) + def get_cnf_clause(self, parent): + raise NotImplementedError(f"CNF generation is not implemented for this class. {self.__class__.__name__}") + class TwoInputInvertedLogicGate(TwoInputLogicGate): """Class representing two input inverted logic gates. diff --git a/ariths_gen/one_bit_circuits/logic_gates/logic_gates.py b/ariths_gen/one_bit_circuits/logic_gates/logic_gates.py index 822b850..7f65e0a 100644 --- a/ariths_gen/one_bit_circuits/logic_gates/logic_gates.py +++ b/ariths_gen/one_bit_circuits/logic_gates/logic_gates.py @@ -60,6 +60,41 @@ class AndGate(TwoInputLogicGate): else: return f".names {self.a.get_wire_value_blif()} {self.b.get_wire_value_blif()} {self.out.get_wire_value_blif()}\n" + \ f"11 1\n" + + def get_cnf_clause(self, parent): + """Generates CNF clause representing AND gate Boolean function using its truth table.""" + + + x = parent.get_cnfvar(self.a) + y = parent.get_cnfvar(self.b) + + if x == -y: # a AND ~a + z = parent.get_cnfvar(ConstantWireValue0()) + parent.set_cnfvar(self.out, z) + return [] + + z = parent.get_cnfvar(self.out, create = True) + +# return f"[[{x},-{z}],[{y},-{z}],[{z},-{x},-{y}]]" + return [[x,-z],[y,-z],[-x,-y,z]] +# """ +# auto z = getnewvar(); +# z je vystupni promenna hradla + +# x <- getvar(in1) +# y <- getvar(in2) + +# do CNF ukladam: + +# XOR: + +# [[-x,y,z],[x,-y,z],[-x,-y,-z],[x,y,-z]] + +# AND: + +# [[x,-z],[y,-z],[-x,-y-,-z]] + + class NandGate(TwoInputInvertedLogicGate): @@ -281,7 +316,7 @@ class XorGate(TwoInputLogicGate): # If constant input is present, logic gate is not generated and corresponding # input value is propagated to the output to connect to other components if a.is_const() and a.value == 1: - assert self.parent_component, "Parent component for gate {self} is not defined" + assert self.parent_component, f"Parent component for gate {self} is not defined" output = NotGate(a=b, prefix=prefix + "_not", outid=outid, parent_component=parent_component) self.parent_component.add_component(output) if parent_component is not None else None self.out = output.out @@ -290,7 +325,7 @@ class XorGate(TwoInputLogicGate): self.out = b self.disable_generation = True elif b.is_const() and b.value == 1: - assert self.parent_component, "Parent component for gate {self} is not defined" + assert self.parent_component, f"Parent component for gate {self} is not defined" output = NotGate(a=a, prefix=prefix + "_not", outid=outid, parent_component=parent_component) self.parent_component.add_component(output) if parent_component is not None else None self.out = output.out @@ -300,6 +335,31 @@ class XorGate(TwoInputLogicGate): self.disable_generation = True else: self.out = Wire(name=prefix) + + + def get_cnf_clause(self, parent): + z = parent.get_cnfvar(self.out, create = True) + x = parent.get_cnfvar(self.a) + y = parent.get_cnfvar(self.b) + + return [[ -x, y, z], [x,-y,z],[x,y,-z],[x,-y,-z]] + +# """ +# auto z = getnewvar(); +# z je vystupni promenna hradla + +# x <- getvar(in1) +# y <- getvar(in2) + +# do CNF ukladam: + +# XOR: + +# [[-x,y,z],[x,-y,z],[-x,-y,-z],[x,y,-z]] + +# AND: + +# [[x,-z],[y,-z],[-x,-y-,-z]] """ BLIF CODE GENERATION """ def get_function_blif(self): @@ -432,3 +492,8 @@ class NotGate(OneInputLogicGate): else: return f".names {self.a.get_wire_value_blif()} {self.out.get_wire_value_blif()}\n" + \ f"0 1\n" + + def get_cnf_clause(self, parent): + x = parent.get_cnfvar(self.a) + parent.set_cnfvar(self.out, -x) + return [] \ No newline at end of file