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 37325f1942
commit 95379c18cc
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 -*-
// 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<unsigned>& vs)

8
tests/core/ltlsynt.test
View file

@ -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 <<EOF
REALIZABLE
aag 2 1 1 2 0
@ -182,7 +186,7 @@ aag 3 1 1 2 1
4 1
6
6
6 4 2
6 2 4
i0 a
o0 b
o1 c