ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
cmath_lowering_policy.cpp File Reference
Include dependency graph for cmath_lowering_policy.cpp:

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)