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 5096efe35ce6df..41e6b889382e16 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 1022ebd015bcd7..adc535694eff81 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 6402af52b3d743..08ad0face5de05 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 336871a5aa2ec3..1747b69ad1c32d 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 364282fc32a9c0..42ad4a139f4236 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 @@ -39,199 +38,64 @@ 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) { - if (preds.Length == 0) + var tree = new PartitionTree(_algebra.True); + foreach (TPredicate pred in preds) { - return new List { _algebra.True }; + // Push each predicate into the partition tree + tree.Refine(_algebra, pred); } - - // 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 seen = new HashSet(); - for (int i = 0; i < preds.Length; i++) - { - // 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(preds[i]); - } - } - // 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 /// 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) + TPredicate thisAndOther = solver.And(_pred, other); + if (solver.IsSatisfiable(thisAndOther)) { - // 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)) { - // 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, minterms may need to be split + if (_left is null) { - // 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); + Debug.Assert(_right is null); + _left = new PartitionTree(thisAndOther); + _right = new PartitionTree(thisMinusOther); } - else // [[this]] subset of [[other]] + else { - // Other implies this, so populate the left child with this - _left = new PartitionTree(_solver, _pred, null, null); + Debug.Assert(_right is not null); + _left.Refine(solver, other); + _right.Refine(solver, other); } } - 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)) - { - // Other is satisfiable in this subtree - TPredicate thisMinusOther = _solver.And(_pred, _solver.Not(other)); - if (_solver.IsSatisfiable(thisMinusOther)) - { - // But other does not imply this whole subtree, refine both children - _left.Refine(other); - _right.Refine(other); - } - else // [[this]] subset of [[other]] - { - // And other implies the whole subtree, include it in all minterms under here - _left.ExtendLeft(); - _right.ExtendLeft(); - } - } - 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 +114,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); } } 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 41dfdf3898bf58..c6dd4228a1c76d 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(); }