1(* ========================================================================= *)
2(* CLAUSE = ID + THEOREM + CONSTRAINTS                                       *)
3(* Copyright (c) 2002-2004 Joe Hurd.                                         *)
4(* ========================================================================= *)
5
6signature mlibClause =
7sig
8
9type ('a,'b) maplet = ('a,'b) mlibUseful.maplet
10type 'a pp          = 'a mlibUseful.pp
11type term           = mlibTerm.term
12type formula        = mlibTerm.formula
13type subst          = mlibSubst.subst
14type thm            = mlibThm.thm
15type termorder      = mlibTermorder.termorder
16
17type parameters =
18  {term_order       : bool,
19   literal_order    : bool,
20   order_stickiness : int,       (* Stickiness of ordering constraints: 0..3 *)
21   termorder_parm   : mlibTermorder.parameters}
22
23type 'a parmupdate = ('a -> 'a) -> parameters -> parameters
24val defaults                : parameters
25val update_term_order       : bool parmupdate
26val update_literal_order    : bool parmupdate
27val update_order_stickiness : int parmupdate
28val update_termorder_parm   : mlibTermorder.parameters parmupdate
29
30type clause
31
32(* Basic operations *)
33type bits = {parm : parameters, id : int, thm : thm, order : termorder}
34val mk_clause   : parameters -> thm -> clause
35val dest_clause : clause -> bits
36val literals    : clause -> formula list
37val is_empty    : clause -> bool
38val dest_rewr   : clause -> int * thm
39val is_rewr     : clause -> bool
40val rebrand     : parameters -> clause -> clause
41
42(* Using ordering constraints to cut down the set of possible inferences *)
43val largest_lits : clause -> (clause * int, formula) maplet list
44val largest_eqs  : clause -> (clause * int * bool, term) maplet list
45val largest_tms  : clause -> (clause * int * int list, term) maplet list
46val drop_order   : clause -> clause
47
48(* Subsumption *)
49val subsumes : clause -> clause -> bool
50
51(* mlibClause rewriting *)
52type rewrs
53val empty    : parameters -> rewrs
54val size     : rewrs -> int
55val peek     : rewrs -> int -> ((term * term) * mlibRewrite.orient) option
56val add      : clause -> rewrs -> rewrs
57val reduce   : rewrs -> rewrs * int list
58val reduced  : rewrs -> bool
59val pp_rewrs : rewrs pp
60
61(* Simplifying rules: these preserve the clause id *)
62val INST       : subst -> clause -> clause
63val FRESH_VARS : clause -> clause
64val NEQ_VARS   : clause -> clause
65val DEMODULATE : mlibUnits.units -> clause -> clause
66val QREWRITE   : rewrs -> clause -> clause
67val REWRITE    : rewrs -> clause -> clause
68
69(* Ordered resolution and paramodulation: these generate new clause ids *)
70val FACTOR       : clause -> clause list
71val RESOLVE      : clause * int -> clause * int -> clause
72val PARAMODULATE : clause * int * bool -> clause * int * int list -> clause
73
74(* mlibClause derivations *)
75datatype derivation =
76  Axiom
77| mlibResolution of clause * clause
78| Paramodulation of clause * clause
79| Factor of clause
80val derivation : clause -> derivation
81
82(* Pretty printing *)
83val show_id         : bool ref
84val show_constraint : bool ref
85val pp_clause       : clause pp
86
87end
88