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 $ *)
16 include Orderings.Blob
20 module Clauses (B : Orderings.Blob) :
23 val eq_clause : B.t Terms.clause -> B.t Terms.clause -> bool
24 val compare_clause : B.t Terms.clause -> B.t Terms.clause -> int
25 val fresh_clause : int -> B.t Terms.clause -> B.t Terms.clause * int
27 val mk_clause : int -> B.t Terms.foterm list -> B.t Terms.foterm list
28 -> B.t Terms.foterm -> B.t Terms.clause * int
30 val mk_passive_clause : B.t Terms.clause -> int * B.t Terms.clause
32 val mk_passive_goal : B.t Terms.clause -> int * B.t Terms.clause
34 val compare_passive_clauses_weight :
35 int * B.t Terms.clause -> int * B.t Terms.clause -> int
37 val compare_passive_clauses_age :
38 int * B.t Terms.clause -> int * B.t Terms.clause -> int