Skip to content
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
14 changes: 8 additions & 6 deletions src/adiar/bdd/evaluate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ namespace adiar
inline bdd::pointer_type
visit(const bdd::node_type& n)
{
const bool a = af(n.label());
const bool a = af(n.level());
return a ? n.high() : n.low();
}

Expand Down Expand Up @@ -77,7 +77,7 @@ namespace adiar
inline bdd::pointer_type
visit(const bdd::node_type& n)
{
const bdd::label_type level = n.label();
const bdd::level_type level = n.level();

while (_next_pair.first < level) {
const optional<pair<bdd::label_type, bool>> p = _generator();
Expand Down Expand Up @@ -148,16 +148,17 @@ namespace adiar
visit(const bdd::node_type& n)
{
// Add skipped levels
while (this->_next_domain && this->_next_domain.value() <= n.label()) {
while (this->_next_domain && this->_next_domain.value() <= n.level()) {
const bdd::label_type next_domain = this->_next_domain.value();
if (next_domain != n.label()) {
if (next_domain != n.level()) {
this->_stack.push({ next_domain, !Visitor::default_direction });
}
this->_next_domain = this->_generator();
}
// Update with this level
const bdd::pointer_type next = this->_visitor.visit(n);
this->_stack.push({ n.label(), next == n.low() });
const bdd::level_type level = n.level();
this->_stack.push({ level, next == n.low() });
return next;
}

Expand Down Expand Up @@ -206,7 +207,8 @@ namespace adiar
visit(const bdd::node_type& n)
{
const bdd::pointer_type next = this->_visitor.visit(n);
this->_consumer({ n.label(), next == n.high() });
const bdd::level_type level = n.level();
this->_consumer({ level, next == n.high() });
return next;
}

Expand Down
38 changes: 19 additions & 19 deletions src/adiar/bdd/if_then_else.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -116,13 +116,13 @@ namespace adiar
inline bool
ite_must_forward(internal::node v,
internal::node::pointer_type t,
internal::node::label_type out_label,
internal::node::level_type out_level,
internal::node::pointer_type t_seek)
{
return
// is it a node at this level?
t.is_node()
&& t.label() == out_label
&& t.level() == out_level
// and we should be seeing it later
&& t_seek < t
// and we haven't by accident just run into it anyway
Expand All @@ -132,11 +132,11 @@ namespace adiar
inline void
ite_init_request(internal::node_ifstream<>& in_nodes,
internal::node& v,
const internal::node::label_type out_label,
const internal::node::level_type out_level,
internal::node::pointer_type& low,
internal::node::pointer_type& high)
{
if (v.label() == out_label) {
if (v.level() == out_level) {
low = v.low();
high = v.high();

Expand Down Expand Up @@ -220,26 +220,26 @@ namespace adiar

// Process root and create initial recursion requests
{
const bdd::label_type out_label = first(v_if.uid(), v_then.uid(), v_else.uid()).label();
const bdd::level_type out_level = first(v_if.uid(), v_then.uid(), v_else.uid()).level();

bdd::pointer_type low_if, low_then, low_else, high_if, high_then, high_else;
ite_init_request(in_nodes_if, v_if, out_label, low_if, high_if);
ite_init_request(in_nodes_then, v_then, out_label, low_then, high_then);
ite_init_request(in_nodes_else, v_else, out_label, low_else, high_else);
ite_init_request(in_nodes_if, v_if, out_level, low_if, high_if);
ite_init_request(in_nodes_then, v_then, out_level, low_then, high_then);
ite_init_request(in_nodes_else, v_else, out_level, low_else, high_else);

const bdd::node_type::uid_type out_uid(out_label, 0);
const bdd::node_type::uid_type out_uid(out_level, 0);
__ite_resolve_request(pq_1, aw, out_uid.as_ptr(false), low_if, low_then, low_else);
__ite_resolve_request(pq_1, aw, out_uid.as_ptr(true), high_if, high_then, high_else);

aw.push(internal::level_info(out_label, 1));
aw.push(internal::level_info(out_level, 1));
}

// Process all nodes in topological order of both BDDs
while (!pq_1.empty()) {
// Set up next level
pq_1.setup_next_level();

const bdd::label_type out_label = pq_1.current_level();
const bdd::level_type out_level = pq_1.current_level();
bdd::id_type out_id = 0;

// Update max 1-level cut
Expand Down Expand Up @@ -290,9 +290,9 @@ namespace adiar
while (v_else.uid() < t_seek && in_nodes_else.can_pull()) { v_else = in_nodes_else.pull(); }

// Forward information across the level
if (ite_must_forward(v_if, req.target[0], out_label, t_seek)
|| ite_must_forward(v_then, req.target[1], out_label, t_seek)
|| ite_must_forward(v_else, req.target[2], out_label, t_seek)) {
if (ite_must_forward(v_if, req.target[0], out_level, t_seek)
|| ite_must_forward(v_then, req.target[1], out_level, t_seek)
|| ite_must_forward(v_else, req.target[2], out_level, t_seek)) {
// An element should be forwarded, if it was not already forwarded (t_seek <= t_x), if it
// isn't the last one to seek (t_x < t_third), and if we actually are holding it.
const bool forward_if =
Expand Down Expand Up @@ -358,15 +358,15 @@ namespace adiar
// Recreate nodes from priority queue carries
bdd::pointer_type low_if, low_then, low_else, high_if, high_then, high_else;

if (req.target[0].is_terminal() || out_label < req.target[0].label()) {
if (req.target[0].is_terminal() || out_level < req.target[0].level()) {
low_if = high_if = req.target[0];
} else {
low_if = req.target[0] == v_if.uid() ? v_if.low() : req.node_carry[0][false];
high_if = req.target[0] == v_if.uid() ? v_if.high() : req.node_carry[0][true];
}

if (req.target[1].is_nil() || req.target[1].is_terminal()
|| out_label < req.target[1].label()) {
|| out_level < req.target[1].level()) {
low_then = high_then = req.target[1];
} else if (req.target[1] == v_then.uid()) {
low_then = v_then.low();
Expand All @@ -380,7 +380,7 @@ namespace adiar
}

if (req.target[2].is_nil() || req.target[2].is_terminal()
|| out_label < req.target[2].label()) {
|| out_level < req.target[2].level()) {
low_else = high_else = req.target[2];
} else if (req.target[2] == v_else.uid()) {
low_else = v_else.low();
Expand All @@ -395,7 +395,7 @@ namespace adiar

// Resolve request
adiar_assert(out_id < bdd::max_id, "Has run out of ids");
const bdd::node_type::uid_type out_uid(out_label, out_id++);
const bdd::node_type::uid_type out_uid(out_level, out_id++);

__ite_resolve_request(pq_1, aw, out_uid.as_ptr(false), low_if, low_then, low_else);
__ite_resolve_request(pq_1, aw, out_uid.as_ptr(true), high_if, high_then, high_else);
Expand All @@ -422,7 +422,7 @@ namespace adiar
}

// Push meta data about this level
aw.push(internal::level_info(out_label, out_id));
aw.push(internal::level_info(out_level, out_id));
}

return __bdd(out_arcs, ep);
Expand Down
10 changes: 5 additions & 5 deletions src/adiar/bdd/relprod.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,10 @@ namespace adiar

public:
void
setup_next_level(const bdd::label_type next_level)
setup_next_level(const bdd::level_type next_level)
{
using result_type = typename LevelPredicate::result_type;
constexpr bool is_total_map = is_convertible<result_type, label_type>;
constexpr bool is_total_map = is_convertible<result_type, level_type>;

if constexpr (is_total_map) {
this->_prune_level = this->_pred(next_level);
Expand Down Expand Up @@ -272,10 +272,10 @@ namespace adiar
////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief Variable remapping of.
////////////////////////////////////////////////////////////////////////////////////////////////
inline bdd::label_type
map_level(bdd::label_type x) const
inline bdd::level_type
map_level(bdd::level_type x) const
{
const optional<bdd::label_type> new_x = this->_m(x);
const optional<bdd::level_type> new_x = this->_m(x);
return new_x.has_value() ? new_x.value() : bdd::max_label + 1;
}

Expand Down
4 changes: 2 additions & 2 deletions src/adiar/builder.h
Original file line number Diff line number Diff line change
Expand Up @@ -250,10 +250,10 @@ namespace adiar
}
if (label > Policy::max_label) { throw invalid_argument("Nodes must have a valid label"); }
if (label > current_label) { throw invalid_argument("Nodes must be added bottom-up"); }
if (low.uid.is_node() && low.uid.label() <= label) {
if (low.uid.is_node() && low.uid.level() <= label) {
throw invalid_argument("Low child must point to a node with higher label");
}
if (high.uid.is_node() && high.uid.label() <= label) {
if (high.uid.is_node() && high.uid.level() <= label) {
throw invalid_argument("High child must point to a node with higher label");
}

Expand Down
2 changes: 1 addition & 1 deletion src/adiar/domain.h
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ namespace adiar
//////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief The variable type of a domain variable.
//////////////////////////////////////////////////////////////////////////////////////////////////
using domain_var = internal::node::label_type;
using domain_var = internal::node::level_type;

//////////////////////////////////////////////////////////////////////////////////////////////////
/// \brief The maximum supported domain variable.
Expand Down
46 changes: 23 additions & 23 deletions src/adiar/internal/algorithms/build.h
Original file line number Diff line number Diff line change
Expand Up @@ -38,20 +38,20 @@ namespace adiar::internal
//////////////////////////////////////////////////////////////////////////////
template <typename DdPolicy>
inline shared_levelized_file<typename DdPolicy::node_type>
build_ithvar(typename DdPolicy::label_type label)
build_ithvar(typename DdPolicy::level_type level)
{
using node_type = typename DdPolicy::node_type;
using pointer_type = typename node_type::pointer_type;

if (node_type::max_label < label) {
throw invalid_argument("Cannot represent that large a label");
if (node_type::max_label < level) {
throw invalid_argument("Cannot represent that large a level");
}

shared_levelized_file<node_type> nf;
{
node_ofstream nw(nf);
nw.unsafe_push(node(label, pointer_type::max_id, pointer_type(false), pointer_type(true)));
nw.unsafe_push(level_info(label, 1u));
nw.unsafe_push(node(level, pointer_type::max_id, pointer_type(false), pointer_type(true)));
nw.unsafe_push(level_info(level, 1u));
nw.unsafe_set_canonical(true);
}

Expand All @@ -65,9 +65,9 @@ namespace adiar::internal
inline typename Policy::dd_type
build_chain(const Policy& policy, const Generator& vars)
{
using label_type = typename Policy::label_type;
using level_type = typename Policy::level_type;

optional<pair<label_type, bool>> next = vars();
optional<pair<level_type, bool>> next = vars();

if (!next) { return build_terminal<Policy>(Policy::init_terminal); }

Expand All @@ -84,16 +84,16 @@ namespace adiar::internal
adiar_assert(root.is_terminal());

do {
const label_type next_var = next.value().first;
const label_type next_negated = next.value().second;
const level_type next_var = next.value().first;
const level_type next_negated = next.value().second;

// Fail if generator is increasing.
if (!root.is_terminal() && root.label() < next_var) {
throw invalid_argument("Labels not given in decreasing order");
if (!root.is_terminal() && root.level() < next_var) {
throw invalid_argument("Levels not given in decreasing order");
}

// Skip value if generator provides the same (legal) value twice.
if (!root.is_terminal() && root.label() == next_var) {
if (!root.is_terminal() && root.level() == next_var) {
next = vars();
continue;
}
Expand All @@ -104,14 +104,14 @@ namespace adiar::internal
continue;
}

// TODO: throw exception for too large labels
// TODO: throw exception for too large levels

// Create node on chain.
using node_type = typename Policy::node_type;

const node_type n = policy.make_node(next_var, root, next_negated);

adiar_assert(n.label() == next_var, "Policy ought to make a node for this level node");
adiar_assert(n.level() == next_var, "Policy ought to make a node for this level node");
adiar_assert(n.id() == node_type::max_id, "Policy ought to make a canonical node");

max_internal_cut = std::max<size_t>(max_internal_cut, n.low().is_node() + n.high().is_node());
Expand Down Expand Up @@ -140,7 +140,7 @@ namespace adiar::internal

root = n.uid();

// Get next label
// Get next level
next = vars();
} while (next);

Expand Down Expand Up @@ -183,13 +183,13 @@ namespace adiar::internal
static constexpr bool init_terminal = InitTerminal;

constexpr bool
skip(const typename DdPolicy::label_type&) const
skip(const typename DdPolicy::level_type&) const
{
return false;
}

inline typename DdPolicy::node_type
make_node(const typename DdPolicy::label_type& l,
make_node(const typename DdPolicy::level_type& l,
const typename DdPolicy::pointer_type& r,
const bool /*negated*/) const
{
Expand All @@ -208,13 +208,13 @@ namespace adiar::internal
static constexpr bool init_terminal = InitTerminal;

constexpr bool
skip(const typename DdPolicy::label_type&) const
skip(const typename DdPolicy::level_type&) const
{
return false;
}

inline typename DdPolicy::node_type
make_node(const typename DdPolicy::label_type& l,
make_node(const typename DdPolicy::level_type& l,
const typename DdPolicy::pointer_type& r,
const bool /*negated*/) const
{
Expand All @@ -234,13 +234,13 @@ namespace adiar::internal
static constexpr bool init_terminal = InitTerminal;

constexpr bool
skip(const typename DdPolicy::label_type&) const
skip(const typename DdPolicy::level_type&) const
{
return false;
}

inline typename DdPolicy::node_type
make_node(const typename DdPolicy::label_type& l,
make_node(const typename DdPolicy::level_type& l,
const typename DdPolicy::pointer_type& r,
const bool /*negated*/) const
{
Expand All @@ -259,7 +259,7 @@ namespace adiar::internal
const Generator& _gen;

public:
using value_type = pair<typename DdPolicy::label_type, bool>;
using value_type = pair<typename DdPolicy::level_type, bool>;
using result_type = optional<value_type>;

private:
Expand All @@ -270,7 +270,7 @@ namespace adiar::internal
}

inline value_type
map(const typename DdPolicy::label_type& x) const
map(const typename DdPolicy::level_type& x) const
{
return make_pair(x, negate);
}
Expand Down
Loading
Loading