--- a/src/Tools/Metis/src/Tptp.sig Mon Sep 13 16:44:20 2010 +0200
+++ b/src/Tools/Metis/src/Tptp.sig Mon Sep 13 21:24:10 2010 +0200
@@ -1,18 +1,73 @@
(* ========================================================================= *)
-(* THE TPTP PROBLEM FILE FORMAT (TPTP v2) *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* THE TPTP PROBLEM FILE FORMAT *)
+(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Tptp =
sig
(* ------------------------------------------------------------------------- *)
-(* Mapping TPTP functions and relations to different names. *)
+(* Mapping to and from TPTP variable, function and relation names. *)
+(* ------------------------------------------------------------------------- *)
+
+type mapping
+
+val defaultMapping : mapping
+
+val mkMapping :
+ {functionMapping : {name : Name.name, arity : int, tptp : string} list,
+ relationMapping : {name : Name.name, arity : int, tptp : string} list} ->
+ mapping
+
+val addVarSetMapping : mapping -> NameSet.set -> mapping
+
+(* ------------------------------------------------------------------------- *)
+(* Interpreting TPTP functions and relations in a finite model. *)
+(* ------------------------------------------------------------------------- *)
+
+val defaultFixedMap : Model.fixedMap
+
+val defaultModel : Model.parameters
+
+val ppFixedMap : mapping -> Model.fixedMap Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP roles. *)
(* ------------------------------------------------------------------------- *)
-val functionMapping : {name : string, arity : int, tptp : string} list ref
+datatype role =
+ AxiomRole
+ | ConjectureRole
+ | DefinitionRole
+ | NegatedConjectureRole
+ | PlainRole
+ | TheoremRole
+ | OtherRole of string;
+
+val isCnfConjectureRole : role -> bool
+
+val isFofConjectureRole : role -> bool
+
+val toStringRole : role -> string
+
+val fromStringRole : string -> role
-val relationMapping : {name : string, arity : int, tptp : string} list ref
+val ppRole : role Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* SZS statuses. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype status =
+ CounterSatisfiableStatus
+ | TheoremStatus
+ | SatisfiableStatus
+ | UnknownStatus
+ | UnsatisfiableStatus
+
+val toStringStatus : status -> string
+
+val ppStatus : status Print.pp
(* ------------------------------------------------------------------------- *)
(* TPTP literals. *)
@@ -22,66 +77,152 @@
Boolean of bool
| Literal of Literal.literal
-val negate : literal -> literal
+val negateLiteral : literal -> literal
+
+val functionsLiteral : literal -> NameAritySet.set
+
+val relationLiteral : literal -> Atom.relation option
+
+val freeVarsLiteral : literal -> NameSet.set
-val literalFunctions : literal -> NameAritySet.set
+(* ------------------------------------------------------------------------- *)
+(* TPTP formula names. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formulaName =
+ FormulaName of string
+
+val ppFormulaName : formulaName Print.pp
-val literalRelation : literal -> Atom.relation option
+(* ------------------------------------------------------------------------- *)
+(* TPTP formula bodies. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype formulaBody =
+ CnfFormulaBody of literal list
+ | FofFormulaBody of Formula.formula
+
+(* ------------------------------------------------------------------------- *)
+(* TPTP formula sources. *)
+(* ------------------------------------------------------------------------- *)
-val literalFreeVars : literal -> NameSet.set
+datatype formulaSource =
+ NoFormulaSource
+ | StripFormulaSource of
+ {inference : string,
+ parents : formulaName list}
+ | NormalizeFormulaSource of
+ {inference : Normalize.inference,
+ parents : formulaName list}
+ | ProofFormulaSource of
+ {inference : Proof.inference,
+ parents : formulaName list}
(* ------------------------------------------------------------------------- *)
(* TPTP formulas. *)
(* ------------------------------------------------------------------------- *)
datatype formula =
- CnfFormula of {name : string, role : string, clause : literal list}
- | FofFormula of {name : string, role : string, formula : Formula.formula}
+ Formula of
+ {name : formulaName,
+ role : role,
+ body : formulaBody,
+ source : formulaSource}
+
+val nameFormula : formula -> formulaName
+
+val roleFormula : formula -> role
-val formulaFunctions : formula -> NameAritySet.set
+val bodyFormula : formula -> formulaBody
+
+val sourceFormula : formula -> formulaSource
+
+val functionsFormula : formula -> NameAritySet.set
-val formulaRelations : formula -> NameAritySet.set
+val relationsFormula : formula -> NameAritySet.set
-val formulaFreeVars : formula -> NameSet.set
+val freeVarsFormula : formula -> NameSet.set
+
+val freeVarsListFormula : formula list -> NameSet.set
-val formulaIsConjecture : formula -> bool
+val isCnfConjectureFormula : formula -> bool
+val isFofConjectureFormula : formula -> bool
+val isConjectureFormula : formula -> bool
-val ppFormula : formula Parser.pp
+(* ------------------------------------------------------------------------- *)
+(* Clause information. *)
+(* ------------------------------------------------------------------------- *)
+
+datatype clauseSource =
+ CnfClauseSource of formulaName * literal list
+ | FofClauseSource of Normalize.thm
-val parseFormula : char Stream.stream -> formula Stream.stream
+type 'a clauseInfo = 'a LiteralSetMap.map
+
+type clauseNames = formulaName clauseInfo
+
+type clauseRoles = role clauseInfo
-val formulaToString : formula -> string
+type clauseSources = clauseSource clauseInfo
+
+val noClauseNames : clauseNames
-val formulaFromString : string -> formula
+val noClauseRoles : clauseRoles
+
+val noClauseSources : clauseSources
(* ------------------------------------------------------------------------- *)
(* TPTP problems. *)
(* ------------------------------------------------------------------------- *)
-datatype goal =
- Cnf of Problem.problem
- | Fof of Formula.formula
+type comments = string list
+
+type includes = string list
-type problem = {comments : string list, formulas : formula list}
+datatype problem =
+ Problem of
+ {comments : comments,
+ includes : includes,
+ formulas : formula list}
-val read : {filename : string} -> problem
-
-val write : {filename : string} -> problem -> unit
-
+val hasCnfConjecture : problem -> bool
+val hasFofConjecture : problem -> bool
val hasConjecture : problem -> bool
-val toGoal : problem -> goal
+val freeVars : problem -> NameSet.set
+
+val mkProblem :
+ {comments : comments,
+ includes : includes,
+ names : clauseNames,
+ roles : clauseRoles,
+ problem : Problem.problem} -> problem
-val fromProblem : Problem.problem -> problem
+val normalize :
+ problem ->
+ {subgoal : Formula.formula * formulaName list,
+ problem : Problem.problem,
+ sources : clauseSources} list
+
+val goal : problem -> Formula.formula
-val prove : {filename : string} -> bool
+val read : {mapping : mapping, filename : string} -> problem
+
+val write :
+ {problem : problem,
+ mapping : mapping,
+ filename : string} -> unit
+
+val prove : {filename : string, mapping : mapping} -> bool
(* ------------------------------------------------------------------------- *)
(* TSTP proofs. *)
(* ------------------------------------------------------------------------- *)
-val ppProof : Proof.proof Parser.pp
-
-val proofToString : Proof.proof -> string
+val fromProof :
+ {problem : problem,
+ proofs : {subgoal : Formula.formula * formulaName list,
+ sources : clauseSources,
+ refutation : Thm.thm} list} -> formula list
end