Lattice Land Core Library
Loading...
Searching...
No Matches
env.hpp
Go to the documentation of this file.
1// Copyright 2021 Pierre Talbot
2
3#ifndef LALA_CORE_ENV_HPP
4#define LALA_CORE_ENV_HPP
5
6#include "battery/utility.hpp"
7#include "battery/vector.hpp"
8#include "battery/string.hpp"
9#include "battery/tuple.hpp"
10#include "battery/variant.hpp"
11#include "ast.hpp"
12#include "diagnostics.hpp"
13
14#include <string>
15#include <unordered_map>
16#include <functional>
17
18namespace lala {
19
20template<class Allocator>
21struct Variable {
22 template<class T>
23 using bvector = battery::vector<T, Allocator>;
24 using bstring = battery::string<Allocator>;
25
29
31 Variable(const Variable<Allocator>&) = default;
32
33 CUDA NI Variable(const bstring& name, const Sort<Allocator>& sort, AVar av, const Allocator& allocator = Allocator{})
34 : name(name, allocator), sort(sort, allocator), avars(allocator)
35 {
36 avars.push_back(av);
37 }
38
39 template <class Alloc2>
40 CUDA NI Variable(const Variable<Alloc2>& other, const Allocator& allocator = Allocator{})
41 : name(other.name, allocator)
42 , sort(other.sort, allocator)
43 , avars(other.avars, allocator)
44 {}
45
46 CUDA NI std::optional<AVar> avar_of(AType aty) const {
47 for(int i = 0; i < avars.size(); ++i) {
48 if(avars[i].aty() == aty) {
49 return avars[i];
50 }
51 }
52 return {};
53 }
54};
55
56template <class Allocator>
58 using allocator_type = Allocator;
61
62 template<class T>
63 using bvector = battery::vector<T, Allocator>;
64 using bstring = battery::string<Allocator>;
65
67
71
72 template <class Alloc2>
76
77 // For this operator=, we suppose `lvars` is updated before.
78 CUDA this_type& operator=(this_type&& other) {
79 return *this;
80 }
81
82 CUDA this_type& operator=(const this_type& other) {
83 return *this;
84 }
85
86 CUDA std::optional<size_t> lvar_index_of(const char* lv) const {
87 for(size_t i = 0; i < lvars->size(); ++i) {
88 if((*lvars)[i].name == lv) {
89 return i;
90 }
91 }
92 return {};
93 }
94
95 CUDA void push_back(variable_type&& var) {
96 lvars->push_back(std::move(var));
97 }
98
99 CUDA void erase(const char* lv) {}
100
102 this->lvars = lvars;
103 }
104};
105
106template <class Allocator>
108 using allocator_type = Allocator;
111
112 template<class T>
113 using bvector = battery::vector<T, Allocator>;
114 using bstring = battery::string<Allocator>;
115
117 std::unordered_map<std::string, size_t> lvar_index;
118
120 for(size_t i = 0; i < lvars->size(); ++i) {
121 lvar_index[std::string((*lvars)[i].name.data())] = i;
122 }
123 }
124
127
130
131 template <class Alloc2>
135
136 // For this operator=, we suppose `lvars` is updated before.
138 lvar_index = std::move(other.lvar_index);
139 return *this;
140 }
142 lvar_index = other.lvar_index;
143 return *this;
144 }
145
146 std::optional<size_t> lvar_index_of(const char* lv) const {
147 auto it = lvar_index.find(std::string(lv));
148 if(it != lvar_index.end()) {
149 return {it->second};
150 }
151 return {};
152 }
153
155 lvar_index[std::string(var.name.data())] = lvars->size();
156 lvars->push_back(std::move(var));
157 }
158
159 void erase(const char* lv) {
160 lvar_index.erase(std::string(lv));
161 }
162
164 this->lvars = lvars;
165 }
166};
167
168template <class Allocator>
170 using allocator_type = Allocator;
173
174 template<class T>
175 using bvector = battery::vector<T, Allocator>;
176 using bstring = battery::string<Allocator>;
177
178 battery::unique_ptr<HashMapVarIndex<allocator_type>, allocator_type> cpu_index;
179 battery::unique_ptr<ListVarIndex<allocator_type>, allocator_type> gpu_index;
180
181 CUDA DispatchIndex(bvector<variable_type>* lvars): cpu_index(nullptr), gpu_index(nullptr) {
182 gpu_index = std::move(battery::allocate_unique<ListVarIndex<allocator_type>>(lvars->get_allocator(), lvars));
183 #ifndef __CUDA_ARCH__
184 cpu_index = std::move(battery::allocate_unique<HashMapVarIndex<allocator_type>>(lvars->get_allocator(), lvars));
185 #endif
186 }
187
189 : gpu_index(std::move(other.gpu_index))
190 {
191 #ifndef __CUDA_ARCH__
192 cpu_index = std::move(other.cpu_index);
193 #endif
194 }
195
197 {
198 gpu_index = std::move(battery::allocate_unique<ListVarIndex<allocator_type>>(lvars->get_allocator(), *other.gpu_index, lvars));
199 #ifndef __CUDA_ARCH__
200 cpu_index = std::move(battery::allocate_unique<HashMapVarIndex<allocator_type>>(lvars->get_allocator(), *other.cpu_index, lvars));
201 #endif
202 }
203
204 template <class Alloc2>
206 {
207 gpu_index = std::move(battery::allocate_unique<ListVarIndex<allocator_type>>(lvars->get_allocator(), *other.gpu_index, lvars));
208 #ifndef __CUDA_ARCH__
209 cpu_index = std::move(battery::allocate_unique<HashMapVarIndex<allocator_type>>(lvars->get_allocator(), *other.cpu_index, lvars));
210 #endif
211 }
212
213 // For this operator=, we suppose `lvars` is updated before.
215 gpu_index = std::move(other.gpu_index);
216 #ifndef __CUDA_ARCH__
217 cpu_index = std::move(other.cpu_index);
218 #endif
219 return *this;
220 }
221
222 CUDA this_type& operator=(const this_type& other) {
223 *gpu_index = *other.gpu_index;
224 #ifndef __CUDA_ARCH__
225 *cpu_index = *other.cpu_index;
226 #endif
227 return *this;
228 }
229
230 CUDA std::optional<size_t> lvar_index_of(const char* lv) const {
231 #ifdef __CUDA_ARCH__
232 return gpu_index->lvar_index_of(lv);
233 #else
234 return cpu_index->lvar_index_of(lv);
235 #endif
236 }
237
238 CUDA void push_back(variable_type&& var) {
239 #ifdef __CUDA_ARCH__
240 gpu_index->push_back(std::move(var));
241 #else
242 cpu_index->push_back(std::move(var));
243 #endif
244 }
245
246 CUDA void erase(const char* lv) {
247 #ifdef __CUDA_ARCH__
248 gpu_index->erase(lv);
249 #else
250 cpu_index->erase(lv);
251 #endif
252 }
253
255 gpu_index->set_lvars(lvars);
256 #ifndef __CUDA_ARCH__
257 cpu_index->set_lvars(lvars);
258 #endif
259 }
260};
261
262/** A `VarEnv` is a variable environment mapping between logical variables and abstract variables. */
263template <class Allocator>
264class VarEnv {
265 template <class F> using fstring = battery::string<typename F::allocator_type>;
266public:
267 using allocator_type = Allocator;
269
270 constexpr static const char* name = "VarEnv";
271
272 template<class T>
273 using bvector = battery::vector<T, Allocator>;
274 using bstring = battery::string<Allocator>;
275
277
278 template <class Alloc2>
279 friend class VarEnv;
280
281private:
283 bvector<bvector<size_t>> avar2lvar;
284 DispatchIndex<allocator_type> var_index; // Note that this must always be declared *after* `lvars` because it stores a reference to it.
285
286public:
288 avar2lvar.push_back(bvector<int>(get_allocator()));
289 return static_cast<AType>(avar2lvar.size()) - 1;
290 }
291
292private:
293 CUDA NI void extends_abstract_doms(AType aty) {
294 assert(aty != UNTYPED);
295 while(aty >= avar2lvar.size()) {
297 }
298 }
299
300 template <class Alloc2, class Alloc3>
301 CUDA NI AVar extends_vars(AType aty, const battery::string<Alloc2>& name, const Sort<Alloc3>& sort) {
302 extends_abstract_doms(aty);
303 AVar avar(aty, static_cast<int>(avar2lvar[aty].size()));
304 // We first verify the variable doesn't already exist.
305 auto lvar_idx = var_index.lvar_index_of(name.data());
306 if(lvar_idx.has_value()) {
307 auto avar_opt = lvars[*lvar_idx].avar_of(aty);
308 if(avar_opt.has_value()) {
309 return *avar_opt;
310 }
311 else {
312 lvars[*lvar_idx].avars.push_back(avar);
313 }
314 }
315 else {
316 lvar_idx ={lvars.size()};
317 var_index.push_back(Variable<allocator_type>{name, sort, avar, get_allocator()});
318 }
319 avar2lvar[aty].push_back(*lvar_idx);
320 return avar;
321 }
322
323 // Variable redeclaration does not lead to an error, instead the abstract type of the variable is added to the abstract variables list (`avars`) of the variable.
324 template <bool diagnose = false, class F>
325 CUDA NI bool interpret_existential(const F& f, AVar& avar, IDiagnostics& diagnostics) {
326 const auto& vname = battery::get<0>(f.exists());
327 if(f.type() == UNTYPED) {
328 RETURN_INTERPRETATION_ERROR("Untyped abstract type: variable `" + vname + "` has no abstract type.");
329 }
330 auto var = variable_of(vname);
331 if(var.has_value()) {
332 if(var->get().sort != battery::get<1>(f.exists())) {
333 RETURN_INTERPRETATION_ERROR("Invalid redeclaration with different sort: variable `" + vname + "` has already been declared and the sort does not coincide.");
334 }
335 }
336 avar = extends_vars(f.type(), vname, battery::get<1>(f.exists()));
337 return true;
338 }
339
340 template <bool diagnose = false, class F>
341 CUDA NI bool interpret_lv(const F& f, AVar& avar, IDiagnostics& diagnostics) {
342 const auto& vname = f.lv();
343 auto var = variable_of(vname);
344 if(var.has_value()) {
345 if(f.type() != UNTYPED) {
346 auto avarf = var->get().avar_of(f.type());
347 if(avarf.has_value()) {
348 avar = AVar(*avarf);
349 return true;
350 }
351 else {
352 RETURN_INTERPRETATION_ERROR("Variable `" + vname + "` has not been declared in the abstract domain `" + fstring<F>::from_int(f.type()) + "`.");
353 }
354 }
355 else {
356 // We take the first abstract variable as a representative. Need more thought on this, but currently we need it for the simplifier, because each variable is typed in both PC and Simplifier, and this interpretation fails.
357
358 // if(var->get().avars.size() == 1) {
359 avar = AVar(var->get().avars[0]);
360 return true;
361 // }
362 // else {
363 // RETURN_INTERPRETATION_ERROR("Variable occurrence `" + vname + "` is untyped, but exists in multiple abstract domains.");
364 // }
365 }
366 }
367 else {
368 RETURN_INTERPRETATION_ERROR("Undeclared variable `" + vname + "`.");
369 }
370 }
371
372public:
373 CUDA VarEnv(const Allocator& allocator): lvars(allocator), avar2lvar(allocator), var_index(&lvars) {}
374 CUDA VarEnv(this_type&& other): lvars(std::move(other.lvars)), avar2lvar(std::move(other.avar2lvar)), var_index(std::move(other.var_index), &lvars) {}
375 CUDA VarEnv(): VarEnv(Allocator{}) {}
376 CUDA VarEnv(const this_type& other): lvars(other.lvars), avar2lvar(other.avar2lvar), var_index(other.var_index, &lvars) {}
377
378 template <class Alloc2>
379 CUDA VarEnv(const VarEnv<Alloc2>& other, const Allocator& allocator = Allocator{})
380 : lvars(other.lvars, allocator)
381 , avar2lvar(other.avar2lvar, allocator)
382 , var_index(other.var_index, &lvars)
383 {}
384
386 lvars = std::move(other.lvars);
387 avar2lvar = std::move(other.avar2lvar);
388 var_index = std::move(other.var_index);
389 var_index.set_lvars(&lvars);
390 return *this;
391 }
392
393 CUDA this_type& operator=(const this_type& other) {
394 lvars = other.lvars;
395 avar2lvar = other.avar2lvar;
396 var_index = DispatchIndex<allocator_type>(other.var_index, &lvars);
397 var_index.set_lvars(&lvars);
398 return *this;
399 }
400
401 template <class Alloc2>
402 CUDA this_type& operator=(const VarEnv<Alloc2>& other) {
403 lvars = other.lvars;
404 avar2lvar = other.avar2lvar;
405 var_index = DispatchIndex<allocator_type>(other.var_index, &lvars);
406 var_index.set_lvars(&lvars);
407 return *this;
408 }
409
411 return lvars.get_allocator();
412 }
413
414 CUDA size_t num_abstract_doms() const {
415 return avar2lvar.size();
416 }
417
418 CUDA size_t num_vars() const {
419 return lvars.size();
420 }
421
422 CUDA size_t num_vars_in(AType aty) const {
423 if(aty >= avar2lvar.size()) {
424 return 0;
425 }
426 else {
427 return avar2lvar[aty].size();
428 }
429 }
430
431 CUDA void print() const {
432 printf("Environment (%lu variables): \n", num_vars());
433 printf("index\t name sort\tavars\n");
434 for(int i = 0; i < num_vars(); ++i) {
435 printf("%d\t", i);
436 const auto& var = lvars[i];
437 printf("%s", var.name.data());
438 for(int i = var.name.size(); i < 20; ++i) {
439 printf(" ");
440 }
441 var.sort.print(); printf("\t\t");
442 for(int j = 0; j < var.avars.size(); ++j) {
443 printf("(%d,%d)", var.avars[j].aty(), var.avars[j].vid());
444 if(j != var.avars.size() - 1) {
445 printf(",");
446 }
447 }
448 printf("\n");
449 }
450 }
451
452 /** A variable environment can interpret formulas of two forms:
453 * - Existential formula with a valid abstract type (`f.type() != UNTYPED`).
454 * - Variable occurrence.
455 * It returns an abstract variable (`AVar`) corresponding to the variable created (existential) or already presents (occurrence). */
456 template <bool diagnose = false, class F>
457 CUDA NI bool interpret(const F& f, AVar& avar, IDiagnostics& diagnostics) {
458 if(f.is(F::E)) {
459 return interpret_existential<diagnose>(f, avar, diagnostics);
460 }
461 else if(f.is(F::LV)) {
462 return interpret_lv<diagnose>(f, avar, diagnostics);
463 }
464 else if(f.is(F::V)) {
465 if(contains(f.v())) {
466 avar = f.v();
467 return true;
468 }
469 else {
470 RETURN_INTERPRETATION_ERROR("Undeclared abstract variable `" + fstring<F>::from_int(f.v().aty()) + ", " + fstring<F>::from_int(f.v().vid()) + "`.");
471 }
472 }
473 else {
474 RETURN_INTERPRETATION_ERROR("Unsupported formula: `VarEnv` can only interpret quantifiers and occurrences of variables.");
475 }
476 }
477
478 CUDA NI std::optional<std::reference_wrapper<const variable_type>> variable_of(const char* lv) const {
479 auto r = var_index.lvar_index_of(lv);
480 if(r.has_value()) {
481 return std::cref(lvars[*r]);
482 }
483 else {
484 return {};
485 }
486 }
487
488 template <class Alloc2>
489 CUDA std::optional<std::reference_wrapper<const variable_type>> variable_of(const battery::string<Alloc2>& lv) const {
490 return variable_of(lv.data());
491 }
492
493 template <class Alloc2>
494 CUDA bool contains(const battery::string<Alloc2>& lv) const {
495 return contains(lv.data());
496 }
497
498 CUDA bool contains(const char* lv) const {
499 return variable_of(lv).has_value();
500 }
501
502 CUDA bool contains(AVar av) const {
503 if(!av.is_untyped()) {
504 return avar2lvar.size() > av.aty() && avar2lvar[av.aty()].size() > av.vid();
505 }
506 return false;
507 }
508
509 CUDA const variable_type& operator[](int i) const {
510 return lvars[i];
511 }
512
513 CUDA const variable_type& operator[](AVar av) const {
514 return lvars[avar2lvar[av.aty()][av.vid()]];
515 }
516
517 CUDA const bstring& name_of(AVar av) const {
518 return (*this)[av].name;
519 }
520
521 CUDA const Sort<Allocator>& sort_of(AVar av) const {
522 return (*this)[av].sort;
523 }
524
529
530 /** Save the state of the environment. */
531 CUDA NI snapshot_type snapshot() const {
532 snapshot_type snap;
533 for(int i = 0; i < lvars.size(); ++i) {
534 snap.lvars_snap.push_back(lvars[i].avars.size());
535 }
536 for(int i = 0; i < avar2lvar.size(); ++i) {
537 snap.avar2lvar_snap.push_back(avar2lvar[i].size());
538 }
539 return std::move(snap);
540 }
541
542 /** Restore the environment to its previous state `snap`. */
543 CUDA NI void restore(const snapshot_type& snap) {
544 assert(lvars.size() >= snap.lvars_snap.size());
545 assert(avar2lvar.size() >= snap.avar2lvar_snap.size());
546 while(lvars.size() > snap.lvars_snap.size()) {
547 var_index.erase(lvars.back().name.data());
548 lvars.pop_back();
549 }
550 for(int i = 0; i < lvars.size(); ++i) {
551 lvars[i].avars.resize(snap.lvars_snap[i]);
552 }
553 while(avar2lvar.size() > snap.avar2lvar_snap.size()) {
554 avar2lvar.pop_back();
555 }
556 for(int i = 0; i < avar2lvar.size(); ++i) {
557 avar2lvar[i].resize(snap.avar2lvar_snap[i]);
558 }
559 }
560};
561
562/** Given a formula `f` and an environment, return the first variable occurring in `f` or `{}` if `f` has no variable in `env`. */
563template <class F, class Env>
564CUDA NI std::optional<std::reference_wrapper<const typename Env::variable_type>> var_in(const F& f, const Env& env) {
565 const auto& g = var_in(f);
566 switch(g.index()) {
567 case F::V:
568 if(g.v().is_untyped()) { return {}; }
569 else { return std::cref(env[g.v()]); }
570 case F::E:
571 return env.variable_of(battery::get<0>(g.exists()));
572 case F::LV:
573 return env.variable_of(g.lv());
574 }
575 return {};
576}
577}
578
579#endif
Definition ast.hpp:38
CUDA constexpr int vid() const
Definition ast.hpp:69
CUDA constexpr int aty() const
Definition ast.hpp:65
CUDA constexpr bool is_untyped() const
Definition ast.hpp:61
Definition diagnostics.hpp:19
Definition env.hpp:264
CUDA this_type & operator=(this_type &&other)
Definition env.hpp:385
CUDA const variable_type & operator[](AVar av) const
Definition env.hpp:513
CUDA allocator_type get_allocator() const
Definition env.hpp:410
CUDA VarEnv()
Definition env.hpp:375
CUDA size_t num_abstract_doms() const
Definition env.hpp:414
CUDA void print() const
Definition env.hpp:431
CUDA bool contains(const char *lv) const
Definition env.hpp:498
CUDA this_type & operator=(const this_type &other)
Definition env.hpp:393
CUDA VarEnv(this_type &&other)
Definition env.hpp:374
CUDA NI bool interpret(const F &f, AVar &avar, IDiagnostics &diagnostics)
Definition env.hpp:457
CUDA bool contains(AVar av) const
Definition env.hpp:502
battery::vector< T, Allocator > bvector
Definition env.hpp:273
battery::string< Allocator > bstring
Definition env.hpp:274
CUDA const variable_type & operator[](int i) const
Definition env.hpp:509
CUDA size_t num_vars() const
Definition env.hpp:418
CUDA VarEnv(const VarEnv< Alloc2 > &other, const Allocator &allocator=Allocator{})
Definition env.hpp:379
static constexpr const char * name
Definition env.hpp:270
Allocator allocator_type
Definition env.hpp:267
CUDA size_t num_vars_in(AType aty) const
Definition env.hpp:422
CUDA std::optional< std::reference_wrapper< const variable_type > > variable_of(const battery::string< Alloc2 > &lv) const
Definition env.hpp:489
CUDA VarEnv(const Allocator &allocator)
Definition env.hpp:373
CUDA NI AType extends_abstract_dom()
Definition env.hpp:287
CUDA NI std::optional< std::reference_wrapper< const variable_type > > variable_of(const char *lv) const
Definition env.hpp:478
CUDA const bstring & name_of(AVar av) const
Definition env.hpp:517
CUDA this_type & operator=(const VarEnv< Alloc2 > &other)
Definition env.hpp:402
CUDA const Sort< Allocator > & sort_of(AVar av) const
Definition env.hpp:521
CUDA NI snapshot_type snapshot() const
Definition env.hpp:531
CUDA NI void restore(const snapshot_type &snap)
Definition env.hpp:543
CUDA bool contains(const battery::string< Alloc2 > &lv) const
Definition env.hpp:494
CUDA VarEnv(const this_type &other)
Definition env.hpp:376
#define RETURN_INTERPRETATION_ERROR(MSG)
Definition diagnostics.hpp:155
Definition abstract_deps.hpp:14
int AType
Definition sort.hpp:18
CUDA const TFormula< Allocator, ExtendedSig > & var_in(const TFormula< Allocator, ExtendedSig > &f)
Definition algorithm.hpp:146
#define UNTYPED
Definition sort.hpp:21
Definition env.hpp:169
battery::unique_ptr< HashMapVarIndex< allocator_type >, allocator_type > cpu_index
Definition env.hpp:178
CUDA std::optional< size_t > lvar_index_of(const char *lv) const
Definition env.hpp:230
CUDA void erase(const char *lv)
Definition env.hpp:246
CUDA void set_lvars(bvector< variable_type > *lvars)
Definition env.hpp:254
CUDA this_type & operator=(const this_type &other)
Definition env.hpp:222
CUDA DispatchIndex(const DispatchIndex< Alloc2 > &other, bvector< variable_type > *lvars)
Definition env.hpp:205
CUDA this_type & operator=(this_type &&other)
Definition env.hpp:214
CUDA DispatchIndex(const this_type &other, bvector< variable_type > *lvars)
Definition env.hpp:196
CUDA DispatchIndex(bvector< variable_type > *lvars)
Definition env.hpp:181
battery::string< Allocator > bstring
Definition env.hpp:176
battery::unique_ptr< ListVarIndex< allocator_type >, allocator_type > gpu_index
Definition env.hpp:179
battery::vector< T, Allocator > bvector
Definition env.hpp:175
CUDA void push_back(variable_type &&var)
Definition env.hpp:238
Allocator allocator_type
Definition env.hpp:170
CUDA DispatchIndex(this_type &&other, bvector< variable_type > *lvars)
Definition env.hpp:188
Definition env.hpp:107
HashMapVarIndex(this_type &&other, bvector< variable_type > *lvars)
Definition env.hpp:125
void push_back(variable_type &&var)
Definition env.hpp:154
battery::string< Allocator > bstring
Definition env.hpp:114
std::unordered_map< std::string, size_t > lvar_index
Definition env.hpp:117
bvector< variable_type > * lvars
Definition env.hpp:116
Allocator allocator_type
Definition env.hpp:108
battery::vector< T, Allocator > bvector
Definition env.hpp:113
HashMapVarIndex(const this_type &other, bvector< variable_type > *lvars)
Definition env.hpp:128
this_type & operator=(const this_type &other)
Definition env.hpp:141
std::optional< size_t > lvar_index_of(const char *lv) const
Definition env.hpp:146
void set_lvars(bvector< variable_type > *lvars)
Definition env.hpp:163
HashMapVarIndex(bvector< variable_type > *lvars)
Definition env.hpp:119
void erase(const char *lv)
Definition env.hpp:159
this_type & operator=(this_type &&other)
Definition env.hpp:137
HashMapVarIndex(const HashMapVarIndex< Alloc2 > &other, bvector< variable_type > *lvars)
Definition env.hpp:132
Definition env.hpp:57
CUDA this_type & operator=(this_type &&other)
Definition env.hpp:78
CUDA std::optional< size_t > lvar_index_of(const char *lv) const
Definition env.hpp:86
battery::string< Allocator > bstring
Definition env.hpp:64
bvector< variable_type > * lvars
Definition env.hpp:66
CUDA ListVarIndex(this_type &&, bvector< variable_type > *lvars)
Definition env.hpp:69
CUDA ListVarIndex(const this_type &, bvector< variable_type > *lvars)
Definition env.hpp:70
CUDA ListVarIndex(bvector< variable_type > *lvars)
Definition env.hpp:68
CUDA this_type & operator=(const this_type &other)
Definition env.hpp:82
CUDA void erase(const char *lv)
Definition env.hpp:99
CUDA void push_back(variable_type &&var)
Definition env.hpp:95
Allocator allocator_type
Definition env.hpp:58
CUDA ListVarIndex(const ListVarIndex< Alloc2 > &, bvector< variable_type > *lvars)
Definition env.hpp:73
CUDA void set_lvars(bvector< variable_type > *lvars)
Definition env.hpp:101
battery::vector< T, Allocator > bvector
Definition env.hpp:63
Definition sort.hpp:26
Definition env.hpp:525
bvector< size_t > avar2lvar_snap
Definition env.hpp:527
bvector< size_t > lvars_snap
Definition env.hpp:526
Definition env.hpp:21
bstring name
Definition env.hpp:26
battery::string< Allocator > bstring
Definition env.hpp:24
CUDA NI Variable(const bstring &name, const Sort< Allocator > &sort, AVar av, const Allocator &allocator=Allocator{})
Definition env.hpp:33
CUDA NI Variable(const Variable< Alloc2 > &other, const Allocator &allocator=Allocator{})
Definition env.hpp:40
Variable(const Variable< Allocator > &)=default
Variable(Variable< Allocator > &&)=default
CUDA NI std::optional< AVar > avar_of(AType aty) const
Definition env.hpp:46
battery::vector< T, Allocator > bvector
Definition env.hpp:23
bvector< AVar > avars
Definition env.hpp:28
Sort< Allocator > sort
Definition env.hpp:27