BDD/RelPrev/Renaming (Preliminary Work)

makefile

@@ -156,6 +156,9 @@ test/adiar/internal/data_types/arc:
 test/adiar/internal/data_types/convert:
 	$(MAKE) $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/internal/data_types TEST_NAME=convert
 
+test/adiar/internal/data_types/level_info:
+	$(MAKE) $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/internal/data_types TEST_NAME=level_info
+
 test/adiar/internal/data_types/node:
 	$(MAKE) $(MAKE_FLAGS) test TEST_FOLDER=test/adiar/internal/data_types TEST_NAME=node
 

src/CMakeLists.txt

@@ -4,3 +4,8 @@ add_subdirectory (adiar)
 # Setup MAIN target
 add_executable (adiar_playground playground.cpp)
 target_link_libraries(adiar_playground adiar)
+
+# Dump assembly output too (if GCC)
+if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
+  set_target_properties(adiar_playground PROPERTIES COMPILE_FLAGS "-save-temps")
+endif ()

src/adiar/bdd/bdd.cpp

@@ -77,8 +77,8 @@ namespace adiar
   bdd&
   bdd::operator=(const bdd& other)
   {
-    this->negate = other.negate;
-    this->file   = other.file;
+    this->_negate = other._negate;
+    this->_file   = other._file;
     return *this;
   }
 

src/adiar/bdd/negate.cpp

@@ -7,15 +7,15 @@ namespace adiar
   bdd
   bdd_not(const bdd& in)
   {
-    bdd out    = in;
-    out.negate = !in.negate;
+    bdd out     = in;
+    out._negate = !in._negate;
     return out;
   }
 
   bdd
   bdd_not(bdd&& b)
   {
-    b.negate = !b.negate;
+    b._negate = !b._negate;
     return std::move(b);
   }
 }

src/adiar/internal/algorithms/convert.h

@@ -47,7 +47,7 @@ namespace adiar::internal
     static typename to_policy::dd_type
     on_empty_labels(const typename from_policy::dd_type& dd)
     {
-      return typename to_policy::dd_type(dd.file, dd.negate);
+      return typename to_policy::dd_type(dd.file_ptr(), dd.is_negated());
     }
 
     static typename to_policy::dd_type
@@ -80,8 +80,8 @@ namespace adiar::internal
           nw.unsafe_push(next_node);
           nw.unsafe_push(level_info(next_label, 1u));
         } else {
-          // If we kill the resulting node once, then we will also do it for all
-          // the other labels we still are missing.
+          // If we kill the resulting node once, then we will also do it for all the other labels we
+          // still are missing.
           has_output = false;
           break;
         }

src/adiar/internal/algorithms/nested_sweeping.h

@@ -2095,13 +2095,13 @@ namespace adiar::internal
     // Is it a terminal?
     if (input.template has<shared_node_file_type>()
         && input.template get<shared_node_file_type>()->is_terminal()) {
-      return reduced_t(input.template get<shared_node_file_type>(), input.negate);
+      return reduced_t(input.template get<shared_node_file_type>(), input._negate);
     }
 
     // Otherwise obtain the semi-transposed DAG (construct it if necessary)
     const shared_arc_file_type dag = input.template has<shared_arc_file_type>()
       ? input.template get<shared_arc_file_type>()
-      : transpose(reduced_t(input.template get<shared_node_file_type>(), input.negate));
+      : transpose(reduced_t(input.template get<shared_node_file_type>(), input._negate));
 
     // Compute amount of memory available for auxiliary data structures after having opened all
     // streams.

src/adiar/internal/algorithms/pred.cpp

