2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
12 (* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *)
14 val lexicograph : ('a -> 'b -> int) -> 'a list -> 'b list -> int
16 module Utils (B : Orderings.Blob) :
18 val eq_foterm : B.t Terms.foterm -> B.t Terms.foterm -> bool
19 val compare_foterm : B.t Terms.foterm -> B.t Terms.foterm -> int
21 val eq_literal : B.t Terms.literal -> B.t Terms.literal -> bool
22 val compare_literal : B.t Terms.literal -> B.t Terms.literal -> int
24 (* mk_clause [maxvar] [type] [proof] -> [clause] * [maxvar] *)
27 B.t Terms.foterm list -> (* negative literals in clause *)
28 B.t Terms.foterm list -> (* positive literals in clause *)
30 B.t Terms.clause * int
32 val mk_passive_clause :
33 B.t Terms.clause -> B.t Terms.passive_clause
36 B.t Terms.clause -> B.t Terms.passive_clause
38 val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool
39 val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int
43 int -> B.t Terms.clause -> B.t Terms.clause * int
45 (* relocate [maxvar] [varlist] -> [newmaxvar] * [varlist] * [relocsubst] *)
47 int -> int list -> B.t Terms.substitution ->
48 int * int list * B.t Terms.substitution
50 val compare_passive_clauses_weight :
51 B.t Terms.passive_clause -> B.t Terms.passive_clause -> int
53 val compare_passive_clauses_age :
54 B.t Terms.passive_clause -> B.t Terms.passive_clause -> int