From 894b08ca7d14aa7e31c35f3acb3903a1c3472a27 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 22 Jul 2006 17:14:13 +0000 Subject: [PATCH] matitaprover --- components/METAS/meta.helm-tptp_grafite.src | 5 + components/Makefile | 1 + components/acic_content/.depend | 4 +- components/binaries/Makefile | 2 +- components/cic/libraryObjects.ml | 58 +- components/cic/libraryObjects.mli | 6 + components/cic_proof_checking/cicPp.ml | 2 + components/content_pres/.depend | 6 +- components/grafite/grafiteAst.ml | 1 + components/grafite/grafiteAstPp.ml | 1 + components/grafite_engine/grafiteEngine.ml | 5 + components/grafite_engine/grafiteTypes.ml | 1 + .../grafite_parser/grafiteDisambiguate.ml | 1 + components/grafite_parser/grafiteParser.ml | 1 + components/library/librarySync.ml | 18 +- .../syntax_extensions/profiling_macros.ml | 3 + components/tactics/autoTactic.ml | 2 + components/tactics/autoTactic.mli | 2 + components/tactics/paramodulation/equality.ml | 107 ++- .../tactics/paramodulation/equality.mli | 5 +- components/tactics/paramodulation/indexing.ml | 10 +- .../tactics/paramodulation/inference.ml | 12 +- .../tactics/paramodulation/saturation.ml | 94 ++- components/tptp_grafite/.depend | 7 + .../tptp2grafite => tptp_grafite}/Makefile | 37 +- .../tptp2grafite => tptp_grafite}/ast.ml | 0 .../tptp2grafite => tptp_grafite}/lexer.mll | 0 components/tptp_grafite/main.ml | 22 + .../tptp2grafite => tptp_grafite}/parser.mly | 0 .../main.ml => tptp_grafite/tptp2grafite.ml} | 85 +-- components/tptp_grafite/tptp2grafite.mli | 29 + .../unit_equality_problems | 0 configure.ac | 1 + matita/.depend | 24 +- matita/Makefile | 12 +- matita/matitaInit.ml | 5 + matita/matitac.ml | 1 + matita/tests/TPTP/elenco_unsatisfiable.txt | 698 ++++++++++++++++++ matita/tests/TPTP/try.sh | 23 +- 39 files changed, 1119 insertions(+), 172 deletions(-) create mode 100644 components/METAS/meta.helm-tptp_grafite.src create mode 100644 components/tptp_grafite/.depend rename components/{binaries/tptp2grafite => tptp_grafite}/Makefile (51%) rename components/{binaries/tptp2grafite => tptp_grafite}/ast.ml (100%) rename components/{binaries/tptp2grafite => tptp_grafite}/lexer.mll (100%) create mode 100644 components/tptp_grafite/main.ml rename components/{binaries/tptp2grafite => tptp_grafite}/parser.mly (100%) rename components/{binaries/tptp2grafite/main.ml => tptp_grafite/tptp2grafite.ml} (85%) create mode 100644 components/tptp_grafite/tptp2grafite.mli rename components/{binaries/tptp2grafite => tptp_grafite}/unit_equality_problems (100%) create mode 100644 matita/tests/TPTP/elenco_unsatisfiable.txt diff --git a/components/METAS/meta.helm-tptp_grafite.src b/components/METAS/meta.helm-tptp_grafite.src new file mode 100644 index 000000000..4c1675626 --- /dev/null +++ b/components/METAS/meta.helm-tptp_grafite.src @@ -0,0 +1,5 @@ +requires="helm-acic_content helm-grafite helm-lexicon" +version="0.0.1" +archive(byte)="tptp_grafite.cma" +archive(native)="tptp_grafite.cmxa" +linkopts="" diff --git a/components/Makefile b/components/Makefile index 948ba8f36..cfe1fd517 100644 --- a/components/Makefile +++ b/components/Makefile @@ -32,6 +32,7 @@ MODULES = \ lexicon \ grafite_engine \ grafite_parser \ + tptp_grafite \ $(NULL) METAS = $(MODULES:%=METAS/META.helm-%) diff --git a/components/acic_content/.depend b/components/acic_content/.depend index f6399321e..a0f6ba9ca 100644 --- a/components/acic_content/.depend +++ b/components/acic_content/.depend @@ -25,6 +25,6 @@ acic2astMatcher.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationPp.cmi \ acic2astMatcher.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \ acic2astMatcher.cmi termAcicContent.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationPp.cmi \ - acic2astMatcher.cmi termAcicContent.cmi + acic2content.cmi acic2astMatcher.cmi termAcicContent.cmi termAcicContent.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationPp.cmx \ - acic2astMatcher.cmx termAcicContent.cmi + acic2content.cmx acic2astMatcher.cmx termAcicContent.cmi diff --git a/components/binaries/Makefile b/components/binaries/Makefile index 0f79acfe4..a2b89ee97 100644 --- a/components/binaries/Makefile +++ b/components/binaries/Makefile @@ -1,6 +1,6 @@ H=@ -BINARIES=extractor table_creator utilities saturate tptp2grafite +BINARIES=extractor table_creator utilities saturate all: $(BINARIES:%=rec@all@%) opt: $(BINARIES:%=rec@opt@%) diff --git a/components/cic/libraryObjects.ml b/components/cic/libraryObjects.ml index 7a4112ad5..dc36636fe 100644 --- a/components/cic/libraryObjects.ml +++ b/components/cic/libraryObjects.ml @@ -55,17 +55,23 @@ let insert_unique e extract l = let set_default what l = match what,l with - "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;eq_ind_r_URI] -> + "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI; + eq_ind_r_URI;eq_f_URI;eq_f_sym_URI] -> eq_URIs_ref := - insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,eq_ind_r_URI) - (fun x,_,_,_,_ -> x) !eq_URIs_ref + insert_unique + (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI, + eq_ind_r_URI,eq_f_URI,eq_f_sym_URI) + (fun x,_,_,_,_,_,_ -> x) !eq_URIs_ref | "true",[true_URI] -> true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref | "false",[false_URI] -> false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref | "absurd",[absurd_URI] -> absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref - | _,_ -> raise (NotRecognized what) + | _,l -> + raise + (NotRecognized (what^" with "^string_of_int(List.length l)^" params")) +;; let reset_defaults () = eq_URIs_ref := default_eq_URIs; @@ -76,11 +82,11 @@ let reset_defaults () = (**** LOOKUP FUNCTIONS ****) let eq_URI () = - try let eq,_,_,_,_ = List.hd !eq_URIs_ref in Some eq + try let eq,_,_,_,_,_,_ = List.hd !eq_URIs_ref in Some eq with Failure "hd" -> None let is_eq_URI uri = - List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref + List.exists (fun (eq,_,_,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref let is_eq_refl_URI uri = let urieq = UriManager.strip_xpointer uri in @@ -89,39 +95,63 @@ let is_eq_refl_URI uri = ;; let is_eq_ind_URI uri = - List.exists (fun (_,_,_,eq_ind,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref + List.exists (fun (_,_,_,eq_ind,_,_,_) -> UriManager.eq eq_ind uri) !eq_URIs_ref let is_eq_ind_r_URI uri = - List.exists (fun (_,_,_,_,eq_ind_r) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref + List.exists (fun (_,_,_,_,eq_ind_r,_,_) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref let is_trans_eq_URI uri = - List.exists (fun (_,_,trans_eq,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref + List.exists (fun (_,_,trans_eq,_,_,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref let is_sym_eq_URI uri = - List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref + List.exists (fun (_,sym_eq,_,_,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref +let is_eq_f_URI uri = + List.exists (fun (_,_,_,_,_,eq_f,_) -> UriManager.eq eq_f uri) !eq_URIs_ref +let is_eq_f_sym_URI uri = + List.exists (fun (_,_,_,_,_,_,eq_f1) -> UriManager.eq eq_f1 uri) !eq_URIs_ref + + let eq_refl_URI ~eq:uri = let uri = UriManager.strip_xpointer uri in UriManager.uri_of_string (UriManager.string_of_uri uri ^ "#xpointer(1/1/1)") let sym_eq_URI ~eq:uri = try - let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,x,_,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let trans_eq_URI ~eq:uri = try - let _,_,x,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,_,x,_,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let eq_ind_URI ~eq:uri = try - let _,_,_,x,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,_,_,x,_,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let eq_ind_r_URI ~eq:uri = try - let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + let _,_,_,_,x,_,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) + +let eq_f_URI ~eq:uri = + try + let _,_,_,_,_,x,_ = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) +let eq_f_sym_URI ~eq:uri = + try + let _,_,_,_,_,_,x = List.find (fun eq,_,_,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) + + +let eq_URI_of_eq_f_URI eq_f_URI = + try + let x,_,_,_,_,_,_ = + List.find (fun _,_,_,_,_,u,_ -> UriManager.eq eq_f_URI u) !eq_URIs_ref + in x + with Not_found -> raise (NotRecognized (UriManager.string_of_uri eq_f_URI)) + let true_URI () = try Some (List.hd !true_URIs_ref) with Failure "hd" -> None let false_URI () = diff --git a/components/cic/libraryObjects.mli b/components/cic/libraryObjects.mli index 9dfe54902..0cd9f2e97 100644 --- a/components/cic/libraryObjects.mli +++ b/components/cic/libraryObjects.mli @@ -34,6 +34,10 @@ val is_eq_ind_URI : UriManager.uri -> bool val is_eq_ind_r_URI : UriManager.uri -> bool val is_trans_eq_URI : UriManager.uri -> bool val is_sym_eq_URI : UriManager.uri -> bool +val is_eq_f_URI : UriManager.uri -> bool +val is_eq_f_sym_URI : UriManager.uri -> bool + +val eq_URI_of_eq_f_URI : UriManager.uri -> UriManager.uri exception NotRecognized of string;; @@ -42,6 +46,8 @@ val eq_ind_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri val trans_eq_URI : eq:UriManager.uri -> UriManager.uri val sym_eq_URI : eq:UriManager.uri -> UriManager.uri +val eq_f_URI : eq:UriManager.uri -> UriManager.uri +val eq_f_sym_URI : eq:UriManager.uri -> UriManager.uri val false_URI : unit -> UriManager.uri option diff --git a/components/cic_proof_checking/cicPp.ml b/components/cic_proof_checking/cicPp.ml index e44c6b588..feca7c3cf 100644 --- a/components/cic_proof_checking/cicPp.ml +++ b/components/cic_proof_checking/cicPp.ml @@ -80,8 +80,10 @@ let rec pp t l = UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l | C.Meta (n,l1) -> "?" ^ (string_of_int n) ^ "[" ^ +(* String.concat " ; " (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^ +*) "]" | C.Sort s -> (match s with diff --git a/components/content_pres/.depend b/components/content_pres/.depend index d16c75a76..2de502ee5 100644 --- a/components/content_pres/.depend +++ b/components/content_pres/.depend @@ -1,5 +1,5 @@ cicNotationPres.cmi: mpresentation.cmi box.cmi -boxPp.cmi: cicNotationPres.cmi +boxPp.cmi: mpresentation.cmi cicNotationPres.cmi box.cmi content2pres.cmi: cicNotationPres.cmi sequent2pres.cmi: cicNotationPres.cmi renderingAttrs.cmo: renderingAttrs.cmi @@ -30,8 +30,8 @@ content2pres.cmo: termContentPres.cmi renderingAttrs.cmi mpresentation.cmi \ cicNotationPres.cmi box.cmi content2pres.cmi content2pres.cmx: termContentPres.cmx renderingAttrs.cmx mpresentation.cmx \ cicNotationPres.cmx box.cmx content2pres.cmi -objPp.cmo: content2pres.cmi boxPp.cmi objPp.cmi -objPp.cmx: content2pres.cmx boxPp.cmx objPp.cmi +objPp.cmo: content2pres.cmi cicNotationPres.cmi boxPp.cmi objPp.cmi +objPp.cmx: content2pres.cmx cicNotationPres.cmx boxPp.cmx objPp.cmi sequent2pres.cmo: termContentPres.cmi mpresentation.cmi cicNotationPres.cmi \ box.cmi sequent2pres.cmi sequent2pres.cmx: termContentPres.cmx mpresentation.cmx cicNotationPres.cmx \ diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index d38943da1..246df11c2 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -116,6 +116,7 @@ type 'obj command = | Include of loc * string | Set of loc * string * string | Drop of loc + | Print of loc * string | Qed of loc | Coercion of loc * UriManager.uri * bool (* add composites *) | Obj of loc * 'obj diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index d35a8af11..4a94152de 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -207,6 +207,7 @@ let pp_command ~obj_pp = function | Include (_,path) -> "include \"" ^ path ^ "\"" | Qed _ -> "qed" | Drop _ -> "drop" + | Print (_,s) -> "print " ^ s | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites | Obj (_,obj) -> obj_pp obj diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index ab43c6cc1..d99ab8593 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -582,6 +582,11 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status let status,cmd = disambiguate_command status (text,prefix_len,cmd) in let status,uris = match cmd with + | GrafiteAst.Print (_,"proofterm") -> + let _,_,p,_ = GrafiteTypes.get_current_proof status in + print_endline (AutoTactic.pp_proofterm p); + status,[] + | GrafiteAst.Print (_,_) -> status,[] | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; GrafiteTypes.add_moo_content [cmd] status,[] diff --git a/components/grafite_engine/grafiteTypes.ml b/components/grafite_engine/grafiteTypes.ml index 0c02e1b6c..0d59e4b46 100644 --- a/components/grafite_engine/grafiteTypes.ml +++ b/components/grafite_engine/grafiteTypes.ml @@ -62,6 +62,7 @@ type status = { let get_current_proof status = match status.proof_status with | Incomplete_proof { proof = p } -> p + | Proof p -> p | _ -> raise (Statement_error "no ongoing proof") let get_proof_metasenv status = diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 76e5e6d86..04521361d 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -294,6 +294,7 @@ let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)= | GrafiteAst.Coercion _ | GrafiteAst.Default _ | GrafiteAst.Drop _ + | GrafiteAst.Print _ | GrafiteAst.Include _ | GrafiteAst.Qed _ | GrafiteAst.Set _ as cmd -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index fadecd61e..13ee7297e 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -467,6 +467,7 @@ EXTEND IDENT "set"; n = QSTRING; v = QSTRING -> GrafiteAst.Set (loc, n, v) | IDENT "drop" -> GrafiteAst.Drop loc + | IDENT "print"; s = IDENT -> GrafiteAst.Print (loc,s) | IDENT "qed" -> GrafiteAst.Qed loc | IDENT "variant" ; name = IDENT; SYMBOL ":"; typ = term; SYMBOL <:unicode> ; newname = IDENT -> diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index a59294aaa..338e84bbe 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -59,6 +59,12 @@ let paths_and_uris_of_obj uri = xmlunivgraphpath, univgraphuri let save_object_to_disk uri obj ugraph univlist = + let write f x = + if not (Helm_registry.get_opt_default + Helm_registry.bool "matita.nodisk" ~default:false) + then + f x + in let ensure_path_exists path = let dir = Filename.dirname path in HExtlib.mkdir dir @@ -74,11 +80,11 @@ let save_object_to_disk uri obj ugraph univlist = xmlunivgraphpath, univgraphuri = paths_and_uris_of_obj uri in - List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]); + write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]); (* now write to disk *) - ensure_path_exists xmlpath; - Xml.pp ~gzip:true xml (Some xmlpath); - CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph univlist; + write ensure_path_exists xmlpath; + write (Xml.pp ~gzip:true xml) (Some xmlpath); + write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist; (* we return a list of uri,path we registered/created *) (uri,xmlpath) :: (univgraphuri,xmlunivgraphpath) :: @@ -86,8 +92,8 @@ let save_object_to_disk uri obj ugraph univlist = (match bodyxml,bodyuri with None,_ -> [] | Some bodyxml,Some bodyuri-> - ensure_path_exists xmlbodypath; - Xml.pp ~gzip:true bodyxml (Some xmlbodypath); + write ensure_path_exists xmlbodypath; + write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath); [bodyuri, xmlbodypath] | _-> assert false) diff --git a/components/syntax_extensions/profiling_macros.ml b/components/syntax_extensions/profiling_macros.ml index 479e67381..9f5034a58 100644 --- a/components/syntax_extensions/profiling_macros.ml +++ b/components/syntax_extensions/profiling_macros.ml @@ -72,8 +72,11 @@ let profile_stop _ label = stop label extra ;; +(* Quotation.add "profiler" (Quotation.ExStr banner);; Quotation.add "profile" (Quotation.ExStr profile_start_stop);; Quotation.add "start" (Quotation.ExStr profile_start);; Quotation.add "stop" (Quotation.ExStr profile_stop);; Quotation.add "show" (Quotation.ExStr profile_show);; +*) + diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index d4dc5592c..f063eeafb 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -494,3 +494,5 @@ let applyS_tac ~dbd ~term = | CicUnification.UnificationFailure msg | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) + +let pp_proofterm = Equality.pp_proofterm;; diff --git a/components/tactics/autoTactic.mli b/components/tactics/autoTactic.mli index 1dfe0e2a9..354b1b738 100644 --- a/components/tactics/autoTactic.mli +++ b/components/tactics/autoTactic.mli @@ -30,3 +30,5 @@ val auto_tac: ProofEngineTypes.tactic val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic + +val pp_proofterm: Cic.term -> string diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 368a80f5d..0b0b73e3f 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let _profiler = <:profiler<_profiler>>;; +(* let _profiler = <:profiler<_profiler>>;; *) (* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *) @@ -94,7 +94,8 @@ let string_of_equality ?env eq = id w (CicPp.ppterm ty) (CicPp.ppterm left) (Utils.string_of_comparison o) (CicPp.ppterm right) - (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) + (*(String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))*) + "..." | Some (_, context, _) -> let names = Utils.names_of_context context in let w, _, (ty, left, right, o), m , id = open_equality eq in @@ -102,7 +103,8 @@ let string_of_equality ?env eq = id w (CicPp.pp ty names) (CicPp.pp left names) (Utils.string_of_comparison o) (CicPp.pp right names) - (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) +(* (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *) + "..." ;; let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) = @@ -326,10 +328,9 @@ let canonical t context menv = (canonical context (mk_sym uri_sym ty m r p2)) (canonical context (mk_sym uri_sym ty l m p1)) | Cic.Appl (([Cic.Const(uri_feq,ens);ty1;ty2;f;x;y;p])) -> - - let eq_f_sym = - Cic.Const (UriManager.uri_of_string - "cic:/matita/logic/equality/eq_f1.con",[]) + let eq = LibraryObjects.eq_URI_of_eq_f_URI uri_feq in + let eq_f_sym = + Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, []) in Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p])) @@ -509,9 +510,8 @@ let contextualize uri ty left right t = | t -> (* let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in *) (* let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in *) - let uri_feq = - UriManager.uri_of_string "cic:/matita/logic/equality/eq_f.con" - in + + let uri_feq = LibraryObjects.eq_f_URI ~eq:uri in let pred = (* let r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in *) let l = @@ -599,7 +599,7 @@ let parametrize_proof p l r ty = (fun (instance,p,n) m -> (instance@[m], Cic.Lambda - (Cic.Name ("x"^string_of_int n), + (Cic.Name ("X"^string_of_int n), CicSubstitution.lift (lift_no - n - 1) (ty_of_m m), p), n+1)) @@ -636,12 +636,14 @@ let string_of_id names id = | Exact t -> Printf.sprintf "%d = %s: %s = %s [%s]" id (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names) - (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) + "..." +(* (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *) | Step (_,(step,id1, (_,id2), _) ) -> Printf.sprintf "%6d: %s %6d %6d %s = %s [%s]" id (string_of_rule step) id1 id2 (CicPp.pp l names) (CicPp.pp r names) - (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) +(* (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) *) + "..." with Not_found -> assert false @@ -1141,7 +1143,7 @@ module IntSet = Set.Make(IntOT);; let n_purged = ref 0;; let collect alive1 alive2 alive3 = - let _ = <:start> in +(* let _ = <:start> in *) let deps_of id = let p,_,_ = proof_of_id id in match p with @@ -1164,14 +1166,87 @@ let collect alive1 alive2 alive3 = in n_purged := !n_purged + List.length to_purge; List.iter (Hashtbl.remove id_to_eq) to_purge; - let _ = <:stop> in () +(* let _ = <:stop> in () *) ;; let id_of e = let _,_,_,_,id = open_equality e in id ;; -let get_stats () = +let get_stats () = "" +(* <:show> ^ "# of purged eq by the collector: " ^ string_of_int !n_purged ^ "\n" +*) +;; + +let rec pp_proofterm name t context = + let rec skip_lambda tys ctx = function + | Cic.Lambda (n,s,t) -> skip_lambda (s::tys) ((Some n)::ctx) t + | t -> ctx,tys,t + in + let rename s name = + match name with + | Cic.Name s1 -> Cic.Name (s ^ s1) + | _ -> assert false + in + let rec skip_letin ctx = function + | Cic.LetIn (n,b,t) -> + pp_proofterm (Some (rename "Lemma " n)) b ctx:: + skip_letin ((Some n)::ctx) t + | t -> + let ppterm t = CicPp.pp t ctx in + let rec pp inner = function + | Cic.Appl [Cic.Const (uri,[]);_;l;m;r;p1;p2] + when Pcre.pmatch ~pat:"trans_eq" (UriManager.string_of_uri uri)-> + if not inner then + (" " ^ ppterm l) :: pp true p1 @ + [ " = " ^ ppterm m ] @ pp true p2 @ + [ " = " ^ ppterm r ] + else + pp true p1 @ + [ " = " ^ ppterm m ] @ pp true p2 + | Cic.Appl [Cic.Const (uri,[]);_;l;m;p] + when Pcre.pmatch ~pat:"sym_eq" (UriManager.string_of_uri uri)-> + pp true p + | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] + when Pcre.pmatch ~pat:"eq_f" (UriManager.string_of_uri uri)-> + pp true p + | Cic.Appl [Cic.Const (uri,[]);_;_;_;_;_;p] + when Pcre.pmatch ~pat:"eq_f1" (UriManager.string_of_uri uri)-> + pp true p + | Cic.Appl [Cic.MutConstruct (uri,_,_,[]);_;_;t;p] + when Pcre.pmatch ~pat:"ex.ind" (UriManager.string_of_uri uri)-> + [ "witness " ^ ppterm t ] @ pp true p + | Cic.Appl (t::_) ->[ " [by " ^ ppterm t ^ "]"] + | t ->[ " [by " ^ ppterm t ^ "]"] + in + let rec compat = function + | a::b::tl -> (b ^ a) :: compat tl + | h::[] -> [h] + | [] -> [] + in + let compat l = List.hd l :: compat (List.tl l) in + compat (pp false t) @ ["";""] + in + let names, tys, body = skip_lambda [] context t in + let ppname name = (match name with Some (Cic.Name s) -> s | _ -> "") in + ppname name ^ ":\n" ^ + (if context = [] then + let rec pp_l ctx = function + | (t,name)::tl -> + " " ^ ppname name ^ ": " ^ CicPp.pp t ctx ^ "\n" ^ + pp_l (name::ctx) tl + | [] -> "\n\n" + in + pp_l [] (List.rev (List.combine tys names)) + else "") + ^ + String.concat "\n" (skip_letin names body) ;; + +let pp_proofterm t = + "\n\n" ^ + pp_proofterm (Some (Cic.Name "Hypothesis")) t [] +;; + diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli index 019578ccc..1a909dfc4 100644 --- a/components/tactics/paramodulation/equality.mli +++ b/components/tactics/paramodulation/equality.mli @@ -39,6 +39,8 @@ val pp_proof: (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int -> Cic.term -> string +val pp_proofterm: Cic.term -> string + val reset : unit -> unit val mk_equality : @@ -71,7 +73,8 @@ val build_goal_proof: UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> Cic.context -> Cic.metasenv -> Cic.term * Cic.term list -val build_proof_term : UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term +val build_proof_term : + UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term (** ensures that metavariables in equality are unique *) val fix_metas_goal: int -> goal -> int * goal diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index a4bdef1a2..f3af1b482 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let _profiler = <:profiler<_profiler>>;; +(* let _profiler = <:profiler<_profiler>>;; *) (* $Id$ *) @@ -180,15 +180,9 @@ let get_candidates ?env mode tree term = let s = match mode with | Matching -> - let _ = <:start> in - <:stop> | Unification -> - let _ = <:start> in - <:stop> in Index.PosEqSet.elements s @@ -1039,4 +1033,4 @@ let rec demodulation_goal env table goal = | None -> do_right () ;; -let get_stats () = <:show> ;; +let get_stats () = "" ;; diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index 408a7cdb8..f04024122 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let _profiler = <:profiler<_profiler>>;; +(* let _profiler = <:profiler<_profiler>>;; *) (* $Id$ *) @@ -320,10 +320,10 @@ let equations_blacklist = let equations_blacklist = UriManager.UriSet.empty;; let tty_of_u u = - let _ = <:start> in +(* let _ = <:start> in *) let t = CicUtil.term_of_uri u in let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - let _ = <:stop> in +(* let _ = <:stop> in *) t, ty ;; @@ -336,7 +336,7 @@ let find_library_equalities caso_strano dbd context status maxmeta = let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in - let _ = <:start> in +(* let _ = <:start> in *) let signature = if caso_strano then begin @@ -364,7 +364,7 @@ let find_library_equalities caso_strano dbd context status maxmeta = None in let eqs = (MetadataQuery.equations_for_goal ~dbd ?signature status) in - let _ = <:stop> in +(* let _ = <:stop> in *) let candidates = List.fold_left (fun l uri -> @@ -520,4 +520,4 @@ let find_context_hypotheses env equalities_indexes = res ;; -let get_stats () = <:show> ;; +let get_stats () = "" (*<:show>*) ;; diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index c40b4a9ac..021afb5ab 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -23,7 +23,7 @@ * http://cs.unibo.it/helm/. *) -let _profiler = <:profiler<_profiler>>;; +(* let _profiler = <:profiler<_profiler>>;; *) (* $Id$ *) @@ -174,9 +174,11 @@ let rec select env g passive = if w < 30 then hd, (tl, EqualitySet.remove hd pos_set) else +(* (prerr_endline ("+++ skipping giant of size "^string_of_int w^" +++"); - select env g (tl@[hd],pos_set)) +*) + select env g (tl@[hd],pos_set) | _ -> assert false in skip_giant pos_list pos_set) @@ -265,8 +267,10 @@ let filter_dependent passive id = (eq::list, set), no) pos_list (([],pos_set),0) in +(* if no_pruned > 0 then prerr_endline ("+++ pruning "^ string_of_int no_pruned ^" passives +++"); +*) passive ;; @@ -355,11 +359,11 @@ let infer eq_uri env current (active_list, active_table) = let maxm, copy_of_current = Equality.fix_metas !maxmeta current in maxmeta := maxm; let active_table = Indexing.index active_table copy_of_current in - let _ = <:start> in +(* let _ = <:start> in *) let maxm, res = Indexing.superposition_right eq_uri !maxmeta env active_table current in - let _ = <:stop> in +(* let _ = <:stop> in *) if Utils.debug_metas then ignore(List.map (function current -> @@ -386,9 +390,9 @@ let infer eq_uri env current (active_list, active_table) = maxmeta := maxm; *) let curr_table = Indexing.index Indexing.empty current in - let _ = <:start> in +(* let _ = <:start> in *) let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in - let _ = <:stop> in +(* let _ = <:stop> in *) if Utils.debug_metas then ignore(List.map (function current -> @@ -814,11 +818,13 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = (* match Indexing.subsumption env table goal_equation with*) match Indexing.unification env table goal_equation with | Some (subst, equality, swapped ) -> +(* prerr_endline - ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env); + ("GOAL SUBSUMED IS: "^Equality.string_of_equality goal_equation ~env); prerr_endline - ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env); - prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst); + ("GOAL IS SUBSUMED BY: "^Equality.string_of_equality equality ~env); + prerr_endline ("SUBST:"^Subst.ppsubst ~names subst); +*) let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in let p = @@ -899,8 +905,10 @@ let infer_goal_set env active goals = | [] -> active_goals, [] | hd::tl -> let changed,selected = simplify_goal env hd active in +(* if changed then prerr_endline ("--------------- goal semplificato"); +*) let (_,_,t1) = selected in let already_in = List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1) @@ -967,6 +975,13 @@ let pp_goals label goals context = (snd goals); ;; +let print_status iterno goals active passive = + print_endline + (Printf.sprintf "\n%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)" + iterno (size_of_active active) (size_of_passive passive) + (size_of_goal_set_a goals) (size_of_goal_set_p goals)) +;; + (** given-clause algorithm with full reduction strategy: NEW implementation *) (* here goals is a set of goals in OR *) let given_clause @@ -989,17 +1004,9 @@ let given_clause else if Unix.gettimeofday () > max_time then (ParamodulationFailure "No more time to spend") else -(* - let _ = prerr_endline "simpl goal with active" in - let _ = <:start> in - let goals = simplify_goal_set env goals passive active in - let _ = <:stop> in -*) let _ = - prerr_endline - (Printf.sprintf "%d #ACTIVES: %d #PASSIVES: %d #GOALSET: %d(%d)\n" - iterno (size_of_active active) (size_of_passive passive) - (size_of_goal_set_a goals) (size_of_goal_set_p goals)) +(* print_status iterno goals active passive *) + Printf.printf ".%!"; in (* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *) let passive = @@ -1018,8 +1025,8 @@ let given_clause in match check_if_goals_set_is_solved env active goals with | Some p -> - prerr_endline - (Printf.sprintf "Found a proof in: %f\n" + print_endline + (Printf.sprintf "\nFound a proof in: %f\n" (Unix.gettimeofday() -. initial_time)); ParamodulationSuccess p | None -> @@ -1035,6 +1042,7 @@ let given_clause (* COLLECTION OF GARBAGED EQUALITIES *) if iterno mod 40 = 0 then begin + print_status iterno goals active passive; let active = List.map Equality.id_of (fst active) in let passive = List.map Equality.id_of (fst passive) in let goal = ids_of_goal_set goals in @@ -1042,24 +1050,21 @@ let given_clause end; let current, passive = select env goals passive in (* SIMPLIFICATION OF CURRENT *) +(* prerr_endline ("Selected : " ^ Equality.string_of_equality ~env current); +*) let res = forward_simplify eq_uri env current active in match res with | None -> step goals theorems passive active (iterno+1) | Some current -> -(* - prerr_endline - ("Selected simpl: " ^ - Equality.string_of_equality ~env current); -*) (* GENERATION OF NEW EQUATIONS *) - prerr_endline "infer"; +(* prerr_endline "infer"; *) let new' = infer eq_uri env current active in - prerr_endline "infer goal"; +(* prerr_endline "infer goal"; *) (* match check_if_goals_set_is_solved env active goals with | Some p -> @@ -1077,7 +1082,7 @@ let given_clause infer_goal_set_with_current env current goals active in (* FORWARD AND BACKWARD SIMPLIFICATION *) - prerr_endline "fwd/back simpl"; +(* prerr_endline "fwd/back simpl"; *) let rec simplify new' active passive head = let new' = forward_simplify_new eq_uri env new' active @@ -1098,12 +1103,12 @@ let given_clause let active, passive, new', head = simplify new' active passive [] in - prerr_endline "simpl goal with new"; +(* prerr_endline "simpl goal with new"; *) let goals = let a,b,_ = build_table new' in - let _ = <:start> in +(* let _ = <:start> in *) let rc = simplify_goal_set env goals (a,b) in - let _ = <:stop> in +(* let _ = <:stop> in *) rc in let passive = add_to_passive passive new' head in @@ -1289,13 +1294,15 @@ let saturate raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s))) | ParamodulationSuccess (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) -> - prerr_endline "OK, found a proof!"; - prerr_endline + print_endline "Proof:"; + print_endline (Equality.pp_proof names goalproof newproof subsumption_subst subsumption_id type_of_goal); - prerr_endline "ENDOFPROOFS___"; +(* prerr_endline "ENDOFPROOFS"; *) +(* prerr_endline ("max weight: " ^ (string_of_int (Equality.max_weight goalproof newproof))); +*) (* generation of the CIC proof *) let side_effects = List.filter (fun i -> i <> goalno) @@ -1308,7 +1315,7 @@ let saturate eq_uri goalproof initial type_of_goal side_effects context proof_menv in - prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); +(* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *) let goal_proof = Subst.apply_subst subsumption_subst goal_proof in let metas_still_open_in_proof = Utils.metas_of_term goal_proof in (*prerr_endline (CicPp.pp goal_proof names);*) @@ -1318,7 +1325,7 @@ let saturate List.map (Subst.apply_subst subsumption_subst) side_effects_t in (* replacing fake mets with real ones *) - prerr_endline "replacing metas..."; +(* prerr_endline "replacing metas..."; *) let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in let goal_proof_menv, what, with_what,free_meta = List.fold_left @@ -1351,7 +1358,8 @@ let saturate (ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv:goal_proof_menv) in -prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_metas) ); +(* prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int + * free_metas) ); *) (* check/refine/... build the new proof *) let replaced_goal = ProofEngineReduction.replace @@ -1376,7 +1384,7 @@ prerr_endline ("freemetas: " ^ String.concat "," (List.map string_of_int free_me let final_subst = (goalno,(context,goal_proof,type_of_goal))::subst_side_effects in -prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); +(* prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); *) let _ = try CicTypeChecker.type_of_aux' real_menv context goal_proof @@ -1398,12 +1406,14 @@ prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); let open_goals = match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[] in +(* Printf.eprintf "GOALS APERTI: %s\nMETASENV PRIMA:\n%s\nMETASENV DOPO:\n%s\n" (String.concat ", " (List.map string_of_int open_goals)) (CicMetaSubst.ppmetasenv [] metasenv) (CicMetaSubst.ppmetasenv [] real_metasenv); - prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time); +*) + print_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time); proof, open_goals ;; @@ -1736,8 +1746,10 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = proof,[goalno] ;; -let get_stats () = +let get_stats () = "" +(* <:show> ^ Indexing.get_stats () ^ Inference.get_stats () ^ Equality.get_stats () ;; +*) diff --git a/components/tptp_grafite/.depend b/components/tptp_grafite/.depend new file mode 100644 index 000000000..bc310327f --- /dev/null +++ b/components/tptp_grafite/.depend @@ -0,0 +1,7 @@ +parser.cmi: ast.cmo +lexer.cmo: parser.cmi +lexer.cmx: parser.cmx +parser.cmo: ast.cmo parser.cmi +parser.cmx: ast.cmx parser.cmi +tptp2grafite.cmo: parser.cmi lexer.cmo ast.cmo tptp2grafite.cmi +tptp2grafite.cmx: parser.cmx lexer.cmx ast.cmx tptp2grafite.cmi diff --git a/components/binaries/tptp2grafite/Makefile b/components/tptp_grafite/Makefile similarity index 51% rename from components/binaries/tptp2grafite/Makefile rename to components/tptp_grafite/Makefile index 071bf8ddb..c5c6e6346 100644 --- a/components/binaries/tptp2grafite/Makefile +++ b/components/tptp_grafite/Makefile @@ -1,24 +1,31 @@ -OCAMLC = OCAMLPATH=../../METAS ocamlfind ocamlc -package helm-grafite_parser +PACKAGE = tptp_grafite +PREDICATES = + +INTERFACE_FILES= parser.mli tptp2grafite.mli + +IMPLEMENTATION_FILES = ast.ml lexer.ml $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = +EXTRA_OBJECTS_TO_CLEAN = + TPTPDIR=/home/$(USER)/TPTP-v3.1.1/ -opt all: tptp2grafite - echo -n +all: tptp2grafite +clean: clean_tests -tptp2grafite: ast.ml parser.mly lexer.mll main.ml - $(OCAMLC) -c ast.ml +clean_tests: + rm -f tptp2grafite + +parser.mli parser.ml:parser.mly ocamlyacc parser.mly - $(OCAMLC) -c parser.mli - $(OCAMLC) -c parser.ml +lexer.ml: ocamllex lexer.mll - $(OCAMLC) -c lexer.ml - $(OCAMLC) -c main.ml - $(OCAMLC) -linkpkg -o tptp2grafite ast.cmo lexer.cmo parser.cmo main.cmo -clean: - rm -f tptp2grafite *.cmo *.cmi parser.mli parser.ml lexer.ml rm *.output +LOCAL_LINKOPTS = -package helm-$(PACKAGE) -linkpkg +tptp2grafite: main.ml tptp_grafite.cma + @echo " OCAMLC $<" + @$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< test: tptp2grafite - cat $(TPTPDIR)/`head -n 1 unit_equality_problems` | ./tptp2grafite testall: tptp2grafite for X in `cat unit_equality_problems`; do\ @@ -37,3 +44,7 @@ parse: ./tptp2grafite -tptppath $(TPTPDIR) $$X \ > /dev/null || echo Failed: $$X; \ done + +include ../../Makefile.defs +include ../Makefile.common + diff --git a/components/binaries/tptp2grafite/ast.ml b/components/tptp_grafite/ast.ml similarity index 100% rename from components/binaries/tptp2grafite/ast.ml rename to components/tptp_grafite/ast.ml diff --git a/components/binaries/tptp2grafite/lexer.mll b/components/tptp_grafite/lexer.mll similarity index 100% rename from components/binaries/tptp2grafite/lexer.mll rename to components/tptp_grafite/lexer.mll diff --git a/components/tptp_grafite/main.ml b/components/tptp_grafite/main.ml new file mode 100644 index 000000000..e52b77c43 --- /dev/null +++ b/components/tptp_grafite/main.ml @@ -0,0 +1,22 @@ +(* OPTIONS *) +let tptppath = ref "./";; +let spec = [ + ("-tptppath", + Arg.String (fun x -> tptppath := x), + "Where to find the Axioms/ and Problems/ directory") +] + +(* MAIN *) +let _ = + let usage = "Usage: tptp2grafite [options] file" in + let inputfile = ref "" in + Arg.parse spec (fun s -> inputfile := s) usage; + if !inputfile = "" then + begin + prerr_endline usage; + exit 1 + end; + print_endline + (Tptp2grafite.tptp2grafite ~filename:!inputfile ~tptppath:!tptppath ()); + exit 0 + diff --git a/components/binaries/tptp2grafite/parser.mly b/components/tptp_grafite/parser.mly similarity index 100% rename from components/binaries/tptp2grafite/parser.mly rename to components/tptp_grafite/parser.mly diff --git a/components/binaries/tptp2grafite/main.ml b/components/tptp_grafite/tptp2grafite.ml similarity index 85% rename from components/binaries/tptp2grafite/main.ml rename to components/tptp_grafite/tptp2grafite.ml index 980f2b456..841ac5f5c 100644 --- a/components/binaries/tptp2grafite/main.ml +++ b/components/tptp_grafite/tptp2grafite.ml @@ -177,8 +177,10 @@ let convert_ast statements context = function | A.Negated_conjecture -> assert_formulae_is_1eq_negated f; let fv = collect_fv_from_formulae f in +(* if fv <> [] then prerr_endline ("FREE VARIABLES: " ^ String.concat "," fv); +*) let f = PT.Binder (`Forall, @@ -202,7 +204,10 @@ let convert_ast statements context = function else [])@ [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, GA.Auto (floc,["paramodulation",""])), - Some (GA.Dot(floc))))]@ + Some (GA.Dot(floc)))); + GA.Executable(floc,GA.Tactical(floc, GA.Try(floc, + GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc)))) + ]@ (if fv <> [] then (List.flatten (List.map @@ -212,9 +217,8 @@ let convert_ast statements context = function (GA.Merge floc)))]) fv)) else [])@ - [GA.Executable(floc,GA.Tactical(floc, GA.Try(floc, - GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc)))); - GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))], + [GA.Executable(floc,GA.Command(floc, GA.Print(floc,"proofterm"))); + GA.Executable(floc,GA.Command(floc, GA.Qed(floc)))], context | A.Definition | A.Lemma @@ -225,27 +229,15 @@ let convert_ast statements context = function | A.Unknown -> assert false ;; -(* OPTIONS *) -let tptppath = ref "./";; -let librarymode = ref false;; -let spec = [ - ("-tptppath", - Arg.String (fun x -> tptppath := x), - "Where to find the Axioms/ and Problems/ directory"); - ("-librarymode", - Arg.Set librarymode, - "... not supported yet") -] - (* HELPERS *) -let resolve s = +let resolve ~tptppath s = let resolved_name = if Filename.check_suffix s ".p" then (assert (String.length s > 5); let prefix = String.sub s 0 3 in - !tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s) + tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s) else - !tptppath ^ "/" ^ s + tptppath ^ "/" ^ s in if HExtlib.is_regular resolved_name then resolved_name @@ -257,25 +249,17 @@ let resolve s = ;; (* MAIN *) -let _ = - let usage = "Usage: tptp2grafite [options] file" in - let inputfile = ref "" in - Arg.parse spec (fun s -> inputfile := s) usage; - if !inputfile = "" then - begin - prerr_endline usage; - exit 1 - end; +let tptp2grafite ?raw_preamble ~tptppath ~filename () = let rec aux = function | [] -> [] | ((A.Inclusion (file,_)) as hd) :: tl -> - let file = resolve file in + let file = resolve ~tptppath file in let lexbuf = Lexing.from_channel (open_in file) in let statements = Parser.main Lexer.yylex lexbuf in hd :: aux (statements @ tl) | hd::tl -> hd :: aux tl in - let statements = aux [A.Inclusion (!inputfile ^ ".p",[])] in + let statements = aux [A.Inclusion (filename,[])] in let grafite_ast_statements,_ = List.fold_left (fun (st, ctx) f -> @@ -299,26 +283,37 @@ let _ = CicNotationPp.set_pp_term term_pp; let lazy_term_pp = fun x -> assert false in let obj_pp = CicNotationPp.pp_obj in - print_endline - (GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t) + GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t in + let buri = Pcre.replace ~pat:"\\.p$" ("cic:/matita/TPTP/" ^ filename) in let extra_statements_start = [ GA.Executable(floc,GA.Command(floc, - GA.Set(floc,"baseuri","cic:/matita/TPTP/" ^ !inputfile))); - GA.Executable(floc,GA.Command(floc, GA.Include(floc,"logic/equality.ma")))] + GA.Set(floc,"baseuri",buri)))] + in + let preamble = + match raw_preamble with + | None -> + pp (GA.Executable(floc, + GA.Command(floc,GA.Include(floc,"logic/equality.ma")))) + | Some s -> s buri in - List.iter pp extra_statements_start; - List.iter - (fun (n,s) -> - print_endline - (LexiconAstPp.pp_command - (LA.Alias(floc, - LA.Ident_alias(n,s))) ^ ".")) - [(*("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"); + let extra_statements_end = [] in + let aliases = [] + (*[("eq","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"); ("trans_eq","cic:/Coq/Init/Logic/trans_eq.con"); ("eq_ind_r","cic:/Coq/Init/Logic/eq_ind_r.con"); ("eq_ind","cic:/Coq/Init/Logic/eq_ind.con"); ("sym_eq","cic:/Coq/Init/Logic/sym_eq.con"); - ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)") *)]; - List.iter pp grafite_ast_statements; - exit 0 + ("refl_equal","cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)")] *) + in + let s1 = List.map pp extra_statements_start in + let s2 = + List.map + (fun (n,s) -> + LexiconAstPp.pp_command (LA.Alias(floc, LA.Ident_alias(n,s))) ^ ".") + aliases + in + let s3 = List.map pp grafite_ast_statements in + let s4 = List.map pp extra_statements_end in + String.concat "\n" (s1@[preamble]@s2@s3@s4) +;; diff --git a/components/tptp_grafite/tptp2grafite.mli b/components/tptp_grafite/tptp2grafite.mli new file mode 100644 index 000000000..7dfa2d3d0 --- /dev/null +++ b/components/tptp_grafite/tptp2grafite.mli @@ -0,0 +1,29 @@ +(* Copyright (C) 2006, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.cs.unibo.it/ + *) + +val tptp2grafite: + ?raw_preamble:(string -> string) -> + tptppath:string -> filename:string -> unit -> + string diff --git a/components/binaries/tptp2grafite/unit_equality_problems b/components/tptp_grafite/unit_equality_problems similarity index 100% rename from components/binaries/tptp2grafite/unit_equality_problems rename to components/tptp_grafite/unit_equality_problems diff --git a/configure.ac b/configure.ac index d3f381e67..a1f233b6b 100644 --- a/configure.ac +++ b/configure.ac @@ -76,6 +76,7 @@ FINDLIB_COMREQUIRES="\ helm-cic_disambiguation \ helm-grafite \ helm-grafite_engine \ +helm-tptp_grafite \ helm-grafite_parser \ helm-hgdome \ helm-tactics \ diff --git a/matita/.depend b/matita/.depend index b893373e1..f67366bd7 100644 --- a/matita/.depend +++ b/matita/.depend @@ -14,10 +14,10 @@ matitacLib.cmo: matitamakeLib.cmi matitaMisc.cmi matitaInit.cmi \ matitaExcPp.cmi matitaEngine.cmi buildTimeConf.cmi matitacLib.cmi matitacLib.cmx: matitamakeLib.cmx matitaMisc.cmx matitaInit.cmx \ matitaExcPp.cmx matitaEngine.cmx buildTimeConf.cmx matitacLib.cmi -matitac.cmo: matitamake.cmi matitadep.cmi matitaclean.cmi matitacLib.cmi \ - gragrep.cmi -matitac.cmx: matitamake.cmx matitadep.cmx matitaclean.cmx matitacLib.cmx \ - gragrep.cmx +matitac.cmo: matitaprover.cmo matitamake.cmi matitadep.cmi matitaclean.cmi \ + matitacLib.cmi gragrep.cmi +matitac.cmx: matitaprover.cmx matitamake.cmx matitadep.cmx matitaclean.cmx \ + matitacLib.cmx gragrep.cmx matitadep.cmo: matitaInit.cmi matitadep.cmi matitadep.cmx: matitaInit.cmx matitadep.cmi matitaEngine.cmo: matitaEngine.cmi @@ -41,18 +41,20 @@ matitamakeLib.cmx: buildTimeConf.cmx matitamakeLib.cmi matitamake.cmo: matitamakeLib.cmi matitaInit.cmi matitamake.cmi matitamake.cmx: matitamakeLib.cmx matitaInit.cmx matitamake.cmi matitaMathView.cmo: matitaTypes.cmi matitaScript.cmi matitaMisc.cmi \ - matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi buildTimeConf.cmi \ - applyTransformation.cmi matitaMathView.cmi + matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi lablGraphviz.cmi \ + buildTimeConf.cmi applyTransformation.cmi matitaMathView.cmi matitaMathView.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \ - matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitaMathView.cmi + matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx lablGraphviz.cmx \ + buildTimeConf.cmx applyTransformation.cmx matitaMathView.cmi matitaMisc.cmo: buildTimeConf.cmi matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: matitaTypes.cmi matitaScript.cmi matitaMathView.cmi \ - matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi lablGraphviz.cmi \ - buildTimeConf.cmi + matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi buildTimeConf.cmi matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMathView.cmx \ - matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx lablGraphviz.cmx \ + matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx buildTimeConf.cmx +matitaprover.cmo: matitaInit.cmi matitaExcPp.cmi matitaEngine.cmi \ + buildTimeConf.cmi +matitaprover.cmx: matitaInit.cmx matitaExcPp.cmx matitaEngine.cmx \ buildTimeConf.cmx matitaScript.cmo: matitamakeLib.cmi matitaTypes.cmi matitaMisc.cmi \ matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmi \ diff --git a/matita/Makefile b/matita/Makefile index 34bbe6328..46ad75c29 100644 --- a/matita/Makefile +++ b/matita/Makefile @@ -16,7 +16,7 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) INSTALL_PROGRAMS= matita matitac INSTALL_PROGRAMS_LINKS_MATITA= cicbrowser -INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean +INSTALL_PROGRAMS_LINKS_MATITAC= matitadep matitamake matitaclean matitaprover MATITA_FLAGS = -noprofile NODB=false @@ -52,6 +52,7 @@ CCMOS = \ matitaExcPp.cmo \ matitaEngine.cmo \ matitacLib.cmo \ + matitaprover.cmo \ $(NULL) MAINCMOS = \ matitadep.cmo \ @@ -60,7 +61,7 @@ MAINCMOS = \ gragrep.cmo \ $(NULL) PROGRAMS_BYTE = \ - matita matitac cicbrowser matitadep matitaclean matitamake + matita matitac cicbrowser matitadep matitaclean matitamake matitaprover PROGRAMS = $(PROGRAMS_BYTE) matitatop PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE)) NOINST_PROGRAMS = dump_moo gragrep @@ -139,6 +140,11 @@ matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS) $(H)echo " OCAMLC $<" $(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $< +matitaprover: matitac + $(H)test -f $@ || ln -s $< $@ +matitaprover.opt: matitac.opt + $(H)test -f $@ || ln -s $< $@ + matitadep: matitac $(H)test -f $@ || ln -s $< $@ matitadep.opt: matitac.opt @@ -325,6 +331,8 @@ matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml strip $@ matitadep.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ +matitaprover.opt.static: matitac.opt.static + $(H)test -f $@ || ln -s $< $@ matitaclean.opt.static: matitac.opt.static $(H)test -f $@ || ln -s $< $@ matitamake.opt.static: matitac.opt.static diff --git a/matita/matitaInit.ml b/matita/matitaInit.ml index 5866b74d8..a2a5b93fa 100644 --- a/matita/matitaInit.ml +++ b/matita/matitaInit.ml @@ -134,6 +134,11 @@ Options:" "gragrep", sprintf "Grafite Grep v%s Usage: gragrep [ -r ] PATH +Options:" + BuildTimeConf.version; + "matitaprover", + sprintf "Matita's prover v%s +Usage: matitaprover [ -tptppath ] FILE.p Options:" BuildTimeConf.version; "matita", diff --git a/matita/matitac.ml b/matita/matitac.ml index 05add3ce4..ced922a23 100644 --- a/matita/matitac.ml +++ b/matita/matitac.ml @@ -31,6 +31,7 @@ let main () = | "matitadep" | "matitadep.opt" -> Matitadep.main () | "matitaclean" | "matitaclean.opt" -> Matitaclean.main () | "matitamake" | "matitamake.opt" -> Matitamake.main () + | "matitaprover" | "matitaprover.opt" -> Matitaprover.main () | _ -> (* let _ = Paramodulation.Saturation.init () in *) diff --git a/matita/tests/TPTP/elenco_unsatisfiable.txt b/matita/tests/TPTP/elenco_unsatisfiable.txt new file mode 100644 index 000000000..e70ebb599 --- /dev/null +++ b/matita/tests/TPTP/elenco_unsatisfiable.txt @@ -0,0 +1,698 @@ +ALG005-1.p +ALG006-1.p +ALG007-1.p +BOO001-1.p +BOO002-1.p +BOO002-2.p +BOO003-2.p +BOO003-4.p +BOO004-2.p +BOO004-4.p +BOO005-2.p +BOO005-4.p +BOO006-2.p +BOO006-4.p +BOO007-2.p +BOO007-4.p +BOO008-2.p +BOO008-4.p +BOO009-2.p +BOO009-4.p +BOO010-2.p +BOO010-4.p +BOO011-2.p +BOO011-4.p +BOO012-2.p +BOO012-4.p +BOO013-2.p +BOO013-4.p +BOO014-2.p +BOO014-4.p +BOO015-2.p +BOO015-4.p +BOO016-2.p +BOO017-2.p +BOO018-4.p +BOO021-1.p +BOO022-1.p +BOO023-1.p +BOO024-1.p +BOO025-1.p +BOO026-1.p +BOO028-1.p +BOO029-1.p +BOO031-1.p +BOO034-1.p +BOO067-1.p +BOO068-1.p +BOO069-1.p +BOO070-1.p +BOO071-1.p +BOO072-1.p +BOO073-1.p +BOO074-1.p +BOO075-1.p +BOO076-1.p +COL001-1.p +COL001-2.p +COL002-1.p +COL002-4.p +COL002-5.p +COL003-1.p +COL004-1.p +COL004-3.p +COL006-1.p +COL006-5.p +COL006-6.p +COL006-7.p +COL007-1.p +COL008-1.p +COL009-1.p +COL010-1.p +COL011-1.p +COL012-1.p +COL013-1.p +COL014-1.p +COL015-1.p +COL016-1.p +COL017-1.p +COL018-1.p +COL019-1.p +COL020-1.p +COL021-1.p +COL022-1.p +COL023-1.p +COL024-1.p +COL025-1.p +COL026-1.p +COL027-1.p +COL029-1.p +COL030-1.p +COL031-1.p +COL032-1.p +COL033-1.p +COL034-1.p +COL035-1.p +COL036-1.p +COL037-1.p +COL038-1.p +COL039-1.p +COL041-1.p +COL042-1.p +COL042-6.p +COL042-7.p +COL042-8.p +COL042-9.p +COL043-1.p +COL043-3.p +COL044-1.p +COL044-6.p +COL044-7.p +COL044-8.p +COL044-9.p +COL045-1.p +COL046-1.p +COL048-1.p +COL049-1.p +COL050-1.p +COL051-1.p +COL052-1.p +COL053-1.p +COL056-1.p +COL057-1.p +COL058-1.p +COL058-2.p +COL058-3.p +COL059-1.p +COL060-1.p +COL060-2.p +COL060-3.p +COL061-1.p +COL061-2.p +COL061-3.p +COL062-1.p +COL062-2.p +COL062-3.p +COL063-1.p +COL063-2.p +COL063-3.p +COL063-4.p +COL063-5.p +COL063-6.p +COL064-1.p +COL064-2.p +COL064-3.p +COL064-4.p +COL064-5.p +COL064-6.p +COL064-7.p +COL064-8.p +COL064-9.p +COL065-1.p +COL066-1.p +COL066-2.p +COL066-3.p +COL070-1.p +COL075-2.p +COL083-1.p +COL084-1.p +COL085-1.p +COL086-1.p +GRP001-2.p +GRP001-4.p +GRP002-2.p +GRP002-3.p +GRP002-4.p +GRP010-4.p +GRP011-4.p +GRP012-4.p +GRP014-1.p +GRP022-2.p +GRP023-2.p +GRP024-5.p +GRP114-1.p +GRP115-1.p +GRP116-1.p +GRP117-1.p +GRP118-1.p +GRP119-1.p +GRP120-1.p +GRP121-1.p +GRP122-1.p +GRP136-1.p +GRP137-1.p +GRP138-1.p +GRP139-1.p +GRP140-1.p +GRP141-1.p +GRP142-1.p +GRP143-1.p +GRP144-1.p +GRP145-1.p +GRP146-1.p +GRP147-1.p +GRP148-1.p +GRP149-1.p +GRP150-1.p +GRP151-1.p +GRP152-1.p +GRP153-1.p +GRP154-1.p +GRP155-1.p +GRP156-1.p +GRP157-1.p +GRP158-1.p +GRP159-1.p +GRP160-1.p +GRP161-1.p +GRP162-1.p +GRP163-1.p +GRP164-1.p +GRP164-2.p +GRP165-1.p +GRP165-2.p +GRP166-1.p +GRP166-2.p +GRP166-3.p +GRP166-4.p +GRP167-1.p +GRP167-2.p +GRP167-3.p +GRP167-4.p +GRP167-5.p +GRP168-1.p +GRP168-2.p +GRP169-1.p +GRP169-2.p +GRP170-1.p +GRP170-2.p +GRP170-3.p +GRP170-4.p +GRP171-1.p +GRP171-2.p +GRP172-1.p +GRP172-2.p +GRP173-1.p +GRP174-1.p +GRP175-1.p +GRP175-2.p +GRP175-3.p +GRP175-4.p +GRP176-1.p +GRP176-2.p +GRP177-2.p +GRP178-1.p +GRP178-2.p +GRP179-1.p +GRP179-2.p +GRP179-3.p +GRP180-1.p +GRP180-2.p +GRP181-1.p +GRP181-2.p +GRP181-3.p +GRP181-4.p +GRP182-1.p +GRP182-2.p +GRP182-3.p +GRP182-4.p +GRP183-1.p +GRP183-2.p +GRP183-3.p +GRP183-4.p +GRP184-1.p +GRP184-2.p +GRP184-3.p +GRP184-4.p +GRP185-1.p +GRP185-2.p +GRP185-3.p +GRP185-4.p +GRP186-1.p +GRP186-2.p +GRP186-3.p +GRP186-4.p +GRP187-1.p +GRP188-1.p +GRP188-2.p +GRP189-1.p +GRP189-2.p +GRP190-1.p +GRP190-2.p +GRP191-1.p +GRP191-2.p +GRP192-1.p +GRP193-1.p +GRP193-2.p +GRP195-1.p +GRP196-1.p +GRP200-1.p +GRP201-1.p +GRP202-1.p +GRP203-1.p +GRP205-1.p +GRP206-1.p +GRP403-1.p +GRP404-1.p +GRP405-1.p +GRP406-1.p +GRP407-1.p +GRP408-1.p +GRP409-1.p +GRP410-1.p +GRP411-1.p +GRP412-1.p +GRP413-1.p +GRP414-1.p +GRP415-1.p +GRP416-1.p +GRP417-1.p +GRP418-1.p +GRP419-1.p +GRP420-1.p +GRP421-1.p +GRP422-1.p +GRP423-1.p +GRP424-1.p +GRP425-1.p +GRP426-1.p +GRP427-1.p +GRP428-1.p +GRP429-1.p +GRP430-1.p +GRP431-1.p +GRP432-1.p +GRP433-1.p +GRP434-1.p +GRP435-1.p +GRP436-1.p +GRP437-1.p +GRP438-1.p +GRP439-1.p +GRP440-1.p +GRP441-1.p +GRP442-1.p +GRP443-1.p +GRP444-1.p +GRP445-1.p +GRP446-1.p +GRP447-1.p +GRP448-1.p +GRP449-1.p +GRP450-1.p +GRP451-1.p +GRP452-1.p +GRP453-1.p +GRP454-1.p +GRP455-1.p +GRP456-1.p +GRP457-1.p +GRP458-1.p +GRP459-1.p +GRP460-1.p +GRP461-1.p +GRP462-1.p +GRP463-1.p +GRP464-1.p +GRP465-1.p +GRP466-1.p +GRP467-1.p +GRP468-1.p +GRP469-1.p +GRP470-1.p +GRP471-1.p +GRP472-1.p +GRP473-1.p +GRP474-1.p +GRP475-1.p +GRP476-1.p +GRP477-1.p +GRP478-1.p +GRP479-1.p +GRP480-1.p +GRP481-1.p +GRP482-1.p +GRP483-1.p +GRP484-1.p +GRP485-1.p +GRP486-1.p +GRP487-1.p +GRP488-1.p +GRP489-1.p +GRP490-1.p +GRP491-1.p +GRP492-1.p +GRP493-1.p +GRP494-1.p +GRP495-1.p +GRP496-1.p +GRP497-1.p +GRP498-1.p +GRP499-1.p +GRP500-1.p +GRP501-1.p +GRP502-1.p +GRP503-1.p +GRP504-1.p +GRP505-1.p +GRP506-1.p +GRP507-1.p +GRP508-1.p +GRP509-1.p +GRP510-1.p +GRP511-1.p +GRP512-1.p +GRP513-1.p +GRP514-1.p +GRP515-1.p +GRP516-1.p +GRP517-1.p +GRP518-1.p +GRP519-1.p +GRP520-1.p +GRP521-1.p +GRP522-1.p +GRP523-1.p +GRP524-1.p +GRP525-1.p +GRP526-1.p +GRP527-1.p +GRP528-1.p +GRP529-1.p +GRP530-1.p +GRP531-1.p +GRP532-1.p +GRP533-1.p +GRP534-1.p +GRP535-1.p +GRP536-1.p +GRP537-1.p +GRP538-1.p +GRP539-1.p +GRP540-1.p +GRP541-1.p +GRP542-1.p +GRP543-1.p +GRP544-1.p +GRP545-1.p +GRP546-1.p +GRP547-1.p +GRP548-1.p +GRP549-1.p +GRP550-1.p +GRP551-1.p +GRP552-1.p +GRP553-1.p +GRP554-1.p +GRP555-1.p +GRP556-1.p +GRP557-1.p +GRP558-1.p +GRP559-1.p +GRP560-1.p +GRP561-1.p +GRP562-1.p +GRP563-1.p +GRP564-1.p +GRP565-1.p +GRP566-1.p +GRP567-1.p +GRP568-1.p +GRP569-1.p +GRP570-1.p +GRP571-1.p +GRP572-1.p +GRP573-1.p +GRP574-1.p +GRP575-1.p +GRP576-1.p +GRP577-1.p +GRP578-1.p +GRP579-1.p +GRP580-1.p +GRP581-1.p +GRP582-1.p +GRP583-1.p +GRP584-1.p +GRP585-1.p +GRP586-1.p +GRP587-1.p +GRP588-1.p +GRP589-1.p +GRP590-1.p +GRP591-1.p +GRP592-1.p +GRP593-1.p +GRP594-1.p +GRP595-1.p +GRP596-1.p +GRP597-1.p +GRP598-1.p +GRP599-1.p +GRP600-1.p +GRP601-1.p +GRP602-1.p +GRP603-1.p +GRP604-1.p +GRP605-1.p +GRP606-1.p +GRP607-1.p +GRP608-1.p +GRP609-1.p +GRP610-1.p +GRP611-1.p +GRP612-1.p +GRP613-1.p +GRP614-1.p +GRP615-1.p +GRP616-1.p +LAT006-1.p +LAT007-1.p +LAT008-1.p +LAT009-1.p +LAT010-1.p +LAT011-1.p +LAT012-1.p +LAT013-1.p +LAT014-1.p +LAT017-1.p +LAT018-1.p +LAT019-1.p +LAT020-1.p +LAT021-1.p +LAT022-1.p +LAT023-1.p +LAT026-1.p +LAT027-1.p +LAT028-1.p +LAT031-1.p +LAT032-1.p +LAT033-1.p +LAT034-1.p +LAT038-1.p +LAT039-1.p +LAT039-2.p +LAT040-1.p +LAT042-1.p +LAT043-1.p +LAT044-1.p +LAT045-1.p +LAT070-1.p +LAT072-1.p +LAT074-1.p +LAT075-1.p +LAT076-1.p +LAT077-1.p +LAT078-1.p +LAT079-1.p +LAT080-1.p +LAT081-1.p +LAT082-1.p +LAT083-1.p +LAT084-1.p +LAT085-1.p +LAT086-1.p +LAT087-1.p +LAT088-1.p +LAT089-1.p +LAT090-1.p +LAT091-1.p +LAT092-1.p +LAT093-1.p +LAT094-1.p +LAT095-1.p +LAT096-1.p +LAT097-1.p +LAT138-1.p +LAT139-1.p +LAT140-1.p +LAT141-1.p +LAT142-1.p +LAT143-1.p +LAT144-1.p +LAT145-1.p +LAT146-1.p +LAT147-1.p +LAT148-1.p +LAT149-1.p +LAT150-1.p +LAT151-1.p +LAT152-1.p +LAT153-1.p +LAT154-1.p +LAT155-1.p +LAT156-1.p +LAT157-1.p +LAT158-1.p +LAT159-1.p +LAT160-1.p +LAT161-1.p +LAT162-1.p +LAT163-1.p +LAT164-1.p +LAT165-1.p +LAT166-1.p +LAT167-1.p +LAT168-1.p +LAT169-1.p +LAT170-1.p +LAT171-1.p +LAT172-1.p +LAT173-1.p +LAT174-1.p +LAT175-1.p +LAT176-1.p +LAT177-1.p +LCL109-2.p +LCL109-6.p +LCL110-2.p +LCL111-2.p +LCL112-2.p +LCL113-2.p +LCL114-2.p +LCL115-2.p +LCL116-2.p +LCL132-1.p +LCL133-1.p +LCL134-1.p +LCL135-1.p +LCL138-1.p +LCL139-1.p +LCL140-1.p +LCL141-1.p +LCL153-1.p +LCL154-1.p +LCL155-1.p +LCL156-1.p +LCL157-1.p +LCL158-1.p +LCL159-1.p +LCL160-1.p +LCL161-1.p +LCL162-1.p +LCL163-1.p +LCL164-1.p +LDA001-1.p +LDA002-1.p +LDA007-3.p +RNG007-4.p +RNG008-3.p +RNG008-4.p +RNG008-7.p +RNG009-5.p +RNG009-7.p +RNG011-5.p +RNG012-6.p +RNG013-6.p +RNG014-6.p +RNG015-6.p +RNG016-6.p +RNG017-6.p +RNG018-6.p +RNG019-6.p +RNG019-7.p +RNG020-6.p +RNG020-7.p +RNG021-6.p +RNG021-7.p +RNG023-6.p +RNG023-7.p +RNG024-6.p +RNG024-7.p +RNG025-4.p +RNG025-5.p +RNG025-6.p +RNG025-7.p +RNG026-6.p +RNG026-7.p +RNG027-5.p +RNG027-7.p +RNG027-8.p +RNG027-9.p +RNG028-5.p +RNG028-7.p +RNG028-8.p +RNG028-9.p +RNG029-5.p +RNG029-6.p +RNG029-7.p +RNG035-7.p +ROB001-1.p +ROB002-1.p +ROB003-1.p +ROB004-1.p +ROB005-1.p +ROB006-1.p +ROB006-2.p +ROB008-1.p +ROB009-1.p +ROB010-1.p +ROB013-1.p +ROB022-1.p +ROB023-1.p +ROB026-1.p +ROB030-1.p +ROB031-1.p +ROB032-1.p +SYN080-1.p +SYN083-1.p diff --git a/matita/tests/TPTP/try.sh b/matita/tests/TPTP/try.sh index fdf8031b3..bd5b982fb 100755 --- a/matita/tests/TPTP/try.sh +++ b/matita/tests/TPTP/try.sh @@ -1,10 +1,18 @@ #!/bin/sh +prover=y + MATITAC=../../matitac.opt #MATITAC=../../matitac +MATITAPROVER=../../matitaprover.opt +TPTPPATH=/home/tassi/helm/trunk/TPTP-v3.1.1/ if [ -z "$1" ]; then - TODO=Unsatisfiable/[A-Z]*.ma + if [ $prover = 'y' ]; then + TODO=`cat elenco_unsatisfiable.txt` + else + TODO=Unsatisfiable/[A-Z]*.ma + fi else TODO=`cat $1` fi @@ -15,8 +23,17 @@ i=1 for X in $TODO; do echo -n "$X ... " LOGNAME=logs/log.`basename $X` - $MATITAC -nodb $X > $LOGNAME 2>&1 - RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'` + if [ $prover = 'y' ]; then + $MATITAPROVER -tptppath $TPTPPATH $X > $LOGNAME 2>&1 + else + $MATITAC -nodb $X > $LOGNAME 2>&1 + fi + if [ $prover = 'y' ]; then + BASE=`echo $X | cut -c 1-3` + RATING=`grep "Rating" $TPTPPATH/Problems/$BASE/$X | sed 's/v.*//' | sed 's/%//'` + else + RATING=`grep "Rating" $X | sed 's/v.*//' | sed 's/(\*//'` + fi if [ `grep "Found a proof" $LOGNAME | wc -l` -gt 0 ]; then TIME=`grep "TIME NEEDED" $LOGNAME` MAXWEIGHT=`grep "max weight:" $LOGNAME` -- 2.39.2