diff --git a/Makefile.in b/Makefile.in index d28225033bc22035d21534c9b993c2cb4c177e21..fd6d066545eace9da0b84f5883399a8f18c036cd 100644 --- a/Makefile.in +++ b/Makefile.in @@ -50,6 +50,8 @@ OCAMLLIB = @OCAMLLIB@ OCAMLBEST= @OCAMLBEST@ OCAMLVERSION = @OCAMLVERSION@ CAMLP4 = @CAMLP4O@ +PSVIEWER = @PSVIEWER@ +PDFVIEWER = @PDFVIEWER@ INCLUDES = -I src/core -I src/util -I src/parser -I src/output \ -I src/transform -I src @@ -409,8 +411,8 @@ wc: dep: $(MAKE) depend - cat .depend | ocamldot | dot -Tps > dep.ps - gv dep.ps + cat .depend | ocamldot | dot -Tpdf > dep.pdf + $(PDFVIEWER) dep.pdf # distrib ######### diff --git a/configure.in b/configure.in index 5d7dae84510fab8a1fde0d09e600de8b2a77cf9e..16476c2b29816aa015d8328d37a54b328d57c6f7 100644 --- a/configure.in +++ b/configure.in @@ -422,6 +422,10 @@ else fi fi +#Viewer for ps and pdf +AC_CHECK_PROGS(PSVIEWER,gv evince) +AC_CHECK_PROGS(PDFVIEWER,xpdf acroread evince) + # substitutions to perform AC_SUBST(VERBOSEMAKE) AC_SUBST(EXE) @@ -473,6 +477,8 @@ AC_SUBST(MIZARLIB) AC_SUBST(FORPACK) +AC_SUBST(PSVIEWER) +AC_SUBST(PDFVIEWER) # Finally create the Makefile from Makefile.in dnl AC_OUTPUT(Makefile) AC_OUTPUT(Makefile bench/bench) diff --git a/src/core/context_utils.ml b/src/core/context_utils.ml index a09ca1040eef805c1107502e48c27f001c89140b..80b5af9dbeec4c52d545b7731ab4ec8d3b3e321d 100644 --- a/src/core/context_utils.ml +++ b/src/core/context_utils.ml @@ -6,11 +6,5 @@ let cloned_from ctxt i1 i2 = (* Format.printf "@[cloned (%a = %a)?: %a@]@\n" print_ident i2 print_ident i1 print_ctxt ctxt;*) - let rec aux i = - i == i1 || - try - let i3 = Mid.find i ctxt.ctxt_cloned in - List.exists aux i3 - with Not_found -> false - in - aux i2 + try i1 == i2 || Sid.mem i2 (Mid.find i1 ctxt.ctxt_cloned) + with Not_found -> false diff --git a/src/core/theory.ml b/src/core/theory.ml index 0ea70f99aad216b6c5e5dfea4c5a083df1579a40..a58e6c794e5794ec974a95d0e0b6cda4a95f9a3a 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -145,7 +145,7 @@ and namespace = { and context = { ctxt_decls : (decl * context) option; ctxt_known : decl Mid.t; - ctxt_cloned : ident list Mid.t; + ctxt_cloned : Sid.t Mid.t; ctxt_tag : int; } @@ -340,19 +340,23 @@ let empty_inst = { module Context = struct let empty_context = Hctxt.hashcons { - ctxt_decls = None; - ctxt_known = builtin_known; + ctxt_decls = None; + ctxt_known = builtin_known; ctxt_cloned = Mid.empty; - ctxt_tag = -1; + ctxt_tag = -1; } let push_decl ctxt kn d = + (* get the set of prototype symbols represented by [id] *) + let get_cl m id = try Mid.find id m with Not_found -> Sid.empty in + (* add a new association: [id'] represents [id] *) + let add_cl m (id,id') = + (* from now on [id'] represents [id] and everything + * that [id] represented at the moment of cloning *) + Mid.add id' (Sid.add id (Sid.union (get_cl m id) (get_cl m id'))) m + in let cloned = match d.d_node with - | Dclone l -> List.fold_left - (fun m (i1,i2) -> - let l = try Mid.find i1 m with Not_found -> [] in - Mid.add i1 (i2::l) m) - ctxt.ctxt_cloned l + | Dclone l -> List.fold_left add_cl ctxt.ctxt_cloned l | _ -> ctxt.ctxt_cloned in Hctxt.hashcons { ctxt with @@ -878,7 +882,7 @@ let print_uc fmt uc = print_namespace fmt (Theory.get_namespace uc) let print_ctxt fmt ctxt = fprintf fmt "@[ctxt : cloned : %a@]" (Pp.print_iter2 Mid.iter Pp.semi (Pp.constant_string "->") - print_ident (Pp.print_list Pp.simple_comma print_ident)) + print_ident (Pp.print_iter1 Sid.iter Pp.simple_comma print_ident)) ctxt.ctxt_cloned let print_th fmt th = fprintf fmt "" diff --git a/src/core/theory.mli b/src/core/theory.mli index d64bed6a20446b4c42af75c17c737bfdd0aab7e9..64781e708ef04734bc2c3c2fd5ff041fe2656c16 100644 --- a/src/core/theory.mli +++ b/src/core/theory.mli @@ -97,7 +97,7 @@ and namespace = private { and context = private { ctxt_decls : (decl * context) option; ctxt_known : decl Mid.t; - ctxt_cloned : ident list Mid.t; + ctxt_cloned : Sid.t Mid.t; ctxt_tag : int; } diff --git a/src/transform/inlining.ml b/src/transform/inlining.ml index 67ea2bdf8a34b46a3b4008b9ad268f23b9403cda..efd5273531fab6acd2c85ba42a69d81d441adba1 100644 --- a/src/transform/inlining.ml +++ b/src/transform/inlining.ml @@ -12,14 +12,14 @@ type env = { fs : (vsymbol list * term) Mls.t; let empty_env = { fs = Mls.empty; ps = Mls.empty} open Format - +(* let print_env fmt env = let print_map iter pterm pfs = Pp.print_iter2 iter Pp.newline Pp.comma pfs (Pp.print_pair (Pp.print_list Pp.comma Pretty.print_vsymbol) pterm) in fprintf fmt "fs:@[%a@]@\nps:@[%a@]@\n" (print_map Mls.iter Pretty.print_term Pretty.print_lsymbol) env.fs (print_map Mls.iter Pretty.print_fmla Pretty.print_lsymbol) env.ps - +*) let rec replacet env t = let t = substt env t in match t.t_node with