Various architectural changes

[helm.git] / helm / software / components / binaries / matitaprover / tptp_cnf.ml

diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.ml b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
index 8c38d6e6571eaee3b27064fc867a57c4a257d93c..06f777ff64a51830cd0e7b26462973960f975e3d 100644 (file)
--- a/helm/software/components/binaries/matitaprover/tptp_cnf.ml
+++ b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
@@ -5,23 +5,28 @@ let trans_atom = function
   | Ast.NotEq (a,b) -> false, Ast.Function ("==",[Ast.Constant "_"; a; b])
 ;;
 
-let trans_formulae = function
-  | Ast.Disjunction _ -> assert false
-  | Ast.Atom a -> trans_atom a
+let rec trans_formulae (nlit,plit) = function
+  | Ast.Disjunction (a,b) ->
+         trans_formulae (trans_formulae (nlit,plit) b) a
+  | Ast.Atom a ->
+         let is_positive,lit = trans_atom a in
+         if is_positive then (nlit,lit::plit) else (lit::nlit,plit)
   | Ast.NegAtom _ -> assert false
 ;;
 
+let trans_formulae = trans_formulae ([],[]);;
+
 
 (* HELPERS *)
 let resolve ~tptppath s = 
   let resolved_name = 
+    if HExtlib.is_regular s then s else
     if tptppath = "/" then s else
-      if Filename.check_suffix s ".p" then
-        (assert (String.length s > 5);
-        let prefix = String.sub s 0 3 in
-        tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
-      else
-        tptppath ^ "/" ^ s
+    if Filename.check_suffix s ".p" then
+     (assert (String.length s > 5);
+     let prefix = String.sub s 0 3 in
+     tptppath ^ "/Problems/" ^ prefix ^ "/" ^ s)
+    else tptppath ^ "/" ^ s
   in
   if HExtlib.is_regular resolved_name then
     resolved_name
@@ -50,9 +55,9 @@ let parse ~tptppath filename =
       | Ast.Comment _ :: tl -> aux p n tl
       | Ast.AnnotatedFormula (name, 
           (Ast.Axiom | Ast.Hypothesis|Ast.Negated_conjecture), f,_,_) :: tl->
-          let is_positive, f = trans_formulae f in
-          if is_positive then aux (p@[Ast.Constant name,f]) n tl
-          else aux p (n@[Ast.Constant name,f]) tl
+          let (nlit,plit) = trans_formulae f in
+             if plit = [] then aux p (n@[Ast.Constant name,(nlit,plit)]) tl
+             else aux (p@[Ast.Constant name,(nlit,plit)]) n tl
       | _ -> prerr_endline "bad syntax"; assert false
     in
       aux [] [] statements