]> matita.cs.unibo.it Git - helm.git/commitdiff
Branched paramodulation for CNF (Horn clauses)
authordenes <??>
Fri, 17 Jul 2009 09:37:13 +0000 (09:37 +0000)
committerdenes <??>
Fri, 17 Jul 2009 09:37:13 +0000 (09:37 +0000)
17 files changed:
helm/software/components/binaries/matitaprover/run_on_a_list.sh
helm/software/components/binaries/transcript/.depend
helm/software/components/binaries/transcript/.depend.opt
helm/software/components/extlib/hExtlib.ml
helm/software/components/ng_paramodulation/foUtils.ml
helm/software/components/ng_paramodulation/foUtils.mli
helm/software/components/ng_paramodulation/index.ml
helm/software/components/ng_paramodulation/index.mli
helm/software/components/ng_paramodulation/orderings.ml
helm/software/components/ng_paramodulation/orderings.mli
helm/software/components/ng_paramodulation/superposition.ml
helm/software/components/ng_paramodulation/superposition.mli
helm/software/components/ng_paramodulation/terms.ml
helm/software/components/ng_paramodulation/terms.mli
helm/software/components/syntax_extensions/.depend
helm/software/components/tptp_grafite/Makefile
helm/software/components/tptp_grafite/parser.mly

index b62aa8974b19661618a6a1fe76c99bfd8c1de914..c80e128e218c2aec2cd952be1c189d984d4c5842 100755 (executable)
@@ -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
index 87d1ed25c2745435771cee189c10da4a99854448..bb6f22a64b02f88c3881f2c3f490d7f81b186897 100644 (file)
@@ -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 
index f17459162ce81c0ad9c5352cca5e9d99f43cb81c..efadc681eee16cb3cd170845fdd1c7549fbb89b0 100644 (file)
@@ -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 
index cccb467674e22415b59de320e72cbbe845812142..7ae392c5f3534b2dfaa695d6d3a663159fa33dfe 100644 (file)
@@ -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
index 7b57e5bb3d2037b98ff681521c3b55d1ecd6a2cc..8c75baeea18e058f2999fe77a90949b3d8f72d7f 100644 (file)
@@ -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
   ;;
 
index d725d3c7f89126e3f76afb95fd5de9b75d439400..48ef1d90b722bce21765d45baad59825b8b5e0d0 100644 (file)
@@ -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 : 
index 889e1e7ef14955960fb1b88bbb7d8f40581ecf1c..c7a0edcca2bff6e43d7d8165278ae0668f7ebcd4 100644 (file)
@@ -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
index 7d75f28370d00eb487764e4e8d87cd5b18c40f33..51934d1b1f592a1afe69620a47a551ba8dbd0785 100644 (file)
@@ -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
index ba6969aeb143ddaa1df97d72ea3ff61b4c2bcaab..f2151528f698df8472f17c2d608bb2e03a5729ed 100644 (file)
@@ -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 =
index a6d1a87432f71acc0c47cdfa44492b78e092ec64..7c66cc40bced62d6e3a889a38164627513a41064 100644 (file)
@@ -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
 
index 0a7c5cfcc1c82fdb0be718e4ddde26bca391d876..54f7e10466a2a3550d7c08fc50cead3246b60ba4 100644 (file)
@@ -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
index 30d32d540a330d8bdb9495b086a134e0fffd5391..ad780c82c1e1f3fc645cc6a193b59886d2401dbc 100644 (file)
@@ -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
 
 
index 9a225fd27b2807f3a3ea37d57276eb93332e384a..db4c8cad6bce2680f9b98f538373cb8a9c274d5d 100644 (file)
@@ -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 =
index 47295035ca47e7196beb616887c4d98cccbb7a5c..dfed661d4576ba9b0799c4a61669cc98be653ec4 100644 (file)
@@ -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 
 
index 25e67131fca0487c4390d310d8307722b5058067..f3c6a8bd17a7351e99ce8e59905fda76a37cbf08 100644 (file)
@@ -1,5 +1,2 @@
-utf8Macro.cmi: 
-utf8MacroTable.cmo: 
-utf8MacroTable.cmx: 
 utf8Macro.cmo: utf8MacroTable.cmo utf8Macro.cmi 
 utf8Macro.cmx: utf8MacroTable.cmx utf8Macro.cmi 
index c196dd609e418ccd733d2f51b8a00da848ae3a5b..3c130f2161392e9f5f5273652a2525752d3c89b2 100644 (file)
@@ -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
index 4fe172144a4a2636f11f0d840c42ed07fc9f0624..0f3525689212de5c2ae37b3a20d91363018f3afd 100644 (file)
             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: