Lattice Land Core Library
Loading...
Searching...
No Matches
Classes | Public Types | Public Member Functions | Static Public Attributes | Friends | List of all members
lala::VarEnv< Allocator > Class Template Reference

#include <env.hpp>

Classes

struct  snapshot_type
 

Public Types

using allocator_type = Allocator
 
using this_type = VarEnv<Allocator>
 
template<class T >
using bvector = battery::vector<T, Allocator>
 
using bstring = battery::string<Allocator>
 
using variable_type = Variable<Allocator>
 

Public Member Functions

CUDA NI AType extends_abstract_dom ()
 
CUDA VarEnv (const Allocator &allocator)
 
CUDA VarEnv (this_type &&other)
 
CUDA VarEnv ()
 
CUDA VarEnv (const this_type &other)
 
template<class Alloc2 >
CUDA VarEnv (const VarEnv< Alloc2 > &other, const Allocator &allocator=Allocator{})
 
CUDA this_type & operator= (this_type &&other)
 
CUDA this_type & operator= (const this_type &other)
 
template<class Alloc2 >
CUDA this_type & operator= (const VarEnv< Alloc2 > &other)
 
CUDA allocator_type get_allocator () const
 
CUDA size_t num_abstract_doms () const
 
CUDA size_t num_vars () const
 
CUDA size_t num_vars_in (AType aty) const
 
template<bool diagnose = false, class F >
CUDA NI bool interpret (const F &f, AVar &avar, IDiagnostics &diagnostics)
 
CUDA NI std::optional< std::reference_wrapper< const variable_type > > variable_of (const char *lv) const
 
template<class Alloc2 >
CUDA std::optional< std::reference_wrapper< const variable_type > > variable_of (const battery::string< Alloc2 > &lv) const
 
template<class Alloc2 >
CUDA bool contains (const battery::string< Alloc2 > &lv) const
 
CUDA bool contains (const char *lv) const
 
CUDA bool contains (AVar av) const
 
CUDA const variable_type & operator[] (int i) const
 
CUDA const variable_type & operator[] (AVar av) const
 
CUDA const bstring & name_of (AVar av) const
 
CUDA const Sort< Allocator > & sort_of (AVar av) const
 
CUDA NI snapshot_type snapshot () const
 
CUDA NI void restore (const snapshot_type &snap)
 

Static Public Attributes

static constexpr const char * name = "VarEnv"
 

Friends

template<class Alloc2 >
class VarEnv
 

Detailed Description

template<class Allocator>
class lala::VarEnv< Allocator >

A VarEnv is a variable environment mapping between logical variables and abstract variables.

Member Typedef Documentation

◆ allocator_type

template<class Allocator >
using lala::VarEnv< Allocator >::allocator_type = Allocator

◆ this_type

template<class Allocator >
using lala::VarEnv< Allocator >::this_type = VarEnv<Allocator>

◆ bvector

template<class Allocator >
template<class T >
using lala::VarEnv< Allocator >::bvector = battery::vector<T, Allocator>

◆ bstring

template<class Allocator >
using lala::VarEnv< Allocator >::bstring = battery::string<Allocator>

◆ variable_type

template<class Allocator >
using lala::VarEnv< Allocator >::variable_type = Variable<Allocator>

Constructor & Destructor Documentation

◆ VarEnv() [1/5]

template<class Allocator >
CUDA lala::VarEnv< Allocator >::VarEnv ( const Allocator & allocator)
inline

◆ VarEnv() [2/5]

template<class Allocator >
CUDA lala::VarEnv< Allocator >::VarEnv ( this_type && other)
inline

◆ VarEnv() [3/5]

template<class Allocator >
CUDA lala::VarEnv< Allocator >::VarEnv ( )
inline

◆ VarEnv() [4/5]

template<class Allocator >
CUDA lala::VarEnv< Allocator >::VarEnv ( const this_type & other)
inline

◆ VarEnv() [5/5]

template<class Allocator >
template<class Alloc2 >
CUDA lala::VarEnv< Allocator >::VarEnv ( const VarEnv< Alloc2 > & other,
const Allocator & allocator = Allocator{} )
inline

