]> matita.cs.unibo.it Git - helm.git/commitdiff
added generation of hne and heq problems
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 17 Apr 2007 08:21:57 +0000 (08:21 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 17 Apr 2007 08:21:57 +0000 (08:21 +0000)
helm/software/components/tptp_grafite/Makefile
helm/software/components/tptp_grafite/heq_problems [new file with mode: 0644]
helm/software/components/tptp_grafite/hne_problems [new file with mode: 0644]
helm/software/components/tptp_grafite/parser.mly
helm/software/components/tptp_grafite/tptp2grafite.ml
helm/software/components/tptp_grafite/tptp2grafite.mli

index c5c6e63469782de7a2a249a92201a58ef040e3b1..4e4d316772c34cfa56a245b86aaa265612504e8b 100644 (file)
@@ -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/helm/software/components/tptp_grafite/heq_problems b/helm/software/components/tptp_grafite/heq_problems
new file mode 100644 (file)
index 0000000..b45d71c
--- /dev/null
@@ -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/helm/software/components/tptp_grafite/hne_problems b/helm/software/components/tptp_grafite/hne_problems
new file mode 100644 (file)
index 0000000..845ea31
--- /dev/null
@@ -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
index 05577000cf650f214a101af4f2a8a1d23b1e0d1e..4fe172144a4a2636f11f0d840c42ed07fc9f0624 100644 (file)
   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:
index 5a708ceddb8deb46c9a91602c6652d95a814c8e3..5abe88526b4836eb6afb9f5f14550c1d9341908a 100644 (file)
@@ -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 ->
index 24ca1004fbce6a0b70355c3da7897fcd8210511b..0cebccbe350982a14dbdd6316511a3836687612e 100644 (file)
@@ -25,6 +25,7 @@
 
 val tptp2grafite: 
   ?timeout:int ->
+  ?def_depth:int ->
   ?raw_preamble:(string -> string) -> 
   tptppath:string -> filename:string -> unit -> 
     string