Skip to content

Commit

Permalink
#49: Implemented constant logic from old template creator in refactor…
Browse files Browse the repository at this point in the history
…ed template manager
  • Loading branch information
Francesco-Cos committed Jul 10, 2024
1 parent 8d087d9 commit 10690eb
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 1 deletion.
3 changes: 3 additions & 0 deletions sxpat/template_manager/template.py
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,9 @@ def z3_abs_diff(a, b):
# Parameters variables declaration
{{{{params_declaration}}}}

# Constants variables declaration
{{{{consts_declaration}}}}

# wires functions declaration for exact circuit
{{{{exact_wires_declaration}}}}

Expand Down
17 changes: 16 additions & 1 deletion sxpat/template_manager/template_manager.py
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,12 @@ def _use_exact_var(self, node_name: str) -> str:

# is constant
if node_name in self.exact_constants.values():
return sxpat_cfg.Z3_GATES_DICTIONARY[self._exact_graph.graph.nodes[node_name][sxpat_cfg.LABEL]]
succs = list(self._current_graph.graph.successors(node_name))
if len(succs) == 1 and succs[0] in self._current_graph.output_dict.values():
output_i = next(node_i for node_i, node_name in self._current_graph.output_dict.items() if node_name == succs[0])
return f'{sxpat_cfg.CONSTANT_PREFIX}{output_i}'
else:
return sxpat_cfg.Z3_GATES_DICTIONARY[self._exact_graph.graph.nodes[node_name][sxpat_cfg.LABEL]]

# is gate
if node_name in self.exact_gates.values():
Expand Down Expand Up @@ -316,6 +321,16 @@ def _update_builder(self, builder: Builder) -> None:
# error
builder.update(error=self._encoding.output_variable('error'))

# consts_declaration
def get_single_predecessor(out_name): return next(self._current_graph.graph.predecessors(out_name))
constants = self._current_graph.constant_dict.values()
lines = [
self._gen_declare_gate(f'{sxpat_cfg.CONSTANT_PREFIX}{output_i}')
for output_i, output_name in self.outputs.items()
if get_single_predecessor(output_name) in constants
]
builder.update(consts_declaration='\n'.join(lines))

# exact_wires_declaration
builder.update(exact_wires_declaration='\n'.join(
self._gen_declare_bool_function(f'{sxpat_cfg.EXACT_WIRES_PREFIX}{len(self.inputs) + gate_i}', len(self.inputs))
Expand Down

0 comments on commit 10690eb

Please sign in to comment.