@@ -9,14 +9,13 @@ namespace adiar::internal
 {
   statistics::equality_t stats_equality;
 
-  //////////////////////////////////////////////////////////////////////////////
-  // Slow O(sort(N)) I/Os comparison by traversing the product construction and
-  // comparing each related pair of nodes.
-
-  //////////////////////////////////////////////////////////////////////////////
-  // Check whether more requests were processed on this level than allowed. An
-  // isomorphic DAG would not create more requests than the original number of
-  // nodes.
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  // Slow O(sort(N)) I/Os comparison by traversing the product construction and comparing each
+  // related pair of nodes.
+
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  // Check whether more requests were processed on this level than allowed. An isomorphic DAG would
+  // not create more requests than the original number of nodes.
   template <bool tv>
   class input_bound_levels
   {
@@ -28,17 +27,15 @@ namespace adiar::internal
 
   public:
     static size_t
-    pq1_upper_bound(const shared_levelized_file<node>& in_1,
-                    const shared_levelized_file<node>& in_2)
+    pq1_upper_bound(const dd& a, const dd& b)
     {
-      return std::max(in_1->max_2level_cut[cut::Internal], in_2->max_2level_cut[cut::Internal]);
+      return std::max(a->max_2level_cut[cut::Internal], b->max_2level_cut[cut::Internal]);
     }
 
     static size_t
-    pq2_upper_bound(const shared_levelized_file<node>& in_1,
-                    const shared_levelized_file<node>& in_2)
+    pq2_upper_bound(const dd& a, const dd& b)
     {
-      return std::max(in_1->max_1level_cut[cut::Internal], in_2->max_1level_cut[cut::Internal]);
+      return std::max(a->max_1level_cut[cut::Internal], b->max_1level_cut[cut::Internal]);
     }
 
     static constexpr size_t
@@ -48,9 +45,8 @@ namespace adiar::internal
     }
 
   public:
-    input_bound_levels(const shared_levelized_file<node>& f0,
-                       const shared_levelized_file<node>& /*f1*/)
-      : in_meta_1(f0)
+    input_bound_levels(const dd& a, const dd& /*b*/)
+      : in_meta_1(a)
     {}
 
     void
@@ -74,14 +70,14 @@ namespace adiar::internal
     static constexpr bool termination_value = tv;
   };
 
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   /// \brief Policy for isomorphism checking with `comparison_check`.
   ///
   /// \pre To use this operation, the following should be satisfied.
   ///  - The number of nodes are the same
   ///  - The number of levels are the same
   ///  - The label and size of each level are the same
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   // TODO (Decision Diagrams with other kinds of pointers):
   // template<class dd_policy>
   class isomorphism_policy
@@ -155,36 +151,33 @@ namespace adiar::internal
     static constexpr bool no_early_return_value = true;
   };
 
-  //////////////////////////////////////////////////////////////////////////////
-  /// Fast 2N/B I/Os comparison by comparing the i'th nodes numerically. This
-  /// requires, that the shared_levelized_file<node> is 'canonical' in the
-  /// following sense:
+  //////////////////////////////////////////////////////////////////////////////////////////////////
+  /// Fast 2N/B I/Os comparison by comparing the i'th nodes numerically. This requires, that the
+  /// shared_levelized_file<node> is 'canonical' in the following sense:
   ///
   /// - For each level, the ids are decreasing from max_id in increments of one.
   /// - There are no duplicate nodes.
-  /// - Nodes within each level are sorted by the children (e.g. ordered first on
-  ///   'high', secondly on 'low').
+  /// - Nodes within each level are sorted by the children (e.g. ordered first on 'high', secondly
+  ///   on 'low').
   ///
