From 01e25ceb4a7c631f9a067ceccfa6599214e46b1d Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Tue, 11 Mar 2025 17:26:30 -0400 Subject: [PATCH 01/15] Start matching OR pattern --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 87 ++++++++++++++++++- .../Minimization/BooleanMinimizer.cs | 2 +- Mba.Simplifier/Minimization/TruthTable.cs | 55 ++++++++++++ Simplifier/Program.cs | 5 +- 4 files changed, 145 insertions(+), 4 deletions(-) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 1c7b49c..c6453f8 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -105,6 +105,8 @@ private unsafe AstIdx SimplifyBoolean() // e.g. e ^ (a&(b&c)) var factored = Factor(terms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); + TrySimplifyORs(factored.Value); + // TODO: Apply the identify a^(~a&b) => a|b var simplified = SimplifyRec(factored.Value); @@ -226,6 +228,81 @@ private ulong Negate(int x) return xored; } + private AstIdx TrySimplifyORs(AstIdx id) + { + var terms = new List(); + + var worklist = new Stack(); + worklist.Push(id); + + while (worklist.Any()) + { + var curr = worklist.Pop(); + if (ctx.GetOpcode(curr) == AstOp.Xor) + { + worklist.Push(ctx.GetOp0(curr)); + worklist.Push(ctx.GetOp1(curr)); + } + + else + { + terms.Add(curr); + } + } + + var getCost = (AstIdx? idx) => idx == null ? uint.MaxValue : ctx.GetCost(idx.Value); + + bool changed = false; + while (changed) + { + terms.Sort((AstIdx? a, AstIdx? b) => getCost(b).CompareTo(getCost(a))); + for (int aIndex = 0; aIndex < terms.Count; aIndex++) + { + for (int bIndex = aIndex + 1; bIndex < terms.Count; bIndex++) + { + var a = terms[aIndex]; + var b = terms[bIndex]; + if (a == null || b == null) + continue; + + AstIdx? simplified = TryMatchOr(a.Value, b.Value); + TryMatchOr(b.Value, a.Value); + } + } + } + + + return id; + } + + private AstIdx? TryMatchOr(AstIdx term1, AstIdx term2) + { + // Given a^whatever, we are looking for a^(~a&b), where b is possibly unknown. + var a = term1; + + var demandedMask = GetDemandedVarsMask(term1) | GetDemandedVarsMask(term2); + var varSet = new List(); + for (int i = 0; i < variables.Count; i++) + { + if ((demandedMask & (1u << i)) != 0) + varSet.Add(variables[i]); + } + + // Compute table for `a`, as well as what we think is a table for `a^(~a&b)`. + TruthTable aTable = GetTruthTable(term1, varSet); + var combinedTable = GetTruthTable(ctx.Xor(term1, term2), varSet); + + // First variable that the combined table contains all of the set bits within the `a` table + // Then a|what == combinedTable + if ((aTable & combinedTable) != aTable) + return null; + + var bTable = combinedTable ^ aTable; + + // We found a match + return ctx + } + private AstIdx SimplifyRec(AstIdx id) { var kind = ctx.GetOpcode(id); @@ -355,15 +432,21 @@ private AstIdx SimplifyViaLookupTable(AstIdx id, uint demandedMask) varSet.Add(variables[i]); } + var table = GetTruthTable(id, varSet); + + return BooleanMinimizer.FromTruthTable(ctx, varSet, table); + } + + private TruthTable GetTruthTable(AstIdx id, IReadOnlyList varSet) + { // Build a result vector for the millionth time.. - var w = ctx.GetWidth(id); var rv = LinearSimplifier.JitResultVector(ctx, 1, 1, varSet, id, false, (ulong)Math.Pow(2, varSet.Count)); var table = new TruthTable(varSet.Count); for (int i = 0; i < rv.Length; i++) table.SetBit(i, rv[i] != 0); - return BooleanMinimizer.FromTruthTable(ctx, varSet, table); + return table; } } } diff --git a/Mba.Simplifier/Minimization/BooleanMinimizer.cs b/Mba.Simplifier/Minimization/BooleanMinimizer.cs index caee826..e84d0c2 100644 --- a/Mba.Simplifier/Minimization/BooleanMinimizer.cs +++ b/Mba.Simplifier/Minimization/BooleanMinimizer.cs @@ -15,7 +15,7 @@ namespace Mba.Simplifier.Minimization { public static class BooleanMinimizer { - private const bool useLegacyMinimizer = false; + private const bool useLegacyMinimizer = true; public static AstIdx GetBitwise(AstCtx ctx, IReadOnlyList variables, TruthTable truthTable, bool negate = false) { diff --git a/Mba.Simplifier/Minimization/TruthTable.cs b/Mba.Simplifier/Minimization/TruthTable.cs index 75ed6a5..5c9d831 100644 --- a/Mba.Simplifier/Minimization/TruthTable.cs +++ b/Mba.Simplifier/Minimization/TruthTable.cs @@ -48,12 +48,24 @@ public void Negate() SetBit(i, GetBit(i) ? false : true); } + public void And(TruthTable other) + { + for (int i = 0; i < arr.Length; i++) + arr[i] &= other.arr[i]; + } + public void Or(TruthTable other) { for (int i = 0; i < arr.Length; i++) arr[i] |= other.arr[i]; } + public void Xor(TruthTable other) + { + for (int i = 0; i < arr.Length; i++) + arr[i] ^= other.arr[i]; + } + public void Clear() { for (int i = 0; i < arr.Length; i++) @@ -71,6 +83,11 @@ public bool IsDisjoint(TruthTable other) return true; } + public bool IsZero() + { + return arr.All(x => x == 0); + } + public TruthTable Clone() { var table = new TruthTable(numVars); @@ -129,5 +146,43 @@ public int[] AsArray() return arr; } + + public static bool operator ==(TruthTable table1, TruthTable table2) + { + return table1.Equals(table2); + } + + public static bool operator !=(TruthTable table1, TruthTable table2) + { + return !table1.Equals(table2); + } + + public static TruthTable operator ~(TruthTable a) + { + var result = a.Clone(); + result.Negate(); + return result; + } + + public static TruthTable operator &(TruthTable a, TruthTable b) + { + var result = a.Clone(); + result.And(b); + return result; + } + + public static TruthTable operator |(TruthTable a, TruthTable b) + { + var result = a.Clone(); + result.Or(b); + return result; + } + + public static TruthTable operator ^(TruthTable a, TruthTable b) + { + var result = a.Clone(); + result.Xor(b); + return result; + } } } diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index e08fc2b..461761e 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -14,7 +14,10 @@ bool useEqsat = false; bool proveEquivalence = false; string inputText = null; - +inputText = "a&(b|c|d|e)"; +inputText = "(a&b&c&d)|e"; +inputText = "a|b|c|d|e|f|g"; +//inputText = "((d&(-1^(((e&(-1^((f&(-1^g))^g)))^(f&(-1^g)))^g)))^(e&(-1^((f&(-1^g))^g))))"; var printHelp = () => { Console.WriteLine("Usage: Simplifier.exe"); From 6860bd1f164f3dd2530babd6fd5ec2e941a5d584 Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Tue, 11 Mar 2025 19:32:40 -0400 Subject: [PATCH 02/15] Add algorithm for recovering minimized parts of bitwise ORs --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 118 ++++++++++++------ .../Minimization/BitwiseOrReconstructor.cs | 110 ++++++++++++++++ .../Minimization/BooleanMinimizer.cs | 3 +- Mba.Simplifier/Minimization/TruthTable.cs | 10 +- Simplifier/Program.cs | 2 + 5 files changed, 198 insertions(+), 45 deletions(-) create mode 100644 Mba.Simplifier/Minimization/BitwiseOrReconstructor.cs diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index c6453f8..2426376 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -1,9 +1,11 @@ -using Mba.Ast; +using Antlr4.Runtime.Tree; +using Mba.Ast; using Mba.Common.MSiMBA; using Mba.Common.Utility; using Mba.Simplifier.Bindings; using Mba.Simplifier.Pipeline; using Mba.Utility; +using Microsoft.Z3; using System; using System.Collections.Generic; using System.Diagnostics; @@ -42,40 +44,7 @@ private unsafe AstIdx SimplifyBoolean() // If the truth table has a positive constant offset, negate the result vector. bool negated = truthTable.GetBit(0); var resultVec = truthTable.AsList().Select(x => negated ? Negate(x) : (uint)x).ToArray(); - var variableCombinations = MultibitSiMBA.GetVariableCombinations(variables.Count); - - // Keep track of which variables are demanded by which combination, - // as well as which result vector idx corresponds to which combination. - var groupSizes = MultibitSiMBA.GetGroupSizes(variables.Count); - List<(ulong trueMask, int resultVecIdx)> combToMaskAndIdx = new(); - for (int i = 0; i < variableCombinations.Length; i++) - { - var comb = variableCombinations[i]; - var myIndex = MultibitSiMBA.GetGroupSizeIndex(groupSizes, comb); - combToMaskAndIdx.Add((comb, (int)myIndex)); - } - - var varCount = variables.Count; - bool onlyOneVar = varCount == 1; - int width = (int)(varCount == 1 ? 1 : 2u << (ushort)(varCount - 1)); - List terms = new(); - fixed (ulong* ptr = &resultVec[0]) - { - for (int i = 0; i < variableCombinations.Length; i++) - { - // Fetch the result vector index for this conjunction. - // If the coefficient is zero, we can skip it. - var comb = variableCombinations[i]; - var (trueMask, index) = combToMaskAndIdx[i]; - var coeff = ptr[index]; - if (coeff == 0) - continue; - - // Subtract the coefficient from the result vector. - MultibitSiMBA.SubtractCoeff(1, ptr, 0, coeff, index, width, varCount, onlyOneVar, trueMask); - terms.Add(i); - } - } + var (terms, variableCombinations) = GetAnfTerms(ctx, variables, resultVec); AstIdx? result = null; foreach (var term in terms) @@ -123,6 +92,46 @@ private unsafe AstIdx SimplifyBoolean() return negated ? ctx.Neg(simplified) : simplified; } + private static unsafe (List terms, ulong[] variableCombinations) GetAnfTerms(AstCtx ctx, IReadOnlyList variables, ulong[] resultVec) + { + var variableCombinations = MultibitSiMBA.GetVariableCombinations(variables.Count); + + // Keep track of which variables are demanded by which combination, + // as well as which result vector idx corresponds to which combination. + var groupSizes = MultibitSiMBA.GetGroupSizes(variables.Count); + List<(ulong trueMask, int resultVecIdx)> combToMaskAndIdx = new(); + for (int i = 0; i < variableCombinations.Length; i++) + { + var comb = variableCombinations[i]; + var myIndex = MultibitSiMBA.GetGroupSizeIndex(groupSizes, comb); + combToMaskAndIdx.Add((comb, (int)myIndex)); + } + + var varCount = variables.Count; + bool onlyOneVar = varCount == 1; + int width = (int)(varCount == 1 ? 1 : 2u << (ushort)(varCount - 1)); + List terms = new(); + fixed (ulong* ptr = &resultVec[0]) + { + for (int i = 0; i < variableCombinations.Length; i++) + { + // Fetch the result vector index for this conjunction. + // If the coefficient is zero, we can skip it. + var comb = variableCombinations[i]; + var (trueMask, index) = combToMaskAndIdx[i]; + var coeff = ptr[index]; + if (coeff == 0) + continue; + + // Subtract the coefficient from the result vector. + MultibitSiMBA.SubtractCoeff(1, ptr, 0, coeff, index, width, varCount, onlyOneVar, trueMask); + terms.Add(i); + } + } + + return (terms, variableCombinations); + } + private ulong Negate(int x) { return (uint)((~x) & 1); @@ -252,7 +261,7 @@ private AstIdx TrySimplifyORs(AstIdx id) var getCost = (AstIdx? idx) => idx == null ? uint.MaxValue : ctx.GetCost(idx.Value); - bool changed = false; + bool changed = true; while (changed) { terms.Sort((AstIdx? a, AstIdx? b) => getCost(b).CompareTo(getCost(a))); @@ -266,7 +275,8 @@ private AstIdx TrySimplifyORs(AstIdx id) continue; AstIdx? simplified = TryMatchOr(a.Value, b.Value); - TryMatchOr(b.Value, a.Value); + simplified = TryMatchOr(b.Value, a.Value); + Console.WriteLine(""); } } } @@ -297,10 +307,40 @@ private AstIdx TrySimplifyORs(AstIdx id) if ((aTable & combinedTable) != aTable) return null; - var bTable = combinedTable ^ aTable; + var bTable = combinedTable | aTable; + + if ((aTable | bTable) != combinedTable) + Debugger.Break(); + + var ORed = aTable | bTable; + if (ORed != combinedTable) + Debugger.Break(); // We found a match - return ctx + bool negated = bTable.GetBit(0); + var resultVec = bTable.AsList().Select(x => negated ? Negate(x) : (uint)x).ToArray(); + var (bTerms, variableCombinations) = GetAnfTerms(ctx, varSet, resultVec); + if (negated) + Debugger.Break(); + + new BitwiseOrReconstructor(ctx, varSet, aTable, bTable).Match(); + + AstIdx? result = null; + foreach (var term in bTerms) + { + var conj = LinearSimplifier.ConjunctionFromVarMask(ctx, varSet, 1, variableCombinations[term], null); + if (result == null) + result = conj; + else + result = ctx.Xor(result.Value, conj); + } + + // Yield a XOR of factored variable conjunctions + // e.g. e ^ (a&(b&c)) + //var factored = Factor(bTerms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); + + return ctx.Or(term1, result.Value); + //return SimplifyRec(ctx.Or(term1, factored.Value)); } private AstIdx SimplifyRec(AstIdx id) diff --git a/Mba.Simplifier/Minimization/BitwiseOrReconstructor.cs b/Mba.Simplifier/Minimization/BitwiseOrReconstructor.cs new file mode 100644 index 0000000..07af4c7 --- /dev/null +++ b/Mba.Simplifier/Minimization/BitwiseOrReconstructor.cs @@ -0,0 +1,110 @@ +using Mba.Simplifier.Bindings; +using Mba.Utility; +using System; +using System.Collections.Generic; +using System.Diagnostics; +using System.Linq; +using System.Text; +using System.Threading.Tasks; + +namespace Mba.Simplifier.Minimization +{ + /// + /// Given a truth table for `a` and a truth table for `a|b`, this class recovers a truth table for `b`. + /// Note that `a` and `b` are both arbitrary boolean truth tables, making this nontrivial. + /// We implemented an algorithm to compare the truth tables, eliminating undemanded variables from all positive DNF terms in `a|b` + /// until we find a minimal result. + /// + public class BitwiseOrReconstructor + { + private readonly AstCtx ctx; + + private readonly IReadOnlyList variables; + + private readonly TruthTable aTable; + + private readonly ushort[] aDemandedVars; + + private readonly TruthTable oredTable; + + private readonly ushort[] oredDemandedVars; + + public BitwiseOrReconstructor(AstCtx ctx, IReadOnlyList variables, TruthTable aTable, TruthTable oredTable) + { + this.ctx = ctx; + this.variables = variables; + this.aTable = aTable.Clone(); + this.aDemandedVars = new ushort[this.aTable.NumBits]; + this.oredTable = oredTable.Clone(); + this.oredDemandedVars = new ushort[this.oredTable.NumBits]; + } + + public AstIdx Match() + { + // Take the combined tables and eliminate all positive rows that overlap with `a` + oredTable.Xor(aTable); + + // Enumerate through all truth table rows and make all variables demanded + SetDemandedVars(aTable, aDemandedVars); + SetDemandedVars(oredTable, oredDemandedVars); + + for (int i = 0; i < oredTable.NumBits; i++) + { + // Skip zeroed out rows + if (!oredTable.GetBit(i)) + continue; + + for(ushort varIdx = 0; varIdx < oredTable.NumVars; varIdx++) + { + var vMask = 1 << varIdx; + bool set = (i & vMask) != 0; + var otherIdx = set ? i & ~vMask : i | vMask; + // If changing the value of this variable would result in a different outcome, we cannot eliminate it. + if (!aTable.GetBit(otherIdx)) + continue; + + // Otherwise we can eliminate this variable. + oredDemandedVars[i] &= (ushort)~vMask; + } + } + + // Then finally convert the truth table to DNF. + var terms = new List(); + for (int i = 0; i < oredTable.NumBits; i++) + { + var bitwise = new List(); + if (!oredTable.GetBit(i)) + continue; + if (oredDemandedVars[i] == 0) + continue; + + for (ushort varIdx = 0; varIdx < oredTable.NumVars; varIdx++) + { + var vMask = 1 << varIdx; + // Skip undemanded variables. + if ((oredDemandedVars[i] & vMask) == 0) + continue; + + var negated = (i & vMask) == 0; + bitwise.Add(negated ? ctx.Neg(variables[varIdx]) : variables[varIdx]); + } + + terms.Add(ctx.And(bitwise)); + + } + + var expr = ctx.Or(terms); + return expr; + } + + private static void SetDemandedVars(TruthTable table, ushort[] demandedVars) + { + var mask = (ushort)ModuloReducer.GetMask((uint)table.NumVars); + for(int i = 0; i < table.NumBits; i++) + { + if (table.GetBit(i)) + demandedVars[i] = mask; + } + } + } +} diff --git a/Mba.Simplifier/Minimization/BooleanMinimizer.cs b/Mba.Simplifier/Minimization/BooleanMinimizer.cs index e84d0c2..2b38cf9 100644 --- a/Mba.Simplifier/Minimization/BooleanMinimizer.cs +++ b/Mba.Simplifier/Minimization/BooleanMinimizer.cs @@ -37,7 +37,8 @@ public static AstIdx GetBitwise(AstCtx ctx, IReadOnlyList variables, Tru // If there are four or less variables, we can pull the optimal representation from the truth table. // TODO: One could possibly construct a 5 variable truth table for all 5 variable NPN classes. - if (variables.Count <= 4) + //if (variables.Count <= 4) + if (false) { return FromTruthTable(ctx, variables, truthTable); } diff --git a/Mba.Simplifier/Minimization/TruthTable.cs b/Mba.Simplifier/Minimization/TruthTable.cs index 5c9d831..83faf6b 100644 --- a/Mba.Simplifier/Minimization/TruthTable.cs +++ b/Mba.Simplifier/Minimization/TruthTable.cs @@ -12,15 +12,15 @@ namespace Mba.Simplifier.Minimization { public struct TruthTable { - private readonly int numVars; + public int NumVars { get; } - public int NumBits => 1 << (ushort)numVars; + public int NumBits => 1 << (ushort)NumVars; public readonly ulong[] arr; public TruthTable(int numVars) { - this.numVars = numVars; + this.NumVars = numVars; int width = NumBits <= 64 ? 1 : (NumBits >> 6); arr = new ulong[width]; } @@ -90,7 +90,7 @@ public bool IsZero() public TruthTable Clone() { - var table = new TruthTable(numVars); + var table = new TruthTable(NumVars); for(int i = 0; i < arr.Length ; i++) table.arr[i] = arr[i]; return table; @@ -108,7 +108,7 @@ public override bool Equals([NotNullWhen(true)] object? obj) { if(obj is not TruthTable table) return false; - if (numVars != table.numVars) + if (NumVars != table.NumVars) return false; for(int i = 0; i < arr.Length; i++) diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index 461761e..3daf714 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -17,6 +17,8 @@ inputText = "a&(b|c|d|e)"; inputText = "(a&b&c&d)|e"; inputText = "a|b|c|d|e|f|g"; +inputText = "a|b"; +inputText = "a|b|c"; //inputText = "((d&(-1^(((e&(-1^((f&(-1^g))^g)))^(f&(-1^g)))^g)))^(e&(-1^((f&(-1^g))^g))))"; var printHelp = () => { From 57e46c69c3d691e340e5e4d4e14d34ca861a05d9 Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Tue, 11 Mar 2025 20:21:35 -0400 Subject: [PATCH 03/15] Properly implement generic recovery of bitwise ORs --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 72 +++++++++++++++------ Simplifier/Program.cs | 6 ++ 2 files changed, 60 insertions(+), 18 deletions(-) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 2426376..c878893 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -72,9 +72,9 @@ private unsafe AstIdx SimplifyBoolean() // Yield a XOR of factored variable conjunctions // e.g. e ^ (a&(b&c)) - var factored = Factor(terms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); + var factored = Factor(ctx, variables, terms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); - TrySimplifyORs(factored.Value); + factored = TrySimplifyORs(factored.Value); // TODO: Apply the identify a^(~a&b) => a|b var simplified = SimplifyRec(factored.Value); @@ -89,7 +89,7 @@ private unsafe AstIdx SimplifyBoolean() } */ - return negated ? ctx.Neg(simplified) : simplified; + return negated ? ctx.Neg(simplified) : simplified; } private static unsafe (List terms, ulong[] variableCombinations) GetAnfTerms(AstCtx ctx, IReadOnlyList variables, ulong[] resultVec) @@ -138,7 +138,7 @@ private ulong Negate(int x) } // Apply greedy factoring over a sum of variable conjunctions - private AstIdx? Factor(List conjs, Dictionary demandedVarsMap) + private static AstIdx? Factor(AstCtx ctx, IReadOnlyList variables, List conjs, Dictionary demandedVarsMap) { var getConjFromMask = (uint mask) => LinearSimplifier.ConjunctionFromVarMask(ctx, variables, 1, mask, null); @@ -204,34 +204,34 @@ private ulong Negate(int x) output.Add(conj); mask |= 1u << varIdx; - demandedVarsMap.TryAdd(conj, mask); + //demandedVarsMap.TryAdd(conj, mask); continue; } // Otherwise recursively factor - var other = Factor(elems, demandedVarsMap); + var other = Factor(ctx, variables, elems, demandedVarsMap); var and = ctx.And(result, other.Value); output.Add(and); // Update the demanded mask. - var demanded = (1u << varIdx) | demandedVarsMap[other.Value]; - demandedVarsMap.TryAdd(and, demanded); + //var demanded = (1u << varIdx) | demandedVarsMap[other.Value]; + //demandedVarsMap.TryAdd(and, demanded); } // Compute the union of all demanded variables. var demandedSum = 0u; - foreach (var id in output) - demandedSum |= demandedVarsMap[id]; + //foreach (var id in output) + // demandedSum |= demandedVarsMap[id]; // Compute the XOR of all the terms. var xored = ctx.Xor(output); - demandedVarsMap.TryAdd(xored, demandedSum); + //demandedVarsMap.TryAdd(xored, demandedSum); // If we have a constant offset of one, add it back. if (has) { xored = ctx.Xor(ctx.Constant(ulong.MaxValue, ctx.GetWidth(variables[0])), xored); - demandedVarsMap.TryAdd(xored, demandedSum); + //demandedVarsMap.TryAdd(xored, demandedSum); } return xored; @@ -264,7 +264,8 @@ private AstIdx TrySimplifyORs(AstIdx id) bool changed = true; while (changed) { - terms.Sort((AstIdx? a, AstIdx? b) => getCost(b).CompareTo(getCost(a))); + changed = false; + terms.Sort((AstIdx? a, AstIdx? b) => getCost(a).CompareTo(getCost(b))); for (int aIndex = 0; aIndex < terms.Count; aIndex++) { for (int bIndex = aIndex + 1; bIndex < terms.Count; bIndex++) @@ -275,14 +276,31 @@ private AstIdx TrySimplifyORs(AstIdx id) continue; AstIdx? simplified = TryMatchOr(a.Value, b.Value); + if (simplified != null) + { + changed = true; + terms[aIndex] = simplified; + terms[bIndex] = null; + continue; + } simplified = TryMatchOr(b.Value, a.Value); - Console.WriteLine(""); + if (simplified != null) + { + changed = true; + terms[aIndex] = simplified; + terms[bIndex] = null; + continue; + } } } } - return id; + var bar = ctx.Xor(terms.Where(x => x != null).Select(x => x.Value)); + + Console.WriteLine($"\n\n\n{ctx.GetAstString(bar)}"); + + return bar; } private AstIdx? TryMatchOr(AstIdx term1, AstIdx term2) @@ -316,6 +334,8 @@ private AstIdx TrySimplifyORs(AstIdx id) if (ORed != combinedTable) Debugger.Break(); + bTable = GetTruthTable(new BitwiseOrReconstructor(ctx, varSet, aTable, bTable).Match(), varSet); + // We found a match bool negated = bTable.GetBit(0); var resultVec = bTable.AsList().Select(x => negated ? Negate(x) : (uint)x).ToArray(); @@ -323,8 +343,8 @@ private AstIdx TrySimplifyORs(AstIdx id) if (negated) Debugger.Break(); - new BitwiseOrReconstructor(ctx, varSet, aTable, bTable).Match(); + AstIdx? result = null; foreach (var term in bTerms) { @@ -334,12 +354,15 @@ private AstIdx TrySimplifyORs(AstIdx id) else result = ctx.Xor(result.Value, conj); } + + + //var result = Factor(bTerms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); // Yield a XOR of factored variable conjunctions // e.g. e ^ (a&(b&c)) - //var factored = Factor(bTerms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); + var factored = Factor(ctx, varSet, bTerms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); - return ctx.Or(term1, result.Value); + return ctx.Or(term1, factored.Value); //return SimplifyRec(ctx.Or(term1, factored.Value)); } @@ -457,6 +480,7 @@ private uint GetDemandedVarsMask(AstIdx id) AstOp.Neg => op0(), AstOp.Constant => 0, AstOp.Symbol => 1u << variables.IndexOf(id), // N is generally so small (<= 8) that this is fine. + _ => throw new InvalidOperationException("Unrecognized opcode") }; demandedVarsMap.TryAdd(id, mask); @@ -479,7 +503,19 @@ private AstIdx SimplifyViaLookupTable(AstIdx id, uint demandedMask) private TruthTable GetTruthTable(AstIdx id, IReadOnlyList varSet) { + /* // Build a result vector for the millionth time.. + var cVars = ctx.CollectVariables(id); + var collected = String.Join(", ", cVars.Select(x => ctx.GetAstString(x))); + var given = String.Join(", ", varSet.Select(x => ctx.GetAstString(x))); + + Console.WriteLine($"collected vars: {collected} --- given: {given}, for string {ctx.GetAstString(id)}"); + + + if (cVars.Any(x => !varSet.ToList().Contains(x))) + Debugger.Break(); + */ + var rv = LinearSimplifier.JitResultVector(ctx, 1, 1, varSet, id, false, (ulong)Math.Pow(2, varSet.Count)); var table = new TruthTable(varSet.Count); diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index 3daf714..9c42f1d 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -20,6 +20,12 @@ inputText = "a|b"; inputText = "a|b|c"; //inputText = "((d&(-1^(((e&(-1^((f&(-1^g))^g)))^(f&(-1^g)))^g)))^(e&(-1^((f&(-1^g))^g))))"; +inputText = "(a|b|c|d|e|f|g)^(a&b&c)"; + +inputText = "d & a & e ^ (b ^ a ^ c ^ -1) & d ^ e & a ^ e & b ^ e & c ^ (b ^ a) & d & (l & i) ^ d & e & (c ^ b) ^ c & f & g ^ h ^ g & f & (d & c & e) ^ g & f & (b & d & e) ^ g & f & (d & a & e) ^ g & f & (d & a) ^ g & f & (b & d) ^ g & f & (d & c) ^ g & f & (e & a) ^ g & f & (e & b) ^ g & f & (e & c) ^ g & f & a ^ g & f & b ^ d & a & e & h ^ b & d & e & h ^ d & c & e & h ^ c & f & g & h ^ d & a & h ^ b & d & h ^ d & c & h ^ e & a & h ^ d & h ^ i ^ b & d & h & i ^ i & (g & f & (b & d & e)) ^ g & f & (e & c) & h ^ e & h & (c ^ b) ^ h & (g & f & (b & d)) ^ g & f & (d & c) & h ^ g & f & (d & c & e) & i ^ g & f & (d & a) & i ^ i & (g & f & (b & d)) ^ g & f & (e & b) & i ^ g & f & (e & c) & i ^ d & a & e & h & i ^ b & d & e & h & i ^ d & c & e & h & i ^ d & a & e & i ^ b & d & e & i ^ d & a & h & i ^ d & a & i ^ b & d & i ^ d & c & i ^ e & a & i ^ e & b & i ^ d & i ^ i & h ^ (g & f & (e & a) ^ g & f & (e & b)) & h ^ i & h & (e & c) ^ g & f & (d & a & e) & h & l ^ i & h & (g & f & (b & d & e)) ^ g & f & (d & a & e) & h & i ^ (g & f & (d & a & e) ^ g & f & (b & d & e)) & h ^ (g & f & (d & c & e) ^ g & f & (d & a)) & h ^ (g & f & a ^ g & f & b) & h ^ g & f & (d & a) & h & i ^ i & h & (g & f & (b & d)) ^ g & f & (d & c) & h & i ^ g & f & (e & a) & (i & h) ^ g & f & (e & b) & (i & h) ^ i & h & (g & f & (e & c)) ^ l & (g & f & (b & d & e)) ^ g & f & (d & c & e) & l ^ g & f & (d & a) & h & l ^ g & f & (d & c) & h & l ^ g & f & (d & a) & i & l ^ g & f & (e & c) & i & l ^ d & a & e & h & i & l ^ b & d & e & h & i & l ^ d & c & e & h & i & l ^ g & f & (d & a) & l ^ l & (g & f & (b & d)) ^ g & f & (d & c) & l ^ g & f & (e & a) & l ^ g & f & (e & b) & l ^ g & f & (e & c) & l ^ d & a & e & h & l ^ b & d & e & h & l ^ d & c & e & h & l ^ g & f & a & h & l ^ d & a & e & i & l ^ b & d & e & i & l ^ b & d & h & i & l ^ b & d & e & l ^ d & c & e & l ^ (g & f & a ^ g & f & b) & l ^ (c & f & g ^ d & a & h) & l ^ b & d & h & l ^ d & c & h & l ^ e & a & h & l ^ l & (e & h & (c ^ b)) ^ e & a & i & l ^ (b & d ^ (e & a ^ d & c)) & l ^ e & b & l ^ e & c & l ^ d & h & l ^ d & i & l ^ i & h & l ^ d & l ^ (i ^ h) & l ^ (b ^ a) & e & (i & h) ^ l & i & (g & f & (e & a) & h) ^ ((b ^ a ^ c) & e & (g & f) & (d & h & i) ^ -1) & l ^ l & i & (g & f & (b & d) ^ g & f & (d & c)) ^ l & h & (g & f & (e & c)) ^ d & (i & h & c) ^ g & f & (i & h & c) ^ d & c & h & (l & i) ^ (e & b & i ^ d & a) & l ^ (d & h ^ e & c ^ (g & f & b ^ c & f & g)) & i ^ (g & f & (d & c & e) & i ^ g & f & (d & a & e)) & l ^ l & i & (d & c & e) ^ l & i & (g & f & a) ^ l & i & (g & f & b) ^ l & i & (e & c) ^ l & i & (d & h) ^ l & h & (g & f & (b & d & e)) ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e)) & i ^ (g & f & a ^ g & f & b) & h & i ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e) & i) & l ^ l & i & (g & f & (b & d & e)) ^ g & f & (d & a) & h & i & l ^ l & i & (h & (g & f & (b & d))) ^ g & f & (d & c) & h & i & l ^ (g & f & (e & b) ^ g & f & (e & c)) & h & (l & i) ^ l & h & (g & f & (b & d)) ^ l & h & (g & f & (e & a) ^ g & f & (e & b)) ^ l & i & (g & f & (e & a) ^ g & f & (e & b) ^ g & f & a & h) ^ (g & f & b ^ c & f & g) & h & l ^ l & i & (c & f & g ^ d & a & h) ^ l & i & ((g & f & b ^ c & f & g) & h) ^ (b ^ a) & e & (i & h) & l ^ d & (l & i & c) ^ (g & f & (e & a) ^ d & c & e ^ g & f & (d & c) ^ g & f & a) & i ^ (i & h & (e & c) ^ d & a & e) & l"; +inputText = "(((~((((((y&x)^(t&x))^(t&y))^x)^y)^t))|(~((((((z&y)^(t&x))^(t&y))^y)^z)^t)))|((~t)&(~z)))"; +inputText = "(((t&(((z&y)^x)^z))|((((((y&x)^(z&y))^(t&x))^(t&y))^(t&z))^y))|(((((((z&x)^(z&y))^(t&x))^(t&y))^(t&z))^x)^y))"; +//inputText = "a|b|c"; var printHelp = () => { Console.WriteLine("Usage: Simplifier.exe"); From e89a8df859fbb6c31ca129d58c483319be0863de Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Tue, 11 Mar 2025 20:52:51 -0400 Subject: [PATCH 04/15] Recursively apply bitwise OR recovery --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 57 +++++++++++++++------ Simplifier/Program.cs | 17 +++++- 2 files changed, 56 insertions(+), 18 deletions(-) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index c878893..95590f6 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -74,7 +74,8 @@ private unsafe AstIdx SimplifyBoolean() // e.g. e ^ (a&(b&c)) var factored = Factor(ctx, variables, terms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); - factored = TrySimplifyORs(factored.Value); + factored = SimplifyORsRec(factored.Value); + //factored = TrySimplifyORs(factored.Value); // TODO: Apply the identify a^(~a&b) => a|b var simplified = SimplifyRec(factored.Value); @@ -237,28 +238,50 @@ private ulong Negate(int x) return xored; } - private AstIdx TrySimplifyORs(AstIdx id) + private AstIdx SimplifyORsRec(AstIdx id) { - var terms = new List(); + var op0 = () => SimplifyORsRec(ctx.GetOp0(id)); + var op1 = () => SimplifyORsRec(ctx.GetOp1(id)); - var worklist = new Stack(); - worklist.Push(id); - - while (worklist.Any()) + var getTerms = (AstIdx id) => { - var curr = worklist.Pop(); - if (ctx.GetOpcode(curr) == AstOp.Xor) - { - worklist.Push(ctx.GetOp0(curr)); - worklist.Push(ctx.GetOp1(curr)); - } + var terms = new List(); - else + var worklist = new Stack(); + worklist.Push(id); + + while (worklist.Any()) { - terms.Add(curr); + var curr = worklist.Pop(); + if (ctx.GetOpcode(curr) == AstOp.Xor) + { + worklist.Push(ctx.GetOp0(curr)); + worklist.Push(ctx.GetOp1(curr)); + } + + else + { + terms.Add(curr); + } } - } + return terms; + }; + + var opcode = ctx.GetOpcode(id); + return opcode switch + { + AstOp.And or AstOp.Or => ctx.Binop(opcode, op0(), op1()), + AstOp.Xor => TrySimplifyORs(getTerms(id).Select(x => (AstIdx?)SimplifyORsRec(x.Value)).ToList()), + AstOp.Neg => ctx.Neg(op0()), + AstOp.Constant => id, + AstOp.Symbol => id, + }; + } + + private AstIdx TrySimplifyORs(List terms) + { + var getCost = (AstIdx? idx) => idx == null ? uint.MaxValue : ctx.GetCost(idx.Value); bool changed = true; @@ -298,7 +321,7 @@ private AstIdx TrySimplifyORs(AstIdx id) var bar = ctx.Xor(terms.Where(x => x != null).Select(x => x.Value)); - Console.WriteLine($"\n\n\n{ctx.GetAstString(bar)}"); + //Console.WriteLine($"\n\n\n{ctx.GetAstString(bar)}"); return bar; } diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index 9c42f1d..c1934ba 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -25,7 +25,22 @@ inputText = "d & a & e ^ (b ^ a ^ c ^ -1) & d ^ e & a ^ e & b ^ e & c ^ (b ^ a) & d & (l & i) ^ d & e & (c ^ b) ^ c & f & g ^ h ^ g & f & (d & c & e) ^ g & f & (b & d & e) ^ g & f & (d & a & e) ^ g & f & (d & a) ^ g & f & (b & d) ^ g & f & (d & c) ^ g & f & (e & a) ^ g & f & (e & b) ^ g & f & (e & c) ^ g & f & a ^ g & f & b ^ d & a & e & h ^ b & d & e & h ^ d & c & e & h ^ c & f & g & h ^ d & a & h ^ b & d & h ^ d & c & h ^ e & a & h ^ d & h ^ i ^ b & d & h & i ^ i & (g & f & (b & d & e)) ^ g & f & (e & c) & h ^ e & h & (c ^ b) ^ h & (g & f & (b & d)) ^ g & f & (d & c) & h ^ g & f & (d & c & e) & i ^ g & f & (d & a) & i ^ i & (g & f & (b & d)) ^ g & f & (e & b) & i ^ g & f & (e & c) & i ^ d & a & e & h & i ^ b & d & e & h & i ^ d & c & e & h & i ^ d & a & e & i ^ b & d & e & i ^ d & a & h & i ^ d & a & i ^ b & d & i ^ d & c & i ^ e & a & i ^ e & b & i ^ d & i ^ i & h ^ (g & f & (e & a) ^ g & f & (e & b)) & h ^ i & h & (e & c) ^ g & f & (d & a & e) & h & l ^ i & h & (g & f & (b & d & e)) ^ g & f & (d & a & e) & h & i ^ (g & f & (d & a & e) ^ g & f & (b & d & e)) & h ^ (g & f & (d & c & e) ^ g & f & (d & a)) & h ^ (g & f & a ^ g & f & b) & h ^ g & f & (d & a) & h & i ^ i & h & (g & f & (b & d)) ^ g & f & (d & c) & h & i ^ g & f & (e & a) & (i & h) ^ g & f & (e & b) & (i & h) ^ i & h & (g & f & (e & c)) ^ l & (g & f & (b & d & e)) ^ g & f & (d & c & e) & l ^ g & f & (d & a) & h & l ^ g & f & (d & c) & h & l ^ g & f & (d & a) & i & l ^ g & f & (e & c) & i & l ^ d & a & e & h & i & l ^ b & d & e & h & i & l ^ d & c & e & h & i & l ^ g & f & (d & a) & l ^ l & (g & f & (b & d)) ^ g & f & (d & c) & l ^ g & f & (e & a) & l ^ g & f & (e & b) & l ^ g & f & (e & c) & l ^ d & a & e & h & l ^ b & d & e & h & l ^ d & c & e & h & l ^ g & f & a & h & l ^ d & a & e & i & l ^ b & d & e & i & l ^ b & d & h & i & l ^ b & d & e & l ^ d & c & e & l ^ (g & f & a ^ g & f & b) & l ^ (c & f & g ^ d & a & h) & l ^ b & d & h & l ^ d & c & h & l ^ e & a & h & l ^ l & (e & h & (c ^ b)) ^ e & a & i & l ^ (b & d ^ (e & a ^ d & c)) & l ^ e & b & l ^ e & c & l ^ d & h & l ^ d & i & l ^ i & h & l ^ d & l ^ (i ^ h) & l ^ (b ^ a) & e & (i & h) ^ l & i & (g & f & (e & a) & h) ^ ((b ^ a ^ c) & e & (g & f) & (d & h & i) ^ -1) & l ^ l & i & (g & f & (b & d) ^ g & f & (d & c)) ^ l & h & (g & f & (e & c)) ^ d & (i & h & c) ^ g & f & (i & h & c) ^ d & c & h & (l & i) ^ (e & b & i ^ d & a) & l ^ (d & h ^ e & c ^ (g & f & b ^ c & f & g)) & i ^ (g & f & (d & c & e) & i ^ g & f & (d & a & e)) & l ^ l & i & (d & c & e) ^ l & i & (g & f & a) ^ l & i & (g & f & b) ^ l & i & (e & c) ^ l & i & (d & h) ^ l & h & (g & f & (b & d & e)) ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e)) & i ^ (g & f & a ^ g & f & b) & h & i ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e) & i) & l ^ l & i & (g & f & (b & d & e)) ^ g & f & (d & a) & h & i & l ^ l & i & (h & (g & f & (b & d))) ^ g & f & (d & c) & h & i & l ^ (g & f & (e & b) ^ g & f & (e & c)) & h & (l & i) ^ l & h & (g & f & (b & d)) ^ l & h & (g & f & (e & a) ^ g & f & (e & b)) ^ l & i & (g & f & (e & a) ^ g & f & (e & b) ^ g & f & a & h) ^ (g & f & b ^ c & f & g) & h & l ^ l & i & (c & f & g ^ d & a & h) ^ l & i & ((g & f & b ^ c & f & g) & h) ^ (b ^ a) & e & (i & h) & l ^ d & (l & i & c) ^ (g & f & (e & a) ^ d & c & e ^ g & f & (d & c) ^ g & f & a) & i ^ (i & h & (e & c) ^ d & a & e) & l"; inputText = "(((~((((((y&x)^(t&x))^(t&y))^x)^y)^t))|(~((((((z&y)^(t&x))^(t&y))^y)^z)^t)))|((~t)&(~z)))"; inputText = "(((t&(((z&y)^x)^z))|((((((y&x)^(z&y))^(t&x))^(t&y))^(t&z))^y))|(((((((z&x)^(z&y))^(t&x))^(t&y))^(t&z))^x)^y))"; -//inputText = "a|b|c"; + +inputText = "(x0^x1^x2^x3)&(x3|(x4|x5&x6))|x7|x8|x9"; + +inputText = "(x4&(((x5&((x0^x1)^x2))&x6)^((x0^x1)^x2)))"; + +inputText = "(((x5&((x0^x1)^x2))&x6)^((x0^x1)^x2))"; // 0,1,2,5,6 + +inputText = "x0|x1|x2|x3^(x4|x5|x6&x7)"; + +inputText = "(a|b|c)^d"; +inputText = "(((~((((((y&x)^(t&x))^(t&y))^x)^y)^t))|(~((((((z&y)^(t&x))^(t&y))^y)^z)^t)))|((~t)&(~z)))"; +inputText = "(x0^x1^x2^x3)&(x3|(x4|x5&x6))|x7|x8|x9"; + +inputText = "(((((((((((((((((((a&(~b))&(~c))&(~d))&f)&g)|((((((~a)&b)&(~c))&(~d))&f)&g))|((((((~a)&(~b))&c)&(~d))&f)&g))|(((((a&b)&c)&(~d))&f)&g))|((((a&(~b))&(~c))&(~d))&e))|(((((~a)&b)&(~c))&(~d))&e))|(((((~a)&(~b))&c)&(~d))&e))|((((a&b)&c)&(~d))&e))|((((~a)&(~b))&(~c))&d))|(((a&b)&(~c))&d))|(((a&(~b))&c)&d))|((((~a)&b)&c)&d))|h)|i)|l)"; + +inputText = "d & a & e ^ (b ^ a ^ c ^ -1) & d ^ e & a ^ e & b ^ e & c ^ (b ^ a) & d & (l & i) ^ d & e & (c ^ b) ^ c & f & g ^ h ^ g & f & (d & c & e) ^ g & f & (b & d & e) ^ g & f & (d & a & e) ^ g & f & (d & a) ^ g & f & (b & d) ^ g & f & (d & c) ^ g & f & (e & a) ^ g & f & (e & b) ^ g & f & (e & c) ^ g & f & a ^ g & f & b ^ d & a & e & h ^ b & d & e & h ^ d & c & e & h ^ c & f & g & h ^ d & a & h ^ b & d & h ^ d & c & h ^ e & a & h ^ d & h ^ i ^ b & d & h & i ^ i & (g & f & (b & d & e)) ^ g & f & (e & c) & h ^ e & h & (c ^ b) ^ h & (g & f & (b & d)) ^ g & f & (d & c) & h ^ g & f & (d & c & e) & i ^ g & f & (d & a) & i ^ i & (g & f & (b & d)) ^ g & f & (e & b) & i ^ g & f & (e & c) & i ^ d & a & e & h & i ^ b & d & e & h & i ^ d & c & e & h & i ^ d & a & e & i ^ b & d & e & i ^ d & a & h & i ^ d & a & i ^ b & d & i ^ d & c & i ^ e & a & i ^ e & b & i ^ d & i ^ i & h ^ (g & f & (e & a) ^ g & f & (e & b)) & h ^ i & h & (e & c) ^ g & f & (d & a & e) & h & l ^ i & h & (g & f & (b & d & e)) ^ g & f & (d & a & e) & h & i ^ (g & f & (d & a & e) ^ g & f & (b & d & e)) & h ^ (g & f & (d & c & e) ^ g & f & (d & a)) & h ^ (g & f & a ^ g & f & b) & h ^ g & f & (d & a) & h & i ^ i & h & (g & f & (b & d)) ^ g & f & (d & c) & h & i ^ g & f & (e & a) & (i & h) ^ g & f & (e & b) & (i & h) ^ i & h & (g & f & (e & c)) ^ l & (g & f & (b & d & e)) ^ g & f & (d & c & e) & l ^ g & f & (d & a) & h & l ^ g & f & (d & c) & h & l ^ g & f & (d & a) & i & l ^ g & f & (e & c) & i & l ^ d & a & e & h & i & l ^ b & d & e & h & i & l ^ d & c & e & h & i & l ^ g & f & (d & a) & l ^ l & (g & f & (b & d)) ^ g & f & (d & c) & l ^ g & f & (e & a) & l ^ g & f & (e & b) & l ^ g & f & (e & c) & l ^ d & a & e & h & l ^ b & d & e & h & l ^ d & c & e & h & l ^ g & f & a & h & l ^ d & a & e & i & l ^ b & d & e & i & l ^ b & d & h & i & l ^ b & d & e & l ^ d & c & e & l ^ (g & f & a ^ g & f & b) & l ^ (c & f & g ^ d & a & h) & l ^ b & d & h & l ^ d & c & h & l ^ e & a & h & l ^ l & (e & h & (c ^ b)) ^ e & a & i & l ^ (b & d ^ (e & a ^ d & c)) & l ^ e & b & l ^ e & c & l ^ d & h & l ^ d & i & l ^ i & h & l ^ d & l ^ (i ^ h) & l ^ (b ^ a) & e & (i & h) ^ l & i & (g & f & (e & a) & h) ^ ((b ^ a ^ c) & e & (g & f) & (d & h & i) ^ -1) & l ^ l & i & (g & f & (b & d) ^ g & f & (d & c)) ^ l & h & (g & f & (e & c)) ^ d & (i & h & c) ^ g & f & (i & h & c) ^ d & c & h & (l & i) ^ (e & b & i ^ d & a) & l ^ (d & h ^ e & c ^ (g & f & b ^ c & f & g)) & i ^ (g & f & (d & c & e) & i ^ g & f & (d & a & e)) & l ^ l & i & (d & c & e) ^ l & i & (g & f & a) ^ l & i & (g & f & b) ^ l & i & (e & c) ^ l & i & (d & h) ^ l & h & (g & f & (b & d & e)) ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e)) & i ^ (g & f & a ^ g & f & b) & h & i ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e) & i) & l ^ l & i & (g & f & (b & d & e)) ^ g & f & (d & a) & h & i & l ^ l & i & (h & (g & f & (b & d))) ^ g & f & (d & c) & h & i & l ^ (g & f & (e & b) ^ g & f & (e & c)) & h & (l & i) ^ l & h & (g & f & (b & d)) ^ l & h & (g & f & (e & a) ^ g & f & (e & b)) ^ l & i & (g & f & (e & a) ^ g & f & (e & b) ^ g & f & a & h) ^ (g & f & b ^ c & f & g) & h & l ^ l & i & (c & f & g ^ d & a & h) ^ l & i & ((g & f & b ^ c & f & g) & h) ^ (b ^ a) & e & (i & h) & l ^ d & (l & i & c) ^ (g & f & (e & a) ^ d & c & e ^ g & f & (d & c) ^ g & f & a) & i ^ (i & h & (e & c) ^ d & a & e) & l"; var printHelp = () => { Console.WriteLine("Usage: Simplifier.exe"); From c314e827fce360b3d479e4172b31279952c2858a Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Tue, 11 Mar 2025 20:57:44 -0400 Subject: [PATCH 05/15] Repeatedly apply optimizations --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 7 +++++++ Simplifier/Program.cs | 2 ++ 2 files changed, 9 insertions(+) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 95590f6..1048111 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -80,6 +80,13 @@ private unsafe AstIdx SimplifyBoolean() // TODO: Apply the identify a^(~a&b) => a|b var simplified = SimplifyRec(factored.Value); + for(int i = 0; i < 5; i++) + { + simplified = SimplifyORsRec(simplified); + simplified = SimplifyRec(simplified); + simplified = ctx.RecursiveSimplify(simplified); + } + // The results are somewhat improved by running the simplifier a few times, but we don't want to pay this cost for now. /* simplified = SimplifyRec(factored.Value); diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index c1934ba..02b4f57 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -41,6 +41,8 @@ inputText = "(((((((((((((((((((a&(~b))&(~c))&(~d))&f)&g)|((((((~a)&b)&(~c))&(~d))&f)&g))|((((((~a)&(~b))&c)&(~d))&f)&g))|(((((a&b)&c)&(~d))&f)&g))|((((a&(~b))&(~c))&(~d))&e))|(((((~a)&b)&(~c))&(~d))&e))|(((((~a)&(~b))&c)&(~d))&e))|((((a&b)&c)&(~d))&e))|((((~a)&(~b))&(~c))&d))|(((a&b)&(~c))&d))|(((a&(~b))&c)&d))|((((~a)&b)&c)&d))|h)|i)|l)"; inputText = "d & a & e ^ (b ^ a ^ c ^ -1) & d ^ e & a ^ e & b ^ e & c ^ (b ^ a) & d & (l & i) ^ d & e & (c ^ b) ^ c & f & g ^ h ^ g & f & (d & c & e) ^ g & f & (b & d & e) ^ g & f & (d & a & e) ^ g & f & (d & a) ^ g & f & (b & d) ^ g & f & (d & c) ^ g & f & (e & a) ^ g & f & (e & b) ^ g & f & (e & c) ^ g & f & a ^ g & f & b ^ d & a & e & h ^ b & d & e & h ^ d & c & e & h ^ c & f & g & h ^ d & a & h ^ b & d & h ^ d & c & h ^ e & a & h ^ d & h ^ i ^ b & d & h & i ^ i & (g & f & (b & d & e)) ^ g & f & (e & c) & h ^ e & h & (c ^ b) ^ h & (g & f & (b & d)) ^ g & f & (d & c) & h ^ g & f & (d & c & e) & i ^ g & f & (d & a) & i ^ i & (g & f & (b & d)) ^ g & f & (e & b) & i ^ g & f & (e & c) & i ^ d & a & e & h & i ^ b & d & e & h & i ^ d & c & e & h & i ^ d & a & e & i ^ b & d & e & i ^ d & a & h & i ^ d & a & i ^ b & d & i ^ d & c & i ^ e & a & i ^ e & b & i ^ d & i ^ i & h ^ (g & f & (e & a) ^ g & f & (e & b)) & h ^ i & h & (e & c) ^ g & f & (d & a & e) & h & l ^ i & h & (g & f & (b & d & e)) ^ g & f & (d & a & e) & h & i ^ (g & f & (d & a & e) ^ g & f & (b & d & e)) & h ^ (g & f & (d & c & e) ^ g & f & (d & a)) & h ^ (g & f & a ^ g & f & b) & h ^ g & f & (d & a) & h & i ^ i & h & (g & f & (b & d)) ^ g & f & (d & c) & h & i ^ g & f & (e & a) & (i & h) ^ g & f & (e & b) & (i & h) ^ i & h & (g & f & (e & c)) ^ l & (g & f & (b & d & e)) ^ g & f & (d & c & e) & l ^ g & f & (d & a) & h & l ^ g & f & (d & c) & h & l ^ g & f & (d & a) & i & l ^ g & f & (e & c) & i & l ^ d & a & e & h & i & l ^ b & d & e & h & i & l ^ d & c & e & h & i & l ^ g & f & (d & a) & l ^ l & (g & f & (b & d)) ^ g & f & (d & c) & l ^ g & f & (e & a) & l ^ g & f & (e & b) & l ^ g & f & (e & c) & l ^ d & a & e & h & l ^ b & d & e & h & l ^ d & c & e & h & l ^ g & f & a & h & l ^ d & a & e & i & l ^ b & d & e & i & l ^ b & d & h & i & l ^ b & d & e & l ^ d & c & e & l ^ (g & f & a ^ g & f & b) & l ^ (c & f & g ^ d & a & h) & l ^ b & d & h & l ^ d & c & h & l ^ e & a & h & l ^ l & (e & h & (c ^ b)) ^ e & a & i & l ^ (b & d ^ (e & a ^ d & c)) & l ^ e & b & l ^ e & c & l ^ d & h & l ^ d & i & l ^ i & h & l ^ d & l ^ (i ^ h) & l ^ (b ^ a) & e & (i & h) ^ l & i & (g & f & (e & a) & h) ^ ((b ^ a ^ c) & e & (g & f) & (d & h & i) ^ -1) & l ^ l & i & (g & f & (b & d) ^ g & f & (d & c)) ^ l & h & (g & f & (e & c)) ^ d & (i & h & c) ^ g & f & (i & h & c) ^ d & c & h & (l & i) ^ (e & b & i ^ d & a) & l ^ (d & h ^ e & c ^ (g & f & b ^ c & f & g)) & i ^ (g & f & (d & c & e) & i ^ g & f & (d & a & e)) & l ^ l & i & (d & c & e) ^ l & i & (g & f & a) ^ l & i & (g & f & b) ^ l & i & (e & c) ^ l & i & (d & h) ^ l & h & (g & f & (b & d & e)) ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e)) & i ^ (g & f & a ^ g & f & b) & h & i ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e) & i) & l ^ l & i & (g & f & (b & d & e)) ^ g & f & (d & a) & h & i & l ^ l & i & (h & (g & f & (b & d))) ^ g & f & (d & c) & h & i & l ^ (g & f & (e & b) ^ g & f & (e & c)) & h & (l & i) ^ l & h & (g & f & (b & d)) ^ l & h & (g & f & (e & a) ^ g & f & (e & b)) ^ l & i & (g & f & (e & a) ^ g & f & (e & b) ^ g & f & a & h) ^ (g & f & b ^ c & f & g) & h & l ^ l & i & (c & f & g ^ d & a & h) ^ l & i & ((g & f & b ^ c & f & g) & h) ^ (b ^ a) & e & (i & h) & l ^ d & (l & i & c) ^ (g & f & (e & a) ^ d & c & e ^ g & f & (d & c) ^ g & f & a) & i ^ (i & h & (e & c) ^ d & a & e) & l"; + +inputText = "((((e&((a^b)^c))|((f&((a^b)^c))&g))|((h|i)|l))^(d&(((((h&(((~((a^b)^c))^((f&((a^b)^c))&g))^(e&(((f&((a^b)^c))&g)^((a^b)^c)))))|(i&(((~((a^b)^c))^((f&((a^b)^c))&g))^(e&(((f&((a^b)^c))&g)^((a^b)^c))))))|(l&((((f&((a^b)^c))&g)|(e&((a^b)^c)))^(~((a^b)^c)))))^(((f&((a^b)^c))&g)|(e&((a^b)^c))))^(~((a^b)^c)))))"; var printHelp = () => { Console.WriteLine("Usage: Simplifier.exe"); From a640f4a9f4de7ef3cbbd9579d2a98e387dc9802b Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Wed, 12 Mar 2025 11:37:26 -0400 Subject: [PATCH 06/15] Bug fixes and miscompile debugging --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 4 ++-- Simplifier/Program.cs | 5 +++++ 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 1048111..8a5a6ca 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -80,11 +80,11 @@ private unsafe AstIdx SimplifyBoolean() // TODO: Apply the identify a^(~a&b) => a|b var simplified = SimplifyRec(factored.Value); - for(int i = 0; i < 5; i++) + for(int i = 0; i < 100; i++) { simplified = SimplifyORsRec(simplified); simplified = SimplifyRec(simplified); - simplified = ctx.RecursiveSimplify(simplified); + //simplified = ctx.RecursiveSimplify(simplified); } // The results are somewhat improved by running the simplifier a few times, but we don't want to pay this cost for now. diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index 02b4f57..524ed40 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -43,6 +43,11 @@ inputText = "d & a & e ^ (b ^ a ^ c ^ -1) & d ^ e & a ^ e & b ^ e & c ^ (b ^ a) & d & (l & i) ^ d & e & (c ^ b) ^ c & f & g ^ h ^ g & f & (d & c & e) ^ g & f & (b & d & e) ^ g & f & (d & a & e) ^ g & f & (d & a) ^ g & f & (b & d) ^ g & f & (d & c) ^ g & f & (e & a) ^ g & f & (e & b) ^ g & f & (e & c) ^ g & f & a ^ g & f & b ^ d & a & e & h ^ b & d & e & h ^ d & c & e & h ^ c & f & g & h ^ d & a & h ^ b & d & h ^ d & c & h ^ e & a & h ^ d & h ^ i ^ b & d & h & i ^ i & (g & f & (b & d & e)) ^ g & f & (e & c) & h ^ e & h & (c ^ b) ^ h & (g & f & (b & d)) ^ g & f & (d & c) & h ^ g & f & (d & c & e) & i ^ g & f & (d & a) & i ^ i & (g & f & (b & d)) ^ g & f & (e & b) & i ^ g & f & (e & c) & i ^ d & a & e & h & i ^ b & d & e & h & i ^ d & c & e & h & i ^ d & a & e & i ^ b & d & e & i ^ d & a & h & i ^ d & a & i ^ b & d & i ^ d & c & i ^ e & a & i ^ e & b & i ^ d & i ^ i & h ^ (g & f & (e & a) ^ g & f & (e & b)) & h ^ i & h & (e & c) ^ g & f & (d & a & e) & h & l ^ i & h & (g & f & (b & d & e)) ^ g & f & (d & a & e) & h & i ^ (g & f & (d & a & e) ^ g & f & (b & d & e)) & h ^ (g & f & (d & c & e) ^ g & f & (d & a)) & h ^ (g & f & a ^ g & f & b) & h ^ g & f & (d & a) & h & i ^ i & h & (g & f & (b & d)) ^ g & f & (d & c) & h & i ^ g & f & (e & a) & (i & h) ^ g & f & (e & b) & (i & h) ^ i & h & (g & f & (e & c)) ^ l & (g & f & (b & d & e)) ^ g & f & (d & c & e) & l ^ g & f & (d & a) & h & l ^ g & f & (d & c) & h & l ^ g & f & (d & a) & i & l ^ g & f & (e & c) & i & l ^ d & a & e & h & i & l ^ b & d & e & h & i & l ^ d & c & e & h & i & l ^ g & f & (d & a) & l ^ l & (g & f & (b & d)) ^ g & f & (d & c) & l ^ g & f & (e & a) & l ^ g & f & (e & b) & l ^ g & f & (e & c) & l ^ d & a & e & h & l ^ b & d & e & h & l ^ d & c & e & h & l ^ g & f & a & h & l ^ d & a & e & i & l ^ b & d & e & i & l ^ b & d & h & i & l ^ b & d & e & l ^ d & c & e & l ^ (g & f & a ^ g & f & b) & l ^ (c & f & g ^ d & a & h) & l ^ b & d & h & l ^ d & c & h & l ^ e & a & h & l ^ l & (e & h & (c ^ b)) ^ e & a & i & l ^ (b & d ^ (e & a ^ d & c)) & l ^ e & b & l ^ e & c & l ^ d & h & l ^ d & i & l ^ i & h & l ^ d & l ^ (i ^ h) & l ^ (b ^ a) & e & (i & h) ^ l & i & (g & f & (e & a) & h) ^ ((b ^ a ^ c) & e & (g & f) & (d & h & i) ^ -1) & l ^ l & i & (g & f & (b & d) ^ g & f & (d & c)) ^ l & h & (g & f & (e & c)) ^ d & (i & h & c) ^ g & f & (i & h & c) ^ d & c & h & (l & i) ^ (e & b & i ^ d & a) & l ^ (d & h ^ e & c ^ (g & f & b ^ c & f & g)) & i ^ (g & f & (d & c & e) & i ^ g & f & (d & a & e)) & l ^ l & i & (d & c & e) ^ l & i & (g & f & a) ^ l & i & (g & f & b) ^ l & i & (e & c) ^ l & i & (d & h) ^ l & h & (g & f & (b & d & e)) ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e)) & i ^ (g & f & a ^ g & f & b) & h & i ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e) & i) & l ^ l & i & (g & f & (b & d & e)) ^ g & f & (d & a) & h & i & l ^ l & i & (h & (g & f & (b & d))) ^ g & f & (d & c) & h & i & l ^ (g & f & (e & b) ^ g & f & (e & c)) & h & (l & i) ^ l & h & (g & f & (b & d)) ^ l & h & (g & f & (e & a) ^ g & f & (e & b)) ^ l & i & (g & f & (e & a) ^ g & f & (e & b) ^ g & f & a & h) ^ (g & f & b ^ c & f & g) & h & l ^ l & i & (c & f & g ^ d & a & h) ^ l & i & ((g & f & b ^ c & f & g) & h) ^ (b ^ a) & e & (i & h) & l ^ d & (l & i & c) ^ (g & f & (e & a) ^ d & c & e ^ g & f & (d & c) ^ g & f & a) & i ^ (i & h & (e & c) ^ d & a & e) & l"; inputText = "((((e&((a^b)^c))|((f&((a^b)^c))&g))|((h|i)|l))^(d&(((((h&(((~((a^b)^c))^((f&((a^b)^c))&g))^(e&(((f&((a^b)^c))&g)^((a^b)^c)))))|(i&(((~((a^b)^c))^((f&((a^b)^c))&g))^(e&(((f&((a^b)^c))&g)^((a^b)^c))))))|(l&((((f&((a^b)^c))&g)|(e&((a^b)^c)))^(~((a^b)^c)))))^(((f&((a^b)^c))&g)|(e&((a^b)^c))))^(~((a^b)^c)))))"; + +inputText = "(x0^x1^x2^x3)&(x3|(x4|x5&x6))|x7|x8|x9"; + +inputText = "(a^b)|(c^d)"; + var printHelp = () => { Console.WriteLine("Usage: Simplifier.exe"); From b95ab35774317e85a0721c46596d7f9f71e98085 Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Fri, 14 Mar 2025 02:43:35 -0400 Subject: [PATCH 07/15] changes --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 65 +++++++++++++++++++++ Simplifier/Program.cs | 4 ++ 2 files changed, 69 insertions(+) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 8a5a6ca..38f380d 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -39,6 +39,69 @@ private AnfMinimizer(AstCtx ctx, IReadOnlyList variables, TruthTable tru this.truthTable = truthTable; } + private void Groebner() + { + // Collect all dnf terms + var terms = new List(); + for (int i = 0; i < truthTable.NumBits; i++) + { + if (!truthTable.GetBit(i)) + continue; + + // Construct dnf for this term + var bitwise = new List(); + for (ushort varIdx = 0; varIdx < truthTable.NumVars; varIdx++) + { + var vMask = 1 << varIdx; + var negated = (i & vMask) == 0; + bitwise.Add(negated ? ctx.Neg(variables[varIdx]) : variables[varIdx]); + } + + terms.Add(ctx.And(bitwise)); + } + + foreach (var term in terms) + { + var table = GetTruthTable(term, variables); + bool negated = table.GetBit(0); + var resultVec = table.AsList().Select(x => negated ? Negate(x) : (uint)x).ToArray(); + var (anfTerms, variableCombinations) = GetAnfTerms(ctx, variables, resultVec); + + anfTerms.Reverse(); + + AstIdx? result = null; + foreach (var anfTerm in anfTerms) + { + var conj = LinearSimplifier.ConjunctionFromVarMask(ctx, variables, 1, variableCombinations[anfTerm], null); + if (result == null) + result = conj; + else + result = ctx.Xor(result.Value, conj); + } + + + + if (negated) + result = ctx.Xor(ctx.Constant(ulong.MaxValue, ctx.GetWidth(result.Value)), result.Value); + + var normal = ctx.GetAstString(result.Value); + var astStr = ctx.GetAstString(result.Value); + astStr = astStr.Replace("(", ""); + astStr = astStr.Replace(")", ""); + astStr = astStr.Replace("&", "*"); + astStr = astStr.Replace("^", " + "); + + normal = astStr.Replace("(", ""); + normal = astStr.Replace(")", ""); + //normal = astStr.Replace("&", "*"); + //normal = astStr.Replace("^", " + "); + //Console.WriteLine($"{astStr} = 1"); + Console.WriteLine($"{normal} = 1"); + } + + Debugger.Break(); + } + private unsafe AstIdx SimplifyBoolean() { // If the truth table has a positive constant offset, negate the result vector. @@ -46,6 +109,8 @@ private unsafe AstIdx SimplifyBoolean() var resultVec = truthTable.AsList().Select(x => negated ? Negate(x) : (uint)x).ToArray(); var (terms, variableCombinations) = GetAnfTerms(ctx, variables, resultVec); + Groebner(); + AstIdx? result = null; foreach (var term in terms) { diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index 524ed40..9d09014 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -48,6 +48,10 @@ inputText = "(a^b)|(c^d)"; +inputText = "a^b^c"; + + + var printHelp = () => { Console.WriteLine("Usage: Simplifier.exe"); From 61aff6e6fcd29d6839f55b48a39fe5f825d6cb69 Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Tue, 25 Mar 2025 01:22:43 -0400 Subject: [PATCH 08/15] changes --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 2 +- Simplifier/Program.cs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 38f380d..01c9fe0 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -109,7 +109,7 @@ private unsafe AstIdx SimplifyBoolean() var resultVec = truthTable.AsList().Select(x => negated ? Negate(x) : (uint)x).ToArray(); var (terms, variableCombinations) = GetAnfTerms(ctx, variables, resultVec); - Groebner(); + //Groebner(); AstIdx? result = null; foreach (var term in terms) diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index 9d09014..7a61008 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -48,7 +48,7 @@ inputText = "(a^b)|(c^d)"; -inputText = "a^b^c"; +//inputText = "a^b^c"; From 1e73973d57d01a7638146dbec923250f91c71cc0 Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Fri, 6 Jun 2025 10:31:14 -0400 Subject: [PATCH 09/15] Add VarConj class --- MSiMBA | 2 +- Mba.Simplifier/Minimization/AnfMinimizer.cs | 27 +++++++++++++++++++++ 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/MSiMBA b/MSiMBA index 59d3e12..a146394 160000 --- a/MSiMBA +++ b/MSiMBA @@ -1 +1 @@ -Subproject commit 59d3e12dee832e9ded53f00cdfbbb1581f2eb8d2 +Subproject commit a1463945ab252534004701764c3422f63d159b62 diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 01c9fe0..06467f8 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -16,6 +16,33 @@ namespace Mba.Simplifier.Minimization { + public struct VarConj + { + public uint Idx; + + public VarConj(uint idx) + { + Idx = idx; + } + + public override string ToString() + { + var conjs = new List(); + for(ushort i = 0; i < 32; i++) + { + if((Idx & 1u << i) != 0) + conjs.Add(i); + } + + return String.Join("*", conjs); + } + + public unsafe static implicit operator uint(VarConj reg) => reg.Idx; + + public unsafe static implicit operator VarConj(uint reg) => new VarConj(reg); + + } + public class AnfMinimizer { private readonly AstCtx ctx; From ad7b5529491a4b1d627e60361adccb30b66b08ff Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Fri, 6 Jun 2025 10:57:24 -0400 Subject: [PATCH 10/15] Add datastructure for debugging --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 29 ++++++++++++--------- Simplifier/Program.cs | 2 ++ 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 06467f8..9930618 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -20,6 +20,8 @@ public struct VarConj { public uint Idx; + bool IsOnes => Idx == uint.MaxValue; + public VarConj(uint idx) { Idx = idx; @@ -27,11 +29,14 @@ public VarConj(uint idx) public override string ToString() { - var conjs = new List(); + if (IsOnes) + return "-1"; + + var conjs = new List(); for(ushort i = 0; i < 32; i++) { if((Idx & 1u << i) != 0) - conjs.Add(i); + conjs.Add($"x{i}"); } return String.Join("*", conjs); @@ -51,7 +56,7 @@ public class AnfMinimizer private readonly TruthTable truthTable; - private readonly Dictionary demandedVarsMap = new(); + private readonly Dictionary demandedVarsMap = new(); // Simplify the boolean expression as a 1-bit polynomial. // When the ground truth contains many XORs, this yields exponentially more compact results than DNF. @@ -164,7 +169,7 @@ private unsafe AstIdx SimplifyBoolean() // Yield a XOR of factored variable conjunctions // e.g. e ^ (a&(b&c)) - var factored = Factor(ctx, variables, terms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); + var factored = Factor(ctx, variables, terms.Select(x => (VarConj)variableCombinations[x]).ToList(), demandedVarsMap); factored = SimplifyORsRec(factored.Value); //factored = TrySimplifyORs(factored.Value); @@ -238,12 +243,12 @@ private ulong Negate(int x) } // Apply greedy factoring over a sum of variable conjunctions - private static AstIdx? Factor(AstCtx ctx, IReadOnlyList variables, List conjs, Dictionary demandedVarsMap) + private static AstIdx? Factor(AstCtx ctx, IReadOnlyList variables, List conjs, Dictionary demandedVarsMap) { var getConjFromMask = (uint mask) => LinearSimplifier.ConjunctionFromVarMask(ctx, variables, 1, mask, null); // Remove the constant term if it exists - bool has = conjs.Remove(uint.MaxValue); + bool hasOnes = conjs.Remove(uint.MaxValue); var variableCounts = new (int, uint)[variables.Count]; // Collect the number of times we encounter each variable. @@ -261,10 +266,10 @@ private ulong Negate(int x) Array.Sort(variableCounts, (a, b) => b.Item2.CompareTo(a.Item2)); // For each conjunction, we take out the leading factor. - var groups = new Dictionary>(); + var groups = new Dictionary>(); foreach (var conj in conjs) { - for (int index = 0; index < variableCounts.Length; index++) + for (int index = 0; index < variables.Count; index++) { var i = variableCounts[index].Item1; @@ -273,7 +278,7 @@ private ulong Negate(int x) { var newConj = conj & ~mask; if (!groups.ContainsKey(i)) - groups[i] = new List(); + groups[i] = new List(); if (newConj != 0) groups[i].Add(newConj); @@ -328,7 +333,7 @@ private ulong Negate(int x) //demandedVarsMap.TryAdd(xored, demandedSum); // If we have a constant offset of one, add it back. - if (has) + if (hasOnes) { xored = ctx.Xor(ctx.Constant(ulong.MaxValue, ctx.GetWidth(variables[0])), xored); //demandedVarsMap.TryAdd(xored, demandedSum); @@ -482,7 +487,7 @@ private AstIdx TrySimplifyORs(List terms) // Yield a XOR of factored variable conjunctions // e.g. e ^ (a&(b&c)) - var factored = Factor(ctx, varSet, bTerms.Select(x => (uint)variableCombinations[x]).ToList(), demandedVarsMap); + var factored = Factor(ctx, varSet, bTerms.Select(x => (VarConj)variableCombinations[x]).ToList(), demandedVarsMap); return ctx.Or(term1, factored.Value); //return SimplifyRec(ctx.Or(term1, factored.Value)); @@ -588,7 +593,7 @@ private AstIdx SimplifyRec(AstIdx id) private uint GetDemandedVarsMask(AstIdx id) { // If we already know the mask, return it. - uint mask = 0; + VarConj mask = 0; if (demandedVarsMap.TryGetValue(id, out mask)) return mask; diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index 7a61008..00fcaf8 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -48,6 +48,8 @@ inputText = "(a^b)|(c^d)"; +inputText = "(a&b&c&d)"; + //inputText = "a^b^c"; From dc7e9121c9c989827192dd8561e6bd51f145760a Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Mon, 16 Jun 2025 15:45:12 -0400 Subject: [PATCH 11/15] some changes --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 164 +++++++++++++++++--- Simplifier/Program.cs | 4 +- 2 files changed, 141 insertions(+), 27 deletions(-) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 9930618..6797947 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -16,17 +16,64 @@ namespace Mba.Simplifier.Minimization { - public struct VarConj + // Represents a sum of monomials in gf(2) + public class AnfPoly { - public uint Idx; + private int? hashCode; - bool IsOnes => Idx == uint.MaxValue; + public List Monoms { get; } - public VarConj(uint idx) + public AnfPoly() { - Idx = idx; + Monoms = new(); } + public AnfPoly(List monoms) + { + Monoms = monoms; + } + + public override int GetHashCode() + { + return hashCode.Value; + } + + // This is a bit dirty but the hashcode needs to be mutable so that we can unnecessary heap allocations + public void UpdateHash() + { + int hash = 17; + foreach (var m in Monoms) + hash = hash * 31 + m.GetHashCode(); + + hashCode = hash; + } + + public override string ToString() + { + return String.Join(" + ", Monoms); + } + } + + // Algebraic normal form monomials + // This can either be a product of variables (a*b*c), or a constant (-1) + public struct AnfMonom + { + public uint Mask; + + bool IsOnes => Mask == uint.MaxValue; + + public AnfMonom(uint idx) + { + Mask = idx; + } + + public bool ContainsVariable(int varIndex) + => !IsOnes && ((Mask & (1u << (ushort)varIndex)) != 0); + + // Returns a monomial without the selected variable included + public AnfMonom WithoutVariable(int varIndex) + => Mask & ~((1u << (ushort)varIndex)); + public override string ToString() { if (IsOnes) @@ -35,17 +82,23 @@ public override string ToString() var conjs = new List(); for(ushort i = 0; i < 32; i++) { - if((Idx & 1u << i) != 0) + if((Mask & 1u << i) != 0) conjs.Add($"x{i}"); } return String.Join("*", conjs); } - public unsafe static implicit operator uint(VarConj reg) => reg.Idx; + public override int GetHashCode() + { + return Mask.GetHashCode(); + } + + public static AnfMonom Ones => new AnfMonom(uint.MaxValue); - public unsafe static implicit operator VarConj(uint reg) => new VarConj(reg); + public unsafe static implicit operator uint(AnfMonom reg) => reg.Mask; + public unsafe static implicit operator AnfMonom(uint reg) => new AnfMonom(reg); } public class AnfMinimizer @@ -56,7 +109,7 @@ public class AnfMinimizer private readonly TruthTable truthTable; - private readonly Dictionary demandedVarsMap = new(); + private readonly Dictionary demandedVarsMap = new(); // Simplify the boolean expression as a 1-bit polynomial. // When the ground truth contains many XORs, this yields exponentially more compact results than DNF. @@ -169,8 +222,7 @@ private unsafe AstIdx SimplifyBoolean() // Yield a XOR of factored variable conjunctions // e.g. e ^ (a&(b&c)) - var factored = Factor(ctx, variables, terms.Select(x => (VarConj)variableCombinations[x]).ToList(), demandedVarsMap); - + var factored = Factor(ctx, variables, new AnfPoly(terms.Select(x => (AnfMonom)variableCombinations[x]).ToList()), demandedVarsMap); factored = SimplifyORsRec(factored.Value); //factored = TrySimplifyORs(factored.Value); @@ -243,16 +295,18 @@ private ulong Negate(int x) } // Apply greedy factoring over a sum of variable conjunctions - private static AstIdx? Factor(AstCtx ctx, IReadOnlyList variables, List conjs, Dictionary demandedVarsMap) + private static AstIdx? Factor(AstCtx ctx, IReadOnlyList variables, AnfPoly poly, Dictionary demandedVarsMap) { + //var bar = Factor2(ctx, variables, poly, demandedVarsMap); + var getConjFromMask = (uint mask) => LinearSimplifier.ConjunctionFromVarMask(ctx, variables, 1, mask, null); // Remove the constant term if it exists - bool hasOnes = conjs.Remove(uint.MaxValue); + bool hasOnes = poly.Monoms.Remove(uint.MaxValue); var variableCounts = new (int, uint)[variables.Count]; // Collect the number of times we encounter each variable. - foreach (var conj in conjs) + foreach (var conj in poly.Monoms) { for (int i = 0; i < variables.Count; i++) { @@ -266,8 +320,8 @@ private ulong Negate(int x) Array.Sort(variableCounts, (a, b) => b.Item2.CompareTo(a.Item2)); // For each conjunction, we take out the leading factor. - var groups = new Dictionary>(); - foreach (var conj in conjs) + var groups = new Dictionary(); + foreach (var conj in poly.Monoms) { for (int index = 0; index < variables.Count; index++) { @@ -278,12 +332,12 @@ private ulong Negate(int x) { var newConj = conj & ~mask; if (!groups.ContainsKey(i)) - groups[i] = new List(); + groups[i] = new AnfPoly(); if (newConj != 0) - groups[i].Add(newConj); + groups[i].Monoms.Add(newConj); else - groups[i].Add(uint.MaxValue); + groups[i].Monoms.Add(uint.MaxValue); break; } @@ -296,15 +350,15 @@ private ulong Negate(int x) { AstIdx result = variables[varIdx]; // If we have just 1 a single variable, yield it. - if (elems.Count == 0 || (elems.Count == 1 && elems[0] == uint.MaxValue)) + if (elems.Monoms.Count == 0 || (elems.Monoms.Count == 1 && elems.Monoms[0] == uint.MaxValue)) { output.Add(result); // In this case we already know the demanded mask continue; } // If we have 1 variable by another conjunction, yield it. - else if (elems.Count == 1) + else if (elems.Monoms.Count == 1) { - var mask = elems[0]; + var mask = elems.Monoms[0]; var conj = ctx.And(result, getConjFromMask(mask)); output.Add(conj); @@ -342,6 +396,68 @@ private ulong Negate(int x) return xored; } + private static AstIdx Factor2(AstCtx ctx, IReadOnlyList variables, AnfPoly poly, Dictionary demandedVarsMap) + { + // Remove the constant term if it exists + bool hasOnes = poly.Monoms.Remove(uint.MaxValue); + + var curr = poly; + var terms = new List<(int? varFactor, AnfPoly poly)>(); + while(true) + { + var result = RemoveGcf(variables, curr); + if (result == null) + { + terms.Add((null, curr)); + break; + } + + terms.Add((result.Value.factor, result.Value.withFactorRemoved)); + curr = result.Value.others; + } + + + + return 0; + } + + private static (int factor, AnfPoly withFactorRemoved, AnfPoly others)? RemoveGcf(IReadOnlyList variables, AnfPoly poly) + { + // Count the number of times each variable occurs. + var variableCounts = new (int, uint)[variables.Count]; + foreach (var conj in poly.Monoms) + { + for (int i = 0; i < variables.Count; i++) + { + var mask = (uint)1 << i; + if ((conj & mask) != 0) + variableCounts[i] = (i, variableCounts[i].Item2 + 1); + } + } + + // Compute which variable is most common among the monomials + var gcfVarIndex = variableCounts.MaxBy(x => x.Item2).Item1; + + if (variableCounts[gcfVarIndex].Item2 <= 1) + return null; + + + var withFactorRemoved = new AnfPoly(); + var others = new AnfPoly(); + foreach (var monom in poly.Monoms) + { + if (monom.ContainsVariable(gcfVarIndex)) + { + bool singleVariable = monom.Mask == 1u << (ushort)gcfVarIndex; + withFactorRemoved.Monoms.Add(singleVariable ? AnfMonom.Ones : monom.WithoutVariable(gcfVarIndex)); + } + else + others.Monoms.Add(monom); + } + + return (gcfVarIndex, withFactorRemoved, others); + } + private AstIdx SimplifyORsRec(AstIdx id) { var op0 = () => SimplifyORsRec(ctx.GetOp0(id)); @@ -487,7 +603,7 @@ private AstIdx TrySimplifyORs(List terms) // Yield a XOR of factored variable conjunctions // e.g. e ^ (a&(b&c)) - var factored = Factor(ctx, varSet, bTerms.Select(x => (VarConj)variableCombinations[x]).ToList(), demandedVarsMap); + var factored = Factor(ctx, varSet, new AnfPoly(bTerms.Select(x => (AnfMonom)variableCombinations[x]).ToList()), demandedVarsMap); return ctx.Or(term1, factored.Value); //return SimplifyRec(ctx.Or(term1, factored.Value)); @@ -593,7 +709,7 @@ private AstIdx SimplifyRec(AstIdx id) private uint GetDemandedVarsMask(AstIdx id) { // If we already know the mask, return it. - VarConj mask = 0; + AnfMonom mask = 0; if (demandedVarsMap.TryGetValue(id, out mask)) return mask; diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index 00fcaf8..dd5694a 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -48,11 +48,9 @@ inputText = "(a^b)|(c^d)"; -inputText = "(a&b&c&d)"; - //inputText = "a^b^c"; - +inputText = "(~((~x0 & ~x1) | ((x0 & ~x3) ^ ~x2 ^ x5) | ((x0 & ~x4) ^ (~x1 & ~x2)) | (x2 & ~x0) | (~x1 & (x2 ^ x4)) | (x2 & ~x4) | ((x3 & (~x0 ^ x1)) ^ ~x0 ^ x2 ^ x4 ^ x6))) | ((x2 & ((x0 & ((x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x3 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x5 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x5 & ~x0 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (~x3 & ~x4)))) | ((x0 & ((x1 & ((x4 & ((x2 & (x3 ^ x5 ^ x6)) ^ ~x7)) ^ (x3 & ((x5 & ~x2) ^ x6)) ^ (x6 & ~x5) ^ ~x7)) ^ (x6 & ((x2 & (~x3 ^ x4 ^ x5)) ^ (~x3 & ~x4))) ^ (x4 & ((~(x2 & x3)) ^ x5 ^ x7)) ^ (x5 & ~x2) ^ ~x7)) ^ (x5 & ~x2 & ((x4 & (~x1 ^ x3)) ^ ~x3 ^ (x1 & x6)))) | ((x0 & ((x5 & ((x1 & ((x4 & (~x2 ^ x3)) ^ x6 ^ x7)) ^ (x3 & (~x2 ^ x4 ^ x6)) ^ (~(x2 & x4)) ^ x6 ^ x7)) ^ (x2 & ((x1 & ((x3 & (~x4 ^ x6)) ^ (~(x4 & x6)))) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x7 & (~x1 ^ x3 ^ x4)) ^ (x4 & (x1 ^ x3)))) ^ (x1 & ((x2 & ((x3 & (x4 ^ x6 ^ x7)) ^ (x4 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & ((x4 & ~x3) ^ x6 ^ x7)) ^ (x3 & (x4 ^ x7)))) ^ (x3 & ((x4 & ((x2 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & (~x2 ^ x6)))) ^ (x5 & (~x2 ^ x6 ^ (x4 & x7))) ^ (x2 & x4 & (x6 ^ x7))) | (~(((x0 & ~x2) ^ ~x3 ^ x5) | x1 | (x4 ^ x2) | ((x2 & ~x0) ^ x6))) | ((x2 & ((x4 & ((x1 & (x0 ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x0 & (~x5 ^ x6)) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x0 & ((x1 & ((~(x3 & x6)) ^ x7)) ^ (~(x5 & x6)) ^ x7)) ^ (x1 & x6 & (x3 ^ x5)))) ^ (x1 & ((x6 & ((x0 & (x3 ^ x4 ^ x5)) ^ (x3 & ~x4) ^ x5)) ^ (x4 & x5 & (~(x0 & x3)))))) | ((x2 & ((x0 & ((x1 & ((x3 & (~x5 ^ x7)) ^ (x4 & ~x5) ^ x5 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ (x5 & ~x3) ^ ~x4 ^ x7)) ^ (x3 & ((x6 & (~x1 ^ x4 ^ x7)) ^ (x1 & (x4 ^ x5)) ^ ~x4 ^ x5 ^ x7)) ^ (x1 & ((x5 & (~x4 ^ x6)) ^ x4 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ ~x4 ^ x5 ^ x7)) ^ (x5 & ~x0 & (~x1 ^ x3) & (x4 ^ x6))) | ((x0 & ((x2 & ((x4 & ((x6 & ~x1) ^ ~x3 ^ x5 ^ x7)) ^ (x6 & (~x3 ^ x5)) ^ (~x1 & ~x7))) ^ (x3 & ((x1 & ((~(x4 & x5)) ^ x6 ^ x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & ((x6 & ~x5) ^ ~x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & x5 & ~x2 & (x4 ^ x6))) | ((x0 & ((x1 & ((x2 & ((x3 & (x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (x5 & (~x3 ^ x4 ^ x6 ^ x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x2 & ((x3 & (~x4 ^ x7)) ^ (x5 & (~x4 ^ x6)) ^ ~x7)) ^ (x5 & ((x3 & (~x4 ^ x6)) ^ ~x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x1 & ((x5 & ((x2 & (~x4 ^ x6 ^ x7)) ^ (~x3 & (~x4 ^ x6)))) ^ (x2 & ((x3 & (~x6 ^ x7)) ^ (x4 & x6))) ^ (x4 & x6 & ~x3))) ^ (x4 & ~x7 & (~x2 ^ x3)) ^ (x5 & ~x3 & (~x2 ^ x7))) | ((x0 & ((x1 & ((x2 & ((x3 & (x4 ^ x5 ^ x6)) ^ (x4 & ~x6) ^ x5)) ^ (x3 & (~x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (~x3 & ((x2 & (x4 ^ x5 ^ x6)) ^ (x6 & ~x4) ^ ~x5 ^ x7)))) ^ (x4 & ((x1 & ((x3 & (~x2 ^ x6 ^ x7)) ^ (x2 & ~x6) ^ ~x7)) ^ (x2 & ~x3 & ~x6) ^ (~x3 & ~x7))) ^ (x5 & ~x1 & ~x2 & ~x3) ^ (x1 & x3 & x6 & ~x2)) | ((x0 & ((x1 & ((x3 & (~((x2 & ~x7) ^ (x4 & ~x5)))) ^ (x4 & (~x2 ^ x6)) ^ ~x5 ^ x6 ^ (x2 & x7))) ^ (x2 & ((x6 & (~x3 ^ x5 ^ x7)) ^ (x4 & (x3 ^ x7)) ^ (~(x5 & x7)))) ^ (x3 & ((~(x4 & x5)) ^ x7)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x3 & ((x2 & ((x4 & (~x5 ^ x6)) ^ (x1 & (x5 ^ x7)) ^ ~x5 ^ x6)) ^ (x1 & ((x6 & ~x7) ^ ~x4 ^ x5)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x2 & ((x5 & ~x1 & ~x7) ^ (~x6 & ~x7))) ^ (x4 & ((x1 & ~x7) ^ (x5 & ~x6) ^ ~x7)) ^ (x5 & x6 & ~x1)) | ((x5 & ((x1 & ((x0 & ((x2 & ~x3) ^ ~x3 ^ x6)) ^ (~x3 & (~x2 ^ x6)))) ^ (x4 & ~x3 & (~x0 ^ x2)) ^ (x6 & ((x0 & ~x2) ^ ~x3)))) ^ (x0 & x3 & ((x1 & (x2 ^ x4 ^ x6 ^ x7)) ^ ((~x4 ^ x7) & (x2 ^ x6))))) | ((x2 & ((x6 & ((x0 & ((x1 & ~x3) ^ ~x4)) ^ (x5 & (~x1 ^ x4)) ^ (x3 & ~x4))) ^ (x1 & ((x0 & ~x4) ^ (x3 & ~x4) ^ x5)) ^ (~x4 & (x0 ^ x3 ^ x5)))) ^ (x0 & ((x1 & ((x4 & (~(x5 & ~x3))) ^ (~(x6 & ~x3)))) ^ (~x4 & ~x6))) ^ (x3 & ~x4 & (~x1 ^ x6)) ^ (x5 & ~x6 & (~x1 ^ x4))) | (~(~x5 | x0 | x2 | x3 | x4)) | ((x0 & ((x2 & ((x1 & ((x3 & (~x6 ^ x7)) ^ (x4 & ~x5) ^ ~x6)) ^ (x3 & (~x5 ^ x6 ^ x7)) ^ (x5 & ~x6) ^ ~x4)) ^ (x6 & ((x1 & (~x3 ^ x5)) ^ (x5 & ~x3) ^ ~x4)) ^ (x1 & (~(x4 & (~(x3 & x5))))) ^ (x5 & ~x3) ^ ~x4)) ^ (x3 & ((x2 & ((x1 & ~x6) ^ ~x5 ^ x6 ^ (x4 & x7))) ^ (x4 & (~x1 ^ x6)) ^ (x5 & ~x6) ^ ~x1 ^ x6)) ^ (x5 & ((x4 & ((x1 & ~x2) ^ ~x2 ^ x6)) ^ (x1 & ~x2) ^ (x2 & x6))) ^ (x1 & x2 & x6 & ~x4)) | (~(~x1 | ~x5 | (x2 ^ x0) | (x4 ^ x0) | x3)) | ((x2 & ((x0 & ((x4 & ((x1 & ~x5) ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x5 & (~x3 ^ x6 ^ x7)) ^ (x6 & ((~(x1 & x3)) ^ x7)) ^ (x1 & x3 & x7))) ^ (x1 & ((x5 & (x3 ^ x6 ^ x7)) ^ (x6 & (x3 ^ x7)) ^ ~x4 ^ x7)) ^ (x4 & ((x3 & ~x5) ^ ~x5 ^ x6)) ^ (x5 & (~x6 ^ x7)) ^ (~x6 & ~x7))) ^ (x0 & ((x6 & ((x3 & (~x1 ^ x4 ^ x5)) ^ (x7 & ~x1) ^ x4 ^ x5)) ^ (x5 & ~x4 & (x1 ^ x3)))) ^ (((x4 & ~x7) ^ (x5 & ~x3)) & (x1 ^ x6))) | (~((~(x4 ^ x1 ^ x0)) | ((x0 & (~(x1 & ~x2))) ^ (x3 & ~x5) ^ (~(x1 & x2)) ^ x5) | (x6 ^ x3 ^ x2) | (x3 & ~x1) | (x0 & x3) | (x2 & x3) | (~x1 & (~x0 ^ x5)) | (x0 & (x1 ^ x5)) | (x2 & (~x0 ^ x1 ^ x5)))) | (~(~x5 | x0 | x1 | x3 | (x6 ^ x2))) | (x1 & x5 & ~x0 & ~x2 & (x4 ^ x6)) | (x0 & x1 & ((x4 & ~x3 & (x5 ^ x6)) ^ (x2 & x6 & ~x3))) | (x5 & ~x3 & (~x0 ^ x2) & (x4 ^ x6)) | (x0 & x2 & x6 & ~x3 & ~x4) | (x1 & ((x6 & ((x3 & ~x2 & (~x0 ^ x4)) ^ (x0 & x4 & ~x2))) ^ (x0 & x4 & x5 & ~x3))) | ((x0 & ((x1 & ((x2 & ((x3 & (~x4 ^ x5)) ^ (x4 & (x5 ^ x6)) ^ x5)) ^ (x6 & (~x3 ^ x7)) ^ (~((x4 & ~x5) ^ (x7 & ~x3))))) ^ (x6 & ((x4 & (~x2 ^ x3)) ^ ~x2 ^ x3 ^ x5 ^ x7)) ^ (x5 & ((x2 & (x3 ^ x4 ^ x7)) ^ (x4 & ~x3))) ^ (x7 & (~(x3 & ~x2))) ^ ~x4)) ^ (x2 & ((x1 & ((x6 & (~x4 ^ x7)) ^ (x5 & ~x7) ^ ~x4 ^ x7)) ^ (x6 & (~x3 ^ x4 ^ x7)) ^ (x4 & ~x5) ^ (x7 & ~x5) ^ ~x3)) ^ (x5 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (x3 & ~x4) ^ (x6 & (x4 ^ x7)) ^ ~x7)) ^ (x3 & ~x6 & (x4 ^ x7))) | (x0 & x1 & x2 & x7 & (x3 ^ x5))\r\n"; var printHelp = () => { From b8ac953af7061976a7a28009f1ca79754e5eeaaa Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Thu, 19 Jun 2025 17:01:35 -0400 Subject: [PATCH 12/15] Add list-like data structure for representing booleans --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 202 +++++++++++------ .../Minimization/Factoring/BoolCtx.cs | 213 ++++++++++++++++++ .../Minimization/Factoring/BoolExpr.cs | 96 ++++++++ .../Factoring/BoolExprFormatter.cs | 58 +++++ .../Minimization/Factoring/BoolMinimizer.cs | 12 + Simplifier/Program.cs | 4 +- 6 files changed, 517 insertions(+), 68 deletions(-) create mode 100644 Mba.Simplifier/Minimization/Factoring/BoolCtx.cs create mode 100644 Mba.Simplifier/Minimization/Factoring/BoolExpr.cs create mode 100644 Mba.Simplifier/Minimization/Factoring/BoolExprFormatter.cs create mode 100644 Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 6797947..15d4d21 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -3,9 +3,9 @@ using Mba.Common.MSiMBA; using Mba.Common.Utility; using Mba.Simplifier.Bindings; +using Mba.Simplifier.Minimization.Factoring; using Mba.Simplifier.Pipeline; using Mba.Utility; -using Microsoft.Z3; using System; using System.Collections.Generic; using System.Diagnostics; @@ -38,6 +38,13 @@ public override int GetHashCode() return hashCode.Value; } + public override bool Equals(object? obj) + { + if (obj is not AnfPoly other) + return false; + return Monoms.SequenceEqual(other.Monoms); + } + // This is a bit dirty but the hashcode needs to be mutable so that we can unnecessary heap allocations public void UpdateHash() { @@ -48,6 +55,13 @@ public void UpdateHash() hashCode = hash; } + public AnfPoly Clone() + { + var clone = new AnfPoly(Monoms.ToList()); + clone.hashCode = hashCode; + return clone; + } + public override string ToString() { return String.Join(" + ", Monoms); @@ -60,7 +74,7 @@ public struct AnfMonom { public uint Mask; - bool IsOnes => Mask == uint.MaxValue; + public bool IsOnes => Mask == uint.MaxValue; public AnfMonom(uint idx) { @@ -124,69 +138,6 @@ private AnfMinimizer(AstCtx ctx, IReadOnlyList variables, TruthTable tru this.truthTable = truthTable; } - private void Groebner() - { - // Collect all dnf terms - var terms = new List(); - for (int i = 0; i < truthTable.NumBits; i++) - { - if (!truthTable.GetBit(i)) - continue; - - // Construct dnf for this term - var bitwise = new List(); - for (ushort varIdx = 0; varIdx < truthTable.NumVars; varIdx++) - { - var vMask = 1 << varIdx; - var negated = (i & vMask) == 0; - bitwise.Add(negated ? ctx.Neg(variables[varIdx]) : variables[varIdx]); - } - - terms.Add(ctx.And(bitwise)); - } - - foreach (var term in terms) - { - var table = GetTruthTable(term, variables); - bool negated = table.GetBit(0); - var resultVec = table.AsList().Select(x => negated ? Negate(x) : (uint)x).ToArray(); - var (anfTerms, variableCombinations) = GetAnfTerms(ctx, variables, resultVec); - - anfTerms.Reverse(); - - AstIdx? result = null; - foreach (var anfTerm in anfTerms) - { - var conj = LinearSimplifier.ConjunctionFromVarMask(ctx, variables, 1, variableCombinations[anfTerm], null); - if (result == null) - result = conj; - else - result = ctx.Xor(result.Value, conj); - } - - - - if (negated) - result = ctx.Xor(ctx.Constant(ulong.MaxValue, ctx.GetWidth(result.Value)), result.Value); - - var normal = ctx.GetAstString(result.Value); - var astStr = ctx.GetAstString(result.Value); - astStr = astStr.Replace("(", ""); - astStr = astStr.Replace(")", ""); - astStr = astStr.Replace("&", "*"); - astStr = astStr.Replace("^", " + "); - - normal = astStr.Replace("(", ""); - normal = astStr.Replace(")", ""); - //normal = astStr.Replace("&", "*"); - //normal = astStr.Replace("^", " + "); - //Console.WriteLine($"{astStr} = 1"); - Console.WriteLine($"{normal} = 1"); - } - - Debugger.Break(); - } - private unsafe AstIdx SimplifyBoolean() { // If the truth table has a positive constant offset, negate the result vector. @@ -297,7 +248,7 @@ private ulong Negate(int x) // Apply greedy factoring over a sum of variable conjunctions private static AstIdx? Factor(AstCtx ctx, IReadOnlyList variables, AnfPoly poly, Dictionary demandedVarsMap) { - //var bar = Factor2(ctx, variables, poly, demandedVarsMap); + var bar = Factor2(ctx, variables, poly, demandedVarsMap); var getConjFromMask = (uint mask) => LinearSimplifier.ConjunctionFromVarMask(ctx, variables, 1, mask, null); @@ -396,8 +347,35 @@ private ulong Negate(int x) return xored; } + // Yield a factored sum of products? private static AstIdx Factor2(AstCtx ctx, IReadOnlyList variables, AnfPoly poly, Dictionary demandedVarsMap) { + var boolCtx = new BoolCtx(); + ExprId.ctx = boolCtx; + List terms2 = new(); + foreach(var monom in poly.Monoms) + { + if (monom.IsOnes) + { + terms2.Add(boolCtx.Constant(uint.MaxValue)); + continue; + } + + var vars = new List(); + for (ushort i = 0; i < 32; i++) + { + if ((monom.Mask & 1u << i) != 0) + vars.Add(boolCtx.Var(i)); + } + + terms2.Add(boolCtx.Mul(vars)); + } + + var id = boolCtx.Add(terms2); + + + Console.WriteLine(id.ToString()); + // Remove the constant term if it exists bool hasOnes = poly.Monoms.Remove(uint.MaxValue); @@ -416,8 +394,34 @@ private static AstIdx Factor2(AstCtx ctx, IReadOnlyList variables, AnfPo curr = result.Value.others; } + // We have a list of (var * poly). + // Now we want to spot cases where the poly is shared among list elements, e.g.: + // - (x0, -1 + x2 + x3) + // - (x1, -1 + x2 + x3) + var groupedByLhs = new Dictionary(); + foreach(var (varFactor, polyFactor) in terms) + { + // Recompute the hash since the polynomial may have changed + polyFactor.UpdateHash(); + + var currMonom = varFactor == null ? AnfMonom.Ones : new AnfMonom(1u << (ushort)varFactor.Value); + if (!groupedByLhs.ContainsKey(polyFactor)) + { + var nnew = new AnfPoly(); + nnew.Monoms.Add(currMonom); + groupedByLhs[polyFactor] = nnew; + continue; + } + + groupedByLhs[polyFactor].Monoms.Add(currMonom); + } + // Sum of products... + + // Returns a list of AnfPoly products... + // But what about sums...? + // return 0; } @@ -501,7 +505,6 @@ private AstIdx SimplifyORsRec(AstIdx id) private AstIdx TrySimplifyORs(List terms) { - var getCost = (AstIdx? idx) => idx == null ? uint.MaxValue : ctx.GetCost(idx.Value); bool changed = true; @@ -767,5 +770,70 @@ private TruthTable GetTruthTable(AstIdx id, IReadOnlyList varSet) return table; } + + + + private void Groebner() + { + // Collect all dnf terms + var terms = new List(); + for (int i = 0; i < truthTable.NumBits; i++) + { + if (!truthTable.GetBit(i)) + continue; + + // Construct dnf for this term + var bitwise = new List(); + for (ushort varIdx = 0; varIdx < truthTable.NumVars; varIdx++) + { + var vMask = 1 << varIdx; + var negated = (i & vMask) == 0; + bitwise.Add(negated ? ctx.Neg(variables[varIdx]) : variables[varIdx]); + } + + terms.Add(ctx.And(bitwise)); + } + + foreach (var term in terms) + { + var table = GetTruthTable(term, variables); + bool negated = table.GetBit(0); + var resultVec = table.AsList().Select(x => negated ? Negate(x) : (uint)x).ToArray(); + var (anfTerms, variableCombinations) = GetAnfTerms(ctx, variables, resultVec); + + anfTerms.Reverse(); + + AstIdx? result = null; + foreach (var anfTerm in anfTerms) + { + var conj = LinearSimplifier.ConjunctionFromVarMask(ctx, variables, 1, variableCombinations[anfTerm], null); + if (result == null) + result = conj; + else + result = ctx.Xor(result.Value, conj); + } + + + + if (negated) + result = ctx.Xor(ctx.Constant(ulong.MaxValue, ctx.GetWidth(result.Value)), result.Value); + + var normal = ctx.GetAstString(result.Value); + var astStr = ctx.GetAstString(result.Value); + astStr = astStr.Replace("(", ""); + astStr = astStr.Replace(")", ""); + astStr = astStr.Replace("&", "*"); + astStr = astStr.Replace("^", " + "); + + normal = astStr.Replace("(", ""); + normal = astStr.Replace(")", ""); + //normal = astStr.Replace("&", "*"); + //normal = astStr.Replace("^", " + "); + //Console.WriteLine($"{astStr} = 1"); + Console.WriteLine($"{normal} = 1"); + } + + Debugger.Break(); + } } } diff --git a/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs b/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs new file mode 100644 index 0000000..a771062 --- /dev/null +++ b/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs @@ -0,0 +1,213 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Threading.Tasks; + +namespace Mba.Simplifier.Minimization.Factoring +{ + public class BoolCtx + { + // Hash consed list of all unique nodes + private readonly List elements = new(20000); + + // Mapping of unique nodes to their corresponding indices + private readonly Dictionary exprToIdx = new(20000); + + // Reduce allocations by reusing the same empty list across all childless nodes. + private readonly List emptyList = new(); + + // Expr id of the constant 1 + public ExprId Constant1Id { get; set; } + + public BoolCtx() + { + Constant1Id = Constant(1); + } + + public ExprId Var(uint varIdx) + { + var vNode = new BoolExpr(ExprKind.Var, emptyList, (uint)varIdx); + return AddExpr(vNode); + } + + public ExprId Constant(uint constant) + { + // Reduce the constant modulo 2. + constant &= 1; + + var vNode = new BoolExpr(ExprKind.Const, emptyList, constant); + return AddExpr(vNode); + } + + public ExprId Add(List children) + { + children = ReduceSumCoefficient(children); + children = Sort(children); + + /* + var output = new List(); + ExprId? lastInstance = null; + for(int i = 0; i < children.Count; i++) + { + if (lastInstance == null) + lastInstance = 0; + } + */ + + var vNode = new BoolExpr(ExprKind.Add, children); + return AddExpr(vNode); + } + + + private List ReduceSumCoefficient(List children) + { + return children; + var output = new List(); + + var grouped = children.GroupBy(x => x); + foreach (var group in grouped) + { + var coeff = ((uint)group.Count()) & 1; + if (coeff == 0) + continue; + + output.Add(group.First()); + } + + return output; + } + + + public ExprId Add(ExprId op1, ExprId op2) + => Add(new() { op1, op2 }); + + public ExprId Mul(List children) + { + //children = ReduceMulPower(children); + children = Sort(children); + /* + for(int i = children.Count - 1; i >= 0; i++) + { + if (i == 0) + continue; + + var op0Id = children[i]; + var op0 = Get(op0Id); + var op0Kind = op0.Kind; + + var op1Id = children[i - 1]; + var op1 = Get(op1Id); + var op1Kind = op1.Kind; + } + */ + + var vNode = new BoolExpr(ExprKind.Mul, children); + return AddExpr(vNode); + } + + private List ReduceMulPower(List children) + { + var output = new List(); + + var grouped = children.GroupBy(x => x); + foreach (var group in grouped) + { + output.Add(group.First()); + continue; + } + + return output; + } + + // TODO: Rewrite more performantly. + // Attempt to canonicalize the order of operands. + private List Sort(IReadOnlyList children) + { + return children.OrderBy(x => GetSort(x)).ToList(); ; + } + + public ulong GetSort(ExprId id) + { + var expr = Get(id); + + ulong output = 0; + + // Constants always take priority. + output |= ((ulong)Convert.ToUInt64(expr.Kind == ExprKind.Const)) << (ushort)63; + // Variables take the next priority. + output |= ((ulong)Convert.ToUInt64(expr.Kind == ExprKind.Var)) << (ushort)62; + // Anything else, we don't care about + output |= 0x3FFFFFFFFFFFFFFFu & (uint)id.Idx; + return output; + } + + public ExprId Mul(ExprId op1, ExprId op2) + { + var v0 = Get(op1); + if (TryGetConstValue(op1, out var constant)) + { + return constant == 1 ? op2 : op1; + } + var v1 = Get(op2); + if (TryGetConstValue(op2, out constant)) + { + return constant == 1 ? op1 : op2; + } + + return Mul(new() { op1, op2 }); + } + + // ~x => x+1 + public ExprId Neg(ExprId op1) + => Add(Constant1Id, op1); + + // x&y = x*y + public ExprId And(ExprId op1, ExprId op2) + => Mul(op1, op2); + + // x|y = ~((~x)*(~y)) + public ExprId Or(ExprId op1, ExprId op2) + => Neg(Mul(Neg(op1), Neg(op2))); + + public ExprId Xor(ExprId op1, ExprId op2) + => Add(op1, op2); + + public ExprId AddExpr(BoolExpr expr) + { + if (exprToIdx.TryGetValue(expr, out ExprId existingId)) + return existingId; + + var id = elements.Count; + elements.Add(expr); + exprToIdx[expr] = id; + return id; + } + + public BoolExpr Get(ExprId id) + => elements[id]; + + public string GetVarName(BoolExpr expr) + { + return $"x{expr.Data}"; + } + + public uint GetConstValue(BoolExpr expr) + { + return expr.Data; + } + + public bool TryGetConstValue(ExprId exprId, out uint constant) + { + var v0 = Get(exprId); + if (v0.Kind == ExprKind.Const) + { + constant = GetConstValue(v0); + return true; + } + + constant = 0; + return false; + } + } +} diff --git a/Mba.Simplifier/Minimization/Factoring/BoolExpr.cs b/Mba.Simplifier/Minimization/Factoring/BoolExpr.cs new file mode 100644 index 0000000..2a49951 --- /dev/null +++ b/Mba.Simplifier/Minimization/Factoring/BoolExpr.cs @@ -0,0 +1,96 @@ +using Mba.Simplifier.Bindings; +using Microsoft.Z3; +using System; +using System.Collections.Generic; +using System.Diagnostics.CodeAnalysis; +using System.Linq; +using System.Text; +using System.Threading.Tasks; + +namespace Mba.Simplifier.Minimization.Factoring +{ + public struct ExprId + { + public int Idx; + + public ExprId(int idx) + { + Idx = idx; + } + + public override string ToString() + { + if (ctx == null) + return Idx.ToString(); + //return ctx.GetAstString(Idx); + return BoolExprFormatter.FormatAst(ctx, Idx); + } + + public unsafe static implicit operator int(ExprId reg) => reg.Idx; + + public unsafe static implicit operator ExprId(int reg) => new ExprId(reg); + + // This is a hack to allow viewing AST nodes in the debugger. + public static BoolCtx ctx; + } + + public enum ExprKind : byte + { + Var = 0, + Const = 1, + Add = 2, + Mul = 3, + } + + // Hash consed immutable AST structure. + // Technically this is a DAG. + public struct BoolExpr + { + public readonly ExprKind Kind; + + public readonly IReadOnlyList Children; + + // Optional field for variable names and constant values. + public readonly uint Data; + private readonly int hash; + + public BoolExpr(ExprKind exprId, List children, uint data = 0) + { + Kind = exprId; + Children = children; + Data = data; + hash = CalcHash(); + } + + private int CalcHash() + { + int hash = 17; + hash = hash * 23 + (int)Kind; + foreach (var id in Children) + hash = hash * 23 + id.GetHashCode(); + return hash; + } + + public override int GetHashCode() + { + return hash; + } + + public override bool Equals([NotNullWhen(true)] object? obj) + { + if (obj is not BoolExpr other) + return false; + + if (hash != other.GetHashCode() || Kind != other.Kind || Data != other.Data || Children.Count != other.Children.Count) + return false; + + for (int i = 0; i < Children.Count; i++) + { + if (Children[i] != other.Children[i]) + return false; + } + + return true; + } + } +} diff --git a/Mba.Simplifier/Minimization/Factoring/BoolExprFormatter.cs b/Mba.Simplifier/Minimization/Factoring/BoolExprFormatter.cs new file mode 100644 index 0000000..223d4db --- /dev/null +++ b/Mba.Simplifier/Minimization/Factoring/BoolExprFormatter.cs @@ -0,0 +1,58 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Threading.Tasks; + +namespace Mba.Simplifier.Minimization.Factoring +{ + public static class BoolExprFormatter + { + public static string FormatAst(BoolCtx ctx, ExprId id) + { + var sb = new StringBuilder(); + FormatInternal(ctx, id, ref sb); + return sb.ToString(); + } + + private static void FormatInternal(BoolCtx ctx, ExprId id, ref StringBuilder sb) + { + var node = ctx.Get(id); + switch (node.Kind) + { + case ExprKind.Var: + sb.Append(ctx.GetVarName(node)); + break; + case ExprKind.Const: + sb.Append(ctx.GetConstValue(node)); + break; + case ExprKind.Add: + case ExprKind.Mul: + sb.Append("("); + + for (int i = 0; i < node.Children.Count; i++) + { + FormatInternal(ctx, node.Children[i], ref sb); + if (i != node.Children.Count - 1) + sb.Append(GetOperatorName(node.Kind)); + } + + + sb.Append(")"); + break; + default: + throw new InvalidOperationException(); + } + } + + private static string GetOperatorName(ExprKind exprKind) + { + return exprKind switch + { + ExprKind.Add => "+", + ExprKind.Mul => "*", + _ => throw new InvalidOperationException($"Unrecognized operator: {exprKind}") + }; + } + } +} diff --git a/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs b/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs new file mode 100644 index 0000000..564fae3 --- /dev/null +++ b/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs @@ -0,0 +1,12 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Threading.Tasks; + +namespace Mba.Simplifier.Minimization.Factoring +{ + internal class BoolMinimizer + { + } +} diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index dd5694a..d3379e6 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -48,9 +48,11 @@ inputText = "(a^b)|(c^d)"; +//inputText = "a|b|c|d"; + //inputText = "a^b^c"; -inputText = "(~((~x0 & ~x1) | ((x0 & ~x3) ^ ~x2 ^ x5) | ((x0 & ~x4) ^ (~x1 & ~x2)) | (x2 & ~x0) | (~x1 & (x2 ^ x4)) | (x2 & ~x4) | ((x3 & (~x0 ^ x1)) ^ ~x0 ^ x2 ^ x4 ^ x6))) | ((x2 & ((x0 & ((x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x3 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x5 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x5 & ~x0 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (~x3 & ~x4)))) | ((x0 & ((x1 & ((x4 & ((x2 & (x3 ^ x5 ^ x6)) ^ ~x7)) ^ (x3 & ((x5 & ~x2) ^ x6)) ^ (x6 & ~x5) ^ ~x7)) ^ (x6 & ((x2 & (~x3 ^ x4 ^ x5)) ^ (~x3 & ~x4))) ^ (x4 & ((~(x2 & x3)) ^ x5 ^ x7)) ^ (x5 & ~x2) ^ ~x7)) ^ (x5 & ~x2 & ((x4 & (~x1 ^ x3)) ^ ~x3 ^ (x1 & x6)))) | ((x0 & ((x5 & ((x1 & ((x4 & (~x2 ^ x3)) ^ x6 ^ x7)) ^ (x3 & (~x2 ^ x4 ^ x6)) ^ (~(x2 & x4)) ^ x6 ^ x7)) ^ (x2 & ((x1 & ((x3 & (~x4 ^ x6)) ^ (~(x4 & x6)))) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x7 & (~x1 ^ x3 ^ x4)) ^ (x4 & (x1 ^ x3)))) ^ (x1 & ((x2 & ((x3 & (x4 ^ x6 ^ x7)) ^ (x4 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & ((x4 & ~x3) ^ x6 ^ x7)) ^ (x3 & (x4 ^ x7)))) ^ (x3 & ((x4 & ((x2 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & (~x2 ^ x6)))) ^ (x5 & (~x2 ^ x6 ^ (x4 & x7))) ^ (x2 & x4 & (x6 ^ x7))) | (~(((x0 & ~x2) ^ ~x3 ^ x5) | x1 | (x4 ^ x2) | ((x2 & ~x0) ^ x6))) | ((x2 & ((x4 & ((x1 & (x0 ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x0 & (~x5 ^ x6)) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x0 & ((x1 & ((~(x3 & x6)) ^ x7)) ^ (~(x5 & x6)) ^ x7)) ^ (x1 & x6 & (x3 ^ x5)))) ^ (x1 & ((x6 & ((x0 & (x3 ^ x4 ^ x5)) ^ (x3 & ~x4) ^ x5)) ^ (x4 & x5 & (~(x0 & x3)))))) | ((x2 & ((x0 & ((x1 & ((x3 & (~x5 ^ x7)) ^ (x4 & ~x5) ^ x5 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ (x5 & ~x3) ^ ~x4 ^ x7)) ^ (x3 & ((x6 & (~x1 ^ x4 ^ x7)) ^ (x1 & (x4 ^ x5)) ^ ~x4 ^ x5 ^ x7)) ^ (x1 & ((x5 & (~x4 ^ x6)) ^ x4 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ ~x4 ^ x5 ^ x7)) ^ (x5 & ~x0 & (~x1 ^ x3) & (x4 ^ x6))) | ((x0 & ((x2 & ((x4 & ((x6 & ~x1) ^ ~x3 ^ x5 ^ x7)) ^ (x6 & (~x3 ^ x5)) ^ (~x1 & ~x7))) ^ (x3 & ((x1 & ((~(x4 & x5)) ^ x6 ^ x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & ((x6 & ~x5) ^ ~x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & x5 & ~x2 & (x4 ^ x6))) | ((x0 & ((x1 & ((x2 & ((x3 & (x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (x5 & (~x3 ^ x4 ^ x6 ^ x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x2 & ((x3 & (~x4 ^ x7)) ^ (x5 & (~x4 ^ x6)) ^ ~x7)) ^ (x5 & ((x3 & (~x4 ^ x6)) ^ ~x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x1 & ((x5 & ((x2 & (~x4 ^ x6 ^ x7)) ^ (~x3 & (~x4 ^ x6)))) ^ (x2 & ((x3 & (~x6 ^ x7)) ^ (x4 & x6))) ^ (x4 & x6 & ~x3))) ^ (x4 & ~x7 & (~x2 ^ x3)) ^ (x5 & ~x3 & (~x2 ^ x7))) | ((x0 & ((x1 & ((x2 & ((x3 & (x4 ^ x5 ^ x6)) ^ (x4 & ~x6) ^ x5)) ^ (x3 & (~x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (~x3 & ((x2 & (x4 ^ x5 ^ x6)) ^ (x6 & ~x4) ^ ~x5 ^ x7)))) ^ (x4 & ((x1 & ((x3 & (~x2 ^ x6 ^ x7)) ^ (x2 & ~x6) ^ ~x7)) ^ (x2 & ~x3 & ~x6) ^ (~x3 & ~x7))) ^ (x5 & ~x1 & ~x2 & ~x3) ^ (x1 & x3 & x6 & ~x2)) | ((x0 & ((x1 & ((x3 & (~((x2 & ~x7) ^ (x4 & ~x5)))) ^ (x4 & (~x2 ^ x6)) ^ ~x5 ^ x6 ^ (x2 & x7))) ^ (x2 & ((x6 & (~x3 ^ x5 ^ x7)) ^ (x4 & (x3 ^ x7)) ^ (~(x5 & x7)))) ^ (x3 & ((~(x4 & x5)) ^ x7)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x3 & ((x2 & ((x4 & (~x5 ^ x6)) ^ (x1 & (x5 ^ x7)) ^ ~x5 ^ x6)) ^ (x1 & ((x6 & ~x7) ^ ~x4 ^ x5)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x2 & ((x5 & ~x1 & ~x7) ^ (~x6 & ~x7))) ^ (x4 & ((x1 & ~x7) ^ (x5 & ~x6) ^ ~x7)) ^ (x5 & x6 & ~x1)) | ((x5 & ((x1 & ((x0 & ((x2 & ~x3) ^ ~x3 ^ x6)) ^ (~x3 & (~x2 ^ x6)))) ^ (x4 & ~x3 & (~x0 ^ x2)) ^ (x6 & ((x0 & ~x2) ^ ~x3)))) ^ (x0 & x3 & ((x1 & (x2 ^ x4 ^ x6 ^ x7)) ^ ((~x4 ^ x7) & (x2 ^ x6))))) | ((x2 & ((x6 & ((x0 & ((x1 & ~x3) ^ ~x4)) ^ (x5 & (~x1 ^ x4)) ^ (x3 & ~x4))) ^ (x1 & ((x0 & ~x4) ^ (x3 & ~x4) ^ x5)) ^ (~x4 & (x0 ^ x3 ^ x5)))) ^ (x0 & ((x1 & ((x4 & (~(x5 & ~x3))) ^ (~(x6 & ~x3)))) ^ (~x4 & ~x6))) ^ (x3 & ~x4 & (~x1 ^ x6)) ^ (x5 & ~x6 & (~x1 ^ x4))) | (~(~x5 | x0 | x2 | x3 | x4)) | ((x0 & ((x2 & ((x1 & ((x3 & (~x6 ^ x7)) ^ (x4 & ~x5) ^ ~x6)) ^ (x3 & (~x5 ^ x6 ^ x7)) ^ (x5 & ~x6) ^ ~x4)) ^ (x6 & ((x1 & (~x3 ^ x5)) ^ (x5 & ~x3) ^ ~x4)) ^ (x1 & (~(x4 & (~(x3 & x5))))) ^ (x5 & ~x3) ^ ~x4)) ^ (x3 & ((x2 & ((x1 & ~x6) ^ ~x5 ^ x6 ^ (x4 & x7))) ^ (x4 & (~x1 ^ x6)) ^ (x5 & ~x6) ^ ~x1 ^ x6)) ^ (x5 & ((x4 & ((x1 & ~x2) ^ ~x2 ^ x6)) ^ (x1 & ~x2) ^ (x2 & x6))) ^ (x1 & x2 & x6 & ~x4)) | (~(~x1 | ~x5 | (x2 ^ x0) | (x4 ^ x0) | x3)) | ((x2 & ((x0 & ((x4 & ((x1 & ~x5) ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x5 & (~x3 ^ x6 ^ x7)) ^ (x6 & ((~(x1 & x3)) ^ x7)) ^ (x1 & x3 & x7))) ^ (x1 & ((x5 & (x3 ^ x6 ^ x7)) ^ (x6 & (x3 ^ x7)) ^ ~x4 ^ x7)) ^ (x4 & ((x3 & ~x5) ^ ~x5 ^ x6)) ^ (x5 & (~x6 ^ x7)) ^ (~x6 & ~x7))) ^ (x0 & ((x6 & ((x3 & (~x1 ^ x4 ^ x5)) ^ (x7 & ~x1) ^ x4 ^ x5)) ^ (x5 & ~x4 & (x1 ^ x3)))) ^ (((x4 & ~x7) ^ (x5 & ~x3)) & (x1 ^ x6))) | (~((~(x4 ^ x1 ^ x0)) | ((x0 & (~(x1 & ~x2))) ^ (x3 & ~x5) ^ (~(x1 & x2)) ^ x5) | (x6 ^ x3 ^ x2) | (x3 & ~x1) | (x0 & x3) | (x2 & x3) | (~x1 & (~x0 ^ x5)) | (x0 & (x1 ^ x5)) | (x2 & (~x0 ^ x1 ^ x5)))) | (~(~x5 | x0 | x1 | x3 | (x6 ^ x2))) | (x1 & x5 & ~x0 & ~x2 & (x4 ^ x6)) | (x0 & x1 & ((x4 & ~x3 & (x5 ^ x6)) ^ (x2 & x6 & ~x3))) | (x5 & ~x3 & (~x0 ^ x2) & (x4 ^ x6)) | (x0 & x2 & x6 & ~x3 & ~x4) | (x1 & ((x6 & ((x3 & ~x2 & (~x0 ^ x4)) ^ (x0 & x4 & ~x2))) ^ (x0 & x4 & x5 & ~x3))) | ((x0 & ((x1 & ((x2 & ((x3 & (~x4 ^ x5)) ^ (x4 & (x5 ^ x6)) ^ x5)) ^ (x6 & (~x3 ^ x7)) ^ (~((x4 & ~x5) ^ (x7 & ~x3))))) ^ (x6 & ((x4 & (~x2 ^ x3)) ^ ~x2 ^ x3 ^ x5 ^ x7)) ^ (x5 & ((x2 & (x3 ^ x4 ^ x7)) ^ (x4 & ~x3))) ^ (x7 & (~(x3 & ~x2))) ^ ~x4)) ^ (x2 & ((x1 & ((x6 & (~x4 ^ x7)) ^ (x5 & ~x7) ^ ~x4 ^ x7)) ^ (x6 & (~x3 ^ x4 ^ x7)) ^ (x4 & ~x5) ^ (x7 & ~x5) ^ ~x3)) ^ (x5 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (x3 & ~x4) ^ (x6 & (x4 ^ x7)) ^ ~x7)) ^ (x3 & ~x6 & (x4 ^ x7))) | (x0 & x1 & x2 & x7 & (x3 ^ x5))\r\n"; +//inputText = "(~((~x0 & ~x1) | ((x0 & ~x3) ^ ~x2 ^ x5) | ((x0 & ~x4) ^ (~x1 & ~x2)) | (x2 & ~x0) | (~x1 & (x2 ^ x4)) | (x2 & ~x4) | ((x3 & (~x0 ^ x1)) ^ ~x0 ^ x2 ^ x4 ^ x6))) | ((x2 & ((x0 & ((x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x3 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x5 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x5 & ~x0 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (~x3 & ~x4)))) | ((x0 & ((x1 & ((x4 & ((x2 & (x3 ^ x5 ^ x6)) ^ ~x7)) ^ (x3 & ((x5 & ~x2) ^ x6)) ^ (x6 & ~x5) ^ ~x7)) ^ (x6 & ((x2 & (~x3 ^ x4 ^ x5)) ^ (~x3 & ~x4))) ^ (x4 & ((~(x2 & x3)) ^ x5 ^ x7)) ^ (x5 & ~x2) ^ ~x7)) ^ (x5 & ~x2 & ((x4 & (~x1 ^ x3)) ^ ~x3 ^ (x1 & x6)))) | ((x0 & ((x5 & ((x1 & ((x4 & (~x2 ^ x3)) ^ x6 ^ x7)) ^ (x3 & (~x2 ^ x4 ^ x6)) ^ (~(x2 & x4)) ^ x6 ^ x7)) ^ (x2 & ((x1 & ((x3 & (~x4 ^ x6)) ^ (~(x4 & x6)))) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x7 & (~x1 ^ x3 ^ x4)) ^ (x4 & (x1 ^ x3)))) ^ (x1 & ((x2 & ((x3 & (x4 ^ x6 ^ x7)) ^ (x4 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & ((x4 & ~x3) ^ x6 ^ x7)) ^ (x3 & (x4 ^ x7)))) ^ (x3 & ((x4 & ((x2 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & (~x2 ^ x6)))) ^ (x5 & (~x2 ^ x6 ^ (x4 & x7))) ^ (x2 & x4 & (x6 ^ x7))) | (~(((x0 & ~x2) ^ ~x3 ^ x5) | x1 | (x4 ^ x2) | ((x2 & ~x0) ^ x6))) | ((x2 & ((x4 & ((x1 & (x0 ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x0 & (~x5 ^ x6)) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x0 & ((x1 & ((~(x3 & x6)) ^ x7)) ^ (~(x5 & x6)) ^ x7)) ^ (x1 & x6 & (x3 ^ x5)))) ^ (x1 & ((x6 & ((x0 & (x3 ^ x4 ^ x5)) ^ (x3 & ~x4) ^ x5)) ^ (x4 & x5 & (~(x0 & x3)))))) | ((x2 & ((x0 & ((x1 & ((x3 & (~x5 ^ x7)) ^ (x4 & ~x5) ^ x5 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ (x5 & ~x3) ^ ~x4 ^ x7)) ^ (x3 & ((x6 & (~x1 ^ x4 ^ x7)) ^ (x1 & (x4 ^ x5)) ^ ~x4 ^ x5 ^ x7)) ^ (x1 & ((x5 & (~x4 ^ x6)) ^ x4 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ ~x4 ^ x5 ^ x7)) ^ (x5 & ~x0 & (~x1 ^ x3) & (x4 ^ x6))) | ((x0 & ((x2 & ((x4 & ((x6 & ~x1) ^ ~x3 ^ x5 ^ x7)) ^ (x6 & (~x3 ^ x5)) ^ (~x1 & ~x7))) ^ (x3 & ((x1 & ((~(x4 & x5)) ^ x6 ^ x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & ((x6 & ~x5) ^ ~x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & x5 & ~x2 & (x4 ^ x6))) | ((x0 & ((x1 & ((x2 & ((x3 & (x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (x5 & (~x3 ^ x4 ^ x6 ^ x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x2 & ((x3 & (~x4 ^ x7)) ^ (x5 & (~x4 ^ x6)) ^ ~x7)) ^ (x5 & ((x3 & (~x4 ^ x6)) ^ ~x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x1 & ((x5 & ((x2 & (~x4 ^ x6 ^ x7)) ^ (~x3 & (~x4 ^ x6)))) ^ (x2 & ((x3 & (~x6 ^ x7)) ^ (x4 & x6))) ^ (x4 & x6 & ~x3))) ^ (x4 & ~x7 & (~x2 ^ x3)) ^ (x5 & ~x3 & (~x2 ^ x7))) | ((x0 & ((x1 & ((x2 & ((x3 & (x4 ^ x5 ^ x6)) ^ (x4 & ~x6) ^ x5)) ^ (x3 & (~x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (~x3 & ((x2 & (x4 ^ x5 ^ x6)) ^ (x6 & ~x4) ^ ~x5 ^ x7)))) ^ (x4 & ((x1 & ((x3 & (~x2 ^ x6 ^ x7)) ^ (x2 & ~x6) ^ ~x7)) ^ (x2 & ~x3 & ~x6) ^ (~x3 & ~x7))) ^ (x5 & ~x1 & ~x2 & ~x3) ^ (x1 & x3 & x6 & ~x2)) | ((x0 & ((x1 & ((x3 & (~((x2 & ~x7) ^ (x4 & ~x5)))) ^ (x4 & (~x2 ^ x6)) ^ ~x5 ^ x6 ^ (x2 & x7))) ^ (x2 & ((x6 & (~x3 ^ x5 ^ x7)) ^ (x4 & (x3 ^ x7)) ^ (~(x5 & x7)))) ^ (x3 & ((~(x4 & x5)) ^ x7)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x3 & ((x2 & ((x4 & (~x5 ^ x6)) ^ (x1 & (x5 ^ x7)) ^ ~x5 ^ x6)) ^ (x1 & ((x6 & ~x7) ^ ~x4 ^ x5)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x2 & ((x5 & ~x1 & ~x7) ^ (~x6 & ~x7))) ^ (x4 & ((x1 & ~x7) ^ (x5 & ~x6) ^ ~x7)) ^ (x5 & x6 & ~x1)) | ((x5 & ((x1 & ((x0 & ((x2 & ~x3) ^ ~x3 ^ x6)) ^ (~x3 & (~x2 ^ x6)))) ^ (x4 & ~x3 & (~x0 ^ x2)) ^ (x6 & ((x0 & ~x2) ^ ~x3)))) ^ (x0 & x3 & ((x1 & (x2 ^ x4 ^ x6 ^ x7)) ^ ((~x4 ^ x7) & (x2 ^ x6))))) | ((x2 & ((x6 & ((x0 & ((x1 & ~x3) ^ ~x4)) ^ (x5 & (~x1 ^ x4)) ^ (x3 & ~x4))) ^ (x1 & ((x0 & ~x4) ^ (x3 & ~x4) ^ x5)) ^ (~x4 & (x0 ^ x3 ^ x5)))) ^ (x0 & ((x1 & ((x4 & (~(x5 & ~x3))) ^ (~(x6 & ~x3)))) ^ (~x4 & ~x6))) ^ (x3 & ~x4 & (~x1 ^ x6)) ^ (x5 & ~x6 & (~x1 ^ x4))) | (~(~x5 | x0 | x2 | x3 | x4)) | ((x0 & ((x2 & ((x1 & ((x3 & (~x6 ^ x7)) ^ (x4 & ~x5) ^ ~x6)) ^ (x3 & (~x5 ^ x6 ^ x7)) ^ (x5 & ~x6) ^ ~x4)) ^ (x6 & ((x1 & (~x3 ^ x5)) ^ (x5 & ~x3) ^ ~x4)) ^ (x1 & (~(x4 & (~(x3 & x5))))) ^ (x5 & ~x3) ^ ~x4)) ^ (x3 & ((x2 & ((x1 & ~x6) ^ ~x5 ^ x6 ^ (x4 & x7))) ^ (x4 & (~x1 ^ x6)) ^ (x5 & ~x6) ^ ~x1 ^ x6)) ^ (x5 & ((x4 & ((x1 & ~x2) ^ ~x2 ^ x6)) ^ (x1 & ~x2) ^ (x2 & x6))) ^ (x1 & x2 & x6 & ~x4)) | (~(~x1 | ~x5 | (x2 ^ x0) | (x4 ^ x0) | x3)) | ((x2 & ((x0 & ((x4 & ((x1 & ~x5) ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x5 & (~x3 ^ x6 ^ x7)) ^ (x6 & ((~(x1 & x3)) ^ x7)) ^ (x1 & x3 & x7))) ^ (x1 & ((x5 & (x3 ^ x6 ^ x7)) ^ (x6 & (x3 ^ x7)) ^ ~x4 ^ x7)) ^ (x4 & ((x3 & ~x5) ^ ~x5 ^ x6)) ^ (x5 & (~x6 ^ x7)) ^ (~x6 & ~x7))) ^ (x0 & ((x6 & ((x3 & (~x1 ^ x4 ^ x5)) ^ (x7 & ~x1) ^ x4 ^ x5)) ^ (x5 & ~x4 & (x1 ^ x3)))) ^ (((x4 & ~x7) ^ (x5 & ~x3)) & (x1 ^ x6))) | (~((~(x4 ^ x1 ^ x0)) | ((x0 & (~(x1 & ~x2))) ^ (x3 & ~x5) ^ (~(x1 & x2)) ^ x5) | (x6 ^ x3 ^ x2) | (x3 & ~x1) | (x0 & x3) | (x2 & x3) | (~x1 & (~x0 ^ x5)) | (x0 & (x1 ^ x5)) | (x2 & (~x0 ^ x1 ^ x5)))) | (~(~x5 | x0 | x1 | x3 | (x6 ^ x2))) | (x1 & x5 & ~x0 & ~x2 & (x4 ^ x6)) | (x0 & x1 & ((x4 & ~x3 & (x5 ^ x6)) ^ (x2 & x6 & ~x3))) | (x5 & ~x3 & (~x0 ^ x2) & (x4 ^ x6)) | (x0 & x2 & x6 & ~x3 & ~x4) | (x1 & ((x6 & ((x3 & ~x2 & (~x0 ^ x4)) ^ (x0 & x4 & ~x2))) ^ (x0 & x4 & x5 & ~x3))) | ((x0 & ((x1 & ((x2 & ((x3 & (~x4 ^ x5)) ^ (x4 & (x5 ^ x6)) ^ x5)) ^ (x6 & (~x3 ^ x7)) ^ (~((x4 & ~x5) ^ (x7 & ~x3))))) ^ (x6 & ((x4 & (~x2 ^ x3)) ^ ~x2 ^ x3 ^ x5 ^ x7)) ^ (x5 & ((x2 & (x3 ^ x4 ^ x7)) ^ (x4 & ~x3))) ^ (x7 & (~(x3 & ~x2))) ^ ~x4)) ^ (x2 & ((x1 & ((x6 & (~x4 ^ x7)) ^ (x5 & ~x7) ^ ~x4 ^ x7)) ^ (x6 & (~x3 ^ x4 ^ x7)) ^ (x4 & ~x5) ^ (x7 & ~x5) ^ ~x3)) ^ (x5 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (x3 & ~x4) ^ (x6 & (x4 ^ x7)) ^ ~x7)) ^ (x3 & ~x6 & (x4 ^ x7))) | (x0 & x1 & x2 & x7 & (x3 ^ x5))\r\n"; var printHelp = () => { From a53f7d23c993cb41736faa75fec8a9fa587c98bf Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Thu, 19 Jun 2025 19:16:12 -0400 Subject: [PATCH 13/15] Factor by most common literal --- Mba.Simplifier/Minimization/AnfMinimizer.cs | 2 + .../Minimization/Factoring/BoolCtx.cs | 51 ++++++-- .../Minimization/Factoring/BoolExpr.cs | 2 + .../Minimization/Factoring/BoolMinimizer.cs | 118 +++++++++++++++++- Simplifier/Program.cs | 3 +- 5 files changed, 162 insertions(+), 14 deletions(-) diff --git a/Mba.Simplifier/Minimization/AnfMinimizer.cs b/Mba.Simplifier/Minimization/AnfMinimizer.cs index 15d4d21..7e048ea 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -376,6 +376,8 @@ private static AstIdx Factor2(AstCtx ctx, IReadOnlyList variables, AnfPo Console.WriteLine(id.ToString()); + new BoolMinimizer(boolCtx).Minimize(id); + // Remove the constant term if it exists bool hasOnes = poly.Monoms.Remove(uint.MaxValue); diff --git a/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs b/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs index a771062..edf60ab 100644 --- a/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs +++ b/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs @@ -1,5 +1,7 @@ -using System; +using Mba.Ast; +using System; using System.Collections.Generic; +using System.Diagnostics; using System.Linq; using System.Text; using System.Threading.Tasks; @@ -17,6 +19,8 @@ public class BoolCtx // Reduce allocations by reusing the same empty list across all childless nodes. private readonly List emptyList = new(); + public int VarCount { get; private set; } = 0; + // Expr id of the constant 1 public ExprId Constant1Id { get; set; } @@ -27,6 +31,7 @@ public BoolCtx() public ExprId Var(uint varIdx) { + VarCount = Math.Max(VarCount, (int)varIdx + 1); var vNode = new BoolExpr(ExprKind.Var, emptyList, (uint)varIdx); return AddExpr(vNode); } @@ -42,23 +47,34 @@ public ExprId Constant(uint constant) public ExprId Add(List children) { + var output = new List(); + Hoist(ExprKind.Add, children, output); + children = output; + children = ReduceSumCoefficient(children); - children = Sort(children); + if (children.Count == 1) + return children[0]; - /* - var output = new List(); - ExprId? lastInstance = null; - for(int i = 0; i < children.Count; i++) - { - if (lastInstance == null) - lastInstance = 0; - } - */ + children = Sort(children); var vNode = new BoolExpr(ExprKind.Add, children); return AddExpr(vNode); } + private void Hoist(ExprKind kind, IReadOnlyList children, List output) + { + foreach(var child in children) + { + if (Get(child).Kind != kind) + { + output.Add(child); + continue; + } + + Hoist(kind, Get(child).Children, output); + } + } + private List ReduceSumCoefficient(List children) { @@ -84,6 +100,13 @@ public ExprId Add(ExprId op1, ExprId op2) public ExprId Mul(List children) { + var output = new List(); + Hoist(ExprKind.Mul, children, output); + children = output; + + if (children.Count == 1) + return children[0]; + //children = ReduceMulPower(children); children = Sort(children); /* @@ -187,11 +210,17 @@ public ExprId AddExpr(BoolExpr expr) public BoolExpr Get(ExprId id) => elements[id]; + public ExprKind GetOpcode(ExprId id) + => elements[id].Kind; + public string GetVarName(BoolExpr expr) { return $"x{expr.Data}"; } + public uint GetVarIndex(BoolExpr expr) + => expr.Data; + public uint GetConstValue(BoolExpr expr) { return expr.Data; diff --git a/Mba.Simplifier/Minimization/Factoring/BoolExpr.cs b/Mba.Simplifier/Minimization/Factoring/BoolExpr.cs index 2a49951..60df5ec 100644 --- a/Mba.Simplifier/Minimization/Factoring/BoolExpr.cs +++ b/Mba.Simplifier/Minimization/Factoring/BoolExpr.cs @@ -13,6 +13,8 @@ public struct ExprId { public int Idx; + public BoolExpr Expr => ctx.Get(Idx); + public ExprId(int idx) { Idx = idx; diff --git a/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs b/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs index 564fae3..43132fe 100644 --- a/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs +++ b/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs @@ -1,12 +1,126 @@ -using System; +using Mba.Simplifier.Bindings; +using System; using System.Collections.Generic; +using System.Diagnostics; using System.Linq; using System.Text; using System.Threading.Tasks; namespace Mba.Simplifier.Minimization.Factoring { - internal class BoolMinimizer + public class BoolMinimizer { + private readonly BoolCtx ctx; + + public BoolMinimizer(BoolCtx ctx) + { + this.ctx = ctx; + } + + public void Minimize(ExprId id) + { + var bar = TryFactorByLiteral(id); + Debugger.Break(); + } + + private ExprId TryFactorByLiteral(ExprId id) + { + var node = ctx.Get(id); + if (node.Kind != ExprKind.Add) + return id; + + // Calculate the frequency of each literal + var literalCounts = new int[(int)ctx.VarCount]; + GetLiteralCounts(node.Children, literalCounts); + + // If there is no literal that occurs more than once, there is no factoring to be done. + var bestIdx = GetMostCommonIdx(literalCounts); + if (bestIdx == -1 || literalCounts[bestIdx] <= 1) + return id; + + // Otherwise we have a common literal. + // E.g. if we have ab + ac + c, we want to factor it into a(b+c) + c + var literal = ctx.Var((uint)bestIdx); + var factors = new List(); + var others = new List(); + foreach(var childId in node.Children) + { + var child = ctx.Get(childId); + // If we have a literal, factor it out. + if (child.Kind == ExprKind.Var) + { + if (childId == literal) + factors.Add(ctx.Constant1Id); + else + others.Add(childId); + + continue; + } + + if (child.Kind == ExprKind.Const) + { + others.Add(childId); + continue; + } + + if (child.Kind != ExprKind.Mul) + throw new InvalidOperationException($"Failed to hoist terms!"); + var products = child.Children; + // If we have a multiplication, and the literal is not one of the factors, skip it. + bool containsLiteral = products.Contains(literal); + if (!containsLiteral) + { + others.Add(childId); + continue; + } + + Debug.Assert(products.Count(x => x == literal) == 1); + var withoutLiteral = products.Where(x => x != literal).ToList(); + var mul = ctx.Mul(withoutLiteral); + factors.Add(mul); + } + + + var lhs = ctx.Add(factors); + var part1 = ctx.Mul(literal, TryFactorByLiteral(lhs)); + + var part2 = ctx.Add(others); + part2 = TryFactorByLiteral(part2); + + var result = ctx.Add(part1, part2); + return result; + } + + private void GetLiteralCounts(IReadOnlyList ids, int[] literalCounts) + { + foreach(var id in ids) + { + var node = ctx.Get(id); + if (node.Kind == ExprKind.Var) + { + var varIdx = ctx.GetVarIndex(node); + literalCounts[varIdx] += 1; + } + if (node.Kind == ExprKind.Mul) + GetLiteralCounts(node.Children, literalCounts); + } + } + + private int GetMostCommonIdx(int[] literalCounts) + { + int bestIdx = -1; + for(int i = 0; i < literalCounts.Length; i++) + { + if (bestIdx == -1) + { + bestIdx = i; + continue; + } + + bestIdx = literalCounts[i] > literalCounts[bestIdx] ? i : bestIdx; + } + return bestIdx; + } + } } diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index d3379e6..e341405 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -48,7 +48,8 @@ inputText = "(a^b)|(c^d)"; -//inputText = "a|b|c|d"; + +inputText = "a|b|c|d"; //inputText = "a^b^c"; From 246e87ba86b8821caab3c11762aaa0d20fc6e193 Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Thu, 19 Jun 2025 20:15:34 -0400 Subject: [PATCH 14/15] more pattern matching --- .../Minimization/Factoring/BoolMinimizer.cs | 40 +++++++++++++++++++ Simplifier/Program.cs | 12 ++++++ 2 files changed, 52 insertions(+) diff --git a/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs b/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs index 43132fe..9404417 100644 --- a/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs +++ b/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs @@ -12,6 +12,8 @@ public class BoolMinimizer { private readonly BoolCtx ctx; + private Dictionary costMap = new(); + public BoolMinimizer(BoolCtx ctx) { this.ctx = ctx; @@ -23,9 +25,12 @@ public void Minimize(ExprId id) Debugger.Break(); } + // Try to match a*b + a*c => a*(b+c), considering only the most common literal. private ExprId TryFactorByLiteral(ExprId id) { var node = ctx.Get(id); + if (node.Kind == ExprKind.Mul) + Debugger.Break(); if (node.Kind != ExprKind.Add) return id; @@ -122,5 +127,40 @@ private int GetMostCommonIdx(int[] literalCounts) return bestIdx; } + // We are looking for a*b + a*c, where `a` can now be an arbitrary linear combination. + private ExprId TryFactorBySum(ExprId id) + { + var node = ctx.Get(id); + if(node.Kind != ExprKind.Add) + { + Debugger.Break(); + return id; + } + } + + + private uint GetCost(ExprId id) + { + if (costMap.TryGetValue(id, out var existing)) + return existing; + + uint cost = 1; + var node = ctx.Get(id); + if (node.Kind == ExprKind.Const || node.Kind == ExprKind.Var) + { + cost = 1; + } + + else + { + foreach(var child in node.Children) + { + cost += 1 + GetCost(child); + } + } + + costMap[id] = existing; + return cost; + } } } diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index e341405..a33116f 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -48,9 +48,21 @@ inputText = "(a^b)|(c^d)"; +inputText = "d & a & e ^ (b ^ a ^ c ^ -1) & d ^ e & a ^ e & b ^ e & c ^ (b ^ a) & d & (l & i) ^ d & e & (c ^ b) ^ c & f & g ^ h ^ g & f & (d & c & e) ^ g & f & (b & d & e) ^ g & f & (d & a & e) ^ g & f & (d & a) ^ g & f & (b & d) ^ g & f & (d & c) ^ g & f & (e & a) ^ g & f & (e & b) ^ g & f & (e & c) ^ g & f & a ^ g & f & b ^ d & a & e & h ^ b & d & e & h ^ d & c & e & h ^ c & f & g & h ^ d & a & h ^ b & d & h ^ d & c & h ^ e & a & h ^ d & h ^ i ^ b & d & h & i ^ i & (g & f & (b & d & e)) ^ g & f & (e & c) & h ^ e & h & (c ^ b) ^ h & (g & f & (b & d)) ^ g & f & (d & c) & h ^ g & f & (d & c & e) & i ^ g & f & (d & a) & i ^ i & (g & f & (b & d)) ^ g & f & (e & b) & i ^ g & f & (e & c) & i ^ d & a & e & h & i ^ b & d & e & h & i ^ d & c & e & h & i ^ d & a & e & i ^ b & d & e & i ^ d & a & h & i ^ d & a & i ^ b & d & i ^ d & c & i ^ e & a & i ^ e & b & i ^ d & i ^ i & h ^ (g & f & (e & a) ^ g & f & (e & b)) & h ^ i & h & (e & c) ^ g & f & (d & a & e) & h & l ^ i & h & (g & f & (b & d & e)) ^ g & f & (d & a & e) & h & i ^ (g & f & (d & a & e) ^ g & f & (b & d & e)) & h ^ (g & f & (d & c & e) ^ g & f & (d & a)) & h ^ (g & f & a ^ g & f & b) & h ^ g & f & (d & a) & h & i ^ i & h & (g & f & (b & d)) ^ g & f & (d & c) & h & i ^ g & f & (e & a) & (i & h) ^ g & f & (e & b) & (i & h) ^ i & h & (g & f & (e & c)) ^ l & (g & f & (b & d & e)) ^ g & f & (d & c & e) & l ^ g & f & (d & a) & h & l ^ g & f & (d & c) & h & l ^ g & f & (d & a) & i & l ^ g & f & (e & c) & i & l ^ d & a & e & h & i & l ^ b & d & e & h & i & l ^ d & c & e & h & i & l ^ g & f & (d & a) & l ^ l & (g & f & (b & d)) ^ g & f & (d & c) & l ^ g & f & (e & a) & l ^ g & f & (e & b) & l ^ g & f & (e & c) & l ^ d & a & e & h & l ^ b & d & e & h & l ^ d & c & e & h & l ^ g & f & a & h & l ^ d & a & e & i & l ^ b & d & e & i & l ^ b & d & h & i & l ^ b & d & e & l ^ d & c & e & l ^ (g & f & a ^ g & f & b) & l ^ (c & f & g ^ d & a & h) & l ^ b & d & h & l ^ d & c & h & l ^ e & a & h & l ^ l & (e & h & (c ^ b)) ^ e & a & i & l ^ (b & d ^ (e & a ^ d & c)) & l ^ e & b & l ^ e & c & l ^ d & h & l ^ d & i & l ^ i & h & l ^ d & l ^ (i ^ h) & l ^ (b ^ a) & e & (i & h) ^ l & i & (g & f & (e & a) & h) ^ ((b ^ a ^ c) & e & (g & f) & (d & h & i) ^ -1) & l ^ l & i & (g & f & (b & d) ^ g & f & (d & c)) ^ l & h & (g & f & (e & c)) ^ d & (i & h & c) ^ g & f & (i & h & c) ^ d & c & h & (l & i) ^ (e & b & i ^ d & a) & l ^ (d & h ^ e & c ^ (g & f & b ^ c & f & g)) & i ^ (g & f & (d & c & e) & i ^ g & f & (d & a & e)) & l ^ l & i & (d & c & e) ^ l & i & (g & f & a) ^ l & i & (g & f & b) ^ l & i & (e & c) ^ l & i & (d & h) ^ l & h & (g & f & (b & d & e)) ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e)) & i ^ (g & f & a ^ g & f & b) & h & i ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e) & i) & l ^ l & i & (g & f & (b & d & e)) ^ g & f & (d & a) & h & i & l ^ l & i & (h & (g & f & (b & d))) ^ g & f & (d & c) & h & i & l ^ (g & f & (e & b) ^ g & f & (e & c)) & h & (l & i) ^ l & h & (g & f & (b & d)) ^ l & h & (g & f & (e & a) ^ g & f & (e & b)) ^ l & i & (g & f & (e & a) ^ g & f & (e & b) ^ g & f & a & h) ^ (g & f & b ^ c & f & g) & h & l ^ l & i & (c & f & g ^ d & a & h) ^ l & i & ((g & f & b ^ c & f & g) & h) ^ (b ^ a) & e & (i & h) & l ^ d & (l & i & c) ^ (g & f & (e & a) ^ d & c & e ^ g & f & (d & c) ^ g & f & a) & i ^ (i & h & (e & c) ^ d & a & e) & l"; + + inputText = "a|b|c|d"; +inputText = "(a^b)|(c^d)"; + +inputText = "x0|x1|x2|x3^(x4|x5|x6&x7)"; + +inputText = "d & a & e ^ (b ^ a ^ c ^ -1) & d ^ e & a ^ e & b ^ e & c ^ (b ^ a) & d & (l & i) ^ d & e & (c ^ b) ^ c & f & g ^ h ^ g & f & (d & c & e) ^ g & f & (b & d & e) ^ g & f & (d & a & e) ^ g & f & (d & a) ^ g & f & (b & d) ^ g & f & (d & c) ^ g & f & (e & a) ^ g & f & (e & b) ^ g & f & (e & c) ^ g & f & a ^ g & f & b ^ d & a & e & h ^ b & d & e & h ^ d & c & e & h ^ c & f & g & h ^ d & a & h ^ b & d & h ^ d & c & h ^ e & a & h ^ d & h ^ i ^ b & d & h & i ^ i & (g & f & (b & d & e)) ^ g & f & (e & c) & h ^ e & h & (c ^ b) ^ h & (g & f & (b & d)) ^ g & f & (d & c) & h ^ g & f & (d & c & e) & i ^ g & f & (d & a) & i ^ i & (g & f & (b & d)) ^ g & f & (e & b) & i ^ g & f & (e & c) & i ^ d & a & e & h & i ^ b & d & e & h & i ^ d & c & e & h & i ^ d & a & e & i ^ b & d & e & i ^ d & a & h & i ^ d & a & i ^ b & d & i ^ d & c & i ^ e & a & i ^ e & b & i ^ d & i ^ i & h ^ (g & f & (e & a) ^ g & f & (e & b)) & h ^ i & h & (e & c) ^ g & f & (d & a & e) & h & l ^ i & h & (g & f & (b & d & e)) ^ g & f & (d & a & e) & h & i ^ (g & f & (d & a & e) ^ g & f & (b & d & e)) & h ^ (g & f & (d & c & e) ^ g & f & (d & a)) & h ^ (g & f & a ^ g & f & b) & h ^ g & f & (d & a) & h & i ^ i & h & (g & f & (b & d)) ^ g & f & (d & c) & h & i ^ g & f & (e & a) & (i & h) ^ g & f & (e & b) & (i & h) ^ i & h & (g & f & (e & c)) ^ l & (g & f & (b & d & e)) ^ g & f & (d & c & e) & l ^ g & f & (d & a) & h & l ^ g & f & (d & c) & h & l ^ g & f & (d & a) & i & l ^ g & f & (e & c) & i & l ^ d & a & e & h & i & l ^ b & d & e & h & i & l ^ d & c & e & h & i & l ^ g & f & (d & a) & l ^ l & (g & f & (b & d)) ^ g & f & (d & c) & l ^ g & f & (e & a) & l ^ g & f & (e & b) & l ^ g & f & (e & c) & l ^ d & a & e & h & l ^ b & d & e & h & l ^ d & c & e & h & l ^ g & f & a & h & l ^ d & a & e & i & l ^ b & d & e & i & l ^ b & d & h & i & l ^ b & d & e & l ^ d & c & e & l ^ (g & f & a ^ g & f & b) & l ^ (c & f & g ^ d & a & h) & l ^ b & d & h & l ^ d & c & h & l ^ e & a & h & l ^ l & (e & h & (c ^ b)) ^ e & a & i & l ^ (b & d ^ (e & a ^ d & c)) & l ^ e & b & l ^ e & c & l ^ d & h & l ^ d & i & l ^ i & h & l ^ d & l ^ (i ^ h) & l ^ (b ^ a) & e & (i & h) ^ l & i & (g & f & (e & a) & h) ^ ((b ^ a ^ c) & e & (g & f) & (d & h & i) ^ -1) & l ^ l & i & (g & f & (b & d) ^ g & f & (d & c)) ^ l & h & (g & f & (e & c)) ^ d & (i & h & c) ^ g & f & (i & h & c) ^ d & c & h & (l & i) ^ (e & b & i ^ d & a) & l ^ (d & h ^ e & c ^ (g & f & b ^ c & f & g)) & i ^ (g & f & (d & c & e) & i ^ g & f & (d & a & e)) & l ^ l & i & (d & c & e) ^ l & i & (g & f & a) ^ l & i & (g & f & b) ^ l & i & (e & c) ^ l & i & (d & h) ^ l & h & (g & f & (b & d & e)) ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e)) & i ^ (g & f & a ^ g & f & b) & h & i ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e) & i) & l ^ l & i & (g & f & (b & d & e)) ^ g & f & (d & a) & h & i & l ^ l & i & (h & (g & f & (b & d))) ^ g & f & (d & c) & h & i & l ^ (g & f & (e & b) ^ g & f & (e & c)) & h & (l & i) ^ l & h & (g & f & (b & d)) ^ l & h & (g & f & (e & a) ^ g & f & (e & b)) ^ l & i & (g & f & (e & a) ^ g & f & (e & b) ^ g & f & a & h) ^ (g & f & b ^ c & f & g) & h & l ^ l & i & (c & f & g ^ d & a & h) ^ l & i & ((g & f & b ^ c & f & g) & h) ^ (b ^ a) & e & (i & h) & l ^ d & (l & i & c) ^ (g & f & (e & a) ^ d & c & e ^ g & f & (d & c) ^ g & f & a) & i ^ (i & h & (e & c) ^ d & a & e) & l"; + + +//inputText = "(x0^x1^x2^x3)&(x3|(x4|x5&x6))|x7|x8|x9"; + //inputText = "a^b^c"; //inputText = "(~((~x0 & ~x1) | ((x0 & ~x3) ^ ~x2 ^ x5) | ((x0 & ~x4) ^ (~x1 & ~x2)) | (x2 & ~x0) | (~x1 & (x2 ^ x4)) | (x2 & ~x4) | ((x3 & (~x0 ^ x1)) ^ ~x0 ^ x2 ^ x4 ^ x6))) | ((x2 & ((x0 & ((x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x3 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x5 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x5 & ~x0 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (~x3 & ~x4)))) | ((x0 & ((x1 & ((x4 & ((x2 & (x3 ^ x5 ^ x6)) ^ ~x7)) ^ (x3 & ((x5 & ~x2) ^ x6)) ^ (x6 & ~x5) ^ ~x7)) ^ (x6 & ((x2 & (~x3 ^ x4 ^ x5)) ^ (~x3 & ~x4))) ^ (x4 & ((~(x2 & x3)) ^ x5 ^ x7)) ^ (x5 & ~x2) ^ ~x7)) ^ (x5 & ~x2 & ((x4 & (~x1 ^ x3)) ^ ~x3 ^ (x1 & x6)))) | ((x0 & ((x5 & ((x1 & ((x4 & (~x2 ^ x3)) ^ x6 ^ x7)) ^ (x3 & (~x2 ^ x4 ^ x6)) ^ (~(x2 & x4)) ^ x6 ^ x7)) ^ (x2 & ((x1 & ((x3 & (~x4 ^ x6)) ^ (~(x4 & x6)))) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x7 & (~x1 ^ x3 ^ x4)) ^ (x4 & (x1 ^ x3)))) ^ (x1 & ((x2 & ((x3 & (x4 ^ x6 ^ x7)) ^ (x4 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & ((x4 & ~x3) ^ x6 ^ x7)) ^ (x3 & (x4 ^ x7)))) ^ (x3 & ((x4 & ((x2 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & (~x2 ^ x6)))) ^ (x5 & (~x2 ^ x6 ^ (x4 & x7))) ^ (x2 & x4 & (x6 ^ x7))) | (~(((x0 & ~x2) ^ ~x3 ^ x5) | x1 | (x4 ^ x2) | ((x2 & ~x0) ^ x6))) | ((x2 & ((x4 & ((x1 & (x0 ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x0 & (~x5 ^ x6)) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x0 & ((x1 & ((~(x3 & x6)) ^ x7)) ^ (~(x5 & x6)) ^ x7)) ^ (x1 & x6 & (x3 ^ x5)))) ^ (x1 & ((x6 & ((x0 & (x3 ^ x4 ^ x5)) ^ (x3 & ~x4) ^ x5)) ^ (x4 & x5 & (~(x0 & x3)))))) | ((x2 & ((x0 & ((x1 & ((x3 & (~x5 ^ x7)) ^ (x4 & ~x5) ^ x5 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ (x5 & ~x3) ^ ~x4 ^ x7)) ^ (x3 & ((x6 & (~x1 ^ x4 ^ x7)) ^ (x1 & (x4 ^ x5)) ^ ~x4 ^ x5 ^ x7)) ^ (x1 & ((x5 & (~x4 ^ x6)) ^ x4 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ ~x4 ^ x5 ^ x7)) ^ (x5 & ~x0 & (~x1 ^ x3) & (x4 ^ x6))) | ((x0 & ((x2 & ((x4 & ((x6 & ~x1) ^ ~x3 ^ x5 ^ x7)) ^ (x6 & (~x3 ^ x5)) ^ (~x1 & ~x7))) ^ (x3 & ((x1 & ((~(x4 & x5)) ^ x6 ^ x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & ((x6 & ~x5) ^ ~x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & x5 & ~x2 & (x4 ^ x6))) | ((x0 & ((x1 & ((x2 & ((x3 & (x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (x5 & (~x3 ^ x4 ^ x6 ^ x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x2 & ((x3 & (~x4 ^ x7)) ^ (x5 & (~x4 ^ x6)) ^ ~x7)) ^ (x5 & ((x3 & (~x4 ^ x6)) ^ ~x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x1 & ((x5 & ((x2 & (~x4 ^ x6 ^ x7)) ^ (~x3 & (~x4 ^ x6)))) ^ (x2 & ((x3 & (~x6 ^ x7)) ^ (x4 & x6))) ^ (x4 & x6 & ~x3))) ^ (x4 & ~x7 & (~x2 ^ x3)) ^ (x5 & ~x3 & (~x2 ^ x7))) | ((x0 & ((x1 & ((x2 & ((x3 & (x4 ^ x5 ^ x6)) ^ (x4 & ~x6) ^ x5)) ^ (x3 & (~x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (~x3 & ((x2 & (x4 ^ x5 ^ x6)) ^ (x6 & ~x4) ^ ~x5 ^ x7)))) ^ (x4 & ((x1 & ((x3 & (~x2 ^ x6 ^ x7)) ^ (x2 & ~x6) ^ ~x7)) ^ (x2 & ~x3 & ~x6) ^ (~x3 & ~x7))) ^ (x5 & ~x1 & ~x2 & ~x3) ^ (x1 & x3 & x6 & ~x2)) | ((x0 & ((x1 & ((x3 & (~((x2 & ~x7) ^ (x4 & ~x5)))) ^ (x4 & (~x2 ^ x6)) ^ ~x5 ^ x6 ^ (x2 & x7))) ^ (x2 & ((x6 & (~x3 ^ x5 ^ x7)) ^ (x4 & (x3 ^ x7)) ^ (~(x5 & x7)))) ^ (x3 & ((~(x4 & x5)) ^ x7)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x3 & ((x2 & ((x4 & (~x5 ^ x6)) ^ (x1 & (x5 ^ x7)) ^ ~x5 ^ x6)) ^ (x1 & ((x6 & ~x7) ^ ~x4 ^ x5)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x2 & ((x5 & ~x1 & ~x7) ^ (~x6 & ~x7))) ^ (x4 & ((x1 & ~x7) ^ (x5 & ~x6) ^ ~x7)) ^ (x5 & x6 & ~x1)) | ((x5 & ((x1 & ((x0 & ((x2 & ~x3) ^ ~x3 ^ x6)) ^ (~x3 & (~x2 ^ x6)))) ^ (x4 & ~x3 & (~x0 ^ x2)) ^ (x6 & ((x0 & ~x2) ^ ~x3)))) ^ (x0 & x3 & ((x1 & (x2 ^ x4 ^ x6 ^ x7)) ^ ((~x4 ^ x7) & (x2 ^ x6))))) | ((x2 & ((x6 & ((x0 & ((x1 & ~x3) ^ ~x4)) ^ (x5 & (~x1 ^ x4)) ^ (x3 & ~x4))) ^ (x1 & ((x0 & ~x4) ^ (x3 & ~x4) ^ x5)) ^ (~x4 & (x0 ^ x3 ^ x5)))) ^ (x0 & ((x1 & ((x4 & (~(x5 & ~x3))) ^ (~(x6 & ~x3)))) ^ (~x4 & ~x6))) ^ (x3 & ~x4 & (~x1 ^ x6)) ^ (x5 & ~x6 & (~x1 ^ x4))) | (~(~x5 | x0 | x2 | x3 | x4)) | ((x0 & ((x2 & ((x1 & ((x3 & (~x6 ^ x7)) ^ (x4 & ~x5) ^ ~x6)) ^ (x3 & (~x5 ^ x6 ^ x7)) ^ (x5 & ~x6) ^ ~x4)) ^ (x6 & ((x1 & (~x3 ^ x5)) ^ (x5 & ~x3) ^ ~x4)) ^ (x1 & (~(x4 & (~(x3 & x5))))) ^ (x5 & ~x3) ^ ~x4)) ^ (x3 & ((x2 & ((x1 & ~x6) ^ ~x5 ^ x6 ^ (x4 & x7))) ^ (x4 & (~x1 ^ x6)) ^ (x5 & ~x6) ^ ~x1 ^ x6)) ^ (x5 & ((x4 & ((x1 & ~x2) ^ ~x2 ^ x6)) ^ (x1 & ~x2) ^ (x2 & x6))) ^ (x1 & x2 & x6 & ~x4)) | (~(~x1 | ~x5 | (x2 ^ x0) | (x4 ^ x0) | x3)) | ((x2 & ((x0 & ((x4 & ((x1 & ~x5) ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x5 & (~x3 ^ x6 ^ x7)) ^ (x6 & ((~(x1 & x3)) ^ x7)) ^ (x1 & x3 & x7))) ^ (x1 & ((x5 & (x3 ^ x6 ^ x7)) ^ (x6 & (x3 ^ x7)) ^ ~x4 ^ x7)) ^ (x4 & ((x3 & ~x5) ^ ~x5 ^ x6)) ^ (x5 & (~x6 ^ x7)) ^ (~x6 & ~x7))) ^ (x0 & ((x6 & ((x3 & (~x1 ^ x4 ^ x5)) ^ (x7 & ~x1) ^ x4 ^ x5)) ^ (x5 & ~x4 & (x1 ^ x3)))) ^ (((x4 & ~x7) ^ (x5 & ~x3)) & (x1 ^ x6))) | (~((~(x4 ^ x1 ^ x0)) | ((x0 & (~(x1 & ~x2))) ^ (x3 & ~x5) ^ (~(x1 & x2)) ^ x5) | (x6 ^ x3 ^ x2) | (x3 & ~x1) | (x0 & x3) | (x2 & x3) | (~x1 & (~x0 ^ x5)) | (x0 & (x1 ^ x5)) | (x2 & (~x0 ^ x1 ^ x5)))) | (~(~x5 | x0 | x1 | x3 | (x6 ^ x2))) | (x1 & x5 & ~x0 & ~x2 & (x4 ^ x6)) | (x0 & x1 & ((x4 & ~x3 & (x5 ^ x6)) ^ (x2 & x6 & ~x3))) | (x5 & ~x3 & (~x0 ^ x2) & (x4 ^ x6)) | (x0 & x2 & x6 & ~x3 & ~x4) | (x1 & ((x6 & ((x3 & ~x2 & (~x0 ^ x4)) ^ (x0 & x4 & ~x2))) ^ (x0 & x4 & x5 & ~x3))) | ((x0 & ((x1 & ((x2 & ((x3 & (~x4 ^ x5)) ^ (x4 & (x5 ^ x6)) ^ x5)) ^ (x6 & (~x3 ^ x7)) ^ (~((x4 & ~x5) ^ (x7 & ~x3))))) ^ (x6 & ((x4 & (~x2 ^ x3)) ^ ~x2 ^ x3 ^ x5 ^ x7)) ^ (x5 & ((x2 & (x3 ^ x4 ^ x7)) ^ (x4 & ~x3))) ^ (x7 & (~(x3 & ~x2))) ^ ~x4)) ^ (x2 & ((x1 & ((x6 & (~x4 ^ x7)) ^ (x5 & ~x7) ^ ~x4 ^ x7)) ^ (x6 & (~x3 ^ x4 ^ x7)) ^ (x4 & ~x5) ^ (x7 & ~x5) ^ ~x3)) ^ (x5 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (x3 & ~x4) ^ (x6 & (x4 ^ x7)) ^ ~x7)) ^ (x3 & ~x6 & (x4 ^ x7))) | (x0 & x1 & x2 & x7 & (x3 ^ x5))\r\n"; From cfca512cba5a79a785e1b01b8a06d7c6fa6590e2 Mon Sep 17 00:00:00 2001 From: Colton1skees Date: Thu, 19 Jun 2025 22:08:20 -0400 Subject: [PATCH 15/15] Absolutely terrible implementation of new pattern.. but it gives great results --- .../Minimization/Factoring/BoolCtx.cs | 2 +- .../Minimization/Factoring/BoolMinimizer.cs | 116 ++++++++++++++++++ Simplifier/Program.cs | 10 +- 3 files changed, 125 insertions(+), 3 deletions(-) diff --git a/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs b/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs index edf60ab..9158c77 100644 --- a/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs +++ b/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs @@ -78,7 +78,7 @@ private void Hoist(ExprKind kind, IReadOnlyList children, List o private List ReduceSumCoefficient(List children) { - return children; + //return children; var output = new List(); var grouped = children.GroupBy(x => x); diff --git a/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs b/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs index 9404417..2b51d54 100644 --- a/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs +++ b/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs @@ -22,6 +22,16 @@ public BoolMinimizer(BoolCtx ctx) public void Minimize(ExprId id) { var bar = TryFactorByLiteral(id); + + var bar2 = TryFactorByExpandedSum(bar); + + ExprId res = bar2; + for(int i = 0; i < 10; i++) + { + res = TryFactorByLiteral(res); + res = TryFactorByExpandedSum(res); + } + Debugger.Break(); } @@ -133,9 +143,115 @@ private ExprId TryFactorBySum(ExprId id) var node = ctx.Get(id); if(node.Kind != ExprKind.Add) { + foreach (var c in node.Children) + TryFactorBySum(c); Debugger.Break(); return id; } + + Dictionary countMap = new(); + foreach(var childId in node.Children) + { + var child = ctx.Get(childId); + if (child.Kind == ExprKind.Mul) + { + foreach (var factor in child.Children) + { + countMap.TryAdd(factor, 0); + countMap[factor] += 1; + } + } + } + + // If there are no factors with more than one occurrence, there is no factoring to do. + if (!countMap.Any(x => x.Value > 1)) + return id; + + + foreach (var c in node.Children) + TryFactorBySum(c); + + return id; + } + + // We are looking for a*b + a, where a is some arbitrary linear combination + // E.g. x1*(x2 + 1) + x2 + 1 + private ExprId TryFactorByExpandedSum(ExprId id) + { + var node = ctx.Get(id); + if (node.Kind == ExprKind.Const || node.Kind == ExprKind.Var) + return id; + if(node.Kind == ExprKind.Mul) + { + return ctx.Mul(node.Children.Select(x => TryFactorByExpandedSum(x)).ToList()); + } + + + var currTerms = node.Children.ToList(); + + bool changed = true; + + start: + while (changed) + { + changed = false; + foreach (var childId in currTerms.ToList()) + { + var child = ctx.Get(childId); + if (child.Kind != ExprKind.Mul) + continue; + + // We have a multiplication of N asts, e.g. (a+b+c)*(b+c) + // Enumerate through the factors of the multiplication + foreach (var factorId in child.Children) + { + var factor = ctx.Get(factorId); + if (factor.Kind != ExprKind.Add) + continue; + + bool found = true; + foreach (var term in factor.Children) + { + if (!currTerms.Contains(term)) + { + found = false; + break; + } + } + + if (!found) + continue; + + // Remove the linear combination from the terms + currTerms = currTerms.Where(x => !factor.Children.Contains(x)).ToList(); + // Remove the product from the list of terms, we need to recompute it + currTerms = currTerms.Where(x => x != childId).ToList(); + + + var nnew = ctx.Mul(child.Children.Where(x => x != factorId).ToList()); + nnew = ctx.Add(nnew, ctx.Constant1Id); + nnew = ctx.Mul(nnew, factorId); + + currTerms.Add(nnew); + + + changed = true; + //Debugger.Break(); + goto start; + Debugger.Break(); + + } + } + } + + currTerms = currTerms.Select(x => TryFactorByExpandedSum(x)).ToList(); + + var res = ctx.Add(currTerms); + + //foreach (var c in node.Children) + // TryFactorByExpandedSum(c); + + return res; } diff --git a/Simplifier/Program.cs b/Simplifier/Program.cs index a33116f..a75bc10 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -56,17 +56,23 @@ inputText = "(a^b)|(c^d)"; -inputText = "x0|x1|x2|x3^(x4|x5|x6&x7)"; +inputText = "(a|b|c)^d"; -inputText = "d & a & e ^ (b ^ a ^ c ^ -1) & d ^ e & a ^ e & b ^ e & c ^ (b ^ a) & d & (l & i) ^ d & e & (c ^ b) ^ c & f & g ^ h ^ g & f & (d & c & e) ^ g & f & (b & d & e) ^ g & f & (d & a & e) ^ g & f & (d & a) ^ g & f & (b & d) ^ g & f & (d & c) ^ g & f & (e & a) ^ g & f & (e & b) ^ g & f & (e & c) ^ g & f & a ^ g & f & b ^ d & a & e & h ^ b & d & e & h ^ d & c & e & h ^ c & f & g & h ^ d & a & h ^ b & d & h ^ d & c & h ^ e & a & h ^ d & h ^ i ^ b & d & h & i ^ i & (g & f & (b & d & e)) ^ g & f & (e & c) & h ^ e & h & (c ^ b) ^ h & (g & f & (b & d)) ^ g & f & (d & c) & h ^ g & f & (d & c & e) & i ^ g & f & (d & a) & i ^ i & (g & f & (b & d)) ^ g & f & (e & b) & i ^ g & f & (e & c) & i ^ d & a & e & h & i ^ b & d & e & h & i ^ d & c & e & h & i ^ d & a & e & i ^ b & d & e & i ^ d & a & h & i ^ d & a & i ^ b & d & i ^ d & c & i ^ e & a & i ^ e & b & i ^ d & i ^ i & h ^ (g & f & (e & a) ^ g & f & (e & b)) & h ^ i & h & (e & c) ^ g & f & (d & a & e) & h & l ^ i & h & (g & f & (b & d & e)) ^ g & f & (d & a & e) & h & i ^ (g & f & (d & a & e) ^ g & f & (b & d & e)) & h ^ (g & f & (d & c & e) ^ g & f & (d & a)) & h ^ (g & f & a ^ g & f & b) & h ^ g & f & (d & a) & h & i ^ i & h & (g & f & (b & d)) ^ g & f & (d & c) & h & i ^ g & f & (e & a) & (i & h) ^ g & f & (e & b) & (i & h) ^ i & h & (g & f & (e & c)) ^ l & (g & f & (b & d & e)) ^ g & f & (d & c & e) & l ^ g & f & (d & a) & h & l ^ g & f & (d & c) & h & l ^ g & f & (d & a) & i & l ^ g & f & (e & c) & i & l ^ d & a & e & h & i & l ^ b & d & e & h & i & l ^ d & c & e & h & i & l ^ g & f & (d & a) & l ^ l & (g & f & (b & d)) ^ g & f & (d & c) & l ^ g & f & (e & a) & l ^ g & f & (e & b) & l ^ g & f & (e & c) & l ^ d & a & e & h & l ^ b & d & e & h & l ^ d & c & e & h & l ^ g & f & a & h & l ^ d & a & e & i & l ^ b & d & e & i & l ^ b & d & h & i & l ^ b & d & e & l ^ d & c & e & l ^ (g & f & a ^ g & f & b) & l ^ (c & f & g ^ d & a & h) & l ^ b & d & h & l ^ d & c & h & l ^ e & a & h & l ^ l & (e & h & (c ^ b)) ^ e & a & i & l ^ (b & d ^ (e & a ^ d & c)) & l ^ e & b & l ^ e & c & l ^ d & h & l ^ d & i & l ^ i & h & l ^ d & l ^ (i ^ h) & l ^ (b ^ a) & e & (i & h) ^ l & i & (g & f & (e & a) & h) ^ ((b ^ a ^ c) & e & (g & f) & (d & h & i) ^ -1) & l ^ l & i & (g & f & (b & d) ^ g & f & (d & c)) ^ l & h & (g & f & (e & c)) ^ d & (i & h & c) ^ g & f & (i & h & c) ^ d & c & h & (l & i) ^ (e & b & i ^ d & a) & l ^ (d & h ^ e & c ^ (g & f & b ^ c & f & g)) & i ^ (g & f & (d & c & e) & i ^ g & f & (d & a & e)) & l ^ l & i & (d & c & e) ^ l & i & (g & f & a) ^ l & i & (g & f & b) ^ l & i & (e & c) ^ l & i & (d & h) ^ l & h & (g & f & (b & d & e)) ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e)) & i ^ (g & f & a ^ g & f & b) & h & i ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e) & i) & l ^ l & i & (g & f & (b & d & e)) ^ g & f & (d & a) & h & i & l ^ l & i & (h & (g & f & (b & d))) ^ g & f & (d & c) & h & i & l ^ (g & f & (e & b) ^ g & f & (e & c)) & h & (l & i) ^ l & h & (g & f & (b & d)) ^ l & h & (g & f & (e & a) ^ g & f & (e & b)) ^ l & i & (g & f & (e & a) ^ g & f & (e & b) ^ g & f & a & h) ^ (g & f & b ^ c & f & g) & h & l ^ l & i & (c & f & g ^ d & a & h) ^ l & i & ((g & f & b ^ c & f & g) & h) ^ (b ^ a) & e & (i & h) & l ^ d & (l & i & c) ^ (g & f & (e & a) ^ d & c & e ^ g & f & (d & c) ^ g & f & a) & i ^ (i & h & (e & c) ^ d & a & e) & l"; +inputText = "(x0^x1^x2^x3)&(x3|(x4|x5&x6))|x7|x8|x9"; +//inputText = "x0|x1|x2|x3^(x4|x5|x6&x7)"; +//inputText = "d & a & e ^ (b ^ a ^ c ^ -1) & d ^ e & a ^ e & b ^ e & c ^ (b ^ a) & d & (l & i) ^ d & e & (c ^ b) ^ c & f & g ^ h ^ g & f & (d & c & e) ^ g & f & (b & d & e) ^ g & f & (d & a & e) ^ g & f & (d & a) ^ g & f & (b & d) ^ g & f & (d & c) ^ g & f & (e & a) ^ g & f & (e & b) ^ g & f & (e & c) ^ g & f & a ^ g & f & b ^ d & a & e & h ^ b & d & e & h ^ d & c & e & h ^ c & f & g & h ^ d & a & h ^ b & d & h ^ d & c & h ^ e & a & h ^ d & h ^ i ^ b & d & h & i ^ i & (g & f & (b & d & e)) ^ g & f & (e & c) & h ^ e & h & (c ^ b) ^ h & (g & f & (b & d)) ^ g & f & (d & c) & h ^ g & f & (d & c & e) & i ^ g & f & (d & a) & i ^ i & (g & f & (b & d)) ^ g & f & (e & b) & i ^ g & f & (e & c) & i ^ d & a & e & h & i ^ b & d & e & h & i ^ d & c & e & h & i ^ d & a & e & i ^ b & d & e & i ^ d & a & h & i ^ d & a & i ^ b & d & i ^ d & c & i ^ e & a & i ^ e & b & i ^ d & i ^ i & h ^ (g & f & (e & a) ^ g & f & (e & b)) & h ^ i & h & (e & c) ^ g & f & (d & a & e) & h & l ^ i & h & (g & f & (b & d & e)) ^ g & f & (d & a & e) & h & i ^ (g & f & (d & a & e) ^ g & f & (b & d & e)) & h ^ (g & f & (d & c & e) ^ g & f & (d & a)) & h ^ (g & f & a ^ g & f & b) & h ^ g & f & (d & a) & h & i ^ i & h & (g & f & (b & d)) ^ g & f & (d & c) & h & i ^ g & f & (e & a) & (i & h) ^ g & f & (e & b) & (i & h) ^ i & h & (g & f & (e & c)) ^ l & (g & f & (b & d & e)) ^ g & f & (d & c & e) & l ^ g & f & (d & a) & h & l ^ g & f & (d & c) & h & l ^ g & f & (d & a) & i & l ^ g & f & (e & c) & i & l ^ d & a & e & h & i & l ^ b & d & e & h & i & l ^ d & c & e & h & i & l ^ g & f & (d & a) & l ^ l & (g & f & (b & d)) ^ g & f & (d & c) & l ^ g & f & (e & a) & l ^ g & f & (e & b) & l ^ g & f & (e & c) & l ^ d & a & e & h & l ^ b & d & e & h & l ^ d & c & e & h & l ^ g & f & a & h & l ^ d & a & e & i & l ^ b & d & e & i & l ^ b & d & h & i & l ^ b & d & e & l ^ d & c & e & l ^ (g & f & a ^ g & f & b) & l ^ (c & f & g ^ d & a & h) & l ^ b & d & h & l ^ d & c & h & l ^ e & a & h & l ^ l & (e & h & (c ^ b)) ^ e & a & i & l ^ (b & d ^ (e & a ^ d & c)) & l ^ e & b & l ^ e & c & l ^ d & h & l ^ d & i & l ^ i & h & l ^ d & l ^ (i ^ h) & l ^ (b ^ a) & e & (i & h) ^ l & i & (g & f & (e & a) & h) ^ ((b ^ a ^ c) & e & (g & f) & (d & h & i) ^ -1) & l ^ l & i & (g & f & (b & d) ^ g & f & (d & c)) ^ l & h & (g & f & (e & c)) ^ d & (i & h & c) ^ g & f & (i & h & c) ^ d & c & h & (l & i) ^ (e & b & i ^ d & a) & l ^ (d & h ^ e & c ^ (g & f & b ^ c & f & g)) & i ^ (g & f & (d & c & e) & i ^ g & f & (d & a & e)) & l ^ l & i & (d & c & e) ^ l & i & (g & f & a) ^ l & i & (g & f & b) ^ l & i & (e & c) ^ l & i & (d & h) ^ l & h & (g & f & (b & d & e)) ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e)) & i ^ (g & f & a ^ g & f & b) & h & i ^ (g & f & (d & c & e) & h ^ g & f & (d & a & e) & i) & l ^ l & i & (g & f & (b & d & e)) ^ g & f & (d & a) & h & i & l ^ l & i & (h & (g & f & (b & d))) ^ g & f & (d & c) & h & i & l ^ (g & f & (e & b) ^ g & f & (e & c)) & h & (l & i) ^ l & h & (g & f & (b & d)) ^ l & h & (g & f & (e & a) ^ g & f & (e & b)) ^ l & i & (g & f & (e & a) ^ g & f & (e & b) ^ g & f & a & h) ^ (g & f & b ^ c & f & g) & h & l ^ l & i & (c & f & g ^ d & a & h) ^ l & i & ((g & f & b ^ c & f & g) & h) ^ (b ^ a) & e & (i & h) & l ^ d & (l & i & c) ^ (g & f & (e & a) ^ d & c & e ^ g & f & (d & c) ^ g & f & a) & i ^ (i & h & (e & c) ^ d & a & e) & l"; + +//inputText = "(a^b)|(c^d)"; //inputText = "(x0^x1^x2^x3)&(x3|(x4|x5&x6))|x7|x8|x9"; //inputText = "a^b^c"; //inputText = "(~((~x0 & ~x1) | ((x0 & ~x3) ^ ~x2 ^ x5) | ((x0 & ~x4) ^ (~x1 & ~x2)) | (x2 & ~x0) | (~x1 & (x2 ^ x4)) | (x2 & ~x4) | ((x3 & (~x0 ^ x1)) ^ ~x0 ^ x2 ^ x4 ^ x6))) | ((x2 & ((x0 & ((x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x3 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x1 & ((x4 & (~x3 ^ x5 ^ x6)) ^ (x7 & (~x5 ^ x6)) ^ (~(x3 & x5)) ^ x6)) ^ (x6 & (~x4 ^ x5 ^ x7)) ^ (x3 & (x4 ^ x5)) ^ (x7 & ~x5) ^ ~x4)) ^ (x5 & ~x0 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (~x3 & ~x4)))) | ((x0 & ((x1 & ((x4 & ((x2 & (x3 ^ x5 ^ x6)) ^ ~x7)) ^ (x3 & ((x5 & ~x2) ^ x6)) ^ (x6 & ~x5) ^ ~x7)) ^ (x6 & ((x2 & (~x3 ^ x4 ^ x5)) ^ (~x3 & ~x4))) ^ (x4 & ((~(x2 & x3)) ^ x5 ^ x7)) ^ (x5 & ~x2) ^ ~x7)) ^ (x5 & ~x2 & ((x4 & (~x1 ^ x3)) ^ ~x3 ^ (x1 & x6)))) | ((x0 & ((x5 & ((x1 & ((x4 & (~x2 ^ x3)) ^ x6 ^ x7)) ^ (x3 & (~x2 ^ x4 ^ x6)) ^ (~(x2 & x4)) ^ x6 ^ x7)) ^ (x2 & ((x1 & ((x3 & (~x4 ^ x6)) ^ (~(x4 & x6)))) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x7 & (~x1 ^ x3 ^ x4)) ^ (x4 & (x1 ^ x3)))) ^ (x1 & ((x2 & ((x3 & (x4 ^ x6 ^ x7)) ^ (x4 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & ((x4 & ~x3) ^ x6 ^ x7)) ^ (x3 & (x4 ^ x7)))) ^ (x3 & ((x4 & ((x2 & ~x6) ^ ~x5 ^ x7)) ^ (x5 & (~x2 ^ x6)))) ^ (x5 & (~x2 ^ x6 ^ (x4 & x7))) ^ (x2 & x4 & (x6 ^ x7))) | (~(((x0 & ~x2) ^ ~x3 ^ x5) | x1 | (x4 ^ x2) | ((x2 & ~x0) ^ x6))) | ((x2 & ((x4 & ((x1 & (x0 ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x0 & (~x5 ^ x6)) ^ (x3 & ~x6) ^ x6 ^ x7)) ^ (x0 & ((x1 & ((~(x3 & x6)) ^ x7)) ^ (~(x5 & x6)) ^ x7)) ^ (x1 & x6 & (x3 ^ x5)))) ^ (x1 & ((x6 & ((x0 & (x3 ^ x4 ^ x5)) ^ (x3 & ~x4) ^ x5)) ^ (x4 & x5 & (~(x0 & x3)))))) | ((x2 & ((x0 & ((x1 & ((x3 & (~x5 ^ x7)) ^ (x4 & ~x5) ^ x5 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ (x5 & ~x3) ^ ~x4 ^ x7)) ^ (x3 & ((x6 & (~x1 ^ x4 ^ x7)) ^ (x1 & (x4 ^ x5)) ^ ~x4 ^ x5 ^ x7)) ^ (x1 & ((x5 & (~x4 ^ x6)) ^ x4 ^ x6)) ^ (x6 & (~x4 ^ x7)) ^ ~x4 ^ x5 ^ x7)) ^ (x5 & ~x0 & (~x1 ^ x3) & (x4 ^ x6))) | ((x0 & ((x2 & ((x4 & ((x6 & ~x1) ^ ~x3 ^ x5 ^ x7)) ^ (x6 & (~x3 ^ x5)) ^ (~x1 & ~x7))) ^ (x3 & ((x1 & ((~(x4 & x5)) ^ x6 ^ x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & ((x6 & ~x5) ^ ~x7)) ^ (~x4 & (~x6 ^ x7)))) ^ (x1 & x5 & ~x2 & (x4 ^ x6))) | ((x0 & ((x1 & ((x2 & ((x3 & (x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (x5 & (~x3 ^ x4 ^ x6 ^ x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x2 & ((x3 & (~x4 ^ x7)) ^ (x5 & (~x4 ^ x6)) ^ ~x7)) ^ (x5 & ((x3 & (~x4 ^ x6)) ^ ~x7)) ^ (x6 & (~x3 ^ x4)) ^ ~x7)) ^ (x1 & ((x5 & ((x2 & (~x4 ^ x6 ^ x7)) ^ (~x3 & (~x4 ^ x6)))) ^ (x2 & ((x3 & (~x6 ^ x7)) ^ (x4 & x6))) ^ (x4 & x6 & ~x3))) ^ (x4 & ~x7 & (~x2 ^ x3)) ^ (x5 & ~x3 & (~x2 ^ x7))) | ((x0 & ((x1 & ((x2 & ((x3 & (x4 ^ x5 ^ x6)) ^ (x4 & ~x6) ^ x5)) ^ (x3 & (~x5 ^ x7)) ^ (x6 & ~x4) ^ ~x5 ^ x7)) ^ (~x3 & ((x2 & (x4 ^ x5 ^ x6)) ^ (x6 & ~x4) ^ ~x5 ^ x7)))) ^ (x4 & ((x1 & ((x3 & (~x2 ^ x6 ^ x7)) ^ (x2 & ~x6) ^ ~x7)) ^ (x2 & ~x3 & ~x6) ^ (~x3 & ~x7))) ^ (x5 & ~x1 & ~x2 & ~x3) ^ (x1 & x3 & x6 & ~x2)) | ((x0 & ((x1 & ((x3 & (~((x2 & ~x7) ^ (x4 & ~x5)))) ^ (x4 & (~x2 ^ x6)) ^ ~x5 ^ x6 ^ (x2 & x7))) ^ (x2 & ((x6 & (~x3 ^ x5 ^ x7)) ^ (x4 & (x3 ^ x7)) ^ (~(x5 & x7)))) ^ (x3 & ((~(x4 & x5)) ^ x7)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x3 & ((x2 & ((x4 & (~x5 ^ x6)) ^ (x1 & (x5 ^ x7)) ^ ~x5 ^ x6)) ^ (x1 & ((x6 & ~x7) ^ ~x4 ^ x5)) ^ (x4 & (x6 ^ x7)) ^ ~x5 ^ x6)) ^ (x2 & ((x5 & ~x1 & ~x7) ^ (~x6 & ~x7))) ^ (x4 & ((x1 & ~x7) ^ (x5 & ~x6) ^ ~x7)) ^ (x5 & x6 & ~x1)) | ((x5 & ((x1 & ((x0 & ((x2 & ~x3) ^ ~x3 ^ x6)) ^ (~x3 & (~x2 ^ x6)))) ^ (x4 & ~x3 & (~x0 ^ x2)) ^ (x6 & ((x0 & ~x2) ^ ~x3)))) ^ (x0 & x3 & ((x1 & (x2 ^ x4 ^ x6 ^ x7)) ^ ((~x4 ^ x7) & (x2 ^ x6))))) | ((x2 & ((x6 & ((x0 & ((x1 & ~x3) ^ ~x4)) ^ (x5 & (~x1 ^ x4)) ^ (x3 & ~x4))) ^ (x1 & ((x0 & ~x4) ^ (x3 & ~x4) ^ x5)) ^ (~x4 & (x0 ^ x3 ^ x5)))) ^ (x0 & ((x1 & ((x4 & (~(x5 & ~x3))) ^ (~(x6 & ~x3)))) ^ (~x4 & ~x6))) ^ (x3 & ~x4 & (~x1 ^ x6)) ^ (x5 & ~x6 & (~x1 ^ x4))) | (~(~x5 | x0 | x2 | x3 | x4)) | ((x0 & ((x2 & ((x1 & ((x3 & (~x6 ^ x7)) ^ (x4 & ~x5) ^ ~x6)) ^ (x3 & (~x5 ^ x6 ^ x7)) ^ (x5 & ~x6) ^ ~x4)) ^ (x6 & ((x1 & (~x3 ^ x5)) ^ (x5 & ~x3) ^ ~x4)) ^ (x1 & (~(x4 & (~(x3 & x5))))) ^ (x5 & ~x3) ^ ~x4)) ^ (x3 & ((x2 & ((x1 & ~x6) ^ ~x5 ^ x6 ^ (x4 & x7))) ^ (x4 & (~x1 ^ x6)) ^ (x5 & ~x6) ^ ~x1 ^ x6)) ^ (x5 & ((x4 & ((x1 & ~x2) ^ ~x2 ^ x6)) ^ (x1 & ~x2) ^ (x2 & x6))) ^ (x1 & x2 & x6 & ~x4)) | (~(~x1 | ~x5 | (x2 ^ x0) | (x4 ^ x0) | x3)) | ((x2 & ((x0 & ((x4 & ((x1 & ~x5) ^ x3 ^ x5 ^ x6 ^ x7)) ^ (x5 & (~x3 ^ x6 ^ x7)) ^ (x6 & ((~(x1 & x3)) ^ x7)) ^ (x1 & x3 & x7))) ^ (x1 & ((x5 & (x3 ^ x6 ^ x7)) ^ (x6 & (x3 ^ x7)) ^ ~x4 ^ x7)) ^ (x4 & ((x3 & ~x5) ^ ~x5 ^ x6)) ^ (x5 & (~x6 ^ x7)) ^ (~x6 & ~x7))) ^ (x0 & ((x6 & ((x3 & (~x1 ^ x4 ^ x5)) ^ (x7 & ~x1) ^ x4 ^ x5)) ^ (x5 & ~x4 & (x1 ^ x3)))) ^ (((x4 & ~x7) ^ (x5 & ~x3)) & (x1 ^ x6))) | (~((~(x4 ^ x1 ^ x0)) | ((x0 & (~(x1 & ~x2))) ^ (x3 & ~x5) ^ (~(x1 & x2)) ^ x5) | (x6 ^ x3 ^ x2) | (x3 & ~x1) | (x0 & x3) | (x2 & x3) | (~x1 & (~x0 ^ x5)) | (x0 & (x1 ^ x5)) | (x2 & (~x0 ^ x1 ^ x5)))) | (~(~x5 | x0 | x1 | x3 | (x6 ^ x2))) | (x1 & x5 & ~x0 & ~x2 & (x4 ^ x6)) | (x0 & x1 & ((x4 & ~x3 & (x5 ^ x6)) ^ (x2 & x6 & ~x3))) | (x5 & ~x3 & (~x0 ^ x2) & (x4 ^ x6)) | (x0 & x2 & x6 & ~x3 & ~x4) | (x1 & ((x6 & ((x3 & ~x2 & (~x0 ^ x4)) ^ (x0 & x4 & ~x2))) ^ (x0 & x4 & x5 & ~x3))) | ((x0 & ((x1 & ((x2 & ((x3 & (~x4 ^ x5)) ^ (x4 & (x5 ^ x6)) ^ x5)) ^ (x6 & (~x3 ^ x7)) ^ (~((x4 & ~x5) ^ (x7 & ~x3))))) ^ (x6 & ((x4 & (~x2 ^ x3)) ^ ~x2 ^ x3 ^ x5 ^ x7)) ^ (x5 & ((x2 & (x3 ^ x4 ^ x7)) ^ (x4 & ~x3))) ^ (x7 & (~(x3 & ~x2))) ^ ~x4)) ^ (x2 & ((x1 & ((x6 & (~x4 ^ x7)) ^ (x5 & ~x7) ^ ~x4 ^ x7)) ^ (x6 & (~x3 ^ x4 ^ x7)) ^ (x4 & ~x5) ^ (x7 & ~x5) ^ ~x3)) ^ (x5 & ((x1 & ((x3 & ~x4) ^ ~x6)) ^ (x3 & ~x4) ^ (x6 & (x4 ^ x7)) ^ ~x7)) ^ (x3 & ~x6 & (x4 ^ x7))) | (x0 & x1 & x2 & x7 & (x3 ^ x5))\r\n"; +inputText = "a|b|c|d"; + var printHelp = () => { Console.WriteLine("Usage: Simplifier.exe");