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>
19template<
class Allocator>
22 using bvector = battery::vector<T, Allocator>;
23 using bstring = battery::string<Allocator>;
38 template <
class Alloc2>
46 for(
int i = 0; i <
avars.size(); ++i) {
47 if(
avars[i].aty() == aty) {
55template <
class Allocator>
62 using bvector = battery::vector<T, Allocator>;
63 using bstring = battery::string<Allocator>;
71 template <
class Alloc2>
86 for(
size_t i = 0; i <
lvars->size(); ++i) {
87 if((*
lvars)[i].name == lv) {
95 lvars->push_back(std::move(var));
98 CUDA
void erase(
const char* lv) {}
105template <
class Allocator>
112 using bvector = battery::vector<T, Allocator>;
119 for(
size_t i = 0; i <
lvars->size(); ++i) {
130 template <
class Alloc2>
155 lvars->push_back(std::move(var));
167template <
class Allocator>
174 using bvector = battery::vector<T, Allocator>;
182 #ifndef __CUDA_ARCH__
190 #ifndef __CUDA_ARCH__
198 #ifndef __CUDA_ARCH__
203 template <
class Alloc2>
207 #ifndef __CUDA_ARCH__
215 #ifndef __CUDA_ARCH__
223 #ifndef __CUDA_ARCH__
255 #ifndef __CUDA_ARCH__
262template <
class Allocator>
264 template <
class F>
using fstring = battery::string<typename F::allocator_type>;
269 constexpr static const char*
name =
"VarEnv";
272 using bvector = battery::vector<T, Allocator>;
277 template <
class Alloc2>
288 return static_cast<AType>(avar2lvar.size()) - 1;
292 CUDA NI
void extends_abstract_doms(
AType aty) {
294 while(aty >= avar2lvar.size()) {
299 template <
class Alloc2,
class Alloc3>
300 CUDA NI AVar extends_vars(
AType aty,
const battery::string<Alloc2>&
name,
const Sort<Alloc3>& sort) {
301 extends_abstract_doms(aty);
302 AVar avar(aty,
static_cast<int>(avar2lvar[aty].size()));
305 if(lvar_idx.has_value()) {
306 auto avar_opt = lvars[*lvar_idx].avar_of(aty);
307 if(avar_opt.has_value()) {
311 lvars[*lvar_idx].avars.push_back(avar);
315 lvar_idx ={lvars.size()};
318 avar2lvar[aty].push_back(*lvar_idx);
323 template <
bool diagnose = false,
class F>
324 CUDA NI
bool interpret_existential(
const F& f, AVar& avar, IDiagnostics& diagnostics) {
325 const auto& vname = battery::get<0>(f.exists());
330 if(var.has_value()) {
331 if(var->sort != battery::get<1>(f.exists())) {
332 RETURN_INTERPRETATION_ERROR(
"Invalid redeclaration with different sort: variable `" + vname +
"` has already been declared and the sort does not coincide.");
335 avar = extends_vars(f.type(), vname, battery::get<1>(f.exists()));
339 template <
bool diagnose = false,
class F>
340 CUDA NI
bool interpret_lv(
const F& f, AVar& avar, IDiagnostics& diagnostics) {
341 const auto& vname = f.lv();
343 if(var.has_value()) {
345 auto avar = var->avar_of(f.type());
346 if(avar.has_value()) {
351 RETURN_INTERPRETATION_ERROR(
"Variable `" + vname +
"` has not been declared in the abstract domain `" + fstring<F>::from_int(f.type()) +
"`.");
358 avar = AVar(var->avars[0]);
372 CUDA
VarEnv(
const Allocator& allocator): lvars(allocator), avar2lvar(allocator), var_index(&lvars) {}
373 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(
const this_type& other): lvars(other.lvars), avar2lvar(other.avar2lvar), var_index(other.var_index, &lvars) {}
377 template <
class Alloc2>
379 : lvars(other.lvars, allocator)
380 , avar2lvar(other.avar2lvar, allocator)
381 , var_index(other.var_index, &lvars)
385 lvars = std::move(other.lvars);
386 avar2lvar = std::move(other.avar2lvar);
387 var_index = std::move(other.var_index);
394 avar2lvar = other.avar2lvar;
400 template <
class Alloc2>
403 avar2lvar = other.avar2lvar;
410 return lvars.get_allocator();
414 return avar2lvar.size();
422 if(aty >= avar2lvar.size()) {
426 return avar2lvar[aty].size();
434 template <
bool diagnose = false,
class F>
437 return interpret_existential<diagnose>(f, avar, diagnostics);
439 else if(f.is(F::LV)) {
440 return interpret_lv<diagnose>(f, avar, diagnostics);
442 else if(f.is(F::V)) {
448 RETURN_INTERPRETATION_ERROR(
"Undeclared abstract variable `" + fstring<F>::from_int(f.v().aty()) +
", " + fstring<F>::from_int(f.v().vid()) +
"`.");
456 CUDA NI thrust::optional<const variable_type&>
variable_of(
const char* lv)
const {
466 template <
class Alloc2>
467 CUDA thrust::optional<const variable_type&>
variable_of(
const battery::string<Alloc2>& lv)
const {
471 template <
class Alloc2>
472 CUDA
bool contains(
const battery::string<Alloc2>& lv)
const {
482 return avar2lvar.size() > av.
aty() && avar2lvar[av.
aty()].size() > av.
vid();
492 return lvars[avar2lvar[av.
aty()][av.
vid()]];
496 return (*
this)[av].name;
500 return (*
this)[av].sort;
511 for(
int i = 0; i < lvars.size(); ++i) {
512 snap.
lvars_snap.push_back(lvars[i].avars.size());
514 for(
int i = 0; i < avar2lvar.size(); ++i) {
517 return std::move(snap);
522 assert(lvars.size() >= snap.
lvars_snap.size());
524 while(lvars.size() > snap.
lvars_snap.size()) {
525 var_index.
erase(lvars.back().name.data());
528 for(
int i = 0; i < lvars.size(); ++i) {
532 avar2lvar.pop_back();
534 for(
int i = 0; i < avar2lvar.size(); ++i) {
541template <
class F,
class Env>
542CUDA NI thrust::optional<const typename Env::variable_type&>
var_in(
const F& f,
const Env& env) {
543 const auto& g =
var_in(f);
546 if(g.v().is_untyped()) {
return {}; }
547 else {
return env[g.v()]; }
549 return env.variable_of(battery::get<0>(g.exists()));
551 return env.variable_of(g.lv());
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
CUDA this_type & operator=(this_type &&other)
Definition env.hpp:384
CUDA const variable_type & operator[](AVar av) const
Definition env.hpp:491
CUDA allocator_type get_allocator() const
Definition env.hpp:409
CUDA VarEnv()
Definition env.hpp:374
CUDA size_t num_abstract_doms() const
Definition env.hpp:413
CUDA bool contains(const char *lv) const
Definition env.hpp:476
CUDA this_type & operator=(const this_type &other)
Definition env.hpp:392
CUDA VarEnv(this_type &&other)
Definition env.hpp:373
CUDA NI bool interpret(const F &f, AVar &avar, IDiagnostics &diagnostics)
Definition env.hpp:435
CUDA bool contains(AVar av) const
Definition env.hpp:480
battery::vector< T, Allocator > bvector
Definition env.hpp:272
battery::string< Allocator > bstring
Definition env.hpp:273
CUDA const variable_type & operator[](int i) const
Definition env.hpp:487
CUDA NI thrust::optional< const variable_type & > variable_of(const char *lv) const
Definition env.hpp:456
CUDA size_t num_vars() const
Definition env.hpp:417
CUDA VarEnv(const VarEnv< Alloc2 > &other, const Allocator &allocator=Allocator{})
Definition env.hpp:378
static constexpr const char * name
Definition env.hpp:269
Allocator allocator_type
Definition env.hpp:266
CUDA size_t num_vars_in(AType aty) const
Definition env.hpp:421
CUDA thrust::optional< const variable_type & > variable_of(const battery::string< Alloc2 > &lv) const
Definition env.hpp:467
CUDA VarEnv(const Allocator &allocator)
Definition env.hpp:372
CUDA NI AType extends_abstract_dom()
Definition env.hpp:286
CUDA const bstring & name_of(AVar av) const
Definition env.hpp:495
CUDA this_type & operator=(const VarEnv< Alloc2 > &other)
Definition env.hpp:401
CUDA const Sort< Allocator > & sort_of(AVar av) const
Definition env.hpp:499
CUDA NI snapshot_type snapshot() const
Definition env.hpp:509
CUDA NI void restore(const snapshot_type &snap)
Definition env.hpp:521
CUDA bool contains(const battery::string< Alloc2 > &lv) const
Definition env.hpp:472
CUDA VarEnv(const this_type &other)
Definition env.hpp:375
#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:145
#define UNTYPED
Definition sort.hpp:21
battery::unique_ptr< HashMapVarIndex< allocator_type >, allocator_type > cpu_index
Definition env.hpp:177
CUDA void erase(const char *lv)
Definition env.hpp:245
CUDA void set_lvars(bvector< variable_type > *lvars)
Definition env.hpp:253
CUDA this_type & operator=(const this_type &other)
Definition env.hpp:221
CUDA DispatchIndex(const DispatchIndex< Alloc2 > &other, bvector< variable_type > *lvars)
Definition env.hpp:204
CUDA this_type & operator=(this_type &&other)
Definition env.hpp:213
CUDA DispatchIndex(const this_type &other, bvector< variable_type > *lvars)
Definition env.hpp:195
CUDA thrust::optional< size_t > lvar_index_of(const char *lv) const
Definition env.hpp:229
CUDA DispatchIndex(bvector< variable_type > *lvars)
Definition env.hpp:180
battery::string< Allocator > bstring
Definition env.hpp:175
battery::unique_ptr< ListVarIndex< allocator_type >, allocator_type > gpu_index
Definition env.hpp:178
battery::vector< T, Allocator > bvector
Definition env.hpp:174
CUDA void push_back(variable_type &&var)
Definition env.hpp:237
Allocator allocator_type
Definition env.hpp:169
CUDA DispatchIndex(this_type &&other, bvector< variable_type > *lvars)
Definition env.hpp:187
HashMapVarIndex(this_type &&other, bvector< variable_type > *lvars)
Definition env.hpp:124
void push_back(variable_type &&var)
Definition env.hpp:153
battery::string< Allocator > bstring
Definition env.hpp:113
std::unordered_map< std::string, size_t > lvar_index
Definition env.hpp:116
bvector< variable_type > * lvars
Definition env.hpp:115
Allocator allocator_type
Definition env.hpp:107
battery::vector< T, Allocator > bvector
Definition env.hpp:112
HashMapVarIndex(const this_type &other, bvector< variable_type > *lvars)
Definition env.hpp:127
this_type & operator=(const this_type &other)
Definition env.hpp:140
thrust::optional< size_t > lvar_index_of(const char *lv) const
Definition env.hpp:145
void set_lvars(bvector< variable_type > *lvars)
Definition env.hpp:162
HashMapVarIndex(bvector< variable_type > *lvars)
Definition env.hpp:118
void erase(const char *lv)
Definition env.hpp:158
this_type & operator=(this_type &&other)
Definition env.hpp:136
HashMapVarIndex(const HashMapVarIndex< Alloc2 > &other, bvector< variable_type > *lvars)
Definition env.hpp:131
CUDA this_type & operator=(this_type &&other)
Definition env.hpp:77
battery::string< Allocator > bstring
Definition env.hpp:63
CUDA thrust::optional< size_t > lvar_index_of(const char *lv) const
Definition env.hpp:85
bvector< variable_type > * lvars
Definition env.hpp:65
CUDA ListVarIndex(this_type &&, bvector< variable_type > *lvars)
Definition env.hpp:68
CUDA ListVarIndex(const this_type &, bvector< variable_type > *lvars)
Definition env.hpp:69
CUDA ListVarIndex(bvector< variable_type > *lvars)
Definition env.hpp:67
CUDA this_type & operator=(const this_type &other)
Definition env.hpp:81
CUDA void erase(const char *lv)
Definition env.hpp:98
CUDA void push_back(variable_type &&var)
Definition env.hpp:94
Allocator allocator_type
Definition env.hpp:57
CUDA ListVarIndex(const ListVarIndex< Alloc2 > &, bvector< variable_type > *lvars)
Definition env.hpp:72
CUDA void set_lvars(bvector< variable_type > *lvars)
Definition env.hpp:100
battery::vector< T, Allocator > bvector
Definition env.hpp:62
bvector< size_t > avar2lvar_snap
Definition env.hpp:505
bvector< size_t > lvars_snap
Definition env.hpp:504
bstring name
Definition env.hpp:25
battery::string< Allocator > bstring
Definition env.hpp:23
CUDA NI thrust::optional< AVar > avar_of(AType aty) const
Definition env.hpp:45
CUDA NI Variable(const bstring &name, const Sort< Allocator > &sort, AVar av, const Allocator &allocator=Allocator{})
Definition env.hpp:32
CUDA NI Variable(const Variable< Alloc2 > &other, const Allocator &allocator=Allocator{})
Definition env.hpp:39
Variable(const Variable< Allocator > &)=default
Variable(Variable< Allocator > &&)=default
battery::vector< T, Allocator > bvector
Definition env.hpp:22
bvector< AVar > avars
Definition env.hpp:27
Sort< Allocator > sort
Definition env.hpp:26