Apply suggestions from code review

Co-authored-by: Hichem R. A. <[email protected]>

src/lib/reasoners/bitlist.mli

@@ -79,7 +79,7 @@ val num_unknown : t -> int
 (** [num_unknown b] returns the number of bits unknown in [b]. *)
 
 val is_fully_known : t -> bool
-(** [is_fully_known b] determines there are unknown bits in [b] or not.
+(** [is_fully_known b] determines if there are unknown bits in [b] or not.
     [is_fully_known b] is [true] iff [num_unknown b] is [0]. *)
 
 val value : t -> Z.t

src/lib/reasoners/bitv.ml

@@ -311,13 +311,13 @@ let extract_st i j { bv; sz } =
     | Ext (r, sz, k, _) ->
       [{ bv = Ext (r, sz, i + k, j + k) ; sz = j - i + 1 }]
 
-(* extract i..j from a composition of size size
+(* extract [i..j] from a composition of size [size]
 
     an element of size [sz] at the head of the composition contains the bits
     [size - 1 .. size - sz] inclusive *)
 let rec extract size i j = function
   | [] ->
-    (* We can't extract a bv of length 0! *)
+    (* We can't extract from a bv of length 0! *)
     assert false
   | [ st ] ->
     assert (st.sz = size);

src/lib/reasoners/bitv.mli

@@ -48,7 +48,7 @@ type 'a simple_term = ('a simple_term_aux) alpha_term
 
 type 'a abstract = 'a simple_term list
 
-(** [extract size i j x] extracts [i..=j] from a composition of size [size].
+(** [extract size i j x] extracts [i..j] from a composition of size [size].
 
     An element of size [sz] at the head of the composition contains the bits
     [size - 1 .. size - sz] inclusive. *)

src/lib/reasoners/bitv_rel.ml

@@ -79,13 +79,13 @@ module MX = Shostak.MXH
 
 module Domains : sig
   type t
-  (** The type of domain maps. A domain map maps each representatives (semantic
-      values, of type [X.r]) to their associated domains.
+  (** The type of domain maps. A domain map maps each representative (semantic
+      value, of type [X.r]) to its associated domain.
 
       The keys of the domain maps are expected to be current *class
-      representatives*, i.e.  normal forms wrt the `Uf` module, in which case we
-      say the domain map is *normalized*. Use `subst` to ensure that domain maps
-      stay normalized. *)
+      representatives*, i.e.  normal forms wrt to the `Uf` module, in which
+      case we say the domain map is *normalized*. Use `subst` to ensure that
+      domain maps stay normalized. *)
 
   val pp : t Fmt.t
   (** Pretty-printer for domain maps. *)
@@ -495,7 +495,7 @@ end = struct
 
   type t = {
     cs_set : CS.t ;
-    (*** All the contraints currently active *)
+    (*** All the constraints currently active *)
     cs_map : CS.t MX.t ;
     (*** Mapping from semantic values to the constraints that involves them *)
     fresh : CS.t ;
@@ -663,7 +663,7 @@ let add_eqs =
 
    - The constraints that were never propagated since they were added (this
       includes constraints that changed due to substitutions)
-   - The contraints involving variables whose domain changed since the last
+   - The constraints involving variables whose domain changed since the last
       propagation *)
 let propagate =
   let rec propagate changed bcs dom =
@@ -748,7 +748,7 @@ let assume env uf la =
           "bitlist domain: @[%a@]" Domains.pp domain;
         Printer.print_dbg
           ~module_name:"Bitv_rel" ~function_name:"assume"
-          "bitlist contraints: @[%a@]" Constraints.pp constraints;
+          "bitlist constraints: @[%a@]" Constraints.pp constraints;
       );
       (congruence, domain, constraints, eqs, size_splits)
     with Bitlist.Inconsistent ex ->

src/lib/reasoners/rel_utils.ml

@@ -219,7 +219,7 @@ module Congruence : sig
       semantic value prior to calling [remove], or [Invalid_argument] will be
       raised.
 
-      Raised [Invalid_argument] if [r] is not a registered semantic value. *)
+      @raise [Invalid_argument] if [r] is not a registered semantic value. *)
 
   val subst : X.r -> X.r -> t -> (X.r -> X.r -> 'a -> 'a) -> 'a -> t * 'a
   (** [subst p v t f x] performs a local congruence closure of the