3 #ifndef LALA_CORE_ENV_HPP
4 #define LALA_CORE_ENV_HPP
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"
15 #include <unordered_map>
20 template<
class Allocator>
23 using bvector = battery::vector<T, Allocator>;
24 using bstring = battery::string<Allocator>;
39 template <
class Alloc2>
47 for(
int i = 0; i <
avars.size(); ++i) {
48 if(
avars[i].aty() == aty) {
56 template <
class Allocator>
63 using bvector = battery::vector<T, Allocator>;
64 using bstring = battery::string<Allocator>;
72 template <
class Alloc2>
87 for(
size_t i = 0; i <
lvars->size(); ++i) {
88 if((*
lvars)[i].name == lv) {
96 lvars->push_back(std::move(var));
99 CUDA
void erase(
const char* lv) {}
106 template <
class Allocator>
113 using bvector = battery::vector<T, Allocator>;
120 for(
size_t i = 0; i <
lvars->size(); ++i) {
131 template <
class Alloc2>
156 lvars->push_back(std::move(var));
168 template <
class Allocator>
175 using bvector = battery::vector<T, Allocator>;
183 #ifndef __CUDA_ARCH__
191 #ifndef __CUDA_ARCH__
199 #ifndef __CUDA_ARCH__
204 template <
class Alloc2>
208 #ifndef __CUDA_ARCH__
216 #ifndef __CUDA_ARCH__
224 #ifndef __CUDA_ARCH__
256 #ifndef __CUDA_ARCH__
263 template <
class Allocator>
265 template <
class F>
using fstring = battery::string<typename F::allocator_type>;
270 constexpr
static const char*
name =
"VarEnv";
273 using bvector = battery::vector<T, Allocator>;
278 template <
class Alloc2>
289 return static_cast<AType>(avar2lvar.size()) - 1;
293 CUDA NI
void extends_abstract_doms(
AType aty) {
295 while(aty >= avar2lvar.size()) {
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()));
306 if(lvar_idx.has_value()) {
307 auto avar_opt = lvars[*lvar_idx].avar_of(aty);
308 if(avar_opt.has_value()) {
312 lvars[*lvar_idx].avars.push_back(avar);
316 lvar_idx ={lvars.size()};
319 avar2lvar[aty].push_back(*lvar_idx);
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());
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.");
336 avar = extends_vars(f.type(), vname, battery::get<1>(f.exists()));
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();
344 if(var.has_value()) {
346 auto avarf = var->get().avar_of(f.type());
347 if(avarf.has_value()) {
352 RETURN_INTERPRETATION_ERROR(
"Variable `" + vname +
"` has not been declared in the abstract domain `" + fstring<F>::from_int(f.type()) +
"`.");
359 avar = AVar(var->get().avars[0]);
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) {}
376 CUDA
VarEnv(
const this_type& other): lvars(other.lvars), avar2lvar(other.avar2lvar), var_index(other.var_index, &lvars) {}
378 template <
class Alloc2>
380 : lvars(other.lvars, allocator)
381 , avar2lvar(other.avar2lvar, allocator)
382 , var_index(other.var_index, &lvars)
386 lvars = std::move(other.lvars);
387 avar2lvar = std::move(other.avar2lvar);
388 var_index = std::move(other.var_index);
395 avar2lvar = other.avar2lvar;
401 template <
class Alloc2>
404 avar2lvar = other.avar2lvar;
411 return lvars.get_allocator();
415 return avar2lvar.size();
423 if(aty >= avar2lvar.size()) {
427 return avar2lvar[aty].size();
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) {
436 const auto& var = lvars[i];
437 printf(
"%s", var.name.data());
438 for(
int i = var.name.size(); i < 20; ++i) {
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) {
456 template <
bool diagnose = false,
class F>
459 return interpret_existential<diagnose>(f, avar, diagnostics);
461 else if(f.is(F::LV)) {
462 return interpret_lv<diagnose>(f, avar, diagnostics);
464 else if(f.is(F::V)) {
470 RETURN_INTERPRETATION_ERROR(
"Undeclared abstract variable `" + fstring<F>::from_int(f.v().aty()) +
", " + fstring<F>::from_int(f.v().vid()) +
"`.");
478 CUDA NI std::optional<std::reference_wrapper<const variable_type>>
variable_of(
const char* lv)
const {
481 return std::cref(lvars[*r]);
488 template <
class Alloc2>
489 CUDA std::optional<std::reference_wrapper<const variable_type>>
variable_of(
const battery::string<Alloc2>& lv)
const {
493 template <
class Alloc2>
494 CUDA
bool contains(
const battery::string<Alloc2>& lv)
const {
504 return avar2lvar.size() > av.
aty() && avar2lvar[av.
aty()].size() > av.
vid();
514 return lvars[avar2lvar[av.
aty()][av.
vid()]];
518 return (*
this)[av].name;
522 return (*
this)[av].sort;
533 for(
int i = 0; i < lvars.size(); ++i) {
534 snap.
lvars_snap.push_back(lvars[i].avars.size());
536 for(
int i = 0; i < avar2lvar.size(); ++i) {
539 return std::move(snap);
544 assert(lvars.size() >= snap.
lvars_snap.size());
546 while(lvars.size() > snap.
lvars_snap.size()) {
547 var_index.
erase(lvars.back().name.data());
550 for(
int i = 0; i < lvars.size(); ++i) {
554 avar2lvar.pop_back();
556 for(
int i = 0; i < avar2lvar.size(); ++i) {
563 template <
class F,
class Env>
564 CUDA 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);
568 if(g.v().is_untyped()) {
return {}; }
569 else {
return std::cref(env[g.v()]); }
571 return env.variable_of(battery::get<0>(g.exists()));
573 return env.variable_of(g.lv());
constexpr CUDA bool is_untyped() const
Definition: ast.hpp:61
constexpr CUDA int aty() const
Definition: ast.hpp:65
constexpr CUDA int vid() const
Definition: ast.hpp:69
Definition: diagnostics.hpp:19
CUDA allocator_type get_allocator() const
Definition: env.hpp:410
CUDA const variable_type & operator[](AVar av) const
Definition: env.hpp:513
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 const Sort< Allocator > & sort_of(AVar av) const
Definition: env.hpp:521
CUDA this_type & operator=(this_type &&other)
Definition: env.hpp:385
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
CUDA NI std::optional< std::reference_wrapper< const variable_type > > variable_of(const char *lv) const
Definition: env.hpp:478
CUDA this_type & operator=(const VarEnv< Alloc2 > &other)
Definition: env.hpp:402
battery::vector< T, Allocator > bvector
Definition: env.hpp:273
battery::string< Allocator > bstring
Definition: env.hpp:274
CUDA const bstring & name_of(AVar av) const
Definition: env.hpp:517
CUDA size_t num_vars() const
Definition: env.hpp:418
CUDA VarEnv(const VarEnv< Alloc2 > &other, const Allocator &allocator=Allocator{})
Definition: env.hpp:379
Allocator allocator_type
Definition: env.hpp:267
constexpr static const char * name
Definition: env.hpp:270
CUDA this_type & operator=(const this_type &other)
Definition: env.hpp:393
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 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
CUDA const variable_type & operator[](int i) const
Definition: env.hpp:509
#define RETURN_INTERPRETATION_ERROR(MSG)
Definition: diagnostics.hpp:155
Definition: abstract_deps.hpp:14
CUDA const TFormula< Allocator, ExtendedSig > & var_in(const TFormula< Allocator, ExtendedSig > &f)
Definition: algorithm.hpp:146
int AType
Definition: sort.hpp:18
#define UNTYPED
Definition: sort.hpp:21
battery::unique_ptr< HashMapVarIndex< allocator_type >, allocator_type > cpu_index
Definition: env.hpp:178
CUDA void erase(const char *lv)
Definition: env.hpp:246
CUDA void set_lvars(bvector< variable_type > *lvars)
Definition: env.hpp:254
CUDA DispatchIndex(const DispatchIndex< Alloc2 > &other, bvector< variable_type > *lvars)
Definition: env.hpp:205
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
CUDA this_type & operator=(const this_type &other)
Definition: env.hpp:222
Allocator allocator_type
Definition: env.hpp:170
CUDA DispatchIndex(this_type &&other, bvector< variable_type > *lvars)
Definition: env.hpp:188
CUDA std::optional< size_t > lvar_index_of(const char *lv) const
Definition: env.hpp:230
CUDA this_type & operator=(this_type &&other)
Definition: env.hpp:214
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
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
this_type & operator=(this_type &&other)
Definition: env.hpp:137
HashMapVarIndex(bvector< variable_type > *lvars)
Definition: env.hpp:119
void erase(const char *lv)
Definition: env.hpp:159
this_type & operator=(const this_type &other)
Definition: env.hpp:141
HashMapVarIndex(const HashMapVarIndex< Alloc2 > &other, bvector< variable_type > *lvars)
Definition: env.hpp:132
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 this_type & operator=(this_type &&other)
Definition: env.hpp:78
CUDA this_type & operator=(const this_type &other)
Definition: env.hpp:82
CUDA ListVarIndex(const this_type &, bvector< variable_type > *lvars)
Definition: env.hpp:70
CUDA ListVarIndex(bvector< variable_type > *lvars)
Definition: env.hpp:68
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
bvector< size_t > avar2lvar_snap
Definition: env.hpp:527
bvector< size_t > lvars_snap
Definition: env.hpp:526
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
battery::vector< T, Allocator > bvector
Definition: env.hpp:23
bvector< AVar > avars
Definition: env.hpp:28
CUDA NI std::optional< AVar > avar_of(AType aty) const
Definition: env.hpp:46
Sort< Allocator > sort
Definition: env.hpp:27