1(* ========================================================================= *)
2(* THE SET OF SUPPORT                                                        *)
3(* Copyright (c) 2002-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6signature mlibSupport =
7sig
8
9type 'a pp   = 'a mlibUseful.pp
10type formula = mlibTerm.formula
11type clause  = mlibClause.clause
12
13type parameters =
14  {size_power    : real,
15   literal_power : real,
16   model_power   : real,
17   model_perts   : int,
18   model_checks  : int,
19   model_parms   : mlibModel.parameters list}
20
21type 'a parmupdate = ('a -> 'a) -> parameters -> parameters
22val defaults             : parameters
23val update_size_power    : real parmupdate
24val update_literal_power : real parmupdate
25val update_model_power   : real parmupdate
26val update_model_perts   : int parmupdate
27val update_model_checks  : int parmupdate
28val update_model_parms   : mlibModel.parameters list parmupdate
29
30(* The set of support type *)
31type sos
32type distance
33
34(* Basic operations *)
35val new     : parameters -> formula list -> clause list -> sos
36val size    : sos -> int
37val to_list : sos -> clause list
38val pp_sos  : sos pp
39
40(* Adding new clauses *)
41val add : distance * clause list -> sos -> sos
42
43(* Removing the lightest clause *)
44val remove : sos -> ((distance * clause) * sos) option
45
46end
47