+let rec embed m = function
+ | Ast.Variable name ->
+ (try m, List.assoc name m
+ with Not_found ->
+ let t = Terms.Var ~-(List.length m) in
+ (name,t)::m, t)
+ | Ast.Constant name -> m, Terms.Leaf (hash name)
+ | Ast.Function (name,args) ->
+ let m, args =
+ HExtlib.list_mapi_acc
+ (fun x _ m -> embed m x) m args
+ in
+ m, Terms.Node (Terms.Leaf (hash name):: args)
+;;
+
+let saturate bo (nlit,plit) =
+ let vars,nlit = HExtlib.list_mapi_acc (fun x _ m -> embed m x) [] nlit in
+ let vars,plit = HExtlib.list_mapi_acc (fun x _ m -> embed m x) vars plit in
+ let _, bo = embed vars bo in
+ let bo = Terms.Node (bo :: List.map snd (List.rev vars)) in
+ bo, (nlit, plit)
+;;
+
+let embed t = snd(embed [] t);;
+
+