From 4af98c3107fe3687d2af7c7443038b4bab18ba2e Mon Sep 17 00:00:00 2001 From: vikria Date: Mon, 21 Oct 2024 21:23:08 +0300 Subject: [PATCH 01/10] update version --- .../duplicate_gates_cleaner.hpp | 174 ++++++++++++------ 1 file changed, 120 insertions(+), 54 deletions(-) diff --git a/src/simplification/duplicate_gates_cleaner.hpp b/src/simplification/duplicate_gates_cleaner.hpp index 8fa7606..5a73c06 100644 --- a/src/simplification/duplicate_gates_cleaner.hpp +++ b/src/simplification/duplicate_gates_cleaner.hpp @@ -1,21 +1,17 @@ #pragma once -#include -#include #include -#include +#include +#include #include +#include +#include -#include "src/algo.hpp" -#include "src/common/csat_types.hpp" -#include "src/simplification/transformer_base.hpp" -#include "src/structures/circuit/gate_info.hpp" -#include "src/structures/circuit/icircuit.hpp" -#include "src/utility/converters.hpp" -#include "src/utility/encoder.hpp" -#include "src/utility/logger.hpp" +#include "core/framework/algorithms/algo.hpp" +#include "core/framework/preprocessing/transformer_base.hpp" +#include "core/framework/utility/converters.hpp" -namespace csat::simplification +namespace csat::preprocessing { /** @@ -23,10 +19,13 @@ namespace csat::simplification * Duplicates are gates with the same operands and operator * * Note that this algorithm requires RedundantGatesCleaner to be applied right before. + * Note that this algorithm will not reduce duplicate operands of gate, but will account + * them "as one operand" during duplicates search. To reduce such gates one can use + * separate `DuplicateOperandsCleaner` strategy. * * @tparam CircuitT */ -template>> +template > > class DuplicateGatesCleaner_ : public ITransformer { csat::Logger logger{"DuplicateGatesCleaner"}; @@ -34,65 +33,69 @@ class DuplicateGatesCleaner_ : public ITransformer public: CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr> encoder) + std::unique_ptr encoder) { logger.debug("========================================================================================="); logger.debug("START DuplicateGatesCleaner"); - logger.debug("Top sort"); + GateEncoder new_encoder{}; + + // Topsort, from inputs to outputs. csat::GateIdContainer gateSorting(algo::TopSortAlgorithm::sorting(*circuit)); std::reverse(gateSorting.begin(), gateSorting.end()); - logger.debug("Building mask to delete gates and filling map -- old_to_new_gateId"); - // 0 -- if gate is a duplicate, 1 -- otherwise - BoolVector safe_mask(circuit->getNumberOfGates(), true); - // maps encoded (`operator_operand1_operand2...`) gate to new gate id - GateEncoder auxiliary_names_encoder{}; - // surjection of old gate ids to new gate ids - std::map old_to_new_gateId{}; - // bijection of old gate ids to new gate ids - GateEncoder new_encoder{}; - std::string encoded_name; + BoolVector safe_mask(circuit->getNumberOfGates(), true); // 0 -- if gate is a duplicate, 1 -- otherwise + + // `auxiliary_encoder` helps to deduplicate gates by mapping same auxiliary name to one index. + GateEncoder auxiliary_encoder{}; + // maps original gate ID to auxiliary ID, gotten from `auxiliary_encoder`. + std::unordered_map gate_id_to_auxiliary_id{}; + logger.debug("Building mask to delete gates and filling map -- gate_id_to_auxiliary_id"); + std::string auxiliary_name; for (GateId gateId : gateSorting) { - encoded_name = get_gate_auxiliary_name_( - gateId, circuit->getGateType(gateId), circuit->getGateOperands(gateId), old_to_new_gateId); - logger.debug("Gate number ", gateId, ". Its encoded_name is ", encoded_name); + logger.debug("Processing gate ", gateId); + auxiliary_name.clear(); + auxiliary_name = formatGateAuxiliaryName_( + gateId, circuit->getGateType(gateId), circuit->getGateOperands(gateId), gate_id_to_auxiliary_id); + logger.debug("Auxiliary name for gate ", gateId, " is ", auxiliary_name); - if (auxiliary_names_encoder.keyExists(encoded_name)) + if (auxiliary_encoder.keyExists(auxiliary_name)) { logger.debug("Gate number ", gateId, " is a Duplicate and will be removed."); - safe_mask.at(gateId) = 0; + safe_mask.at(gateId) = false; } else { - new_encoder.encodeGate(gateId); + logger.debug( + "Gate number ", gateId, " is either unique, or first of found duplicated, and will be saved."); + new_encoder.encodeGate(encoder->decodeGate(gateId)); } - old_to_new_gateId[gateId] = auxiliary_names_encoder.encodeGate(encoded_name); + gate_id_to_auxiliary_id[gateId] = auxiliary_encoder.encodeGate(auxiliary_name); } logger.debug("Building new circuit"); - GateInfoContainer gate_info(auxiliary_names_encoder.size()); + GateInfoContainer gate_info(auxiliary_encoder.size()); for (GateId gateId = 0; gateId < circuit->getNumberOfGates(); ++gateId) { - if (safe_mask.at(gateId) != 0) + if (safe_mask.at(gateId)) { logger.debug( "New Gate ", - old_to_new_gateId.at(gateId), + gate_id_to_auxiliary_id.at(gateId), "; Type: ", utils::gateTypeToString(circuit->getGateType(gateId)), - "; Operands: "); + "; Operands: ", + formatOperandsString_(circuit->getGateOperands(gateId), gate_id_to_auxiliary_id).str()); GateIdContainer masked_operands_{}; for (GateId operand : circuit->getGateOperands(gateId)) { - masked_operands_.push_back(old_to_new_gateId.at(operand)); - logger.debug(old_to_new_gateId.at(operand)); + masked_operands_.push_back(gate_id_to_auxiliary_id.at(operand)); } - gate_info.at(old_to_new_gateId.at(gateId)) = {circuit->getGateType(gateId), masked_operands_}; + gate_info.at(gate_id_to_auxiliary_id.at(gateId)) = {circuit->getGateType(gateId), masked_operands_}; } } @@ -100,37 +103,100 @@ class DuplicateGatesCleaner_ : public ITransformer new_output_gates.reserve(circuit->getOutputGates().size()); for (GateId output_gate : circuit->getOutputGates()) { - new_output_gates.push_back(old_to_new_gateId.at(output_gate)); + new_output_gates.push_back(gate_id_to_auxiliary_id.at(output_gate)); } logger.debug("END DuplicateGatesCleaner"); logger.debug("========================================================================================="); - return { - std::make_unique(gate_info, new_output_gates), utils::mergeGateEncoders(*encoder, new_encoder)}; + return {std::make_unique(gate_info, new_output_gates), std::make_unique(new_encoder)}; }; private: - std::string get_gate_auxiliary_name_( - GateId idx, - GateType type, + /** + * Formats new auxiliary name for the gate based on its attributes (type, operands). + * Such name may be used to determine literal duplicates in the circuit. + * + * @param gateId -- original ID of gate. + * @param gateType -- type of gate. + * @param operands -- gate's operand IDs. + * @param encoder -- mapping of circuit gates' original IDs to new names. Must already contain + * value for each operand of provided gate. It is needed to detect dependant duplicates + * in only one circuit iteration. + * @return auxiliary name of gate. + */ + std::string formatGateAuxiliaryName_( + GateId gateId, + GateType gateType, GateIdContainer const& operands, - std::map const& encoder) + std::unordered_map const& deduplicator) { - std::string encoded_name; - encoded_name = std::to_string(static_cast(type)); + std::stringstream auxiliary_name; + auxiliary_name << std::to_string(static_cast(gateType)); + + // All Input gates are unique, but we can't differentiate them + // by their operands (since there are none), so we simply add + // their current (unique) index to auxiliary name and return. + if (gateType == GateType::INPUT) + { + auxiliary_name << '_' + std::to_string(gateId); + return auxiliary_name.str(); + } - if (type == GateType::INPUT) + // Preparing set of operands, by accounting already found duplicates. + GateIdContainer prepared_operands{}; + prepared_operands.reserve(operands.size()); + std::transform( + operands.begin(), + operands.end(), + std::back_inserter(prepared_operands), + [&deduplicator](GateId operand) { return deduplicator.at(operand); }); + + // For gates defined by symmetrical function operands are sorted during + // circuit construction (see GateInfo), but then some of their operands + // may be decided to be duplicates, so we resort them so such gates with + // same set of operands will have same auxiliary name and will be detected + // as duplicates. + if (utils::symmetricOperatorQ(gateType)) { - encoded_name += '_' + std::to_string(idx); + std::sort(prepared_operands.begin(), prepared_operands.end()); + // Since several operands of same gate may be decided to be duplicates + // we can have here something like `AND(X, X, Y)`, which is equivalent + // to the `AND(X, Y)`, hence to allow such duplicated to be found we + // also clean such duplicates. + if (utils::reducibleMultipleOperandsQ(gateType)) + { + // Note: `unique` requires container to be sorted. + auto last = std::unique(prepared_operands.begin(), prepared_operands.end()); + prepared_operands.erase(last, prepared_operands.end()); + } } - for (GateId const operand : operands) + // Adds names of gate's operands to its auxiliary name. + for (GateId operand : prepared_operands) { - encoded_name += '_' + std::to_string(encoder.at(operand)); + auxiliary_name << '_' + std::to_string(operand); } - return encoded_name; + return auxiliary_name.str(); }; + + std::stringstream formatOperandsString_( + GateIdContainer const& operands, + std::unordered_map const& encoder) + { + std::stringstream ss; + if (operands.empty()) + { + return ss; + } + + ss << encoder.at(operands[0]); + for (auto ptr = operands.begin() + 1; ptr != operands.end(); ++ptr) + { + ss << ',' << encoder.at(*ptr); + } + return ss; + } }; -} // namespace csat::simplification +} // namespace csat::preprocessing \ No newline at end of file From 4711566b5288feb714b7c626e3b1d9de3fefac75 Mon Sep 17 00:00:00 2001 From: vikria Date: Mon, 21 Oct 2024 21:26:18 +0300 Subject: [PATCH 02/10] fix --- src/simplification/duplicate_gates_cleaner.hpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/simplification/duplicate_gates_cleaner.hpp b/src/simplification/duplicate_gates_cleaner.hpp index 5a73c06..684e81b 100644 --- a/src/simplification/duplicate_gates_cleaner.hpp +++ b/src/simplification/duplicate_gates_cleaner.hpp @@ -7,11 +7,11 @@ #include #include -#include "core/framework/algorithms/algo.hpp" -#include "core/framework/preprocessing/transformer_base.hpp" -#include "core/framework/utility/converters.hpp" +#include "src/algo.hpp" +#include "src/simplification/transformer_base.hpp" +#include "src/utility/converters.hpp" -namespace csat::preprocessing +namespace csat::simplification { /** @@ -199,4 +199,4 @@ class DuplicateGatesCleaner_ : public ITransformer } }; -} // namespace csat::preprocessing \ No newline at end of file +} // namespace csat::simplification \ No newline at end of file From 12d65f317485bc25f9bcde9467e5c168eb9c8d25 Mon Sep 17 00:00:00 2001 From: vikria Date: Mon, 21 Oct 2024 21:26:56 +0300 Subject: [PATCH 03/10] fix --- src/simplification/duplicate_gates_cleaner.hpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/simplification/duplicate_gates_cleaner.hpp b/src/simplification/duplicate_gates_cleaner.hpp index 684e81b..1ce214d 100644 --- a/src/simplification/duplicate_gates_cleaner.hpp +++ b/src/simplification/duplicate_gates_cleaner.hpp @@ -199,4 +199,4 @@ class DuplicateGatesCleaner_ : public ITransformer } }; -} // namespace csat::simplification \ No newline at end of file +} // namespace csat::simplification From 9d9cf1f1903bd88331b0d1c761622f6dd97b5241 Mon Sep 17 00:00:00 2001 From: vikria Date: Mon, 21 Oct 2024 21:33:25 +0300 Subject: [PATCH 04/10] need refactor --- src/simplification/duplicate_gates_cleaner.hpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/simplification/duplicate_gates_cleaner.hpp b/src/simplification/duplicate_gates_cleaner.hpp index 1ce214d..5f5269b 100644 --- a/src/simplification/duplicate_gates_cleaner.hpp +++ b/src/simplification/duplicate_gates_cleaner.hpp @@ -33,12 +33,12 @@ class DuplicateGatesCleaner_ : public ITransformer public: CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr encoder) + std::unique_ptr> encoder) { logger.debug("========================================================================================="); logger.debug("START DuplicateGatesCleaner"); - GateEncoder new_encoder{}; + GateEncoder new_encoder{}; // Topsort, from inputs to outputs. csat::GateIdContainer gateSorting(algo::TopSortAlgorithm::sorting(*circuit)); @@ -47,7 +47,7 @@ class DuplicateGatesCleaner_ : public ITransformer BoolVector safe_mask(circuit->getNumberOfGates(), true); // 0 -- if gate is a duplicate, 1 -- otherwise // `auxiliary_encoder` helps to deduplicate gates by mapping same auxiliary name to one index. - GateEncoder auxiliary_encoder{}; + GateEncoder auxiliary_encoder{}; // maps original gate ID to auxiliary ID, gotten from `auxiliary_encoder`. std::unordered_map gate_id_to_auxiliary_id{}; From 8112bd32acc8e22351dd2cfd8c3f429a801dcfcd Mon Sep 17 00:00:00 2001 From: vikria Date: Tue, 22 Oct 2024 18:31:18 +0300 Subject: [PATCH 05/10] update algo + encoder --- app/simplify.cpp | 12 +- src/parser/ibench_parser.hpp | 4 +- src/simplification/composition.hpp | 4 +- src/simplification/constant_gate_reducer.hpp | 6 +- .../duplicate_operands_cleaner.hpp | 4 +- src/simplification/reduce_not_composition.hpp | 4 +- .../redundant_gates_cleaner.hpp | 41 ++++-- .../three_inputs_optimization.hpp | 6 +- .../three_inputs_optimization_bench.hpp | 4 +- src/simplification/transformer_base.hpp | 10 +- src/utility/converters.hpp | 31 ++++- src/utility/encoder.hpp | 130 +++--------------- src/utility/write_utils.hpp | 2 +- .../simplification/constant_gate_reducer.cpp | 18 +-- .../duplicate_gates_cleaner.cpp | 10 +- .../duplicate_operands_cleaner.cpp | 22 +-- .../simplification/reduce_not_composition.cpp | 8 +- .../redundant_gates_cleaner.cpp | 10 +- .../simplification/utils/three_coloring.cpp | 8 +- .../simplification/utils/two_coloring.cpp | 10 +- tests/src_test/utility/encoder_test.cpp | 33 +---- 21 files changed, 148 insertions(+), 229 deletions(-) diff --git a/app/simplify.cpp b/app/simplify.cpp index 293caf7..3710cc4 100644 --- a/app/simplify.cpp +++ b/app/simplify.cpp @@ -24,7 +24,7 @@ /** * prints circuit (encoded name => name from file) */ -void printCircuit(csat::DAG const &circuit, csat::utils::GateEncoder const &encoder) { +void printCircuit(csat::DAG const &circuit, csat::utils::GateEncoder const &encoder) { for (auto input: circuit.getInputGates()) { std::cout << "INPUT(" << input << " => " << encoder.decodeGate(input) << ")\n"; } @@ -75,7 +75,7 @@ std::ifstream openInputFile(const std::string &file_path, csat::Logger &logger) } std::unique_ptr parseCircuitFile(std::ifstream &file, const std::string &file_path, csat::Logger &logger, - csat::utils::GateEncoder &encoder) { + csat::utils::GateEncoder &encoder) { logger.debug("Reading file ", file_path, "."); auto parser = csat::parser::BenchToCircuit(); parser.parseStream(file); @@ -83,9 +83,9 @@ std::unique_ptr parseCircuitFile(std::ifstream &file, const std::stri return parser.instantiate(); } -std::tuple, std::unique_ptr > > applyPreprocessing( +std::tuple, std::unique_ptr > applyPreprocessing( std::string const& basis, std::unique_ptr &csat_instance, - csat::utils::GateEncoder &encoder) { + csat::utils::GateEncoder &encoder) { if (basis == "AIG") { return csat::simplification::Composition< csat::DAG, @@ -123,7 +123,7 @@ std::tuple, std::unique_ptr &csat_instance, - csat::utils::GateEncoder &encoder, const std::string &file_path) { + csat::utils::GateEncoder &encoder, const std::string &file_path) { if (auto output_dir = program.present("-o")) { std::ofstream file_out(*output_dir / std::filesystem::path(file_path).filename()); WriteBenchFile(*csat_instance, encoder, file_out); @@ -185,7 +185,7 @@ void runBenchmark(const std::string &file_path, const argparse::ArgumentParser & std::optional &file_stat) { auto file = openInputFile(file_path, logger); - csat::utils::GateEncoder encoder; + csat::utils::GateEncoder encoder; auto csat_instance = parseCircuitFile(file, file_path, logger, encoder); int64_t gatesBefore = csat_instance->getNumberOfGates(); diff --git a/src/parser/ibench_parser.hpp b/src/parser/ibench_parser.hpp index 170f165..38254c3 100644 --- a/src/parser/ibench_parser.hpp +++ b/src/parser/ibench_parser.hpp @@ -44,13 +44,13 @@ class IBenchParser : public ICircuitParser } /* Encoder of inputs and gates. */ - csat::utils::GateEncoder encoder; + csat::utils::GateEncoder encoder; /** * @return Encoder, built according to parser info. */ [[nodiscard]] - csat::utils::GateEncoder const& getEncoder() const + csat::utils::GateEncoder const& getEncoder() const { return encoder; } diff --git a/src/simplification/composition.hpp b/src/simplification/composition.hpp index 62e13be..30bfb14 100644 --- a/src/simplification/composition.hpp +++ b/src/simplification/composition.hpp @@ -39,7 +39,7 @@ struct Composition : public ITransformer */ CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr> encoder) + std::unique_ptr encoder) { auto _transformer = TransformerT(); auto [_circuit, _encoder] = _transformer.transform(std::move(circuit), std::move(encoder)); @@ -61,7 +61,7 @@ struct Composition : public ITransformer public: CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr> encoder) + std::unique_ptr encoder) { auto _transformer = TransformerT(); return _transformer.transform(std::move(circuit), std::move(encoder)); diff --git a/src/simplification/constant_gate_reducer.hpp b/src/simplification/constant_gate_reducer.hpp index 06e4cc4..cd0dfaf 100644 --- a/src/simplification/constant_gate_reducer.hpp +++ b/src/simplification/constant_gate_reducer.hpp @@ -53,7 +53,7 @@ class ConstantGateReducer_ : public ITransformer */ CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr> encoder) + std::unique_ptr encoder) { logger.debug("START ConstantGateReducer"); @@ -232,7 +232,7 @@ class ConstantGateReducer_ : public ITransformer return { std::make_unique(std::move(gate_info), std::move(new_output_gates)), - std::make_unique>(*encoder)}; + std::make_unique(*encoder)}; }; private: @@ -265,7 +265,7 @@ class ConstantGateReducer_ : public ITransformer */ void createMiniCircuit_( GateInfoContainer& gate_info, - GateEncoder& encoder, + GateEncoder& encoder, GateIdContainer& new_output_gates, std::string const& new_gate_name_prefix, GateId& circuit_size, diff --git a/src/simplification/duplicate_operands_cleaner.hpp b/src/simplification/duplicate_operands_cleaner.hpp index 3747f1c..7ab21a6 100644 --- a/src/simplification/duplicate_operands_cleaner.hpp +++ b/src/simplification/duplicate_operands_cleaner.hpp @@ -56,7 +56,7 @@ class DuplicateOperandsCleaner_ : public ITransformer */ CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr> encoder) + std::unique_ptr encoder) { logger.debug("START DuplicateOperandsCleaner"); @@ -265,7 +265,7 @@ class DuplicateOperandsCleaner_ : public ITransformer return { std::make_unique(std::move(gate_info), std::move(new_output_gates)), - std::make_unique>(*encoder)}; + std::make_unique(*encoder)}; }; private: diff --git a/src/simplification/reduce_not_composition.hpp b/src/simplification/reduce_not_composition.hpp index d2b6e9b..055dbc5 100644 --- a/src/simplification/reduce_not_composition.hpp +++ b/src/simplification/reduce_not_composition.hpp @@ -39,7 +39,7 @@ class ReduceNotComposition_ : public ITransformer */ CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr> encoder) + std::unique_ptr encoder) { logger.debug("========================================================================================="); logger.debug("START ReduceNotComposition"); @@ -73,7 +73,7 @@ class ReduceNotComposition_ : public ITransformer return { std::make_unique(gate_info, circuit->getOutputGates()), - std::make_unique>(*encoder)}; + std::make_unique(*encoder)}; }; private: diff --git a/src/simplification/redundant_gates_cleaner.hpp b/src/simplification/redundant_gates_cleaner.hpp index e66a642..57f442f 100644 --- a/src/simplification/redundant_gates_cleaner.hpp +++ b/src/simplification/redundant_gates_cleaner.hpp @@ -3,7 +3,8 @@ #include #include #include -#include +#include +#include #include "src/algo.hpp" #include "src/common/csat_types.hpp" @@ -40,61 +41,75 @@ class RedundantGatesCleaner_ : public ITransformer */ CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr> encoder) + std::unique_ptr encoder) { logger.debug("========================================================================================="); logger.debug("START RedundantGatesCleaner."); - GateEncoder encoder_old_to_new{}; + GateEncoder new_encoder{}; // Use dfs to get markers of visited and unvisited gates auto mask_use_output = algo::performDepthFirstSearch(*circuit, circuit->getOutputGates()); - // first step: getting valid encoding + // First step: getting valid encoding -- encode only gates, which will + // be taken to the new circuit (hence discarding all redundant gates). for (GateId gateId = 0; gateId < circuit->getNumberOfGates(); ++gateId) { + std::string_view gate_name = encoder->decodeGate(gateId); if (mask_use_output.at(gateId) != algo::DFSState::UNVISITED || (preserveInputs && circuit->getGateType(gateId) == GateType::INPUT)) { - encoder_old_to_new.encodeGate(gateId); + new_encoder.encodeGate(gate_name); continue; } - logger.debug("Gate number ", gateId, " is redundant and will be removed"); + logger.debug("Gate '", gate_name, "' (#", gateId, ") is redundant and will be removed"); } - // Rebuid circuit - GateInfoContainer gate_info(encoder_old_to_new.size()); + // Second step: recollect each gate data by encoding all its operands with + // new encoder build above. + GateInfoContainer gate_info(new_encoder.size()); for (GateId gateId = 0; gateId < circuit->getNumberOfGates(); ++gateId) { - if (encoder_old_to_new.keyExists(gateId)) + std::string_view gate_name = encoder->decodeGate(gateId); + // If new encoder doesn't contain name of a gate, this gate is redundant. + if (new_encoder.keyExists(gate_name)) { GateIdContainer encoded_operands_{}; for (GateId operand : circuit->getGateOperands(gateId)) { + // All operands must be visited, since current gate was visited. assert( mask_use_output.at(gateId) != algo::DFSState::UNVISITED || (preserveInputs && circuit->getGateType(gateId) == GateType::INPUT)); - encoded_operands_.push_back(encoder_old_to_new.encodeGate(operand)); + std::string_view operand_name = encoder->decodeGate(operand); + encoded_operands_.push_back(new_encoder.encodeGate(operand_name)); } - gate_info.at(encoder_old_to_new.encodeGate(gateId)) = { + // Build new gate info object for current gate. + gate_info.at(new_encoder.encodeGate(gate_name)) = { circuit->getGateType(gateId), std::move(encoded_operands_)}; } } + // Third step: recollect output gates. // All outputs must be visited since DFS starts from them. GateIdContainer new_output_gates{}; new_output_gates.reserve(circuit->getOutputGates().size()); for (GateId output_gate : circuit->getOutputGates()) { - new_output_gates.push_back(encoder_old_to_new.encodeGate(output_gate)); + assert( + mask_use_output.at(output_gate) != algo::DFSState::UNVISITED + || (preserveInputs && circuit->getGateType(output_gate) == GateType::INPUT)); + + std::string_view output_name = encoder->decodeGate(output_gate); + new_output_gates.push_back(new_encoder.encodeGate(output_name)); } logger.debug("END RedundantGatesCleaner."); logger.debug("========================================================================================="); return { std::make_unique(std::move(gate_info), std::move(new_output_gates)), - utils::mergeGateEncoders(*encoder, encoder_old_to_new)}; + std::make_unique(new_encoder)}; }; }; diff --git a/src/simplification/three_inputs_optimization.hpp b/src/simplification/three_inputs_optimization.hpp index fb0185c..553edec 100644 --- a/src/simplification/three_inputs_optimization.hpp +++ b/src/simplification/three_inputs_optimization.hpp @@ -169,7 +169,7 @@ class ThreeInputsSubcircuitMinimization : public ITransformer CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr> encoder) + std::unique_ptr encoder) { logger.debug("========================================================================================="); logger.debug("START ThreeInputsSubcircuitMinimization"); @@ -203,7 +203,7 @@ class ThreeInputsSubcircuitMinimization : public ITransformer { return { std::make_unique(gate_info, circuit->getOutputGates()), - std::make_unique>(*encoder)}; + std::make_unique(*encoder)}; } CircuitStatsSingleton::getInstance().iter_number += 1; CircuitStatsSingleton::getInstance().last_iter_gates_simplification = 0; @@ -744,7 +744,7 @@ class ThreeInputsSubcircuitMinimization : public ITransformer return { std::make_unique(gate_info, circuit->getOutputGates()), - std::make_unique>(*encoder)}; + std::make_unique(*encoder)}; } }; diff --git a/src/simplification/three_inputs_optimization_bench.hpp b/src/simplification/three_inputs_optimization_bench.hpp index 49f21bf..77183de 100644 --- a/src/simplification/three_inputs_optimization_bench.hpp +++ b/src/simplification/three_inputs_optimization_bench.hpp @@ -143,7 +143,7 @@ class ThreeInputsSubcircuitMinimizationBench : public ITransformer CircuitAndEncoder transform( std::unique_ptr circuit, - std::unique_ptr> encoder) + std::unique_ptr encoder) { logger.debug("========================================================================================="); logger.debug("START ThreeInputsSubcircuitMinimization"); @@ -714,7 +714,7 @@ class ThreeInputsSubcircuitMinimizationBench : public ITransformer return { std::make_unique(gate_info, circuit->getOutputGates()), - std::make_unique>(*encoder)}; + std::make_unique(*encoder)}; } }; diff --git a/src/simplification/transformer_base.hpp b/src/simplification/transformer_base.hpp index 3fe17a9..9a5cbae 100644 --- a/src/simplification/transformer_base.hpp +++ b/src/simplification/transformer_base.hpp @@ -16,8 +16,8 @@ namespace csat::simplification using csat::utils::GateEncoder; -template>> -using CircuitAndEncoder = std::pair, std::unique_ptr>>; +template>> +using CircuitAndEncoder = std::pair, std::unique_ptr>; /** * Base interface for all circuit transformers. @@ -28,14 +28,14 @@ template apply(CircuitT const& circuit, GateEncoder const& encoder) + CircuitAndEncoder apply(CircuitT const& circuit, GateEncoder const& encoder) { - return transform(std::make_unique(circuit), std::make_unique>(encoder)); + return transform(std::make_unique(circuit), std::make_unique(encoder)); } virtual CircuitAndEncoder transform( std::unique_ptr, - std::unique_ptr>) = 0; + std::unique_ptr) = 0; }; static std::string getUniqueId_() diff --git a/src/utility/converters.hpp b/src/utility/converters.hpp index e94085c..54efd09 100644 --- a/src/utility/converters.hpp +++ b/src/utility/converters.hpp @@ -148,7 +148,7 @@ inline MinArity gateTypeToMinArity(GateType gate_type) noexcept } /** - * @return True if the given `gate_type` can have arity greater than `gateTypeToMinArity(gate_type)`. + * @return True iff the given `gate_type` can have arity greater than `gateTypeToMinArity(gate_type)`. */ [[maybe_unused]] inline bool expandableArityQ(GateType gate_type) noexcept @@ -173,7 +173,7 @@ inline bool expandableArityQ(GateType gate_type) noexcept } /** - * @return True if operands can be swapped without changing the results. + * @return True iff operands can be swapped without changing the results. */ [[maybe_unused]] inline bool symmetricOperatorQ(GateType gate_type) noexcept @@ -197,4 +197,31 @@ inline bool symmetricOperatorQ(GateType gate_type) noexcept return _type_map.at(gate_type); } +/** + * @return True iff two gates of given type that differ only by number of multiple operands + * are equivalent (e.g. `AND(X, X, Y) ~ AND(X, Y)`, but `XOR(X, X, Y) !~ XOR(X, Y)`). + */ +inline bool reducibleMultipleOperandsQ(GateType gate_type) +noexcept +{ + static const std::unordered_map _type_map + { + {GateType::INPUT, true}, + {GateType::NOT, true}, + {GateType::AND, true}, + {GateType::NAND, true}, + {GateType::OR, true}, + {GateType::NOR, true}, + {GateType::XOR, false}, + {GateType::NXOR, false}, + {GateType::IFF, true}, + {GateType::MUX, false}, + {GateType::BUFF, true}, + {GateType::CONST_FALSE, true}, + {GateType::CONST_TRUE, true} + }; + + return _type_map.at(gate_type); +} + } // namespace csat::utils diff --git a/src/utility/encoder.hpp b/src/utility/encoder.hpp index 3cc5aed..3c15834 100644 --- a/src/utility/encoder.hpp +++ b/src/utility/encoder.hpp @@ -1,10 +1,7 @@ #pragma once -#include -#include -#include #include -#include +#include #include #include "src/common/csat_types.hpp" @@ -12,104 +9,28 @@ namespace csat::utils { -template -class GateEncoder -{ - protected: - /* Next var to be added to encoding map. */ - size_t next_var_ = 0; - /* Encoding map `variable name`->`numerical value`. */ - std::map encoder_{}; - /* Inverse encoding map. */ - std::map decoder_{}; - - public: - GateEncoder() = default; - GateEncoder(GateEncoder const&) = default; - ~GateEncoder() = default; - - /** - * @param key -- name of a gate that need to be encoded. - * @return id of gate in encoding from 0 through N. - */ - GateId encodeGate(KeyT const& key) noexcept - { - auto search = encoder_.find(key); - if (search == encoder_.end()) - { - decoder_[next_var_] = key; - encoder_[key] = next_var_; - return next_var_++; - } - else - { - return search->second; - } - }; - - /** - * @param id -- id of gate in encoding from 0 through N. - * @return Original gate name (key). - */ - [[nodiscard]] - KeyT decodeGate(GateId id) const - { - return decoder_.at(id); - }; - - /** - * @param key -- name of a gate that need to be check for presence. - * @return True if key is in class otherwise False. - */ - [[nodiscard]] - bool keyExists(KeyT const& key) const - { - return encoder_.find(key) != encoder_.end(); - }; - - /** - * Returns number of elements in encoding. - */ - [[nodiscard]] - size_t size() const - { - return next_var_; - } - - /** - * Clears internal state of encoder. - */ - void clear() - { - next_var_ = 0; - encoder_.clear(); - decoder_.clear(); - } -}; - /** - * GateEncoder specification for string, that allows usage of string_view. + * GateEncoder which allows to map original gate names to contiguous integers range. */ -template<> -class GateEncoder +class GateEncoder { protected: size_t next_var_ = 0; - std::map> encoder_; - std::map decoder_; - + std::map> encoder_{}; + std::map decoder_{}; + public: - GateEncoder() = default; + GateEncoder() = default; GateEncoder(GateEncoder const&) = default; - ~GateEncoder() = default; - - GateId encodeGate(std::string_view const& key) noexcept + ~GateEncoder() = default; + + GateId encodeGate(std::string_view key) + noexcept { auto search = encoder_.find(key); if (search == encoder_.end()) { - // TODO: rly string??? - decoder_[next_var_] = std::string(key); + decoder_[next_var_] = std::string(key); encoder_[std::string(key)] = next_var_; return next_var_++; } @@ -118,25 +39,25 @@ class GateEncoder return search->second; } }; - + [[nodiscard]] - std::string decodeGate(GateId id) const + std::string const& decodeGate(GateId id) const { return decoder_.at(id); }; - + [[nodiscard]] - bool keyExists(std::string_view const& key) const + bool keyExists(std::string_view key) const { return encoder_.find(key) != encoder_.end(); }; - + [[nodiscard]] size_t size() const { return next_var_; } - + void clear() { next_var_ = 0; @@ -145,19 +66,4 @@ class GateEncoder } }; -template -inline std::unique_ptr> mergeGateEncoders( - GateEncoder const& first, - GateEncoder const& second) noexcept -{ - GateEncoder _newEncoder; - - for (size_t code_two = 0; code_two < second.size(); ++code_two) - { - _newEncoder.encodeGate(first.decodeGate(second.decodeGate(code_two))); - } - - return std::make_unique>(_newEncoder); -} - } // namespace csat::utils diff --git a/src/utility/write_utils.hpp b/src/utility/write_utils.hpp index 566307a..18daecb 100644 --- a/src/utility/write_utils.hpp +++ b/src/utility/write_utils.hpp @@ -20,7 +20,7 @@ namespace csat template > > void WriteBenchFile( CircuitT const& circuit, - csat::utils::GateEncoder const& encoder, + csat::utils::GateEncoder const& encoder, std::ofstream& file_out) { csat::Logger const logger("WriteBenchFile"); diff --git a/tests/src_test/simplification/constant_gate_reducer.cpp b/tests/src_test/simplification/constant_gate_reducer.cpp index e5bfee0..b0f9149 100644 --- a/tests/src_test/simplification/constant_gate_reducer.cpp +++ b/tests/src_test/simplification/constant_gate_reducer.cpp @@ -30,7 +30,7 @@ TEST(ConstantGateReducer, SimpleTest) {5} ); - GateEncoder encoder{}; + GateEncoder encoder{}; encoder.encodeGate("0"); encoder.encodeGate("1"); encoder.encodeGate("2"); @@ -64,7 +64,7 @@ TEST(ConstantGateReducer, ChangeOutput) {2} ); - GateEncoder encoder{}; + GateEncoder encoder{}; encoder.encodeGate("0"); encoder.encodeGate("2"); encoder.encodeGate("1"); @@ -91,7 +91,7 @@ TEST(ConstantGateReducer, KnownAnswer) {2} ); - GateEncoder encoder{}; + GateEncoder encoder{}; encoder.encodeGate("0"); encoder.encodeGate("2"); encoder.encodeGate("1"); @@ -122,7 +122,7 @@ TEST(ConstantGateReducer, NoChanges) {2} ); - GateEncoder encoder{}; + GateEncoder encoder{}; encoder.encodeGate("0"); encoder.encodeGate("1"); encoder.encodeGate("2"); @@ -154,10 +154,12 @@ TEST(ConstantGateReducer, UnusedGates) {4} ); - GateEncoder encoder{}; + GateEncoder encoder{}; encoder.encodeGate("0"); encoder.encodeGate("1"); - encoder.encodeGate("2"); + encoder.encodeGate("2"); + encoder.encodeGate("3"); + encoder.encodeGate("4"); auto [circuit, _] = Composition< DAG, @@ -185,7 +187,7 @@ TEST(ConstantGateReducer, SeveralOutputs) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -218,7 +220,7 @@ TEST(ConstantGateReducer, SaveCONST) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, diff --git a/tests/src_test/simplification/duplicate_gates_cleaner.cpp b/tests/src_test/simplification/duplicate_gates_cleaner.cpp index b296540..c8d668d 100644 --- a/tests/src_test/simplification/duplicate_gates_cleaner.cpp +++ b/tests/src_test/simplification/duplicate_gates_cleaner.cpp @@ -30,7 +30,7 @@ TEST(DuplicateGatesCleaner, SimpleTest) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -62,7 +62,7 @@ TEST(DuplicateGatesCleaner, NoSorted) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -103,7 +103,7 @@ TEST(DuplicateGatesCleaner, SeveralLevels) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -145,7 +145,7 @@ TEST(DuplicateGatesCleaner, SeveralOutput) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -184,7 +184,7 @@ TEST(DuplicateGatesCleaner, SeveralLevelsMUX) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, diff --git a/tests/src_test/simplification/duplicate_operands_cleaner.cpp b/tests/src_test/simplification/duplicate_operands_cleaner.cpp index 5153c7b..2a5159a 100644 --- a/tests/src_test/simplification/duplicate_operands_cleaner.cpp +++ b/tests/src_test/simplification/duplicate_operands_cleaner.cpp @@ -30,7 +30,7 @@ TEST(DuplicateOperandsCleaner, KnownAnswer1) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -62,7 +62,7 @@ TEST(DuplicateOperandsCleaner, Bamboo) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -92,7 +92,7 @@ TEST(DuplicateOperandsCleaner, CreateNOT) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -129,7 +129,7 @@ TEST(DuplicateOperandsCleaner, MaxReductions) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -170,7 +170,7 @@ TEST(DuplicateOperandsCleaner, ChangeOutput1) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, encoder_] = Composition< DAG, @@ -202,7 +202,7 @@ TEST(DuplicateOperandsCleaner, ChangeOutputsType) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, encoder_] = Composition< DAG, @@ -231,7 +231,7 @@ TEST(DuplicateOperandsCleaner, KnownAnswer2) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -261,7 +261,7 @@ TEST(DuplicateOperandsCleaner, ChangeOutput2) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -291,7 +291,7 @@ TEST(DuplicateOperandsCleaner, InputIsOutput) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -320,7 +320,7 @@ TEST(DuplicateOperandsCleaner, SeveralOutputs) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -351,7 +351,7 @@ TEST(DuplicateOperandsCleaner, SaveCONST) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, diff --git a/tests/src_test/simplification/reduce_not_composition.cpp b/tests/src_test/simplification/reduce_not_composition.cpp index b88697c..87426d2 100644 --- a/tests/src_test/simplification/reduce_not_composition.cpp +++ b/tests/src_test/simplification/reduce_not_composition.cpp @@ -31,7 +31,7 @@ TEST(ReduceNotComposition, SimpleTest) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -66,7 +66,7 @@ TEST(ReduceNotComposition, UseMiddleNot) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -102,7 +102,7 @@ TEST(ReduceNotComposition, NotIsOutput) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -135,7 +135,7 @@ TEST(ReduceNotComposition, NoChanges) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, diff --git a/tests/src_test/simplification/redundant_gates_cleaner.cpp b/tests/src_test/simplification/redundant_gates_cleaner.cpp index f63df81..b901a40 100644 --- a/tests/src_test/simplification/redundant_gates_cleaner.cpp +++ b/tests/src_test/simplification/redundant_gates_cleaner.cpp @@ -33,7 +33,7 @@ TEST(RedundantGatesCleaner, SimpleTest) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -65,7 +65,7 @@ TEST(RedundantGatesCleaner, NotBreaksAnything) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -100,7 +100,7 @@ TEST(RedundantGatesCleaner, NotMarkedOutput) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -134,7 +134,7 @@ TEST(RedundantGatesCleaner, ConnectedOutputs) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, @@ -174,7 +174,7 @@ TEST(RedundantGatesCleaner, NewGatesMUXandCONST) parser.parseStream(stream); std::unique_ptr csat_instance = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); auto [circuit, _] = Composition< DAG, diff --git a/tests/src_test/simplification/utils/three_coloring.cpp b/tests/src_test/simplification/utils/three_coloring.cpp index 88ec671..c209fa3 100644 --- a/tests/src_test/simplification/utils/three_coloring.cpp +++ b/tests/src_test/simplification/utils/three_coloring.cpp @@ -19,7 +19,7 @@ using namespace csat::utils; std::pair>, std::vector>> parse_colors ( ThreeColoring& threeColoring, - csat::utils::GateEncoder& encoder + csat::utils::GateEncoder& encoder ) { std::vector> color_parents; std::vector> gates_by_color; @@ -57,7 +57,7 @@ TEST(ThreeColoring, SmallTest) parser.parseStream(stream); std::unique_ptr circuit = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); ThreeColoring threeColoring = ThreeColoring(*circuit); auto [color_parents, gates_by_color] = parse_colors(threeColoring, encoder); @@ -90,7 +90,7 @@ TEST(ThreeColoring, BiggerTest) parser.parseStream(stream); std::unique_ptr circuit = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); ThreeColoring threeColoring = ThreeColoring(*circuit); auto [color_parents, gates_by_color] = parse_colors(threeColoring, encoder); @@ -132,7 +132,7 @@ TEST(ThreeColoring, HardTest) parser.parseStream(stream); std::unique_ptr circuit = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); ThreeColoring threeColoring = ThreeColoring(*circuit); auto [color_parents, gates_by_color] = parse_colors(threeColoring, encoder); diff --git a/tests/src_test/simplification/utils/two_coloring.cpp b/tests/src_test/simplification/utils/two_coloring.cpp index 46d7886..f32343d 100644 --- a/tests/src_test/simplification/utils/two_coloring.cpp +++ b/tests/src_test/simplification/utils/two_coloring.cpp @@ -19,7 +19,7 @@ using namespace csat::utils; std::pair>, std::vector>> parse_colors ( TwoColoring& twoColoring, - csat::utils::GateEncoder& encoder + csat::utils::GateEncoder& encoder ) { std::vector> color_parents; std::vector> gates_by_color; @@ -56,7 +56,7 @@ TEST(TwoColoring, SmallTest) parser.parseStream(stream); std::unique_ptr circuit = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); TwoColoring twoColoring = TwoColoring(*circuit); auto [color_parents, gates_by_color] = parse_colors(twoColoring, encoder); @@ -89,7 +89,7 @@ TEST(TwoColoring, OneBigColor) parser.parseStream(stream); std::unique_ptr circuit = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); TwoColoring twoColoring = TwoColoring(*circuit); auto [color_parents, gates_by_color] = parse_colors(twoColoring, encoder); @@ -119,7 +119,7 @@ TEST(TwoColoring, LongNegationChains) parser.parseStream(stream); std::unique_ptr circuit = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); TwoColoring twoColoring = TwoColoring(*circuit); auto [color_parents, gates_by_color] = parse_colors(twoColoring, encoder); @@ -152,7 +152,7 @@ TEST(TwoColoring, BiggerTest) parser.parseStream(stream); std::unique_ptr circuit = parser.instantiate(); - csat::utils::GateEncoder encoder = parser.getEncoder(); + csat::utils::GateEncoder encoder = parser.getEncoder(); TwoColoring twoColoring = TwoColoring(*circuit); auto [color_parents, gates_by_color] = parse_colors(twoColoring, encoder); diff --git a/tests/src_test/utility/encoder_test.cpp b/tests/src_test/utility/encoder_test.cpp index 38871c2..bf0bccc 100644 --- a/tests/src_test/utility/encoder_test.cpp +++ b/tests/src_test/utility/encoder_test.cpp @@ -17,7 +17,7 @@ TEST(EncoderTest, EncodeDecode) { logger.info("Testing simple encoding/decoding"); - GateEncoder enc; + GateEncoder enc; enc.encodeGate("a"); enc.encodeGate("b"); enc.encodeGate("c"); @@ -40,35 +40,4 @@ TEST(EncoderTest, EncodeDecode) } - -TEST(EncoderTest, Merge) -{ - logger.info("Testing simple encoder merging cases"); - - GateEncoder first; - first.encodeGate("a"); - first.encodeGate("b"); - first.encodeGate("c"); - first.encodeGate("d"); - first.encodeGate("e"); - - GateEncoder second; - second.encodeGate(0); - second.encodeGate(2); - second.encodeGate(3); - - auto merged = mergeGateEncoders(first, second); - - ASSERT_TRUE(merged->size() == 3); - - ASSERT_TRUE(merged->decodeGate(0) == "a"); - ASSERT_TRUE(merged->encodeGate("a") == second.encodeGate(first.encodeGate("a"))); - - ASSERT_TRUE(merged->decodeGate(1) == "c"); - ASSERT_TRUE(merged->encodeGate("c") == second.encodeGate(first.encodeGate("c"))); - - ASSERT_TRUE(merged->decodeGate(2) == "d"); - ASSERT_TRUE(merged->encodeGate("d") == second.encodeGate(first.encodeGate("d"))); -} - } // namespace From 72431f7b363f07e5a2eaaebe0c8989d83c37ad9f Mon Sep 17 00:00:00 2001 From: vikria Date: Tue, 22 Oct 2024 18:53:45 +0300 Subject: [PATCH 06/10] tests + format --- .../duplicate_gates_cleaner.hpp | 94 ++++++++----------- src/simplification/reduce_not_composition.hpp | 3 +- .../redundant_gates_cleaner.hpp | 10 +- .../three_inputs_optimization.hpp | 3 +- .../three_inputs_optimization_bench.hpp | 3 +- src/utility/converters.hpp | 34 ++++--- src/utility/encoder.hpp | 23 +++-- src/utility/write_utils.hpp | 5 +- .../duplicate_gates_cleaner.cpp | 75 +++++++++++++++ 9 files changed, 152 insertions(+), 98 deletions(-) diff --git a/src/simplification/duplicate_gates_cleaner.hpp b/src/simplification/duplicate_gates_cleaner.hpp index 79634ab..684e81b 100644 --- a/src/simplification/duplicate_gates_cleaner.hpp +++ b/src/simplification/duplicate_gates_cleaner.hpp @@ -25,16 +25,11 @@ namespace csat::simplification * * @tparam CircuitT */ -template< - class CircuitT, - typename = std::enable_if_t< - std::is_base_of_v - > -> +template > > class DuplicateGatesCleaner_ : public ITransformer { csat::Logger logger{"DuplicateGatesCleaner"}; - + public: CircuitAndEncoder transform( std::unique_ptr circuit, @@ -42,47 +37,45 @@ class DuplicateGatesCleaner_ : public ITransformer { logger.debug("========================================================================================="); logger.debug("START DuplicateGatesCleaner"); - + GateEncoder new_encoder{}; - + // Topsort, from inputs to outputs. csat::GateIdContainer gateSorting(algo::TopSortAlgorithm::sorting(*circuit)); std::reverse(gateSorting.begin(), gateSorting.end()); - - BoolVector safe_mask(circuit->getNumberOfGates(), true); // 0 -- if gate is a duplicate, 1 -- otherwise + + BoolVector safe_mask(circuit->getNumberOfGates(), true); // 0 -- if gate is a duplicate, 1 -- otherwise // `auxiliary_encoder` helps to deduplicate gates by mapping same auxiliary name to one index. GateEncoder auxiliary_encoder{}; // maps original gate ID to auxiliary ID, gotten from `auxiliary_encoder`. std::unordered_map gate_id_to_auxiliary_id{}; - + logger.debug("Building mask to delete gates and filling map -- gate_id_to_auxiliary_id"); std::string auxiliary_name; - for (GateId gateId: gateSorting) + for (GateId gateId : gateSorting) { logger.debug("Processing gate ", gateId); auxiliary_name.clear(); auxiliary_name = formatGateAuxiliaryName_( - gateId, - circuit->getGateType(gateId), - circuit->getGateOperands(gateId), - gate_id_to_auxiliary_id - ); + gateId, circuit->getGateType(gateId), circuit->getGateOperands(gateId), gate_id_to_auxiliary_id); logger.debug("Auxiliary name for gate ", gateId, " is ", auxiliary_name); - - if (auxiliary_encoder.keyExists(auxiliary_name)) { + + if (auxiliary_encoder.keyExists(auxiliary_name)) + { logger.debug("Gate number ", gateId, " is a Duplicate and will be removed."); safe_mask.at(gateId) = false; } else { - logger.debug("Gate number ", gateId, " is either unique, or first of found duplicated, and will be saved."); + logger.debug( + "Gate number ", gateId, " is either unique, or first of found duplicated, and will be saved."); new_encoder.encodeGate(encoder->decodeGate(gateId)); } - + gate_id_to_auxiliary_id[gateId] = auxiliary_encoder.encodeGate(auxiliary_name); } - + logger.debug("Building new circuit"); GateInfoContainer gate_info(auxiliary_encoder.size()); for (GateId gateId = 0; gateId < circuit->getNumberOfGates(); ++gateId) @@ -90,40 +83,35 @@ class DuplicateGatesCleaner_ : public ITransformer if (safe_mask.at(gateId)) { logger.debug( - "New Gate ", gate_id_to_auxiliary_id.at(gateId), - "; Type: ", utils::gateTypeToString(circuit->getGateType(gateId)), - "; Operands: ", formatOperandsString_(circuit->getGateOperands(gateId), gate_id_to_auxiliary_id).str() - ); - + "New Gate ", + gate_id_to_auxiliary_id.at(gateId), + "; Type: ", + utils::gateTypeToString(circuit->getGateType(gateId)), + "; Operands: ", + formatOperandsString_(circuit->getGateOperands(gateId), gate_id_to_auxiliary_id).str()); + GateIdContainer masked_operands_{}; - for (GateId operand: circuit->getGateOperands(gateId)) + for (GateId operand : circuit->getGateOperands(gateId)) { masked_operands_.push_back(gate_id_to_auxiliary_id.at(operand)); } - gate_info.at(gate_id_to_auxiliary_id.at(gateId)) = { - circuit->getGateType(gateId), - masked_operands_ - }; + gate_info.at(gate_id_to_auxiliary_id.at(gateId)) = {circuit->getGateType(gateId), masked_operands_}; } } - + GateIdContainer new_output_gates{}; new_output_gates.reserve(circuit->getOutputGates().size()); - for (GateId output_gate: circuit->getOutputGates()) + for (GateId output_gate : circuit->getOutputGates()) { new_output_gates.push_back(gate_id_to_auxiliary_id.at(output_gate)); } - + logger.debug("END DuplicateGatesCleaner"); logger.debug("========================================================================================="); - return { - std::make_unique(gate_info, new_output_gates), - std::make_unique(new_encoder) - }; + return {std::make_unique(gate_info, new_output_gates), std::make_unique(new_encoder)}; }; - + private: - /** * Formats new auxiliary name for the gate based on its attributes (type, operands). * Such name may be used to determine literal duplicates in the circuit. @@ -153,7 +141,7 @@ class DuplicateGatesCleaner_ : public ITransformer auxiliary_name << '_' + std::to_string(gateId); return auxiliary_name.str(); } - + // Preparing set of operands, by accounting already found duplicates. GateIdContainer prepared_operands{}; prepared_operands.reserve(operands.size()); @@ -162,7 +150,7 @@ class DuplicateGatesCleaner_ : public ITransformer operands.end(), std::back_inserter(prepared_operands), [&deduplicator](GateId operand) { return deduplicator.at(operand); }); - + // For gates defined by symmetrical function operands are sorted during // circuit construction (see GateInfo), but then some of their operands // may be decided to be duplicates, so we resort them so such gates with @@ -182,27 +170,28 @@ class DuplicateGatesCleaner_ : public ITransformer prepared_operands.erase(last, prepared_operands.end()); } } - + // Adds names of gate's operands to its auxiliary name. - for (GateId operand: prepared_operands) + for (GateId operand : prepared_operands) { auxiliary_name << '_' + std::to_string(operand); } - + return auxiliary_name.str(); }; - + std::stringstream formatOperandsString_( GateIdContainer const& operands, std::unordered_map const& encoder) { std::stringstream ss; - if (operands.empty()) { + if (operands.empty()) + { return ss; } - + ss << encoder.at(operands[0]); - for(auto ptr = operands.begin() + 1; ptr != operands.end(); ++ptr) + for (auto ptr = operands.begin() + 1; ptr != operands.end(); ++ptr) { ss << ',' << encoder.at(*ptr); } @@ -210,5 +199,4 @@ class DuplicateGatesCleaner_ : public ITransformer } }; - -} // namespace csat::simplification \ No newline at end of file +} // namespace csat::simplification \ No newline at end of file diff --git a/src/simplification/reduce_not_composition.hpp b/src/simplification/reduce_not_composition.hpp index 055dbc5..53e24d5 100644 --- a/src/simplification/reduce_not_composition.hpp +++ b/src/simplification/reduce_not_composition.hpp @@ -72,8 +72,7 @@ class ReduceNotComposition_ : public ITransformer logger.debug("========================================================================================="); return { - std::make_unique(gate_info, circuit->getOutputGates()), - std::make_unique(*encoder)}; + std::make_unique(gate_info, circuit->getOutputGates()), std::make_unique(*encoder)}; }; private: diff --git a/src/simplification/redundant_gates_cleaner.hpp b/src/simplification/redundant_gates_cleaner.hpp index 57f442f..a9d6070 100644 --- a/src/simplification/redundant_gates_cleaner.hpp +++ b/src/simplification/redundant_gates_cleaner.hpp @@ -2,9 +2,9 @@ #include #include -#include -#include #include +#include +#include #include "src/algo.hpp" #include "src/common/csat_types.hpp" @@ -86,7 +86,7 @@ class RedundantGatesCleaner_ : public ITransformer encoded_operands_.push_back(new_encoder.encodeGate(operand_name)); } // Build new gate info object for current gate. - gate_info.at(new_encoder.encodeGate(gate_name)) = { + gate_info.at(new_encoder.encodeGate(gate_name)) = { circuit->getGateType(gateId), std::move(encoded_operands_)}; } } @@ -98,8 +98,8 @@ class RedundantGatesCleaner_ : public ITransformer for (GateId output_gate : circuit->getOutputGates()) { assert( - mask_use_output.at(output_gate) != algo::DFSState::UNVISITED - || (preserveInputs && circuit->getGateType(output_gate) == GateType::INPUT)); + mask_use_output.at(output_gate) != algo::DFSState::UNVISITED || + (preserveInputs && circuit->getGateType(output_gate) == GateType::INPUT)); std::string_view output_name = encoder->decodeGate(output_gate); new_output_gates.push_back(new_encoder.encodeGate(output_name)); diff --git a/src/simplification/three_inputs_optimization.hpp b/src/simplification/three_inputs_optimization.hpp index 553edec..8fdee26 100644 --- a/src/simplification/three_inputs_optimization.hpp +++ b/src/simplification/three_inputs_optimization.hpp @@ -743,8 +743,7 @@ class ThreeInputsSubcircuitMinimization : public ITransformer stats.print(); return { - std::make_unique(gate_info, circuit->getOutputGates()), - std::make_unique(*encoder)}; + std::make_unique(gate_info, circuit->getOutputGates()), std::make_unique(*encoder)}; } }; diff --git a/src/simplification/three_inputs_optimization_bench.hpp b/src/simplification/three_inputs_optimization_bench.hpp index 77183de..278ec5e 100644 --- a/src/simplification/three_inputs_optimization_bench.hpp +++ b/src/simplification/three_inputs_optimization_bench.hpp @@ -713,8 +713,7 @@ class ThreeInputsSubcircuitMinimizationBench : public ITransformer stats.print(); return { - std::make_unique(gate_info, circuit->getOutputGates()), - std::make_unique(*encoder)}; + std::make_unique(gate_info, circuit->getOutputGates()), std::make_unique(*encoder)}; } }; diff --git a/src/utility/converters.hpp b/src/utility/converters.hpp index 54efd09..7b9e950 100644 --- a/src/utility/converters.hpp +++ b/src/utility/converters.hpp @@ -201,25 +201,23 @@ inline bool symmetricOperatorQ(GateType gate_type) noexcept * @return True iff two gates of given type that differ only by number of multiple operands * are equivalent (e.g. `AND(X, X, Y) ~ AND(X, Y)`, but `XOR(X, X, Y) !~ XOR(X, Y)`). */ -inline bool reducibleMultipleOperandsQ(GateType gate_type) -noexcept +inline bool reducibleMultipleOperandsQ(GateType gate_type) noexcept { - static const std::unordered_map _type_map - { - {GateType::INPUT, true}, - {GateType::NOT, true}, - {GateType::AND, true}, - {GateType::NAND, true}, - {GateType::OR, true}, - {GateType::NOR, true}, - {GateType::XOR, false}, - {GateType::NXOR, false}, - {GateType::IFF, true}, - {GateType::MUX, false}, - {GateType::BUFF, true}, - {GateType::CONST_FALSE, true}, - {GateType::CONST_TRUE, true} - }; + static std::unordered_map const _type_map{ + {GateType::INPUT, true }, + {GateType::NOT, true }, + {GateType::AND, true }, + {GateType::NAND, true }, + {GateType::OR, true }, + {GateType::NOR, true }, + {GateType::XOR, false}, + {GateType::NXOR, false}, + {GateType::IFF, true }, + {GateType::MUX, false}, + {GateType::BUFF, true }, + {GateType::CONST_FALSE, true }, + {GateType::CONST_TRUE, true } + }; return _type_map.at(gate_type); } diff --git a/src/utility/encoder.hpp b/src/utility/encoder.hpp index 3c15834..2a85b3d 100644 --- a/src/utility/encoder.hpp +++ b/src/utility/encoder.hpp @@ -1,7 +1,7 @@ #pragma once -#include #include +#include #include #include "src/common/csat_types.hpp" @@ -18,19 +18,18 @@ class GateEncoder size_t next_var_ = 0; std::map> encoder_{}; std::map decoder_{}; - + public: - GateEncoder() = default; + GateEncoder() = default; GateEncoder(GateEncoder const&) = default; - ~GateEncoder() = default; - - GateId encodeGate(std::string_view key) - noexcept + ~GateEncoder() = default; + + GateId encodeGate(std::string_view key) noexcept { auto search = encoder_.find(key); if (search == encoder_.end()) { - decoder_[next_var_] = std::string(key); + decoder_[next_var_] = std::string(key); encoder_[std::string(key)] = next_var_; return next_var_++; } @@ -39,25 +38,25 @@ class GateEncoder return search->second; } }; - + [[nodiscard]] std::string const& decodeGate(GateId id) const { return decoder_.at(id); }; - + [[nodiscard]] bool keyExists(std::string_view key) const { return encoder_.find(key) != encoder_.end(); }; - + [[nodiscard]] size_t size() const { return next_var_; } - + void clear() { next_var_ = 0; diff --git a/src/utility/write_utils.hpp b/src/utility/write_utils.hpp index 18daecb..02b8a7d 100644 --- a/src/utility/write_utils.hpp +++ b/src/utility/write_utils.hpp @@ -18,10 +18,7 @@ namespace csat * @tparam CircuitT */ template > > -void WriteBenchFile( - CircuitT const& circuit, - csat::utils::GateEncoder const& encoder, - std::ofstream& file_out) +void WriteBenchFile(CircuitT const& circuit, csat::utils::GateEncoder const& encoder, std::ofstream& file_out) { csat::Logger const logger("WriteBenchFile"); logger.debug("WriteBenchFile start."); diff --git a/tests/src_test/simplification/duplicate_gates_cleaner.cpp b/tests/src_test/simplification/duplicate_gates_cleaner.cpp index c8d668d..9f2dac3 100644 --- a/tests/src_test/simplification/duplicate_gates_cleaner.cpp +++ b/tests/src_test/simplification/duplicate_gates_cleaner.cpp @@ -213,4 +213,79 @@ TEST(DuplicateGatesCleaner, SeveralLevelsMUX) ASSERT_EQ(circuit->getGateOperands(10), GateIdContainer({6, 9})); } + +TEST(DuplicateGatesCleaner, ReducibleDuplicateOfOperands) +{ + std::string const dag = "INPUT(0)\n" + "INPUT(1)\n" + "\n" + "2 = AND(1, 0)\n" + "3 = AND(0, 1)\n" + "4 = AND(0, 2, 3)\n" + "5 = AND(0, 2)\n" + "6 = OR(4, 5)\n" + "\n" + "OUTPUT(6)\n"; + + std::istringstream stream(dag); + csat::parser::BenchToCircuit parser; + parser.parseStream(stream); + + std::unique_ptr csat_instance = parser.instantiate(); + csat::utils::GateEncoder encoder = parser.getEncoder(); + + auto [circuit, _] = Composition< + DAG, + DuplicateGatesCleaner + >().apply(*csat_instance, encoder); + + ASSERT_EQ(circuit->getNumberOfGates(), 5); + ASSERT_EQ(circuit->getGateType(0), GateType::INPUT); + ASSERT_EQ(circuit->getGateType(1), GateType::INPUT); + ASSERT_EQ(circuit->getGateType(2), GateType::AND); + ASSERT_EQ(circuit->getGateOperands(2), GateIdContainer({0, 1})); + ASSERT_EQ(circuit->getGateType(3), GateType::AND); + ASSERT_EQ(circuit->getGateOperands(3), GateIdContainer({0, 2, 2})); + ASSERT_EQ(circuit->getGateType(4), GateType::OR); + ASSERT_EQ(circuit->getGateOperands(4), GateIdContainer({3, 3})); +} + +TEST(DuplicateGatesCleaner, XorNotReducible) +{ + std::string const dag = "INPUT(0)\n" + "INPUT(1)\n" + "\n" + "2 = AND(1, 0)\n" + "3 = AND(0, 1)\n" + "4 = XOR(0, 2, 3)\n" + "5 = XOR(0, 2)\n" + "6 = OR(4, 5)\n" + "\n" + "OUTPUT(6)\n"; + + std::istringstream stream(dag); + csat::parser::BenchToCircuit parser; + parser.parseStream(stream); + + std::unique_ptr csat_instance = parser.instantiate(); + csat::utils::GateEncoder encoder = parser.getEncoder(); + + auto [circuit, _] = Composition< + DAG, + DuplicateGatesCleaner + >().apply(*csat_instance, encoder); + + ASSERT_EQ(circuit->getNumberOfGates(), 6); + ASSERT_EQ(circuit->getGateType(0), GateType::INPUT); + ASSERT_EQ(circuit->getGateType(1), GateType::INPUT); + ASSERT_EQ(circuit->getGateType(2), GateType::AND); + ASSERT_EQ(circuit->getGateOperands(2), GateIdContainer({0, 1})); + ASSERT_EQ(circuit->getGateType(3), GateType::XOR); + ASSERT_EQ(circuit->getGateOperands(3), GateIdContainer({0, 2, 2})); + ASSERT_EQ(circuit->getGateType(4), GateType::XOR); + ASSERT_EQ(circuit->getGateOperands(4), GateIdContainer({0, 2})); + ASSERT_EQ(circuit->getGateType(5), GateType::OR); + ASSERT_EQ(circuit->getGateOperands(5), GateIdContainer({3, 4})); +} + } // namespace From d138884f2dab13fdba4abbac08f7916a3ed74228 Mon Sep 17 00:00:00 2001 From: vikria Date: Wed, 23 Oct 2024 20:15:17 +0300 Subject: [PATCH 07/10] format --- app/simplify.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/app/simplify.cpp b/app/simplify.cpp index 861e580..fb4121e 100644 --- a/app/simplify.cpp +++ b/app/simplify.cpp @@ -19,8 +19,9 @@ /** * prints circuit (encoded name => name from file) */ -void printCircuit(csat::DAG const &circuit, csat::utils::GateEncoder const &encoder) { - for (auto input: circuit.getInputGates()) +void printCircuit(csat::DAG const& circuit, csat::utils::GateEncoder const& encoder) +{ + for (auto input : circuit.getInputGates()) { std::cout << "INPUT(" << input << " => " << encoder.decodeGate(input) << ")\n"; } From d52aa83175d7f1c967dd2087480e3cefe0c782d2 Mon Sep 17 00:00:00 2001 From: vikria Date: Wed, 23 Oct 2024 20:16:09 +0300 Subject: [PATCH 08/10] format --- app/simplify.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/app/simplify.cpp b/app/simplify.cpp index fb4121e..f947b78 100644 --- a/app/simplify.cpp +++ b/app/simplify.cpp @@ -19,7 +19,7 @@ /** * prints circuit (encoded name => name from file) */ -void printCircuit(csat::DAG const& circuit, csat::utils::GateEncoder const& encoder) +void printCircuit(csat::DAG const& circuit, csat::utils::GateEncoder const& encoder) { for (auto input : circuit.getInputGates()) { From 1db4ab872e616ebbd7e185929c5b1e9ec6864df6 Mon Sep 17 00:00:00 2001 From: spefk Date: Thu, 9 Oct 2025 12:33:49 +0300 Subject: [PATCH 09/10] formatting --- app/simplifier.cpp | 2 +- src/simplification/nest.hpp | 2 +- src/utility/write_utils.hpp | 9 +++------ 3 files changed, 5 insertions(+), 8 deletions(-) diff --git a/app/simplifier.cpp b/app/simplifier.cpp index c39f5ec..6c0090f 100644 --- a/app/simplifier.cpp +++ b/app/simplifier.cpp @@ -39,7 +39,7 @@ std::ifstream openFileStream(std::string const& file_path, csat::Logger& logger) /** * Helper to run specific simplification strategies on the circuit in the provided basis. */ -std::tuple, std::unique_ptr > applySimplification( +std::tuple, std::unique_ptr > applySimplification( std::string const& basis, std::unique_ptr& csat_instance, csat::utils::GateEncoder& encoder) diff --git a/src/simplification/nest.hpp b/src/simplification/nest.hpp index 012b066..3d09e61 100644 --- a/src/simplification/nest.hpp +++ b/src/simplification/nest.hpp @@ -48,7 +48,7 @@ struct Nest : public ITransformer std::unique_ptr circuit, std::unique_ptr encoder) { - std::unique_ptr circuit_ = std::move(circuit); + std::unique_ptr circuit_ = std::move(circuit); std::unique_ptr encoder_ = std::move(encoder); for (std::size_t it = 0; it < n; ++it) { diff --git a/src/utility/write_utils.hpp b/src/utility/write_utils.hpp index ad96caa..2246b60 100644 --- a/src/utility/write_utils.hpp +++ b/src/utility/write_utils.hpp @@ -21,10 +21,7 @@ namespace csat * @tparam CircuitT */ template > > -void writeBenchFile( - CircuitT const& circuit, - utils::GateEncoder const& encoder, - std::ofstream& file_out) +void writeBenchFile(CircuitT const& circuit, utils::GateEncoder const& encoder, std::ofstream& file_out) { Logger const logger("writeBenchFile"); logger.debug("writeBenchFile start."); @@ -48,8 +45,8 @@ void writeBenchFile( { if (circuit.getGateType(gateId) != GateType::INPUT) { - file_out << encoder.decodeGate(gateId) << " = " - << utils::gateTypeToString(circuit.getGateType(gateId)) << "("; + file_out << encoder.decodeGate(gateId) << " = " << utils::gateTypeToString(circuit.getGateType(gateId)) + << "("; auto operands = circuit.getGateOperands(gateId); size_t num_operands = operands.size(); From 050c7f31758631d09421ec98911d340526cbc36d Mon Sep 17 00:00:00 2001 From: spefk Date: Thu, 9 Oct 2025 12:46:10 +0300 Subject: [PATCH 10/10] fix --- src/simplification/duplicate_gates_cleaner.hpp | 6 ++++-- src/simplification/redundant_gates_cleaner.hpp | 8 ++++---- src/utility/write_utils.hpp | 2 +- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/simplification/duplicate_gates_cleaner.hpp b/src/simplification/duplicate_gates_cleaner.hpp index 684e81b..1de798d 100644 --- a/src/simplification/duplicate_gates_cleaner.hpp +++ b/src/simplification/duplicate_gates_cleaner.hpp @@ -40,12 +40,14 @@ class DuplicateGatesCleaner_ : public ITransformer GateEncoder new_encoder{}; + logger.debug("Performing top sort"); // Topsort, from inputs to outputs. csat::GateIdContainer gateSorting(algo::TopSortAlgorithm::sorting(*circuit)); std::reverse(gateSorting.begin(), gateSorting.end()); - BoolVector safe_mask(circuit->getNumberOfGates(), true); // 0 -- if gate is a duplicate, 1 -- otherwise - + logger.debug("Building mask to delete gates and filling map -- old_to_new_gateId"); + // 0 -- if gate is a duplicate, 1 -- otherwise + BoolVector safe_mask(circuit->getNumberOfGates(), true); // `auxiliary_encoder` helps to deduplicate gates by mapping same auxiliary name to one index. GateEncoder auxiliary_encoder{}; // maps original gate ID to auxiliary ID, gotten from `auxiliary_encoder`. diff --git a/src/simplification/redundant_gates_cleaner.hpp b/src/simplification/redundant_gates_cleaner.hpp index a9d6070..408adb6 100644 --- a/src/simplification/redundant_gates_cleaner.hpp +++ b/src/simplification/redundant_gates_cleaner.hpp @@ -54,7 +54,7 @@ class RedundantGatesCleaner_ : public ITransformer // be taken to the new circuit (hence discarding all redundant gates). for (GateId gateId = 0; gateId < circuit->getNumberOfGates(); ++gateId) { - std::string_view gate_name = encoder->decodeGate(gateId); + std::string_view const gate_name = encoder->decodeGate(gateId); if (mask_use_output.at(gateId) != algo::DFSState::UNVISITED || (preserveInputs && circuit->getGateType(gateId) == GateType::INPUT)) { @@ -70,7 +70,7 @@ class RedundantGatesCleaner_ : public ITransformer GateInfoContainer gate_info(new_encoder.size()); for (GateId gateId = 0; gateId < circuit->getNumberOfGates(); ++gateId) { - std::string_view gate_name = encoder->decodeGate(gateId); + std::string_view const gate_name = encoder->decodeGate(gateId); // If new encoder doesn't contain name of a gate, this gate is redundant. if (new_encoder.keyExists(gate_name)) { @@ -82,7 +82,7 @@ class RedundantGatesCleaner_ : public ITransformer mask_use_output.at(gateId) != algo::DFSState::UNVISITED || (preserveInputs && circuit->getGateType(gateId) == GateType::INPUT)); - std::string_view operand_name = encoder->decodeGate(operand); + std::string_view const operand_name = encoder->decodeGate(operand); encoded_operands_.push_back(new_encoder.encodeGate(operand_name)); } // Build new gate info object for current gate. @@ -101,7 +101,7 @@ class RedundantGatesCleaner_ : public ITransformer mask_use_output.at(output_gate) != algo::DFSState::UNVISITED || (preserveInputs && circuit->getGateType(output_gate) == GateType::INPUT)); - std::string_view output_name = encoder->decodeGate(output_gate); + std::string_view const output_name = encoder->decodeGate(output_gate); new_output_gates.push_back(new_encoder.encodeGate(output_name)); } diff --git a/src/utility/write_utils.hpp b/src/utility/write_utils.hpp index 2246b60..2ed514a 100644 --- a/src/utility/write_utils.hpp +++ b/src/utility/write_utils.hpp @@ -71,7 +71,7 @@ void writeBenchFile(CircuitT const& circuit, utils::GateEncoder const& encoder, * Prints circuit to stdout where each gate is written in the following notation * " => " */ -void printCircuit(DAG const& circuit, utils::GateEncoder const& encoder) +inline void printCircuit(DAG const& circuit, utils::GateEncoder const& encoder) { for (auto input : circuit.getInputGates()) {