Gymbo

gd.h
Go to the documentation of this file.
1
7 #pragma once
8 #include <random>
9
10 #include "type.h"
11
12 namespace gymbo {
13
28 struct GDOptimizer {
29 int num_epochs;
30 float lr;
31 float eps;
32 float param_low;
33 float param_high;
34 bool sign_grad;
36 bool init_param_uniform_int;
40 bool contain_randomized_vars;
42 int seed;
43 int num_used_itr;
44
61 GDOptimizer(int num_epochs = 100, float lr = 1.0, float eps = 1.0,
62 float param_low = -10.0, float param_high = 10.0,
63 bool sign_grad = true, bool init_param_uniform_int = true,
64 int seed = 42)
65 : num_epochs(num_epochs),
66 lr(lr),
67 eps(eps),
68 param_low(param_low),
69 param_high(param_high),
70 sign_grad(sign_grad),
71 init_param_uniform_int(init_param_uniform_int),
72 seed(seed),
73 num_used_itr(0) {}
74
85 bool eval(std::vector<Sym> &path_constraints,
86 std::unordered_map<int, float> params) {
87 bool result = true;
88 for (int i = 0; i < path_constraints.size(); i++) {
89 result = result && (path_constraints[i].eval(params, eps) <= 0.0f);
90 }
91 return result;
92 }
93
110 bool solve(std::vector<Sym> &path_constraints,
111 std::unordered_map<int, float> &params,
112 bool is_init_params_const = true) {
113 if (path_constraints.size() == 0) {
114 return true;
115 }
116
117 std::mt19937 gen(seed);
118 std::uniform_int_distribution<> idist(param_low, param_high);
119 std::uniform_real_distribution<float> rdist(param_low, param_high);
120
121 std::unordered_map<int, bool> is_const;
122 std::unordered_set<int> unique_var_ids;
123
124 for (int i = 0; i < path_constraints.size(); i++) {
125 path_constraints[i].gather_var_ids(unique_var_ids);
126 }
127
128 for (int i : unique_var_ids) {
129 if (params.find(i) == params.end()) {
130 if (init_param_uniform_int) {
131 params.emplace(std::make_pair(i, idist(gen)));
132 } else {
133 params.emplace(std::make_pair(i, rdist(gen)));
134 }
135 is_const.emplace(std::make_pair(i, false));
136 } else {
137 is_const.emplace(std::make_pair(i, is_init_params_const));
138 }
139 }
140
141 int itr = 0;
142 bool is_sat = eval(path_constraints, params);
143 bool is_converge = false;
144
145 while ((!is_sat) && (!is_converge) && (itr < num_epochs)) {
146 Grad grads = Grad({});
147 for (int i = 0; i < path_constraints.size(); i++) {
148 if (path_constraints[i].eval(params, eps) > 0.0f) {
149 grads = grads + path_constraints[i].grad(params, eps);
150 }
151 }
152 is_converge = true;
153 for (auto &g : grads.val) {
154 if (!is_const.at(g.first)) {
155 if (g.second != 0.0f) {
156 is_converge = false;
157 }
158 if (!sign_grad) {
159 params.at(g.first) -= lr * g.second;
160 } else {
161 float sign = 0.0f;
162 if (g.second > 0.0f) {
163 sign = 1.0;
164 } else if (g.second < 0.0f) {
165 sign = -1.0f;
166 }
167 params.at(g.first) -= lr * sign;
168 }
169 }
170 }
171 is_sat = eval(path_constraints, params);
172 itr++;
173 num_used_itr++;
174 }
175 return is_sat;
176 }
177 };
178 } // namespace gymbo
gymbo
Definition: compiler.h:11
gymbo::gen
void gen(Node *node, Prog &prg)
Generates virtual instructions for a given AST node.
Definition: compiler.h:35
gymbo::GDOptimizer
Gradient Descent Optimizer for Symbolic Path Constraints.
Definition: gd.h:28
gymbo::GDOptimizer::sign_grad
bool sign_grad
Definition: gd.h:34
gymbo::GDOptimizer::init_param_uniform_int
bool init_param_uniform_int
Definition: gd.h:36
gymbo::GDOptimizer::num_used_itr
int num_used_itr
Number of used iterations during optimization.
Definition: gd.h:43
gymbo::GDOptimizer::lr
float lr
Learning rate for gradient descent.
Definition: gd.h:30
gymbo::GDOptimizer::contain_randomized_vars
bool contain_randomized_vars
Definition: gd.h:40
gymbo::GDOptimizer::param_low
float param_low
Lower bound for parameter initialization.
Definition: gd.h:32
gymbo::GDOptimizer::num_epochs
int num_epochs
Maximum number of optimization epochs.
Definition: gd.h:29
gymbo::GDOptimizer::eps
float eps
The smallest positive value.
Definition: gd.h:31
gymbo::GDOptimizer::eval
bool eval(std::vector< Sym > &path_constraints, std::unordered_map< int, float > params)
Evaluate if path constraints are satisfied for given parameters.
Definition: gd.h:85
gymbo::GDOptimizer::param_high
float param_high
Upper bound for parameter initialization.
Definition: gd.h:33
gymbo::GDOptimizer::seed
int seed
Random seed for initializing parameter values.
Definition: gd.h:42
gymbo::GDOptimizer::solve
bool solve(std::vector< Sym > &path_constraints, std::unordered_map< int, float > &params, bool is_init_params_const=true)
Solve path constraints using gradient descent optimization.
Definition: gd.h:110
gymbo::GDOptimizer::GDOptimizer
GDOptimizer(int num_epochs=100, float lr=1.0, float eps=1.0, float param_low=-10.0, float param_high=10.0, bool sign_grad=true, bool init_param_uniform_int=true, int seed=42)
Constructor for GDOptimizer.
Definition: gd.h:61
gymbo::Grad
Struct representing the gradient of a symbolic expression.
Definition: type.h:153
gymbo::Grad::val
std::unordered_map< int, float > val
Definition: type.h:155
type.h
Implementatations of basic alias, types, and classes.