From 4b0899b3692a276ea5aface7857c2882cb4d2972 Mon Sep 17 00:00:00 2001 From: Olli Saarikivi Date: Thu, 4 Nov 2021 16:24:01 -0700 Subject: [PATCH 1/2] Simplify and optimize minterm generation PartitionTree had a holdover from when it was tracking the predicates that made up each minterm, which caused it to use order n too much memory for some patterns. Nodes with the same predicate as the parent are no longer created. This also significantly simplified the algorithm. --- .../Symbolic/Algebras/MintermGenerator.cs | 167 +++--------------- 1 file changed, 25 insertions(+), 142 deletions(-) diff --git a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/MintermGenerator.cs b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/MintermGenerator.cs index 364282fc32a9c..a9db4c3203daa 100644 --- a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/MintermGenerator.cs +++ b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/MintermGenerator.cs @@ -4,7 +4,6 @@ using System.Collections.Generic; using System.Diagnostics; using System.Diagnostics.CodeAnalysis; -using System.Runtime.CompilerServices; using System.Threading; namespace System.Text.RegularExpressions.Symbolic @@ -41,17 +40,9 @@ public MintermGenerator(IBooleanAlgebra algebra) /// all minterms of the given predicate sequence public List GenerateMinterms(params TPredicate[] preds) { - if (preds.Length == 0) - { - return new List { _algebra.True }; - } - - // The minterms will be solved using non-equivalent predicates, i.e., the equivalence classes of preds. The - // following code maps each predicate to an equivalence class and also stores for each equivalence class the - // predicates belonging to it, so that a valuation for the original predicates may be reconstructed. - - var tree = new PartitionTree(_algebra); + var tree = new PartitionTree(_algebra.True); + // The minterms will be solved using non-equivalent predicates, i.e., the equivalence classes of preds var seen = new HashSet(); for (int i = 0; i < preds.Length; i++) { @@ -59,7 +50,7 @@ public List GenerateMinterms(params TPredicate[] preds) if (seen.Add(new EquivalenceClass(_algebra, preds[i]))) { // Push each equivalence class into the partition tree - tree.Refine(preds[i]); + tree.Refine(_algebra, preds[i]); } } @@ -88,150 +79,48 @@ internal EquivalenceClass(IBooleanAlgebra algebra, TPredicate set) /// /// Predicates are pushed into the tree with Refine(), which creates leaves in the tree for all satisfiable /// and non-overlapping combinations with any previously pushed predicates. At the end of the process the - /// minterms can be read from the paths to the leaves of the tree. - /// - /// The valuations of the predicates are represented as follows. Given a path a^-1, a^0, a^1, ..., a^n, predicate - /// p^i is true in the corresponding minterm if and only if a^i is the left child of a^i-1. - /// - /// This class assumes that all predicates passed to Refine() are non-equivalent. + /// minterms can be read from the leaves of the tree. /// private sealed class PartitionTree { internal readonly TPredicate _pred; - private readonly IBooleanAlgebra _solver; private PartitionTree? _left; - private PartitionTree? _right; // complement + private PartitionTree? _right; - /// Create the root of the partition tree. - /// Nodes below this will be indexed starting from 0. The initial predicate is true. - internal PartitionTree(IBooleanAlgebra solver) : this(solver, solver.True, null, null) { } - - private PartitionTree(IBooleanAlgebra solver, TPredicate pred, PartitionTree? left, PartitionTree? right) + internal PartitionTree(TPredicate pred) { - _solver = solver; _pred = pred; - _left = left; - _right = right; } - internal void Refine(TPredicate other) + internal void Refine(IBooleanAlgebra solver, TPredicate other) { if (!StackHelper.TryEnsureSufficientExecutionStack()) { - StackHelper.CallOnEmptyStack(Refine, other); + StackHelper.CallOnEmptyStack(Refine, solver, other); return; } - if (_left is null && _right is null) - { - // If this is a leaf node create left and/or right children for the new predicate - TPredicate thisAndOther = _solver.And(_pred, other); - if (_solver.IsSatisfiable(thisAndOther)) - { - // The predicates overlap, now check if this is contained in other - TPredicate thisMinusOther = _solver.And(_pred, _solver.Not(other)); - if (_solver.IsSatisfiable(thisMinusOther)) - { - // This is not contained in other, both children are needed - _left = new PartitionTree(_solver, thisAndOther, null, null); - - // The right child corresponds to a conjunction with a negation, which matches thisMinusOther - _right = new PartitionTree(_solver, thisMinusOther, null, null); - } - else // [[this]] subset of [[other]] - { - // Other implies this, so populate the left child with this - _left = new PartitionTree(_solver, _pred, null, null); - } - } - else // [[this]] subset of [[not(other)]] - { - // negation of other implies this, so populate the right child with this - _right = new PartitionTree(_solver, _pred, null, null); //other must be false - } - } - else if (_left is null) - { - // No choice has to be made here, refine the single child that exists - _right!.Refine(other); - } - else if (_right is null) - { - // No choice has to be made here, refine the single child that exists - _left!.Refine(other); - } - else + TPredicate thisAndOther = solver.And(_pred, other); + if (solver.IsSatisfiable(thisAndOther)) { - TPredicate thisAndOther = _solver.And(_pred, other); - if (_solver.IsSatisfiable(thisAndOther)) + // The predicates overlap, now check if this is contained in other + TPredicate thisMinusOther = solver.And(_pred, solver.Not(other)); + if (solver.IsSatisfiable(thisMinusOther)) { - // Other is satisfiable in this subtree - TPredicate thisMinusOther = _solver.And(_pred, _solver.Not(other)); - if (_solver.IsSatisfiable(thisMinusOther)) + // This is not contained in other, minterms may need to be split + if (_left is null) { - // But other does not imply this whole subtree, refine both children - _left.Refine(other); - _right.Refine(other); + Debug.Assert(_right is null); + _left = new PartitionTree(thisAndOther); + _right = new PartitionTree(thisMinusOther); } - else // [[this]] subset of [[other]] + else { - // And other implies the whole subtree, include it in all minterms under here - _left.ExtendLeft(); - _right.ExtendLeft(); + Debug.Assert(_right is not null); + _left.Refine(solver, other); + _right.Refine(solver, other); } } - else // [[this]] subset of [[not(other)]] - { - // Other is not satisfiable in this subtree, include its negation in all minterms under here - _left.ExtendRight(); - _right.ExtendRight(); - } - } - } - - /// - /// Include the next predicate in all minterms under this node. Assumes the next predicate implies the predicate - /// of this node. - /// - private void ExtendLeft() - { - if (!StackHelper.TryEnsureSufficientExecutionStack()) - { - StackHelper.CallOnEmptyStack(ExtendLeft); - return; - } - - if (_left is null && _right is null) - { - _left = new PartitionTree(_solver, _pred, null, null); - } - else - { - _left?.ExtendLeft(); - _right?.ExtendLeft(); - } - } - - /// - /// Include the negation of next predicate in all minterms under this node. Assumes the negation of the next - /// predicate implies the predicate of this node. - /// - private void ExtendRight() - { - if (!StackHelper.TryEnsureSufficientExecutionStack()) - { - StackHelper.CallOnEmptyStack(ExtendRight); - return; - } - - if (_left is null && _right is null) - { - _right = new PartitionTree(_solver, _pred, null, null); - } - else - { - _left?.ExtendRight(); - _right?.ExtendRight(); } } @@ -250,15 +139,9 @@ internal List GetLeafPredicates() } else { - if (node._left is not null) - { - stack.Push(node._left); - } - - if (node._right is not null) - { - stack.Push(node._right); - } + Debug.Assert(node._left is not null && node._right is not null); + stack.Push(node._left); + stack.Push(node._right); } } From 9d0a33b4195baa175072a4f64a9b47c1c8e48229 Mon Sep 17 00:00:00 2001 From: Olli Saarikivi Date: Fri, 5 Nov 2021 10:38:19 -0700 Subject: [PATCH 2/2] Make MintermGenerator take an IEnumerable Also remove the deduplication in there, since its now optional and the only call site already passes in a unique set of predicates. --- .../Symbolic/Algebras/BDDAlgebra.cs | 2 +- .../Symbolic/Algebras/BV64Algebra.cs | 2 +- .../Symbolic/Algebras/BVAlgebra.cs | 2 +- .../Symbolic/Algebras/IBooleanAlgebra.cs | 4 +-- .../Symbolic/Algebras/MintermGenerator.cs | 33 +++---------------- .../Symbolic/SymbolicRegexNode.cs | 16 +-------- 6 files changed, 10 insertions(+), 49 deletions(-) diff --git a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BDDAlgebra.cs b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BDDAlgebra.cs index 5096efe35ce6d..41e6b889382e1 100644 --- a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BDDAlgebra.cs +++ b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BDDAlgebra.cs @@ -288,7 +288,7 @@ private BDD ShiftLeftImpl(Dictionary<(BDD set, int k), BDD> shiftCache, BDD set, /// /// the BDDs to create the minterms for /// BDDs for the minterm - public List GenerateMinterms(params BDD[] sets) => _mintermGen.GenerateMinterms(sets); + public List GenerateMinterms(IEnumerable sets) => _mintermGen.GenerateMinterms(sets); /// /// Make a set containing all integers whose bits up to maxBit equal n. diff --git a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BV64Algebra.cs b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BV64Algebra.cs index 1022ebd015bcd..adc535694eff8 100644 --- a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BV64Algebra.cs +++ b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BV64Algebra.cs @@ -55,7 +55,7 @@ public BV64Algebra(CharSetSolver solver, BDD[] minterms) : public bool AreEquivalent(ulong predicate1, ulong predicate2) => predicate1 == predicate2; - public List GenerateMinterms(params ulong[] constraints) => _mintermGenerator.GenerateMinterms(constraints); + public List GenerateMinterms(IEnumerable constraints) => _mintermGenerator.GenerateMinterms(constraints); [MethodImpl(MethodImplOptions.AggressiveInlining)] public bool IsSatisfiable(ulong predicate) => predicate != _false; diff --git a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BVAlgebra.cs b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BVAlgebra.cs index 6402af52b3d74..08ad0face5de0 100644 --- a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BVAlgebra.cs +++ b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BVAlgebra.cs @@ -78,7 +78,7 @@ public BVAlgebra(CharSetSolver solver, BDD[] minterms) : public bool HashCodesRespectEquivalence => true; public CharSetSolver CharSetProvider => throw new NotSupportedException(); public bool AreEquivalent(BV predicate1, BV predicate2) => predicate1.Equals(predicate2); - public List GenerateMinterms(params BV[] constraints) => _mintermGenerator.GenerateMinterms(constraints); + public List GenerateMinterms(IEnumerable constraints) => _mintermGenerator.GenerateMinterms(constraints); [MethodImpl(MethodImplOptions.AggressiveInlining)] public bool IsSatisfiable(BV predicate) => !predicate.Equals(False); diff --git a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/IBooleanAlgebra.cs b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/IBooleanAlgebra.cs index 336871a5aa2ec..1747b69ad1c32 100644 --- a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/IBooleanAlgebra.cs +++ b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/IBooleanAlgebra.cs @@ -78,8 +78,8 @@ internal interface IBooleanAlgebra /// where c'_i = c_i if b_i = true and c'_i is Not(c_i) otherwise. /// If n=0 return Tuple({},True) /// - /// array of constraints + /// constraints /// constraints that are satisfiable - List GenerateMinterms(params T[] constraints); + List GenerateMinterms(IEnumerable constraints); } } diff --git a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/MintermGenerator.cs b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/MintermGenerator.cs index a9db4c3203daa..42ad4a139f423 100644 --- a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/MintermGenerator.cs +++ b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/MintermGenerator.cs @@ -38,43 +38,18 @@ public MintermGenerator(IBooleanAlgebra algebra) /// /// array of predicates /// all minterms of the given predicate sequence - public List GenerateMinterms(params TPredicate[] preds) + public List GenerateMinterms(IEnumerable preds) { var tree = new PartitionTree(_algebra.True); - - // The minterms will be solved using non-equivalent predicates, i.e., the equivalence classes of preds - var seen = new HashSet(); - for (int i = 0; i < preds.Length; i++) + foreach (TPredicate pred in preds) { - // Use a wrapper that overloads Equals to be logical equivalence as the key - if (seen.Add(new EquivalenceClass(_algebra, preds[i]))) - { - // Push each equivalence class into the partition tree - tree.Refine(_algebra, preds[i]); - } + // Push each predicate into the partition tree + tree.Refine(_algebra, pred); } - // Return all minterms as the leaves of the partition tree return tree.GetLeafPredicates(); } - /// Wraps a predicate as an equivalence class object whose Equals method is equivalence checking. - private readonly struct EquivalenceClass - { - private readonly TPredicate _set; - private readonly IBooleanAlgebra _algebra; - - internal EquivalenceClass(IBooleanAlgebra algebra, TPredicate set) - { - _set = set; - _algebra = algebra; - } - - public override int GetHashCode() => _set.GetHashCode(); - - public override bool Equals([NotNullWhen(true)] object? obj) => obj is EquivalenceClass ec && _algebra.AreEquivalent(_set, ec._set); - } - /// A partition tree for efficiently solving minterms. /// /// Predicates are pushed into the tree with Refine(), which creates leaves in the tree for all satisfiable diff --git a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/SymbolicRegexNode.cs b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/SymbolicRegexNode.cs index 41dfdf3898bf5..c6dd4228a1c76 100644 --- a/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/SymbolicRegexNode.cs +++ b/src/libraries/System.Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/SymbolicRegexNode.cs @@ -1203,10 +1203,6 @@ public HashSet GetPredicates() { var predicates = new HashSet(); CollectPredicates_helper(predicates); - if (predicates.Count == 0) - { - predicates.Add(_builder._solver.True); - } return predicates; } @@ -1292,17 +1288,7 @@ public S[] ComputeMinterms() Debug.Assert(typeof(S).IsAssignableTo(typeof(IComparable))); HashSet predicates = GetPredicates(); - Debug.Assert(predicates.Count != 0); - - S[] predicatesArray = new S[predicates.Count]; - int i = 0; - foreach (S s in predicates) - { - predicatesArray[i++] = s; - } - Debug.Assert(i == predicatesArray.Length); - - List mt = _builder._solver.GenerateMinterms(predicatesArray); + List mt = _builder._solver.GenerateMinterms(predicates); mt.Sort(); return mt.ToArray(); }