+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
] (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
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);
()
;;
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;;
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
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 ->
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
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 =
(*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
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 ->
let pp_bag ~formatter:f bag =
Format.fprintf f "@[<v>";
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 "@]"
;;
;;
(* 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
;;
(* 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
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
* *)
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
projects / helm.git / commitdiff