src/Tools/Metis/src/metis.sml

 (* ========================================================================= *)
 (* METIS FIRST ORDER PROVER                                                  *)
 (*                                                                           *)
-(* Copyright (c) 2001-2007 Joe Hurd                                          *)
+(* Copyright (c) 2001 Joe Hurd                                               *)
 (*                                                                           *)
 (* Metis is free software; you can redistribute it and/or modify             *)
 (* it under the terms of the GNU General Public License as published by      *)
 (* the Free Software Foundation; either version 2 of the License, or         *)
 (* (at your option) any later version.                                       *)

 (* ========================================================================= *)
 
 open Useful;
 
 (* ------------------------------------------------------------------------- *)
-(* The program name.                                                         *)
+(* The program name and version.                                             *)
 (* ------------------------------------------------------------------------- *)
 
 val PROGRAM = "metis";
 
+val VERSION = "2.2";
+
+val versionString = PROGRAM^" "^VERSION^" (release 20100825)"^"\n";
+
 (* ------------------------------------------------------------------------- *)
 (* Program options.                                                          *)
 (* ------------------------------------------------------------------------- *)
 
 val QUIET = ref false;
 
 val TEST = ref false;
 
-val ITEMS = ["name","goal","clauses","size","category","proof","saturated"];
+val TPTP : string option ref = ref NONE;
+
+val ITEMS = ["name","goal","clauses","size","category","proof","saturation"];
+
+val extended_items = "all" :: ITEMS;
 
 val show_items = map (fn s => (s, ref false)) ITEMS;
 
 fun show_ref s =
     case List.find (equal s o fst) show_items of
       NONE => raise Bug ("item " ^ s ^ " not found")
     | SOME (_,r) => r;
 
+fun show_set b = app (fn (_,r) => r := b) show_items;
+
 fun showing s = not (!QUIET) andalso (s = "status" orelse !(show_ref s));
 
 fun notshowing s = not (showing s);
 
 fun showing_any () = List.exists showing ITEMS;
 
 fun notshowing_any () = not (showing_any ());
 
-fun show s = case show_ref s of r => r := true;
-
-fun hide s = case show_ref s of r => r := false;
+fun show "all" = show_set true
+  | show s = case show_ref s of r => r := true;
+
+fun hide "all" = show_set false
+  | hide s = case show_ref s of r => r := false;
+
+(* ------------------------------------------------------------------------- *)
+(* Process command line arguments and environment variables.                 *)
+(* ------------------------------------------------------------------------- *)
 
 local
   open Useful Options;
 in
   val specialOptions =
     [{switches = ["--show"], arguments = ["ITEM"],
       description = "show ITEM (see below for list)",
       processor =
-        beginOpt (enumOpt ITEMS endOpt) (fn _ => fn s => show s)},
+        beginOpt (enumOpt extended_items endOpt) (fn _ => fn s => show s)},
      {switches = ["--hide"], arguments = ["ITEM"],
       description = "hide ITEM (see below for list)",
       processor =
-        beginOpt (enumOpt ITEMS endOpt) (fn _ => fn s => hide s)},
+        beginOpt (enumOpt extended_items endOpt) (fn _ => fn s => hide s)},
+     {switches = ["--tptp"], arguments = ["DIR"],
+      description = "specify the TPTP installation directory",
+      processor =
+        beginOpt (stringOpt endOpt) (fn _ => fn s => TPTP := SOME s)},
      {switches = ["-q","--quiet"], arguments = [],
       description = "Run quietly; indicate provability with return value",
       processor = beginOpt endOpt (fn _ => QUIET := true)},
      {switches = ["--test"], arguments = [],
       description = "Skip the proof search for the input problems",
       processor = beginOpt endOpt (fn _ => TEST := true)}];
 end;
 
-val VERSION = "2.0";
-
-val versionString = "Metis "^VERSION^" (release 20071110)"^"\n";
-
 val programOptions =
     {name = PROGRAM,
      version = versionString,
      header = "usage: "^PROGRAM^" [option ...] problem.tptp ...\n" ^
               "Proves the input TPTP problem files.\n",
-     footer = "Possible ITEMs are {" ^ join "," ITEMS ^ "}.\n" ^
+     footer = "Possible ITEMs are {" ^ join "," extended_items ^ "}.\n" ^
               "Problems can be read from standard input using the " ^
               "special - filename.\n",
      options = specialOptions @ Options.basicOptions};
 
 fun exit x : unit = Options.exit programOptions x;
 fun succeed () = Options.succeed programOptions;
 fun fail mesg = Options.fail programOptions mesg;
 fun usage mesg = Options.usage programOptions mesg;
 
