alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

aiger: order the inputs of binary AND gates

Browse source 
* spot/twaalgos/aiger.cc: Here.
* tests/core/ltlsynt.test: Adjust, and add test case for aiger=optim.
This commit is contained in:
Alexandre Duret-Lutz 2023-07-26 23:57:12 +02:00
parent e548bf0a8e
commit 531252119c
2 changed files with 21 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

30
spot/twaalgos/aiger.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- 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). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -552,20 +552,20 @@ namespace spot
assert(var2bdd_.count(v1)); assert(var2bdd_.count(v1));
assert(var2bdd_.count(v2)); assert(var2bdd_.count(v2));
if (v1 != v2) if (SPOT_UNLIKELY(v1 > v2))
{ std::swap(v1, v2);
bdd b = var2bdd_[v1] & var2bdd_[v2]; if (SPOT_UNLIKELY(v1 == v2))
auto [it, inserted] = bdd2var_.try_emplace(b.id(), 0); return v1;
if (!inserted)
return it->second; bdd b = var2bdd_[v1] & var2bdd_[v2];
max_var_ += 2; auto [it, inserted] = bdd2var_.try_emplace(b.id(), 0);
it->second = max_var_; if (!inserted)
and_gates_.emplace_back(v1, v2); return it->second;
register_new_lit_(max_var_, b); max_var_ += 2;
return max_var_; it->second = max_var_;
} and_gates_.emplace_back(v1, v2);
else register_new_lit_(max_var_, b);
return v1; return max_var_;
} }
unsigned aig::aig_and(std::vector<unsigned>& vs) unsigned aig::aig_and(std::vector<unsigned>& vs)

8
tests/core/ltlsynt.test
View file

@ -1,6 +1,6 @@
#! /bin/sh #! /bin/sh
# -*- coding: utf-8 -*- # -*- 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). # Développement de l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # 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 --algo=ds --simplify=no --aiger=isop >out
diff out exp 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 <<EOF cat >exp <<EOF
REALIZABLE REALIZABLE
aag 2 1 1 2 0 aag 2 1 1 2 0
@ -182,7 +186,7 @@ aag 3 1 1 2 1
4 1 4 1
6 6
6 6
6 4 2 6 2 4
i0 a i0 a
o0 b o0 b
o1 c o1 c