Skip to content

irept: Use singly-linked lists with SUB_IS_LIST [depends on: #3606] #2035

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Dec 20, 2018
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
64 changes: 48 additions & 16 deletions src/util/irep.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
#include "string_hash.h"
#include "irep_hash.h"

#ifdef SUB_IS_LIST
#ifdef NAMED_SUB_IS_FORWARD_LIST
#include <algorithm>
#endif

Expand All @@ -31,7 +31,7 @@ irept nil_rep_storage;
irept::dt irept::empty_d;
#endif

#ifdef SUB_IS_LIST
#ifdef NAMED_SUB_IS_FORWARD_LIST
static inline bool named_subt_order(
const std::pair<irep_namet, irept> &a,
const irep_namet &b)
Expand Down Expand Up @@ -152,9 +152,9 @@ void irept::nonrecursive_destructor(dt *old_data)

if(d->ref_count==0)
{
stack.reserve(stack.size()+
d->named_sub.size()+
d->sub.size());
stack.reserve(
stack.size() + std::distance(d->named_sub.begin(), d->named_sub.end()) +
d->sub.size());

for(named_subt::iterator
it=d->named_sub.begin();
Expand Down Expand Up @@ -203,7 +203,7 @@ const irep_idt &irept::get(const irep_namet &name) const
{
const named_subt &s = get_named_sub();

#ifdef SUB_IS_LIST
#ifdef NAMED_SUB_IS_FORWARD_LIST
named_subt::const_iterator it=named_subt_lower_bound(s, name);

if(it==s.end() ||
Expand Down Expand Up @@ -259,11 +259,16 @@ void irept::remove(const irep_namet &name)
{
named_subt &s = get_named_sub();

#ifdef SUB_IS_LIST
#ifdef NAMED_SUB_IS_FORWARD_LIST
named_subt::iterator it=named_subt_lower_bound(s, name);

if(it!=s.end() && it->first==name)
s.erase(it);
{
named_subt::iterator before = s.before_begin();
while(std::next(before) != it)
++before;
s.erase_after(before);
}
#else
s.erase(name);
#endif
Expand All @@ -273,7 +278,7 @@ const irept &irept::find(const irep_namet &name) const
{
const named_subt &s = get_named_sub();

#ifdef SUB_IS_LIST
#ifdef NAMED_SUB_IS_FORWARD_LIST
named_subt::const_iterator it=named_subt_lower_bound(s, name);

if(it==s.end() ||
Expand All @@ -293,12 +298,17 @@ irept &irept::add(const irep_namet &name)
{
named_subt &s = get_named_sub();

#ifdef SUB_IS_LIST
#ifdef NAMED_SUB_IS_FORWARD_LIST
named_subt::iterator it=named_subt_lower_bound(s, name);

if(it==s.end() ||
it->first!=name)
it=s.insert(it, std::make_pair(name, irept()));
{
named_subt::iterator before = s.before_begin();
while(std::next(before) != it)
++before;
it = s.emplace_after(before, name, irept());
}

return it->second;
#else
Expand All @@ -310,12 +320,17 @@ irept &irept::add(const irep_namet &name, const irept &irep)
{
named_subt &s = get_named_sub();

#ifdef SUB_IS_LIST
#ifdef NAMED_SUB_IS_FORWARD_LIST
named_subt::iterator it=named_subt_lower_bound(s, name);

if(it==s.end() ||
it->first!=name)
it=s.insert(it, std::make_pair(name, irep));
{
named_subt::iterator before = s.before_begin();
while(std::next(before) != it)
++before;
it = s.emplace_after(before, name, irep);
}
else
it->second=irep;

Expand Down Expand Up @@ -407,13 +422,24 @@ bool irept::full_eq(const irept &other) const

const irept::subt &i1_sub=get_sub();
const irept::subt &i2_sub=other.get_sub();

if(i1_sub.size() != i2_sub.size())
return false;

const irept::named_subt &i1_named_sub=get_named_sub();
const irept::named_subt &i2_named_sub=other.get_named_sub();

#ifdef NAMED_SUB_IS_FORWARD_LIST
if(
i1_sub.size() != i2_sub.size() ||
i1_named_sub.size() != i2_named_sub.size())
std::distance(i1_named_sub.begin(), i1_named_sub.end()) !=
std::distance(i2_named_sub.begin(), i2_named_sub.end()))
{
return false;
}
#else
if(i1_named_sub.size() != i2_named_sub.size())
return false;
#endif

for(std::size_t i=0; i<i1_sub.size(); i++)
if(!i1_sub[i].full_eq(i2_sub[i]))
Expand Down Expand Up @@ -667,7 +693,13 @@ std::size_t irept::full_hash() const
result=hash_combine(result, it->second.full_hash());
}

result = hash_finalize(result, named_sub.size() + sub.size());
#ifdef NAMED_SUB_IS_FORWARD_LIST
const std::size_t named_sub_size =
std::distance(named_sub.begin(), named_sub.end());
#else
const std::size_t named_sub_size = named_sub.size();
#endif
result = hash_finalize(result, named_sub_size + sub.size());

return result;
}
Expand Down
14 changes: 7 additions & 7 deletions src/util/irep.h
Original file line number Diff line number Diff line change
Expand Up @@ -20,10 +20,10 @@ Author: Daniel Kroening, [email protected]
#define SHARING
// #define HASH_CODE
#define USE_MOVE
// #define SUB_IS_LIST
// #define NAMED_SUB_IS_FORWARD_LIST

#ifdef SUB_IS_LIST
#include <list>
#ifdef NAMED_SUB_IS_FORWARD_LIST
#include <forward_list>
#else
#include <map>
#endif
Expand Down Expand Up @@ -160,11 +160,11 @@ class irept
// use std::forward_list or std::vector< unique_ptr<T> > to save
// memory and increase efficiency.

#ifdef SUB_IS_LIST
typedef std::list<std::pair<irep_namet, irept> > named_subt;
#else
#ifdef NAMED_SUB_IS_FORWARD_LIST
typedef std::forward_list<std::pair<irep_namet, irept>> named_subt;
#else
typedef std::map<irep_namet, irept> named_subt;
#endif
#endif

bool is_nil() const { return id()==ID_nil; }
bool is_not_nil() const { return id()!=ID_nil; }
Expand Down
10 changes: 8 additions & 2 deletions src/util/irep_hash_container.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -54,15 +54,21 @@ void irep_hash_container_baset::pack(
{
// we pack: the irep id, the sub size, the subs, the named-sub size, and
// each of the named subs with their ids
packed.reserve(1 + 1 + sub.size() + 1 + named_sub.size() * 2);
#ifdef NAMED_SUB_IS_FORWARD_LIST
const std::size_t named_sub_size =
std::distance(named_sub.begin(), named_sub.end());
#else
const std::size_t named_sub_size = named_sub.size();
#endif
packed.reserve(1 + 1 + sub.size() + 1 + named_sub_size * 2);

packed.push_back(irep_id_hash()(irep.id()));

packed.push_back(sub.size());
forall_irep(it, sub)
packed.push_back(number(*it));

packed.push_back(named_sub.size());
packed.push_back(named_sub_size);
for(const auto &sub_irep : named_sub)
{
packed.push_back(irep_id_hash()(sub_irep.first)); // id
Expand Down
8 changes: 7 additions & 1 deletion src/util/lispirep.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,13 @@ void irep2lisp(const irept &src, lispexprt &dest)
dest.value="";
dest.type=lispexprt::List;

dest.reserve(2 + 2 * src.get_sub().size() + 2 * src.get_named_sub().size());
#ifdef NAMED_SUB_IS_FORWARD_LIST
const std::size_t named_sub_size =
std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
#else
const std::size_t named_sub_size = src.get_named_sub().size();
#endif
dest.reserve(2 + 2 * src.get_sub().size() + 2 * named_sub_size);

lispexprt id;
id.type=lispexprt::String;
Expand Down
65 changes: 49 additions & 16 deletions src/util/merge_irep.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,13 @@ std::size_t to_be_merged_irept::hash() const
result, static_cast<const merged_irept &>(it->second).hash());
}

result=hash_finalize(result, named_sub.size()+sub.size());
#ifdef NAMED_SUB_IS_FORWARD_LIST
const std::size_t named_sub_size =
std::distance(named_sub.begin(), named_sub.end());
#else
const std::size_t named_sub_size = named_sub.size();
#endif
result = hash_finalize(result, named_sub_size + sub.size());

return result;
}
Expand All @@ -45,8 +51,17 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const

if(sub.size()!=o_sub.size())
return false;
#ifdef NAMED_SUB_IS_FORWARD_LIST
if(
std::distance(named_sub.begin(), named_sub.end()) !=
std::distance(o_named_sub.begin(), o_named_sub.end()))
{
return false;
}
#else
if(named_sub.size()!=o_named_sub.size())
return false;
#endif

{
irept::subt::const_iterator s_it=sub.begin();
Expand Down Expand Up @@ -95,13 +110,19 @@ const merged_irept &merged_irepst::merged(const irept &irep)
const irept::named_subt &src_named_sub=irep.get_named_sub();
irept::named_subt &dest_named_sub=new_irep.get_named_sub();

#ifdef NAMED_SUB_IS_FORWARD_LIST
irept::named_subt::iterator before = dest_named_sub.before_begin();
#endif
forall_named_irep(it, src_named_sub)
#ifdef SUB_IS_LIST
dest_named_sub.push_back(
std::make_pair(it->first, merged(it->second))); // recursive call
#else
{
#ifdef NAMED_SUB_IS_FORWARD_LIST
dest_named_sub.emplace_after(
before, it->first, merged(it->second)); // recursive call
++before;
#else
dest_named_sub[it->first]=merged(it->second); // recursive call
#endif
#endif
}

std::pair<to_be_merged_irep_storet::const_iterator, bool> result=
to_be_merged_irep_store.insert(to_be_merged_irept(new_irep));
Expand Down Expand Up @@ -140,13 +161,19 @@ const irept &merge_irept::merged(const irept &irep)
const irept::named_subt &src_named_sub=irep.get_named_sub();
irept::named_subt &dest_named_sub=new_irep.get_named_sub();

#ifdef NAMED_SUB_IS_FORWARD_LIST
irept::named_subt::iterator before = dest_named_sub.before_begin();
#endif
forall_named_irep(it, src_named_sub)
#ifdef SUB_IS_LIST
dest_named_sub.push_back(
std::make_pair(it->first, merged(it->second))); // recursive call
#else
{
#ifdef NAMED_SUB_IS_FORWARD_LIST
dest_named_sub.emplace_after(
before, it->first, merged(it->second)); // recursive call
++before;
#else
dest_named_sub[it->first]=merged(it->second); // recursive call
#endif
#endif
}

return *irep_store.insert(std::move(new_irep)).first;
}
Expand Down Expand Up @@ -177,13 +204,19 @@ const irept &merge_full_irept::merged(const irept &irep)
const irept::named_subt &src_named_sub=irep.get_named_sub();
irept::named_subt &dest_named_sub=new_irep.get_named_sub();

#ifdef NAMED_SUB_IS_FORWARD_LIST
irept::named_subt::iterator before = dest_named_sub.before_begin();
#endif
forall_named_irep(it, src_named_sub)
#ifdef SUB_IS_LIST
dest_named_sub.push_back(
std::make_pair(it->first, merged(it->second))); // recursive call
#else
{
#ifdef NAMED_SUB_IS_FORWARD_LIST
dest_named_sub.emplace_after(
before, it->first, merged(it->second)); // recursive call
++before;
#else
dest_named_sub[it->first]=merged(it->second); // recursive call
#endif
#endif
}

return *irep_store.insert(std::move(new_irep)).first;
}
26 changes: 18 additions & 8 deletions unit/util/irep.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ SCENARIO("irept_memory", "[core][utils][irept]")
REQUIRE(sizeof(std::vector<int>) == 3 * sizeof(void *));
#endif

#ifndef SUB_IS_LIST
#ifndef NAMED_SUB_IS_FORWARD_LIST
const std::size_t named_size = sizeof(std::map<int, int>);
# ifndef _GLIBCXX_DEBUG
# ifdef __APPLE__
Expand All @@ -47,9 +47,9 @@ SCENARIO("irept_memory", "[core][utils][irept]")
# endif
# endif
#else
const std::size_t named_size = sizeof(std::list<int>);
const std::size_t named_size = sizeof(std::forward_list<int>);
# ifndef _GLIBCXX_DEBUG
REQUIRE(sizeof(std::list<int>) == 3 * sizeof(void *));
REQUIRE(sizeof(std::forward_list<int>) == sizeof(void *));
# endif
#endif

Expand Down Expand Up @@ -140,12 +140,16 @@ SCENARIO("irept_memory", "[core][utils][irept]")
irep.add("a_new_element", irep2);
REQUIRE(!irept::is_comment("a_new_element"));
REQUIRE(irep.find("a_new_element").id() == "second_irep");
REQUIRE(irep.get_named_sub().size() == 1);
std::size_t named_sub_size =
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
REQUIRE(named_sub_size == 1);

irep.add("#a_comment", irep2);
REQUIRE(irept::is_comment("#a_comment"));
REQUIRE(irep.find("#a_comment").id() == "second_irep");
REQUIRE(irep.get_named_sub().size() == 2);
named_sub_size =
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
REQUIRE(named_sub_size == 2);
REQUIRE(irept::number_of_non_comments(irep.get_named_sub()) == 1);

irept bak(irep);
Expand All @@ -160,17 +164,23 @@ SCENARIO("irept_memory", "[core][utils][irept]")

irep.move_to_named_sub("another_entry", irep2);
REQUIRE(irep.get_sub().size() == 1);
REQUIRE(irep.get_named_sub().size() == 2);
named_sub_size =
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
REQUIRE(named_sub_size == 2);

irept irep3;
irep.move_to_named_sub("#a_comment", irep3);
REQUIRE(irep.find("#a_comment").id().empty());
REQUIRE(irep.get_sub().size() == 1);
REQUIRE(irep.get_named_sub().size() == 2);
named_sub_size =
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
REQUIRE(named_sub_size == 2);

irept irep4;
irep.move_to_named_sub("#another_comment", irep4);
REQUIRE(irep.get_named_sub().size() == 3);
named_sub_size =
std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
REQUIRE(named_sub_size == 3);
}

THEN("Setting and getting works")
Expand Down