1(* ========================================================================= *) 2(* FINITE MODELS *) 3(* Copyright (c) 2003-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6signature mlibModel = 7sig 8 9type 'a pp = 'a mlibUseful.pp 10type term = mlibTerm.term 11type formula = mlibTerm.formula 12 13(* The parts of the model that are fixed and cannot be perturbed *) 14(* Note: a model of size N has integer elements 0...N-1 *) 15type fix = int -> {func : (string * int list) -> int option, 16 pred : (string * int list) -> bool option} 17val fix_merge : fix -> fix -> fix 18val fix_mergel : fix list -> fix 19val map_fix : (string -> string option) -> fix -> fix 20val pure_fix : fix (* = *) 21val basic_fix : fix (* id fst snd #1 #2 #3 <> *) 22val modulo_fix : fix (* 0 1 2 suc pre ~ + - * exp mod *) 23 (* < <= > >= is_0 divides odd even *) 24val heap_fix : fix (* 0 1 2 suc pre + - * exp < <= > >= is_0 *) 25val set_fix : fix (* empty univ union inter compl card in subset *) 26 27(* Parameters *) 28type parameters = {size : int, fix : fix} 29val defaults : parameters 30val update_size : (int -> int) -> parameters -> parameters 31val update_fix : (fix -> fix) -> parameters -> parameters 32 33(* The type of finite models *) 34type model 35 36(* Basic operations *) 37val new : parameters -> model 38val size : model -> int 39 40(* Evaluate ground terms and sentences *) 41val evaluate_term : model -> term -> int 42val evaluate_formula : model -> formula -> bool 43 44(* Check whether a random grounding of a formula is satisfied by the model *) 45val check : model -> formula -> bool 46val checkn : model -> formula -> int -> int 47val count : model -> formula -> int * int (* num of satisfying groundings *) 48 49(* Try to make formulas true by applying random perturbations to the model *) 50val perturb : formula list -> int -> model -> model 51 52(* Pretty-printing *) 53val pp_model : model pp 54val term_to_string : model -> term -> string 55val formula_to_string : model -> formula -> string 56 57end 58