Class BddEquivalenceChecker

Namespace

LogicalOptimizer

Assembly

LogicalOptimizer.dll

BDD backend: builds both sides in one manager and compares canonical roots. Returns Unknown when the node budget is exceeded (no counterexample extraction).

public sealed class BddEquivalenceChecker : IEquivalenceChecker

Inheritance

object

BddEquivalenceChecker

Implements

IEquivalenceChecker

Inherited Members

object.Equals(object)

object.Equals(object, object)

object.GetHashCode()

object.GetType()

object.ReferenceEquals(object, object)

object.ToString()

Constructors

BddEquivalenceChecker(int)

public BddEquivalenceChecker(int nodeBudget = 1000000)

Parameters

nodeBudget int

Methods

Check(AstNode, AstNode, CancellationToken)

public EquivalenceCheckResult Check(AstNode left, AstNode right, CancellationToken cancellationToken = default)

Parameters

left AstNode

right AstNode

cancellationToken CancellationToken

Returns

EquivalenceCheckResult