From 568a31c83ad3aa6cbc12975e9cb8b957c80c5d1d Mon Sep 17 00:00:00 2001
From: Lofty <dan.ravensloft@gmail.com>
Date: Tue, 31 Mar 2026 10:22:17 +0100
Subject: [PATCH] write_xaiger2: fix function argument evaluation order

---
 backends/aiger2/aiger.cc | 47 ++++++++++++++++++++++++++++++----------
 1 file changed, 35 insertions(+), 12 deletions(-)

diff --git a/backends/aiger2/aiger.cc b/backends/aiger2/aiger.cc
index 6f32d05de..78aba4bee 100644
--- a/backends/aiger2/aiger.cc
+++ b/backends/aiger2/aiger.cc
@@ -197,7 +197,9 @@ struct Index {
 
 	Lit OR(Lit a, Lit b)
 	{
-		return NOT(AND(NOT(a), NOT(b)));
+		Lit not_a = NOT(a);
+		Lit not_b = NOT(b);
+		return NOT(AND(not_a, not_b));
 	}
 
 	Lit MUX(Lit a, Lit b, Lit s)
@@ -211,17 +213,24 @@ struct Index {
 				return b;
 		}
 
-		return OR(AND(a, NOT(s)), AND(b, s));
+		Lit not_s = NOT(s);
+		Lit a_active = AND(a, not_s);
+		Lit b_active = AND(b, s);
+		return OR(a_active, b_active);
 	}
 
 	Lit XOR(Lit a, Lit b)
 	{
-		return OR(AND(a, NOT(b)), AND(NOT(a), b));
+		Lit not_a = NOT(a);
+		Lit not_b = NOT(b);
+		Lit a_and_not_b = AND(a, not_b);
+		Lit not_a_and_b = AND(not_a, b);
+		return OR(a_and_not_b, not_a_and_b);
 	}
 
 	Lit XNOR(Lit a, Lit b)
 	{
-		return NOT(OR(AND(a, NOT(b)), AND(NOT(a), b)));
+		return NOT(XOR(a, b));
 	}
 
 	Lit CARRY(Lit a, Lit b, Lit c)
@@ -233,7 +242,10 @@ struct Index {
 				return AND(a, b);
 			}
 		}
-		return OR(AND(a, b), AND(c, OR(a, b)));
+		Lit a_or_b = OR(a, b);
+		Lit a_or_b_and_c = AND(c, a_or_b);
+		Lit a_and_b = AND(a, b);
+		return OR(a_and_b, a_or_b_and_c);
 	}
 
 	Lit REDUCE(std::vector<Lit> lits, bool op_xor=false)
@@ -381,7 +393,7 @@ struct Index {
 				} else if (cell->type.in(ID($xor), ID($_XOR_))) {
 					return XOR(a, b);
 				} else if (cell->type.in(ID($xnor), ID($_XNOR_))) {
-					return NOT(XOR(a, b));
+					return XNOR(a, b);
 				} else if (cell->type.in(ID($_ANDNOT_))) {
 					return AND(a, NOT(b));
 				} else if (cell->type.in(ID($_ORNOT_))) {
@@ -401,7 +413,9 @@ struct Index {
 					if (oport == ID::Y) {
 						return XOR(ab, c);
 					} else /* oport == ID::X */ {
-						return OR(AND(a, b), AND(c, ab));
+						Lit a_and_b = AND(a, b);
+						Lit c_and_ab = AND(c, ab);
+						return OR(a_and_b, c_and_ab);
 					}
 				} else if (cell->type.in(ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_))) {
 					Lit c, d;
@@ -412,10 +426,15 @@ struct Index {
 					else
 						d = cell->type == ID($_AOI3_) ? CTRUE : CFALSE;
 
-					if (/* aoi */ cell->type.in(ID($_AOI3_), ID($_AOI4_)))
-						return NOT(OR(AND(a, b), AND(c, d)));
-					else
-						return NOT(AND(OR(a, b), OR(c, d)));
+					if (/* aoi */ cell->type.in(ID($_AOI3_), ID($_AOI4_))) {
+						Lit a_and_b = AND(a, b);
+						Lit c_and_d = AND(c, d);
+						return NOT(OR(a_and_b, c_and_d));
+					} else {
+						Lit a_or_b = OR(a, b);
+						Lit c_or_d = OR(c, d);
+						return NOT(AND(a_or_b, c_or_d));
+					}
 				} else {
 					log_abort();
 				}
@@ -436,7 +455,11 @@ struct Index {
 				sels.push_back(NOT(s));
 			}
 
-			return OR(AND(REDUCE(sels), a), NOT(REDUCE(bar)));
+			Lit reduce_sels = REDUCE(sels);
+			Lit reduce_sels_and_a = AND(reduce_sels, a);
+			Lit reduce_bar = NOT(REDUCE(bar));
+
+			return OR(reduce_sels_and_a, reduce_bar);
 		} else if (cell->type == ID($bmux)) {
 			SigSpec aport = cell->getPort(ID::A);
 			SigSpec sport = cell->getPort(ID::S);