From 95a14ced97592a4116485f94c6ffa806feb62dbc Mon Sep 17 00:00:00 2001 From: denes Date: Fri, 17 Jul 2009 09:37:13 +0000 Subject: [PATCH] Branched paramodulation for CNF (Horn clauses) --- .../binaries/matitaprover/run_on_a_list.sh | 2 +- .../components/binaries/transcript/.depend | 5 --- .../binaries/transcript/.depend.opt | 5 --- helm/software/components/extlib/hExtlib.ml | 4 +- .../components/ng_paramodulation/foUtils.ml | 43 +++++++++---------- .../components/ng_paramodulation/foUtils.mli | 23 +++++----- .../components/ng_paramodulation/index.ml | 10 ++--- .../components/ng_paramodulation/index.mli | 8 ++-- .../components/ng_paramodulation/orderings.ml | 32 ++++---------- .../ng_paramodulation/orderings.mli | 3 +- .../ng_paramodulation/superposition.ml | 28 ++++++------ .../ng_paramodulation/superposition.mli | 36 ++++++++-------- .../components/ng_paramodulation/terms.ml | 13 ++++-- .../components/ng_paramodulation/terms.mli | 11 ++++- .../components/syntax_extensions/.depend | 3 -- .../software/components/tptp_grafite/Makefile | 2 +- .../components/tptp_grafite/parser.mly | 7 ++- 17 files changed, 113 insertions(+), 122 deletions(-) diff --git a/helm/software/components/binaries/matitaprover/run_on_a_list.sh b/helm/software/components/binaries/matitaprover/run_on_a_list.sh index b62aa8974..c80e128e2 100755 --- a/helm/software/components/binaries/matitaprover/run_on_a_list.sh +++ b/helm/software/components/binaries/matitaprover/run_on_a_list.sh @@ -8,7 +8,7 @@ fi > 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 diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index 87d1ed25c..bb6f22a64 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,11 +1,6 @@ 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 diff --git a/helm/software/components/binaries/transcript/.depend.opt b/helm/software/components/binaries/transcript/.depend.opt index f17459162..efadc681e 100644 --- a/helm/software/components/binaries/transcript/.depend.opt +++ b/helm/software/components/binaries/transcript/.depend.opt @@ -1,11 +1,6 @@ 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 diff --git a/helm/software/components/extlib/hExtlib.ml b/helm/software/components/extlib/hExtlib.ml index cccb46767..7ae392c5f 100644 --- a/helm/software/components/extlib/hExtlib.ml +++ b/helm/software/components/extlib/hExtlib.ml @@ -27,9 +27,9 @@ (** 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 diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index 7b57e5bb3..8c75baeea 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -69,8 +69,8 @@ module Utils (B : Orderings.Blob) = struct | 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 @@ -79,10 +79,9 @@ module Utils (B : Orderings.Blob) = struct 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 @@ -92,50 +91,48 @@ module Utils (B : Orderings.Blob) = struct 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 ;; diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli index d725d3c7f..48ef1d90b 100644 --- a/helm/software/components/ng_paramodulation/foUtils.mli +++ b/helm/software/components/ng_paramodulation/foUtils.mli @@ -21,23 +21,26 @@ module Utils (B : Orderings.Blob) : 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 : diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml index 889e1e7ef..c7a0edcca 100644 --- a/helm/software/components/ng_paramodulation/index.ml +++ b/helm/software/components/ng_paramodulation/index.ml @@ -16,16 +16,16 @@ module Index(B : Orderings.Blob) = struct 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 @@ -79,7 +79,7 @@ module Index(B : Orderings.Blob) = struct 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 -> @@ -93,6 +93,6 @@ module Index(B : Orderings.Blob) = struct 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 diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli index 7d75f2837..51934d1b1 100644 --- a/helm/software/components/ng_paramodulation/index.mli +++ b/helm/software/components/ng_paramodulation/index.mli @@ -14,7 +14,7 @@ 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 @@ -26,9 +26,9 @@ module Index (B : Orderings.Blob) : 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 diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml index ba6969aeb..f2151528f 100644 --- a/helm/software/components/ng_paramodulation/orderings.ml +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -25,9 +25,7 @@ module type Blob = 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 @@ -76,7 +74,7 @@ let weight_of_term term = (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 @@ -96,22 +94,10 @@ let compute_unit_clause_weight (_,l, _, _) = 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 : @@ -206,7 +192,7 @@ module NRKBO (B : Terms.Blob) = struct 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 *) @@ -239,7 +225,7 @@ module KBO (B : Terms.Blob) = struct 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 > *) @@ -304,7 +290,7 @@ module LPO (B : Terms.Blob) = struct 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 = diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli index a6d1a8743..7c66cc40b 100644 --- a/helm/software/components/ng_paramodulation/orderings.mli +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -25,8 +25,7 @@ module type Blob = (* 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 diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 0a7c5cfcc..54f7e1046 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -20,7 +20,7 @@ module Superposition (B : Orderings.Blob) = 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 _ = ();; @@ -165,7 +165,7 @@ module Superposition (B : Orderings.Blob) = ((*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) @@ -273,8 +273,8 @@ module Superposition (B : Orderings.Blob) = (* 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 @@ -481,7 +481,7 @@ module Superposition (B : Orderings.Blob) = 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 -> @@ -489,7 +489,7 @@ module Superposition (B : Orderings.Blob) = |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)) @@ -502,7 +502,7 @@ module Superposition (B : Orderings.Blob) = 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 * @@ -513,7 +513,7 @@ module Superposition (B : Orderings.Blob) = | 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 -> @@ -523,7 +523,7 @@ module Superposition (B : Orderings.Blob) = |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 @@ -565,7 +565,7 @@ module Superposition (B : Orderings.Blob) = | 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) @@ -693,12 +693,12 @@ module Superposition (B : Orderings.Blob) = (* 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 *) @@ -715,10 +715,10 @@ module Superposition (B : Orderings.Blob) = (* 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 diff --git a/helm/software/components/ng_paramodulation/superposition.mli b/helm/software/components/ng_paramodulation/superposition.mli index 30d32d540..ad780c82c 100644 --- a/helm/software/components/ng_paramodulation/superposition.mli +++ b/helm/software/components/ng_paramodulation/superposition.mli @@ -15,34 +15,34 @@ module Superposition (B : Orderings.Blob) : 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 : @@ -50,29 +50,29 @@ module Superposition (B : Orderings.Blob) : 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 diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 9a225fd27..db4c8cad6 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -44,15 +44,22 @@ type 'a unit_clause = * 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 = diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 47295035c..dfed661d4 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -50,9 +50,16 @@ type 'a unit_clause = * 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 diff --git a/helm/software/components/syntax_extensions/.depend b/helm/software/components/syntax_extensions/.depend index 25e67131f..f3c6a8bd1 100644 --- a/helm/software/components/syntax_extensions/.depend +++ b/helm/software/components/syntax_extensions/.depend @@ -1,5 +1,2 @@ -utf8Macro.cmi: -utf8MacroTable.cmo: -utf8MacroTable.cmx: utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi diff --git a/helm/software/components/tptp_grafite/Makefile b/helm/software/components/tptp_grafite/Makefile index c196dd609..3c130f216 100644 --- a/helm/software/components/tptp_grafite/Makefile +++ b/helm/software/components/tptp_grafite/Makefile @@ -7,7 +7,7 @@ IMPLEMENTATION_FILES = ast.ml lexer.ml $(INTERFACE_FILES:%.mli=%.ml) 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 diff --git a/helm/software/components/tptp_grafite/parser.mly b/helm/software/components/tptp_grafite/parser.mly index 4fe172144..0f3525689 100644 --- a/helm/software/components/tptp_grafite/parser.mly +++ b/helm/software/components/tptp_grafite/parser.mly @@ -56,7 +56,12 @@ 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: -- 2.39.2