1(* ========================================================================= *) 2(* PROCESSING SETS OF CLAUSES AT A TIME *) 3(* Copyright (c) 2002-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6signature mlibClauseset = 7sig 8 9type 'a pp = 'a mlibUseful.pp 10type clause = mlibClause.clause 11 12type filter = {subsumption : bool, simplification : int, splitting : bool} 13type parameters = {prefactoring : filter, postfactoring : filter} 14 15val defaults : parameters 16val update_subsumption : (bool -> bool) -> filter -> filter 17val update_simplification : (int -> int) -> filter -> filter 18val update_splitting : (bool -> bool) -> filter -> filter 19val update_prefactoring : (filter -> filter) -> parameters -> parameters 20val update_postfactoring : (filter -> filter) -> parameters -> parameters 21 22(* mlibClause sets *) 23type clauseset 24val empty : mlibClause.parameters * parameters -> clauseset 25val parm : clauseset -> mlibClause.parameters * parameters 26val size : clauseset -> int 27val units : clauseset -> mlibUnits.units 28val rewrites : clauseset -> mlibClause.rewrs 29val clauses : clauseset -> clause list 30val new_units : mlibUnits.units -> clauseset -> clauseset 31 32(* Simplify and strengthen clauses *) 33val simplify : clauseset -> clause -> clause 34val strengthen : clauseset -> clause -> clause option 35 36(* Forward subsumption checking *) 37val subsumed : clauseset -> clause -> bool 38 39(* Add a clause into the set *) 40val add : clause -> clauseset -> clauseset 41 42(* Derive (unfactored) consequences of a clause *) 43val deduce : clauseset -> clause -> clause list 44 45(* Factor clauses *) 46val factor : clause list -> clauseset -> clause list * clauseset 47 48(* Pretty-printing *) 49val pp_clauseset : clauseset pp 50 51end 52