XAG optimization based on satisfiability don't cares

docs/algorithms/xag_optimization.rst

@@ -0,0 +1,7 @@
+Various XAG optimization algorithms
+-----------------------------------
+
+**Header:** ``mockturtle/algorithms/xag_optimization.hpp``
+
+.. doxygenfunction:: mockturtle::xag_constant_fanin_optimization
+.. doxygenfunction:: mockturtle::xag_dont_cares_optimization

docs/changelog.rst

@@ -18,8 +18,9 @@ v0.2 (not yet released)
     - Cleanup LUT networks (`cleanup_luts`) `#191 <https://github.com/lsils/mockturtle/pull/191>`_
     - Extract linear subcircuits in XAGs (`extract_linear_circuit` and `merge_linear_circuit`) `#204 <https://github.com/lsils/mockturtle/pull/204>`_
     - Linear resynthesis using Paar algorithm (`linear_resynthesis_paar`) `#211 <https://github.com/lsils/mockturtle/pull/211>`_
-    - AND gate optimization by computing transitive linear fanin `#232 <https://github.com/lsils/mockturtle/pull/232>`_
-    - SAT-based satisfiability don't cares checker (`satisfiability_dont_cares_checker`) `236 <https://github.com/lsils/mockturtle/pull/236>`_
+    - XAG optimization by computing transitive linear fanin `#232 <https://github.com/lsils/mockturtle/pull/232>`_
+    - SAT-based satisfiability don't cares checker (`satisfiability_dont_cares_checker`) `#236 <https://github.com/lsils/mockturtle/pull/236>`_
+    - XAG optimization based on satisfiability don't cares (`xag_dont_cares_optimization`) `#237 <https://github.com/lsils/mockturtle/pull/237>`_
 * Views:
     - Assign names to signals and outputs (`names_view`) `#181 <https://github.com/lsils/mockturtle/pull/181>`_ `#184 <https://github.com/lsils/mockturtle/pull/184>`_
 * I/O:

docs/index.rst

@@ -48,7 +48,7 @@ Welcome to mockturtle's documentation!
    algorithms/extract_linear
    algorithms/linear_resynthesis
    algorithms/gates_to_nodes
-   algorithms/xag_constant_fanin_optimization
+   algorithms/xag_optimization
 
 .. toctree::
    :maxdepth: 2

include/mockturtle/algorithms/xag_constant_fanin_optimization.hpp → include/mockturtle/algorithms/xag_optimization.hpp

@@ -36,6 +36,7 @@
 #include <string>
 
 #include "cleanup.hpp"
+#include "dont_cares.hpp"
 #include "../networks/xag.hpp"
 #include "../utils/node_map.hpp"
 #include "../views/topo_view.hpp"
@@ -182,4 +183,54 @@ xag_network xag_constant_fanin_optimization( xag_network const& xag )
   return detail::xag_constant_fanin_optimization_impl( xag ).run();
 }
 
+/*! \brief Optimizes some AND gates using satisfiability don't cares
+ *
+ * If an AND gate is satisfiability don't care for assignment 00, it can be
+ * replaced by an XNOR gate, therefore reducing the multiplicative complexity.
+ */
+xag_network xag_dont_cares_optimization( xag_network const& xag )
+{
+  node_map<xag_network::signal, xag_network> old_to_new( xag );
+
+  xag_network dest;
+  old_to_new[xag.get_constant( false )] = dest.get_constant( false );
+
+  xag.foreach_pi( [&]( auto const& n ) {
+    old_to_new[n] = dest.create_pi();
+  } );
+
+  satisfiability_dont_cares_checker<xag_network> checker( xag );
+
+  topo_view<xag_network>{xag}.foreach_node( [&]( auto const& n ) {
+    if ( xag.is_constant( n ) || xag.is_pi( n ) ) return;
+
+    std::array<xag_network::signal, 2> fanin;
+    xag.foreach_fanin( n, [&]( auto const& f, auto i ) {
+      fanin[i] = old_to_new[f] ^ xag.is_complemented( f );
+    } );
+
+    if ( xag.is_and( n ) )
+    {
+      if ( checker.is_dont_care( n, {false, false} ) )
+      {
+        old_to_new[n] = dest.create_xnor( fanin[0], fanin[1] );
+      }
+      else
+      {
+        old_to_new[n] = dest.create_and( fanin[0], fanin[1] );
+      }
+    }
+    else /* is XOR */
+    {
+      old_to_new[n] = dest.create_xor( fanin[0], fanin[1] );
+    }
+  } );
+
+  xag.foreach_po( [&]( auto const& f ) {
+    dest.create_po( old_to_new[f] ^ xag.is_complemented( f ) );
+  });
+
+  return dest;
+}
+
 } /* namespace mockturtle */