Member Function Documentation

◆ extends_abstract_dom()

template<class Allocator >
CUDA NI AType lala::VarEnv< Allocator >::extends_abstract_dom ( )
inline

◆ operator=() [1/3]

template<class Allocator >
CUDA this_type & lala::VarEnv< Allocator >::operator= ( this_type && other)
inline

◆ operator=() [2/3]

template<class Allocator >
CUDA this_type & lala::VarEnv< Allocator >::operator= ( const this_type & other)
inline

◆ operator=() [3/3]

template<class Allocator >
template<class Alloc2 >
CUDA this_type & lala::VarEnv< Allocator >::operator= ( const VarEnv< Alloc2 > & other)
inline

◆ get_allocator()

template<class Allocator >
CUDA allocator_type lala::VarEnv< Allocator >::get_allocator ( ) const
inline

◆ num_abstract_doms()

template<class Allocator >
CUDA size_t lala::VarEnv< Allocator >::num_abstract_doms ( ) const
inline

◆ num_vars()

template<class Allocator >
CUDA size_t lala::VarEnv< Allocator >::num_vars ( ) const
inline

◆ num_vars_in()

template<class Allocator >
CUDA size_t lala::VarEnv< Allocator >::num_vars_in ( AType aty) const
inline

◆ interpret()

template<class Allocator >
template<bool diagnose = false, class F >
CUDA NI bool lala::VarEnv< Allocator >::interpret ( const F & f,
AVar & avar,
IDiagnostics & diagnostics )
inline

A variable environment can interpret formulas of two forms:

  • Existential formula with a valid abstract type (f.type() != UNTYPED).
  • Variable occurrence. It returns an abstract variable (AVar) corresponding to the variable created (existential) or already presents (occurrence).

◆ variable_of() [1/2]

template<class Allocator >
CUDA NI std::optional< std::reference_wrapper< const variable_type > > lala::VarEnv< Allocator >::variable_of ( const char * lv) const
inline

◆ variable_of() [2/2]

template<class Allocator >
template<class Alloc2 >
CUDA std::optional< std::reference_wrapper< const variable_type > > lala::VarEnv< Allocator >::variable_of ( const battery::string< Alloc2 > & lv) const
inline

◆ contains() [1/3]

template<class Allocator >
template<class Alloc2 >
CUDA bool lala::VarEnv< Allocator >::contains ( const battery::string< Alloc2 > & lv) const
inline

◆ contains() [2/3]

template<class Allocator >
CUDA bool lala::VarEnv< Allocator >::contains ( const char * lv) const
inline

◆ contains() [3/3]

template<class Allocator >
CUDA bool lala::VarEnv< Allocator >::contains ( AVar av) const
inline

◆ operator[]() [1/2]

template<class Allocator >
CUDA const variable_type & lala::VarEnv< Allocator >::operator[] ( int i) const
inline

◆ operator[]() [2/2]

template<class Allocator >
CUDA const variable_type & lala::VarEnv< Allocator >::operator[] ( AVar av) const
inline

◆ name_of()

template<class Allocator >
CUDA const bstring & lala::VarEnv< Allocator >::name_of ( AVar av) const
inline

◆ sort_of()

template<class Allocator >
CUDA const Sort< Allocator > & lala::VarEnv< Allocator >::sort_of ( AVar av) const
inline

◆ snapshot()

template<class Allocator >
CUDA NI snapshot_type lala::VarEnv< Allocator >::snapshot ( ) const
inline

Save the state of the environment.

◆ restore()

template<class Allocator >
CUDA NI void lala::VarEnv< Allocator >::restore ( const snapshot_type & snap)
inline

Restore the environment to its previous state snap.

Friends And Related Symbol Documentation

◆ VarEnv

template<class Allocator >
template<class Alloc2 >
friend class VarEnv
friend

Member Data Documentation

◆ name

template<class Allocator >
const char* lala::VarEnv< Allocator >::name = "VarEnv"
staticconstexpr
The documentation for this class was generated from the following file: