WatForm / fortress

Fortress: Finite Model Finder for Many-Sorted First-Order Logic
MIT License
5 stars 0 forks source link

Speed up Evaluator by compiling definitions to Scala functions #135

Closed ryandancy closed 3 months ago

ryandancy commented 3 months ago

Evaluator was performing poorly (in terms of runtime of the transformer itself) due to spending a lot of time duplicating substitutions inside definitions. Since evaluating a definition is essentially just a function, this adds DefinitionJit, which explicitly transforms function definitions into Scala functions mapping Option[Value] arguments into an Option[Value] output.

There are also a couple other speedups included. The evaluator is now fast enough to be competitive - we should try both the Evaluate and EvaluateQDef compilers, but my intuition is that EvaluateQDef will end up being the winner.

Note: There's a lot of (at least conceptual) duplication between Evaluator and DefinitionJit which should be cleaned up at some point.