Address review comment

src/lib/reasoners/satml.ml

@@ -840,15 +840,15 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
     Vec.shrink watched !new_sz_w
 
   let acts_add_decision_lit env lit =
-    let atom, _ = Atom.add_lit_atom env.hcons_env lit [] in
+    let atom, _ = Atom.add_atom env.hcons_env lit [] in
     if atom.var.level < 0 then (
       assert (not atom.is_true && not atom.neg.is_true);
       env.next_decisions <- atom :: env.next_decisions
     ) else
       assert (atom.is_true || atom.neg.is_true)
 
   let acts_add_split env lit =
-    let atom, _ = Atom.add_lit_atom env.hcons_env lit [] in
+    let atom, _ = Atom.add_atom env.hcons_env lit [] in
     if atom.var.level < 0 then (
       assert (not atom.is_true && not atom.neg.is_true);
       env.next_split <- Some atom
@@ -861,7 +861,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
        We can't update the theory inside this function, because it is called
        from within the theory. *)
-    let atom, _ = Atom.add_lit_atom env.hcons_env lit [] in
+    let atom, _ = Atom.add_atom env.hcons_env lit [] in
     env.next_objective <- Some (fn, value, atom)
 
   let[@inline] theory_slice env : _ Th_util.acts = {

src/lib/structures/satml_types.ml

@@ -114,9 +114,9 @@ module type ATOM = sig
   val hash_atom  : atom -> int
   val tag_atom   : atom -> int
 
-  val add_lit_atom :
+  val add_atom :
     hcons_env -> Shostak.Literal.t -> var list -> atom * var list
-  val add_atom : hcons_env -> E.t -> var list -> atom * var list
+  val add_expr_atom : hcons_env -> E.t -> var list -> atom * var list
 
   module Set : Set.S with type elt = atom
   module Map : Map.S with type key = atom
@@ -330,12 +330,12 @@ module Atom : ATOM = struct
       incr hcons.cpt;
       var, negated, var :: acc
 
-  let add_lit_atom hcons lit acc =
+  let add_atom hcons lit acc =
     let var, negated, acc = make_var hcons lit acc in
     (if negated then var.na else var.pa), acc
 
-  let add_atom hcons lit acc =
-    add_lit_atom hcons (Shostak.Literal.make @@ LTerm lit) acc
+  let add_expr_atom hcons lit acc =
+    add_atom hcons (Shostak.Literal.make @@ LTerm lit) acc
 
   (* with this code, all envs created with empty_hcons_env () will be
      initialized with the good reference to "vrai" *)
@@ -344,7 +344,7 @@ module Atom : ATOM = struct
 
   let empty_hcons_env, vrai_atom =
     let empty_hcons = { tbl= HT.create 5048 ; cpt = ref (-1) } in
-    let a, _ = add_atom empty_hcons E.vrai [] in
+    let a, _ = add_expr_atom empty_hcons E.vrai [] in
     a.is_true <- true;
     a.var.level <- 0;
     a.var.reason <- None;
@@ -638,7 +638,7 @@ module Flat_Formula : FLAT_FORMULA = struct
   let complements f1 f2 = f1.tag == f2.neg.tag
 
   let mk_lit hcons a acc =
-    let at, acc = Atom.add_atom hcons.atoms a acc in
+    let at, acc = Atom.add_expr_atom hcons.atoms a acc in
     let at =
       if Options.get_disable_flat_formulas_simplification () then at
       else
@@ -895,7 +895,7 @@ module Flat_Formula : FLAT_FORMULA = struct
       else
         let lit = E.fresh_name Ty.Tbool in
         let xlit, new_v = mk_lit hcons lit !new_vars in
-        let at_lit, new_v = Atom.add_atom hcons.atoms lit new_v in
+        let at_lit, new_v = Atom.add_expr_atom hcons.atoms lit new_v in
         new_vars := new_v;
         lem := (f, (xlit, at_lit)) :: !lem
                [@ocaml.ppwarning "xlit or at_lit is probably redundant"]
@@ -954,7 +954,7 @@ module Flat_Formula : FLAT_FORMULA = struct
   (* CNF_ABSTR a la Tseitin *)
 
   let atom_of_lit hcons lit is_neg new_vars =
-    let a, l = Atom.add_atom hcons.atoms lit new_vars in
+    let a, l = Atom.add_expr_atom hcons.atoms lit new_vars in
     if is_neg then a.Atom.neg,l else a,l
 
   let mk_new_proxy n =
@@ -1021,7 +1021,7 @@ module Proxy_formula = struct
     with Not_found -> None
 
   let atom_of_lit hcons lit is_neg new_vars =
-    let a, l = Atom.add_atom hcons lit new_vars in
+    let a, l = Atom.add_expr_atom hcons lit new_vars in
     if is_neg then a.Atom.neg,l else a,l
 
   let mk_new_proxy n =

src/lib/structures/satml_types.mli

@@ -110,9 +110,9 @@ module type ATOM = sig
   val hash_atom  : atom -> int
   val tag_atom   : atom -> int
 
-  val add_lit_atom :
+  val add_atom :
     hcons_env -> Shostak.Literal.t -> var list -> atom * var list
-  val add_atom : hcons_env -> Expr.t -> var list -> atom * var list
+  val add_expr_atom : hcons_env -> Expr.t -> var list -> atom * var list
 
   module Set : Set.S with type elt = atom
   module Map : Map.S with type key = atom