Skip to content
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

BDD/RelPrev/Renaming (Preliminary Work) #676

Merged
merged 30 commits into from
Jun 22, 2024
Merged
Changes from 1 commit
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
e0d178e
Add missing '_' prefix to '__dd' and 'dd' class member variables and …
SSoelvsten Jun 17, 2024
724d802
Use public member functions rather than being friends of 'dd' class
SSoelvsten Jun 18, 2024
80658fc
Add 'shift_replace' for 'ptr_uint64'
SSoelvsten Jun 18, 2024
710ca6a
Add 'shift_replace' for 'node'
SSoelvsten Jun 18, 2024
fda5b93
Debug 'level_info' and add 'shift_replace(...)'
SSoelvsten Jun 18, 2024
cb5f599
Fix incorrect name of type in 'level_info_stream' according to style …
SSoelvsten Jun 18, 2024
33ee67c
Update 'level_info_stream' to code style
SSoelvsten Jun 18, 2024
448037d
Add missing unit tests for 'level_info_stream'
SSoelvsten Jun 18, 2024
c06456a
Fix incorrect type name according to style guide
SSoelvsten Jun 18, 2024
f7ad53a
Add missing tests and remove duplicated inputs for tests for 'node_st…
SSoelvsten Jun 18, 2024
fdf41b4
Add TODO for better responsibility/performance
SSoelvsten Jun 18, 2024
8503ad8
Fill and Extend comments in <adiar/internal/io/...>
SSoelvsten Jun 18, 2024
511856f
Extend comments in <adiar/internal/dd_func.h> to column 100
SSoelvsten Jun 18, 2024
f038049
Clean-up of code to auto-detect 'replace_type'
SSoelvsten Jun 18, 2024
4a65c22
Swap order of member functions
SSoelvsten Jun 18, 2024
7946159
Clean up 'level_merger' and add missing unit tests
SSoelvsten Jun 18, 2024
c85d24a
Clean up interface of 'comparison_check'
SSoelvsten Jun 18, 2024
6493fa5
Clean up tests for 'bdd_apply'
SSoelvsten Jun 18, 2024
075ca23
Clean up of 'bdd_ite' implementation
SSoelvsten Jun 19, 2024
141db3b
Fix conversion of negated BDD terminal into ZDD throws exception
SSoelvsten Jun 19, 2024
5121d15
Fix descriptions for convert algorithm groups
SSoelvsten Jun 19, 2024
d345743
Add missing unit tests for on-the-fly negation
SSoelvsten Jun 20, 2024
db4c306
Keep Assembler output for 'playground' target to investigate low-leve…
SSoelvsten Jun 21, 2024
88819d4
Make 'shift_replace(const ptr_uint64&)' branchless (Thanks, Lasse!)
SSoelvsten Jun 20, 2024
7899929
Move befriending of 'essential(...)' into a more reasonable place
SSoelvsten Jun 21, 2024
5f30f5a
Add 'cnot(const ptr_uint64&, bool)' for a more branch-less on-the-fly…
SSoelvsten Jun 21, 2024
33b4147
Clean up in tests for 'node' class
SSoelvsten Jun 21, 2024
7cda4ec
Add 'cnot(const node&, bool)' for more branch-less on-the-fly negation
SSoelvsten Jun 21, 2024
af26f39
Extend 'file_stream<>' documentation comments to 100
SSoelvsten Jun 21, 2024
e01d502
Move on-the-fly negation into 'node_stream' and 'node_random_access'
SSoelvsten Jun 21, 2024
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
Prev Previous commit
Next Next commit
Fix conversion of negated BDD terminal into ZDD throws exception
SSoelvsten committed Jun 21, 2024
commit 141db3b138dff8c49058985619ee87cf00099292
4 changes: 1 addition & 3 deletions src/adiar/zdd/zdd.cpp
Original file line number Diff line number Diff line change
@@ -47,9 +47,7 @@ namespace adiar

zdd::zdd(const shared_node_file_type& A, bool negate)
: internal::dd(A, negate)
{
if (negate) { throw invalid_argument("ZDDs cannot be negated"); }
}
{}

