ascii ordered construction added

Author: Catoverflow

ROBDD.cpp

@@ -4,12 +4,13 @@ bool BDD_node::operator==(const BDD_node &rhs) const
 {
     return this->var == rhs.var && this->low == rhs.low && this->high == rhs.high;
 }
-ROBDD::ROBDD()
+ROBDD::ROBDD(bool order_by_ascii)
 {
     this->zero = new BDD_node({0, nullptr, nullptr});
     this->one = new BDD_node({1, nullptr, nullptr});
     this->node_table[*(this->zero)] = this->zero;
     this->node_table[*(this->one)] = this->one;
+    this->order_by_ascii = order_by_ascii;
 }
 
 BDD_node *ROBDD::get_one() const
@@ -29,7 +30,11 @@ unsigned int ROBDD::get_ID(std::string var)
 {
     // new var
     if (this->var_to_ID.find(var) == this->var_to_ID.end())
-        this->var_to_ID[var] = avail_ID++;
+    {
+        this->var_to_ID[var] = avail_ID;
+        this->ID_to_var[avail_ID] = var;
+        avail_ID++;
+    }
     return this->var_to_ID[var];
 }
 
@@ -94,6 +99,10 @@ BDD_node *ROBDD::apply(binary_op op, BDD_node *left, BDD_node *right)
 
 BDD_node *ROBDD::_apply(binary_op op, BDD_node *left, BDD_node *right)
 {
+    auto less = [&](BDD_node *lhs, BDD_node *rhs)
+    {
+        return this->order_by_ascii ? this->ID_to_var[lhs->var] < this->ID_to_var[rhs->var] : lhs->var < rhs->var;
+    };
     auto found = this->apply_table[op].find(std::pair<BDD_node *, BDD_node *>(left, right));
     BDD_node *res;
     if (found != this->apply_table[op].end())
@@ -106,13 +115,13 @@ BDD_node *ROBDD::_apply(binary_op op, BDD_node *left, BDD_node *right)
         auto r = this->_apply(op, left->high, right->high);
         res = this->make_node(left->var, l, r);
     }
-    else if ((left->var < right->var and left->var > 1) or right->var <= 1) // unfold left BDD tree
+    else if ((less(left, right) and left->var > 1) or right->var <= 1) // unfold left BDD tree
     {
         auto l = this->_apply(op, left->low, right);
         auto r = this->_apply(op, left->high, right);
         res = this->make_node(left->var, l, r);
     }
-    else if ((left->var > right->var and right->var > 1) or left->var <= 1) // unfold right BDD tree
+    else // unfold right BDD tree
     {
         auto l = this->_apply(op, left, right->low);
         auto r = this->_apply(op, left, right->high);
@@ -165,8 +174,6 @@ void ROBDD::output(std::ofstream &out)
     this->printed[this->zero] = 0;
     this->printed[this->one] = 1;
     this->uuid = 2;
-    for (auto it : this->var_to_ID)
-        this->ID_to_var[it.second] = it.first;
     out << "digraph ROBDD {\n"
         << "fontname=\"Helvetica,Arial,sans-serif\"\n"
         << "node [fontname=\"Helvetica,Arial,sans-serif\"]\n"

ROBDD.hpp

@@ -40,11 +40,12 @@ struct ROBDD
         }
     };
     BDD_node *root;
-
+    bool order_by_ascii;
     // Construction
     // for make_node()
     std::unordered_map<BDD_node, BDD_node *, BDD_node_hash> node_table;
     std::unordered_map<std::string, unsigned int> var_to_ID;
+    std::unordered_map<unsigned int, std::string> ID_to_var;
     // for var -> ID assignment
     unsigned int avail_ID = 2; // 0 & 1 is reserved
     // for apply()
@@ -54,7 +55,6 @@ struct ROBDD
 
     // Q-A
     // for ROBDD printing
-    std::unordered_map<unsigned int, std::string> ID_to_var;
     std::unordered_map<BDD_node *, size_t> printed;
     void _output(BDD_node *, std::ofstream &);
     // for node -> ID assignment, ID only works as unique tag for graphviz
@@ -65,7 +65,7 @@ struct ROBDD
     BDD_node *one, *zero;
 
 public:
-    ROBDD();
+    ROBDD(bool order_by_ascii = false);
     // get id for var
     unsigned int get_ID(std::string var);
     // add or return existed node

main.cpp

@@ -11,14 +11,14 @@ bool frontend_err = false;
 int main(int argc, char **argv)
 {
     // for command line args parsing
-    bool all_sat_flag = 0, any_sat_flag = 0, sat_count_flag = 0, timing_flag = 0;
+    bool all_sat_flag = 0, any_sat_flag = 0, sat_count_flag = 0, timing_flag = 0, order_flag = 0;
     std::chrono::steady_clock::time_point begin, end;
     char *output_filename = nullptr;
     char flag;
     opterr = 0;
 
     // ref: https://www.gnu.org/software/libc/manual/html_node/Example-of-Getopt.html
-    while ((flag = getopt(argc, argv, "Sscto:")) != -1)
+    while ((flag = getopt(argc, argv, "SscAato:")) != -1)
     {
         switch (flag)
         {
@@ -31,6 +31,12 @@ int main(int argc, char **argv)
         case 'c':
             sat_count_flag = 1;
             break;
+        case 'a':
+            order_flag = 0;
+            break;
+        case 'A':
+            order_flag = 1;
+            break;
         case 't':
             timing_flag = 1;
             break;
@@ -47,6 +53,9 @@ int main(int argc, char **argv)
             std::cerr << "Usage: ROBDD [-Ssct] [-o filename]" << std::endl;
             std::cerr << " -s\t\t- Check if the proposition is All-SAT" << std::endl;
             std::cerr << " -S\t\t- Check if the proposition is Any-SAT" << std::endl;
+            std::cerr << " -A\t\t- Construct ROBDD under fixed ASCII order," << std::endl
+                      << "\t\t  smallest variable at top" << std::endl;
+            std::cerr << " -a (default)\t- Construct ROBDD under parsing order" << std::endl;
             std::cerr << " -c\t\t- Return SAT count for the proposition" << std::endl;
             std::cerr << " -t\t\t- Return ROBDD construction time cost" << std::endl;
             std::cerr << " -o filename\t- Print ROBDD to filename.svg" << std::endl;
@@ -57,7 +66,7 @@ int main(int argc, char **argv)
     }
     if (timing_flag)
         begin = std::chrono::steady_clock::now();
-    T = new ROBDD();
+    T = new ROBDD(order_flag);
     yyparse();
     if (timing_flag)
         end = std::chrono::steady_clock::now();