ufmg-smite / lean-smt

Tactics for discharging Lean goals into SMT solvers.
Apache License 2.0
80 stars 18 forks source link

Only track fvars needed by translation. #102

Closed abdoo8080 closed 1 month ago

abdoo8080 commented 1 month ago

Only translate free variables encountered during translation. If an expression contains a free variable not needed for translation, we skip it. This, unfortunately, requires disabling of the caching infrastructure to properly handle free variables introduced by quantifiers.

Fixes issue #97.