construction for neg bug fix

Author: Catoverflow

ROBDD.cpp

@@ -1,5 +1,9 @@
 #include "ROBDD.hpp"
 #include <fstream>
+bool BDD_node::operator==(const BDD_node &rhs) const
+{
+    return this->var == rhs.var && this->low == rhs.low && this->high == rhs.high;
+}
 ROBDD::ROBDD()
 {
     this->zero = new BDD_node({0, nullptr, nullptr});
@@ -8,11 +12,11 @@ ROBDD::ROBDD()
     this->node_table[*(this->one)] = this->one;
 }
 
-BDD_node* ROBDD::get_one() const
+BDD_node *ROBDD::get_one() const
 {
     return this->one;
 }
-BDD_node* ROBDD::get_zero() const
+BDD_node *ROBDD::get_zero() const
 {
     return this->zero;
 }
@@ -173,7 +177,6 @@ void ROBDD::output(std::ofstream &out)
     this->printed.clear();
 }
 
-
 void ROBDD::_output(BDD_node *node, std::ofstream &out)
 {
     // print node itself
@@ -187,7 +190,7 @@ void ROBDD::_output(BDD_node *node, std::ofstream &out)
             out << this->ID_to_var[node->var];
         else
             out << node->var;
-        out << "\"]" <<  std::endl; // use label as node name
+        out << "\"]" << std::endl; // use label as node name
     }
     // no subnodes
     if (node->var <= 1)

ROBDD.hpp

@@ -17,7 +17,7 @@ struct BDD_node
     // var = 0 and var = 1 reserved
     unsigned int var;
     BDD_node *low, *high;
-    bool operator==(const BDD_node &rhs) const { return this->var == rhs.var && this->low == rhs.low && this->high == rhs.high; }
+    bool operator==(const BDD_node &rhs) const;
 };
 struct ROBDD
 {
@@ -26,8 +26,8 @@ struct ROBDD
     {
         std::size_t operator()(const BDD_node &T) const
         {
-            return std::hash<void *>()(static_cast<void *>(T.low))
-                 ^ std::hash<void *>()(static_cast<void *>(T.high))
+            return (std::hash<void *>()(static_cast<void *>(T.low)) // hash result affected by order
+                 - std::hash<void *>()(static_cast<void *>(T.high)))
                  ^ std::hash<int>()(T.var);
         }
     };
@@ -36,7 +36,7 @@ struct ROBDD
         std::size_t operator()(const std::pair<BDD_node *, BDD_node *> &T) const
         {
             return std::hash<void *>()(static_cast<void *>(T.first))
-                 ^ std::hash<void *>()(static_cast<void *>(T.second));
+                 - std::hash<void *>()(static_cast<void *>(T.second));
         }
     };
     BDD_node *root;

expression.y

@@ -47,7 +47,7 @@ func
 | term {$$ = $1;}
 
 term
-: NOT atom {$$ = $2; auto tmp = $$->high; $$->high = $$->low; $$->low = tmp;}
+: NOT atom {$$ = T->make_node($2->var, $2->high, $2->low);}
 | atom {$$ = $1;}
 
 atom