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 1c7b49c..7e048ea 100644 --- a/Mba.Simplifier/Minimization/AnfMinimizer.cs +++ b/Mba.Simplifier/Minimization/AnfMinimizer.cs @@ -1,7 +1,9 @@ -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.Minimization.Factoring; using Mba.Simplifier.Pipeline; using Mba.Utility; using System; @@ -14,6 +16,105 @@ namespace Mba.Simplifier.Minimization { + // Represents a sum of monomials in gf(2) + public class AnfPoly + { + private int? hashCode; + + public List Monoms { get; } + + public AnfPoly() + { + Monoms = new(); + } + + public AnfPoly(List monoms) + { + Monoms = monoms; + } + + 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() + { + int hash = 17; + foreach (var m in Monoms) + hash = hash * 31 + m.GetHashCode(); + + hashCode = hash; + } + + public AnfPoly Clone() + { + var clone = new AnfPoly(Monoms.ToList()); + clone.hashCode = hashCode; + return clone; + } + + 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; + + public 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) + return "-1"; + + var conjs = new List(); + for(ushort i = 0; i < 32; i++) + { + if((Mask & 1u << i) != 0) + conjs.Add($"x{i}"); + } + + return String.Join("*", conjs); + } + + public override int GetHashCode() + { + return Mask.GetHashCode(); + } + + public static AnfMonom Ones => new AnfMonom(uint.MaxValue); + + public unsafe static implicit operator uint(AnfMonom reg) => reg.Mask; + + public unsafe static implicit operator AnfMonom(uint reg) => new AnfMonom(reg); + } + public class AnfMinimizer { private readonly AstCtx ctx; @@ -22,7 +123,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. @@ -42,40 +143,9 @@ 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); + var (terms, variableCombinations) = GetAnfTerms(ctx, variables, resultVec); - // 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); - } - } + //Groebner(); AstIdx? result = null; foreach (var term in terms) @@ -103,11 +173,20 @@ 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, new AnfPoly(terms.Select(x => (AnfMonom)variableCombinations[x]).ToList()), demandedVarsMap); + factored = SimplifyORsRec(factored.Value); + //factored = TrySimplifyORs(factored.Value); // TODO: Apply the identify a^(~a&b) => a|b var simplified = SimplifyRec(factored.Value); + for(int i = 0; i < 100; 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); @@ -118,7 +197,47 @@ 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) + { + 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) @@ -127,16 +246,18 @@ 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, 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 has = 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++) { @@ -150,10 +271,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>(); - foreach (var conj in conjs) + var groups = new Dictionary(); + foreach (var conj in poly.Monoms) { - for (int index = 0; index < variableCounts.Length; index++) + for (int index = 0; index < variables.Count; index++) { var i = variableCounts[index].Item1; @@ -162,12 +283,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; } @@ -180,52 +301,319 @@ 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); 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) + if (hasOnes) { xored = ctx.Xor(ctx.Constant(ulong.MaxValue, ctx.GetWidth(variables[0])), xored); - demandedVarsMap.TryAdd(xored, demandedSum); + //demandedVarsMap.TryAdd(xored, demandedSum); } 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()); + + new BoolMinimizer(boolCtx).Minimize(id); + + // 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; + } + + // 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; + } + + 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)); + var op1 = () => SimplifyORsRec(ctx.GetOp1(id)); + + var getTerms = (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); + } + } + + 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; + while (changed) + { + 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++) + { + var a = terms[aIndex]; + var b = terms[bIndex]; + if (a == null || b == null) + 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); + if (simplified != null) + { + changed = true; + terms[aIndex] = simplified; + terms[bIndex] = null; + continue; + } + } + } + } + + + 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) + { + // 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; + + if ((aTable | bTable) != combinedTable) + Debugger.Break(); + + var ORed = aTable | bTable; + 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(); + var (bTerms, variableCombinations) = GetAnfTerms(ctx, varSet, resultVec); + if (negated) + Debugger.Break(); + + + + 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); + } + + + //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(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)); + } + private AstIdx SimplifyRec(AstIdx id) { var kind = ctx.GetOpcode(id); @@ -326,7 +714,7 @@ private AstIdx SimplifyRec(AstIdx id) private uint GetDemandedVarsMask(AstIdx id) { // If we already know the mask, return it. - uint mask = 0; + AnfMonom mask = 0; if (demandedVarsMap.TryGetValue(id, out mask)) return mask; @@ -340,6 +728,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); @@ -355,15 +744,98 @@ 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 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); for (int i = 0; i < rv.Length; i++) table.SetBit(i, rv[i] != 0); - return BooleanMinimizer.FromTruthTable(ctx, varSet, table); + 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/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 caee826..2b38cf9 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) { @@ -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/Factoring/BoolCtx.cs b/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs new file mode 100644 index 0000000..9158c77 --- /dev/null +++ b/Mba.Simplifier/Minimization/Factoring/BoolCtx.cs @@ -0,0 +1,242 @@ +using Mba.Ast; +using System; +using System.Collections.Generic; +using System.Diagnostics; +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(); + + public int VarCount { get; private set; } = 0; + + // Expr id of the constant 1 + public ExprId Constant1Id { get; set; } + + public BoolCtx() + { + Constant1Id = Constant(1); + } + + public ExprId Var(uint varIdx) + { + VarCount = Math.Max(VarCount, (int)varIdx + 1); + 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) + { + var output = new List(); + Hoist(ExprKind.Add, children, output); + children = output; + + children = ReduceSumCoefficient(children); + if (children.Count == 1) + return children[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) + { + //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) + { + var output = new List(); + Hoist(ExprKind.Mul, children, output); + children = output; + + if (children.Count == 1) + return children[0]; + + //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 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; + } + + 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..60df5ec --- /dev/null +++ b/Mba.Simplifier/Minimization/Factoring/BoolExpr.cs @@ -0,0 +1,98 @@ +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 BoolExpr Expr => ctx.Get(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..2b51d54 --- /dev/null +++ b/Mba.Simplifier/Minimization/Factoring/BoolMinimizer.cs @@ -0,0 +1,282 @@ +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 +{ + public class BoolMinimizer + { + private readonly BoolCtx ctx; + + private Dictionary costMap = new(); + + public BoolMinimizer(BoolCtx ctx) + { + this.ctx = 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(); + } + + // 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; + + // 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; + } + + // 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) + { + 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; + } + + + 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/Mba.Simplifier/Minimization/TruthTable.cs b/Mba.Simplifier/Minimization/TruthTable.cs index 75ed6a5..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]; } @@ -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,9 +83,14 @@ public bool IsDisjoint(TruthTable other) return true; } + public bool IsZero() + { + return arr.All(x => x == 0); + } + 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; @@ -91,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++) @@ -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..a75bc10 100644 --- a/Simplifier/Program.cs +++ b/Simplifier/Program.cs @@ -14,6 +14,64 @@ 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 = "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 = "(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"; + +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)"; + +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 = "(a|b|c)^d"; + +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 = () => {