|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
#include <python-frontend/math/cmath_lowering_policy.h>Namespaces | |
| namespace | cmath_lowering_policy |
| Budget model that decides when cmath calls should be lowered inline vs dispatched to the Python model. | |
Functions | |
| static void | cmath_lowering_policy::measure_recursive (const nlohmann::json &node, size_t depth, expr_cost &cost) |
| expr_cost | cmath_lowering_policy::measure (const nlohmann::json &arg) |
| bool | cmath_lowering_policy::within_budget (const nlohmann::json &arg, const budget &b) |