Persistable Decision Diagrams

[SSoelvsten]

Despite the fact that Adiar works by storing everything on disk, we currently do not allow the user to truly save/load files on disk.

Solution

• [x] Add move member function to file<elem_t> and levelized_file<elem_t> ( Done in #397 )
• [x] Move meta information of levelized_file<elem_t> into a __levelized_file_stats<elem_t> struct that levelized_file<elem_t> publicly inherits from.
• [x] Add make_persistent member function to file<elem_t> and levelized_file<elem_t> ( Done in #397 )
  • [ ] Store the __levelized_file_stats<elem_t> in the file header of the levels file, as shown in the External memory queue example.
• [ ] Store (and load) the non-shareable information of the BDD, e.g. the negate flag. Since persisted files might be reused, the above values should instead be placed in a text file. If so, we should store the path to the persisted file.
  • .version = <adiar::version()> ( see #140 ) With the version number we can warn the user for the need to migrate older files. This will be useful if we ever implement complement edges.
  • .diagram_type = <bdd / zdd> With this we know what type of decision diagram to return (or can verify it indeed contains the requested type).
  • .negate = <negation flag> Should be used with the constructor of the decision_diagram
  • elem_size = <sizeof(node)> Just to double-check it (probably) matches the node type of the decision diagram.
  • nodes_path = <path/to/nodes>
  • levels_path = <path/to/levels>
• [ ] void bdd_save(const bdd &f, std::string file_path): Move the underlying temporary file and mark it as a persistent file instead. This way we do not duplicate the entire (possibly several GiB sized) file.
  1. Use (move(prefix_path)) to place the files at the requested place.
     • If it already was persistent then use copy(file) + move(prefix_path) . Alternatively, if we want to reuse persisted files, then we can abort early and just goto step 4.
  2. Set it to be persistent (make_persistent())
  3. Store the non-shareable information.
• [ ] bdd bdd_load(std::string file_path):
  1. Make a new node_file using the non-default path-specific constructor.
  2. Using the above constructor, create a node_file and then use the current constructor for a bdd that takes both a node_file and a negate boolean and return that.

These functions can be defined in adiar/bdd/io.cpp and adiar/zdd/io.cpp

[SSoelvsten]

I moved this into the Symbolic Model Checking Milestone since this is probably when we need it ourselves to store and load the transition function etc.

[SSoelvsten]

The rewrite in #397 also cleans up the code for files. Specifically, it also exposes TPIE's persistence of a file and adds move and copy functions for a file. This covers the most risky parts of this issue!