src/Tools/Metis/src/Clause.sig

echo prover input via raw_messages, for improved protocol tracing;

(* ========================================================================= *)
(* CLAUSE = ID + THEOREM                                                     *)
(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
(* ========================================================================= *)

signature Clause =
sig

(* ------------------------------------------------------------------------- *)
(* A type of clause.                                                         *)
(* ------------------------------------------------------------------------- *)

datatype literalOrder =
    NoLiteralOrder
  | UnsignedLiteralOrder
  | PositiveLiteralOrder

type parameters =
     {ordering : KnuthBendixOrder.kbo,
      orderLiterals : literalOrder,
      orderTerms : bool}

type clauseId = int

type clauseInfo = {parameters : parameters, id : clauseId, thm : Thm.thm}

type clause

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

val default : parameters

val newId : unit -> clauseId

val mk : clauseInfo -> clause

val dest : clause -> clauseInfo

val id : clause -> clauseId

val thm : clause -> Thm.thm

val equalThms : clause -> clause -> bool

val literals : clause -> Thm.clause

val isTautology : clause -> bool

val isContradiction : clause -> bool

(* ------------------------------------------------------------------------- *)
(* The term ordering is used to cut down inferences.                         *)
(* ------------------------------------------------------------------------- *)

val largestLiterals : clause -> LiteralSet.set

val largestEquations :
    clause -> (Literal.literal * Rewrite.orient * Term.term) list

val largestSubterms :
    clause -> (Literal.literal * Term.path * Term.term) list

val allSubterms : clause -> (Literal.literal * Term.path * Term.term) list

(* ------------------------------------------------------------------------- *)
(* Subsumption.                                                              *)
(* ------------------------------------------------------------------------- *)

val subsumes : clause Subsume.subsume -> clause -> bool

(* ------------------------------------------------------------------------- *)
(* Simplifying rules: these preserve the clause id.                          *)
(* ------------------------------------------------------------------------- *)

val freshVars : clause -> clause

val simplify : clause -> clause option

val reduce : Units.units -> clause -> clause

val rewrite : Rewrite.rewrite -> clause -> clause

(* ------------------------------------------------------------------------- *)
(* Inference rules: these generate new clause ids.                           *)
(* ------------------------------------------------------------------------- *)

val factor : clause -> clause list

val resolve : clause * Literal.literal -> clause * Literal.literal -> clause

val paramodulate :
    clause * Literal.literal * Rewrite.orient * Term.term ->
    clause * Literal.literal * Term.path * Term.term -> clause

(* ------------------------------------------------------------------------- *)
(* Pretty printing.                                                          *)
(* ------------------------------------------------------------------------- *)

val showId : bool ref

val pp : clause Print.pp

val toString : clause -> string

end