From: Enrico Tassi Date: Thu, 25 Jun 2009 16:47:21 +0000 (+0000) Subject: the prover is almost OK, types in fuctors a bit extended to X-Git-Tag: make_still_working~3793 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f7bfbdc706a75256c0e9b15ecc242175f562eb71;p=helm.git the prover is almost OK, types in fuctors a bit extended to ease their instantiation --- diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml index 5a438c7b6..b80091e81 100644 --- a/helm/software/components/binaries/matitaprover/matitaprover.ml +++ b/helm/software/components/binaries/matitaprover/matitaprover.ml @@ -1,3 +1,22 @@ +module OT = struct type t = string let compare = Pervasives.compare end +module HC = Map.Make(OT) + +type leaf = int * string + +let cache = ref HC.empty +let num = ref 100 + +let hash s = + try HC.find s !cache + with Not_found -> + cache := HC.add s (!num,s) !cache; + decr num; + HC.find s !cache +;; + +hash "==";; +hash "_";; + let main () = let problem_file = ref "no-file-given" in let tptppath = ref "./" in @@ -6,40 +25,34 @@ let main () = ] (fun x -> problem_file := x) "matitaprover [problemfile]"; let hypotheses, goals = Tptp_cnf.parse ~tptppath:!tptppath !problem_file in let goal = match goals with [x] -> x | _ -> assert false in - let module B : Terms.Blob with type t = Ast.term = struct - type t = Ast.term - let eq a b = a = b - let compare = Pervasives.compare - let eqP = Ast.Constant "==" - let pp = function - | Ast.Constant x -> x - | Ast.Variable _ -> assert false - | Ast.Function _ -> assert false - ;; - let embed x = - let rec aux m = function + let module B : Terms.Blob with type t = leaf and type input = Ast.term = struct + type t = leaf + let eq a b = a == b + let compare (a,_) (b,_) = Pervasives.compare a b + let eqP = hash "==" + let pp (_,a) = a + type input = Ast.term + let rec embed m = function | Ast.Variable name -> (try m, List.assoc name m with Not_found -> - let t = Terms.Var (List.length m) in + let t = Terms.Var ~-(List.length m) in (name,t)::m, t) - | Ast.Constant _ as t -> m, Terms.Leaf t + | Ast.Constant name -> m, Terms.Leaf (hash name) | Ast.Function (name,args) -> let m, args = HExtlib.list_mapi_acc - (fun x _ m -> aux m x) m args + (fun x _ m -> embed m x) m args in - m, Terms.Node (Terms.Leaf (Ast.Constant name):: args) - in - aux [] x + m, Terms.Node (Terms.Leaf (hash name):: args) ;; let saturate bo ty = - let vars, ty = embed ty in - let _, bo = embed bo in + let vars, ty = embed [] ty in + let _, bo = embed vars bo in let bo = Terms.Node (bo :: List.map snd (List.rev vars)) in bo, ty ;; - let embed t = snd(embed t);; + let embed t = snd(embed [] t);; end in @@ -50,10 +63,12 @@ let main () = let bag, passives = HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses in + prerr_endline "Order"; + HC.iter (fun _ (w,x) -> prerr_endline (" " ^ x ^ " is " ^ string_of_int w)) !cache; prerr_endline "Facts"; - prerr_endline (String.concat "\n" (List.map Pp.pp_unit_clause passives)); + List.iter (fun x -> prerr_endline (" " ^ Pp.pp_unit_clause x)) passives; prerr_endline "Goal"; - prerr_endline (Pp.pp_unit_clause g_passives); + prerr_endline (" " ^ Pp.pp_unit_clause g_passives); ignore(P.paramod bag ~g_passives:[g_passives] ~passives); () ;; diff --git a/helm/software/components/ng_paramodulation/cicBlob.ml b/helm/software/components/ng_paramodulation/cicBlob.ml index 5c672cddf..fd6947e9c 100644 --- a/helm/software/components/ng_paramodulation/cicBlob.ml +++ b/helm/software/components/ng_paramodulation/cicBlob.ml @@ -32,6 +32,8 @@ module CicBlob(C : CicContext) : Terms.Blob with type t = Cic.term = struct let names = List.map (function Some (x,_) -> Some x | _ -> None) C.context;; let pp t = CicPp.pp t names;; + type input = t + let embed t = assert false;; let eqP = assert false;; diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index aa2f4f939..2ed7eef23 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -18,7 +18,8 @@ module type NCicContext = val context : NCic.context end -module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct +module NCicBlob(C : NCicContext) : Terms.Blob +with type t = NCic.term and type input = NCic.term = struct type t = NCic.term @@ -47,6 +48,8 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct let pp t = NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;; + type input = NCic.term + let rec embed = function | NCic.Meta (i,_) -> Terms.Var i, [i] | NCic.Appl l -> diff --git a/helm/software/components/ng_paramodulation/nCicBlob.mli b/helm/software/components/ng_paramodulation/nCicBlob.mli index 5fafaf54f..16a8c33a2 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.mli +++ b/helm/software/components/ng_paramodulation/nCicBlob.mli @@ -18,5 +18,6 @@ module type NCicContext = val context : NCic.context end -module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term +module NCicBlob(C : NCicContext) : Terms.Blob +with type t = NCic.term and type input = NCic.term diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index 5fe0a34c1..dc346d7c4 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -19,7 +19,10 @@ let nparamod rdb metasenv subst context t table = let context = context end in - let module B = NCicBlob.NCicBlob(C) in + let module B : Terms.Blob + with type t = NCic.term and type input = NCic.term + = NCicBlob.NCicBlob(C) + in let module P = Paramod.Paramod(B) in let bag, maxvar = Terms.M.empty, 0 in let (bag,maxvar), passives = diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 47975fb3b..d63d1449a 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -14,7 +14,7 @@ (*let debug s = prerr_endline s ;;*) let debug _ = ();; -let max_nb_iter = 999999999 ;; +let max_nb_iter = max_int ;; let amount_of_time = 300.0 ;; module Paramod (B : Terms.Blob) = struct diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli index 266449499..9a2d397ca 100644 --- a/helm/software/components/ng_paramodulation/paramod.mli +++ b/helm/software/components/ng_paramodulation/paramod.mli @@ -14,8 +14,8 @@ module Paramod ( B : Terms.Blob ) : sig type bag = B.t Terms.bag * int - val mk_passive : bag -> B.t * B.t -> bag * B.t Terms.unit_clause - val mk_goal : bag -> B.t * B.t -> bag * B.t Terms.unit_clause + val mk_passive : bag -> B.input * B.input -> bag * B.t Terms.unit_clause + val mk_goal : bag -> B.input * B.input -> bag * B.t Terms.unit_clause val paramod : bag -> g_passives:B.t Terms.unit_clause list -> passives:B.t Terms.unit_clause list -> diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml index 8a74fa762..e9628220d 100644 --- a/helm/software/components/ng_paramodulation/pp.ml +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -123,7 +123,7 @@ let pp_unit_clause ~formatter:f c = let pp_bag ~formatter:f bag = Format.fprintf f "@["; Terms.M.iter - (fun _ c,_ -> pp_unit_clause ~formatter:f c;Format.fprintf f "@;") bag; + (fun _ (c,_) -> pp_unit_clause ~formatter:f c;Format.fprintf f "@;") bag; Format.fprintf f "@]" ;; diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index e931423b9..3957e925e 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -178,11 +178,12 @@ module Superposition (B : Terms.Blob) = ;; (* move away *) - let is_identity_clause = function + let is_identity_clause ~unify = function | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true - | _, Terms.Equation (l,r,_,_), vl, proof -> + | _, Terms.Equation (l,r,_,_), vl, proof when unify -> (try ignore(Unif.unification vl [] l r); true with FoUnif.UnificationFailure _ -> false) + | _, Terms.Equation (_,_,_,_), _, _ -> false | _, Terms.Predicate _, _, _ -> assert false ;; @@ -404,7 +405,7 @@ module Superposition (B : Terms.Blob) = (* this is like simplify but raises Success *) let simplify_goal maxvar table bag g_actives clause = let bag, clause = demodulate bag clause table in - if (is_identity_clause clause) + if (is_identity_clause ~unify:true clause) then raise (Success (bag, maxvar, clause)) (* else diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index f2a3de020..1d1465f9e 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -65,7 +65,8 @@ module type Blob = val compare : t -> t -> int val eqP : t val pp : t -> string - val embed : t -> t foterm - val saturate : t -> t -> t foterm * t foterm + type input + val embed : input -> t foterm + val saturate : input -> input -> t foterm * t foterm end diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 7c60f0562..e0576d1f3 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -71,9 +71,10 @@ module type Blob = * *) val pp : t -> string - val embed : t -> t foterm + type input + val embed : input -> t foterm (* saturate [proof] [type] -> [proof] * [type] *) - val saturate : t -> t -> t foterm * t foterm + val saturate : input -> input -> t foterm * t foterm end