diff --git a/src/tgbaalgos/dtbasat.cc b/src/tgbaalgos/dtbasat.cc index fb7c3210d..969bde0d6 100644 --- a/src/tgbaalgos/dtbasat.cc +++ b/src/tgbaalgos/dtbasat.cc @@ -24,7 +24,7 @@ #include "reachiter.hh" #include #include -#include "scc.hh" +#include "sccinfo.hh" #include "tgba/bddprint.hh" #include "stats.hh" #include "misc/satsolver.hh" @@ -57,11 +57,11 @@ namespace spot struct transition { - int src; + unsigned src; bdd cond; - int dst; + unsigned dst; - transition(int src, bdd cond, int dst) + transition(unsigned src, bdd cond, unsigned dst) : src(src), cond(cond), dst(dst) { } @@ -89,10 +89,10 @@ namespace spot struct src_cond { - int src; + unsigned src; bdd cond; - src_cond(int src, bdd cond) + src_cond(unsigned src, bdd cond) : src(src), cond(cond) { } @@ -115,10 +115,10 @@ namespace spot struct state_pair { - int a; - int b; + unsigned a; + unsigned b; - state_pair(int a, int b) + state_pair(unsigned a, unsigned b) : a(a), b(b) { } @@ -210,77 +210,48 @@ namespace spot std::map prodid; std::map pathid_ref; std::map pathid_cand; - int nvars; - typedef std::unordered_map state_map; - typedef std::unordered_map int_map; - state_map state_to_int; - int_map int_to_state; - int cand_size; - - ~dict() - { - state_map::const_iterator s = state_to_int.begin(); - while (s != state_to_int.end()) - // Always advance the iterator before deleting the key. - s++->first->destroy(); - } + int nvars = 0; + unsigned cand_size; }; - - class filler_dfs: public tgba_reachable_iterator_depth_first + unsigned declare_vars(const const_tgba_digraph_ptr& aut, + dict& d, + bdd ap, + bool state_based, + scc_info& sm) { - protected: - dict& d; - int size_; - bdd ap_; - bool state_based_; - scc_map& sm_; - public: - filler_dfs(const const_tgba_ptr& aut, dict& d, bdd ap, bool state_based, - scc_map& sm) - : tgba_reachable_iterator_depth_first(aut), d(d), ap_(ap), - state_based_(state_based), sm_(sm) - { - d.nvars = 0; - } + unsigned ref_size = aut->num_states(); - int size() - { - return size_; - } + if (d.cand_size == -1U) + for (unsigned i = 0; i < ref_size; ++i) + if (sm.reachable_state(i)) + ++d.cand_size; // Note that we start from -1U the + // cand_size is one less than the + // number of reachable states. - void end() - { - size_ = seen.size(); + for (unsigned i = 0; i < ref_size; ++i) + { + if (!sm.reachable_state(i)) + continue; - if (d.cand_size == -1) - d.cand_size = size_ - 1; + unsigned i_scc = sm.scc_of(i); + bool is_trivial = sm.is_trivial(i_scc); - // Reverse the "seen" map. States are labeled from 1 to size_. - for (dict::state_map::const_iterator i2 = seen.begin(); - i2 != seen.end(); ++i2) - d.int_to_state[i2->second] = i2->first; + for (unsigned j = 0; j < d.cand_size; ++j) + { + d.prodid[state_pair(j, i)] = ++d.nvars; - for (int i = 1; i <= size_; ++i) - { - unsigned i_scc = sm_.scc_of_state(d.int_to_state[i]); + // skip trivial SCCs + if (is_trivial) + continue; - bool is_trivial = sm_.trivial(i_scc); - - for (int j = 1; j <= d.cand_size; ++j) - { - d.prodid[state_pair(j, i)] = ++d.nvars; - - // skip trivial SCCs - if (is_trivial) - continue; - - for (int k = 1; k <= size_; ++k) - { - if (sm_.scc_of_state(d.int_to_state[k]) != i_scc) - continue; - for (int l = 1; l <= d.cand_size; ++l) + for (unsigned k = 0; k < ref_size; ++k) + { + if (!sm.reachable_state(k)) + continue; + if (sm.scc_of(k) != i_scc) + continue; + for (unsigned l = 0; l < d.cand_size; ++l) { if (i == k && j == l) continue; @@ -288,51 +259,52 @@ namespace spot d.pathid_ref[p] = ++d.nvars; d.pathid_cand[p] = ++d.nvars; } - } - } - } + } + } + } - std::swap(d.state_to_int, seen); - - for (int i = 1; i <= d.cand_size; ++i) + for (unsigned i = 0; i < d.cand_size; ++i) { int transacc = -1; - if (state_based_) + if (state_based) // All outgoing transitions use the same acceptance variable. transacc = ++d.nvars; - for (int j = 1; j <= d.cand_size; ++j) + for (unsigned j = 0; j < d.cand_size; ++j) { bdd all = bddtrue; while (all != bddfalse) { - bdd one = bdd_satoneset(all, ap_, bddfalse); + bdd one = bdd_satoneset(all, ap, bddfalse); all -= one; transition t(i, one, j); d.transid[t] = ++d.nvars; d.revtransid.emplace(d.nvars, t); int ta = d.transacc[t] = - state_based_ ? transacc : ++d.nvars; + state_based ? transacc : ++d.nvars; d.revtransacc.emplace(ta, t); } } } - } - }; + + return ref_size; + } typedef std::pair sat_stats; static - sat_stats dtba_to_sat(std::ostream& out, const_tgba_ptr ref, + sat_stats dtba_to_sat(std::ostream& out, + const const_tgba_digraph_ptr& ref, dict& d, bool state_based) { clause_counter nclauses; - int ref_size = 0; - scc_map sm(ref); - sm.build_map(); - bdd ap = sm.aprec_set_of(sm.initial()); + // Compute the AP used in the hard way. + bdd ap = bddtrue; + for (auto& t: ref->transitions()) + if (!ref->is_dead_transition(t)) + ap &= bdd_support(t.cond); // Count the number of atomic propositions int nap = 0; @@ -346,12 +318,10 @@ namespace spot nap = 1 << nap; } - // Number all the SAT variable we may need. - { - filler_dfs f(ref, d, ap, state_based, sm); - f.run(); - ref_size = f.size(); - } + scc_info sm(ref); + + // Number all the SAT variables we may need. + unsigned ref_size = declare_vars(ref, d, ap, state_based, sm); // empty automaton is impossible if (d.cand_size == 0) @@ -370,14 +340,14 @@ namespace spot #endif dout << "symmetry-breaking clauses\n"; - int j = 0; + unsigned j = 0; bdd all = bddtrue; while (all != bddfalse) { bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; - for (int i = 1; i < d.cand_size; ++i) - for (int k = (i - 1) * nap + j + 3; k <= d.cand_size; ++k) + for (unsigned i = 0; i < d.cand_size - 1; ++i) + for (unsigned k = i * nap + j + 2; k < d.cand_size; ++k) { transition t(i, s, k); int ti = d.transid[t]; @@ -391,7 +361,7 @@ namespace spot dout << "(none)\n"; dout << "(1) the candidate automaton is complete\n"; - for (int q1 = 1; q1 <= d.cand_size; ++q1) + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) { bdd all = bddtrue; while (all != bddfalse) @@ -401,7 +371,7 @@ namespace spot #if DEBUG dout; - for (int q2 = 1; q2 <= d.cand_size; q2++) + for (unsigned q2 = 0; q2 < d.cand_size; q2++) { transition t(q1, s, q2); out << t << "δ"; @@ -411,7 +381,7 @@ namespace spot out << '\n'; #endif - for (int q2 = 1; q2 <= d.cand_size; q2++) + for (unsigned q2 = 0; q2 < d.cand_size; q2++) { transition t(q1, s, q2); int ti = d.transid[t]; @@ -425,31 +395,28 @@ namespace spot } dout << "(2) the initial state is reachable\n"; - dout << state_pair(1, 1) << '\n'; - out << d.prodid[state_pair(1, 1)] << " 0\n"; + dout << state_pair(0, 0) << '\n'; + out << d.prodid[state_pair(0, 0)] << " 0\n"; ++nclauses; for (std::map::const_iterator pit = d.prodid.begin(); pit != d.prodid.end(); ++pit) { - int q1 = pit->first.a; - int q1p = pit->first.b; + unsigned q1 = pit->first.a; + unsigned q1p = pit->first.b; dout << "(3) augmenting paths based on Cand[" << q1 << "] and Ref[" << q1p << "]\n"; - for (auto it: ref->succ(d.int_to_state[q1p])) + for (auto& tr: ref->out(q1p)) { - const state* dps = it->current_state(); - int dp = d.state_to_int[dps]; - dps->destroy(); - - bdd all = it->current_condition(); + unsigned dp = tr.dst; + bdd all = tr.cond; while (all != bddfalse) { bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; - for (int q2 = 1; q2 <= d.cand_size; q2++) + for (unsigned q2 = 0; q2 < d.cand_size; q2++) { transition t(q1, s, q2); int ti = d.transid[t]; @@ -474,19 +441,23 @@ namespace spot // construction of contraints (4,5) : all loops in the product // where no accepting run is detected in the ref. automaton, // must also be marked as not accepting in the cand. automaton - for (int q1p = 1; q1p <= ref_size; ++q1p) + for (unsigned q1p = 0; q1p < ref_size; ++q1p) { - unsigned q1p_scc = sm.scc_of_state(d.int_to_state[q1p]); - if (sm.trivial(q1p_scc)) + if (!sm.reachable_state(q1p)) continue; - for (int q2p = 1; q2p <= ref_size; ++q2p) + unsigned q1p_scc = sm.scc_of(q1p); + if (sm.is_trivial(q1p_scc)) + continue; + for (unsigned q2p = 0; q2p < ref_size; ++q2p) { + if (!sm.reachable_state(q2p)) + continue; // We are only interested in transition that can form a // cycle, so they must belong to the same SCC. - if (sm.scc_of_state(d.int_to_state[q2p]) != q1p_scc) + if (sm.scc_of(q2p) != q1p_scc) continue; - for (int q1 = 1; q1 <= d.cand_size; ++q1) - for (int q2 = 1; q2 <= d.cand_size; ++q2) + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) { path p1(q1, q1p, q2, q2p); @@ -499,25 +470,20 @@ namespace spot else pid1 = d.pathid_ref[p1]; - for (auto it: ref->succ(d.int_to_state[q2p])) + for (auto& tr: ref->out(q2p)) { - const state* dps = it->current_state(); + unsigned dp = tr.dst; // Skip destinations not in the SCC. - if (sm.scc_of_state(dps) != q1p_scc) - { - dps->destroy(); - continue; - } - int dp = d.state_to_int[dps]; - dps->destroy(); - - if (it->current_acceptance_conditions() == all_acc) + if (sm.scc_of(dp) != q1p_scc) continue; - for (int q3 = 1; q3 <= d.cand_size; ++q3) + + if (tr.acc == all_acc) + continue; + for (unsigned q3 = 0; q3 < d.cand_size; ++q3) { if (dp == q1p && q3 == q1) // (4) looping { - bdd all = it->current_condition(); + bdd all = tr.cond; while (all != bddfalse) { bdd s = bdd_satoneset(all, ap, bddfalse); @@ -544,7 +510,7 @@ namespace spot if (pid1 == pid2) continue; - bdd all = it->current_condition(); + bdd all = tr.cond; while (all != bddfalse) { bdd s = bdd_satoneset(all, ap, bddfalse); @@ -568,19 +534,23 @@ namespace spot // construction of contraints (6,7): all loops in the product // where accepting run is detected in the ref. automaton, must // also be marked as accepting in the candidate. - for (int q1p = 1; q1p <= ref_size; ++q1p) + for (unsigned q1p = 0; q1p < ref_size; ++q1p) { - unsigned q1p_scc = sm.scc_of_state(d.int_to_state[q1p]); - if (sm.trivial(q1p_scc)) + if (!sm.reachable_state(q1p)) continue; - for (int q2p = 1; q2p <= ref_size; ++q2p) + unsigned q1p_scc = sm.scc_of(q1p); + if (sm.is_trivial(q1p_scc)) + continue; + for (unsigned q2p = 0; q2p < ref_size; ++q2p) { + if (!sm.reachable_state(q2p)) + continue; // We are only interested in transition that can form a // cycle, so they must belong to the same SCC. - if (sm.scc_of_state(d.int_to_state[q2p]) != q1p_scc) + if (sm.scc_of(q2p) != q1p_scc) continue; - for (int q1 = 1; q1 <= d.cand_size; ++q1) - for (int q2 = 1; q2 <= d.cand_size; ++q2) + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) { path p1(q1, q1p, q2, q2p); dout << "(6&7) matching paths from candidate based on " @@ -592,27 +562,21 @@ namespace spot else pid1 = d.pathid_cand[p1]; - for (auto it: ref->succ(d.int_to_state[q2p])) + for (auto& tr: ref->out(q2p)) { - const state* dps = it->current_state(); + unsigned dp = tr.dst; // Skip destinations not in the SCC. - if (sm.scc_of_state(dps) != q1p_scc) - { - dps->destroy(); - continue; - } - int dp = d.state_to_int[dps]; - dps->destroy(); - for (int q3 = 1; q3 <= d.cand_size; q3++) + if (sm.scc_of(dp) != q1p_scc) + continue; + for (unsigned q3 = 0; q3 < d.cand_size; q3++) { if (dp == q1p && q3 == q1) // (6) looping { // We only care about the looping case if // it is accepting in the reference. - if (it->current_acceptance_conditions() - != all_acc) + if (tr.acc != all_acc) continue; - bdd all = it->current_condition(); + bdd all = tr.cond; while (all != bddfalse) { bdd s = bdd_satoneset(all, ap, bddfalse); @@ -637,7 +601,7 @@ namespace spot if (pid1 == pid2) continue; - bdd all = it->current_condition(); + bdd all = tr.cond; while (all != bddfalse) { bdd s = bdd_satoneset(all, ap, bddfalse); @@ -667,7 +631,7 @@ namespace spot static tgba_digraph_ptr sat_build(const satsolver::solution& solution, dict& satdict, - const_tgba_ptr aut, bool state_based) + const_tgba_digraph_ptr aut, bool state_based) { auto autdict = aut->get_dict(); auto a = make_tgba_digraph(autdict); @@ -710,7 +674,7 @@ namespace spot && acc_states.find(t->second.src) != acc_states.end(); last_aut_trans = - a->new_acc_transition(t->second.src - 1, t->second.dst - 1, + a->new_acc_transition(t->second.src, t->second.dst, t->second.cond, accept); last_sat_trans = &t->second; @@ -770,8 +734,8 @@ namespace spot } tgba_digraph_ptr - dtba_sat_synthetize(const const_tgba_ptr& a, int target_state_number, - bool state_based) + dtba_sat_synthetize(const const_tgba_digraph_ptr& a, + int target_state_number, bool state_based) { if (target_state_number == 0) return nullptr; @@ -828,7 +792,7 @@ namespace spot } tgba_digraph_ptr - dtba_sat_minimize(const const_tgba_ptr& a, bool state_based) + dtba_sat_minimize(const const_tgba_digraph_ptr& a, bool state_based) { int n_states = stats_reachable(a).states; @@ -847,7 +811,8 @@ namespace spot } tgba_digraph_ptr - dtba_sat_minimize_dichotomy(const const_tgba_ptr& a, bool state_based) + dtba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a, + bool state_based) { int max_states = stats_reachable(a).states - 1; int min_states = 1; diff --git a/src/tgbaalgos/dtbasat.hh b/src/tgbaalgos/dtbasat.hh index 65edfa939..effb8302c 100644 --- a/src/tgbaalgos/dtbasat.hh +++ b/src/tgbaalgos/dtbasat.hh @@ -41,7 +41,7 @@ namespace spot /// If no equivalent deterministic TBA with \a target_state_number /// states is found, a null pointer SPOT_API tgba_digraph_ptr - dtba_sat_synthetize(const const_tgba_ptr& a, + dtba_sat_synthetize(const const_tgba_digraph_ptr& a, int target_state_number, bool state_based = false); @@ -52,7 +52,8 @@ namespace spot /// /// If no smaller TBA exist, this returns a null pointer. SPOT_API tgba_digraph_ptr - dtba_sat_minimize(const const_tgba_ptr& a, bool state_based = false); + dtba_sat_minimize(const const_tgba_digraph_ptr& a, + bool state_based = false); /// \brief Attempt to minimize a deterministic TBA with a SAT solver. /// @@ -61,7 +62,7 @@ namespace spot // /// If no smaller TBA exist, this returns a null pointer. SPOT_API tgba_digraph_ptr - dtba_sat_minimize_dichotomy(const const_tgba_ptr& a, + dtba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a, bool state_based = false); } diff --git a/src/tgbaalgos/dtgbasat.cc b/src/tgbaalgos/dtgbasat.cc index 0502f3af6..d1251a847 100644 --- a/src/tgbaalgos/dtgbasat.cc +++ b/src/tgbaalgos/dtgbasat.cc @@ -24,7 +24,7 @@ #include "reachiter.hh" #include #include -#include "scc.hh" +#include "sccinfo.hh" #include "tgba/bddprint.hh" #include "ltlast/constant.hh" #include "stats.hh" @@ -60,9 +60,9 @@ namespace spot struct transition { - int src; + unsigned src; bdd cond; - int dst; + unsigned dst; transition(int src, bdd cond, int dst) : src(src), cond(cond), dst(dst) @@ -92,7 +92,7 @@ namespace spot struct src_cond { - int src; + unsigned src; bdd cond; src_cond(int src, bdd cond) @@ -118,10 +118,10 @@ namespace spot struct transition_acc { - int src; + unsigned src; bdd cond; bdd acc; - int dst; + unsigned dst; transition_acc(int src, bdd cond, bdd acc, int dst) : src(src), cond(cond), acc(acc), dst(dst) @@ -156,22 +156,22 @@ namespace spot struct path { - int src_cand; - int src_ref; - int dst_cand; - int dst_ref; + unsigned src_cand; + unsigned src_ref; + unsigned dst_cand; + unsigned dst_ref; bdd acc_cand; bdd acc_ref; - path(int src_cand, int src_ref) + path(unsigned src_cand, unsigned src_ref) : src_cand(src_cand), src_ref(src_ref), dst_cand(src_cand), dst_ref(src_ref), acc_cand(bddfalse), acc_ref(bddfalse) { } - path(int src_cand, int src_ref, - int dst_cand, int dst_ref, + path(unsigned src_cand, unsigned src_ref, + unsigned dst_cand, unsigned dst_ref, bdd acc_cand, bdd acc_ref) : src_cand(src_cand), src_ref(src_ref), dst_cand(dst_cand), dst_ref(dst_ref), @@ -259,13 +259,13 @@ namespace spot rev_acc_map revtransaccid; std::map pathid; - int nvars; - typedef std::unordered_map state_map; - typedef std::unordered_map int_map; - state_map state_to_int; - int_map int_to_state; - int cand_size; + int nvars = 0; + //typedef std::unordered_map state_map; + //typedef std::unordered_map int_map; + //state_map state_to_int; + // int_map int_to_state; + unsigned cand_size; unsigned int cand_nacc; std::vector cand_acc; // size cand_nacc @@ -275,206 +275,185 @@ namespace spot bdd cand_all_acc; bdd ref_all_acc; + std::vector is_weak_scc; + ~dict() { - state_map::const_iterator s = state_to_int.begin(); - while (s != state_to_int.end()) - // Always advance the iterator before deleting the key. - s++->first->destroy(); - aut->get_dict()->unregister_all_my_variables(this); } }; - class filler_dfs: public tgba_reachable_iterator_depth_first + unsigned declare_vars(const const_tgba_digraph_ptr& aut, + dict& d, bdd ap, bool state_based, scc_info& sm) { - protected: - dict& d; - int size_; - bdd ap_; - bool state_based_; - scc_map& sm_; - public: - filler_dfs(const const_tgba_ptr& aut, dict& d, bdd ap, bool state_based, - scc_map& sm) - : tgba_reachable_iterator_depth_first(aut), d(d), ap_(ap), - state_based_(state_based), sm_(sm) - { - d.nvars = 0; + bdd_dict_ptr bd = aut->get_dict(); + ltl::default_environment& env = ltl::default_environment::instance(); - bdd_dict_ptr bd = aut->get_dict(); - ltl::default_environment& env = ltl::default_environment::instance(); + d.cand_acc.resize(d.cand_nacc); + d.all_cand_acc.push_back(bddfalse); - d.cand_acc.resize(d.cand_nacc); - d.all_cand_acc.push_back(bddfalse); + bdd allneg = bddtrue; + for (unsigned n = 0; n < d.cand_nacc; ++n) + { + std::ostringstream s; + s << n; + const ltl::formula* af = env.require(s.str()); + int v = bd->register_acceptance_variable(af, &d); + af->destroy(); + d.cand_acc[n] = bdd_ithvar(v); + allneg &= bdd_nithvar(v); + } + for (unsigned n = 0; n < d.cand_nacc; ++n) + { + bdd c = bdd_exist(allneg, d.cand_acc[n]) & d.cand_acc[n]; + d.cand_acc[n] = c; - bdd allneg = bddtrue; - for (unsigned n = 0; n < d.cand_nacc; ++n) - { - std::ostringstream s; - s << n; - const ltl::formula* af = env.require(s.str()); - int v = bd->register_acceptance_variable(af, &d); - af->destroy(); - d.cand_acc[n] = bdd_ithvar(v); - allneg &= bdd_nithvar(v); - } - for (unsigned n = 0; n < d.cand_nacc; ++n) - { - bdd c = bdd_exist(allneg, d.cand_acc[n]) & d.cand_acc[n]; - d.cand_acc[n] = c; + size_t s = d.all_cand_acc.size(); + for (size_t i = 0; i < s; ++i) + d.all_cand_acc.push_back(d.all_cand_acc[i] | c); + } + d.cand_all_acc = bdd_support(allneg); + d.ref_all_acc = bdd_support(aut->all_acceptance_conditions()); - size_t s = d.all_cand_acc.size(); - for (size_t i = 0; i < s; ++i) - d.all_cand_acc.push_back(d.all_cand_acc[i] | c); - } - d.cand_all_acc = bdd_support(allneg); - d.ref_all_acc = bdd_support(aut->all_acceptance_conditions()); + bdd refall = d.ref_all_acc; + bdd refnegall = aut->neg_acceptance_conditions(); - bdd refall = d.ref_all_acc; - bdd refnegall = aut->neg_acceptance_conditions(); + d.all_ref_acc.push_back(bddfalse); + while (refall != bddtrue) + { + bdd v = bdd_ithvar(bdd_var(refall)); + bdd c = bdd_exist(refnegall, v) & v; - d.all_ref_acc.push_back(bddfalse); - while (refall != bddtrue) - { - bdd v = bdd_ithvar(bdd_var(refall)); - bdd c = bdd_exist(refnegall, v) & v; + size_t s = d.all_ref_acc.size(); + for (size_t i = 0; i < s; ++i) + d.all_ref_acc.push_back(d.all_ref_acc[i] | c); - size_t s = d.all_ref_acc.size(); - for (size_t i = 0; i < s; ++i) - d.all_ref_acc.push_back(d.all_ref_acc[i] | c); + refall = bdd_high(refall); + } - refall = bdd_high(refall); - } - } + unsigned ref_size = aut->num_states(); - int size() - { - return size_; - } + if (d.cand_size == -1U) + for (unsigned i = 0; i < ref_size; ++i) + if (sm.reachable_state(i)) + ++d.cand_size; // Note that we start from -1U the + // cand_size is one less than the + // number of reachable states. - void end() - { - size_ = seen.size(); + for (unsigned i = 0; i < ref_size; ++i) + { + if (!sm.reachable_state(i)) + continue; + unsigned i_scc = sm.scc_of(i); + bool is_weak = d.is_weak_scc[i_scc]; - if (d.cand_size == -1) - d.cand_size = size_ - 1; + for (unsigned j = 0; j < d.cand_size; ++j) + { + for (unsigned k = 0; k < ref_size; ++k) + { + if (!sm.reachable_state(k)) + continue; + if (sm.scc_of(k) != i_scc) + continue; + for (unsigned l = 0; l < d.cand_size; ++l) + { + size_t sfp = is_weak ? 1 : d.all_ref_acc.size(); + for (size_t fp = 0; fp < sfp; ++fp) + { + size_t sf = d.all_cand_acc.size(); + for (size_t f = 0; f < sf; ++f) + { + path p(j, i, l, k, + d.all_cand_acc[f], + d.all_ref_acc[fp]); + d.pathid[p] = ++d.nvars; + } - for (dict::state_map::const_iterator i2 = seen.begin(); - i2 != seen.end(); ++i2) - d.int_to_state[i2->second] = i2->first; + } + } + } + } + } - for (int i = 1; i <= size_; ++i) - { - unsigned i_scc = sm_.scc_of_state(d.int_to_state[i]); - bool is_weak = is_weak_scc(sm_, i_scc); - - for (int j = 1; j <= d.cand_size; ++j) + if (!state_based) + { + for (unsigned i = 0; i < d.cand_size; ++i) + for (unsigned j = 0; j < d.cand_size; ++j) { - for (int k = 1; k <= size_; ++k) + bdd all = bddtrue; + while (all != bddfalse) { - if (sm_.scc_of_state(d.int_to_state[k]) != i_scc) - continue; - for (int l = 1; l <= d.cand_size; ++l) - { - size_t sfp = is_weak ? 1 : d.all_ref_acc.size(); - for (size_t fp = 0; fp < sfp; ++fp) - { - size_t sf = d.all_cand_acc.size(); - for (size_t f = 0; f < sf; ++f) - { - path p(j, i, l, k, - d.all_cand_acc[f], - d.all_ref_acc[fp]); - d.pathid[p] = ++d.nvars; - } + bdd one = bdd_satoneset(all, ap, bddfalse); + all -= one; - } + transition t(i, one, j); + d.transid[t] = ++d.nvars; + d.revtransid.emplace(d.nvars, t); + + // Create the variable for the accepting transition + // immediately afterwards. It helps parsing the + // result. + for (unsigned n = 0; n < d.cand_nacc; ++n) + { + transition_acc ta(i, one, d.cand_acc[n], j); + d.transaccid[ta] = ++d.nvars; + d.revtransaccid.emplace(d.nvars, ta); } } } - } + } + else // state based + { + for (unsigned i = 0; i < d.cand_size; ++i) + for (unsigned n = 0; n < d.cand_nacc; ++n) + { + ++d.nvars; + for (unsigned j = 1; j < d.cand_size; ++j) + { + bdd all = bddtrue; + while (all != bddfalse) + { + bdd one = bdd_satoneset(all, ap, bddfalse); + all -= one; - std::swap(d.state_to_int, seen); + transition_acc ta(i, one, d.cand_acc[n], j); + d.transaccid[ta] = d.nvars; + d.revtransaccid.emplace(d.nvars, ta); + } + } + } + for (unsigned i = 0; i < d.cand_size; ++i) + for (unsigned j = 0; j < d.cand_size; ++j) + { + bdd all = bddtrue; + while (all != bddfalse) + { + bdd one = bdd_satoneset(all, ap, bddfalse); + all -= one; - if (!state_based_) - { - for (int i = 1; i <= d.cand_size; ++i) - for (int j = 1; j <= d.cand_size; ++j) - { - bdd all = bddtrue; - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, ap_, bddfalse); - all -= one; - - transition t(i, one, j); - d.transid[t] = ++d.nvars; - d.revtransid.emplace(d.nvars, t); - - // Create the variable for the accepting transition - // immediately afterwards. It helps parsing the - // result. - for (unsigned n = 0; n < d.cand_nacc; ++n) - { - transition_acc ta(i, one, d.cand_acc[n], j); - d.transaccid[ta] = ++d.nvars; - d.revtransaccid.emplace(d.nvars, ta); - } - } - } - } - else // state based - { - for (int i = 1; i <= d.cand_size; ++i) - for (unsigned n = 0; n < d.cand_nacc; ++n) - { - ++d.nvars; - for (int j = 1; j <= d.cand_size; ++j) - { - bdd all = bddtrue; - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, ap_, bddfalse); - all -= one; - - transition_acc ta(i, one, d.cand_acc[n], j); - d.transaccid[ta] = d.nvars; - d.revtransaccid.emplace(d.nvars, ta); - } - } - } - for (int i = 1; i <= d.cand_size; ++i) - for (int j = 1; j <= d.cand_size; ++j) - { - bdd all = bddtrue; - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, ap_, bddfalse); - all -= one; - - transition t(i, one, j); - d.transid[t] = ++d.nvars; - d.revtransid.emplace(d.nvars, t); - } - } - } - } - }; + transition t(i, one, j); + d.transid[t] = ++d.nvars; + d.revtransid.emplace(d.nvars, t); + } + } + } + return ref_size; + } typedef std::pair sat_stats; static - sat_stats dtgba_to_sat(std::ostream& out, const_tgba_ptr ref, + sat_stats dtgba_to_sat(std::ostream& out, const_tgba_digraph_ptr ref, dict& d, bool state_based) { clause_counter nclauses; - int ref_size = 0; - scc_map sm(ref); - sm.build_map(); - bdd ap = sm.aprec_set_of(sm.initial()); + // Compute the AP used in the hard way. + bdd ap = bddtrue; + for (auto& t: ref->transitions()) + if (!ref->is_dead_transition(t)) + ap &= bdd_support(t.cond); // Count the number of atomic propositions int nap = 0; @@ -488,12 +467,11 @@ namespace spot nap = 1 << nap; } - // Number all the SAT variable we may need. - { - filler_dfs f(ref, d, ap, state_based, sm); - f.run(); - ref_size = f.size(); - } + scc_info sm(ref); + d.is_weak_scc = sm.weak_sccs(); + + // Number all the SAT variables we may need. + unsigned ref_size = declare_vars(ref, d, ap, state_based, sm); // empty automaton is impossible if (d.cand_size == 0) @@ -518,8 +496,8 @@ namespace spot { bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; - for (int i = 1; i < d.cand_size; ++i) - for (int k = (i - 1) * nap + j + 3; k <= d.cand_size; ++k) + for (unsigned i = 0; i < d.cand_size - 1; ++i) + for (unsigned k = i * nap + j + 2; k < d.cand_size; ++k) { transition t(i, s, k); int ti = d.transid[t]; @@ -533,7 +511,7 @@ namespace spot dout << "(none)\n"; dout << "(8) the candidate automaton is complete\n"; - for (int q1 = 1; q1 <= d.cand_size; ++q1) + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) { bdd all = bddtrue; while (all != bddfalse) @@ -543,7 +521,7 @@ namespace spot #if DEBUG dout; - for (int q2 = 1; q2 <= d.cand_size; q2++) + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) { transition t(q1, s, q2); out << t << "δ"; @@ -553,7 +531,7 @@ namespace spot out << '\n'; #endif - for (int q2 = 1; q2 <= d.cand_size; q2++) + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) { transition t(q1, s, q2); int ti = d.transid[t]; @@ -566,66 +544,69 @@ namespace spot } dout << "(9) the initial state is reachable\n"; - dout << path(1, 1) << '\n'; - out << d.pathid[path(1, 1)] << " 0\n"; + dout << path(0, 0) << '\n'; + out << d.pathid[path(0, 0)] << " 0\n"; ++nclauses; - for (int q1 = 1; q1 <= d.cand_size; ++q1) - for (int q1p = 1; q1p <= ref_size; ++q1p) - { - dout << "(10) augmenting paths based on Cand[" << q1 - << "] and Ref[" << q1p << "]\n"; - path p1(q1, q1p); - int p1id = d.pathid[p1]; + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) + for (unsigned q1p = 0; q1p < ref_size; ++q1p) + { + if (!sm.reachable_state(q1p)) + continue; + dout << "(10) augmenting paths based on Cand[" << q1 + << "] and Ref[" << q1p << "]\n"; + path p1(q1, q1p); + int p1id = d.pathid[p1]; - for (auto it: ref->succ(d.int_to_state[q1p])) - { - const state* dps = it->current_state(); - int dp = d.state_to_int[dps]; - dps->destroy(); + for (auto& tr: ref->out(q1p)) + { + unsigned dp = tr.dst; + bdd all = tr.cond; + while (all != bddfalse) + { + bdd s = bdd_satoneset(all, ap, bddfalse); + all -= s; - bdd all = it->current_condition(); - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) + { + transition t(q1, s, q2); + int ti = d.transid[t]; - for (int q2 = 1; q2 <= d.cand_size; q2++) - { - transition t(q1, s, q2); - int ti = d.transid[t]; + path p2(q2, dp); + int succ = d.pathid[p2]; - path p2(q2, dp); - int succ = d.pathid[p2]; + if (p1id == succ) + continue; - if (p1id == succ) - continue; - - dout << p1 << " ∧ " << t << "δ → " << p2 << '\n'; - out << -p1id << ' ' << -ti << ' ' << succ << " 0\n"; - ++nclauses; - } - } - } - } + dout << p1 << " ∧ " << t << "δ → " << p2 << '\n'; + out << -p1id << ' ' << -ti << ' ' << succ << " 0\n"; + ++nclauses; + } + } + } + } bdd all_acc = ref->all_acceptance_conditions(); // construction of constraints (11,12,13) - for (int q1p = 1; q1p <= ref_size; ++q1p) + for (unsigned q1p = 0; q1p < ref_size; ++q1p) { - unsigned q1p_scc = sm.scc_of_state(d.int_to_state[q1p]); - for (int q2p = 1; q2p <= ref_size; ++q2p) + if (!sm.reachable_state(q1p)) + continue; + unsigned q1p_scc = sm.scc_of(q1p); + for (unsigned q2p = 0; q2p < ref_size; ++q2p) { + if (!sm.reachable_state(q2p)) + continue; // We are only interested in transition that can form a // cycle, so they must belong to the same SCC. - if (sm.scc_of_state(d.int_to_state[q2p]) != q1p_scc) + if (sm.scc_of(q2p) != q1p_scc) continue; - bool is_weak = is_weak_scc(sm, q1p_scc); - bool is_acc = sm.accepting(q1p_scc); + bool is_weak = d.is_weak_scc[q1p_scc]; + bool is_acc = sm.is_accepting_scc(q1p_scc); - for (int q1 = 1; q1 <= d.cand_size; ++q1) - for (int q2 = 1; q2 <= d.cand_size; ++q2) + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) { size_t sf = d.all_cand_acc.size(); size_t sfp = is_weak ? 1 : d.all_ref_acc.size(); @@ -639,24 +620,17 @@ namespace spot int pid = d.pathid[p]; - for (auto it: ref->succ(d.int_to_state[q2p])) + for (auto& tr: ref->out(q2p)) { - const state* dps = it->current_state(); + unsigned dp = tr.dst; // Skip destinations not in the SCC. - if (sm.scc_of_state(dps) != q1p_scc) - { - dps->destroy(); - continue; - } - int dp = d.state_to_int[dps]; - dps->destroy(); + if (sm.scc_of(dp) != q1p_scc) + continue; - for (int q3 = 1; q3 <= d.cand_size; ++q3) + for (unsigned q3 = 0; q3 < d.cand_size; ++q3) { - bdd all = it->current_condition(); - bdd curacc = - it->current_acceptance_conditions(); - + bdd all = tr.cond; + bdd curacc = tr.acc; while (all != bddfalse) { bdd l = bdd_satoneset(all, ap, bddfalse); @@ -839,7 +813,7 @@ namespace spot static tgba_digraph_ptr sat_build(const satsolver::solution& solution, dict& satdict, - const_tgba_ptr aut, bool state_based) + const_tgba_digraph_ptr aut, bool state_based) { auto autdict = aut->get_dict(); auto a = make_tgba_digraph(autdict); @@ -888,8 +862,8 @@ namespace spot acc = i->second; } - last_aut_trans = a->new_transition(t->second.src - 1, - t->second.dst - 1, + last_aut_trans = a->new_transition(t->second.src, + t->second.dst, t->second.cond, acc); last_sat_trans = &t->second; @@ -936,8 +910,9 @@ namespace spot } tgba_digraph_ptr - dtgba_sat_synthetize (const const_tgba_ptr& a, unsigned target_acc_number, - int target_state_number, bool state_based) + dtgba_sat_synthetize(const const_tgba_digraph_ptr& a, + unsigned target_acc_number, + int target_state_number, bool state_based) { if (target_state_number == 0) return nullptr; @@ -997,7 +972,7 @@ namespace spot } tgba_digraph_ptr - dtgba_sat_minimize(const const_tgba_ptr& a, + dtgba_sat_minimize(const const_tgba_digraph_ptr& a, unsigned target_acc_number, bool state_based) { @@ -1019,7 +994,7 @@ namespace spot } tgba_digraph_ptr - dtgba_sat_minimize_dichotomy(const const_tgba_ptr& a, + dtgba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a, unsigned target_acc_number, bool state_based) { diff --git a/src/tgbaalgos/dtgbasat.hh b/src/tgbaalgos/dtgbasat.hh index 241dbc733..9e560f113 100644 --- a/src/tgbaalgos/dtgbasat.hh +++ b/src/tgbaalgos/dtgbasat.hh @@ -45,7 +45,7 @@ namespace spot /// equivalent to \a a. If no such TGBA is found, a null pointer is /// returned. SPOT_API tgba_digraph_ptr - dtgba_sat_synthetize(const const_tgba_ptr& a, + dtgba_sat_synthetize(const const_tgba_digraph_ptr& a, unsigned target_acc_number, int target_state_number, bool state_based = false); @@ -57,7 +57,7 @@ namespace spot /// /// If no smaller TGBA exist, this returns a null pointer. SPOT_API tgba_digraph_ptr - dtgba_sat_minimize(const const_tgba_ptr& a, + dtgba_sat_minimize(const const_tgba_digraph_ptr& a, unsigned target_acc_number, bool state_based = false); @@ -68,7 +68,7 @@ namespace spot // /// If no smaller TBA exist, this returns a null pointer. SPOT_API tgba_digraph_ptr - dtgba_sat_minimize_dichotomy(const const_tgba_ptr& a, + dtgba_sat_minimize_dichotomy(const const_tgba_digraph_ptr& a, unsigned target_acc_number, bool state_based = false); } diff --git a/src/tgbaalgos/sccinfo.cc b/src/tgbaalgos/sccinfo.cc index 0c1acce98..2d8a05a58 100644 --- a/src/tgbaalgos/sccinfo.cc +++ b/src/tgbaalgos/sccinfo.cc @@ -250,6 +250,17 @@ namespace spot return result; } + std::vector scc_info::weak_sccs() const + { + unsigned n = scc_count(); + std::vector result(scc_count()); + auto acc = used_acc(); + bdd all = bdd_support(aut_->neg_acceptance_conditions()); + for (unsigned s = 0; s < n; ++s) + result[s] = !is_accepting_scc(s) || acc[s] == all; + return result; + } + bdd scc_info::scc_ap_support(unsigned scc) const { bdd support = bddtrue; diff --git a/src/tgbaalgos/sccinfo.hh b/src/tgbaalgos/sccinfo.hh index 840410f68..09c7a2d1d 100644 --- a/src/tgbaalgos/sccinfo.hh +++ b/src/tgbaalgos/sccinfo.hh @@ -147,6 +147,8 @@ namespace spot /// at position #i. std::vector used_acc() const; + std::vector weak_sccs() const; + bdd scc_ap_support(unsigned scc) const; }; diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index 134ffedb6..fc2981ef3 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -1369,7 +1369,8 @@ checked_main(int argc, char** argv) if (opt_dtbasat >= 0) { tm.start("dtbasat"); - auto satminimized = dtba_sat_synthetize(a, opt_dtbasat); + auto satminimized = + dtba_sat_synthetize(ensure_digraph(a), opt_dtbasat); tm.stop("dtbasat"); if (satminimized) a = satminimized; @@ -1377,7 +1378,8 @@ checked_main(int argc, char** argv) else if (opt_dtgbasat >= 0) { tm.start("dtgbasat"); - auto satminimized = dtgba_sat_minimize(a, opt_dtgbasat); + auto satminimized = dtgba_sat_minimize(ensure_digraph(a), + opt_dtgbasat); tm.stop("dtgbasat"); if (satminimized) a = satminimized;