diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index af255a167..6b608dd59 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2022 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2023 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -552,20 +552,20 @@ namespace spot assert(var2bdd_.count(v1)); assert(var2bdd_.count(v2)); - if (v1 != v2) - { - bdd b = var2bdd_[v1] & var2bdd_[v2]; - auto [it, inserted] = bdd2var_.try_emplace(b.id(), 0); - if (!inserted) - return it->second; - max_var_ += 2; - it->second = max_var_; - and_gates_.emplace_back(v1, v2); - register_new_lit_(max_var_, b); - return max_var_; - } - else - return v1; + if (SPOT_UNLIKELY(v1 > v2)) + std::swap(v1, v2); + if (SPOT_UNLIKELY(v1 == v2)) + return v1; + + bdd b = var2bdd_[v1] & var2bdd_[v2]; + auto [it, inserted] = bdd2var_.try_emplace(b.id(), 0); + if (!inserted) + return it->second; + max_var_ += 2; + it->second = max_var_; + and_gates_.emplace_back(v1, v2); + register_new_lit_(max_var_, b); + return max_var_; } unsigned aig::aig_and(std::vector& vs) diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test index 4a7595539..02d248754 100644 --- a/tests/core/ltlsynt.test +++ b/tests/core/ltlsynt.test @@ -1,6 +1,6 @@ #! /bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2017, 2019-2022 Laboratoire de Recherche et +# Copyright (C) 2017, 2019-2023 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -160,6 +160,10 @@ ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ --algo=ds --simplify=no --aiger=isop >out diff out exp +ltlsynt --ins=a --outs=b,c -f 'GFa <-> (GFb & GFc)' \ + --algo=ds --simplify=no --aiger=optim >out +diff out exp + cat >exp <