From 32bf9982884909d3561dc969d9dba98578f70602 Mon Sep 17 00:00:00 2001 From: Julia Date: Thu, 5 May 2022 23:33:16 +0200 Subject: [PATCH] added star_postfilter to remove dual rays from final stars --- ocaml/Resolution.ml | 9 ++++++--- ocaml/Unification.ml | 3 +-- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/ocaml/Resolution.ml b/ocaml/Resolution.ml index a707fbb..d1ae874 100644 --- a/ocaml/Resolution.ml +++ b/ocaml/Resolution.ml @@ -213,12 +213,15 @@ let star_filter const ((i, j),(ri,rj)) prob = else (List.filter (fun a -> a <> rj) (get_star const j)) ) -(* TODO faire un filtre post application, const_filter*) - (* convert the (ray,ray) list part of a link to an equation, converting its rays to terms *) let link_to_eq prob = List.map (fun (ra, rb) -> (ray_to_term (inv_pol_ray ra)), ray_to_term rb) prob +(* removes prob rays from stars *) +let star_postfilter star prob = + let (prob_a, prob_b) = List.split prob in + List.filter (fun a -> Not(List.mem a prob_a || List.mem a prob_b )) star + (* takes a token, a graph and a constellation and returns the list of tokens to check next and a list of solvable equation *) let divide_token (fam, n_star) graph const = let rec aux g toklist prob fstar = @@ -244,7 +247,7 @@ let exec const = | [] -> star,prob | h::t -> aux (Option.get (divide_token h graph const_ext)) end - in let ((i,_),(_,_)) = (List.hd (List.hd graph)) in let (starf, probf) = aux ([(0,i)],[],[]) in substit_star starf (List.map (fun (i,b) -> (i,term_to_ray b)) (Option.get (solve (link_to_eq probf) []))) + in let ((i,_),(_,_)) = (List.hd (List.hd graph)) in let (starf, probf) = aux ([(0,i)],[],[]) in substit_star (star_postfilter starf probf) (List.map (fun (i,b) -> (i,term_to_ray b)) (Option.get (solve (link_to_eq probf) []))) (* test constellation cyclique déterministe *) let test = [ [Func("c", Neg, [x]); x] ; [Func("c", Pos, [Func("f", Npol, [y])]) ; Func("c", Npol, [x]) ] ] ;; diff --git a/ocaml/Unification.ml b/ocaml/Unification.ml index 03a43da..95a3cc3 100644 --- a/ocaml/Unification.ml +++ b/ocaml/Unification.ml @@ -86,8 +86,7 @@ let rec solve eq sub = | (Func(f, fs), Func(g, gs))::t -> if f = g then (solve ((List.combine fs gs)@t) sub) else None (* If f and g are not equal, the equation can't be solved *) and elim id term eq sub = - if eq = [] then Some sub - else if occurs id term then None (* If that's the cas, we would have something like x = f(x) which can't be solved *) + if occurs id term then None (* If that's the cas, we would have something like x = f(x) which can't be solved *) else let sigma_xy = [(id, term)] in (solve (List.map (fun (a,b) -> (substit a sigma_xy, substit b sigma_xy)) eq) (sigma_xy@sub)) (* We apply the sigma_xy substitution and we add it to the solution list *)