verse-lab / ego Goto Github PK

First of all, thanks for developing this great library! This is exactly what I was looking for.

I just tried to compile the dev version of this library but I got the following error:

File "ego/lib/generic.ml", line 354, characters 50-64:
354 |       let cls2 = self.@[remove_class_data] id2 |> Option.get_exn in
Error (alert deprecated): Containers.Option.get_exn
use CCOpt.get_exn_or instead

The problem is indeed with this line:

which is attempting to use Option.get_exn. This function exists in Base but not in Stdlib.

Fix

A simple fix is to replace this line by:

      let[@warning "-8"] Some cls2 = self.@[remove_class_data] id2 in

I am happy to make a PR if that's convenient to you.

I'm playing with ego and I stumbled upon an issue where I got a randomly generated expression:

(("x" - "x") / (("y" - "y") * 0.40430094613793788)) + ("x" - 0.3616009492803367)

It causes an error:

Uncaught exception:    
  
  (Failure "merge failed: float values 0.163459 <> 0.066087 ")

I simplified it to following expression which still causes an error, simplified further does not cause an issue:

(0 / (0 * 0.40430094613793788)) + ("x" - 0.3616009492803367)

I include my eval and rules.

I regressed into finding these rules cause the issue:

let mm2da_rule =
  EGraph.Rule.make_constant ~from:(qf [%s "?a" * "?b" / "?a"]) ~into:(qf [%s "?b"])
;;

let mm4da_rule =
  EGraph.Rule.make_constant
    ~from:(qf [%s "?a" * "?b" * "?c" * "?d" / "?a"])
    ~into:(qf [%s "?b" * "?c" * "?d"])
;;

My limited understanding of math tells me it's a correct simplification of an expression, is it not?

Do you have any clue what might've I done wrong?

Thanks,
Łukasz

I believe I have found a bug related to egraph merging/rebuilding. It occurs in this test in basic.ml:

let%test "test" =
  let g = EGraph.init () in
  let c1 = EGraph.add_sexp g [%s 1] in
  let c2 = EGraph.add_sexp g [%s 2] in
  let f1 = EGraph.add_sexp g [%s (f 1)] in
  let f2 = EGraph.add_sexp g [%s (f 2)] in
  EGraph.merge g c1 c2;
  EGraph.rebuild g;
  let query = Query.of_sexp [%s f "?a"] in
  let matches = EGraph.ematch g (EGraph.eclasses g) query |> Iter.length in
  Alcotest.(check int) "check num matches" 1 matches

Here, we merge 1 and 2, so f 1 = f 2 by congruence. Thus the query f ?a should return exactly one match. However, two matches are found instead.
This behavior is the same before and after the patch I previously made, and I believe its cause is unrelated to the e-matching algorithm itself.

After some investigating, I determined that initially, there are four e-classes, which I will call c1, c2, f1, f2, which correspond to
the expressions 1, 2, f 1, and f 2, respectively. Since 1 and 2 are merged, the e-classes c1 and c2 are merged, so f1 and f2 should be merged as well. However, they are not merged, and so both f1 and f2 are treated as e-classes we should search, erroneously adding another match. This can be verified by checking that f1 and f2 do not have the same canonical e-class id after rebuilding.

I don't yet fully understand the problem, but it seems that the rebuilding is not propagating to the parent e-classes. In particular, I'm a bit confused about the e-graph's class_members field, which purportedly maps e-classes to its children e-nodes. From my understanding (see egg paper sec. 3.1), maintaining the congruence invariant requires upward merging, which would mean storing the parent e-nodes for each e-class instead. But I could be misunderstanding it.

Hello :)

We're thinking about using ego for a Master's thesis project (for Gillian).
Is ego maintained still? If PRs are submitted, will they be accepted? :)

Cheers