Module interface_eq 

Interface Equality Management for Theory Combination.

This module manages interface equalities in Nelson-Oppen combination:

• Minimal interface equality generation
• Equality generation strategies
• Interface equality scheduling
• Equality minimization algorithms

Interface Equalities

Interface equalities are equalities between shared terms that must be communicated between theories. The goal is to generate a minimal set of equalities that allows theories to infer all relevant equalities.

Generation Strategies

• Eager: Generate all possible interface equalities upfront
• Lazy: Generate equalities on-demand
• Minimal: Generate only necessary equalities (star topology)
• Incremental: Add equalities incrementally as needed

Star Topology

For a set of equivalent terms {t1, t2, …, tn}, we can use a “star” topology: pick one term as the representative and only share equalities t1 = rep, t2 = rep, …, tn = rep. This requires O(n) equalities instead of O(n²).

References

• Nelson & Oppen (1979): “Simplification by Cooperating Decision Procedures”
• Shostak (1984): “Deciding Combinations of Theories”
• Z3’s smt/theory_combine.cpp

Structs

Equality

Equality between two terms.

EqualityMinimizer

Minimizer for interface equalities.

EqualityPriority

Priority for interface equality.

EqualityScheduler

Equality scheduler for coordinating propagation.

InterfaceEClass

Equivalence class for interface terms.

InterfaceEquality

Interface equality with metadata.

InterfaceEqualityConfig

Configuration for interface equality management.

InterfaceEqualityManager

Interface equality manager.

InterfaceEqualityStats

Statistics for interface equality management.

Enums

GenerationStrategy

Equality generation strategy.

SchedulingPolicy

Scheduling policy for equalities.

Type Aliases

DecisionLevel

Decision level.

TermId

Term identifier.

TheoryId

Theory identifier.