zdd::zdd(const zdd& A)
: internal::dd(A)
54 changes: 30 additions & 24 deletions test/adiar/internal/algorithms/test_convert.cpp
Original file line number Diff line number Diff line change
@@ -94,32 +94,18 @@ go_bandit([]() {
});

describe("bdd_from(const zdd&, ForwardIt, ForwardIt)", [&]() {
it("returns F terminal on Ø with dom = Ø", [&]() {
it("returns same file for F terminal on Ø with dom = Ø", [&]() {
__bdd out = bdd_from(zdd_F, dom_empty.begin(), dom_empty.end());

node_test_stream out_nodes(out);

AssertThat(out_nodes.can_pull(), Is().True());
AssertThat(out_nodes.pull(), Is().EqualTo(node(false)));

AssertThat(out_nodes.can_pull(), Is().False());

level_info_test_stream ms(out);
AssertThat(ms.can_pull(), Is().False());
AssertThat(out.get<__bdd::shared_node_file_type>(), Is().EqualTo(zdd_F.file_ptr()));
AssertThat(out._negate, Is().False());
});

it("returns T terminal on { Ø } with dom = Ø", [&]() {
it("returns same file for T terminal on { Ø } with dom = Ø", [&]() {
__bdd out = bdd_from(zdd_T, dom_empty.begin(), dom_empty.end());

node_test_stream out_nodes(out);

AssertThat(out_nodes.can_pull(), Is().True());
AssertThat(out_nodes.pull(), Is().EqualTo(node(true)));

AssertThat(out_nodes.can_pull(), Is().False());

level_info_test_stream ms(out);
AssertThat(ms.can_pull(), Is().False());
AssertThat(out.get<__bdd::shared_node_file_type>(), Is().EqualTo(zdd_T.file_ptr()));
AssertThat(out._negate, Is().False());
});

it("returns F terminal on Ø with dom = { 0,1,2 }", [&]() {
@@ -1161,24 +1147,44 @@ go_bandit([]() {
it("returns Ø on F terminal with dom = Ø", [&]() {
__zdd out = zdd_from(bdd_F, dom_empty.begin(), dom_empty.end());

AssertThat(out.get<__zdd::shared_node_file_type>(), Is().EqualTo(bdd_F.file_ptr()));
AssertThat(out._negate, Is().False());
});

it("returns { Ø } on T terminal with dom = Ø", [&]() {
__zdd out = zdd_from(bdd_T, dom_empty.begin(), dom_empty.end());

AssertThat(out.get<__zdd::shared_node_file_type>(), Is().EqualTo(bdd_T.file_ptr()));
AssertThat(out._negate, Is().False());
});

it("returns Ø on negated F terminal with dom = Ø", [&]() {
__zdd out = zdd_from(bdd_not(bdd_F), dom_empty.begin(), dom_empty.end());

AssertThat(out.get<__zdd::shared_node_file_type>(), Is().EqualTo(bdd_F.file_ptr()));
AssertThat(out._negate, Is().True());

node_test_stream out_nodes(out);

AssertThat(out_nodes.can_pull(), Is().True());
AssertThat(out_nodes.pull(), Is().EqualTo(node(false)));
AssertThat(out_nodes.pull(), Is().EqualTo(node(true)));

AssertThat(out_nodes.can_pull(), Is().False());

level_info_test_stream ms(out);
AssertThat(ms.can_pull(), Is().False());
});

it("returns { Ø } on T terminal with dom = Ø", [&]() {
__zdd out = zdd_from(bdd_T, dom_empty.begin(), dom_empty.end());
it("returns { Ø } on negated T terminal with dom = Ø", [&]() {
__zdd out = zdd_from(bdd_not(bdd_T), dom_empty.begin(), dom_empty.end());

AssertThat(out.get<__zdd::shared_node_file_type>(), Is().EqualTo(bdd_T.file_ptr()));
AssertThat(out._negate, Is().True());

node_test_stream out_nodes(out);

AssertThat(out_nodes.can_pull(), Is().True());
AssertThat(out_nodes.pull(), Is().EqualTo(node(true)));
AssertThat(out_nodes.pull(), Is().EqualTo(node(false)));

AssertThat(out_nodes.can_pull(), Is().False());