diff --git a/NEWS b/NEWS index aa16106f3..cc61c1236 100644 --- a/NEWS +++ b/NEWS @@ -100,6 +100,10 @@ New in spot 2.11.6.dev (not yet released) - spot::scc_info has a new option PROCESS_UNREACHABLE_STATES that causes it to enumerated even unreachable SCCs. + - spot::realizability_simplifier is a new class that performs the + removal of superfluous APs that is now performed by ltlsynt + (search for --polarity and --global-equivalence above). + Bugs fixed: - tgba_determinize()'s use_simulation option would cause it to diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc index 05d190994..0ff44625d 100644 --- a/bin/ltlsynt.cc +++ b/bin/ltlsynt.cc @@ -286,47 +286,15 @@ namespace static void dispatch_print_hoa(spot::twa_graph_ptr& game, - const std::vector* input_aps = nullptr, - const spot::relabeling_map* rm = nullptr) + const spot::realizability_simplifier* rs = nullptr) { // Add any AP we removed. This is a game, so player moves are // separated. Consequently at this point we cannot deal with // removed signals such as "o1 <-> i2": if the game has to be // printed, we can only optimize for signals such as o1 <-> o2. - if (rm && !rm->empty()) - { - assert(input_aps); - auto& sp = spot::get_state_players(game); + if (rs) + rs->patch_game(game); - bdd add = bddtrue; - for (auto [k, v]: *rm) - { - int i = game->register_ap(k); - // skip inputs - if (std::find(input_aps->begin(), input_aps->end(), - k.ap_name()) != input_aps->end()) - continue; - if (v.is_tt()) - add &= bdd_ithvar(i); - else if (v.is_ff()) - add &= bdd_nithvar(i); - else - { - bdd bv; - if (v.is(spot::op::ap)) - bv = bdd_ithvar(game->register_ap(v.ap_name())); - else // Not Ap - bv = bdd_nithvar(game->register_ap(v[0].ap_name())); - add &= bdd_biimp(bdd_ithvar(i), bv); - } - } - for (auto& e: game->edges()) - if (sp[e.src]) - e.cond &= add; - set_synthesis_outputs(game, - get_synthesis_outputs(game) - & bdd_support(add)); - } if (opt_dot) spot::print_dot(std::cout, game, opt_print_hoa_args); else if (opt_print_pg) @@ -429,168 +397,26 @@ namespace gi->bv->total_time = sw.stop(); }; - // Check if some output propositions are always in positive form, - // or always in negative form. - // In syntcomp, this occurs more frequently for input variables than - // output variable. See issue #529 for some examples. - - spot::relabeling_map rm; - bool first_dap = true; - auto display_ap = [&rm, &first_dap](spot::formula p) - { - if (SPOT_LIKELY(!gi->verbose_stream)) - return; - if (first_dap) - { - *gi->verbose_stream - << "the following signals can be temporarily removed:\n"; - first_dap = false; - } - *gi->verbose_stream << " " << p << " := " << rm[p] <<'\n'; - }; - spot::formula oldf; + // Attempt to remove superfluous atomic propositions + spot::realizability_simplifier* rs = nullptr; if (opt_polarity || opt_gequiv) { - robin_hood::unordered_set ap_inputs; - for (const std::string& ap: input_aps) - ap_inputs.insert(spot::formula::ap(ap)); - - do + unsigned opt = 0; + if (opt_polarity) + opt |= spot::realizability_simplifier::polarity; + if (opt_gequiv) { - bool rm_has_new_terms = false; - oldf = f; - - if (opt_polarity) - { - std::set lits = spot::collect_literals(f); - for (const std::string& ap: output_aps) - { - spot::formula pos = spot::formula::ap(ap); - spot::formula neg = spot::formula::Not(pos); - bool has_pos = lits.find(pos) != lits.end(); - bool has_neg = lits.find(neg) != lits.end(); - if (has_pos ^ has_neg) - { - rm[pos] = - has_pos ? spot::formula::tt() : spot::formula::ff(); - rm_has_new_terms = true; - display_ap(pos); - } - } - for (const std::string& ap: input_aps) - { - spot::formula pos = spot::formula::ap(ap); - spot::formula neg = spot::formula::Not(pos); - bool has_pos = lits.find(pos) != lits.end(); - bool has_neg = lits.find(neg) != lits.end(); - if (has_pos ^ has_neg) - { - rm[pos] = - has_neg ? spot::formula::tt() : spot::formula::ff(); - rm_has_new_terms = true; - display_ap(pos); - } - } - if (rm_has_new_terms) - { - f = spot::relabel_apply(f, &rm); - if (gi->verbose_stream) - *gi->verbose_stream << "new formula: " << f << '\n'; - rm_has_new_terms = false; - } - } - if (opt_gequiv) - { - // check for equivalent terms - spot::formula_ptr_less_than_bool_first cmp; - for (std::vector& equiv: - spot::collect_equivalent_literals(f)) - { - // For each set of equivalent literals, we want to - // pick a representative. That representative - // should be an input if one of the literal is an - // input. (If we have two inputs or more, the - // formula is not realizable.) - spot::formula repr = nullptr; - bool repr_is_input = false; - spot::formula input_seen = nullptr; - for (spot::formula lit: equiv) - { - spot::formula ap = lit; - if (ap.is(spot::op::Not)) - ap = ap[0]; - if (ap_inputs.find(ap) != ap_inputs.end()) - { - if (input_seen) - { - // ouch! we have two equivalent inputs. - // This means the formula is simply - // unrealizable. Make it false for the - // rest of the algorithm. - f = spot::formula::ff(); - goto done; - } - input_seen = lit; - // Normally, we want the input to be the - // representative. However as a special - // case, we ignore the input literal from - // the set if we are asked to print a - // game. Fixing the game to add a i<->o - // equivalence would require more code - // than I care to write. - // - // So if the set was {i,o1,o2}, instead - // of the desirable - // o1 := i - // o2 := i - // we only do - // o2 := o1 - // when printing games. - if (!want_game()) - { - repr_is_input = true; - repr = lit; - } - } - else if (!repr_is_input && (!repr || cmp(ap, repr))) - repr = lit; - } - // now map equivalent each atomic proposition to the - // representative - spot::formula not_repr = spot::formula::Not(repr); - for (spot::formula lit: equiv) - { - // input or representative are not removed - // (we have repr != input_seen either when input_seen - // is nullptr, or if want_game is true) - if (lit == repr || lit == input_seen) - continue; - if (lit.is(spot::op::Not)) - { - spot::formula ap = lit[0]; - rm[ap] = not_repr; - display_ap(ap); - } - else - { - rm[lit] = repr; - display_ap(lit); - } - rm_has_new_terms = true; - } - } - if (rm_has_new_terms) - { - f = spot::relabel_apply(f, &rm); - if (gi->verbose_stream) - *gi->verbose_stream << "new formula: " << f << '\n'; - rm_has_new_terms = false; - } - } + if (want_game()) + opt |= spot::realizability_simplifier::global_equiv_output_only; + else + opt |= spot::realizability_simplifier::global_equiv; } - while (oldf != f); - done: - /* can't have a label followed by closing brace */; + rs = + new spot::realizability_simplifier(original_f, + input_aps, + opt, + gi ? gi->verbose_stream : nullptr); + f = rs->simplified_formula(); } std::vector sub_form; @@ -617,11 +443,18 @@ namespace { sub_form = { f }; sub_outs.resize(1); - for (const std::string& apstr: output_aps) + if (rs) { - spot::formula ap = spot::formula::ap(apstr); - if (rm.find(ap) == rm.end()) - sub_outs[0].insert(ap); + robin_hood::unordered_set removed_outputs; + for (auto [from, from_is_input, to] : rs->get_mapping()) + if (!from_is_input) + removed_outputs.insert(from); + for (const std::string& apstr: output_aps) + { + spot::formula ap = spot::formula::ap(apstr); + if (removed_outputs.find(ap) == removed_outputs.end()) + sub_outs[0].insert(ap); + } } } std::vector> sub_outs_str; @@ -683,7 +516,7 @@ namespace } if (want_game()) { - dispatch_print_hoa(arena, &input_aps, &rm); + dispatch_print_hoa(arena, rs); continue; } if (!spot::solve_game(arena, *gi)) @@ -772,7 +605,7 @@ namespace sw2.start(); saig = spot::mealy_machines_to_aig(mealy_machines, opt_print_aiger, input_aps, - sub_outs_str, &rm); + sub_outs_str, rs); if (gi->bv) { gi->bv->aig_time = sw2.stop(); @@ -804,52 +637,8 @@ namespace for (size_t i = 1; i < mealy_machines.size(); ++i) tot_strat = spot::mealy_product(tot_strat, mealy_machines[i].mealy_like); - if (!rm.empty()) // Add any AP we removed - { - bdd add = bddtrue; - bdd additional_outputs = bddtrue; - for (auto [k, v]: rm) - { - int i = tot_strat->register_ap(k); - // skip inputs (they are don't care) - if (std::find(input_aps.begin(), input_aps.end(), k.ap_name()) - != input_aps.end()) - continue; - if (v.is_tt()) - { - bdd bv = bdd_ithvar(i); - additional_outputs &= bv; - add &= bv; - } - else if (v.is_ff()) - { - additional_outputs &= bdd_ithvar(i); - add &= bdd_nithvar(i); - } - else - { - bdd left = bdd_ithvar(i); // this is necessarily an output - additional_outputs &= left; - bool pos = v.is(spot::op::ap); - const std::string apname = - pos ? v.ap_name() : v[0].ap_name(); - bdd right = bdd_ithvar(tot_strat->register_ap(apname)); - // right might be an input - if (std::find(input_aps.begin(), input_aps.end(), apname) - == input_aps.end()) - additional_outputs &= right; - if (pos) - add &= bdd_biimp(left, right); - else - add &= bdd_xor(left, right); - } - } - for (auto& e: tot_strat->edges()) - e.cond &= add; - set_synthesis_outputs(tot_strat, - get_synthesis_outputs(tot_strat) - & additional_outputs); - } + if (rs) // Add any AP we removed + rs->patch_mealy(tot_strat); printer.print(tot_strat, timer_printer_dummy); } diff --git a/spot/tl/apcollect.cc b/spot/tl/apcollect.cc index 87d5e5b3e..0a2c2d259 100644 --- a/spot/tl/apcollect.cc +++ b/spot/tl/apcollect.cc @@ -28,6 +28,9 @@ #include #include #include +#include +#include +#include namespace spot { @@ -281,4 +284,232 @@ namespace spot return scc; } + realizability_simplifier::realizability_simplifier + (formula f, const std::vector& inputs, + unsigned options, std::ostream* verbose) + { + bool first_mapping = true; + relabeling_map rm; + auto add_to_mapping = [&](formula from, bool from_is_input, formula to) + { + mapping_.emplace_back(from, from_is_input, to); + rm[from] = to; + if (SPOT_LIKELY(!verbose)) + return; + if (first_mapping) + { + *verbose << "the following signals can be temporarily removed:\n"; + first_mapping = false; + } + *verbose << " " << from << " := " << to <<'\n'; + }; + global_equiv_output_only_ = + (options & global_equiv_output_only) == global_equiv_output_only; + + robin_hood::unordered_set ap_inputs; + for (const std::string& ap: inputs) + ap_inputs.insert(spot::formula::ap(ap)); + + formula oldf; + f_ = f; + do + { + bool rm_has_new_terms = false; + oldf = f_; + + if (options & polarity) + { + // Check if some output propositions are always in + // positive form, or always in negative form. In + // syntcomp, this occurs more frequently for input + // variables than output variable. See issue #529 for + // some examples. + std::set lits = spot::collect_literals(f_); + for (const formula& lit: lits) + if (lits.find(spot::formula::Not(lit)) == lits.end()) + { + formula ap = lit; + bool neg = false; + if (lit.is(op::Not)) + { + ap = lit[0]; + neg = true; + } + bool is_input = ap_inputs.find(ap) != ap_inputs.end(); + formula to = (is_input == neg) + ? spot::formula::tt() : spot::formula::ff(); + add_to_mapping(ap, is_input, to); + rm_has_new_terms = true; + } + if (rm_has_new_terms) + { + f_ = spot::relabel_apply(f_, &rm); + if (verbose) + *verbose << "new formula: " << f_ << '\n'; + rm_has_new_terms = false; + } + } + if (options & global_equiv) + { + // check for equivalent terms + spot::formula_ptr_less_than_bool_first cmp; + for (std::vector& equiv: + spot::collect_equivalent_literals(f_)) + { + // For each set of equivalent literals, we want to + // pick a representative. That representative + // should be an input if one of the literal is an + // input. (If we have two inputs or more, the + // formula is not realizable.) + spot::formula repr = nullptr; + bool repr_is_input = false; + spot::formula input_seen = nullptr; + for (spot::formula lit: equiv) + { + spot::formula ap = lit; + if (ap.is(spot::op::Not)) + ap = ap[0]; + if (ap_inputs.find(ap) != ap_inputs.end()) + { + if (input_seen) + { + // ouch! we have two equivalent inputs. + // This means the formula is simply + // unrealizable. Make it false for the + // rest of the algorithm. + f = spot::formula::ff(); + return; + } + input_seen = lit; + // Normally, we want the input to be the + // representative. However as a special + // case, we ignore the input literal from + // the set if we are asked to print a + // game. Fixing the game to add a i<->o + // equivalence would require more code + // than I care to write. + // + // So if the set was {i,o1,o2}, instead + // of the desirable + // o1 := i + // o2 := i + // we only do + // o2 := o1 + // when printing games. + if (!global_equiv_output_only_) + { + repr_is_input = true; + repr = lit; + } + } + else if (!repr_is_input && (!repr || cmp(ap, repr))) + repr = lit; + } + // now map equivalent each atomic proposition to the + // representative + spot::formula not_repr = spot::formula::Not(repr); + for (spot::formula lit: equiv) + { + // input or representative are not removed + // (we have repr != input_seen either when input_seen + // is nullptr, or if want_game is true) + if (lit == repr || lit == input_seen) + continue; + SPOT_ASSUME(lit != nullptr); + if (lit.is(spot::op::Not)) + add_to_mapping(lit[0], repr_is_input, not_repr); + else + add_to_mapping(lit, repr_is_input, repr); + rm_has_new_terms = true; + } + } + if (rm_has_new_terms) + { + f_ = spot::relabel_apply(f_, &rm); + if (verbose) + *verbose << "new formula: " << f_ << '\n'; + rm_has_new_terms = false; + } + } + } + while (oldf != f_); + } + + void realizability_simplifier::patch_mealy(twa_graph_ptr mealy) const + { + bdd add = bddtrue; + bdd additional_outputs = bddtrue; + for (auto [k, k_is_input, v]: mapping_) + { + int i = mealy->register_ap(k); + // skip inputs (they are don't care) + if (k_is_input) + continue; + if (v.is_tt()) + { + bdd bv = bdd_ithvar(i); + additional_outputs &= bv; + add &= bv; + } + else if (v.is_ff()) + { + additional_outputs &= bdd_ithvar(i); + add &= bdd_nithvar(i); + } + else + { + bdd left = bdd_ithvar(i); // this is necessarily an output + additional_outputs &= left; + bool pos = v.is(spot::op::ap); + const std::string apname = + pos ? v.ap_name() : v[0].ap_name(); + bdd right = bdd_ithvar(mealy->register_ap(apname)); + if (pos) + add &= bdd_biimp(left, right); + else + add &= bdd_xor(left, right); + } + } + for (auto& e: mealy->edges()) + e.cond &= add; + set_synthesis_outputs(mealy, + get_synthesis_outputs(mealy) + & additional_outputs); + } + + void realizability_simplifier::patch_game(twa_graph_ptr game) const + { + if (SPOT_UNLIKELY(!global_equiv_output_only_)) + throw std::runtime_error("realizability_simplifier::path_game() requires " + "option global_equiv_output_only"); + + auto& sp = spot::get_state_players(game); + bdd add = bddtrue; + for (auto [k, k_is_input, v]: mapping_) + { + int i = game->register_ap(k); + if (k_is_input) + continue; + if (v.is_tt()) + add &= bdd_ithvar(i); + else if (v.is_ff()) + add &= bdd_nithvar(i); + else + { + bdd bv; + if (v.is(spot::op::ap)) + bv = bdd_ithvar(game->register_ap(v.ap_name())); + else // Not Ap + bv = bdd_nithvar(game->register_ap(v[0].ap_name())); + add &= bdd_biimp(bdd_ithvar(i), bv); + } + } + for (auto& e: game->edges()) + if (sp[e.src]) + e.cond &= add; + set_synthesis_outputs(game, + get_synthesis_outputs(game) + & bdd_support(add)); + } + } diff --git a/spot/tl/apcollect.hh b/spot/tl/apcollect.hh index 7cc8ccb3c..b155de551 100644 --- a/spot/tl/apcollect.hh +++ b/spot/tl/apcollect.hh @@ -78,5 +78,51 @@ namespace spot SPOT_API std::vector> collect_equivalent_literals(formula f); + + + + /// \brief Simplify a reactive specification, preserving realizability + class SPOT_API realizability_simplifier final + { + public: + enum realizability_simplifier_option { + /// \brief remove APs with single polarity + polarity = 0b1, + /// \brief remove equivalent APs + global_equiv = 0b10, + /// \brief likewise, but don't consider equivalent input and output + global_equiv_output_only = 0b110, + }; + + realizability_simplifier(formula f, + const std::vector& inputs, + unsigned options = polarity | global_equiv, + std::ostream* verbose = nullptr); + + /// \brief Return the simplified formula. + formula simplified_formula() const + { + return f_; + } + + /// \brief Returns a vector of (from,from_is_input,to) + const std::vector>& get_mapping() const + { + return mapping_; + } + + /// \brief Patch a Mealy machine to add the missing APs. + void patch_mealy(twa_graph_ptr mealy) const; + + /// \brief Patch a game to add the missing APs. + void patch_game(twa_graph_ptr mealy) const; + + private: + void add_to_mapping(formula from, bool from_is_input, formula to); + std::vector> mapping_; + formula f_; + bool global_equiv_output_only_; + }; + /// @} } diff --git a/spot/twaalgos/aiger.cc b/spot/twaalgos/aiger.cc index 455400f7d..49ac54997 100644 --- a/spot/twaalgos/aiger.cc +++ b/spot/twaalgos/aiger.cc @@ -1545,7 +1545,7 @@ namespace const char* mode, const std::vector& unused_ins = {}, const std::vector& unused_outs = {}, - const relabeling_map* rm = nullptr) + const realizability_simplifier* rs = nullptr) { // The aiger circuit can currently noly encode separated mealy machines @@ -1620,19 +1620,19 @@ namespace unused_outs.cbegin(), unused_outs.cend()); - if (rm) + if (rs) // If we have removed some APs from the original formula, they // might have dropped out of the output_names list (depending on // how we split the formula), but they should not have dropped // from the input_names list. So let's fix the output_names // lists by adding anything that's not an input and not already // there. - for (auto [k, v]: *rm) + for (auto [k, k_is_input, v]: rs->get_mapping()) { + if (k_is_input) + continue; const std::string s = k.ap_name(); - if (std::find(input_names_all.begin(), input_names_all.end(), s) - == input_names_all.end() - && std::find(output_names_all.begin(), output_names_all.end(), s) + if (std::find(output_names_all.begin(), output_names_all.end(), s) == output_names_all.end()) output_names_all.push_back(s); } @@ -1985,93 +1985,79 @@ namespace // Reset them for (unsigned i = 0; i < n_outs; ++i) circuit.set_output(i, bdd2var_min(out[i], out_dc[i])); - // Add the unused propositions - // - // RM contains assignments like + + // Set unused signal to false by default + const unsigned n_outs_all = output_names_all.size(); + for (unsigned i = n_outs; i < n_outs_all; ++i) + circuit.set_output(i, circuit.aig_false()); + + // RS may contains assignments for unused signals, such as // out1 := 1 // out2 := 0 // out3 := in1 // out4 := !out3 - // but it is possible that the rhs could refer to a variable - // that is not yet defined because of the ordering. For - // this reason, the first pass will store signals it could not - // complete in the POSTPONE vector. - // - // In that vector, (u,v,b) means that output u should be mapped to - // the same formula as output v, possibly negated (if b). - std::vector> postpone; + // But because the formula is simplified in a loop (forcing + // some of those values in the formula reveal more values to + // be forced), it is possible that the rhs refers to a variable + // that is forced later in the mapping. Therefore the mapping + // should be applied in reverse order. + if (rs) + { + auto mapping = rs->get_mapping(); + for (auto it = mapping.rbegin(); it != mapping.rend(); ++it) + { + auto [from, from_is_input, to] = *it; + if (from_is_input) + continue; - const unsigned n_outs_all = output_names_all.size(); - for (unsigned i = n_outs; i < n_outs_all; ++i) - if (rm) - { - if (auto to = rm->find(formula::ap(output_names_all[i])); - to != rm->end()) - { - if (to->second.is_tt()) - { - circuit.set_output(i, circuit.aig_true()); - continue; - } - else if (to->second.is_ff()) - { - circuit.set_output(i, circuit.aig_false()); - continue; - } - else - { - formula repr = to->second; - bool neg_repr = false; + auto j = std::find(output_names_all.begin(), + output_names_all.end(), + from.ap_name()); + assert(j != output_names_all.end()); + int i = j - output_names_all.begin(); + if (to.is_tt()) + { + circuit.set_output(i, circuit.aig_true()); + continue; + } + else if (to.is_ff()) + { + circuit.set_output(i, circuit.aig_false()); + continue; + } + else + { + formula repr = to; + bool neg_repr = false; if (repr.is(op::Not)) { neg_repr = true; repr = repr[0]; } // is repr an input? - if (auto it = std::find(input_names_all.begin(), + if (auto it2 = std::find(input_names_all.begin(), input_names_all.end(), repr.ap_name()); - it != input_names_all.end()) + it2 != input_names_all.end()) { unsigned ivar = - circuit.input_var(it - input_names_all.begin(), + circuit.input_var(it2 - input_names_all.begin(), neg_repr); circuit.set_output(i, ivar); } // is repr an output? - else if (auto it = std::find(output_names_all.begin(), - output_names_all.end(), - repr.ap_name()); - it != output_names_all.end()) + else { - unsigned outnum = it - output_names_all.begin(); + assert(std::find(output_names_all.begin(), + output_names_all.end(), + repr.ap_name()) == + output_names_all.end()); + unsigned outnum = it2 - output_names_all.begin(); unsigned outvar = circuit.output(outnum); - if (outvar == -1u) - postpone.emplace_back(i, outnum, neg_repr); - else - circuit.set_output(i, outvar + neg_repr); + circuit.set_output(i, outvar + neg_repr); } - } - } - } - else - circuit.set_output(i, circuit.aig_false()); - unsigned postponed = postpone.size(); - while (postponed) - { - unsigned postponed_again = 0; - for (auto [u, v, b]: postpone) - { - unsigned outvar = circuit.output(v); - if (outvar == -1u) - ++postponed_again; - else - circuit.set_output(u, outvar + b); + } } - if (postponed_again >= postponed) - throw std::runtime_error("aiger encoding bug: " - "postponed output shunts not decreasing"); - postponed = postponed_again; } for (unsigned i = 0; i < n_latches; ++i) circuit.set_next_latch(i, bdd2var_min(latch[i], bddfalse)); @@ -2106,7 +2092,7 @@ namespace spot mealy_machine_to_aig(const twa_graph_ptr &m, const char *mode, const std::vector& ins, const std::vector& outs, - const relabeling_map* rm) + const realizability_simplifier* rs) { if (!m) throw std::runtime_error("mealy_machine_to_aig(): " @@ -2139,20 +2125,20 @@ namespace spot } // todo Some additional checks? return auts_to_aiger({{m, get_synthesis_outputs(m)}}, mode, - unused_ins, unused_outs, rm); + unused_ins, unused_outs, rs); } aig_ptr mealy_machine_to_aig(mealy_like& m, const char *mode, const std::vector& ins, const std::vector& outs, - const relabeling_map* rm) + const realizability_simplifier* rs) { if (m.success != mealy_like::realizability_code::REALIZABLE_REGULAR) throw std::runtime_error("mealy_machine_to_aig(): " "Can only handle regular mealy machine, yet."); - return mealy_machine_to_aig(m.mealy_like, mode, ins, outs, rm); + return mealy_machine_to_aig(m.mealy_like, mode, ins, outs, rs); } aig_ptr @@ -2212,7 +2198,7 @@ namespace spot const char *mode, const std::vector& ins, const std::vector>& outs, - const relabeling_map* rm) + const realizability_simplifier* rs) { if (m_vec.empty()) throw std::runtime_error("mealy_machines_to_aig(): No strategy given."); @@ -2269,7 +2255,7 @@ namespace spot if (!used_aps.count(ai)) unused_ins.push_back(ai); - return auts_to_aiger(new_vec, mode, unused_ins, unused_outs, rm); + return auts_to_aiger(new_vec, mode, unused_ins, unused_outs, rs); } aig_ptr @@ -2277,7 +2263,7 @@ namespace spot const char* mode, const std::vector& ins, const std::vector>& outs, - const relabeling_map* rm) + const realizability_simplifier* rs) { // todo extend to TGBA and possibly others const unsigned ns = strat_vec.size(); @@ -2311,7 +2297,7 @@ namespace spot "success identifier."); } } - return mealy_machines_to_aig(m_machines, mode, ins, outs_used, rm); + return mealy_machines_to_aig(m_machines, mode, ins, outs_used, rs); } std::ostream & diff --git a/spot/twaalgos/aiger.hh b/spot/twaalgos/aiger.hh index 9f55f3f00..4737a80be 100644 --- a/spot/twaalgos/aiger.hh +++ b/spot/twaalgos/aiger.hh @@ -25,7 +25,7 @@ #include #include #include -#include +#include #include #include @@ -447,7 +447,7 @@ namespace spot /// synthesis-output is ignored and all properties in \a ins and \a /// outs are guaranteed to appear in the aiger circuit. /// - /// If \a rm is given and is not empty, it can be used to specify how + /// If \a rs is given and is not empty, it can be used to specify how /// unused output should be encoded by mapping them to some constant. ///@{ SPOT_API aig_ptr @@ -456,7 +456,7 @@ namespace spot mealy_machine_to_aig(const twa_graph_ptr& m, const char *mode, const std::vector& ins, const std::vector& outs, - const relabeling_map* rm = nullptr); + const realizability_simplifier* rs = nullptr); SPOT_API aig_ptr mealy_machine_to_aig(const mealy_like& m, const char* mode); @@ -464,7 +464,7 @@ namespace spot mealy_machine_to_aig(mealy_like& m, const char *mode, const std::vector& ins, const std::vector& outs, - const relabeling_map* rm = nullptr); + const realizability_simplifier* rs = nullptr); ///@} /// \ingroup synthesis @@ -481,7 +481,7 @@ namespace spot /// If \a ins and \a outs are used, all properties they list are /// guaranteed to appear in the aiger circuit. /// - /// If \a rm is given and is not empty, it can be used to specify how + /// If \a rs is given and is not empty, it can be used to specify how /// unused output should be encoded by mapping them to some constant. /// @{ SPOT_API aig_ptr @@ -495,13 +495,13 @@ namespace spot const char* mode, const std::vector& ins, const std::vector>& outs, - const relabeling_map* rm = nullptr); + const realizability_simplifier* rs = nullptr); SPOT_API aig_ptr mealy_machines_to_aig(const std::vector& m_vec, const char* mode, const std::vector& ins, const std::vector>& outs, - const relabeling_map* rm = nullptr); + const realizability_simplifier* rs = nullptr); /// @} /// \ingroup twa_io