(* ========================================================================= *)
(* METIS FIRST ORDER PROVER *)
(* *)
(* 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. *)
(* *)
(* Metis is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU General Public License *)
(* along with Metis; if not, write to the Free Software *)
(* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *)
(* ========================================================================= *)
open Useful;
(* ------------------------------------------------------------------------- *)
(* 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 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 "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 extended_items endOpt) (fn _ => fn s => show s)},
{switches = ["--hide"], arguments = ["ITEM"],
description = "hide ITEM (see below for list)",
processor =
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 programOptions =
{name = PROGRAM,
version = versionString,
header = "usage: "^PROGRAM^" [option ...] problem.tptp ...\n" ^
"Proves the input TPTP problem files.\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;
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 #"-" (!Print.lineLength) ^ "\n");
fun display_name filename =
if notshowing "name" then ()
else print ("Problem: " ^ filename ^ "\n\n");
fun display_goal tptp =
if notshowing "goal" then ()
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");
fun display_size cls =
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;
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
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 ("\nSZS output start Saturation for " ^ filename ^ "\n")
val () = app (fn th => print (Thm.toString th ^ "\n")) ths
val () = print ("SZS output end Saturation for " ^ filename ^ "\n\n")
in
()
end;
fun display_status filename status =
if notshowing "status" then ()
else print ("SZS status " ^ Tptp.toStringStatus status ^
" for " ^ filename ^ "\n");
fun display_problem filename cls =
let
(*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 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 problem = Tptp.read {filename = filename, mapping = mapping}
val Tptp.Problem {comments,includes,formulas} = problem
in
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 mapping filename =
let
val () = display_sep ()
val () = display_name filename
val tptp = read mapping filename
val () = display_goal tptp
val problems = Tptp.normalize tptp
in
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
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 = success}
end
handle Error s => die (PROGRAM^" failed:\n" ^ s)
| Bug s => die ("BUG found in "^PROGRAM^" program:\n" ^ s);