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