Module `Term_based.Nonrelational`

module Make
  (Terms : 
    Terms.Sig.TERMS
      with type ('a, 'b) Relation.t = ('a, 'b) Terms.Relations.Equality.t)
  (SVA : Single_value_abstraction.Sig.NUMERIC_ENUM) : 
  Term_based_sig.Domain_S
    with module Query.Boolean_Lattice = SVA.Boolean_Lattice
     and module Query.Integer_Lattice = SVA.Integer_Lattice
     and module Terms = Terms

Simple non-relational abstraction, maps terms to the numeric abstraction provided in SVA. This is for the case where there are no relations between the terms (besides equality).

module MakeUF
  (T : Terms.Sig.TERMS)
  (SVA : Single_value_abstraction.Sig.NUMERIC_ENUM)
  (_ : 
    Terms.Relations.GROUP_ACTION
      with type bitvector = SVA.bitvector
       and type integer = SVA.integer
       and type boolean = SVA.boolean
       and type enum = SVA.enum
       and type ('a, 'b) relation = ('a, 'b) T.Relation.t) : 
  Term_based_sig.DOMAIN_WITH_UNION
    with module Query.Boolean_Lattice = SVA.Boolean_Lattice
     and module Query.Integer_Lattice = SVA.Integer_Lattice
     and module Terms = T

Make the reduced product of a non-relational domain and a labeled union-find. This should then be passed to one of the functions in Union_find, as these are the ones that create relation

Module Term_based.Nonrelational

Module `Term_based.Nonrelational`