Skip to content

Commit

Permalink
Use transposed result of 'bdd_and' in 'bdd_exist' for Relational Product
Browse files Browse the repository at this point in the history
  • Loading branch information
@SSoelvsten
SSoelvsten committed Jun 13, 2024
1 parent d678643 commit 1923c68
Show file tree
Hide file tree
Showing 2 changed files with 46 additions and 26 deletions.
12 changes: 6 additions & 6 deletions src/adiar/bdd/relprod.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,13 +28,13 @@ namespace adiar
const function<optional<bdd::label_type>(bdd::label_type)>& m,
replace_type m_type)
{
const bdd tmp_1 = bdd_and(ep, states, relation);
__bdd tmp_1 = bdd_and(ep, states, relation);

const bdd tmp_2 =
bdd_exists(ep, std::move(tmp_1), [&m](bdd::label_type x) { return !m(x).has_value(); });

const bdd tmp_3 =
bdd_replace(ep, std::move(tmp_2), [&m](bdd::label_type x) { return m(x).value(); }, m_type);
const bdd tmp_3 = bdd_replace(
ep, std::move(tmp_2), [&m](bdd::label_type x) { return m(x).value(); }, m_type);

return tmp_3;
}
Expand Down Expand Up @@ -77,10 +77,10 @@ namespace adiar
const function<optional<bdd::label_type>(bdd::label_type)>& m,
replace_type m_type)
{
const bdd tmp_1 =
bdd_replace(ep, states, [&m](bdd::label_type x) { return m(x).value(); }, m_type);
const bdd tmp_1 = bdd_replace(
ep, states, [&m](bdd::label_type x) { return m(x).value(); }, m_type);

const bdd tmp_2 = bdd_and(ep, std::move(tmp_1), relation);
__bdd tmp_2 = bdd_and(ep, std::move(tmp_1), relation);

const bdd tmp_3 =
bdd_exists(ep, std::move(tmp_2), [&m](bdd::label_type x) { return !m(x).has_value(); });
Expand Down
60 changes: 40 additions & 20 deletions test/adiar/bdd/test_relprod.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1139,12 +1139,14 @@ go_bandit([]() {
AssertThat(out->width, Is().EqualTo(1u));

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

Expand Down Expand Up @@ -1197,12 +1199,14 @@ go_bandit([]() {
AssertThat(out->width, Is().EqualTo(1u));

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

Expand Down Expand Up @@ -2325,12 +2329,14 @@ go_bandit([]() {

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->number_of_terminals[false], Is().EqualTo(1u));
Expand Down Expand Up @@ -2388,12 +2394,14 @@ go_bandit([]() {

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->number_of_terminals[false], Is().EqualTo(1u));
Expand Down Expand Up @@ -4359,12 +4367,14 @@ go_bandit([]() {
AssertThat(out->width, Is().EqualTo(1u));

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

Expand Down Expand Up @@ -4401,12 +4411,14 @@ go_bandit([]() {
AssertThat(out->width, Is().EqualTo(1u));

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

Expand Down Expand Up @@ -4847,12 +4859,14 @@ go_bandit([]() {

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->number_of_terminals[false], Is().EqualTo(1u));
Expand Down Expand Up @@ -4889,12 +4903,14 @@ go_bandit([]() {

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->number_of_terminals[false], Is().EqualTo(1u));
Expand Down Expand Up @@ -5274,12 +5290,14 @@ go_bandit([]() {
AssertThat(out->width, Is().EqualTo(1u));

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

Expand Down Expand Up @@ -5598,12 +5616,14 @@ go_bandit([]() {

AssertThat(out->max_1level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_1level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_1level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->max_2level_cut[cut::Internal], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_False], Is().EqualTo(1u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().EqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().GreaterThanOrEqualTo(2u));
AssertThat(out->max_2level_cut[cut::Internal_True], Is().LessThanOrEqualTo(3u));
AssertThat(out->max_2level_cut[cut::All], Is().EqualTo(3u));

AssertThat(out->number_of_terminals[false], Is().EqualTo(1u));
Expand Down

0 comments on commit 1923c68

Please sign in to comment.