src/Tools/Metis/src/Model.sig

updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)

(* ========================================================================= *)
(* RANDOM FINITE MODELS                                                      *)
(* Copyright (c) 2003 Joe Hurd, distributed under the MIT license            *)
(* ========================================================================= *)

signature Model =
sig

(* ------------------------------------------------------------------------- *)
(* Model size.                                                               *)
(* ------------------------------------------------------------------------- *)

type size = {size : int}

(* ------------------------------------------------------------------------- *)
(* A model of size N has integer elements 0...N-1.                           *)
(* ------------------------------------------------------------------------- *)

type element = int

val zeroElement : element

val incrementElement : size -> element -> element option

(* ------------------------------------------------------------------------- *)
(* The parts of the model that are fixed.                                    *)
(* ------------------------------------------------------------------------- *)

type fixedFunction = size -> element list -> element option

type fixedRelation = size -> element list -> bool option

datatype fixed =
    Fixed of
      {functions : fixedFunction NameArityMap.map,
       relations : fixedRelation NameArityMap.map}

val emptyFixed : fixed

val unionFixed : fixed -> fixed -> fixed

val getFunctionFixed : fixed -> NameArity.nameArity -> fixedFunction

val getRelationFixed : fixed -> NameArity.nameArity -> fixedRelation

val insertFunctionFixed : fixed -> NameArity.nameArity * fixedFunction -> fixed

val insertRelationFixed : fixed -> NameArity.nameArity * fixedRelation -> fixed

val unionListFixed : fixed list -> fixed

val basicFixed : fixed  (* interprets equality and hasType *)

(* ------------------------------------------------------------------------- *)
(* Renaming fixed model parts.                                               *)
(* ------------------------------------------------------------------------- *)

type fixedMap =
     {functionMap : Name.name NameArityMap.map,
      relationMap : Name.name NameArityMap.map}

val mapFixed : fixedMap -> fixed -> fixed

val ppFixedMap : fixedMap Print.pp

(* ------------------------------------------------------------------------- *)
(* Standard fixed model parts.                                               *)
(* ------------------------------------------------------------------------- *)

(* Projections *)

val projectionMin : int

val projectionMax : int

val projectionName : int -> Name.name

val projectionFixed : fixed

(* Arithmetic *)

val numeralMin : int

val numeralMax : int

val numeralName : int -> Name.name

val addName : Name.name

val divName : Name.name

val dividesName : Name.name

val evenName : Name.name

val expName : Name.name

val geName : Name.name

val gtName : Name.name

val isZeroName : Name.name

val leName : Name.name

val ltName : Name.name

val modName : Name.name

val multName : Name.name

val negName : Name.name

val oddName : Name.name

val preName : Name.name

val subName : Name.name

val sucName : Name.name

val modularFixed : fixed

val overflowFixed : fixed

(* Sets *)

val cardName : Name.name

val complementName : Name.name

val differenceName : Name.name

val emptyName : Name.name

val memberName : Name.name

val insertName : Name.name

val intersectName : Name.name

val singletonName : Name.name

val subsetName : Name.name

val symmetricDifferenceName : Name.name

val unionName : Name.name

val universeName : Name.name

val setFixed : fixed

(* Lists *)

val appendName : Name.name

val consName : Name.name

val lengthName : Name.name

val nilName : Name.name

val nullName : Name.name

val tailName : Name.name

val listFixed : fixed

(* ------------------------------------------------------------------------- *)
(* Valuations.                                                               *)
(* ------------------------------------------------------------------------- *)

type valuation

val emptyValuation : valuation

val zeroValuation : NameSet.set -> valuation

val constantValuation : element -> NameSet.set -> valuation

val peekValuation : valuation -> Name.name -> element option

val getValuation : valuation -> Name.name -> element

val insertValuation : valuation -> Name.name * element -> valuation

val randomValuation : {size : int} -> NameSet.set -> valuation

val incrementValuation :
    {size : int} -> NameSet.set -> valuation -> valuation option

val foldValuation :
    {size : int} -> NameSet.set -> (valuation * 'a -> 'a) -> 'a -> 'a

(* ------------------------------------------------------------------------- *)
(* A type of random finite models.                                           *)
(* ------------------------------------------------------------------------- *)

type parameters = {size : int, fixed : fixed}

type model

val default : parameters

val new : parameters -> model

val size : model -> int

(* ------------------------------------------------------------------------- *)
(* Interpreting terms and formulas in the model.                             *)
(* ------------------------------------------------------------------------- *)

val interpretFunction : model -> Term.functionName * element list -> element

val interpretRelation : model -> Atom.relationName * element list -> bool

val interpretTerm : model -> valuation -> Term.term -> element

val interpretAtom : model -> valuation -> Atom.atom -> bool

val interpretFormula : model -> valuation -> Formula.formula -> bool

val interpretLiteral : model -> valuation -> Literal.literal -> bool

val interpretClause : model -> valuation -> Thm.clause -> bool

(* ------------------------------------------------------------------------- *)
(* Check whether random groundings of a formula are true in the model.       *)
(* Note: if it's cheaper, a systematic check will be performed instead.      *)
(* ------------------------------------------------------------------------- *)

val check :
    (model -> valuation -> 'a -> bool) -> {maxChecks : int option} -> model ->
    NameSet.set -> 'a -> {T : int, F : int}

val checkAtom :
    {maxChecks : int option} -> model -> Atom.atom -> {T : int, F : int}

val checkFormula :
    {maxChecks : int option} -> model -> Formula.formula -> {T : int, F : int}

val checkLiteral :
    {maxChecks : int option} -> model -> Literal.literal -> {T : int, F : int}

val checkClause :
    {maxChecks : int option} -> model -> Thm.clause -> {T : int, F : int}

(* ------------------------------------------------------------------------- *)
(* Updating the model.                                                       *)
(* ------------------------------------------------------------------------- *)

val updateFunction :
    model -> (Term.functionName * element list) * element -> unit

val updateRelation :
    model -> (Atom.relationName * element list) * bool -> unit

(* ------------------------------------------------------------------------- *)
(* Choosing a random perturbation to make a formula true in the model.       *)
(* ------------------------------------------------------------------------- *)

val perturbTerm : model -> valuation -> Term.term * element list -> unit

val perturbAtom : model -> valuation -> Atom.atom * bool -> unit

val perturbLiteral : model -> valuation -> Literal.literal -> unit

val perturbClause : model -> valuation -> Thm.clause -> unit

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

val pp : model Print.pp

end