Module Theo.CombineSource

Combine(A)(B) creates a new theory that is the sum of A and B. This allows a single BDD to reason about multiple types of atoms simultaneously.

The resulting module provides Left and Right functors to lift a Formula operating on the combined theory back to a Formula operating on just A or B. This is the key mechanism that allows syntax modules to be specific to a theory but compatible with the combined BDD.

Parameters

module A : Theory
module B : Theory

Signature

Sourcetype _ t =
  1. | Left : 'a A.t -> 'a t
  2. | Right : 'a B.t -> 'a t

The sum type of theory atoms.

This type is crucial for introspection (via view_constraint). Pattern match on Left or Right to determine which specific theory an atom belongs to.

include Theory with type 'kind t := 'kind t
Sourceval equal : _ t -> _ t -> bool

Equality check for atoms. Must be consistent with compare and hash.

Sourceval compare : _ t -> _ t -> int

Total ordering function. Used for set/map operations and canonical ordering in BDDs.

Sourceval hash : _ t -> int

Hash function for atoms. Must be compatible with equal.

Sourceval to_string : _ t -> string

String representation for debugging.

Sourcemodule Left (F : Formula with type 'kind desc = 'kind t) : Formula with type 'kind desc = 'kind A.t and type t = F.t

Lifts a Formula from the combined theory back to theory A.

Sourcemodule Right (F : Formula with type 'kind desc = 'kind t) : Formula with type 'kind desc = 'kind B.t and type t = F.t

Lifts a Formula from the combined theory back to theory B.