aiger: simplify output code, and fix some function call order

* spot/twaalgos/aiger.cc: Simplify some bit operatitions.  Force the
ordering of operations in aig_and, that was causing a test case to
fail on ARM, and greatly simplify the code and data structures used in
remove_unused().
* tests/core/ltlsynt.test: Adjust expected output.

spot/twaalgos/aiger.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement
+// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -120,7 +120,7 @@ namespace spot
 
       unsigned aig_not(unsigned v)
       {
-        unsigned not_v = v + 1 - 2 * (v % 2);
+        unsigned not_v = v ^ 1;
         assert(var2bdd_.count(v));
         var2bdd_[not_v] = !(var2bdd_[v]);
         bdd2var_[var2bdd_[not_v]] = not_v;
@@ -137,9 +137,8 @@ namespace spot
           return it->second;
         max_var_ += 2;
         and_gates_[max_var_] = {v1, v2};
-        bdd v1v2 = var2bdd_[v1] & var2bdd_[v2];
+        bdd2var_[b] = max_var_;
-        bdd2var_[v1v2] = max_var_;
+        var2bdd_[max_var_] = b;
-        var2bdd_[max_var_] = v1v2;
         return max_var_;
       }
 
@@ -152,14 +151,18 @@ namespace spot
         if (vs.size() == 2)
           return aig_and(vs[0], vs[1]);
         unsigned m = vs.size() / 2;
-        std::vector<unsigned> left(vs.begin(), vs.begin() + m);
+        unsigned left =
-        std::vector<unsigned> right(vs.begin() + m, vs.end());
+          aig_and(std::vector<unsigned>(vs.begin(), vs.begin() + m));
-        return aig_and(aig_and(left), aig_and(right));
+        unsigned right =
+          aig_and(std::vector<unsigned>(vs.begin() + m, vs.end()));
+        return aig_and(left, right);
       }
 
       unsigned aig_or(unsigned v1, unsigned v2)
       {
-        return aig_not(aig_and(aig_not(v1), aig_not(v2)));
+        unsigned n1 = aig_not(v1);
+        unsigned n2 = aig_not(v2);
+        return aig_not(aig_and(n1, n2));
       }
 
       unsigned aig_or(std::vector<unsigned> vs)
@@ -171,45 +174,53 @@ namespace spot
 
       unsigned aig_pos(unsigned v)
       {
-        return v - v % 2;
+
+        return v & ~1;
       }
 
       void remove_unused()
       {
-        std::unordered_set<unsigned> todo;
+        // Run a DFS on the gates and latches to collect
+        // all nodes connected to the output.
+        std::deque<unsigned> todo;
+        std::vector<bool> used(max_var_ / 2 + 1, false);
+        auto mark = [&](unsigned v)
+                    {
+                      unsigned pos = aig_pos(v);
+                      if (!used[pos/2])
+                        {
+                          used[pos/2] = 1;
+                          todo.push_back(pos);
+                        }
+                    };
         for (unsigned v : outputs_)
-          todo.insert(aig_pos(v));
+          mark(v);
-        std::unordered_set<unsigned> used;
         while (!todo.empty())
           {
-            used.insert(todo.begin(), todo.end());
+            unsigned v = todo.front();
-            std::unordered_set<unsigned> todo_next;
+            todo.pop_front();
-            for (unsigned v : todo)
+            auto it_and = and_gates_.find(v);
+            if (it_and != and_gates_.end())
               {
-                auto it_and = and_gates_.find(v);
+                mark(it_and->second.first);
-                if (it_and != and_gates_.end())
+                mark(it_and->second.second);
-                  {
+              }
-                    if (!used.count(aig_pos(it_and->second.first)))
+            else if (v <= (num_inputs_ + latches_.size()) * 2
-                      todo_next.insert(aig_pos(it_and->second.first));
+                     && v > num_inputs_ * 2)
-                    if (!used.count(aig_pos(it_and->second.second)))
+              {
-                      todo_next.insert(aig_pos(it_and->second.second));
+                mark(latches_[v / 2 - num_inputs_ - 1]);
-                  }
-                else if (v <= (num_inputs_ + latches_.size()) * 2
-                         && v > num_inputs_ * 2)
-                  {
-                    unsigned l = v / 2 - num_inputs_ - 1;
-                    if (!used.count(aig_pos(latches_[l])))
-                      todo_next.insert(aig_pos(latches_[l]));
-                  }
               }
-            todo = todo_next;
           }
-        std::unordered_set<unsigned> unused;
+        // Erase and_gates that were not seen in the above
-        for (auto& p : and_gates_)
+        // exploration.
-          if (!used.count(p.first))
+        auto e = and_gates_.end();
-            unused.insert(p.first);
+        for (auto i = and_gates_.begin(); i != e;)
-        for (unsigned v : unused)
+          {
-          and_gates_.erase(v);
+            if (!used[i->first/2])
+              i = and_gates_.erase(i);
+            else
+              ++i;
+          }
       }
 
       void
@@ -244,7 +255,7 @@ namespace spot
       std::vector<bool> v(size);
       for (unsigned i = 0; i < size; ++i)
         {
-          v[i] = s % 2;
+          v[i] = s & 1;
           s >>= 1;
         }
       return v;
@@ -277,7 +288,7 @@ namespace spot
           unsigned st0 = bdd_var(all);
           for (unsigned i = 0; i < size; ++i)
             {
-              b &= s % 2 ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i);
+              b &= (s & 1)  ? bdd_ithvar(st0 + i) : bdd_nithvar(st0 + i);
               s >>= 1;
             }
         }

tests/core/ltlsynt.test

@@ -61,11 +61,11 @@ aag 23 1 2 1 16
 26 4 6
 28 2 26
 30 3 26
-36 29 31
+36 17 23
-38 25 36
+38 13 36
-40 17 23
+40 29 31
-42 13 40
+42 25 40
-44 42 38
+44 38 42
 46 25 29
 i0 a
 o0 b