end
;;
-let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) =
+let success_msg bag l (pp : ?margin:int -> leaf Terms.unit_clause -> string) ord =
print_endline ("% SZS status Unsatisfiable for " ^
Filename.basename !problem_file);
print_endline ("% SZS output start CNFRefutation for " ^
print_endline (pp ~margin:max_int
cl)) l;
print_endline ("% SZS output end CNFRefutation for " ^
- Filename.basename !problem_file)
+ Filename.basename !problem_file);
+ let prefix = string_of_int (Unix.getpid ()) in
+ let prerr_endline s = prerr_endline (prefix ^ ": " ^ s) in
+ let times = Unix.times () in
+ prerr_endline ("solved " ^ !problem_file ^ " in " ^ string_of_float
+ (times.Unix.tms_utime +. times.Unix.tms_stime) ^ " using " ^ ord);
;;
-let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) =
+let start_msg passives g_passives (pp : leaf Terms.unit_clause -> string) oname =
let prefix = string_of_int (Unix.getpid ()) in
let prerr_endline s = prerr_endline (prefix ^ ": " ^ s) in
prerr_endline "Facts:";
prerr_endline "Goal:";
prerr_endline (" " ^ pp g_passives);
prerr_endline "Order:";
- prerr_endline " ...fixme...";
- prerr_endline "Strategy:";
- prerr_endline " ...fixme...";
+ prerr_endline (" " ^ oname);
;;
let report_error s = prerr_endline (string_of_int (Unix.getpid())^": "^s);;
-module Main(C:LeafComparer) = struct
+module Main(C:Orderings.Blob with type t = leaf) = struct
let main goal hypotheses =
- let module B = MakeBlob(C) in
+ let module B = C in
let module Pp = Pp.Pp(B) in
let module P = Paramod.Paramod(B) in
let bag = Terms.empty_bag, 0 in
let bag, passives =
HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses
in
- start_msg passives g_passives Pp.pp_unit_clause;
+ start_msg passives g_passives Pp.pp_unit_clause C.name;
match
P.paramod
~max_steps:max_int bag ~g_passives:[g_passives] ~passives
with
| P.Error s -> report_error s; 3
| P.Unsatisfiable ((bag,_,l)::_) ->
- success_msg bag l Pp.pp_unit_clause; 0
+ success_msg bag l Pp.pp_unit_clause C.name; 0
| P.Unsatisfiable ([]) ->
report_error "Unsatisfiable but no solution output"; 3
| P.GaveUp -> 2
Matitaprover is the first order automatic prover that equips the
Matita interactive theorem prover (http://matita.cs.unibo.it).
-Developed by A.Asperti, M.Denes and E.Tassi, released under GPL-2.1
+Developed by A.Asperti, M.Denes and E.Tassi, released under GPL version 2
+or at your option any later version.
If --tptppath is given, instead of the problem file you can just give the
problem name with the .p suffix (e.g. BOO001-1.p)
if pid = 0 then (exit (f ())) else pid)
[
(fun () ->
- let module M = Main(struct let cmp (a,_) (b,_) = compare a b end) in
+ let module M = Main(Orderings.NRKBO(MakeBlob(struct let cmp (a,_) (b,_) = compare a b end))) in
+ M.main goal hypotheses)
+ ;
+ (fun () ->
+ let module M = Main(Orderings.KBO(MakeBlob(struct let cmp (a,_) (b,_) = compare a b end))) in
M.main goal hypotheses)
;
-(*
(fun () ->
- let module M = Main(struct let cmp (a,_) (b,_) = compare b a end) in
+ let module M = Main(Orderings.LPO(MakeBlob(struct let cmp (a,_) (b,_) = compare a b end))) in
M.main goal hypotheses)
-*)
];
let rec aux () =
if List.length !childs = 0 then
type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
-module Orderings (B : Terms.Blob) = struct
+module type Blob =
+ sig
+ include Terms.Blob
- module Pp = Pp.Pp(B)
+ (* This order relation should be:
+ * - stable for instantiation
+ * - total on ground terms
+ *
+ *)
+ val compare_terms :
+ t Terms.foterm -> t Terms.foterm -> Terms.comparison
+
+ val compute_unit_clause_weight : 't Terms.unit_clause -> int
- type weight = int * (int * int) list;;
+ val compute_goal_weight : 't Terms.unit_clause -> int
-let rec eq_foterm x y =
+ val name : string
+
+ end
+
+type weight = int * (int * int) list;;
+
+let rec eq_foterm f x y =
x == y ||
match x, y with
- | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2
+ | Terms.Leaf t1, Terms.Leaf t2 -> f t1 t2
| Terms.Var i, Terms.Var j -> i = j
- | Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2
+ | Terms.Node l1, Terms.Node l2 -> List.for_all2 (eq_foterm f) l1 l2
| _ -> false
- ;;
+;;
- let string_of_weight (cw, mw) =
- let s =
- String.concat ", "
- (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
- in
- Printf.sprintf "[%d; %s]" cw s
- ;;
+let string_of_weight (cw, mw) =
+ let s =
+ String.concat ", "
+ (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
+ in
+ Printf.sprintf "[%d; %s]" cw s
+;;
- let weight_of_term term =
+let weight_of_term term =
let vars_dict = Hashtbl.create 5 in
let rec aux = function
| Terms.Var i ->
| (m1, _), (m2, _) -> m1 - m2
in
(w, List.sort compare l) (* from the smallest meta to the bigest *)
- ;;
+;;
- let compute_unit_clause_weight (_,l, _, _) =
+let compute_unit_clause_weight (_,l, _, _) =
let weight_of_polynomial w m =
let factor = 2 in
w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
let wl, ml = weight_of_term l in
let wr, mr = weight_of_term r in
weight_of_polynomial (wl+wr) (ml@mr)
- ;;
+;;
let compute_goal_weight (_,l, _, _) =
let weight_of_polynomial w m =
- (abs (wl-wr))
;;
- (* Riazanov: 3.1.5 pag 38 *)
+(* Riazanov: 3.1.5 pag 38 *)
(* Compare weights normalized in a new way :
* Variables should be sorted from the lowest index to the highest
* Variables which do not occur in the term should not be present
* in the normalized polynomial
*)
- let compare_weights (h1, w1) (h2, w2) =
- let rec aux hdiff (lt, gt) diffs w1 w2 =
- match w1, w2 with
- | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
- if var1 = var2 then
- let diffs = (w1 - w2) + diffs in
- let r = compare w1 w2 in
- let lt = lt or (r < 0) in
- let gt = gt or (r > 0) in
- if lt && gt then XINCOMPARABLE else
- aux hdiff (lt, gt) diffs tl1 tl2
- else if var1 < var2 then
- if lt then XINCOMPARABLE else
- aux hdiff (false,true) (diffs+w1) tl1 l2
- else
- if gt then XINCOMPARABLE else
- aux hdiff (true,false) (diffs-w2) l1 tl2
- | [], (_,w2)::tl2 ->
- if gt then XINCOMPARABLE else
- aux hdiff (true,false) (diffs-w2) [] tl2
- | (_,w1)::tl1, [] ->
+let compare_weights (h1, w1) (h2, w2) =
+ let rec aux hdiff (lt, gt) diffs w1 w2 =
+ match w1, w2 with
+ | ((var1, w1)::tl1) as l1, (((var2, w2)::tl2) as l2) ->
+ if var1 = var2 then
+ let diffs = (w1 - w2) + diffs in
+ let r = Pervasives.compare w1 w2 in
+ let lt = lt or (r < 0) in
+ let gt = gt or (r > 0) in
+ if lt && gt then XINCOMPARABLE else
+ aux hdiff (lt, gt) diffs tl1 tl2
+ else if var1 < var2 then
if lt then XINCOMPARABLE else
- aux hdiff (false,true) (diffs+w1) tl1 []
- | [], [] ->
- if lt then
- if hdiff <= 0 then XLT
- else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
- else if gt then
- if hdiff >= 0 then XGT
- else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
- else
- if hdiff < 0 then XLT
- else if hdiff > 0 then XGT
- else XEQ
- in
- aux (h1-h2) (false,false) 0 w1 w2
- ;;
+ aux hdiff (false,true) (diffs+w1) tl1 l2
+ else
+ if gt then XINCOMPARABLE else
+ aux hdiff (true,false) (diffs-w2) l1 tl2
+ | [], (_,w2)::tl2 ->
+ if gt then XINCOMPARABLE else
+ aux hdiff (true,false) (diffs-w2) [] tl2
+ | (_,w1)::tl1, [] ->
+ if lt then XINCOMPARABLE else
+ aux hdiff (false,true) (diffs+w1) tl1 []
+ | [], [] ->
+ if lt then
+ if hdiff <= 0 then XLT
+ else if (- diffs) >= hdiff then XLE else XINCOMPARABLE
+ else if gt then
+ if hdiff >= 0 then XGT
+ else if diffs >= (- hdiff) then XGE else XINCOMPARABLE
+ else
+ if hdiff < 0 then XLT
+ else if hdiff > 0 then XGT
+ else XEQ
+ in
+ aux (h1-h2) (false,false) 0 w1 w2
+;;
+
+(* Riazanov: p. 40, relation >>>
+ * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
+let rec aux_ordering b_compare ?(head_only=false) t1 t2 =
+ match t1, t2 with
+ (* We want to discard any identity equality. *
+ * If we give back XEQ, no inference rule *
+ * will be applied on this equality *)
+ | Terms.Var i, Terms.Var j when i = j ->
+ XEQ
+ (* 1. *)
+ | Terms.Var _, _
+ | _, Terms.Var _ -> XINCOMPARABLE
+ (* 2.a *)
+ | Terms.Leaf a1, Terms.Leaf a2 ->
+ let cmp = b_compare a1 a2 in
+ if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
+ | Terms.Leaf _, Terms.Node _ -> XLT
+ | Terms.Node _, Terms.Leaf _ -> XGT
+ (* 2.b *)
+ | Terms.Node l1, Terms.Node l2 ->
+ let rec cmp t1 t2 =
+ match t1, t2 with
+ | [], [] -> XEQ
+ | _, [] -> (* XGT *) assert false (* hd symbols were eq *)
+ | [], _ -> (* XLT *) assert false (* hd symbols were eq *)
+ | hd1::tl1, hd2::tl2 ->
+ let o = aux_ordering b_compare ~head_only hd1 hd2 in
+ if o = XEQ && not head_only then cmp tl1 tl2 else o
+ in
+ cmp l1 l2
+;;
- (* Riazanov: p. 40, relation >>>
- * if head_only=true then it is not >>> but helps case 2 of 3.14 p 39 *)
- let rec aux_ordering ?(head_only=false) t1 t2 =
- match t1, t2 with
- (* We want to discard any identity equality. *
- * If we give back XEQ, no inference rule *
- * will be applied on this equality *)
- | Terms.Var i, Terms.Var j when i = j ->
- XEQ
- (* 1. *)
- | Terms.Var _, _
- | _, Terms.Var _ -> XINCOMPARABLE
- (* 2.a *)
- | Terms.Leaf a1, Terms.Leaf a2 ->
- let cmp = B.compare a1 a2 in
- if cmp = 0 then XEQ else if cmp < 0 then XLT else XGT
- | Terms.Leaf _, Terms.Node _ -> XLT
- | Terms.Node _, Terms.Leaf _ -> XGT
- (* 2.b *)
- | Terms.Node l1, Terms.Node l2 ->
- let rec cmp t1 t2 =
- match t1, t2 with
- | [], [] -> XEQ
- | _, [] -> (* XGT *) assert false (* hd symbols were eq *)
- | [], _ -> (* XLT *) assert false (* hd symbols were eq *)
- | hd1::tl1, hd2::tl2 ->
- let o = aux_ordering ~head_only hd1 hd2 in
- if o = XEQ && not head_only then cmp tl1 tl2 else o
- in
- cmp l1 l2
- ;;
+let compare_terms o x y =
+ match o x y with
+ | XINCOMPARABLE -> Terms.Incomparable
+ | XGT -> Terms.Gt
+ | XLT -> Terms.Lt
+ | XEQ -> Terms.Eq
+ | _ -> assert false
+;;
+
+module NRKBO (B : Terms.Blob) = struct
+ let name = "nrkbo"
+ include B
+
+ module Pp = Pp.Pp(B)
+
+ let eq_foterm = eq_foterm B.eq;;
+
+ let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let compute_goal_weight = compute_goal_weight;;
(* Riazanov: p. 40, relation >_n *)
let nonrec_kbo t1 t2 =
let w2 = weight_of_term t2 in
match compare_weights w1 w2 with
| XLE -> (* this is .> *)
- if aux_ordering t1 t2 = XLT then XLT else XINCOMPARABLE
+ if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
| XGE ->
- if aux_ordering t1 t2 = XGT then XGT else XINCOMPARABLE
- | XEQ -> aux_ordering t1 t2
+ if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
+ | XEQ -> aux_ordering B.compare t1 t2
| res -> res
;;
+
+ let compare_terms = compare_terms nonrec_kbo;;
+
+ let profiler = HExtlib.profile ~enable:true "compare_terms(nrkbo)";;
+ let compare_terms x y =
+ profiler.HExtlib.profile (compare_terms x) y
+ ;;
+
+end
+module KBO (B : Terms.Blob) = struct
+ let name = "kbo"
+ include B
+
+ module Pp = Pp.Pp(B)
+
+ let eq_foterm = eq_foterm B.eq;;
+
+ let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let compute_goal_weight = compute_goal_weight;;
+
(* Riazanov: p. 38, relation > *)
let rec kbo t1 t2 =
- let aux = aux_ordering ~head_only:true in
+ let aux = aux_ordering B.compare ~head_only:true in
let rec cmp t1 t2 =
match t1, t2 with
| [], [] -> XEQ
| res -> res
;;
+ let compare_terms = compare_terms kbo;;
+
+ let profiler = HExtlib.profile ~enable:true "compare_terms(kbo)";;
+ let compare_terms x y =
+ profiler.HExtlib.profile (compare_terms x) y
+ ;;
+
+end
+
+module LPO (B : Terms.Blob) = struct
+ let name = "lpo"
+ include B
+
+ module Pp = Pp.Pp(B)
+
+ let eq_foterm = eq_foterm B.eq;;
+
+ let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let compute_goal_weight = compute_goal_weight;;
+
let rec lpo s t =
match s,t with
| s, t when eq_foterm s t ->
if lpo x t = XLT then check_subterms t ([],tl)
else false
in
- match aux_ordering hd1 hd2 with
+ match aux_ordering B.compare hd1 hd2 with
| XGT -> if check_subterms s (r_ol,tl2) then XGT
else XINCOMPARABLE
| XLT -> if check_subterms t (l_ol,tl1) then XLT
| XINCOMPARABLE -> XINCOMPARABLE
| _ -> assert false
end
- | _,_ -> aux_ordering s t
+ | _,_ -> aux_ordering B.compare s t
;;
- let compare_terms x y =
- match nonrec_kbo x y with
- | XINCOMPARABLE -> Terms.Incomparable
- | XGT -> Terms.Gt
- | XLT -> Terms.Lt
- | XEQ -> Terms.Eq
- | _ -> assert false
- ;;
+ let compare_terms = compare_terms lpo;;
- let profiler = HExtlib.profile ~enable:true "compare_terms";;
+ let profiler = HExtlib.profile ~enable:true "compare_terms(lpo)";;
let compare_terms x y =
profiler.HExtlib.profile (compare_terms x) y
;;
end
+
projects / helm.git / commitdiff