ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
cmath_lowering_policy.h
Go to the documentation of this file.
1#pragma once
2
3#include <nlohmann/json.hpp>
4#include <cstddef>
5
11{
13{
14 size_t node_count = 0;
15 size_t depth = 0;
16 size_t call_count = 0;
17 size_t binop_count = 0;
18};
19
20struct budget
21{
22 size_t max_node_count = 32;
23 size_t max_depth = 6;
24 size_t max_call_count = 2;
25 size_t max_binop_count = 8;
26};
27
28expr_cost measure(const nlohmann::json &arg);
29bool within_budget(const nlohmann::json &arg, const budget &b = {});
30
31} // namespace cmath_lowering_policy
Budget model that decides when cmath calls should be lowered inline vs dispatched to the Python model...
Definition cmath_lowering_policy.cpp:4
expr_cost measure(const nlohmann::json &arg)
Definition cmath_lowering_policy.cpp:41
bool within_budget(const nlohmann::json &arg, const budget &b)
Definition cmath_lowering_policy.cpp:48
Definition cmath_lowering_policy.h:21
size_t max_node_count
Definition cmath_lowering_policy.h:22
size_t max_call_count
Definition cmath_lowering_policy.h:24
size_t max_binop_count
Definition cmath_lowering_policy.h:25
size_t max_depth
Definition cmath_lowering_policy.h:23
Definition cmath_lowering_policy.h:13
size_t binop_count
Definition cmath_lowering_policy.h:17
size_t call_count
Definition cmath_lowering_policy.h:16
size_t node_count
Definition cmath_lowering_policy.h:14
size_t depth
Definition cmath_lowering_policy.h:15