ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
cmath_lowering_policy.h File Reference
#include <nlohmann/json.hpp>
#include <cstddef>
Include dependency graph for cmath_lowering_policy.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  cmath_lowering_policy::expr_cost
struct  cmath_lowering_policy::budget

Namespaces

namespace  cmath_lowering_policy
 Budget model that decides when cmath calls should be lowered inline vs dispatched to the Python model.

Functions

expr_cost cmath_lowering_policy::measure (const nlohmann::json &arg)
bool cmath_lowering_policy::within_budget (const nlohmann::json &arg, const budget &b)