From e2749d5c90c8d4e977eda1d1aa90b87e17198620 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Mon, 19 Aug 2024 13:40:21 +0200
Subject: [PATCH] glucose2: Allow re-definition of gates

This enables e.g. rewriting the circuit based on discovered
equivalences.

This avoids re-introducing doubly linked lists for the fanout by instead
keeping a vector of variables whose fanout lists contain gate inputs
that were changed to a different literal. The first time propagation
runs with that vector nonempty, it deduplicates that vector and then
traverses the affected lists and moves every changed gate input into the
correct list.
---
 src/sat/glucose2/CGlucoseCore.h | 10 ++++++++
 src/sat/glucose2/Glucose2.cpp   | 45 +++++++++++++++++++++++++++++++++
 src/sat/glucose2/Solver.h       |  1 +
 3 files changed, 56 insertions(+)

diff --git a/src/sat/glucose2/CGlucoseCore.h b/src/sat/glucose2/CGlucoseCore.h
index 22de92d2e..281cab6bc 100644
--- a/src/sat/glucose2/CGlucoseCore.h
+++ b/src/sat/glucose2/CGlucoseCore.h
@@ -246,6 +246,16 @@ inline void Solver::setVarFaninLits( Var v, Lit lit1, Lit lit2 ){
 	int mincap = var(lit1) < var(lit2)? var(lit2): var(lit1);
 	mincap = (v < mincap? mincap: v) + 1;
 
+	if (var2NodeData[ v ].lit0 != toLit(~0)) {
+		flushFanout.push(var(var2NodeData[ v ].lit0));
+		flushFanout.push(var(var2NodeData[ v ].lit1));
+
+		var2NodeData[ v ].lit0 = lit1;
+		var2NodeData[ v ].lit1 = lit2;
+
+		return;
+	}
+
 	var2NodeData[ v ].lit0 = lit1;
 	var2NodeData[ v ].lit1 = lit2;
 
diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp
index 1ba55551f..05836082a 100644
--- a/src/sat/glucose2/Glucose2.cpp
+++ b/src/sat/glucose2/Glucose2.cpp
@@ -1043,6 +1043,49 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
 |________________________________________________________________________________________________@*/
 CRef Solver::propagate()
 {
+
+    if (flushFanout.size() != 0) {
+        sort(flushFanout);
+        int w = 1;
+        for (int r = 1; r < flushFanout.size(); r++) {
+            if (flushFanout[w - 1] != flushFanout[r])
+                flushFanout[w++] = flushFanout[r];
+        }
+        flushFanout.shrink_(flushFanout.size() - w);
+
+        for (int i = 0; i < flushFanout.size(); i++) {
+            Var v = flushFanout[i];
+              var2NodeData[v].sort = 0;
+
+            Lit current = var2Fanout0[v];
+            Lit prev = toLit(~0);
+            while (current != toLit(~0)) {
+                Var found = sign(current) ? var(var2NodeData[var(current)].lit1) : var(var2NodeData[var(current)].lit0);
+
+                if (found == v) {
+                    prev = current;
+                    current = var2FanoutN[toInt(current)];
+                } else {
+                    Lit move = current;
+                    current = var2FanoutN[toInt(current)];
+
+                    if (prev == toLit(~0)) {
+                        var2Fanout0[v] = current;
+                    } else {
+                        var2FanoutN[toInt(prev)] = current;
+                    }
+
+                    var2FanoutN[toInt(move)] = var2Fanout0[found];
+                    var2Fanout0[found] = move;
+                    var2NodeData[found].sort = 0;
+                }
+            }
+
+        }
+
+        flushFanout.shrink_(flushFanout.size());
+    }
+
     CRef    confl     = CRef_Undef;
     int     num_props = 0;
     watches.cleanAll();
@@ -1860,6 +1903,8 @@ void Solver::reset()
     var2NodeData .shrink_(var2NodeData .size());
     var2Fanout0  .shrink_(var2Fanout0  .size());
     var2FanoutN  .shrink_(var2FanoutN  .size());
+
+    flushFanout.shrink_(flushFanout.size());
     //var2FanoutP.clear(false);
     if( CRef_Undef != itpc ){
         itpc = CRef_Undef;       // clause allocator has been cleared, do not worry 
diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h
index e019c2fd3..e9290dd7b 100644
--- a/src/sat/glucose2/Solver.h
+++ b/src/sat/glucose2/Solver.h
@@ -396,6 +396,7 @@ protected:
     //vec<Lit> var2FaninLits; // (~0): undefine
     vec<unsigned> var2TravId;
     vec<Lit> var2Fanout0, var2FanoutN;//, var2FanoutP;
+    vec<Var> flushFanout;
     CRef itpc; // the interpreted clause of a gate 
     void inplace_sort( Var v );