From ddd751449e73a22af523ce78ce1d8f0bb211e941 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 1 Jun 2009 11:57:04 +0000 Subject: [PATCH] we rewrite the paramodulation code! --- .../METAS/meta.helm-ng_paramodulation.src | 5 + .../components/ng_paramodulation/.depend | 12 + .../components/ng_paramodulation/Makefile | 11 + .../components/ng_paramodulation/founif.ml | 14 + .../components/ng_paramodulation/founif.mli | 30 ++ .../components/ng_paramodulation/index.ml | 78 +++++ .../components/ng_paramodulation/index.mli | 31 ++ .../components/ng_paramodulation/orderings.ml | 276 ++++++++++++++++++ .../ng_paramodulation/orderings.mli | 13 + .../components/ng_paramodulation/pp.ml | 19 ++ .../components/ng_paramodulation/pp.mli | 19 ++ .../components/ng_paramodulation/terms.ml | 59 ++++ .../components/ng_paramodulation/terms.mli | 52 ++++ 13 files changed, 619 insertions(+) create mode 100644 helm/software/components/METAS/meta.helm-ng_paramodulation.src create mode 100644 helm/software/components/ng_paramodulation/.depend create mode 100644 helm/software/components/ng_paramodulation/Makefile create mode 100644 helm/software/components/ng_paramodulation/founif.ml create mode 100644 helm/software/components/ng_paramodulation/founif.mli create mode 100644 helm/software/components/ng_paramodulation/index.ml create mode 100644 helm/software/components/ng_paramodulation/index.mli create mode 100644 helm/software/components/ng_paramodulation/orderings.ml create mode 100644 helm/software/components/ng_paramodulation/orderings.mli create mode 100644 helm/software/components/ng_paramodulation/pp.ml create mode 100644 helm/software/components/ng_paramodulation/pp.mli create mode 100644 helm/software/components/ng_paramodulation/terms.ml create mode 100644 helm/software/components/ng_paramodulation/terms.mli diff --git a/helm/software/components/METAS/meta.helm-ng_paramodulation.src b/helm/software/components/METAS/meta.helm-ng_paramodulation.src new file mode 100644 index 000000000..5c7e62b30 --- /dev/null +++ b/helm/software/components/METAS/meta.helm-ng_paramodulation.src @@ -0,0 +1,5 @@ +requires="helm-cic helm-ng_kernel" +version="0.0.1" +archive(byte)="ng_paramodulation.cma" +archive(native)="ng_paramodulation.cmxa" +linkopts="" diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend new file mode 100644 index 000000000..db250f996 --- /dev/null +++ b/helm/software/components/ng_paramodulation/.depend @@ -0,0 +1,12 @@ +terms.cmi: +pp.cmi: terms.cmi +founif.cmi: terms.cmi +index.cmi: terms.cmi +terms.cmo: terms.cmi +terms.cmx: terms.cmi +pp.cmo: pp.cmi +pp.cmx: pp.cmi +founif.cmo: founif.cmi +founif.cmx: founif.cmi +index.cmo: terms.cmi index.cmi +index.cmx: terms.cmx index.cmi diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile new file mode 100644 index 000000000..8612f4bfc --- /dev/null +++ b/helm/software/components/ng_paramodulation/Makefile @@ -0,0 +1,11 @@ +PACKAGE = ng_paramodulation + +INTERFACE_FILES = \ + terms.mli pp.mli founif.mli index.mli orderings.mli + +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + +all: + +include ../../Makefile.defs +include ../Makefile.common diff --git a/helm/software/components/ng_paramodulation/founif.ml b/helm/software/components/ng_paramodulation/founif.ml new file mode 100644 index 000000000..125bded70 --- /dev/null +++ b/helm/software/components/ng_paramodulation/founif.ml @@ -0,0 +1,14 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +let unification = assert false diff --git a/helm/software/components/ng_paramodulation/founif.mli b/helm/software/components/ng_paramodulation/founif.mli new file mode 100644 index 000000000..d959fc309 --- /dev/null +++ b/helm/software/components/ng_paramodulation/founif.mli @@ -0,0 +1,30 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +val unification: + Terms.varlist -> (* global varlist for both terms t1 and t2 *) + Terms.varlist -> (* locked variables: if equal to FV(t2) we match t1 with t2*) + 'a Terms.foterm -> + 'a Terms.foterm -> + 'a Terms.substitution * Terms.varlist + +(* +val unification: + Terms.varlist -> 'a Terms.foterm -> 'a Terms.foterm -> + 'a Terms.substitution * Terms.varlist + +val matching: + Terms.varlist -> Terms.varlist -> 'a Terms.foterm -> 'a Terms.foterm -> + 'a Terms.substitution * Terms.varlist + +*) diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml new file mode 100644 index 000000000..123c51650 --- /dev/null +++ b/helm/software/components/ng_paramodulation/index.ml @@ -0,0 +1,78 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) + +module type Comparable = + sig + type t + val is_eq : t -> t -> bool + end + +module C : Comparable = + struct + type t = NCic.term + let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *) + end + + (* +module C : Comparable = + struct + type t = Cic.term + let is_eq a b = Pervasives.compare a b = 0 (* TODO: optimize *) + end +*) + +open Discrimination_tree + +module ClauseOT : Set.OrderedType + with type t = Terms.direction * C.t Terms.unit_clause = + struct + type t = Terms.direction * C.t Terms.unit_clause + let compare (d1,(id1,_,_,_)) (d2,(id2,_,_,_)) = + Pervasives.compare (d1,id1) (d2,id2) + end + +module ClauseSet = Set.Make(ClauseOT) + +module FotermIndexable : Indexable +with type input = C.t Terms.foterm and + type constant_name = C.t = struct + +type input = C.t Terms.foterm +type constant_name = C.t + +let path_string_of = + let rec aux arity = function + | Terms.Leaf a -> [Constant (a, arity)] + | Terms.Var i -> assert (arity = 0); [Variable] + | Terms.Node (Terms.Var _::_) -> assert false + | Terms.Node ([] | [ _ ] ) -> assert false + | Terms.Node (Terms.Node _::_) -> assert false + | Terms.Node (hd::tl) -> + aux (List.length tl) hd @ List.flatten (List.map (aux 0) tl) + in + aux 0 +;; + +let compare e1 e2 = + match e1,e2 with + | Constant (a1,ar1), Constant (a2,ar2) -> + if C.is_eq a1 a2 then Pervasives.compare ar1 ar2 + else Pervasives.compare e1 e2 (* TODO: OPTIMIZE *) + | _ -> Pervasives.compare e1 e2 +;; + +let string_of_path l = String.concat "." (List.map (fun _ -> "*") l) ;; + +end + +module DiscriminationTree = Make(FotermIndexable)(ClauseSet) diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli new file mode 100644 index 000000000..fdecba91f --- /dev/null +++ b/helm/software/components/ng_paramodulation/index.mli @@ -0,0 +1,31 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) + +module type Comparable = + sig + type t + val is_eq : t -> t -> bool + end + +module C : Comparable + +module FotermIndexable : Discrimination_tree.Indexable +with type constant_name = C.t and + type input = C.t Terms.foterm + +module ClauseSet : Set.S with type elt = Terms.direction * C.t Terms.unit_clause + +module DiscriminationTree : Discrimination_tree.DiscriminationTree +with type constant_name = C.t +and type input = C.t Terms.foterm +and type data = ClauseSet.elt and type dataset = ClauseSet.t diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml new file mode 100644 index 000000000..f15454c62 --- /dev/null +++ b/helm/software/components/ng_paramodulation/orderings.ml @@ -0,0 +1,276 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) + +(* (weight of constants, [(meta, weight_of_meta)]) *) +type weight = int * (int * int) list;; + +let string_of_weight (cw, mw) = + let s = + String.concat ", " + (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw) + in + Printf.sprintf "[%d; %s]" cw s +;; + +let weight_of_term term = + let vars_dict = Hashtbl.create 5 in + let rec aux = function + | Terms.Var i -> + (try + let oldw = Hashtbl.find vars_dict i in + Hashtbl.replace vars_dict i (oldw+1) + with Not_found -> + Hashtbl.add vars_dict i 1); + 0 + | Terms.Leaf _ -> 1 + | Terms.Node l -> List.fold_left (+) 0 (List.map aux l) + in + let w = aux term in + let l = + Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict [] + in + let compare w1 w2 = + match w1, w2 with + | (m1, _), (m2, _) -> m2 - m1 + in + (w, List.sort compare l) (* from the biggest meta to the smallest (0) *) +;; + +let compute_clause_weight = assert false (* + let factor = 2 in + match o with + | Lt -> + let w, m = (weight_of_term + ~consider_metas:true ~count_metas_occurrences:false right) in + w + (factor * (List.length m)) ; + | Le -> assert false + | Gt -> + let w, m = (weight_of_term + ~consider_metas:true ~count_metas_occurrences:false left) in + w + (factor * (List.length m)) ; + | Ge -> assert false + | Eq + | Incomparable -> + let w1, m1 = (weight_of_term + ~consider_metas:true ~count_metas_occurrences:false right) in + let w2, m2 = (weight_of_term + ~consider_metas:true ~count_metas_occurrences:false left) in + w1 + w2 + (factor * (List.length m1)) + (factor * (List.length m2)) +*) +;; + +(* returns a "normalized" version of the polynomial weight wl (with type + * weight list), i.e. a list sorted ascending by meta number, + * from 0 to maxmeta. wl must be sorted descending by meta number. Example: + * normalize_weight 5 (3, [(3, 2); (1, 1)]) -> + * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *) +let normalize_weight maxmeta (cw, wl) = + let rec aux = function + | 0 -> [] + | m -> (m, 0)::(aux (m-1)) + in + let tmpl = aux maxmeta in + let wl = + List.sort + (fun (m, _) (n, _) -> Pervasives.compare m n) + (List.fold_left + (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl) + in + (cw, wl) +;; + + +let normalize_weights (cw1, wl1) (cw2, wl2) = + let rec aux wl1 wl2 = + match wl1, wl2 with + | [], [] -> [], [] + | (m, w)::tl1, (n, w')::tl2 when m = n -> + let res1, res2 = aux tl1 tl2 in + (m, w)::res1, (n, w')::res2 + | (m, w)::tl1, ((n, w')::_ as wl2) when m < n -> + let res1, res2 = aux tl1 wl2 in + (m, w)::res1, (m, 0)::res2 + | ((m, w)::_ as wl1), (n, w')::tl2 when m > n -> + let res1, res2 = aux wl1 tl2 in + (n, 0)::res1, (n, w')::res2 + | [], (n, w)::tl2 -> + let res1, res2 = aux [] tl2 in + (n, 0)::res1, (n, w)::res2 + | (m, w)::tl1, [] -> + let res1, res2 = aux tl1 [] in + (m, w)::res1, (m, 0)::res2 + | _, _ -> assert false + in + let cmp (m, _) (n, _) = compare m n in + let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in + (cw1, wl1), (cw2, wl2) +;; + +(* Riazanov: 3.1.5 pag 38 *) +let compare_weights ((h1, w1) as weight1) ((h2, w2) as weight2)= + let res, diffs = + try + List.fold_left2 + (fun ((lt, eq, gt), diffs) w1 w2 -> + match w1, w2 with + | (meta1, w1), (meta2, w2) when meta1 = meta2 -> + let diffs = (w1 - w2) + diffs in + let r = compare w1 w2 in + if r < 0 then (lt+1, eq, gt), diffs + else if r = 0 then (lt, eq+1, gt), diffs + else (lt, eq, gt+1), diffs + | _ -> assert false) + ((0, 0, 0), 0) w1 w2 + with Invalid_argument _ -> assert false + in + let hdiff = h1 - h2 in + match res with + | (0, _, 0) -> + if hdiff < 0 then Lt + else if hdiff > 0 then Gt + else Eq + | (m, _, 0) -> + if hdiff <= 0 then Lt + else if (- diffs) >= hdiff then Le else Incomparable + | (0, _, m) -> + if hdiff >= 0 then Gt + else if diffs >= (- hdiff) then Ge else Incomparable + | (m, _, n) when m > 0 && n > 0 -> + Incomparable + | _ -> assert false +;; + + +let rec aux_ordering ?(recursion=true) t1 t2 = + let module C = Cic in + let compare_uris u1 u2 = + let res = + compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) in + if res < 0 then Lt + else if res = 0 then Eq + else Gt + in + match t1, t2 with + | C.Meta _, _ + | _, C.Meta _ -> Incomparable + + | t1, t2 when t1 = t2 -> Eq + + | C.Rel n, C.Rel m -> if n > m then Lt else Gt + | C.Rel _, _ -> Lt + | _, C.Rel _ -> Gt + + | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2 + | C.Const _, _ -> Lt + | _, C.Const _ -> Gt + + | C.MutInd (u1, tno1, _), C.MutInd (u2, tno2, _) -> + let res = compare_uris u1 u2 in + if res <> Eq then res + else + let res = compare tno1 tno2 in + if res = 0 then Eq else if res < 0 then Lt else Gt + | C.MutInd _, _ -> Lt + | _, C.MutInd _ -> Gt + + | C.MutConstruct (u1, tno1, cno1, _), C.MutConstruct (u2, tno2, cno2, _) -> + let res = compare_uris u1 u2 in + if res <> Eq then res + else + let res = compare (tno1,cno1) (tno2,cno2) in + if res = 0 then Eq else if res < 0 then Lt else Gt + | C.MutConstruct _, _ -> Lt + | _, C.MutConstruct _ -> Gt + + | C.Appl l1, C.Appl l2 when recursion -> + let rec cmp t1 t2 = + match t1, t2 with + | [], [] -> Eq + | _, [] -> Gt + | [], _ -> Lt + | hd1::tl1, hd2::tl2 -> + let o = aux_ordering hd1 hd2 in + if o = Eq then cmp tl1 tl2 + else o + in + cmp l1 l2 + | C.Appl (h1::t1), C.Appl (h2::t2) when not recursion -> + aux_ordering h1 h2 + + | t1, t2 -> + debug_print + (lazy + (Printf.sprintf "These two terms are not comparable:\n%s\n%s\n\n" + (CicPp.ppterm t1) (CicPp.ppterm t2))); + Incomparable +;; + +let nonrec_kbo t1 t2 = + let w1 = weight_of_term t1 in + let w2 = weight_of_term t2 in + match compare_weights ~normalize:true w1 w2 with + | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable + | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable + | Eq -> aux_ordering t1 t2 + | res -> res +;; + +let rec kbo t1 t2 = + let aux = aux_ordering ~recursion:false in + let w1 = weight_of_term t1 + and w2 = weight_of_term t2 in + let rec cmp t1 t2 = + match t1, t2 with + | [], [] -> Eq + | _, [] -> Gt + | [], _ -> Lt + | hd1::tl1, hd2::tl2 -> + let o = + kbo hd1 hd2 + in + if o = Eq then cmp tl1 tl2 + else o + in + let comparison = compare_weights ~normalize:true w1 w2 in + match comparison with + | Le -> + let r = aux t1 t2 in + if r = Lt then Lt + else if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + if cmp tl1 tl2 = Lt then Lt else Incomparable + | _, _ -> Incomparable + ) else Incomparable + | Ge -> + let r = aux t1 t2 in + if r = Gt then Gt + else if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + if cmp tl1 tl2 = Gt then Gt else Incomparable + | _, _ -> Incomparable + ) else Incomparable + | Eq -> + let r = aux t1 t2 in + if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + cmp tl1 tl2 + | _, _ -> Incomparable + ) else r + | res -> res +;; + +let compare_terms = nonrec_kbo;; + diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli new file mode 100644 index 000000000..9d0f47d22 --- /dev/null +++ b/helm/software/components/ng_paramodulation/orderings.mli @@ -0,0 +1,13 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml new file mode 100644 index 000000000..aff9224e0 --- /dev/null +++ b/helm/software/components/ng_paramodulation/pp.ml @@ -0,0 +1,19 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +let pp_foterm = assert false +let pp_proof = assert false +let pp_substitution = assert false +let pp_unit_clause = assert false + + diff --git a/helm/software/components/ng_paramodulation/pp.mli b/helm/software/components/ng_paramodulation/pp.mli new file mode 100644 index 000000000..46c588676 --- /dev/null +++ b/helm/software/components/ng_paramodulation/pp.mli @@ -0,0 +1,19 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) + +val pp_foterm: ('a -> string) -> 'a Terms.foterm -> string +val pp_proof: ('a -> string) -> 'a Terms.bag -> 'a Terms.proof -> string +val pp_substitution: ('a -> string) -> 'a Terms.substitution -> string +val pp_unit_clause: ('a -> string) -> 'a Terms.unit_clause -> string + + diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml new file mode 100644 index 000000000..91ca56271 --- /dev/null +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -0,0 +1,59 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) + +type 'a foterm = + | Leaf of 'a + | Var of int + | Node of ('a foterm) list + +type 'a substitution = (int * 'a foterm) list + +type comparison = Lt | Le | Eq | Ge | Gt | Incomparable + +type rule = SuperpositionRight | SuperpositionLeft | Demodulation +type direction = Left2Right | Right2Left | Nodir +type position = int list + +type 'a proof = + | Exact of 'a + | Step of rule * int * int * direction * position * 'a substitution + (* rule, eq1, eq2, direction of eq2, position, substitution *) + +type 'a literal = + | Equation of 'a foterm (* lhs *) + * 'a foterm (* rhs *) + * 'a foterm (* type *) + * comparison (* orientation *) + | Predicate of 'a foterm + +type varlist = int list + +type 'a unit_clause = + int (* ID *) + * 'a literal + * varlist (* variable list *) + * 'a proof (* proof *) + +type 'a passive_clause = int * 'a unit_clause (* weight * equation *) + + +module OT = + struct + type t = int + let compare = Pervasives.compare + end + +module M : Map.S with type key = int + = Map.Make(OT) + +type 'a bag = 'a unit_clause M.t diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli new file mode 100644 index 000000000..c49eaff83 --- /dev/null +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -0,0 +1,52 @@ +(* + ||M|| This file is part of HELM, an Hypertextual, Electronic + ||A|| Library of Mathematics, developed at the Computer Science + ||T|| Department, University of Bologna, Italy. + ||I|| + ||T|| HELM is free software; you can redistribute it and/or + ||A|| modify it under the terms of the GNU General Public License + \ / version 2 or (at your option) any later version. + \ / This software is distributed as is, NO WARRANTY. + V_______________________________________________________________ *) + +(* $Id$ *) + +type 'a foterm = + | Leaf of 'a + | Var of int + | Node of ('a foterm) list + +type 'a substitution = (int * 'a foterm) list + +type comparison = Lt | Le | Eq | Ge | Gt | Incomparable + +type rule = SuperpositionRight | SuperpositionLeft | Demodulation +type direction = Left2Right | Right2Left | Nodir +type position = int list + +type 'a proof = + | Exact of 'a + | Step of rule * int * int * direction * position * 'a substitution + (* rule, eq1, eq2, direction of eq2, position, substitution *) + +type 'a literal = + | Equation of 'a foterm (* lhs *) + * 'a foterm (* rhs *) + * 'a foterm (* type *) + * comparison (* orientation *) + | Predicate of 'a foterm + +type varlist = int list + +type 'a unit_clause = + int (* ID *) + * 'a literal + * varlist + * 'a proof (* proof *) + +type 'a passive_clause = int * 'a unit_clause (* weight * equation *) + +module M : Map.S with type key = int + +type 'a bag = 'a unit_clause M.t + -- 2.39.2