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