From 4c0e7bf865843f393d8fbdb73b8469c12e032e5b Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 26 Sep 2019 11:44:15 +0200 Subject: [PATCH] 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 | 91 +++++++++++++++++++++++------------------ tests/core/ltlsynt.test | 10 ++--- 2 files changed, 56 insertions(+), 45 deletions(-) diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 459e82c97..ea8f8ee6e 100644 --- a/spot/twaalgos/aiger.cc +++ b/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_[v1v2] = max_var_; - var2bdd_[max_var_] = v1v2; + bdd2var_[b] = max_var_; + var2bdd_[max_var_] = b; 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 left(vs.begin(), vs.begin() + m); - std::vector right(vs.begin() + m, vs.end()); - return aig_and(aig_and(left), aig_and(right)); + unsigned left = + aig_and(std::vector(vs.begin(), vs.begin() + m)); + unsigned right = + aig_and(std::vector(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 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 todo; + // Run a DFS on the gates and latches to collect + // all nodes connected to the output. + std::deque todo; + std::vector 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)); - std::unordered_set used; + mark(v); while (!todo.empty()) { - used.insert(todo.begin(), todo.end()); - std::unordered_set todo_next; - for (unsigned v : todo) + unsigned v = todo.front(); + todo.pop_front(); + auto it_and = and_gates_.find(v); + if (it_and != and_gates_.end()) { - auto it_and = and_gates_.find(v); - if (it_and != and_gates_.end()) - { - if (!used.count(aig_pos(it_and->second.first))) - todo_next.insert(aig_pos(it_and->second.first)); - if (!used.count(aig_pos(it_and->second.second))) - todo_next.insert(aig_pos(it_and->second.second)); - } - 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])); - } + mark(it_and->second.first); + mark(it_and->second.second); + } + else if (v <= (num_inputs_ + latches_.size()) * 2 + && v > num_inputs_ * 2) + { + mark(latches_[v / 2 - num_inputs_ - 1]); } - todo = todo_next; } - std::unordered_set unused; - for (auto& p : and_gates_) - if (!used.count(p.first)) - unused.insert(p.first); - for (unsigned v : unused) - and_gates_.erase(v); + // Erase and_gates that were not seen in the above + // exploration. + auto e = and_gates_.end(); + for (auto i = and_gates_.begin(); i != e;) + { + if (!used[i->first/2]) + i = and_gates_.erase(i); + else + ++i; + } } void @@ -244,7 +255,7 @@ namespace spot std::vector 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; } } diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index bdd0de907..5a1886e8c 100644 --- a/tests/core/ltlsynt.test +++ b/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 -38 25 36 -40 17 23 -42 13 40 -44 42 38 +36 17 23 +38 13 36 +40 29 31 +42 25 40 +44 38 42 46 25 29 i0 a o0 b