Skip to content

Commit

Permalink
Simplify minterm generation in Regex NonBacktracking engine (#61232)
Browse files Browse the repository at this point in the history 
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.
Remove the deduplication, since its now optional and the only call
site already passes in a unique set of predicates.
Make MintermGenerator take an IEnumerable.
  • Loading branch information
@olsaarik
olsaarik authored Nov 5, 2021
1 parent ed66b28 commit 215ff0b
Show file tree
Hide file tree
Showing 6 changed files with 33 additions and 189 deletions.
2 changes: 1 addition & 1 deletion ...ext.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BDDAlgebra.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -288,7 +288,7 @@ private BDD ShiftLeftImpl(Dictionary<(BDD set, int k), BDD> shiftCache, BDD set,
/// </summary>
/// <param name="sets">the BDDs to create the minterms for</param>
/// <returns>BDDs for the minterm</returns>
public List<BDD> GenerateMinterms(params BDD[] sets) => _mintermGen.GenerateMinterms(sets);
public List<BDD> GenerateMinterms(IEnumerable<BDD> sets) => _mintermGen.GenerateMinterms(sets);

/// <summary>
/// Make a set containing all integers whose bits up to maxBit equal n.
Expand Down
2 changes: 1 addition & 1 deletion ...xt.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BV64Algebra.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ public BV64Algebra(CharSetSolver solver, BDD[] minterms) :

public bool AreEquivalent(ulong predicate1, ulong predicate2) => predicate1 == predicate2;

public List<ulong> GenerateMinterms(params ulong[] constraints) => _mintermGenerator.GenerateMinterms(constraints);
public List<ulong> GenerateMinterms(IEnumerable<ulong> constraints) => _mintermGenerator.GenerateMinterms(constraints);

[MethodImpl(MethodImplOptions.AggressiveInlining)]
public bool IsSatisfiable(ulong predicate) => predicate != _false;
Expand Down
2 changes: 1 addition & 1 deletion ...Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/BVAlgebra.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<BV> GenerateMinterms(params BV[] constraints) => _mintermGenerator.GenerateMinterms(constraints);
public List<BV> GenerateMinterms(IEnumerable<BV> constraints) => _mintermGenerator.GenerateMinterms(constraints);

[MethodImpl(MethodImplOptions.AggressiveInlining)]
public bool IsSatisfiable(BV predicate) => !predicate.Equals(False);
Expand Down
4 changes: 2 additions & 2 deletions ...egularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/IBooleanAlgebra.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,8 @@ internal interface IBooleanAlgebra<T>
/// where c'_i = c_i if b_i = true and c'_i is Not(c_i) otherwise.
/// If n=0 return Tuple({},True)
/// </summary>
/// <param name="constraints">array of constraints</param>
/// <param name="constraints">constraints</param>
/// <returns>constraints that are satisfiable</returns>
List<T> GenerateMinterms(params T[] constraints);
List<T> GenerateMinterms(IEnumerable<T> constraints);
}
}
196 changes: 27 additions & 169 deletions ...gularExpressions/src/System/Text/RegularExpressions/Symbolic/Algebras/MintermGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -39,199 +38,64 @@ public MintermGenerator(IBooleanAlgebra<TPredicate> algebra)
/// </summary>
/// <param name="preds">array of predicates</param>
/// <returns>all minterms of the given predicate sequence</returns>
public List<TPredicate> GenerateMinterms(params TPredicate[] preds)
public List<TPredicate> GenerateMinterms(IEnumerable<TPredicate> preds)
{
if (preds.Length == 0)
var tree = new PartitionTree(_algebra.True);
foreach (TPredicate pred in preds)
{
return new List<TPredicate> { _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<EquivalenceClass>();
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();
}

/// <summary>Wraps a predicate as an equivalence class object whose Equals method is equivalence checking.</summary>
private readonly struct EquivalenceClass
{
private readonly TPredicate _set;
private readonly IBooleanAlgebra<TPredicate> _algebra;

internal EquivalenceClass(IBooleanAlgebra<TPredicate> 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);
}

/// <summary>A partition tree for efficiently solving minterms.</summary>
/// <remarks>
/// 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.
/// </remarks>
private sealed class PartitionTree
{
internal readonly TPredicate _pred;
private readonly IBooleanAlgebra<TPredicate> _solver;
private PartitionTree? _left;
private PartitionTree? _right; // complement
private PartitionTree? _right;

/// <summary>Create the root of the partition tree.</summary>
/// <remarks>Nodes below this will be indexed starting from 0. The initial predicate is true.</remarks>
internal PartitionTree(IBooleanAlgebra<TPredicate> solver) : this(solver, solver.True, null, null) { }

private PartitionTree(IBooleanAlgebra<TPredicate> 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<TPredicate> 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();
}
}
}

/// <summary>
/// Include the next predicate in all minterms under this node. Assumes the next predicate implies the predicate
/// of this node.
/// </summary>
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();
}
}

/// <summary>
/// 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.
/// </summary>
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();
}
}

Expand All @@ -250,15 +114,9 @@ internal List<TPredicate> 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);
}
}

Expand Down
16 changes: 1 addition & 15 deletions ....Text.RegularExpressions/src/System/Text/RegularExpressions/Symbolic/SymbolicRegexNode.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1222,10 +1222,6 @@ public HashSet<S> GetPredicates()
{
var predicates = new HashSet<S>();
CollectPredicates_helper(predicates);
if (predicates.Count == 0)
{
predicates.Add(_builder._solver.True);
}
return predicates;
}

Expand Down Expand Up @@ -1311,17 +1307,7 @@ public S[] ComputeMinterms()
Debug.Assert(typeof(S).IsAssignableTo(typeof(IComparable)));

HashSet<S> 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<S> mt = _builder._solver.GenerateMinterms(predicatesArray);
List<S> mt = _builder._solver.GenerateMinterms(predicates);
mt.Sort();
return mt.ToArray();
}
Expand Down

0 comments on commit 215ff0b

Please sign in to comment.