-val (opts,work) =
-    Options.processOptions programOptions (CommandLine.arguments ());
-
-val () = if null work then usage "no input problem files" else ();
+fun processOptions () =
+    let
+      val args = CommandLine.arguments ()
+
+      val (_,work) = Options.processOptions programOptions args
+
+      val () =
+          case !TPTP of
+            SOME _ => ()
+          | NONE => TPTP := OS.Process.getEnv "TPTP"
+    in
+      work
+    end;
 
 (* ------------------------------------------------------------------------- *)
 (* The core application.                                                     *)
 (* ------------------------------------------------------------------------- *)
+
+(*MetisDebug
+val next_cnf =
+    let
+      val cnf_counter = ref 0
+    in
+      fn () =>
+         let
+           val ref cnf_count = cnf_counter
+           val () = cnf_counter := cnf_count + 1
+         in
+           cnf_count
+         end
+    end;
+*)
 
 local
   fun display_sep () =
       if notshowing_any () then ()
-      else print (nChars #"-" (!Parser.lineLength) ^ "\n");
+      else print (nChars #"-" (!Print.lineLength) ^ "\n");
 
   fun display_name filename =
       if notshowing "name" then ()
       else print ("Problem: " ^ filename ^ "\n\n");
 
-  fun display_goal goal =
+  fun display_goal tptp =
       if notshowing "goal" then ()
-      else print ("Goal:\n" ^ Formula.toString goal ^ "\n\n");
+      else
+        let
+          val goal = Tptp.goal tptp
+        in
+          print ("Goal:\n" ^ Formula.toString goal ^ "\n\n")
+        end;
 
   fun display_clauses cls =
       if notshowing "clauses" then ()
       else print ("Clauses:\n" ^ Problem.toString cls ^ "\n\n");
 

       if notshowing "size" then ()
       else
         let
           fun plural 1 s = "1 " ^ s
             | plural n s = Int.toString n ^ " " ^ s ^ "s"
-                           
+
           val {clauses,literals,symbols,typedSymbols} = Problem.size cls
         in
           print
             ("Size: " ^
              plural clauses "clause" ^ ", " ^
              plural literals "literal" ^ ", " ^
              plural symbols "symbol" ^ ", " ^
              plural typedSymbols "typed symbol" ^ ".\n\n")
         end;
-        
+
   fun display_category cls =
       if notshowing "category" then ()
       else
         let
           val cat = Problem.categorize cls
         in
           print ("Category: " ^ Problem.categoryToString cat ^ ".\n\n")
         end;
 
-  fun display_proof filename th = 
-      if notshowing "proof" then ()
+  local
+    fun display_proof_start filename =
+        print ("\nSZS output start CNFRefutation for " ^ filename ^ "\n");
+
+    fun display_proof_body problem proofs =
+        let
+          val comments = []
+
+          val includes = []
+
+          val formulas =
+              Tptp.fromProof
+                {problem = problem,
+                 proofs = proofs}
+
+          val proof =
+              Tptp.Problem
+                {comments = comments,
+                 includes = includes,
+                 formulas = formulas}
+
+          val mapping = Tptp.defaultMapping
+          val mapping = Tptp.addVarSetMapping mapping (Tptp.freeVars proof)
+
+          val filename = "-"
+        in
+          Tptp.write
+            {problem = proof,
+             mapping = mapping,
+             filename = filename}
+        end;
+
+    fun display_proof_end filename =
+        print ("SZS output end CNFRefutation for " ^ filename ^ "\n\n");
+  in
+    fun display_proof filename problem proofs =
+        if notshowing "proof" then ()
+        else
+          let
+            val () = display_proof_start filename
+            val () = display_proof_body problem proofs
+            val () = display_proof_end filename
+          in
+            ()
+          end;
+  end;
+
+  fun display_saturation filename ths =
+      if notshowing "saturation" then ()
       else
-        (print ("SZS output start CNFRefutation for " ^ filename ^ "\n");
-         print (Tptp.proofToString (Proof.proof th));
-         print ("SZS output end CNFRefutation for " ^ filename ^ "\n\n"));
-
-  fun display_saturated filename ths =
-      if notshowing "saturated" then ()
-      else
-        let
-(*DEBUG
-          val () = Tptp.write {filename = "saturated.tptp"}
-                     (Tptp.fromProblem (map Thm.clause ths))
+        let
+(*MetisDebug
+          val () =
+              let
+                val problem =
+                    Tptp.mkProblem
+                      {comments = ["Saturation clause set for " ^ filename],
+                       includes = [],
+                       names = Tptp.noClauseNames,
+                       roles = Tptp.noClauseRoles,
+                       problem = {axioms = [],
+                                  conjecture = map Thm.clause ths}}
+
+                val mapping =
+                    Tptp.addVarSetMapping Tptp.defaultMapping
+                      (Tptp.freeVars problem)
+              in
+                Tptp.write
+                  {problem = problem,
+                   mapping = mapping,
+                   filename = "saturation.tptp"}
+              end
 *)
-          val () = print ("SZS output start Saturated for " ^ filename ^ "\n")
+          val () = print ("\nSZS output start Saturation for " ^ filename ^ "\n")
           val () = app (fn th => print (Thm.toString th ^ "\n")) ths
-          val () = print ("SZS output end Saturated for " ^ filename ^ "\n\n")
+          val () = print ("SZS output end Saturation for " ^ filename ^ "\n\n")
         in
           ()
         end;
-
-  fun display_result filename result =
-      case result of
-        Resolution.Contradiction th => display_proof filename th
-      | Resolution.Satisfiable ths => display_saturated filename ths;
 
   fun display_status filename status =
       if notshowing "status" then ()
-      else print ("SZS status " ^ status ^ " for " ^ filename ^ "\n");
+      else print ("SZS status " ^ Tptp.toStringStatus status ^
+                  " for " ^ filename ^ "\n");
 
   fun display_problem filename cls =
       let
-(*DEBUG
-        val () = Tptp.write {filename = "cnf.tptp"} (Tptp.fromProblem cls)
+(*MetisDebug
+        val () =
+            let
+              val problem =
+                  Tptp.mkProblem
+                    {comments = ["CNF clauses for " ^ filename],
+                     includes = [],
+                     names = Tptp.noClauseNames,
+                     roles = Tptp.noClauseRoles,
+                     problem = cls}
+
+              val mapping =
+                  Tptp.addVarSetMapping Tptp.defaultMapping
+                    (Tptp.freeVars problem)
+
+              val filename = "cnf_" ^ Int.toString (next_cnf ()) ^ ".tptp"
+            in
+              Tptp.write
+                {problem = problem,
+                 mapping = mapping,
+                 filename = filename}
+            end
 *)
         val () = display_clauses cls
         val () = display_size cls
         val () = display_category cls
       in
         ()
       end;
 
-  fun display_problems filename problems =
-      List.app (display_problem filename) problems;
-
-  fun refute cls =
-      Resolution.loop (Resolution.new Resolution.default (map Thm.axiom cls));
-
-  fun refutable filename cls =
+  fun mkTptpFilename filename =
+      case !TPTP of
+        NONE => filename
+      | SOME tptp =>
+        let
+          val tptp = stripSuffix (equal #"/") tptp
+        in
+          tptp ^ "/" ^ filename
+        end;
+
+  fun readIncludes mapping seen formulas includes =
+      case includes of
+        [] => formulas
+      | inc :: includes =>
+        if StringSet.member inc seen then
+          readIncludes mapping seen formulas includes
+        else
+          let
+            val seen = StringSet.add seen inc
+
+            val filename = mkTptpFilename inc
+
+            val Tptp.Problem {includes = i, formulas = f, ...} =
+                Tptp.read {filename = filename, mapping = mapping}
+
+            val formulas = f @ formulas
+
+            val includes = List.revAppend (i,includes)
+          in
+            readIncludes mapping seen formulas includes
+          end;
+
+  fun read mapping filename =
       let
-        val () = display_problem filename cls
+        val problem = Tptp.read {filename = filename, mapping = mapping}
+
+        val Tptp.Problem {comments,includes,formulas} = problem
       in
-        case refute cls of
-          Resolution.Contradiction th => (display_proof filename th; true)
-        | Resolution.Satisfiable ths => (display_saturated filename ths; false)
+        if null includes then problem
+        else
+          let
+            val seen = StringSet.empty
+
+            val includes = rev includes
+
+            val formulas = readIncludes mapping seen formulas includes
+          in
+            Tptp.Problem
+              {comments = comments,
+               includes = [],
+               formulas = formulas}
+          end
       end;
+
+  val resolutionParameters =
+      let
+        val {active,
+             waiting} = Resolution.default
+
+        val waiting =
+            let
+              val {symbolsWeight,
+                   variablesWeight,
+                   literalsWeight,
+                   models} = waiting
+
+              val models =
+                  case models of
+                    [{model = _,
+                      initialPerturbations,
+                      maxChecks,
+                      perturbations,
+                      weight}] =>
+                    let
+                      val model = Tptp.defaultModel
+                    in
+                      [{model = model,
+                        initialPerturbations = initialPerturbations,
+                        maxChecks = maxChecks,
+                        perturbations = perturbations,
+                        weight = weight}]
+                    end
+                  | _ => raise Bug "resolutionParameters.waiting.models"
+            in
+              {symbolsWeight = symbolsWeight,
+               variablesWeight = variablesWeight,
+               literalsWeight = literalsWeight,
+               models = models}
+            end
+      in
+        {active = active,
+         waiting = waiting}
+      end;
+
+  fun refute {axioms,conjecture} =
+      let
+        val axioms = map Thm.axiom axioms
+        and conjecture = map Thm.axiom conjecture
+        val problem = {axioms = axioms, conjecture = conjecture}
+        val resolution = Resolution.new resolutionParameters problem
+      in
+        Resolution.loop resolution
+      end;
+
+  fun refuteAll filename tptp probs acc =
+      case probs of
+        [] =>
+        let
+          val status =
+              if !TEST then Tptp.UnknownStatus
+              else if Tptp.hasFofConjecture tptp then Tptp.TheoremStatus
+              else Tptp.UnsatisfiableStatus
+
+          val () = display_status filename status
+
+          val () =
+              if !TEST then ()
+              else display_proof filename tptp (rev acc)
+        in
+          true
+        end
+      | prob :: probs =>
+        let
+          val {subgoal,problem,sources} = prob
+
+          val () = display_problem filename problem
+        in
+          if !TEST then refuteAll filename tptp probs acc
+          else
+            case refute problem of
+              Resolution.Contradiction th =>
+              let
+                val subgoalProof =
+                    {subgoal = subgoal,
+                     sources = sources,
+                     refutation = th}
+
+                val acc = subgoalProof :: acc
+              in
+                refuteAll filename tptp probs acc
+              end
+            | Resolution.Satisfiable ths =>
+              let
+                val status =
+                    if Tptp.hasFofConjecture tptp then
+                      Tptp.CounterSatisfiableStatus
+                    else
+                      Tptp.SatisfiableStatus
+
+                val () = display_status filename status
+                val () = display_saturation filename ths
+              in
+                false
+              end
+        end;
 in
-  fun prove filename =
+  fun prove mapping filename =
       let
         val () = display_sep ()
         val () = display_name filename
-        val tptp = Tptp.read {filename = filename}
+        val tptp = read mapping filename
+        val () = display_goal tptp
+        val problems = Tptp.normalize tptp
       in
-        case Tptp.toGoal tptp of
-          Tptp.Cnf prob =>
-          let
-            val () = display_problem filename prob
-          in
-            if !TEST then
-              (display_status filename "Unknown";
-               true)
-            else
-              case refute prob of
-                Resolution.Contradiction th =>
-                (display_status filename "Unsatisfiable";
-                 if showing "proof" then print "\n" else ();
-                 display_proof filename th;
-                 true)
-              | Resolution.Satisfiable ths =>
-                (display_status filename "Satisfiable";
-                 if showing "saturated" then print "\n" else ();
-                 display_saturated filename ths;
-                 false)
-          end
-        | Tptp.Fof goal =>
-          let
-            val () = display_goal goal
-            val problems = Problem.fromGoal goal
-            val result =
-                if !TEST then (display_problems filename problems; true)
-                else List.all (refutable filename) problems
-            val status =
-                if !TEST then "Unknown"
-                else if Tptp.hasConjecture tptp then
-                  if result then "Theorem" else "CounterSatisfiable"
-                else
-                  if result then "Unsatisfiable" else "Satisfiable"
-            val () = display_status filename status
-          in
-            result
-          end
+        refuteAll filename tptp problems []
       end;
+
+  fun proveAll mapping filenames =
+      List.all
+        (if !QUIET then prove mapping
+         else fn filename => prove mapping filename orelse true)
+        filenames;
 end;
 
 (* ------------------------------------------------------------------------- *)
 (* Top level.                                                                *)
 (* ------------------------------------------------------------------------- *)
 
 val () =
 let
-(*DEBUG
-  val () = print "Running in DEBUG mode.\n"
-*)
-  val success = List.all prove work
-  val return = not (!QUIET) orelse success
+  val work = processOptions ()
+
+  val () = if null work then usage "no input problem files" else ()
+
+  val mapping = Tptp.defaultMapping
+
+  val success = proveAll mapping work
 in
-  exit {message = NONE, usage = false, success = return}
+  exit {message = NONE, usage = false, success = success}
 end
 handle Error s => die (PROGRAM^" failed:\n" ^ s)
      | Bug s => die ("BUG found in "^PROGRAM^" program:\n" ^ s);