3#ifndef LALA_CORE_VSTORE_HPP
4#define LALA_CORE_VSTORE_HPP
14 static constexpr bool atoms =
false;
18 static constexpr bool atoms =
true;
37template<
class U,
class Allocator>
45 template <
class Alloc>
53 template <
class VarDom>
57 template <
class Alloc>
58 using tell_type = battery::vector<var_dom<Alloc>, Alloc>;
60 template <
class Alloc>
63 template <
class Alloc = allocator_type>
67 constexpr static const bool sequential = universe_type::sequential;
71 constexpr static const bool preserve_join = universe_type::preserve_join;
72 constexpr static const bool preserve_meet = universe_type::preserve_meet;
75 constexpr static const char*
name =
"VStore";
77 template<
class U2,
class Alloc2>
81 using store_type = battery::vector<universe_type, allocator_type>;
82 using memory_type =
typename universe_type::memory_type;
90 : atype(other.atype), data(other.data), is_at_bot(other.is_at_bot)
95 : atype(atype), data(alloc), is_at_bot(false)
99 : atype(atype), data(size, alloc), is_at_bot(false)
104 : atype(other.atype), data(other.data), is_at_bot(other.is_at_bot)
107 template<
class R,
class Alloc2>
109 : atype(other.atype), data(other.data, alloc), is_at_bot(other.is_at_bot)
114 template<
class R,
class Alloc2,
class... Allocators>
119 atype(other.atype), data(std::move(other.data)), is_at_bot(other.is_at_bot) {}
122 return data.get_allocator();
137 return VStore(atype, alloc);
144 auto s =
VStore{atype, alloc};
153 return bot(env.extends_abstract_dom(), alloc);
160 return top(env.extends_abstract_dom(), alloc);
174 if(is_at_bot) {
return false; }
175 for(
int i = 0; i <
vars(); ++i) {
184 template <
class Alloc = allocator_type>
189 template <
class Alloc>
191 while(snap.size() < data.size()) {
194 is_at_bot.meet_bot();
195 for(
int i = 0; i < snap.size(); ++i) {
196 data[i].join(snap[i]);
197 is_at_bot.join(data[i].
is_bot());
203 template <
bool diagnose,
class F,
class Env,
class Alloc2>
208 if(env.interpret(f.map_atype(atype), k.avar, diagnostics)) {
217 template <
bool diagnose,
class F,
class Env,
class Alloc2>
218 CUDA NI
bool interpret_zero_predicate(
const F& f,
const Env& env,
tell_type<Alloc2>& tell, IDiagnostics& diagnostics)
const {
222 else if(f.is_false()) {
223 tell.push_back(var_dom<Alloc2>(AVar{}, U::bot()));
232 template <IKind kind,
bool diagnose,
class F,
class Env,
class Alloc2>
233 CUDA NI
bool interpret_unary_predicate(
const F& f,
const Env& env,
tell_type<Alloc2>& tell, IDiagnostics& diagnostics)
const {
237 const auto& varf =
var_in(f);
241 tell.push_back(var_dom<Alloc2>(varf.v(), u));
244 auto var =
var_in(f, env);
245 if(!var.has_value()) {
248 auto avar = var->get().avar_of(atype);
249 if(!avar.has_value()) {
250 RETURN_INTERPRETATION_ERROR(
"The variable was not declared in the current abstract element (but exists in other abstract elements).");
252 tell.push_back(var_dom<Alloc2>(*avar, u));
261 template <IKind kind,
bool diagnose,
class F,
class Env,
class Alloc2>
262 CUDA NI
bool interpret_predicate(
const F& f, Env& env,
tell_type<Alloc2>& tell, IDiagnostics& diagnostics)
const {
263 if(f.type() !=
UNTYPED && f.type() !=
aty()) {
268 return interpret_existential<diagnose>(f, env, tell, diagnostics);
272 case 0:
return interpret_zero_predicate<diagnose>(f, env, tell, diagnostics);
273 case 1:
return interpret_unary_predicate<kind, diagnose>(f, env, tell, diagnostics);
279 template <IKind kind,
bool diagnose = false,
class F,
class Env,
class I>
281 if(f.is_untyped() || f.type() ==
aty()) {
282 return interpret_predicate<kind, diagnose>(f, env, intermediate, diagnostics);
300 template <
bool diagnose = false,
class F,
class Env,
class Alloc2>
306 template <
bool diagnose = false,
class F,
class Env,
class Alloc2>
311 template <
class Group,
class Store>
312 CUDA
void copy_to(Group& group, Store& store)
const {
313 assert(
vars() == store.vars());
314 if(group.thread_rank() == 0) {
315 store.is_at_bot = is_at_bot;
320 for (
size_t i = group.thread_rank(); i < store.vars(); i += group.num_threads()) {
321 store.data[i] = data[i];
326 void prefetch(
int dstDevice)
const {
328 cudaMemPrefetchAsync(data.data(), data.size() *
sizeof(
universe_type), dstDevice);
335 data = store_type(data.size(), alloc);
338 template <
class Univ>
345 assert(x.
vid() < data.size());
346 return data[x.
vid()];
355 is_at_bot.join_top();
363 assert(x < data.size());
364 bool has_changed = data[x].meet(dom);
365 has_changed |= is_at_bot.join(data[x].
is_bot());
378 template <
class Alloc2>
383 if(t[0].avar ==
AVar{}) {
384 return is_at_bot.join(
local::B(
true));
386 if(t.back().avar.vid() >= data.size()) {
387 data.resize(t.back().avar.vid()+1);
389 bool has_changed =
false;
390 for(
int i = 0; i < t.size(); ++i) {
391 has_changed |=
embed(t[i].avar, t[i].dom);
397 template <
class U2,
class Alloc2>
399 bool has_changed = is_at_bot.join(other.is_at_bot);
400 int min_size = battery::min(
vars(), other.
vars());
401 for(
int i = 0; i < min_size; ++i) {
402 has_changed |= data[i].meet(other[i]);
404 for(
int i = min_size; i < other.
vars(); ++i) {
405 assert(other[i].
is_top());
411 is_at_bot.meet_bot();
412 for(
int i = 0; i < data.size(); ++i) {
418 template <
class U2,
class Alloc2>
423 int min_size = battery::min(
vars(), other.
vars());
424 bool has_changed = is_at_bot.meet(other.is_at_bot);
425 for(
int i = 0; i < min_size; ++i) {
426 has_changed |= data[i].join(other[i]);
428 for(
int i = min_size; i <
vars(); ++i) {
429 has_changed |= data[i].join(U::top());
431 for(
int i = min_size; i < other.
vars(); ++i) {
432 assert(other[i].
is_top());
440 template <
class Alloc2>
442 for(
int i = 0; i < t.size(); ++i) {
443 if(!(data[t[i].avar.vid()] <= t[i].dom)) {
456 template<
class ExtractionStrategy = NonAtomicExtraction>
457 CUDA
bool is_extractable(
const ExtractionStrategy& strategy = ExtractionStrategy())
const {
461 if constexpr(ExtractionStrategy::atoms) {
462 for(
int i = 0; i < data.size(); ++i) {
472 template<
class ExtractionStrategy = NonAtomicExtraction>
473 __device__
bool is_extractable(
auto& group,
const ExtractionStrategy& strategy = ExtractionStrategy())
const {
477 if constexpr(ExtractionStrategy::atoms) {
479 if(group.thread_rank() == 0) {
483 for(
int i = group.thread_rank(); i < data.size(); i += group.num_threads()) {
500 template<
class U2,
class Alloc2>
502 if((
void*)&ua != (
void*)
this) {
504 ua.is_at_bot.meet_bot();
509 template<
class U2,
class Env,
class Allocator2>
511 auto f = dom.deinterpret(avar, env, allocator);
518 template<
class Env,
class Allocator2 =
typename Env::allocator_type>
521 typename F::Sequence seq{allocator};
522 for(
int i = 0; i < data.size(); ++i) {
524 seq.push_back(F::make_exists(
aty(), env.name_of(v), env.sort_of(v)));
525 seq.push_back(deinterpret(
AVar(
aty(), i), data[i], env, allocator));
527 return F::make_nary(
AND, std::move(seq),
aty());
530 template<
class I,
class Env,
class Allocator2 =
typename Env::allocator_type>
533 if(intermediate.size() == 0) {
534 return F::make_true();
536 else if(intermediate.size() == 1) {
537 return deinterpret(intermediate[0].avar, intermediate[0].dom, env, allocator);
540 typename F::Sequence seq{allocator};
541 for(
int i = 0; i < intermediate.size(); ++i) {
542 seq.push_back(deinterpret(intermediate[i].avar, intermediate[i].dom, env, allocator));
544 return F::make_nary(
AND, std::move(seq),
aty());
553 for(
int i = 0; i <
vars(); ++i) {
555 printf(
"%s", (i+1 ==
vars() ?
"" :
", "));
565template<
class L,
class K,
class Alloc>
568 using U =
decltype(
fmeet(a[0], b[0]));
572 int max_size = battery::max(a.
vars(), b.
vars());
573 int min_size = battery::min(a.
vars(), b.
vars());
575 for(
int i = 0; i < min_size; ++i) {
578 for(
int i = min_size; i < a.
vars(); ++i) {
581 for(
int i = min_size; i < b.
vars(); ++i) {
587template<
class L,
class K,
class Alloc>
590 using U =
decltype(
fjoin(a[0], b[0]));
603 int min_size = battery::min(a.
vars(), b.
vars());
605 for(
int i = 0; i < min_size; ++i) {
612template<
class L,
class K,
class Alloc1,
class Alloc2>
613CUDA
bool operator<=(
const VStore<L, Alloc1>& a,
const VStore<K, Alloc2>& b)
619 int min_size = battery::min(a.vars(), b.vars());
620 for(
int i = 0; i < min_size; ++i) {
621 if(!(a[i] <= b[i])) {
625 for(
int i = min_size; i < b.vars(); ++i) {
634template<
class L,
class K,
class Alloc1,
class Alloc2>
641 int min_size = battery::min(a.
vars(), b.
vars());
643 for(
int i = 0; i < a.
vars(); ++i) {
648 else if(!(a[i] <= b[i])) {
652 else if(!a[i].is_top()) {
657 for(
int i = min_size; i < b.
vars(); ++i) {
666template<
class L,
class K,
class Alloc1,
class Alloc2>
667CUDA
bool operator>=(
const VStore<L, Alloc1>& a,
const VStore<K, Alloc2>& b)
672template<
class L,
class K,
class Alloc1,
class Alloc2>
678template<
class L,
class K,
class Alloc1,
class Alloc2>
688 int min_size = battery::min(a.
vars(), b.
vars());
689 for(
int i = 0; i < min_size; ++i) {
694 for(
int i = min_size; i < a.
vars(); ++i) {
699 for(
int i = min_size; i < b.
vars(); ++i) {
708template<
class L,
class K,
class Alloc1,
class Alloc2>
709CUDA
bool operator!=(
const VStore<L, Alloc1>& a,
const VStore<K, Alloc2>& b)
714template<
class L,
class Alloc>
721 for(
int i = 0; i < vstore.
vars(); ++i) {
722 s << vstore[i] << (i+1 == vstore.
vars() ?
"" :
", ");
CUDA constexpr int vid() const
Definition ast.hpp:69
CUDA constexpr int aty() const
Definition ast.hpp:65
Definition abstract_deps.hpp:28
Definition diagnostics.hpp:19
battery::vector< var_dom< Alloc >, Alloc > tell_type
Definition vstore.hpp:58
static CUDA this_type top(AType atype=UNTYPED, const allocator_type &alloc=allocator_type{})
Definition vstore.hpp:134
static constexpr const bool is_abstract_universe
Definition vstore.hpp:66
CUDA bool deduce(const tell_type< Alloc2 > &t)
Definition vstore.hpp:379
static constexpr const bool preserve_top
Definition vstore.hpp:70
CUDA local::B is_top() const
Definition vstore.hpp:173
static constexpr const bool preserve_bot
Definition vstore.hpp:69
CUDA bool join(const VStore< U2, Alloc2 > &other)
Definition vstore.hpp:419
CUDA bool meet(const VStore< U2, Alloc2 > &other)
Definition vstore.hpp:398
CUDA void copy_to(Group &group, Store &store) const
Definition vstore.hpp:312
static CUDA this_type bot(AType atype=UNTYPED, const allocator_type &alloc=allocator_type{})
Definition vstore.hpp:141
CUDA const universe_type & project(AVar x) const
Definition vstore.hpp:343
CUDA AType aty() const
Definition vstore.hpp:125
CUDA VStore(AType atype, const allocator_type &alloc=allocator_type())
Definition vstore.hpp:94
static constexpr const bool sequential
Definition vstore.hpp:67
tell_type< Alloc > ask_type
Definition vstore.hpp:61
CUDA bool is_extractable(const ExtractionStrategy &strategy=ExtractionStrategy()) const
Definition vstore.hpp:457
CUDA void print() const
Definition vstore.hpp:548
static CUDA this_type top(Env &env, const allocator_type &alloc=allocator_type{})
Definition vstore.hpp:157
CUDA allocator_type get_allocator() const
Definition vstore.hpp:121
CUDA NI TFormula< Allocator2 > deinterpret(const I &intermediate, const Env &env, const Allocator2 &allocator=Allocator2()) const
Definition vstore.hpp:531
CUDA local::B ask(const ask_type< Alloc2 > &t) const
Definition vstore.hpp:441
CUDA void project(AVar x, Univ &u) const
Definition vstore.hpp:339
CUDA void join_top()
Definition vstore.hpp:410
CUDA bool embed(AVar x, const universe_type &dom)
Definition vstore.hpp:370
battery::vector< local_universe, Alloc > snapshot_type
Definition vstore.hpp:64
CUDA local::B is_bot() const
Definition vstore.hpp:166
U universe_type
Definition vstore.hpp:40
static constexpr const bool preserve_join
Definition vstore.hpp:71
CUDA VStore(const VStore< R, allocator_type > &other)
Definition vstore.hpp:103
static constexpr const char * name
Definition vstore.hpp:75
CUDA snapshot_type< Alloc > snapshot(const Alloc &alloc=Alloc()) const
Definition vstore.hpp:185
typename universe_type::local_type local_universe
Definition vstore.hpp:41
friend class VStore
Definition vstore.hpp:78
CUDA bool embed(int x, const universe_type &dom)
Definition vstore.hpp:362
CUDA NI bool interpret(const F &f, Env &env, I &intermediate, IDiagnostics &diagnostics) const
Definition vstore.hpp:280
CUDA VStore(AType atype, size_t size, const allocator_type &alloc=allocator_type())
Definition vstore.hpp:98
CUDA this_type & restore(const snapshot_type< Alloc > &snap)
Definition vstore.hpp:190
CUDA const universe_type & operator[](int x) const
Definition vstore.hpp:350
static constexpr const bool injective_concretization
Definition vstore.hpp:73
static constexpr const bool preserve_concrete_covers
Definition vstore.hpp:74
CUDA void meet_bot()
Definition vstore.hpp:354
CUDA NI bool interpret_ask(const F &f, const Env &env, ask_type< Alloc2 > &ask, IDiagnostics &diagnostics) const
Definition vstore.hpp:307
CUDA VStore(this_type &&other)
Definition vstore.hpp:118
CUDA VStore(const this_type &other)
Definition vstore.hpp:89
static constexpr const bool is_totally_ordered
Definition vstore.hpp:68
CUDA local::B deduce(size_t) const
Definition vstore.hpp:451
CUDA void reset_data(allocator_type alloc)
Definition vstore.hpp:334
CUDA size_t num_deductions() const
Definition vstore.hpp:450
static constexpr const bool preserve_meet
Definition vstore.hpp:72
CUDA NI TFormula< Allocator2 > deinterpret(const Env &env, const Allocator2 &allocator=Allocator2()) const
Definition vstore.hpp:519
CUDA void extract(VStore< U2, Alloc2 > &ua) const
Definition vstore.hpp:501
CUDA VStore(const VStore< R, Alloc2 > &other, const allocator_type &alloc=allocator_type())
Definition vstore.hpp:108
CUDA size_t vars() const
Definition vstore.hpp:130
CUDA VStore(const VStore< R, Alloc2 > &other, const AbstractDeps< Allocators... > &deps)
Definition vstore.hpp:115
Allocator allocator_type
Definition vstore.hpp:42
CUDA NI bool interpret_tell(const F &f, Env &env, tell_type< Alloc2 > &tell, IDiagnostics &diagnostics) const
Definition vstore.hpp:301
static CUDA this_type bot(Env &env, const allocator_type &alloc=allocator_type{})
Definition vstore.hpp:150
#define RETURN_INTERPRETATION_ERROR(MSG)
Definition diagnostics.hpp:155
Definition abstract_deps.hpp:14
std::ostream & operator<<(std::ostream &s, const CartesianProduct< A, As... > &cp)
Definition cartesian_product.hpp:530
CUDA NI void map_avar_to_lvar(F &f, const Env &env, bool erase_type=false)
Definition algorithm.hpp:398
CUDA constexpr LDual dual(const L &x)
Definition arith_bound.hpp:110
int AType
Definition sort.hpp:18
CUDA constexpr auto fjoin(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:463
CUDA constexpr bool operator==(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:503
@ AND
Unary arithmetic function symbols.
Definition ast.hpp:114
CUDA constexpr bool operator<(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:484
CUDA constexpr auto fmeet(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:470
CUDA constexpr bool operator>(const CartesianProduct< As... > &a, const CartesianProduct< Bs... > &b)
Definition cartesian_product.hpp:497
CUDA NI int num_vars(const F &f)
Definition algorithm.hpp:153
CUDA const TFormula< Allocator, ExtendedSig > & var_in(const TFormula< Allocator, ExtendedSig > &f)
Definition algorithm.hpp:145
#define UNTYPED
Definition sort.hpp:21
CUDA var_dom(const Alloc &)
Definition vstore.hpp:51
var_dom(const var_dom< Alloc > &)=default
CUDA var_dom(AVar avar, const local_universe &dom)
Definition vstore.hpp:52
AVar avar
Definition vstore.hpp:47
local_universe dom
Definition vstore.hpp:48
CUDA var_dom(const VarDom &other)
Definition vstore.hpp:54