AIG simplifier using equivalences

Add aig_simplify() function that simplifies an AIG using a given
vector of equivalent node pairs. The function:
- Substitutes equivalent nodes (replacing larger var numbers with smaller)
- Handles equivalences with constants
- Computes transitive closure of equivalences
- Performs constant propagation (a AND false = false, a AND true = a)
- Simplifies trivial cases (a AND a = a, a AND !a = false)

Co-Authored-By: Claude Opus 4.5 <[email protected]>

Author: kroening

src/trans-netlist/Makefile

@@ -1,5 +1,6 @@
 SRC = aig.cpp \
       aig_prop.cpp \
+      aig_simplifier.cpp \
       aig_terminals.cpp \
       bmc_map.cpp \
       build_netlist_var_map.cpp \

src/trans-netlist/aig_simplifier.cpp

@@ -0,0 +1,195 @@
+/*******************************************************************\
+
+Module: AIG Simplifier
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "aig_simplifier.h"
+
+/// Apply a substitution map to a literal
+/// \param l: The literal to substitute
+/// \param substitution: Map from variable numbers to replacement literals
+/// \return The substituted literal
+static literalt
+substitute(literalt l, const std::vector<literalt> &substitution)
+{
+  if(l.is_constant())
+    return l;
+
+  auto var_no = l.var_no();
+  PRECONDITION(var_no < substitution.size());
+
+  // Get the replacement literal and apply the sign
+  return substitution[var_no] ^ l.sign();
+}
+
+/// Simplify an AND node after substitution
+/// \param a: First input literal (after substitution)
+/// \param b: Second input literal (after substitution)
+/// \param dest: The destination AIG to add the node to
+/// \return The literal representing the simplified AND
+static literalt simplify_and(literalt a, literalt b, aigt &dest)
+{
+  // Constant propagation
+  if(a.is_false() || b.is_false())
+    return const_literal(false);
+
+  if(a.is_true())
+    return b;
+
+  if(b.is_true())
+    return a;
+
+  // a AND a = a
+  if(a == b)
+    return a;
+
+  // a AND !a = false
+  if(a == !b)
+    return const_literal(false);
+
+  // Normalize: smaller variable number first
+  if(b.var_no() < a.var_no())
+    std::swap(a, b);
+
+  // Create the AND node
+  return dest.new_and_node(a, b);
+}
+
+aigt aig_simplify(const aigt &src, const equivalencest &equivalences)
+{
+  if(src.empty())
+    return aigt();
+
+  const auto num_nodes = src.number_of_nodes();
+
+  // Build a substitution map: for each variable, what literal should it
+  // be replaced with? Initially, each variable maps to itself.
+  std::vector<literalt> substitution;
+  substitution.reserve(num_nodes);
+
+  for(std::size_t i = 0; i < num_nodes; i++)
+    substitution.emplace_back(i, false);
+
+  // Process equivalences. For each equivalence (l1, l2), we want to
+  // replace references to the larger variable with the smaller one.
+  for(const auto &eq : equivalences)
+  {
+    literalt l1 = eq.first;
+    literalt l2 = eq.second;
+
+    // Skip invalid equivalences
+    if(l1.is_constant() && l2.is_constant())
+      continue;
+
+    // If one is constant, the other should map to that constant
+    if(l1.is_constant())
+    {
+      if(l2.var_no() < num_nodes)
+        substitution[l2.var_no()] = l1 ^ l2.sign();
+      continue;
+    }
+
+    if(l2.is_constant())
+    {
+      if(l1.var_no() < num_nodes)
+        substitution[l1.var_no()] = l2 ^ l1.sign();
+      continue;
+    }
+
+    // Both are non-constant
+    // l1 ≡ l2 means: v1 ^ s1 ≡ v2 ^ s2
+    // We replace the larger variable with the smaller
+    auto v1 = l1.var_no();
+    auto v2 = l2.var_no();
+
+    if(v1 >= num_nodes || v2 >= num_nodes)
+      continue;
+
+    // Compute the sign relationship: if l1 ≡ l2, then
+    // v1 should map to v2 ^ (s1 ^ s2), or vice versa
+    bool signs_differ = l1.sign() != l2.sign();
+
+    if(v1 < v2)
+    {
+      // Replace v2 with v1
+      substitution[v2] = literalt(v1, signs_differ);
+    }
+    else if(v2 < v1)
+    {
+      // Replace v1 with v2
+      substitution[v1] = literalt(v2, signs_differ);
+    }
+    // If v1 == v2, the equivalence is trivial (l1 ≡ l1 or l1 ≡ !l1)
+    // The latter case (l1 ≡ !l1) would be a contradiction, ignore it
+  }
+
+  // Compute transitive closure of substitutions
+  // Repeat until no changes
+  bool changed;
+  do
+  {
+    changed = false;
+    for(std::size_t i = 0; i < num_nodes; i++)
+    {
+      literalt subst = substitution[i];
+      if(subst.is_constant() || subst.var_no() == i)
+        continue;
+
+      // Follow the substitution chain
+      literalt next = substitution[subst.var_no()] ^ subst.sign();
+      if(next != subst)
+      {
+        substitution[i] = next;
+        changed = true;
+      }
+    }
+  } while(changed);
+
+  // Now rebuild the AIG with substitutions applied
+  aigt dest;
+
+  // Map from old node indices to new literals
+  std::vector<literalt> old_to_new(num_nodes);
+
+  for(std::size_t i = 0; i < num_nodes; i++)
+  {
+    const auto &node = src.nodes[i];
+
+    // First, check what this node is substituted with
+    literalt subst = substitution[i];
+
+    if(subst.is_constant())
+    {
+      // This node is equivalent to a constant
+      old_to_new[i] = subst;
+      continue;
+    }
+
+    if(subst.var_no() != i)
+    {
+      // This node is equivalent to another (smaller) node
+      // Use what that node maps to, applying the sign
+      old_to_new[i] = old_to_new[subst.var_no()] ^ subst.sign();
+      continue;
+    }
+
+    // This node is a representative (maps to itself), we need to create it
+    if(node.is_var())
+    {
+      // Variable node
+      old_to_new[i] = dest.new_var_node(node.var_no());
+    }
+    else
+    {
+      // AND node - substitute inputs and simplify
+      literalt new_a = substitute(node.a, old_to_new);
+      literalt new_b = substitute(node.b, old_to_new);
+      old_to_new[i] = simplify_and(new_a, new_b, dest);
+    }
+  }
+
+  return dest;
+}

src/trans-netlist/aig_simplifier.h

@@ -0,0 +1,37 @@
+/*******************************************************************\
+
+Module: AIG Simplifier
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// AIG Simplifier using Equivalences
+
+#ifndef CPROVER_TRANS_NETLIST_AIG_SIMPLIFIER_H
+#define CPROVER_TRANS_NETLIST_AIG_SIMPLIFIER_H
+
+#include "aig.h"
+
+#include <utility>
+#include <vector>
+
+/// A pair of equivalent literals
+using equivalencet = std::pair<literalt, literalt>;
+
+/// A vector of equivalences between literals
+using equivalencest = std::vector<equivalencet>;
+
+/// Simplifies an AIG by substituting equivalent nodes.
+/// Given a set of equivalences, this function creates a new AIG
+/// where equivalent nodes are merged. For each equivalence (l1, l2),
+/// references to the node with the larger variable number are
+/// replaced with references to the node with the smaller variable number.
+/// Constant propagation is performed when an equivalence makes a node constant.
+/// \param src: The source AIG to simplify
+/// \param equivalences: Vector of pairs of equivalent literals
+/// \return The simplified AIG
+aigt aig_simplify(const aigt &src, const equivalencest &equivalences);
+
+#endif // CPROVER_TRANS_NETLIST_AIG_SIMPLIFIER_H

unit/Makefile

@@ -11,6 +11,7 @@ SRC += smvlang/expr2smv.cpp \
        temporal-logic/sva_to_ltl.cpp \
        temporal-logic/nnf.cpp \
        temporal-logic/trivial_sva.cpp \
+       trans-netlist/aig_simplifier.cpp \
        verilog/typename.cpp \
        # Empty last line
 
@@ -25,12 +26,14 @@ CXXFLAGS += -D'LOCAL_IREP_IDS=<hw_cbmc_irep_ids.h>'
 
 OBJ += ../src/smvlang/smvlang$(LIBEXT) \
        ../src/temporal-logic/temporal-logic$(LIBEXT) \
+       ../src/trans-netlist/trans-netlist$(LIBEXT) \
        ../src/verilog/verilog$(LIBEXT)
 
 cprover.dir:
 	$(MAKE) $(MAKEARGS) -C ../src
 
-CPROVER_LIBS = $(CPROVER_DIR)/src/util/util$(LIBEXT) \
+CPROVER_LIBS = $(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \
+               $(CPROVER_DIR)/src/util/util$(LIBEXT) \
                $(CPROVER_DIR)/src/big-int/big-int$(LIBEXT) \
                # Empty last line