egraphs-good / egglog

egraphs + datalog!
https://egraphs-good.github.io/egglog/
MIT License
417 stars 46 forks source link

A rule testing a function evaluation against a literal always matches #343

Closed Roldak closed 7 months ago

Roldak commented 7 months ago

The following program:

(function foo () i64 :merge (min old new))

(rule ((= (foo) 5)) ((set (foo) 4)))

(set (foo) 10)

(run 3)

(query-extract (foo))

prints 4, meaning that the rule was matched. This seems unexpected, to me the rule could only match if the condition was (= (foo) 10).

Strangely, replacing 5 in the condition by (+ 1 4) now gives the expected behavior (i.e. the rule does not match).

It is as if 5 was treated as a free variable in this case, instead of referring to the literal 5 (this might not make any sense, I have 0 knowledge of egglog's internals).

Am I missing something?

Thanks!

oflatt commented 7 months ago

That seems bad!