From 8ad78b2acd1257d97f474af7b42a792f7d491225 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 9 Feb 2019 17:12:33 -0600 Subject: [PATCH] refactor: a bit of cleanup for mcsat --- src/core/Internal.ml | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 3bf3bc39..adaef24d 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -850,20 +850,23 @@ module Make(Plugin : PLUGIN) | None -> assert false ) + let mk_atom_mcsat_ st a = + match a.var.v_assignable with + | Some _ -> () + | None -> + let l = ref [] in + Plugin.iter_assignable st.th + (fun t -> l := Lit.make st.st t :: !l) + a.var.pa.lit; + a.var.v_assignable <- Some !l; + () + (* When we have a new literal, we need to first create the list of its subterms. *) let mk_atom st (f:formula) : atom = let res = Atom.make st.st f in if Plugin.mcsat then ( - begin match res.var.v_assignable with - | Some _ -> () - | None -> - let l = ref [] in - Plugin.iter_assignable st.th - (fun t -> l := Lit.make st.st t :: !l) - res.var.pa.lit; - res.var.v_assignable <- Some !l; - end; + mk_atom_mcsat_ st res; ); res