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

* src/tgbaalgos/dtbasat.cc: Skip clauses for trivial SCCs.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2013-09-05 11:30:58 +02:00
parent 88cd81c547
commit 073334dfd6
1 changed files with 19 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/tgbaalgos/dtbasat.cc
View file

@ -250,6 +250,9 @@ namespace spot
{ {
d.prodid[state_pair(j, i)] = ++d.nvars; d.prodid[state_pair(j, i)] = ++d.nvars;
if (sm_.trivial(i_scc))
continue;
for (dict::state_map::const_iterator k2 = seen.begin(); for (dict::state_map::const_iterator k2 = seen.begin();
k2 != seen.end(); ++k2) k2 != seen.end(); ++k2)
{ {
@ -407,13 +410,18 @@ namespace spot
int q1 = pit->first.a; int q1 = pit->first.a;
int q1p = pit->first.b; int q1p = pit->first.b;
dout << "(2) states Cand[" << q1 << "] and Ref[" << q1p unsigned q1p_scc = sm.scc_of_state(d.int_to_state[q1p]);
<< "] are 0-length paths\n";
path p(q1, q1p, q1, q1p); if (!sm.trivial(q1p_scc))
dout << pit->first << " → (" << p << "R ∧ " << p << "C)\n"; {
out << -pit->second << " " << d.pathid_ref[p] <<" 0\n"; dout << "(2) states Cand[" << q1 << "] and Ref[" << q1p
out << -pit->second << " " << d.pathid_cand[p] <<" 0\n"; << "] are 0-length paths\n";
nclauses += 2; path p(q1, q1p, q1, q1p);
dout << pit->first << " → (" << p << "R ∧ " << p << "C)\n";
out << -pit->second << " " << d.pathid_ref[p] << " 0\n";
out << -pit->second << " " << d.pathid_cand[p] << " 0\n";
nclauses += 2;
}
dout << "(3) augmenting paths based on Cand[" << q1 dout << "(3) augmenting paths based on Cand[" << q1
<< "] and Ref[" << q1p << "]\n"; << "] and Ref[" << q1p << "]\n";
@ -459,6 +467,8 @@ namespace spot
for (int q1p = 1; q1p <= ref_size; ++q1p) for (int q1p = 1; q1p <= ref_size; ++q1p)
{ {
unsigned q1p_scc = sm.scc_of_state(d.int_to_state[q1p]); unsigned q1p_scc = sm.scc_of_state(d.int_to_state[q1p]);
if (sm.trivial(q1p_scc))
continue;
for (int q2p = 1; q2p <= ref_size; ++q2p) for (int q2p = 1; q2p <= ref_size; ++q2p)
{ {
// We are only interested in transition that can form a // We are only interested in transition that can form a
@ -550,6 +560,8 @@ namespace spot
for (int q1p = 1; q1p <= ref_size; ++q1p) for (int q1p = 1; q1p <= ref_size; ++q1p)
{ {
unsigned q1p_scc = sm.scc_of_state(d.int_to_state[q1p]); unsigned q1p_scc = sm.scc_of_state(d.int_to_state[q1p]);
if (sm.trivial(q1p_scc))
continue;
for (int q2p = 1; q2p <= ref_size; ++q2p) for (int q2p = 1; q2p <= ref_size; ++q2p)
{ {
// We are only interested in transition that can form a // We are only interested in transition that can form a