Daniel Kroening
GitHub
commit
09091152ac
|
|
@ -0,0 +1,832 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Sharing map
|
||||
|
||||
Author: Daniel Poetzl
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
#ifndef CPROVER_UTIL_SHARING_MAP_H
|
||||
#define CPROVER_UTIL_SHARING_MAP_H
|
||||
|
||||
#include <string>
|
||||
#include <stack>
|
||||
#include <vector>
|
||||
#include <map>
|
||||
#include <stdexcept>
|
||||
#include <functional>
|
||||
#include <memory>
|
||||
#include <iosfwd>
|
||||
#include <cassert>
|
||||
|
||||
#include <util/string2int.h>
|
||||
#include <util/threeval.h>
|
||||
#include <util/irep.h>
|
||||
#include <util/sharing_node.h>
|
||||
|
||||
#define _sm_assert(b) assert(b)
|
||||
//#define _sm_assert(b)
|
||||
|
||||
#define SHARING_MAPT(R) \
|
||||
template <class keyT, class valueT, class hashT, class predT> \
|
||||
R sharing_mapt<keyT, valueT, hashT, predT>
|
||||
|
||||
#define SHARING_MAPT2(CV, ST) \
|
||||
template <class keyT, class valueT, class hashT, class predT> \
|
||||
CV typename sharing_mapt<keyT, valueT, hashT, predT>::ST \
|
||||
sharing_mapt<keyT, valueT, hashT, predT>
|
||||
|
||||
template <
|
||||
class keyT,
|
||||
class valueT,
|
||||
class hashT=std::hash<keyT>,
|
||||
class predT=std::equal_to<keyT>>
|
||||
class sharing_mapt
|
||||
{
|
||||
public:
|
||||
friend void sharing_map_interface_test();
|
||||
friend void sharing_map_copy_test();
|
||||
friend void sharing_map_collision_test();
|
||||
friend void sharing_map_view_test();
|
||||
|
||||
~sharing_mapt()
|
||||
{
|
||||
}
|
||||
|
||||
typedef keyT key_type;
|
||||
typedef valueT mapped_type;
|
||||
typedef std::pair<const key_type, mapped_type> value_type;
|
||||
|
||||
typedef hashT hash;
|
||||
typedef predT key_equal;
|
||||
|
||||
typedef sharing_mapt<key_type, mapped_type, hash, key_equal> self_type;
|
||||
typedef sharing_nodet<key_type, mapped_type, key_equal> node_type;
|
||||
|
||||
typedef size_t size_type;
|
||||
|
||||
typedef const std::pair<const mapped_type &, const bool> const_find_type;
|
||||
typedef const std::pair<mapped_type &, const bool> find_type;
|
||||
|
||||
typedef std::vector<key_type> keyst;
|
||||
|
||||
typedef typename node_type::subt subt;
|
||||
typedef typename node_type::containert containert;
|
||||
|
||||
// key-value map
|
||||
node_type map;
|
||||
|
||||
// number of elements in the map
|
||||
size_type num=0;
|
||||
|
||||
// dummy element returned when no element was found
|
||||
static mapped_type dummy;
|
||||
|
||||
// compile-time configuration
|
||||
|
||||
static const std::string not_found_msg;
|
||||
|
||||
static const size_t bits;
|
||||
static const size_t chunk;
|
||||
|
||||
static const size_t mask;
|
||||
static const size_t steps;
|
||||
|
||||
// interface
|
||||
|
||||
size_type erase(
|
||||
const key_type &k,
|
||||
const tvt &key_exists=tvt::unknown());
|
||||
|
||||
size_type erase_all(
|
||||
const keyst &ks,
|
||||
const tvt &key_exists=tvt::unknown()); // applies to all keys
|
||||
|
||||
// return true if element was inserted
|
||||
const_find_type insert(
|
||||
const key_type &k,
|
||||
const mapped_type &v,
|
||||
const tvt &key_exists=tvt::unknown());
|
||||
|
||||
const_find_type insert(
|
||||
const value_type &p,
|
||||
const tvt &key_exists=tvt::unknown());
|
||||
|
||||
find_type place(
|
||||
const key_type &k,
|
||||
const mapped_type &v);
|
||||
|
||||
find_type place(
|
||||
const value_type &p);
|
||||
|
||||
find_type find(
|
||||
const key_type &k,
|
||||
const tvt &key_exists=tvt::unknown());
|
||||
|
||||
const_find_type find(const key_type &k) const;
|
||||
|
||||
mapped_type &at(
|
||||
const key_type &k,
|
||||
const tvt &key_exists=tvt::unknown());
|
||||
|
||||
const mapped_type &at(const key_type &k) const;
|
||||
|
||||
mapped_type &operator[](const key_type &k);
|
||||
|
||||
void swap(self_type &other)
|
||||
{
|
||||
map.swap(other.map);
|
||||
|
||||
size_t tmp=num;
|
||||
num=other.num;
|
||||
other.num=tmp;
|
||||
}
|
||||
|
||||
size_type size() const
|
||||
{
|
||||
return num;
|
||||
}
|
||||
|
||||
bool empty() const
|
||||
{
|
||||
return num==0;
|
||||
}
|
||||
|
||||
void clear()
|
||||
{
|
||||
map.clear();
|
||||
num=0;
|
||||
}
|
||||
|
||||
bool has_key(const key_type &k) const
|
||||
{
|
||||
return get_leaf_node(k)!=nullptr;
|
||||
}
|
||||
|
||||
// views
|
||||
|
||||
typedef std::pair<const key_type &, const mapped_type &> view_itemt;
|
||||
typedef std::vector<view_itemt> viewt;
|
||||
|
||||
class delta_view_itemt
|
||||
{
|
||||
public:
|
||||
delta_view_itemt(
|
||||
const bool in_both,
|
||||
const key_type &k,
|
||||
const mapped_type &m,
|
||||
const mapped_type &other_m) :
|
||||
in_both(in_both),
|
||||
k(k),
|
||||
m(m),
|
||||
other_m(other_m) {}
|
||||
|
||||
// if true key is in both maps, if false key is only in the map
|
||||
// from which the view was obtained
|
||||
const bool in_both;
|
||||
|
||||
const key_type &k;
|
||||
|
||||
const mapped_type &m;
|
||||
const mapped_type &other_m;
|
||||
};
|
||||
|
||||
typedef std::vector<delta_view_itemt> delta_viewt;
|
||||
|
||||
void get_view(viewt &view) const;
|
||||
|
||||
void get_delta_view(
|
||||
const self_type &other,
|
||||
delta_viewt &delta_view,
|
||||
const bool only_common=true) const;
|
||||
|
||||
protected:
|
||||
// helpers
|
||||
|
||||
node_type *get_container_node(const key_type &k);
|
||||
const node_type *get_container_node(const key_type &k) const;
|
||||
|
||||
const node_type *get_leaf_node(const key_type &k) const;
|
||||
|
||||
void gather_all(const node_type &n, delta_viewt &delta_view) const;
|
||||
};
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: get_view
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT(void)::get_view(viewt &view) const
|
||||
{
|
||||
assert(view.empty());
|
||||
|
||||
std::stack<const node_type *> stack;
|
||||
|
||||
if(empty())
|
||||
return;
|
||||
|
||||
stack.push(&map);
|
||||
|
||||
do
|
||||
{
|
||||
const node_type *n=stack.top();
|
||||
stack.pop();
|
||||
|
||||
if(n->is_container())
|
||||
{
|
||||
for(const auto &child : n->get_container())
|
||||
{
|
||||
view.push_back(view_itemt(child.get_key(), child.get_value()));
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
assert(n->is_internal());
|
||||
|
||||
for(const auto &child : n->get_sub())
|
||||
{
|
||||
stack.push(&child.second);
|
||||
}
|
||||
}
|
||||
}
|
||||
while(!stack.empty());
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: gather_all
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT(void)::gather_all(const node_type &n, delta_viewt &delta_view)
|
||||
const
|
||||
{
|
||||
std::stack<const node_type *> stack;
|
||||
stack.push(&n);
|
||||
|
||||
do
|
||||
{
|
||||
const node_type *n=stack.top();
|
||||
stack.pop();
|
||||
|
||||
if(n->is_container())
|
||||
{
|
||||
for(const auto &child : n->get_container())
|
||||
{
|
||||
delta_view.push_back(
|
||||
delta_view_itemt(
|
||||
false,
|
||||
child.get_key(),
|
||||
child.get_value(),
|
||||
dummy));
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
assert(n->is_internal());
|
||||
|
||||
for(const auto &child : n->get_sub())
|
||||
{
|
||||
stack.push(&child.second);
|
||||
}
|
||||
}
|
||||
}
|
||||
while(!stack.empty());
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: get_delta_view
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT(void)::get_delta_view(
|
||||
const self_type &other,
|
||||
delta_viewt &delta_view,
|
||||
const bool only_common) const
|
||||
{
|
||||
assert(delta_view.empty());
|
||||
|
||||
typedef std::pair<const node_type *, const node_type *> stack_itemt;
|
||||
std::stack<stack_itemt> stack;
|
||||
|
||||
if(empty())
|
||||
return;
|
||||
|
||||
if(other.empty())
|
||||
{
|
||||
if(!only_common)
|
||||
{
|
||||
gather_all(map, delta_view);
|
||||
}
|
||||
return;
|
||||
}
|
||||
|
||||
stack.push(stack_itemt(&map, &other.map));
|
||||
|
||||
do
|
||||
{
|
||||
const stack_itemt si=stack.top();
|
||||
stack.pop();
|
||||
|
||||
const node_type *n1=si.first;
|
||||
const node_type *n2=si.second;
|
||||
|
||||
if(n1->is_internal())
|
||||
{
|
||||
_sn_assert(n2->is_internal());
|
||||
|
||||
for(const auto &child : n1->get_sub())
|
||||
{
|
||||
const node_type *p;
|
||||
|
||||
p=n2->find_child(child.first);
|
||||
if(p==nullptr)
|
||||
{
|
||||
if(!only_common)
|
||||
{
|
||||
gather_all(child.second, delta_view);
|
||||
}
|
||||
}
|
||||
else if(!child.second.shares_with(*p))
|
||||
{
|
||||
stack.push(stack_itemt(&child.second, p));
|
||||
}
|
||||
}
|
||||
}
|
||||
else if(n1->is_container())
|
||||
{
|
||||
_sn_assert(n2->is_container());
|
||||
|
||||
for(const auto &l1 : n1->get_container())
|
||||
{
|
||||
const key_type &k1=l1.get_key();
|
||||
bool found=false;
|
||||
|
||||
for(const auto &l2 : n2->get_container())
|
||||
{
|
||||
const key_type &k2=l2.get_key();
|
||||
|
||||
if(l1.shares_with(l2))
|
||||
{
|
||||
found=true;
|
||||
break;
|
||||
}
|
||||
|
||||
if(key_equal()(k1, k2))
|
||||
{
|
||||
delta_view.push_back(
|
||||
delta_view_itemt(
|
||||
true,
|
||||
k1,
|
||||
l1.get_value(),
|
||||
l2.get_value()));
|
||||
|
||||
found=true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if(!only_common && !found)
|
||||
{
|
||||
delta_view.push_back(
|
||||
delta_view_itemt(
|
||||
false,
|
||||
l1.get_key(),
|
||||
l1.get_value(),
|
||||
dummy));
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
assert(false);
|
||||
}
|
||||
}
|
||||
while(!stack.empty());
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: get_container_node
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, node_type *)::get_container_node(const key_type &k)
|
||||
{
|
||||
size_t key=hash()(k);
|
||||
node_type *p=↦
|
||||
|
||||
for(unsigned i=0; i<steps; i++)
|
||||
{
|
||||
unsigned bit=key&mask;
|
||||
key>>=chunk;
|
||||
|
||||
p=p->add_child(bit);
|
||||
}
|
||||
|
||||
return p;
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: get_container_node
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(const, node_type *)::get_container_node(const key_type &k) const
|
||||
{
|
||||
size_t key=hash()(k);
|
||||
const node_type *p=↦
|
||||
|
||||
for(unsigned i=0; i<steps; i++)
|
||||
{
|
||||
unsigned bit=key&mask;
|
||||
key>>=chunk;
|
||||
|
||||
p=p->find_child(bit);
|
||||
if(p==nullptr)
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
assert(p->is_container());
|
||||
|
||||
return p;
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: get_leaf_node
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(const, node_type *)::get_leaf_node(const key_type &k) const
|
||||
{
|
||||
const node_type *p=get_container_node(k);
|
||||
if(p==nullptr)
|
||||
return nullptr;
|
||||
|
||||
p=p->find_leaf(k);
|
||||
|
||||
return p;
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: erase
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, size_type)::erase(
|
||||
const key_type &k,
|
||||
const tvt &key_exists)
|
||||
{
|
||||
assert(!key_exists.is_false());
|
||||
|
||||
// check if key exists
|
||||
if(key_exists.is_unknown() && !has_key(k))
|
||||
return 0;
|
||||
|
||||
node_type *del=nullptr;
|
||||
unsigned del_bit;
|
||||
|
||||
size_t key=hash()(k);
|
||||
node_type *p=↦
|
||||
|
||||
for(unsigned i=0; i<steps; i++)
|
||||
{
|
||||
unsigned bit=key&mask;
|
||||
key>>=chunk;
|
||||
|
||||
const subt &sub=as_const(p)->get_sub();
|
||||
if(sub.size()>1 || del==nullptr)
|
||||
{
|
||||
del=p;
|
||||
del_bit=bit;
|
||||
}
|
||||
|
||||
p=p->add_child(bit);
|
||||
}
|
||||
|
||||
_sm_assert(p->is_container());
|
||||
|
||||
{
|
||||
const containert &c=as_const(p)->get_container();
|
||||
|
||||
if(c.size()==1)
|
||||
{
|
||||
del->remove_child(del_bit);
|
||||
num--;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
containert &c=p->get_container();
|
||||
_sm_assert(c.size()>1);
|
||||
p->remove_leaf(k);
|
||||
num--;
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: erase_all
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, size_type)::erase_all(
|
||||
const keyst &ks,
|
||||
const tvt &key_exists)
|
||||
{
|
||||
size_type cnt=0;
|
||||
|
||||
for(const key_type &k : ks)
|
||||
{
|
||||
cnt+=erase(k, key_exists);
|
||||
}
|
||||
|
||||
return cnt;
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: insert
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, const_find_type)::insert(
|
||||
const key_type &k,
|
||||
const mapped_type &m,
|
||||
const tvt &key_exists)
|
||||
{
|
||||
_sn_assert(!key_exists.is_true());
|
||||
|
||||
if(key_exists.is_unknown())
|
||||
{
|
||||
const node_type *p=as_const(this)->get_leaf_node(k);
|
||||
if(p!=nullptr)
|
||||
return const_find_type(p->get_value(), false);
|
||||
}
|
||||
|
||||
node_type *p=get_container_node(k);
|
||||
_sn_assert(p!=nullptr);
|
||||
|
||||
p=p->place_leaf(k, m);
|
||||
num++;
|
||||
|
||||
return const_find_type(as_const(p)->get_value(), true);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: insert
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, const_find_type)::insert(
|
||||
const value_type &p,
|
||||
const tvt &key_exists)
|
||||
{
|
||||
return insert(p.first, p.second, key_exists);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: place
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, find_type)::place(
|
||||
const key_type &k,
|
||||
const mapped_type &m)
|
||||
{
|
||||
node_type *c=get_container_node(k);
|
||||
_sm_assert(c!=nullptr);
|
||||
|
||||
node_type *p=c->find_leaf(k);
|
||||
|
||||
if(p!=nullptr)
|
||||
return find_type(p->get_value(), false);
|
||||
|
||||
p=c->place_leaf(k, m);
|
||||
num++;
|
||||
|
||||
return find_type(p->get_value(), true);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: place
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, find_type)::place(
|
||||
const value_type &p)
|
||||
{
|
||||
return place(p.first, p.second);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: find
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, find_type)::find(
|
||||
const key_type &k,
|
||||
const tvt &key_exists)
|
||||
{
|
||||
_sm_assert(!key_exists.is_false());
|
||||
|
||||
if(key_exists.is_unknown() && !has_key(k))
|
||||
return find_type(dummy, false);
|
||||
|
||||
node_type *p=get_container_node(k);
|
||||
_sm_assert(p!=nullptr);
|
||||
|
||||
p=p->find_leaf(k);
|
||||
_sm_assert(p!=nullptr);
|
||||
|
||||
return find_type(p->get_value(), true);
|
||||
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: find
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, const_find_type)::find(const key_type &k) const
|
||||
{
|
||||
const node_type *p=get_leaf_node(k);
|
||||
|
||||
if(p==nullptr)
|
||||
return const_find_type(dummy, false);
|
||||
|
||||
return const_find_type(p->get_value(), true);
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: at
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, mapped_type &)::at(
|
||||
const key_type &k,
|
||||
const tvt &key_exists)
|
||||
{
|
||||
find_type r=find(k, key_exists);
|
||||
|
||||
if(!r.second)
|
||||
throw std::out_of_range(not_found_msg);
|
||||
|
||||
return r.first;
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: at
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(const, mapped_type &)::at(const key_type &k) const
|
||||
{
|
||||
const_find_type r=find(k);
|
||||
if(!r.second)
|
||||
throw std::out_of_range(not_found_msg);
|
||||
|
||||
return r.first;
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: operator[]
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
SHARING_MAPT2(, mapped_type &)::operator[](const key_type &k)
|
||||
{
|
||||
return place(k, mapped_type()).first;
|
||||
}
|
||||
|
||||
// static constants
|
||||
|
||||
SHARING_MAPT(const std::string)::not_found_msg="key not found";
|
||||
|
||||
// config
|
||||
SHARING_MAPT(const size_t)::bits=18;
|
||||
SHARING_MAPT(const size_t)::chunk=3;
|
||||
|
||||
// derived config
|
||||
SHARING_MAPT(const size_t)::mask=0xffff>>(16-chunk);
|
||||
SHARING_MAPT(const size_t)::steps=bits/chunk;
|
||||
|
||||
SHARING_MAPT2(, mapped_type)::dummy;
|
||||
|
||||
#endif
|
||||
|
|
@ -0,0 +1,346 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Sharing node
|
||||
|
||||
Author: Daniel Poetzl
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
#ifndef CPROVER_UTIL_SHARING_NODE_H
|
||||
#define CPROVER_UTIL_SHARING_NODE_H
|
||||
|
||||
#include <list>
|
||||
#include <map>
|
||||
#include <memory>
|
||||
#include <cassert>
|
||||
|
||||
#define _sn_assert(b) assert(b)
|
||||
//#define _sn_assert(b)
|
||||
|
||||
template <class T>
|
||||
const T *as_const(T *t)
|
||||
{
|
||||
return t;
|
||||
}
|
||||
|
||||
template <
|
||||
class keyT,
|
||||
class valueT,
|
||||
class predT=std::equal_to<keyT>,
|
||||
bool no_sharing=false>
|
||||
class sharing_nodet
|
||||
{
|
||||
public:
|
||||
friend void sharing_node_test();
|
||||
|
||||
typedef keyT key_type;
|
||||
typedef valueT mapped_type;
|
||||
|
||||
typedef predT key_equal;
|
||||
|
||||
typedef sharing_nodet<key_type, mapped_type, key_equal> self_type;
|
||||
|
||||
typedef std::map<unsigned, self_type> subt;
|
||||
typedef std::list<self_type> containert;
|
||||
|
||||
typedef const std::pair<const self_type &, const bool> const_find_type;
|
||||
typedef const std::pair<self_type &, const bool> find_type;
|
||||
|
||||
sharing_nodet() : data(empty_data)
|
||||
{
|
||||
_sn_assert(data.use_count()>=2);
|
||||
}
|
||||
|
||||
sharing_nodet(const key_type &k, const mapped_type &m) : data(empty_data)
|
||||
{
|
||||
_sn_assert(data.use_count()>=2);
|
||||
|
||||
dt &d=write();
|
||||
|
||||
_sn_assert(d.k==nullptr);
|
||||
d.k=std::make_shared<key_type>(k);
|
||||
|
||||
_sn_assert(d.m==nullptr);
|
||||
d.m.reset(new mapped_type(m));
|
||||
}
|
||||
|
||||
sharing_nodet(const self_type &other)
|
||||
{
|
||||
#ifdef SM_NO_SHARING
|
||||
data=std::make_shared<dt>(*other.data);
|
||||
#else
|
||||
if(no_sharing)
|
||||
{
|
||||
data=std::make_shared<dt>(*other.data);
|
||||
}
|
||||
else
|
||||
{
|
||||
data=other.data;
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
// check type of node
|
||||
|
||||
bool is_empty() const
|
||||
{
|
||||
_sn_assert(is_well_formed());
|
||||
return data==empty_data;
|
||||
}
|
||||
|
||||
bool is_internal() const
|
||||
{
|
||||
_sn_assert(is_well_formed());
|
||||
_sn_assert(!is_empty());
|
||||
return !get_sub().empty();
|
||||
}
|
||||
|
||||
bool is_container() const
|
||||
{
|
||||
_sn_assert(is_well_formed());
|
||||
_sn_assert(!is_empty());
|
||||
return !get_container().empty();
|
||||
}
|
||||
|
||||
bool is_leaf() const
|
||||
{
|
||||
_sn_assert(is_well_formed());
|
||||
_sn_assert(!is_empty());
|
||||
return read().is_leaf();
|
||||
}
|
||||
|
||||
// accessors
|
||||
|
||||
const key_type &get_key() const
|
||||
{
|
||||
_sn_assert(is_leaf());
|
||||
return *read().k;
|
||||
}
|
||||
|
||||
const mapped_type &get_value() const
|
||||
{
|
||||
_sn_assert(is_leaf());
|
||||
return *read().m;
|
||||
}
|
||||
|
||||
mapped_type &get_value()
|
||||
{
|
||||
_sn_assert(is_leaf());
|
||||
return *write().m;
|
||||
}
|
||||
|
||||
subt &get_sub()
|
||||
{
|
||||
return write().sub;
|
||||
}
|
||||
|
||||
const subt &get_sub() const
|
||||
{
|
||||
return read().sub;
|
||||
}
|
||||
|
||||
containert &get_container()
|
||||
{
|
||||
return write().con;
|
||||
}
|
||||
|
||||
const containert &get_container() const
|
||||
{
|
||||
return read().con;
|
||||
}
|
||||
|
||||
// internal nodes
|
||||
|
||||
const self_type *find_child(const unsigned n) const
|
||||
{
|
||||
const subt &s=get_sub();
|
||||
typename subt::const_iterator it=s.find(n);
|
||||
|
||||
if(it!=s.end())
|
||||
return &it->second;
|
||||
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
self_type *add_child(const unsigned n)
|
||||
{
|
||||
subt &s=get_sub();
|
||||
return &s[n];
|
||||
}
|
||||
|
||||
void remove_child(const unsigned n)
|
||||
{
|
||||
subt &s=get_sub();
|
||||
size_t r=s.erase(n);
|
||||
|
||||
_sn_assert(r==1);
|
||||
}
|
||||
|
||||
// container nodes
|
||||
|
||||
const self_type *find_leaf(const key_type &k) const
|
||||
{
|
||||
const containert &c=get_container();
|
||||
|
||||
for(const auto &n : c)
|
||||
{
|
||||
if(key_equal()(n.get_key(), k))
|
||||
return &n;
|
||||
}
|
||||
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
self_type *find_leaf(const key_type &k)
|
||||
{
|
||||
containert &c=get_container();
|
||||
|
||||
for(auto &n : c)
|
||||
{
|
||||
if(key_equal()(n.get_key(), k))
|
||||
return &n;
|
||||
}
|
||||
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
// add leaf, key must not exist yet
|
||||
self_type *place_leaf(const key_type &k, const mapped_type &m)
|
||||
{
|
||||
_sn_assert(as_const(this)->find_leaf(k)==nullptr);
|
||||
|
||||
containert &c=get_container();
|
||||
c.push_back(self_type(k, m));
|
||||
|
||||
return &c.back();
|
||||
}
|
||||
|
||||
// remove leaf, key must exist
|
||||
void remove_leaf(const key_type &k)
|
||||
{
|
||||
containert &c=get_container();
|
||||
|
||||
for(typename containert::const_iterator it=c.begin();
|
||||
it!=c.end(); it++)
|
||||
{
|
||||
const self_type &n=*it;
|
||||
|
||||
if(key_equal()(n.get_key(), k))
|
||||
{
|
||||
c.erase(it);
|
||||
return;
|
||||
}
|
||||
}
|
||||
|
||||
assert(false);
|
||||
}
|
||||
|
||||
// misc
|
||||
|
||||
void clear()
|
||||
{
|
||||
*this=self_type();
|
||||
}
|
||||
|
||||
bool shares_with(const self_type &other) const
|
||||
{
|
||||
return data==other.data;
|
||||
}
|
||||
|
||||
void swap(self_type &other)
|
||||
{
|
||||
data.swap(other.data);
|
||||
}
|
||||
|
||||
protected:
|
||||
class dt
|
||||
{
|
||||
public:
|
||||
dt() {}
|
||||
|
||||
dt(const dt &d) : k(d.k), sub(d.sub), con(d.con)
|
||||
{
|
||||
if(d.is_leaf())
|
||||
{
|
||||
_sn_assert(m==nullptr);
|
||||
m.reset(new mapped_type(*d.m));
|
||||
}
|
||||
}
|
||||
|
||||
bool is_leaf() const
|
||||
{
|
||||
_sn_assert(k==nullptr || m!=nullptr);
|
||||
return k!=nullptr;
|
||||
}
|
||||
|
||||
std::shared_ptr<key_type> k;
|
||||
std::unique_ptr<mapped_type> m;
|
||||
|
||||
subt sub;
|
||||
containert con;
|
||||
};
|
||||
|
||||
const dt &read() const
|
||||
{
|
||||
return *data;
|
||||
}
|
||||
|
||||
dt &write()
|
||||
{
|
||||
detach();
|
||||
return *data;
|
||||
}
|
||||
|
||||
void detach()
|
||||
{
|
||||
_sn_assert(data.use_count()>0);
|
||||
|
||||
if(data==empty_data)
|
||||
data=std::make_shared<dt>();
|
||||
else if(data.use_count()>1)
|
||||
data=std::make_shared<dt>(*data);
|
||||
|
||||
_sn_assert(data.use_count()==1);
|
||||
}
|
||||
|
||||
bool is_well_formed() const
|
||||
{
|
||||
if(data==nullptr)
|
||||
return false;
|
||||
|
||||
const dt &d=*data;
|
||||
|
||||
bool b;
|
||||
|
||||
// empty node
|
||||
b=data==empty_data;
|
||||
// internal node
|
||||
b|=d.k==nullptr && d.m==nullptr && get_container().empty() &&
|
||||
!get_sub().empty();
|
||||
// container node
|
||||
b|=d.k==nullptr && d.m==nullptr && !get_container().empty() &&
|
||||
get_sub().empty();
|
||||
// leaf node
|
||||
b|=d.k!=nullptr && d.m!=nullptr && get_container().empty() &&
|
||||
get_sub().empty();
|
||||
|
||||
return b;
|
||||
}
|
||||
|
||||
std::shared_ptr<dt> data;
|
||||
static std::shared_ptr<dt> empty_data;
|
||||
|
||||
// dummy node returned when node was not found
|
||||
static sharing_nodet dummy;
|
||||
};
|
||||
|
||||
template <class keyT, class valueT, class predT, bool no_sharing>
|
||||
std::shared_ptr<typename sharing_nodet<keyT, valueT, predT, no_sharing>::dt>
|
||||
sharing_nodet<keyT, valueT, predT, no_sharing>::empty_data(
|
||||
new sharing_nodet<keyT, valueT, predT, no_sharing>::dt());
|
||||
|
||||
template <class keyT, class valueT, class predT, bool no_sharing>
|
||||
sharing_nodet<keyT, valueT, predT, no_sharing>
|
||||
sharing_nodet<keyT, valueT, predT, no_sharing>::dummy;
|
||||
|
||||
#endif
|
||||
|
|
@ -1,6 +1,8 @@
|
|||
SRC = cpp_parser.cpp cpp_scanner.cpp elf_reader.cpp float_utils.cpp \
|
||||
ieee_float.cpp json.cpp miniBDD.cpp osx_fat_reader.cpp \
|
||||
smt2_parser.cpp wp.cpp string_utils.cpp
|
||||
smt2_parser.cpp wp.cpp string_utils.cpp \
|
||||
sharing_map.cpp \
|
||||
sharing_node.cpp
|
||||
|
||||
INCLUDES= -I ../src/
|
||||
|
||||
|
|
@ -59,3 +61,9 @@ wp$(EXEEXT): wp$(OBJEXT)
|
|||
string_utils$(EXEEXT): string_utils$(OBJEXT)
|
||||
$(LINKBIN)
|
||||
|
||||
sharing_map$(EXEEXT): sharing_map$(OBJEXT)
|
||||
$(LINKBIN)
|
||||
|
||||
sharing_node$(EXEEXT): sharing_node$(OBJEXT)
|
||||
$(LINKBIN)
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,336 @@
|
|||
#include <iostream>
|
||||
#include <cassert>
|
||||
|
||||
#include <util/sharing_map.h>
|
||||
|
||||
typedef sharing_mapt<irep_idt, std::string, irep_id_hash> smt;
|
||||
|
||||
// helpers
|
||||
void fill(smt &sm)
|
||||
{
|
||||
sm.insert("i", "0");
|
||||
sm.insert("j", "1");
|
||||
sm.insert("k", "2");
|
||||
}
|
||||
|
||||
void fill2(smt &sm)
|
||||
{
|
||||
sm.insert("l", "3");
|
||||
sm.insert("m", "4");
|
||||
sm.insert("n", "5");
|
||||
}
|
||||
|
||||
// tests
|
||||
|
||||
void sharing_map_interface_test()
|
||||
{
|
||||
std::cout << "Running interface test" << std::endl;
|
||||
|
||||
// empty map
|
||||
{
|
||||
smt sm;
|
||||
|
||||
assert(sm.empty());
|
||||
assert(sm.size()==0);
|
||||
assert(!sm.has_key("i"));
|
||||
}
|
||||
|
||||
// insert elements
|
||||
{
|
||||
smt sm;
|
||||
|
||||
smt::const_find_type r1=sm.insert(std::make_pair("i", "0"));
|
||||
assert(r1.second);
|
||||
|
||||
smt::const_find_type r2=sm.insert("j", "1");
|
||||
assert(r2.second);
|
||||
|
||||
smt::const_find_type r3=sm.insert(std::make_pair("i", "0"));
|
||||
assert(!r3.second);
|
||||
|
||||
assert(sm.size()==2);
|
||||
assert(!sm.empty());
|
||||
}
|
||||
|
||||
// place elements
|
||||
{
|
||||
smt sm1;
|
||||
smt sm2(sm1);
|
||||
|
||||
smt::find_type r1=sm1.place("i", "0");
|
||||
assert(r1.second);
|
||||
assert(!sm2.has_key("i"));
|
||||
|
||||
std::string &s1=r1.first;
|
||||
s1="1";
|
||||
|
||||
assert(sm1.at("i")=="1");
|
||||
}
|
||||
|
||||
// retrieve elements
|
||||
{
|
||||
smt sm;
|
||||
sm.insert("i", "0");
|
||||
sm.insert("j", "1");
|
||||
|
||||
const smt &sm2=sm;
|
||||
|
||||
std::string s;
|
||||
s=sm2.at("i");
|
||||
assert(s=="0");
|
||||
|
||||
try {
|
||||
sm2.at("k");
|
||||
assert(false);
|
||||
} catch (...) {}
|
||||
|
||||
s=sm2.at("j");
|
||||
assert(s=="1");
|
||||
|
||||
assert(sm.has_key("i"));
|
||||
assert(sm.has_key("j"));
|
||||
assert(!sm.has_key("k"));
|
||||
|
||||
std::string &s2=sm.at("i");
|
||||
s2="3";
|
||||
assert(sm2.at("i")=="3");
|
||||
|
||||
assert(sm.size()==2);
|
||||
|
||||
smt::find_type r=sm.find("i");
|
||||
assert(r.second);
|
||||
r.first="4";
|
||||
assert(sm2.at("i")=="4");
|
||||
|
||||
smt::const_find_type rc=sm2.find("k");
|
||||
assert(!rc.second);
|
||||
}
|
||||
|
||||
// remove elements
|
||||
{
|
||||
smt sm;
|
||||
sm.insert("i", "0");
|
||||
sm.insert("j", "1");
|
||||
|
||||
assert(sm.erase("k")==0);
|
||||
assert(sm.size()==2);
|
||||
|
||||
assert(sm.erase("i")==1);
|
||||
assert(!sm.has_key("i"));
|
||||
|
||||
assert(sm.erase("j")==1);
|
||||
assert(!sm.has_key("j"));
|
||||
|
||||
sm.insert("i", "0");
|
||||
sm.insert("j", "1");
|
||||
|
||||
smt sm3(sm);
|
||||
|
||||
assert(sm.has_key("i"));
|
||||
assert(sm.has_key("j"));
|
||||
assert(sm3.has_key("i"));
|
||||
assert(sm3.has_key("j"));
|
||||
|
||||
sm.erase("i");
|
||||
|
||||
assert(!sm.has_key("i"));
|
||||
assert(sm.has_key("j"));
|
||||
|
||||
assert(sm3.has_key("i"));
|
||||
assert(sm3.has_key("j"));
|
||||
|
||||
sm3.erase("i");
|
||||
assert(!sm3.has_key("i"));
|
||||
}
|
||||
|
||||
// operator[]
|
||||
{
|
||||
smt sm;
|
||||
|
||||
sm["i"];
|
||||
assert(sm.has_key("i"));
|
||||
|
||||
sm["i"]="0";
|
||||
assert(sm.at("i")=="0");
|
||||
|
||||
sm["j"]="1";
|
||||
assert(sm.at("j")=="1");
|
||||
}
|
||||
}
|
||||
|
||||
void sharing_map_copy_test()
|
||||
{
|
||||
std::cout << "Running copy test" << std::endl;
|
||||
|
||||
smt sm1;
|
||||
const smt &sm2=sm1;
|
||||
|
||||
fill(sm1);
|
||||
|
||||
assert(sm2.find("i").first=="0");
|
||||
assert(sm2.find("j").first=="1");
|
||||
assert(sm2.find("k").first=="2");
|
||||
|
||||
smt sm3=sm1;
|
||||
const smt &sm4=sm3;
|
||||
|
||||
assert(sm3.erase("l")==0);
|
||||
assert(sm3.erase("i")==1);
|
||||
|
||||
assert(!sm4.has_key("i"));
|
||||
sm3.place("i", "3");
|
||||
assert(sm4.find("i").first=="3");
|
||||
}
|
||||
|
||||
class some_keyt
|
||||
{
|
||||
public:
|
||||
some_keyt(size_t s) : s(s)
|
||||
{
|
||||
}
|
||||
|
||||
size_t s;
|
||||
|
||||
bool operator==(const some_keyt &other) const
|
||||
{
|
||||
return s==other.s;
|
||||
}
|
||||
};
|
||||
|
||||
class some_key_hash
|
||||
{
|
||||
public:
|
||||
size_t operator()(const some_keyt &k) const
|
||||
{
|
||||
return k.s & 0x3;
|
||||
}
|
||||
};
|
||||
|
||||
void sharing_map_collision_test()
|
||||
{
|
||||
std::cout << "Running collision test" << std::endl;
|
||||
|
||||
typedef sharing_mapt<some_keyt, std::string, some_key_hash> smt;
|
||||
|
||||
smt sm;
|
||||
|
||||
sm.insert(0, "a");
|
||||
sm.insert(8, "b");
|
||||
sm.insert(16, "c");
|
||||
|
||||
sm.insert(1, "d");
|
||||
sm.insert(2, "e");
|
||||
|
||||
sm.erase(8);
|
||||
|
||||
assert(sm.has_key(0));
|
||||
assert(sm.has_key(16));
|
||||
|
||||
assert(sm.has_key(1));
|
||||
assert(sm.has_key(2));
|
||||
|
||||
assert(!sm.has_key(8));
|
||||
}
|
||||
|
||||
void sharing_map_view_test()
|
||||
{
|
||||
std::cout << "Running view test" << std::endl;
|
||||
|
||||
// view test
|
||||
{
|
||||
smt sm;
|
||||
|
||||
fill(sm);
|
||||
|
||||
smt::viewt view;
|
||||
sm.get_view(view);
|
||||
|
||||
assert(view.size()==3);
|
||||
}
|
||||
|
||||
// delta view test (no sharing, same keys)
|
||||
{
|
||||
smt sm1;
|
||||
fill(sm1);
|
||||
|
||||
smt sm2;
|
||||
fill(sm2);
|
||||
|
||||
smt::delta_viewt delta_view;
|
||||
|
||||
sm1.get_delta_view(sm2, delta_view);
|
||||
assert(delta_view.size()==3);
|
||||
|
||||
delta_view.clear();
|
||||
sm1.get_delta_view(sm2, delta_view, false);
|
||||
assert(delta_view.size()==3);
|
||||
}
|
||||
|
||||
// delta view test (all shared, same keys)
|
||||
{
|
||||
smt sm1;
|
||||
fill(sm1);
|
||||
|
||||
smt sm2(sm1);
|
||||
|
||||
smt::delta_viewt delta_view;
|
||||
|
||||
sm1.get_delta_view(sm2, delta_view);
|
||||
assert(delta_view.size()==0);
|
||||
|
||||
delta_view.clear();
|
||||
sm1.get_delta_view(sm2, delta_view, false);
|
||||
assert(delta_view.size()==0);
|
||||
}
|
||||
|
||||
// delta view test (some sharing, same keys)
|
||||
{
|
||||
smt sm1;
|
||||
fill(sm1);
|
||||
|
||||
smt sm2(sm1);
|
||||
auto r=sm2.find("i");
|
||||
assert(r.second);
|
||||
r.first="3";
|
||||
|
||||
smt::delta_viewt delta_view;
|
||||
|
||||
sm1.get_delta_view(sm2, delta_view);
|
||||
assert(delta_view.size()>0); // not everything is shared
|
||||
assert(delta_view.size()<3); // there is some sharing
|
||||
|
||||
delta_view.clear();
|
||||
sm1.get_delta_view(sm2, delta_view, false);
|
||||
assert(delta_view.size()>0); // not everything is shared
|
||||
assert(delta_view.size()<3); // there is some sharing
|
||||
}
|
||||
|
||||
// delta view test (no sharing, different keys)
|
||||
{
|
||||
smt sm1;
|
||||
fill(sm1);
|
||||
|
||||
smt sm2;
|
||||
fill2(sm2);
|
||||
|
||||
smt::delta_viewt delta_view;
|
||||
|
||||
sm1.get_delta_view(sm2, delta_view);
|
||||
assert(delta_view.size()==0);
|
||||
|
||||
delta_view.clear();
|
||||
sm1.get_delta_view(sm2, delta_view, false);
|
||||
assert(delta_view.size()==3);
|
||||
}
|
||||
}
|
||||
|
||||
int main()
|
||||
{
|
||||
sharing_map_interface_test();
|
||||
sharing_map_copy_test();
|
||||
sharing_map_collision_test();
|
||||
sharing_map_view_test();
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
|
@ -0,0 +1,129 @@
|
|||
#include <iostream>
|
||||
#include <cassert>
|
||||
|
||||
#include <util/sharing_node.h>
|
||||
|
||||
void sharing_node_test()
|
||||
{
|
||||
std::cout << "Running sharing node test" << std::endl;
|
||||
|
||||
typedef sharing_nodet<std::string, std::string> snt;
|
||||
|
||||
// internal node test
|
||||
{
|
||||
snt sn1;
|
||||
const snt &sn2=sn1;
|
||||
|
||||
const snt *p2;
|
||||
|
||||
assert(sn1.is_empty());
|
||||
|
||||
sn1.add_child(0);
|
||||
sn1.add_child(1);
|
||||
sn1.add_child(2);
|
||||
|
||||
assert(!sn2.is_empty());
|
||||
assert(sn2.is_internal());
|
||||
assert(!sn2.is_container());
|
||||
assert(!sn2.is_leaf());
|
||||
|
||||
assert(sn2.get_sub().size()==3);
|
||||
|
||||
p2=sn2.find_child(0);
|
||||
assert(p2!=nullptr);
|
||||
|
||||
p2=sn1.find_child(0);
|
||||
assert(p2!=nullptr);
|
||||
|
||||
p2=sn2.find_child(3);
|
||||
assert(p2==nullptr);
|
||||
|
||||
p2=sn1.find_child(3);
|
||||
assert(p2==nullptr);
|
||||
|
||||
sn1.remove_child(0);
|
||||
assert(sn2.get_sub().size()==2);
|
||||
|
||||
sn1.clear();
|
||||
assert(sn2.is_empty());
|
||||
}
|
||||
|
||||
// container node test
|
||||
{
|
||||
snt sn1;
|
||||
|
||||
snt *p1;
|
||||
const snt *p2;
|
||||
|
||||
sn1.add_child(0);
|
||||
sn1.add_child(1);
|
||||
|
||||
p1=sn1.add_child(2);
|
||||
p2=p1;
|
||||
|
||||
assert(p1->find_leaf("a")==nullptr);
|
||||
assert(p2->find_leaf("a")==nullptr);
|
||||
|
||||
p1->place_leaf("a", "b");
|
||||
assert(p2->get_container().size()==1);
|
||||
p1->place_leaf("c", "d");
|
||||
assert(p2->get_container().size()==2);
|
||||
|
||||
assert(p2->is_container());
|
||||
|
||||
p1->remove_leaf("a");
|
||||
assert(p2->get_container().size()==1);
|
||||
}
|
||||
|
||||
// copy test 1
|
||||
{
|
||||
snt sn1;
|
||||
snt sn2;
|
||||
|
||||
sn2=sn1;
|
||||
assert(sn1.data.use_count()==3);
|
||||
assert(sn2.data.use_count()==3);
|
||||
|
||||
sn1.add_child(0);
|
||||
assert(sn1.data.use_count()==1);
|
||||
// the newly created node is empty as well
|
||||
assert(sn2.data.use_count()==3);
|
||||
|
||||
sn2=sn1;
|
||||
assert(sn2.data.use_count()==2);
|
||||
}
|
||||
|
||||
// copy test 2
|
||||
{
|
||||
snt sn1;
|
||||
const snt &sn1c=sn1;
|
||||
snt *p;
|
||||
|
||||
p=sn1.add_child(0);
|
||||
p->place_leaf("x", "y");
|
||||
|
||||
p=sn1.add_child(1);
|
||||
p->place_leaf("a", "b");
|
||||
p->place_leaf("c", "d");
|
||||
|
||||
snt sn2;
|
||||
const snt &sn2c=sn2;
|
||||
sn2=sn1;
|
||||
|
||||
assert(sn1.is_internal());
|
||||
assert(sn2.is_internal());
|
||||
|
||||
sn1.remove_child(0);
|
||||
assert(sn1c.get_sub().size()==1);
|
||||
|
||||
assert(sn2c.get_sub().size()==2);
|
||||
}
|
||||
}
|
||||
|
||||
int main()
|
||||
{
|
||||
sharing_node_test();
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
||||
Loading…
Reference in New Issue