Add fast O(N/B) equality checking

src/adiar/file.h

@@ -11,9 +11,10 @@
 #include <tpie/file.h>
 #include <tpie/sort.h>
 
-// ADIAR imports of the foundational data structure and the union class.
+// ADIAR imports
+// - foundational data structure and the union class.
 #include <adiar/data.h>
-
+// - assertions
 #include <adiar/assert.h>
 
 namespace adiar
@@ -129,6 +130,10 @@ namespace adiar
     static_assert(0 < Files, "The number of files must be positive");
 
   public:
+    // Boolean flag primarily used for __meta_file<node_t,1> to recognise the
+    // easy cases to check for isomorphism.
+    bool canonical = false;
+
     file<meta> _meta_file;
     file<T> _files [Files];
 
@@ -326,25 +331,29 @@ namespace adiar
   {
   public:
     ////////////////////////////////////////////////////////////////////////////
-    /// Construct a temporary node_file
-    ////////////////////////////////////////////////////////////////////////////
+    // Constructors
+
+    // Temporary node_file constructor
     node_file() : __shared_file() { }
 
-    // TODO: Files with persistent file names
+    // TODO: Persistent files with a filename
     // node_file(const std::string &filename) : __shared_file(filename) { }
 
     // Copy constructor
-    node_file(const node_file &other) : __shared_file(other) { }
+    node_file(const node_file &o) : __shared_file(o) { }
 
     // Move constructor
-    node_file(node_file &&other) : __shared_file(other) { }
+    node_file(node_file &&o) : __shared_file(o) { }
 
+    ////////////////////////////////////////////////////////////////////////////
     size_t meta_size() const
     {
       return _file_ptr -> meta_size();
     }
 
     ////////////////////////////////////////////////////////////////////////////
+    // Assignment operator
+    // TODO: Are these not autogenerated?
     node_file& operator= (const node_file &o)
     {
       _file_ptr = o._file_ptr;

src/adiar/file_writer.h

@@ -161,11 +161,10 @@ namespace adiar {
   template <typename T, size_t Files>
   class meta_file_writer
   {
-  private:
+  protected:
     // Keep a local shared_ptr to be in on the reference counting
     std::shared_ptr<__meta_file<T, Files>> _file_ptr;
 
-  protected:
     tpie::file_stream<meta_t> _meta_stream;
     tpie::file_stream<T> _streams [Files];
 
@@ -272,43 +271,60 @@ namespace adiar {
   class node_writer: public meta_file_writer<node_t, 1>
   {
   private:
-    uid_t _latest_node = NIL;
+    node_t _latest_node = { NIL, NIL, NIL };
+    bool _canonical = true;
 
     size_t _level_size = 0u;
 
   public:
     node_writer() : meta_file_writer() { }
-    node_writer(const node_file &nf) : meta_file_writer(nf) { }
+    node_writer(const node_file &nf) : meta_file_writer(nf),
+                                       _canonical(!meta_file_writer::has_pushed()
+                                                  || nf._file_ptr -> canonical) { }
 
     ~node_writer() { detach(); }
 
     ////////////////////////////////////////////////////////////////////////////
     /// \brief Write the next node to the file.
     ///
     /// Writes the given node to the end of the file and also writes to the meta
-    /// file if necessary. The given node must have valid children (not checked)
-    /// and must be topologically prior to any nodes already written to the
-    /// file (checked).
+    /// file if necessary. The given node must have valid children (not
+    /// checked), no duplicate nodes created (not properly checked), and must be
+    /// topologically prior to any nodes already written to the file (checked).
     ////////////////////////////////////////////////////////////////////////////
     void push(const node_t &n)
     {
       adiar_assert(attached(), "file_writer is not yet attached to any file");
 
-      // Check latest was not a sink
-      adiar_assert(is_nil(_latest_node) || !is_sink(_latest_node),
-                  "Cannot push a node after having pushed a sink");
-      adiar_assert(is_nil(_latest_node) || !is_sink(n),
-                  "Cannot push a sink into non-empty file");
+      // Check validity of input based on latest written node
+      if (!is_nil(_latest_node.uid)) {
+        adiar_assert(!is_sink(_latest_node),
+                     "Cannot push a node after having pushed a sink");
+        adiar_assert(!is_sink(n),
+                     "Cannot push a sink into non-empty file");
 
-      // Check it is topologically sorted
-      if (!is_nil(_latest_node)) {
-        adiar_assert(n.uid < _latest_node,
+        // Check it is topologically sorted
+        adiar_assert(n.uid < _latest_node.uid,
                     "Pushed node is required to be prior to the existing nodes");
         adiar_assert(!is_node(n.low) || label_of(n.uid) < label_of(n.low),
                     "Low child must point to a node with a higher label");
         adiar_assert(!is_node(n.high) || label_of(n.uid) < label_of(n.high),
                     "High child must point to a node with a higher label");
 
+        // Check it is canonically sorted
+        if (_canonical) {
+          if (label_of(_latest_node) == label_of(n)) {
+            bool id_diff = id_of(n.uid) == id_of(_latest_node) - 1u;
+            bool children_ordered = n.high < _latest_node.high
+                                    || (n.high == _latest_node.high && n.low < _latest_node.low);
+
+            _canonical = id_diff && children_ordered;
+          } else {
+            bool id_reset = id_of(n) == MAX_ID;
+            _canonical = id_reset;
+          }
+        }
+
         // Check if the meta file has to be updated
         if (label_of(n) != label_of(_latest_node)) {
           meta_file_writer::unsafe_push(create_meta(label_of(_latest_node),
@@ -318,7 +334,7 @@ namespace adiar {
       }
 
       // Write node to file
-      _latest_node = n.uid;
+      _latest_node = n;
       _level_size++;
 
       meta_file_writer::unsafe_push(n, 0);
@@ -341,7 +357,9 @@ namespace adiar {
     }
     bool attached() const { return meta_file_writer::attached(); }
     void detach() {
-      if (!is_nil(_latest_node) && !is_sink(_latest_node)) {
+      _file_ptr -> canonical = _canonical;
+
+      if (!is_nil(_latest_node.uid) && !is_sink(_latest_node)) {
         meta_file_writer::unsafe_push(create_meta(label_of(_latest_node),
                                                   _level_size));
         _level_size = 0u; // move to attach...

src/adiar/isomorphism.cpp

@@ -6,7 +6,6 @@
 
 namespace adiar
 {
-
   //////////////////////////////////////////////////////////////////////////////
   // Slow O(sort(N)) I/Os comparison by traversing the product construction and
   // comparing each related pair of nodes.
@@ -61,7 +60,7 @@ namespace adiar
     adiar_debug(label_of(v1) == label_of(v2), "The levels (and hence the root) should coincide");
 
     if (!in_nodes_1.can_pull()) {
-      adiar_debug(!in_nodes_1.can_pull(), "The number of nodes should coincide");
+      adiar_debug(!in_nodes_2.can_pull(), "The number of nodes should coincide");
       return v1.low == v2.low && v1.high == v2.high;
     }
 
@@ -169,6 +168,36 @@ namespace adiar
     return true;
   }
 
+  //////////////////////////////////////////////////////////////////////////////
+  // Fast 2N/B I/Os comparison by comparing the i'th nodes numerically. This
+  // requires, that the node_file 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').
+  //
+  // 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.
+
+  /////////////////////
+  // Precondition:
+  //  - The number of nodes are the same (to simplify the 'while' condition)
+  //  - The node_files are both 'canonical'.
+  //  - The negation flags given for both node_files agree (breaks canonicity)
+  bool fast_isomorphism_check(const node_file &f1, const node_file &f2)
+  {
+    node_stream<> in_nodes_1(f1);
+    node_stream<> in_nodes_2(f2);
+
+    while (in_nodes_1.can_pull()) {
+      adiar_debug(in_nodes_2.can_pull(), "The number of nodes should coincide");
+      if (in_nodes_1.pull() != in_nodes_2.pull()) { return false; }
+    }
+    return true;
+  }
+
   //////////////////////////////////////////////////////////////////////////////
   bool is_isomorphic(const node_file &f1, const node_file &f2,
                      bool negate1, bool negate2)
@@ -204,6 +233,15 @@ namespace adiar
       }
     }
 
-    return slow_isomorphism_check(f1, f2, negate1, negate2);
+    // TODO: Use 'fast_isomorphism_check' when there is only one node per level.
+
+    // Compare their content to discern whether there exists an isomorphism
+    // between them.
+    if (f1._file_ptr -> canonical && f2._file_ptr -> canonical
+        && negate1 == negate2) {
+      return fast_isomorphism_check(f1, f2);
+    } else {
+      return slow_isomorphism_check(f1, f2, negate1, negate2);
+    }
   }
 }

src/adiar/reduce.cpp

@@ -71,6 +71,8 @@ namespace adiar
   node_file reduce(const arc_file &in_file)
   {
     node_file out_file;
+    out_file._file_ptr -> canonical = true;
+
     node_writer out_writer(out_file);
 
     // Set up