src/Tools/Metis/src/Model.sig

Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.

(* ========================================================================= *)
(* RANDOM FINITE MODELS                                                      *)
(* Copyright (c) 2003-2007 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)

signature Model =
sig

(* ------------------------------------------------------------------------- *)
(* The parts of the model that are fixed.                                    *)
(* Note: a model of size N has integer elements 0...N-1.                     *)
(* ------------------------------------------------------------------------- *)

type fixed =
     {size : int} ->
     {functions : (Term.functionName * int list) -> int option,
      relations : (Atom.relationName * int list) -> bool option}

val fixedMerge : fixed -> fixed -> fixed  (* Prefers the second fixed *)

val fixedMergeList : fixed list -> fixed

val fixedPure : fixed  (* : = *)

val fixedBasic : fixed  (* id fst snd #1 #2 #3 <> *)

val fixedModulo : fixed  (* <numerals> suc pre ~ + - * exp div mod *)
                         (* is_0 divides even odd *)

val fixedOverflowNum : fixed  (* <numerals> suc pre + - * exp div mod *)
                              (* is_0 <= < >= > divides even odd *)

val fixedOverflowInt : fixed  (* <numerals> suc pre + - * exp div mod *)
                              (* is_0 <= < >= > divides even odd *)

val fixedSet : fixed  (* empty univ union intersect compl card in subset *)

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

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

type model

val new : parameters -> model

val size : model -> int

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

type valuation = int NameMap.map

val valuationEmpty : valuation

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

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

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

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

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 checkAtom :
    {maxChecks : int} -> model -> Atom.atom -> {T : int, F : int}

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

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

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

end