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_______________________________________________________________ *)
17 | Node of ('a foterm) list
19 type 'a substitution = (int * 'a foterm) list
21 type comparison = Lt | Eq | Gt | Incomparable | Invertible
23 type rule = Superposition | Demodulation
24 type direction = Left2Right | Right2Left | Nodir
25 type position = int list
29 | Step of rule * int * int * direction * position * 'a substitution
30 (* rule, eq1, eq2, direction of eq2, position, substitution *)
33 | Equation of 'a foterm (* lhs *)
35 * 'a foterm (* type *)
36 * comparison (* orientation *)
37 | Predicate of 'a foterm
39 type varlist = int list
44 * varlist (* variable list *)
45 * 'a proof (* proof *)
49 * ('a literal * bool) list (* left hand side of the arrow,
50 with flag for selection *)
51 * ('a literal * bool) list (* right hand side of the arrow,
52 with flag for selection *)
56 type 'a passive_clause = int * 'a clause (* weight * equation *)
59 let vars_of_term ?(start_acc=[]) t =
60 let rec aux acc = function
62 | Var i -> if (List.mem i acc) then acc else i::acc
63 | Node l -> List.fold_left aux acc l
70 let compare = Pervasives.compare
73 module M : Map.S with type key = int
77 * (('a clause * bool * int) M.t)
79 let add_to_bag (_,nlit,plit,vl,proof) (id,bag) =
81 let clause = (id, nlit, plit, vl, proof) in
82 let bag = M.add id (clause,false,0) bag in
86 let replace_in_bag ((id,_,_,_,_),_,_ as cl) (max_id,bag) =
87 let bag = M.add id cl bag in
91 let get_from_bag id (_,bag) =
95 let empty_bag = (0,M.empty);;
100 val eq : t -> t -> bool
101 val compare : t -> t -> int
105 val embed : input -> t foterm
106 val saturate : input -> input -> t foterm * t foterm