No warning on checking unintroduced variables

[adrianleh]

Current behavior

When trying to check two variables that have not been introduced the egraph manually the check quietly fails.

Example:

(datatype Dim (Plus Dim Dim) (NamedDim String) (Lit i64))
(run 5)
(check (= (Lit 1) (Lit 1)))

This can be fixed by explicitly adding the node to the egraph

(datatype Dim (Plus Dim Dim) (NamedDim String) (Lit i64))
(run 5)
(Lit 1)
(check (= (Lit 1) (Lit 1)))

(Thanks @saulshanabrook)

Expected behavior It would be great if either the nodes could be implicitly introduced to the egraph or if there would be at least a warning informing the user about this potential issue

(from https://egraphs.zulipchat.com/#narrow/stream/375765-egg.2Fegglog/topic/First.20time.20user.20of.20python.20bindings/near/421896795)

[oflatt]

Was this fixed by #344? I think it was, based on testing this in the web demo.

[saulshanabrook]

I was wondering the same thing... but it seems like it still is not working? Unless I am just getting an outdated version somehow:

[adrianleh]

I was also getting this issue online and locally with the version I built from main today.

[oflatt]

Oh that's the behavior I expected. check runs a query, so if the two terms are not in the database it fails

[oflatt]

Perhaps we could improve the documentation or issue a warning, as suggested? When / how would we detect when a warning should be issued?

[adrianleh]

I am not familiar with the inner working off egglog so take this with a grain of salt but naïvely I would think a warning should be issued when running check if there is a term within the checked expressions that is not in the database

[oflatt]

That's a good idea- we could detect when there's a term with no pattern variables in it.

[yihozhang]

Yeah, the current behavior is useful when you want to check whether a certain tuple is in the database (e.g., a tuple that would only be added when something is violated).

[adrianleh]

That makes sense, however, I think a warning would still make sense especially for new users. Advanced users who desire this behavior can then ignore/suppress this warning