-  /// \remark See Section 3.3 in 'Efficient Binary Decision Diagram Manipulation
-  ///         in External Memory' on arXiv (v2 or newer) for an induction proof
-  ///         this is a valid comparison.
+  /// \remark See Section 3.3 in 'Efficient Binary Decision Diagram Manipulation in External Memory'
+  ///         on arXiv (v2 or newer) for an induction proof this is a valid comparison.
   ///
   /// \pre The following are satisfied:
   /// (1) The number of nodes are the same (to simplify the 'while' condition)
   /// (2) Both shared_levelized_file<node>s are 'canonical'.
   /// (3) The negation flags given to both shared_levelized_file<node>s agree
   ///     (breaks canonicity)
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   bool
-  fast_isomorphism_check(const shared_levelized_file<node>& f0,
-                         const shared_levelized_file<node>& f1)
+  fast_isomorphism_check(const dd& a, const dd& b)
   {
-    node_stream<> in_nodes_1(f0);
-    node_stream<> in_nodes_2(f1);
+    node_stream<> in_nodes_a(a);
+    node_stream<> in_nodes_b(b);
 
-    while (in_nodes_1.can_pull()) {
-      adiar_assert(in_nodes_2.can_pull(), "The number of nodes should coincide");
-      if (in_nodes_1.pull() != in_nodes_2.pull()) {
+    while (in_nodes_a.can_pull()) {
+      adiar_assert(in_nodes_b.can_pull(), "The number of nodes should coincide");
+      if (in_nodes_a.pull() != in_nodes_b.pull()) {
 #ifdef ADIAR_STATS
         stats_equality.fast_check.exit_on_mismatch += 1u;
 #endif
@@ -194,67 +187,62 @@ namespace adiar::internal
     return true;
   }
 
-  //////////////////////////////////////////////////////////////////////////////
+  //////////////////////////////////////////////////////////////////////////////////////////////////
   bool
-  is_isomorphic(const exec_policy& ep,
-                const shared_levelized_file<node>& f0,
-                const shared_levelized_file<node>& f1,
-                const bool negate0,
-                const bool negate1)
+  is_isomorphic(const exec_policy& ep, const dd& a, const dd& b)
   {
+    const bool a_negated = a.is_negated();
+    const bool b_negated = b.is_negated();
+
     // Are they literally referring to the same underlying file?
-    if (f0 == f1) {
+    if (a.file_ptr() == b.file_ptr()) {
 #ifdef ADIAR_STATS
       stats_equality.exit_on_same_file += 1u;
 #endif
-      return negate0 == negate1;
+      return a_negated == b_negated;
     }
 
-    // Are they trivially not the same, since they have different number of
-    // nodes?
-    if (f0->size() != f1->size()) {
+    // Are they trivially not the same, since they have different number of nodes?
+    if (a->size() != b->size()) {
 #ifdef ADIAR_STATS
       stats_equality.exit_on_nodecount += 1u;
 #endif
       return false;
     }
 
     // Are they trivially not the same, since their width is different?
-    if (f0->width != f1->width) {
+    if (a->width != b->width) {
 #ifdef ADIAR_STATS
       stats_equality.exit_on_width += 1u;
 #endif
       return false;
     }
 
-    // Are they trivially not the same, since they have different number of
-    // terminal arcs?
-    if (f0->number_of_terminals[negate0] != f1->number_of_terminals[negate1]
-        || f0->number_of_terminals[!negate0] != f1->number_of_terminals[!negate1]) {
+    // Are they trivially not the same, since they have different number of terminal arcs?
+    if (a->number_of_terminals[a_negated] != b->number_of_terminals[b_negated]
+        || a->number_of_terminals[!a_negated] != b->number_of_terminals[!b_negated]) {
 #ifdef ADIAR_STATS
       stats_equality.exit_on_terminalcount += 1u;
 #endif
       return false;
     }
 
-    // Are they trivially not the same, since they have different number of
-    // levels?
-    if (f0->levels() != f1->levels()) {
+    // Are they trivially not the same, since they have different number of levels?
+    if (a->levels() != b->levels()) {
 #ifdef ADIAR_STATS
       stats_equality.exit_on_varcount += 1u;
 #endif
       return false;
     }
 
-    // Are they trivially not the same, since the labels or the size of each
-    // level does not match?
+    // Are they trivially not the same, since the labels or the size of each level does not match?
     { // Create new scope to garbage collect the two meta_streams early
-      level_info_stream<> in_meta_0(f0);
-      level_info_stream<> in_meta_1(f1);
+      level_info_stream<> in_meta_a(a);
+      level_info_stream<> in_meta_b(b);
 
-      while (in_meta_0.can_pull()) {
-        adiar_assert(in_meta_1.can_pull(), "level_info files are same size");
-        if (in_meta_0.pull() != in_meta_1.pull()) {
+      while (in_meta_a.can_pull()) {
+        adiar_assert(in_meta_b.can_pull(), "level_info files are same size");
+        if (in_meta_a.pull() != in_meta_b.pull()) {
 #ifdef ADIAR_STATS
           stats_equality.exit_on_levels_mismatch += 1u;
 #endif
@@ -263,28 +251,20 @@ namespace adiar::internal
       }
     }
 
-    // TODO: Use 'fast_isomorphism_check' when there is only one node per level.
-    // In this case, we can just ignore the id (and only focus on the label and
-    // terminal values).
+    // TODO: Use 'fast_isomorphism_check' when there is only one node per level. In this case, we
+    // can just ignore the id (and only focus on the label and terminal values).
 
-    // Compare their content to discern whether there exists an isomorphism
-    // between them.
-    if (f0->is_canonical() && f1->is_canonical() && negate0 == negate1) {
+    // Compare their content to discern whether there exists an isomorphism between them.
+    if (a->is_canonical() && b->is_canonical() && a_negated == b_negated) {
 #ifdef ADIAR_STATS
       stats_equality.fast_check.runs += 1u;
 #endif
-      return fast_isomorphism_check(f0, f1);
+      return fast_isomorphism_check(a, b);
     } else {
 #ifdef ADIAR_STATS
       stats_equality.slow_check.runs += 1u;
 #endif
-      return comparison_check<isomorphism_policy>(ep, f0, f1, negate0, negate1);
+      return comparison_check<isomorphism_policy>(ep, a, b);
     }
   }
-
-  bool
-  is_isomorphic(const exec_policy& ep, const dd& a, const dd& b)
-  {
-    return is_isomorphic(ep, a.file, b.file, a.negate, b.negate);
-  }
 }