Access variables from check

[rprospero]

I suspect that this is more of a documentation issue than an actual bug, but I cannot seem to find a way to access the variables that are substituted during a check. As a quick example, imagine that I have

(datatype Expr
          (Scalar String)
          (Mul Expr Expr :cost 5))

(let b (Scalar "b"))

(rewrite (Mul (Scalar x) (Scalar y)) (Mul (Scalar y) (Scalar x)))
(rewrite (Mul (Scalar x) (Scalar y)) (Scalar (+ x " " y)))

(let example (Mul b b))

(run 5)

(check (= example
          (Scalar x)))

Now, in this trivial example, I happen to know that the check will pass and the value of x will be "b b". However, I can't seem to find any way to access this value. I know that, in general, there may be multiple possible values for x, but I would be happy seeing any of them.

Again, I suspect that this functionality is already available, but the tutorial and the examples do not seem to contain any documentation on accessing it.

[oflatt]

Good question. From the rust api, egglog has the EGraph::query function:

egglog/src/lib.rs

Line 2402 in 53b9721

pub fn query(

Unfortunately, there's not a nice syntax for getting these variables from egglog. As a work-around, you can make a temporary relation then print it like this:

(datatype Expr
          (Scalar String)
          (Mul Expr Expr :cost 5))

(let b (Scalar "b"))

(rewrite (Mul (Scalar x) (Scalar y)) (Mul (Scalar y) (Scalar x)))
(rewrite (Mul (Scalar x) (Scalar y)) (Scalar (+ x " " y)))

(let example (Mul b b))

(run 5)


(relation output (Expr))

(rule ((= example
          (Scalar x)))
      ((output example)))

(run 1)
(print-function output)