From: Enrico Tassi Date: Tue, 17 Apr 2007 08:21:57 +0000 (+0000) Subject: added generation of hne and heq problems X-Git-Tag: 0.4.95@7852~530 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c651530ffbff86d63868f452ec4fdc59488fc4ee;p=helm.git added generation of hne and heq problems --- diff --git a/components/tptp_grafite/Makefile b/components/tptp_grafite/Makefile index c5c6e6346..4e4d31677 100644 --- a/components/tptp_grafite/Makefile +++ b/components/tptp_grafite/Makefile @@ -32,16 +32,16 @@ testall: tptp2grafite cat $(TPTPDIR)/$$X | ./tptp2grafite || echo ERROR PARSING $$X;\ done -generate: - for X in `cat unit_equality_problems`; do\ - ./tptp2grafite -tptppath $(TPTPDIR) $$X \ - > ../../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \ +generate-%: + for X in `cat $*`; do\ + ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \ + > ../../matita/tests/TPTP/$$X.ma || echo Failed: $$X; \ done -parse: - for X in `cat unit_equality_problems`; do\ +parse-%: + for X in `cat $*`; do\ echo "Parsing $$X"; \ - ./tptp2grafite -tptppath $(TPTPDIR) $$X \ + ./tptp2grafite -tptppath $(TPTPDIR) $$X.p \ > /dev/null || echo Failed: $$X; \ done diff --git a/components/tptp_grafite/heq_problems b/components/tptp_grafite/heq_problems new file mode 100644 index 000000000..b45d71ce3 --- /dev/null +++ b/components/tptp_grafite/heq_problems @@ -0,0 +1,142 @@ +ANA003-1 +ANA004-1 +ANA005-1 +CAT018-4 +COL003-10 +COL003-2 +COL003-3 +COL003-4 +COL003-5 +COL003-6 +COL003-7 +COL003-8 +COL003-9 +COL006-2 +COL006-3 +COL006-4 +COL042-2 +COL042-3 +COL042-4 +COL042-5 +COL043-2 +COL044-2 +COL044-3 +COL044-4 +COL044-5 +HWC002-1 +HWC003-1 +HWC003-2 +HWV002-1 +HWV003-1 +HWV004-1 +LAT001-1 +LAT002-1 +LAT041-1 +LCL109-4 +LCL149-1 +LCL150-1 +LCL152-1 +LCL181-3 +LCL191-3 +LCL192-3 +LCL193-3 +LCL194-3 +LCL195-3 +LCL208-3 +LCL213-3 +LCL214-3 +LCL215-3 +LCL216-3 +LCL217-3 +LCL220-3 +LCL221-3 +LCL222-3 +LCL223-3 +LCL224-3 +LCL225-3 +LCL227-3 +LCL229-3 +LCL230-3 +LCL231-3 +LCL242-3 +LCL243-3 +LCL245-3 +LCL246-3 +LCL247-3 +LCL249-3 +LCL251-3 +LCL252-3 +LCL253-3 +LCL254-3 +LCL255-3 +LCL260-3 +LCL262-3 +LCL263-3 +LCL264-3 +LCL265-3 +LCL266-3 +LCL269-3 +LCL270-3 +LCL271-3 +LCL272-3 +LCL273-3 +LCL274-3 +LCL275-3 +LCL276-3 +LCL277-3 +LCL278-3 +LCL281-3 +LCL282-3 +LCL283-3 +LCL284-3 +LCL285-3 +LCL286-3 +LCL289-3 +LCL293-3 +LCL295-3 +LCL298-3 +LCL299-3 +LCL300-3 +LCL302-3 +LCL303-3 +LCL304-3 +LCL305-3 +LCL306-3 +LCL307-3 +LCL308-3 +LCL309-3 +LCL310-3 +LCL311-3 +LCL312-3 +LCL313-3 +LCL314-3 +LCL315-3 +LCL316-3 +LCL319-3 +LCL324-3 +LCL325-3 +LCL327-3 +LCL328-3 +LCL329-3 +LCL330-3 +LCL331-3 +LCL332-3 +LCL334-3 +LCL335-3 +LCL336-3 +LCL337-3 +LCL339-3 +LCL340-3 +LCL341-3 +LCL344-3 +LCL345-3 +LCL346-3 +LCL347-3 +LCL348-3 +LCL349-3 +LCL351-3 +LCL353-3 +LDA004-1 +ROB014-1 +ROB015-2 +ROB018-1 diff --git a/components/tptp_grafite/hne_problems b/components/tptp_grafite/hne_problems new file mode 100644 index 000000000..845ea315f --- /dev/null +++ b/components/tptp_grafite/hne_problems @@ -0,0 +1,90 @@ +ANA003-2 +LCL001-1 +LCL002-1 +LCL005-1 +LCL019-1 +LCL020-1 +LCL021-1 +LCL024-1 +LCL032-1 +LCL037-1 +LCL038-1 +LCL061-1 +LCL062-1 +LCL063-1 +LCL074-1 +LCL084-2 +LCL084-3 +LCL085-1 +LCL105-1 +LCL119-1 +LCL122-1 +LCL124-1 +LCL125-1 +LCL166-1 +LCL167-1 +LCL218-1 +LCL227-1 +LCL230-1 +LCL231-1 +LCL249-1 +LCL253-1 +LCL369-1 +LCL375-1 +LCL377-1 +LCL393-1 +LCL394-1 +LCL395-1 +LCL423-1 +LCL425-1 +NUM017-1 +PLA001-1 +PLA004-1 +PLA004-2 +PLA005-1 +PLA005-2 +PLA007-1 +PLA008-1 +PLA009-1 +PLA009-2 +PLA010-1 +PLA011-1 +PLA011-2 +PLA012-1 +PLA013-1 +PLA014-1 +PLA014-2 +PLA015-1 +PLA016-1 +PLA018-1 +PLA019-1 +PLA021-1 +PLA023-1 +PUZ039-1 +PUZ040-1 +PUZ042-1 +PUZ050-1 +RNG001-2 +RNG004-3 +SWV014-1 +SYN556-1 +SYN598-1 +SYN599-1 +SYN600-1 +SYN614-1 +SYN615-1 +SYN617-1 +SYN628-1 +SYN631-1 +SYN639-1 +SYN640-1 +SYN646-1 +SYN647-1 +SYN649-1 +SYN653-1 +SYN654-1 +SYN655-1 +SYN704-1 +SYN707-1 +SYN708-1 +SYN711-1 diff --git a/components/tptp_grafite/parser.mly b/components/tptp_grafite/parser.mly index 05577000c..4fe172144 100644 --- a/components/tptp_grafite/parser.mly +++ b/components/tptp_grafite/parser.mly @@ -119,6 +119,11 @@ atomic_word: | LNAME { $1 } | QSTRING { rm_q $1 } + | TYPE { (* workaround! *) + match $1 with + | "theorem" -> "theoremP" + | "axiom" -> "axiomP" + | s -> prerr_endline s;assert false } ; formula_source_and_infos: diff --git a/components/tptp_grafite/tptp2grafite.ml b/components/tptp_grafite/tptp2grafite.ml index 5a708cedd..5abe88526 100644 --- a/components/tptp_grafite/tptp2grafite.ml +++ b/components/tptp_grafite/tptp2grafite.ml @@ -2,11 +2,17 @@ module GA = GrafiteAst;; module LA = LexiconAst;; module PT = CicNotationPt;; module A = Ast;; + +type sort = Prop | Univ;; + let floc = HExtlib.dummy_floc;; + let paramod_timeout = ref 600;; +let depth = ref 10;; let universe = "Univ" ;; +let prop = "Prop";; let kw = [ "and","myand" @@ -17,10 +23,11 @@ let mk_ident s = ;; let rec collect_arities_from_term = function - | A.Constant name -> [name,0] - | A.Variable name -> [] + | A.Constant name -> [name,(0,Univ)] + | A.Variable name -> [name,(0,Univ)] | A.Function (name,l) -> - (name,List.length l)::List.flatten (List.map collect_arities_from_term l) + (name,(List.length l,Univ)):: + List.flatten (List.map collect_arities_from_term l) ;; let rec collect_fv_from_term = function @@ -32,32 +39,42 @@ let rec collect_fv_from_term = function let collect_arities_from_atom a = let aux = function - | A.Proposition name -> assert false - | A.Predicate _ -> assert false + | A.Proposition name -> [name,(0,Prop)] + | A.Predicate (name,args) -> + (name,(List.length args,Prop)) :: + (List.flatten (List.map collect_arities_from_term args)) | A.True -> [] | A.False -> [] - | A.Eq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2 - | A.NotEq (t1,t2) -> collect_arities_from_term t1 @ collect_arities_from_term t2 + | A.Eq (t1,t2) -> + collect_arities_from_term t1 @ collect_arities_from_term t2 + | A.NotEq (t1,t2) -> + collect_arities_from_term t1 @ collect_arities_from_term t2 in - aux a + HExtlib.list_uniq (List.sort compare (List.flatten (List.map aux a))) ;; let collect_fv_from_atom a = let aux = function - | A.Proposition name -> assert false - | A.Predicate _ -> assert false + | A.Proposition name -> [name] + | A.Predicate (name,args) -> + name :: List.flatten (List.map collect_fv_from_term args) | A.True -> [] | A.False -> [] | A.Eq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2 | A.NotEq (t1,t2) -> collect_fv_from_term t1 @ collect_fv_from_term t2 in - HExtlib.list_uniq (List.sort compare (aux a)) + let rec aux2 = function + | [] -> [] + | hd::tl -> aux hd @ aux2 tl + in + HExtlib.list_uniq (List.sort compare (aux2 a)) ;; -let collect_fv_from_formulae = function - | A.Disjunction _ -> assert false +let rec collect_fv_from_formulae = function + | A.Disjunction (a,b) -> + collect_fv_from_formulae a @ collect_fv_from_formulae b | A.NegAtom a - | A.Atom a -> collect_fv_from_atom a + | A.Atom a -> collect_fv_from_atom [a] ;; let rec convert_term = function @@ -67,29 +84,34 @@ let rec convert_term = function PT.Appl (mk_ident name :: List.map convert_term args) ;; -let atom_of_formula = function - | A.Disjunction _ -> assert false - | A.NegAtom a -> a (* removes the negation *) - | A.Atom a -> a +let rec atom_of_formula = function + | A.Disjunction (a,b) -> + atom_of_formula a @ atom_of_formula b + | A.NegAtom a -> [a] (* removes the negation *) + | A.Atom a -> [a] ;; -let rec mk_arrow component = function - | 0 -> mk_ident component +let rec mk_arrow component tail = function + | 0 -> begin + match tail with + | Prop -> mk_ident prop + | Univ -> mk_ident universe + end | n -> PT.Binder (`Forall, ((mk_ident "_"),Some (mk_ident component)), - mk_arrow component (n-1)) + mk_arrow component tail (n-1)) ;; let build_ctx_for_arities univesally arities t = let binder = if univesally then `Forall else `Exists in let rec aux = function | [] -> t - | (name,nargs)::tl -> + | (name,(nargs,sort))::tl -> PT.Binder (binder, - (mk_ident name,Some (mk_arrow universe nargs)), + (mk_ident name,Some (mk_arrow universe sort nargs)), aux tl) in aux arities @@ -97,34 +119,62 @@ let build_ctx_for_arities univesally arities t = let convert_atom universally a = let aux = function - | A.Proposition _ -> assert false + | A.Proposition p -> mk_ident p | A.Predicate (name,params) -> - prerr_endline ("Predicate is unsupported: " ^ name); - assert false + PT.Appl ((mk_ident name) :: (List.map convert_term params)) | A.True -> mk_ident "True" | A.False -> mk_ident "False" | A.Eq (l,r) | A.NotEq (l,r) -> (* removes the negation *) PT.Appl [mk_ident "eq";mk_ident universe;convert_term l;convert_term r] in + let rec aux2 = function + | [] -> assert false + | [x] -> aux x + | he::tl -> + if universally then + PT.Binder (`Forall, (mk_ident "_", Some (aux he)), aux2 tl) + else + PT.Appl [mk_ident "And";aux he;aux2 tl] + in + let arities = collect_arities_from_atom a in + let fv = collect_fv_from_atom a in build_ctx_for_arities universally - (List.map (fun x -> (x,0)) (collect_fv_from_atom a)) (aux a) + (List.filter + (function (x,(0,Univ)) -> List.mem x fv | _-> false) + arities) + (aux2 a) ;; let collect_arities atom ctx = - let atoms = atom::(List.map atom_of_formula ctx) in - HExtlib.list_uniq (List.sort (fun (a,_) (b,_) -> compare a b) - (List.flatten (List.map collect_arities_from_atom atoms))) + let atoms = atom@(List.flatten (List.map atom_of_formula ctx)) in + collect_arities_from_atom atoms ;; -let assert_formulae_is_1eq_negated f = +let collect_arities_from_formulae f = + let rec collect_arities_from_formulae = function + | A.Disjunction (a,b) -> + collect_arities_from_formulae a @ collect_arities_from_formulae b + | A.NegAtom a + | A.Atom a -> collect_arities_from_atom [a] + in + HExtlib.list_uniq (List.sort compare (collect_arities_from_formulae f)) +;; + +let is_formulae_1eq_negated f = let atom = atom_of_formula f in match atom with - | A.Eq (l,r) -> failwith "Negated formula is not negated" - | A.NotEq (l,r) -> () - | _ -> failwith "Not a unit equality formula" + | [A.NotEq (l,r)] -> true + | _ -> false ;; +let collect_fv_1stord_from_formulae f = + let arities = collect_arities_from_formulae f in + let fv = collect_fv_from_formulae f in + List.map fst + (List.filter (function (x,(0,Univ)) -> List.mem x fv | _-> false) arities) +;; + let rec convert_formula fv no_arities context f = let atom = atom_of_formula f in let t = convert_atom (fv = []) atom in @@ -142,13 +192,17 @@ let rec convert_formula fv no_arities context f = ;; let check_if_atom_is_negative = function - | A.True | A.False | A.Proposition _ | A.Predicate _ -> assert false + | A.True -> false + | A.False -> true + | A.Proposition _ -> false + | A.Predicate _ -> false | A.Eq _ -> false | A.NotEq _ -> true ;; -let check_if_formula_is_negative = function - | A.Disjunction _ -> assert false +let rec check_if_formula_is_negative = function + | A.Disjunction (a,b) -> + check_if_formula_is_negative a && check_if_formula_is_negative b | A.NegAtom a -> not (check_if_atom_is_negative a) | A.Atom a -> check_if_atom_is_negative a ;; @@ -177,8 +231,8 @@ let convert_ast statements context = function | A.Negated_conjecture when not (check_if_formula_is_negative f) -> statements, f::context | A.Negated_conjecture -> - assert_formulae_is_1eq_negated f; - let fv = collect_fv_from_formulae f in + let ueq_case = is_formulae_1eq_negated f in + let fv = collect_fv_1stord_from_formulae f in (* if fv <> [] then prerr_endline ("FREE VARIABLES: " ^ String.concat "," fv); @@ -205,7 +259,12 @@ let convert_ast statements context = function fv)) else [])@ [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, - GA.Auto (floc,["paramodulation","";"timeout",string_of_int !paramod_timeout])), + if ueq_case then + GA.Auto (floc,["paramodulation",""; + "timeout",string_of_int !paramod_timeout]) + else + GA.Auto (floc,["depth",string_of_int !depth]) + ), Some (GA.Dot(floc)))); GA.Executable(floc,GA.Tactical(floc, GA.Try(floc, GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc)))) @@ -251,8 +310,9 @@ let resolve ~tptppath s = ;; (* MAIN *) -let tptp2grafite ?(timeout=600) ?raw_preamble ~tptppath ~filename () = +let tptp2grafite ?(timeout=600) ?(def_depth=10) ?raw_preamble ~tptppath ~filename () = paramod_timeout := timeout; + depth := def_depth; let rec aux = function | [] -> [] | ((A.Inclusion (file,_)) as hd) :: tl -> diff --git a/components/tptp_grafite/tptp2grafite.mli b/components/tptp_grafite/tptp2grafite.mli index 24ca1004f..0cebccbe3 100644 --- a/components/tptp_grafite/tptp2grafite.mli +++ b/components/tptp_grafite/tptp2grafite.mli @@ -25,6 +25,7 @@ val tptp2grafite: ?timeout:int -> + ?def_depth:int -> ?raw_preamble:(string -> string) -> tptppath:string -> filename:string -> unit -> string