Extract is:module

Given an e-graph representing expressions of our language, we might want to extract, out of all expressions represented by some equivalence class, the best expression (according to a CostFunction) represented by that class The function extractBest allows us to do exactly that: get the best expression represented in an e-class of an e-graph given a CostFunction

Demonstrates use of programmatic model extraction. When programming with SBV, we typically use sat/allSat calls to compute models automatically. In more advanced uses, however, the user might want to use programmable extraction features to do fancier programming. We demonstrate some of these utilities here.