Brute-forcing with shared subterms

Stream: Equational

[Joachim Breitner]

Mostly to @Nicholas Carlini :

BTW, I was wondering if it would make sense for you (or anyone else trying to brute-force these) to make the following optimization. Instead of brute forcing

∀ x y, x = x * y
∀ x y, x = x * (x * y)

i.e. each rule separately, maybe brute force

fun x y => #[x == x * y,  x == x * (x * y)]

i.e. for each assignment of variables, look at all equations (of that number of variables). Then you could pre-process the equations and give unique subterm a name, and calculate it only once

fun x y =>
  let t1 = x*y
  let t2 = x*t1
  #[x == t,  x == t2]

Could this have an significant effect on brute-force attempts?

[Nicholas Carlini]

Yeah this is on my list of things I want to do. Right now the bottleneck in the code isn't actually evaluating the functions, it's all the scaffolding around that saves the tables, checks if it's a duplicate, etc. And so making the function evaluation even 10x faster would only give like a 2% performance boost. But once I get the rest of the cruft out of the way (probably in a rewrite in rust) I'll start applying optimizations like this.