From 4f170680db2dd7d156cac04ef4e874a2de87f3d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Tue, 20 Feb 2024 14:24:03 +0100 Subject: [PATCH] Address review comment --- src/lib/reasoners/satml.ml | 6 +++--- src/lib/structures/satml_types.ml | 20 ++++++++++---------- src/lib/structures/satml_types.mli | 4 ++-- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 321b1d138..9b89753e0 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -840,7 +840,7 @@ 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 @@ -848,7 +848,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct 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 = { diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml index a76902a34..7e6731fc5 100644 --- a/src/lib/structures/satml_types.ml +++ b/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 = diff --git a/src/lib/structures/satml_types.mli b/src/lib/structures/satml_types.mli index 1109ca820..42eed134c 100644 --- a/src/lib/structures/satml_types.mli +++ b/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