Module shared_terms 

Shared Terms Management for Theory Combination.

Manages terms that appear in multiple theories, enabling efficient equality sharing in Nelson-Oppen combination.

Architecture

• Term Index: Fast lookup of shared terms
• Theory Subscriptions: Theories register interest in terms
• Notification System: Propagate equality information between theories

References

• Nelson & Oppen: “Simplification by Cooperating Decision Procedures” (1979)
• Z3’s smt/theory_combine.cpp

Structs

Equality

Equality between two terms.

SharedTermsConfig

Configuration for shared terms manager.

SharedTermsManager

Shared terms manager for theory combination.

SharedTermsStats

Statistics for shared terms.

Type Aliases

TheoryId

Theory identifier.