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