feat all: add AIG parser and RemoveConstantGates minimization#109
feat all: add AIG parser and RemoveConstantGates minimization#109Seva-Vaskin wants to merge 6 commits intoSPbSAT:mainfrom
Conversation
spefk
left a comment
spefk
left a comment
There was a problem hiding this comment.
Оставил разных комментариев (и минорных, и важных).
В целом, лучше приносить такие большие ПРы частями, потому что 4к кода сложно править и ревьюить (и вообще, по опыту количетсво строк в ПРе как минимум квадратично влияет на время проверки!). В этом ПРе как раз 2 несвязанные части есть, парсер и алгоритм минимизации, которые можно было бы разделить чтобы одно за другое не цеплялось.
| "pebble >= 5.0.7", | ||
| "graphviz >= 0.20.3", | ||
| "sortedcontainers (>=2.4.0,<3.0.0)", | ||
| "notebook (>=7.4.7,<8.0.0)", |
There was a problem hiding this comment.
Это лишняя зависимость для либы т.к. непосредственно не используется (и вообще, скорее однозначно пользовательская) -- нужно убрать и откатить poetry.lock на предыдущую версию (т.е. не update, а честный revert по истории)
И в целом, добавление/обновление зависимостей всегда лучше приносить отдельным ПРом, т.к. так проще отслеживать проблемы.
| @staticmethod | ||
| def from_aig_string(string: str) -> "Circuit": | ||
| """ | ||
| Initialize the circuit from an AIG format string. | ||
|
|
||
| Only ASCII AIG format (.aag) is supported for string input. Only combinational | ||
| circuits (without latches) are supported. | ||
|
|
||
| :param string: string containing AIG data in ASCII format. | ||
| :return: parsed Circuit object. | ||
|
|
||
| """ | ||
| from cirbo.core.parser.aig import AIGParser | ||
|
|
||
| parser = AIGParser() | ||
| return parser.parse_string(string) | ||
|
|
||
| @staticmethod | ||
| def from_aig_bytes(data: bytes) -> "Circuit": | ||
| """ | ||
| Initialize the circuit from AIG format bytes. | ||
|
|
||
| Supports both ASCII (.aag) and binary (.aig) AIGER formats. Only combinational | ||
| circuits (without latches) are supported. | ||
|
|
||
| :param data: bytes containing AIG data. | ||
| :return: parsed Circuit object. | ||
|
|
||
| """ | ||
| from cirbo.core.parser.aig import AIGParser | ||
|
|
||
| parser = AIGParser() | ||
| return parser.parse_bytes(data) |
There was a problem hiding this comment.
Минорно: правда ли на уровне парсера (и схемы соотв.) должны быть разные методы parse_bytes и parse_string, если это можно простой проверкой isinstance вывести динамически? Отдельный parse_file нужен чтобы отличить строку с путём от строки с данными
| __all__ = ['AIGParser'] | ||
|
|
||
|
|
||
| class AIGParseError(Exception): |
There was a problem hiding this comment.
Нужно отнаследовать от CirboError
| pass | ||
|
|
||
|
|
||
| class AIGParser: |
There was a problem hiding this comment.
Не нравится, что эта штука не наследуется от AbstractParser. Получаем две отдельные абстракции, из-за чего целостность теряется. Давай отнаследуем её и как базовый сценарий поддержим работу со строковым входом?
|
|
||
| """ | ||
| path = pathlib.Path(file_path) | ||
| if path.suffix == '.aag': |
There was a problem hiding this comment.
Минорно: чуть чище будет с endswith
| nonlocal _new_circuit, _label_remap, _gate_types | ||
|
|
||
| # remap operands to their simplified labels | ||
| remapped_operands = tuple(_get_remapped_label(op) for op in _gate.operands) |
There was a problem hiding this comment.
Минорно: тот относительно редкий случай, когда можно tuple(map(_get_remapped_label, _gate.operands))
| def _get_const_value(gate_type: gate.GateType) -> int: | ||
| return 1 if gate_type == gate.ALWAYS_TRUE else 0 |
There was a problem hiding this comment.
Немного течет интерфейс -- конст. гейты задаются в _CONST_GATES, а здесь проверяется только gate.ALWAYS_TRUE и else. Чище будет честно проверять оба if == gate.ALWAYS_TRUE и if == gate.ALWAYS_TRUE, и бросать ошибку иначе.
Как вариант, можно заменить _CONST_GATES на дикт где ключи -- типы, а значения -- константные значения этих типов гейтов.
Сами значения правильнее вычислять через вызов .operator (т.е. ALWAYS_TRUE.operator())
| const_operand_infos.append((idx, _get_const_value(op_type))) | ||
|
|
||
| # simplify if we have constant operands | ||
| if const_operand_infos and current_type not in (gate.INPUT, *_CONST_GATES): |
There was a problem hiding this comment.
На каждой итерации создается новый тапл в (gate.INPUT, *_CONST_GATES), что дорого.
| return new_type, new_operands | ||
|
|
||
|
|
||
| class RemoveConstantGates(Transformer): |
There was a problem hiding this comment.
У нас аналогичное упрощение написано в Simplifier'e, и перетащено в cirbo-search сейчас. Я точно не помно, но там вроде поддержано всякое, в т.ч. не только бинарные гейты. Если интересно, можно посмотреть как оно реализовано и поспрашивать Вику, если будет необходимость: https://github.com/SPbSAT/cirbo-search/blob/main/src/minimization/low_effort/constant_gate_reducer.hpp
В целом, в будущем планируем cirbo-search подсоединить в cirbo биндингами, и вызывать упрощения из него, поэтому доработки в рамках упрощений cirbo скорее ограниченно актуальны.
| if original_gate.gate_type == gate.IFF: | ||
| # IFF(const) = const | ||
| new_type = operand_gate_type | ||
| elif original_gate.gate_type == gate.NOT: | ||
| # NOT(ALWAYS_TRUE) = ALWAYS_FALSE, NOT(ALWAYS_FALSE) = ALWAYS_TRUE | ||
| new_type = gate.ALWAYS_FALSE if const_val == 1 else gate.ALWAYS_TRUE | ||
| else: | ||
| raise ValueError(f"Unsupported unary gate type: {original_gate.gate_type}") |
There was a problem hiding this comment.
Здесь тоже идет хардкод конкретных видов гейтов. Имхо, правильнее вызывать operator в нужных местах и довериться полиморфизму.
spefk
changed the title
2 participants
This PR adds two new features to cirbo: