feat core: update duplicate_gates_cleaner (#7)

Co-authored-by: spefk <f.kurmazov.b@gmail.com>

Author: vikria

app/simplifier.cpp

@@ -39,10 +39,10 @@ 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<csat::DAG>, std::unique_ptr<csat::utils::GateEncoder<std::string> > > applySimplification(
+std::tuple<std::unique_ptr<csat::DAG>, std::unique_ptr<csat::utils::GateEncoder> > applySimplification(
     std::string const& basis,
     std::unique_ptr<csat::DAG>& csat_instance,
-    csat::utils::GateEncoder<std::string>& encoder)
+    csat::utils::GateEncoder& encoder)
 {
     if (basis == AIG_BASIS)
     {
@@ -81,7 +81,7 @@ std::tuple<std::unique_ptr<csat::DAG>, std::unique_ptr<csat::utils::GateEncoder<
 void writeResult(
     argparse::ArgumentParser const& program,
     csat::DAG const& simplified_circuit,
-    csat::utils::GateEncoder<std::string> const& encoder,
+    csat::utils::GateEncoder const& encoder,
     std::string const& file_path)
 {
     if (auto output_dir = program.present("-o"))

src/parser/ibench_parser.hpp

@@ -43,13 +43,13 @@ class IBenchParser : public ICircuitParser
     }
 
     /* Encoder of inputs and gates. */
-    csat::utils::GateEncoder<std::string> encoder;
+    csat::utils::GateEncoder encoder;
 
     /**
      * @return Encoder, built according to parser info.
      */
     [[nodiscard]]
-    csat::utils::GateEncoder<std::string> const& getEncoder() const
+    csat::utils::GateEncoder const& getEncoder() const
     {
         return encoder;
     }

src/simplification/composition.hpp

@@ -39,7 +39,7 @@ struct Composition : public ITransformer<CircuitT>
      */
     CircuitAndEncoder<CircuitT, std::string> transform(
         std::unique_ptr<CircuitT> circuit,
-        std::unique_ptr<GateEncoder<std::string>> encoder)
+        std::unique_ptr<GateEncoder> encoder)
     {
         auto _transformer         = TransformerT();
         auto [_circuit, _encoder] = _transformer.transform(std::move(circuit), std::move(encoder));
@@ -61,7 +61,7 @@ struct Composition<CircuitT, TransformerT> : public ITransformer<CircuitT>
   public:
     CircuitAndEncoder<CircuitT, std::string> transform(
         std::unique_ptr<CircuitT> circuit,
-        std::unique_ptr<GateEncoder<std::string>> encoder)
+        std::unique_ptr<GateEncoder> encoder)
     {
         auto _transformer = TransformerT();
         return _transformer.transform(std::move(circuit), std::move(encoder));

src/simplification/constant_gate_reducer.hpp

@@ -53,7 +53,7 @@ class ConstantGateReducer_ : public ITransformer<CircuitT>
      */
     CircuitAndEncoder<CircuitT, std::string> transform(
         std::unique_ptr<CircuitT> circuit,
-        std::unique_ptr<GateEncoder<std::string>> encoder)
+        std::unique_ptr<GateEncoder> encoder)
     {
         logger.debug("START ConstantGateReducer");
 
@@ -232,7 +232,7 @@ class ConstantGateReducer_ : public ITransformer<CircuitT>
 
         return {
             std::make_unique<CircuitT>(std::move(gate_info), std::move(new_output_gates)),
-            std::make_unique<GateEncoder<std::string>>(*encoder)};
+            std::make_unique<GateEncoder>(*encoder)};
     };
 
   private:
@@ -265,7 +265,7 @@ class ConstantGateReducer_ : public ITransformer<CircuitT>
      */
     void createMiniCircuit_(
         GateInfoContainer& gate_info,
-        GateEncoder<std::string>& encoder,
+        GateEncoder& encoder,
         GateIdContainer& new_output_gates,
         std::string const& new_gate_name_prefix,
         GateId& circuit_size,

src/simplification/duplicate_gates_cleaner.hpp

@@ -1,19 +1,15 @@
 #pragma once
 
-#include <algorithm>
-#include <map>
 #include <memory>
-#include <string>
+#include <ranges>
+#include <sstream>
 #include <type_traits>
+#include <unordered_map>
+#include <vector>
 
 #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"
 
 namespace csat::simplification
 {
@@ -23,114 +19,186 @@ 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<class CircuitT, typename = std::enable_if_t<std::is_base_of_v<ICircuit, CircuitT>>>
+template<class CircuitT, typename = std::enable_if_t<std::is_base_of_v<ICircuit, CircuitT> > >
 class DuplicateGatesCleaner_ : public ITransformer<CircuitT>
 {
     csat::Logger logger{"DuplicateGatesCleaner"};
 
   public:
     CircuitAndEncoder<CircuitT, std::string> transform(
         std::unique_ptr<CircuitT> circuit,
-        std::unique_ptr<GateEncoder<std::string>> encoder)
+        std::unique_ptr<GateEncoder> encoder)
     {
         logger.debug("=========================================================================================");
         logger.debug("START DuplicateGatesCleaner");
 
-        logger.debug("Top sort");
+        GateEncoder new_encoder{};
+
+        logger.debug("Performing top sort");
+        // Topsort, from inputs to outputs.
         csat::GateIdContainer gateSorting(algo::TopSortAlgorithm<algo::DFSTopSort>::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(), 1);
-        // maps encoded (`operator_operand1_operand2...`) gate to new gate id
-        GateEncoder<std::string> auxiliary_names_encoder{};
-        // surjection of old gate ids to new gate ids
-        std::map<GateId, GateId> old_to_new_gateId{};
-        // bijection of old gate ids to new gate ids
-        GateEncoder<GateId> new_encoder{};
-        std::string encoded_name;
-
+        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`.
+        std::unordered_map<GateId, GateId> 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_};
             }
         }
 
         GateIdContainer new_output_gates{};
         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<CircuitT>(gate_info, new_output_gates), utils::mergeGateEncoders(*encoder, new_encoder)};
+        return {std::make_unique<CircuitT>(gate_info, new_output_gates), std::make_unique<GateEncoder>(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<GateId, GateId> const& encoder)
+        std::unordered_map<GateId, GateId> const& deduplicator)
     {
-        std::string encoded_name;
-        encoded_name = std::to_string(static_cast<int>(type));
+        std::stringstream auxiliary_name;
+        auxiliary_name << std::to_string(static_cast<uint8_t>(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<GateId, GateId> 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::simplification

src/simplification/duplicate_operands_cleaner.hpp

@@ -56,7 +56,7 @@ class DuplicateOperandsCleaner_ : public ITransformer<CircuitT>
      */
     CircuitAndEncoder<CircuitT, std::string> transform(
         std::unique_ptr<CircuitT> circuit,
-        std::unique_ptr<GateEncoder<std::string>> encoder)
+        std::unique_ptr<GateEncoder> encoder)
     {
         logger.debug("START DuplicateOperandsCleaner");
 
@@ -265,7 +265,7 @@ class DuplicateOperandsCleaner_ : public ITransformer<CircuitT>
 
         return {
             std::make_unique<CircuitT>(std::move(gate_info), std::move(new_output_gates)),
-            std::make_unique<GateEncoder<std::string>>(*encoder)};
+            std::make_unique<GateEncoder>(*encoder)};
     };
 
   private:

src/simplification/nest.hpp

@@ -46,10 +46,10 @@ struct Nest : public ITransformer<CircuitT>
      */
     CircuitAndEncoder<CircuitT, std::string> transform(
         std::unique_ptr<CircuitT> circuit,
-        std::unique_ptr<GateEncoder<std::string>> encoder)
+        std::unique_ptr<GateEncoder> encoder)
     {
-        std::unique_ptr<CircuitT> circuit_                 = std::move(circuit);
-        std::unique_ptr<GateEncoder<std::string>> encoder_ = std::move(encoder);
+        std::unique_ptr<CircuitT> circuit_    = std::move(circuit);
+        std::unique_ptr<GateEncoder> encoder_ = std::move(encoder);
         for (std::size_t it = 0; it < n; ++it)
         {
             auto comp                    = Composition<CircuitT, OtherTransformersT...>();

src/simplification/reduce_not_composition.hpp

@@ -39,7 +39,7 @@ class ReduceNotComposition_ : public ITransformer<CircuitT>
      */
     CircuitAndEncoder<CircuitT, std::string> transform(
         std::unique_ptr<CircuitT> circuit,
-        std::unique_ptr<GateEncoder<std::string>> encoder)
+        std::unique_ptr<GateEncoder> encoder)
     {
         logger.debug("=========================================================================================");
         logger.debug("START ReduceNotComposition");
@@ -72,8 +72,7 @@ class ReduceNotComposition_ : public ITransformer<CircuitT>
         logger.debug("=========================================================================================");
 
         return {
-            std::make_unique<CircuitT>(gate_info, circuit->getOutputGates()),
-            std::make_unique<GateEncoder<std::string>>(*encoder)};
+            std::make_unique<CircuitT>(gate_info, circuit->getOutputGates()), std::make_unique<GateEncoder>(*encoder)};
     };
 
   private: