> log
for PROBLEM in `cat $2`; do
echo running on $PROBLEM
- ./matitaprover.native --timeout $1 --tptppath TPTP-v3.7.0/ $PROBLEM \
+ ./matitaprover.native --timeout $1 --tptppath ~/TPTP-v3.7.0/ $PROBLEM \
>> log 2>&1
echo So far `grep 'SZS status Unsatisfiable' log|wc -l` solved
done
gallina8Parser.cmi: types.cmo
grafiteParser.cmi: types.cmo
grafite.cmi: types.cmo
-engine.cmi:
-types.cmo:
-types.cmx:
-options.cmo:
-options.cmx:
gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmo gallina8Parser.cmi
gallina8Parser.cmi: types.cmx
grafiteParser.cmi: types.cmx
grafite.cmi: types.cmx
-engine.cmi:
-types.cmo:
-types.cmx:
-options.cmo:
-options.cmx:
gallina8Parser.cmo: types.cmx options.cmx gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmx gallina8Parser.cmi
(** PROFILING *)
-let profiling_enabled = ref false ;; (* ComponentsConf.profiling *)
+let profiling_enabled = ref true ;; (* ComponentsConf.profiling *)
-let something_profiled = ref false
+let something_profiled = ref false ;;
let _ =
if !something_profiled then
| Terms.Equation _, Terms.Predicate _ -> 1
;;
- let eq_unit_clause (id1,_,_,_) (id2,_,_,_) = id1 = id2
- let compare_unit_clause (id1,_,_,_) (id2,_,_,_) = Pervasives.compare id1 id2
+ let eq_clause (id1,_,_,_,_) (id2,_,_,_,_) = id1 = id2
+ let compare_clause (id1,_,_,_,_) (id2,_,_,_,_) = Pervasives.compare id1 id2
let relocate maxvar varlist subst =
List.fold_right
varlist (maxvar+1, [], subst)
;;
- let fresh_unit_clause maxvar (id, lit, varlist, proof) =
+ let fresh_clause maxvar (id, nlit, plit, varlist, proof) =
let maxvar, varlist, subst = relocate maxvar varlist Subst.id_subst in
- let lit =
- match lit with
+ let apply_subst_on_lit = function
| Terms.Equation (l,r,ty,o) ->
let l = Subst.apply_subst subst l in
let r = Subst.apply_subst subst r in
let p = Subst.apply_subst subst p in
Terms.Predicate p
in
+ let nlit = List.map apply_subst_on_lit nlit in
+ let plit = List.map apply_subst_on_lit plit in
let proof =
match proof with
| Terms.Exact t -> Terms.Exact (Subst.apply_subst subst t)
| Terms.Step (rule,c1,c2,dir,pos,s) ->
Terms.Step(rule,c1,c2,dir,pos,Subst.concat subst s)
in
- (id, lit, varlist, proof), maxvar
+ (id, nlit, plit, varlist, proof), maxvar
;;
(* may be moved inside the bag *)
- let mk_unit_clause maxvar ty proofterm =
- let varlist =
- let rec aux acc = function
- | Terms.Leaf _ -> acc
- | Terms.Var i -> if List.mem i acc then acc else i::acc
- | Terms.Node l -> List.fold_left aux acc l
- in
- aux (aux [] ty) proofterm
- in
- let lit =
+ let mk_clause maxvar nlit plit proofterm =
+ let foterm_to_lit (acc,literals) ty =
+ let vars = Terms.vars_of_term ~start_acc:acc ty in
match ty with
| Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
let o = Order.compare_terms l r in
- Terms.Equation (l, r, ty, o)
- | t -> Terms.Predicate t
+ (vars,Terms.Equation (l, r, ty, o)::literals)
+ | _ -> (vars,Terms.Predicate ty::literals)
in
+ let varlist = Terms.vars_of_term proofterm in
+ let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in
+ let (varlist,plit) = List.fold_left foterm_to_lit (varlist,[]) plit in
let proof = Terms.Exact proofterm in
- fresh_unit_clause maxvar (0, lit, varlist, proof)
+ fresh_clause maxvar (0, nlit, plit, varlist, proof)
;;
let mk_passive_clause cl =
- (Order.compute_unit_clause_weight cl, cl)
+ (Order.compute_clause_weight cl, cl)
;;
let mk_passive_goal g =
- (Order.compute_unit_clause_weight g, g)
+ (Order.compute_clause_weight g, g)
;;
- let compare_passive_clauses_weight (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =
+ let compare_passive_clauses_weight (w1,(id1,_,_,_,_)) (w2,(id2,_,_,_,_)) =
if w1 = w2 then id1 - id2
else w1 - w2
;;
- let compare_passive_clauses_age (_,(id1,_,_,_)) (_,(id2,_,_,_)) =
+ let compare_passive_clauses_age (_,(id1,_,_,_,_)) (_,(id2,_,_,_,_)) =
id1 - id2
;;
val eq_literal : B.t Terms.literal -> B.t Terms.literal -> bool
val compare_literal : B.t Terms.literal -> B.t Terms.literal -> int
- (* mk_unit_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *)
- val mk_unit_clause :
- int -> B.t Terms.foterm -> B.t Terms.foterm ->
- B.t Terms.unit_clause * int
+ (* mk_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *)
+ val mk_clause :
+ int ->
+ B.t Terms.foterm list -> (* negative literals in clause *)
+ B.t Terms.foterm list -> (* positive literals in clause *)
+ B.t Terms.foterm ->
+ B.t Terms.clause * int
val mk_passive_clause :
- B.t Terms.unit_clause -> B.t Terms.passive_clause
+ B.t Terms.clause -> B.t Terms.passive_clause
val mk_passive_goal :
- B.t Terms.unit_clause -> B.t Terms.passive_clause
+ B.t Terms.clause -> B.t Terms.passive_clause
- val eq_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> bool
- val compare_unit_clause : B.t Terms.unit_clause -> B.t Terms.unit_clause -> int
+ val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool
+ val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int
- val fresh_unit_clause :
- int -> B.t Terms.unit_clause -> B.t Terms.unit_clause * int
+ val fresh_clause :
+ int -> B.t Terms.clause -> B.t Terms.clause * int
(* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *)
val relocate :
module ClauseOT =
struct
- type t = Terms.direction * B.t Terms.unit_clause
+ type t = Terms.direction * B.t Terms.clause
let compare (d1,uc1) (d2,uc2) =
let c = Pervasives.compare d1 d2 in
- if c <> 0 then c else U.compare_unit_clause uc1 uc2
+ if c <> 0 then c else U.compare_clause uc1 uc2
;;
end
module ClauseSet :
- Set.S with type elt = Terms.direction * B.t Terms.unit_clause
+ Set.S with type elt = Terms.direction * B.t Terms.clause
= Set.Make(ClauseOT)
open Discrimination_tree
type dataset = ClauseSet.t
= Make(FotermIndexable)(ClauseSet)
- let index_unit_clause t = function
+ let index_clause t = function
| (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c ->
DT.index t l (Terms.Left2Right, c)
| (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c ->
DT.index t p (Terms.Nodir, c)
;;
- type active_set = B.t Terms.unit_clause list * DT.t
+ type active_set = B.t Terms.clause list * DT.t
end
module Index (B : Orderings.Blob) :
sig
module ClauseSet : Set.S with
- type elt = Terms.direction * B.t Terms.unit_clause
+ type elt = Terms.direction * B.t Terms.clause
module FotermIndexable : Discrimination_tree.Indexable with
type constant_name = B.t and
type data = ClauseSet.elt and
type dataset = ClauseSet.t
- val index_unit_clause :
- DT.t -> B.t Terms.unit_clause -> DT.t
+ val index_clause :
+ DT.t -> B.t Terms.clause -> DT.t
- type active_set = B.t Terms.unit_clause list * DT.t
+ type active_set = B.t Terms.clause list * DT.t
end
val compare_terms :
t Terms.foterm -> t Terms.foterm -> Terms.comparison
- val compute_unit_clause_weight : 't Terms.unit_clause -> int
-
- val compute_goal_weight : 't Terms.unit_clause -> int
+ val compute_clause_weight : 't Terms.clause -> int
val name : string
(w, List.sort compare l) (* from the smallest meta to the bigest *)
;;
-let compute_unit_clause_weight (_,l, _, _) =
+let compute_literal_weight l =
let weight_of_polynomial w m =
let factor = 2 in
w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
weight_of_polynomial (wl+wr) (ml@mr)
;;
-let compute_goal_weight (_,l, _, _) =
- let weight_of_polynomial w m =
- let factor = 2 in
- w + factor * List.fold_left (fun acc (_,occ) -> acc+occ) 0 m
- in
- match l with
- | Terms.Predicate t ->
- let w, m = weight_of_term t in
- weight_of_polynomial w m
- | Terms.Equation (l,r,_,_) ->
- let wl, ml = weight_of_term l in
- let wr, mr = weight_of_term r in
- let wl = weight_of_polynomial wl ml in
- let wr = weight_of_polynomial wr mr in
- - (abs (wl-wr))
- ;;
+let compute_clause_weight (_,nl,pl,_,_) =
+ List.fold_left (fun acc lit -> compute_literal_weight lit + acc) 0 (nl@pl)
+
+let compute_goal_weight = compute_clause_weight;;
(* Riazanov: 3.1.5 pag 38 *)
(* Compare weights normalized in a new way :
let eq_foterm = eq_foterm B.eq;;
- let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let compute_clause_weight = compute_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
(* Riazanov: p. 40, relation >_n *)
let eq_foterm = eq_foterm B.eq;;
- let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let compute_clause_weight = compute_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
(* Riazanov: p. 38, relation > *)
let eq_foterm = eq_foterm B.eq;;
- let compute_unit_clause_weight = compute_unit_clause_weight;;
+ let compute_clause_weight = compute_clause_weight;;
let compute_goal_weight = compute_goal_weight;;
let rec lpo s t =
(* these could be outside the module, but to ease experimentation
* we allow them to be tied with the ordering *)
- val compute_unit_clause_weight : 't Terms.unit_clause -> int
- val compute_goal_weight : 't Terms.unit_clause -> int
+ val compute_clause_weight : 't Terms.clause -> int
val name : string
module Utils = FoUtils.Utils(B)
module Pp = Pp.Pp(B)
- exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+ exception Success of B.t Terms.bag * int * B.t Terms.clause
let debug s = prerr_endline s;;
let debug _ = ();;
((*prerr_endline ("Filtering: " ^
Pp.pp_foterm side ^ " =(< || =)" ^
Pp.pp_foterm newside ^ " coming from " ^
- Pp.pp_unit_clause uc );*)None)
+ Pp.pp_clause uc );*)None)
else
Some (newside, subst, id, dir)
with FoUnif.UnificationFailure _ -> None)
(* in
if are_alpha_eq c1 c2 then bag1,c1
else begin
- prerr_endline (Pp.pp_unit_clause c1);
- prerr_endline (Pp.pp_unit_clause c2);
+ prerr_endline (Pp.pp_clause c1);
+ prerr_endline (Pp.pp_clause c2);
prerr_endline "Bag :";
prerr_endline (Pp.pp_bag bag1);
assert false
match simplify atable maxvar bag new_clause with
| bag,None -> bag,None (* new_clause has been discarded *)
| bag,(Some clause) ->
- let ctable = IDX.index_unit_clause IDX.DT.empty clause in
+ let ctable = IDX.index_clause IDX.DT.empty clause in
let bag, alist, atable =
List.fold_left
(fun (bag, alist, atable) c ->
|bag,None -> (bag,alist,atable)
(* an active clause as been discarded *)
|bag,Some c1 ->
- bag, c :: alist, IDX.index_unit_clause atable c)
+ bag, c :: alist, IDX.index_clause atable c)
(bag,[],IDX.DT.empty) alist
in
bag, Some (clause, (alist,atable))
let simplification_step ~new_cl cl (alist,atable) bag maxvar new_clause =
let atable1 =
if new_cl then atable else
- IDX.index_unit_clause atable cl
+ IDX.index_clause atable cl
in
(* Simplification of new_clause with : *
* - actives and cl if new_clause is not cl *
| bag,Some clause ->
(* Simplification of each active clause with clause *
* which is the simplified form of new_clause *)
- let ctable = IDX.index_unit_clause IDX.DT.empty clause in
+ let ctable = IDX.index_clause IDX.DT.empty clause in
let bag, newa, alist, atable =
List.fold_left
(fun (bag, newa, alist, atable) c ->
|bag,Some c1 ->
if (c1 == c) then
bag, newa, c :: alist,
- IDX.index_unit_clause atable c
+ IDX.index_clause atable c
else
bag, c1 :: newa, alist, atable)
(bag,[],[],IDX.DT.empty) alist
| bag,(None, Some _) -> bag,None
| bag,(Some cl1, Some (clause, (alist,atable), newa)) ->
let alist,atable =
- (clause::alist, IDX.index_unit_clause atable clause)
+ (clause::alist, IDX.index_clause atable clause)
in
keep_simplified_aux ~new_cl:(cl!=cl1) cl1 (alist,atable)
bag (newa@tl)
(* We demodulate actives clause with current until all *
* active clauses are reduced w.r.t each other *)
(* let bag, (alist,atable) = keep_simplified (alist,atable) bag [current] in *)
- let ctable = IDX.index_unit_clause IDX.DT.empty current in
+ let ctable = IDX.index_clause IDX.DT.empty current in
(* let bag, (alist, atable) =
let bag, alist =
HExtlib.filter_map_acc (simplify ctable) bag alist
in
- bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist)
+ bag, (alist, List.fold_left IDX.index_clause IDX.DT.empty alist)
in*)
debug "Simplified active clauses with fact";
(* We superpose active clauses with current *)
(* We add current to active clauses so that it can be *
* superposed with itself *)
let alist, atable =
- current :: alist, IDX.index_unit_clause atable current
+ current :: alist, IDX.index_clause atable current
in
debug "Indexed";
- let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
+ let fresh_current, maxvar = Utils.fresh_clause maxvar current in
(* We need to put fresh_current into the bag so that all *
* variables clauses refer to are known. *)
let bag, fresh_current = Terms.add_to_bag fresh_current bag in
sig
(* bag, maxvar, meeting point *)
- exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+ exception Success of B.t Terms.bag * int * B.t Terms.clause
(* The returned active set is the input one + the selected clause *)
val infer_right :
B.t Terms.bag ->
int -> (* maxvar *)
- B.t Terms.unit_clause -> (* selected passive *)
+ B.t Terms.clause -> (* selected passive *)
Index.Index(B).active_set ->
- B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.unit_clause list
+ B.t Terms.bag * int * Index.Index(B).active_set * B.t Terms.clause list
val infer_left :
B.t Terms.bag ->
int -> (* maxvar *)
- B.t Terms.unit_clause -> (* selected goal *)
+ B.t Terms.clause -> (* selected goal *)
Index.Index(B).active_set ->
- B.t Terms.bag * int * B.t Terms.unit_clause list
+ B.t Terms.bag * int * B.t Terms.clause list
val demodulate :
B.t Terms.bag ->
- B.t Terms.unit_clause ->
- Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.unit_clause
+ B.t Terms.clause ->
+ Index.Index(B).DT.t -> B.t Terms.bag * B.t Terms.clause
val simplify :
Index.Index(B).DT.t ->
int ->
B.t Terms.bag ->
- B.t Terms.unit_clause ->
- B.t Terms.bag * (B.t Terms.unit_clause option)
+ B.t Terms.clause ->
+ B.t Terms.bag * (B.t Terms.clause option)
(* may raise success *)
val simplify_goal :
int ->
Index.Index(B).DT.t ->
B.t Terms.bag ->
- B.t Terms.unit_clause list ->
- B.t Terms.unit_clause ->
- (B.t Terms.bag * B.t Terms.unit_clause) option
+ B.t Terms.clause list ->
+ B.t Terms.clause ->
+ (B.t Terms.bag * B.t Terms.clause) option
val one_pass_simplification:
- B.t Terms.unit_clause ->
+ B.t Terms.clause ->
Index.Index(B).active_set ->
B.t Terms.bag ->
int ->
- B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
+ B.t Terms.bag * (B.t Terms.clause * Index.Index(B).active_set) option
val keep_simplified:
- B.t Terms.unit_clause ->
+ B.t Terms.clause ->
Index.Index(B).active_set ->
B.t Terms.bag ->
int ->
- B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
+ B.t Terms.bag * (B.t Terms.clause * Index.Index(B).active_set) option
val orphan_murder:
B.t Terms.bag ->
- B.t Terms.unit_clause list ->
- B.t Terms.unit_clause ->
+ B.t Terms.clause list ->
+ B.t Terms.clause ->
bool
* varlist (* variable list *)
* 'a proof (* proof *)
-type 'a passive_clause = int * 'a unit_clause (* weight * equation *)
+type 'a clause =
+ int
+ * 'a literal list (* left hand side of the arrow *)
+ * 'a literal list (* right hand side of the arrow *)
+ * varlist
+ * 'a proof
+type 'a passive_clause = int * 'a clause (* weight * equation *)
-let vars_of_term t =
+
+let vars_of_term ?(start_acc=[]) t =
let rec aux acc = function
| Leaf _ -> acc
| Var i -> if (List.mem i acc) then acc else i::acc
| Node l -> List.fold_left aux acc l
- in aux [] t
+ in aux start_acc t
;;
module OT =
* varlist
* 'a proof (* proof *)
-type 'a passive_clause = int * 'a unit_clause (* weight * equation *)
+type 'a clause =
+ int
+ * 'a literal list (* left hand side of the arrow *)
+ * 'a literal list (* right hand side of the arrow *)
+ * varlist
+ * 'a proof
-val vars_of_term : 'a foterm -> int list
+type 'a passive_clause = int * 'a clause (* weight * equation *)
+
+val vars_of_term : ?start_acc:int list -> 'a foterm -> int list
module M : Map.S with type key = int
-utf8Macro.cmi:
-utf8MacroTable.cmo:
-utf8MacroTable.cmx:
utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi
utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi
EXTRA_OBJECTS_TO_INSTALL =
EXTRA_OBJECTS_TO_CLEAN =
-TPTPDIR= /home/$(USER)/work-area/TPTP-v3.2.0/
+TPTPDIR= /home/maxime/TPTP-v3.7.0/
all: tptp2grafite
clean: clean_tests
name COMMA formula_type COMMA formula formula_source_and_infos
RPAREN DOT {
AnnotatedFormula ($3,$5,$7,fst $8,snd $8)
- }
+ }
+ | CNF LPAREN
+ TYPE COMMA formula_type COMMA formula formula_source_and_infos
+ RPAREN DOT {
+ AnnotatedFormula ($3,$5,$7,fst $8,snd $8)
+ }
;
formula_type:
projects / helm.git / commitdiff