diff --git a/spot/misc/satsolver.cc b/spot/misc/satsolver.cc index d0af1a7e5..f94cfe5c4 100644 --- a/spot/misc/satsolver.cc +++ b/spot/misc/satsolver.cc @@ -26,14 +26,15 @@ #include #include #include +#include #include namespace spot { - satsolver::solution + std::vector satsolver_get_solution(const char* filename) { - satsolver::solution sol; + std::vector sol; std::istream* in; if (filename[0] == '-' && filename[1] == 0) in = &std::cin; @@ -54,7 +55,7 @@ namespace spot while (*in >> i) { if (i == 0) - goto done; + goto stop; sol.emplace_back(i); } if (!in->eof()) @@ -63,7 +64,7 @@ namespace spot // fail bit so that will loop over. in->clear(); } - done: + stop: if (in != &std::cin) delete in; return sol; @@ -116,13 +117,13 @@ namespace spot *cnf_stream_ << '\n'; nclauses_ += 1; if (nclauses_ < 0) - throw std::runtime_error("too many SAT clauses (more than INT_MAX)"); + throw std::runtime_error(": too many SAT clauses (more than INT_MAX)."); } void satsolver::adjust_nvars(int nvars) { if (nvars < 0) - throw std::runtime_error("variable number must be at least 0"); + throw std::runtime_error(": total number of lits. must be at least 0."); if (psat_) { @@ -133,7 +134,7 @@ namespace spot if (nvars < nvars_) { throw std::runtime_error( - "wrong number of variables, a bigger one was already added"); + ": wrong number of variables, a bigger one was already added."); } nvars_ = nvars; } @@ -196,19 +197,62 @@ namespace spot } satsolver::solution - satsolver::picosat_get_solution(int res) + spot::satsolver::satsolver_get_sol(const char* filename) + { + satsolver::solution sol; + bool empty = true; + std::istream* in; + in = new std::ifstream(filename); + int c; + while ((c = in->get()) != EOF) + { + // If a line does not start with 'v ', ignore it. + if (c != 'v' || in->get() != ' ') + { + in->ignore(std::numeric_limits::max(), '\n'); + continue; + } + // Otherwise, read integers one by one. + int i; + while (*in >> i) + { + if (i == 0) + goto done; + + if (i > 0 && empty) + { + empty = false; + sol = satsolver::solution(get_nb_vars(), false); + } + + if (i > 0 && !empty) + sol[i - 1] = true; + } + if (!in->eof()) + // If we haven't reached end-of-file, then we just attempted + // to extract something that wasn't an integer. Clear the + // fail bit so that will loop over. + in->clear(); + } + done: + delete in; + if (empty) + { + sol.clear(); + assert(sol.empty()); + } + return sol; + } + + satsolver::solution + satsolver::picosat_get_sol(int res) { satsolver::solution sol; if (res == PICOSAT_SATISFIABLE) { int nvars = get_nb_vars(); for (int lit = 1; lit <= nvars; ++lit) - { - if (picosat_deref(psat_, lit) > 0) - sol.push_back(lit); - else - sol.push_back(-lit); - } + sol.push_back(picosat_deref(psat_, lit) > 0); } return sol; } @@ -221,7 +265,7 @@ namespace spot { p.first = 0; // A subprocess was not executed so nothing failed. int res = picosat_sat(psat_, -1); // -1: no limit (number of decisions). - p.second = picosat_get_solution(res); + p.second = picosat_get_sol(res); } else { @@ -230,11 +274,11 @@ namespace spot *cnf_stream_ << "p cnf " << get_nb_vars() << ' ' << get_nb_clauses(); cnf_stream_->seekp(0, std::ios_base::end); if (!*cnf_stream_) - throw std::runtime_error("Failed to update cnf header"); + throw std::runtime_error(": failed to update cnf header."); temporary_file* output = create_tmpfile("sat-", ".out"); p.first = cmd_.run(cnf_tmp_, output); - p.second = satsolver_get_solution(output->name()); + p.second = satsolver_get_sol(output->name()); delete output; } return p; @@ -248,10 +292,10 @@ namespace spot prime(satsolver); if (!has('I')) - throw std::runtime_error("SPOT_SATSOLVER should contain %I to " + throw std::runtime_error(": SPOT_SATSOLVER should contain %I to " "indicate how to use the input filename."); if (!has('O')) - throw std::runtime_error("SPOT_SATSOLVER should contain %O to " + throw std::runtime_error(": SPOT_SATSOLVER should contain %O to " "indicate how to use the output filename."); } diff --git a/spot/misc/satsolver.hh b/spot/misc/satsolver.hh index 1d3070811..06eea6bf3 100644 --- a/spot/misc/satsolver.hh +++ b/spot/misc/satsolver.hh @@ -114,7 +114,7 @@ namespace spot template void comment(T first, Args... args); - typedef std::vector solution; + typedef std::vector solution; typedef std::pair solution_pair; /// \brief Return std::vector. @@ -130,7 +130,11 @@ namespace spot /// \brief Extract the solution of Picosat output. /// Must be called only if SPOT_SATSOLVER env variable is not set. satsolver::solution - picosat_get_solution(int res); + picosat_get_sol(int res); + + /// \brief Extract the solution of a SAT solver output. + satsolver::solution + satsolver_get_sol(const char* filename); private: // variables /// \brief A satsolver_command. Check if SPOT_SATSOLVER is given. @@ -148,9 +152,8 @@ namespace spot }; /// \brief Extract the solution of a SAT solver output. - SPOT_API satsolver::solution + SPOT_API std::vector satsolver_get_solution(const char* filename); - } namespace spot diff --git a/spot/priv/Makefile.am b/spot/priv/Makefile.am index 82ec970cf..768faa339 100644 --- a/spot/priv/Makefile.am +++ b/spot/priv/Makefile.am @@ -27,6 +27,8 @@ libpriv_la_SOURCES = \ bddalloc.hh \ freelist.cc \ freelist.hh \ + satcommon.hh\ + satcommon.cc\ trim.cc \ trim.hh \ weight.cc \ diff --git a/spot/priv/satcommon.cc b/spot/priv/satcommon.cc new file mode 100644 index 000000000..17f6f76b9 --- /dev/null +++ b/spot/priv/satcommon.cc @@ -0,0 +1,188 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + + +#include +#include +#include +#include +#include +#include +#include + + +#if DEBUG_CMN +#define print_debug std::cerr +#else +#define print_debug while (0) std::cout +#endif + +namespace spot +{ + void + vars_helper::init(unsigned size_src, unsigned size_cond, unsigned size_dst, + unsigned size_nacc, unsigned size_path, bool state_based, bool dtbasat) + { + print_debug << "init(" << size_src << ',' << size_cond << ',' << size_dst + << ',' << size_nacc << ',' << size_path << ',' << state_based << ")\n"; + + size_src_ = size_src; + size_cond_ = size_cond; + size_dst_ = size_dst; + size_nacc_ = size_nacc; + size_path_ = size_path; + state_based_ = state_based; + dtbasat_ = dtbasat; + + sn_mult_ = size_src * size_nacc; + cd_mult_ = size_cond * size_dst; + dn_mult_ = size_dst * size_nacc; + sd_mult_ = size_src * size_dst; + dr_mult_ = size_dst * 2; + sdr_mult_ = sd_mult_ * 2; + cdn_mult_ = size_cond * size_dst * size_nacc; + scd_mult_ = size_src * size_cond * size_dst; + psd_mult_ = size_path * size_src * size_dst; + scdn_mult_ = scd_mult_ * size_nacc; + scdnp_mult_ = scdn_mult_ * size_path; + + assert(scdnp_mult_ != 0); + } + + void + vars_helper::declare_all_vars(int& min_t) + { + min_t_ = min_t; + min_ta_ = min_t_ + scd_mult_; + if (!state_based_) + min_p_ = min_ta_ + scdn_mult_; + else + min_p_ = min_ta_ + sn_mult_; + + if (!dtbasat_) + max_p_ = min_p_ + psd_mult_ - 1; + else + max_p_ = min_p_ + psd_mult_ * 2 - 1; + + print_debug << "declare_all_trans(" << min_t << ") --> min_t_<" + << min_t_ << ">, min_ta_<" << min_ta_ << ">, min_p<" + << min_p_ << ">, max_p<" << max_p_ << ">\n"; + + // Update satdict.nvars. + // max_p_ - 1 was added after noticing that in some cases in dtbasat, the + // last variable is not used and some sat solver can complain about the + // wong number of variable in cnf mode. No worries, if it turns out to be + // used somewhere, it will be taken into account. + min_t = dtbasat_ ? max_p_ - 1 : max_p_; + assert(min_t != min_t_); + } + + std::string + vars_helper::format_t(bdd_dict_ptr& debug_dict, unsigned src, bdd& cond, + unsigned dst) + { + std::ostringstream buffer; + buffer << '<' << src << ',' << bdd_format_formula(debug_dict, cond) + << ',' << dst << '>'; + return buffer.str(); + } + + std::string + vars_helper::format_ta(bdd_dict_ptr& debug_dict, + const acc_cond* debug_cand_acc, unsigned src, bdd& cond, unsigned dst, + const acc_cond::mark_t& acc) + { + std::ostringstream buffer; + buffer << '<' << src << ',' << bdd_format_formula(debug_dict, cond) + << ',' << debug_cand_acc->format(acc) << ',' << dst << '>'; + return buffer.str(); + } + + std::string + vars_helper::format_p(const acc_cond* debug_cand_acc, + const acc_cond* debug_ref_acc, unsigned src_cand, unsigned src_ref, + unsigned dst_cand, unsigned dst_ref, acc_cond::mark_t acc_cand, + acc_cond::mark_t acc_ref) + { + std::ostringstream buffer; + buffer << '<' << src_cand << ',' << src_ref << ',' << dst_cand << ',' + << dst_ref << ", " << debug_cand_acc->format(acc_cand) << ", " + << debug_ref_acc->format(acc_ref) << '>'; + return buffer.str(); + } + + std::string + vars_helper::format_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand, + unsigned dst_ref) + { + std::ostringstream buffer; + buffer << '<' << src_cand << ',' << src_ref; + if (src_cand == dst_cand && src_ref == dst_ref) + buffer << '>'; + else + buffer << ',' << dst_cand << ',' << dst_ref << '>'; + return buffer.str(); + } + + void + print_log(timer_map& t, int target_state_number, + twa_graph_ptr& res, satsolver& solver) + { + // Always copy the environment variable into a static string, + // so that we (1) look it up once, but (2) won't crash if the + // environment is changed. + static std::string log = []() + { + auto s = getenv("SPOT_SATLOG"); + return s ? s : ""; + }(); + if (!log.empty()) + { + std::fstream out(log, + std::ios_base::app | std::ios_base::out); + out.exceptions(std::ifstream::failbit | std::ifstream::badbit); + const timer& te = t.timer("encode"); + const timer& ts = t.timer("solve"); + out << target_state_number << ','; + if (res) + { + twa_sub_statistics st = sub_stats_reachable(res); + out << st.states << ',' << st.edges << ',' << st.transitions; + } + else + { + out << ",,"; + } + std::pair s = solver.stats(); // sat_stats + out << ',' + << s.first << ',' << s.second << ',' + << te.utime() + te.cutime() << ',' + << te.stime() + te.cstime() << ',' + << ts.utime() + ts.cutime() << ',' + << ts.stime() + ts.cstime() << ",\""; + if (res) + { + std::ostringstream f; + print_hoa(f, res, "l"); + escape_rfc4180(out, f.str()); + } + out << "\"\n"; + } + } +} diff --git a/spot/priv/satcommon.hh b/spot/priv/satcommon.hh new file mode 100644 index 000000000..f327c8a51 --- /dev/null +++ b/spot/priv/satcommon.hh @@ -0,0 +1,238 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et +// Développement de l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#pragma once + +#include +#include +#include +#include +#include +#include + +#define DEBUG_CMN 0 + +namespace spot +{ + struct src_cond + { + unsigned src; + bdd cond; + + src_cond(unsigned src, bdd cond) + : src(src), cond(cond) + { + } + + bool operator<(const src_cond& other) const + { + if (this->src < other.src) + return true; + if (this->src > other.src) + return false; + return this->cond.id() < other.cond.id(); + } + + bool operator==(const src_cond& other) const + { + return (this->src == other.src + && this->cond.id() == other.cond.id()); + } + }; + + /// \brief Interface with satsolver's litterals. + /// + /// This class was created to fill the need to optimize memory storage in + /// SAT-minimization. + /// + /// All this relies on the fact that almost everything about the automaton + /// candidate is known in advance and most of the time, litteral's numbers + /// are just incremented continually (they are continuous...). + /// + /// This class allows to handle variables by only manipulating indices. + class vars_helper + { +private: + unsigned size_src_; + unsigned size_cond_; + unsigned size_dst_; + unsigned size_nacc_; + unsigned size_path_; + bool state_based_; + bool dtbasat_; + int min_t_; + int min_ta_; + int min_p_; + int max_p_; + + // Vars that will be precalculated. + unsigned sn_mult_ = 0; // src * nacc + unsigned cd_mult_ = 0; // cond * dst + unsigned dn_mult_ = 0; // dst * nacc + unsigned sd_mult_ = 0; // src * dst + unsigned dr_mult_ = 0; // dst * 2 --> used only in get_prc(...) + unsigned sdr_mult_ = 0; // src * dst * 2 --> used only in get_prc(...) + unsigned scd_mult_ = 0; // src * cond * dst + unsigned cdn_mult_ = 0; // cond * dst * nacc + unsigned psd_mult_ = 0; // path * src * dst + unsigned scdn_mult_ = 0; // src * cond * dst * nacc + unsigned scdnp_mult_ = 0; // src * cond * dst * nacc * path + +public: + vars_helper() + : size_src_(0), size_cond_(0), size_dst_(0), size_nacc_(0), size_path_(0), + state_based_(false), dtbasat_(false), min_t_(0), min_ta_(0), min_p_(0), + max_p_(0) + { +#if DEBUG_CMN + std::cerr << "vars_helper() constructor called\n"; +#endif + } + + ~vars_helper() + { + } + + /// \brief Save all different sizes and precompute some values. + void + init(unsigned size_src, unsigned size_cond, unsigned size_dst, + unsigned size_nacc, unsigned size_path, bool state_based, + bool dtbasat); + + /// \brief Compute min_t litteral as well as min_ta, min_p and max_p. + /// After this step, all litterals are known. + void + declare_all_vars(int& min_t); + + /// \brief Return the transition's litteral corresponding to parameters. + inline int + get_t(unsigned src, unsigned cond, unsigned dst) const + { +#if DEBUG_CMN + if (src >= size_src_ || cond >= size_cond_ || dst >= size_dst_) + { + std::ostringstream buffer; + buffer << "bad arguments get_t(" << src << ',' << cond << ',' << dst + << ")\n"; + throw std::runtime_error(buffer.str()); + } + std::cerr << "get_t(" << src << ',' << cond << ',' << dst << ") = " + << min_t_ + src * cd_mult_ + cond * size_dst_ + dst << '\n'; +#endif + return min_t_ + src * cd_mult_ + cond * size_dst_ + dst; + } + + /// \brief Return the transition_acc's litteral corresponding to parameters. + /// If (state_based), all outgoing transitions use the same acceptance + /// variable. Therefore, for each combination (src, nacc) there is only one + /// litteral. + /// Note that with Büchi automata, there is only one nacc, thus, only one + /// litteral for each src. + inline int + get_ta(unsigned src, unsigned cond, unsigned dst, unsigned nacc = 0) const + { +#if DEBUG_CMN + if (src >= size_src_ || cond >= size_cond_ || dst >= size_dst_ + || nacc >= size_nacc_) + { + std::stringstream buffer; + buffer << "bad arguments get_ta(" << src << ',' << cond << ',' << dst + << ',' << nacc << ")\n"; + throw std::runtime_error(buffer.str()); + } + int res = state_based_ ? min_ta_ + src * size_nacc_ + nacc + : min_ta_ + src * cdn_mult_ + cond * dn_mult_ + (dst * size_nacc_) + + nacc; + std::cerr << "get_ta(" << src << ',' << cond << ',' << dst << ") = " + << res << '\n'; +#endif + return state_based_ ? min_ta_ + src * size_nacc_ + nacc + : min_ta_ + src * cdn_mult_ + cond * dn_mult_ + dst * size_nacc_ + nacc; + } + + /// \brief Return the path's litteral corresponding to parameters. + inline int + get_p(unsigned path, unsigned src, unsigned dst) const + { +#if DEBUG_CMN + if (src >= size_src_ || path >= size_path_ || dst >= size_dst_) + { + std::stringstream buffer; + buffer << "bad arguments get_p(" << path << ',' << src << ',' << dst + << ")\n"; + throw std::runtime_error(buffer.str()); + } + std::cerr << "get_p(" << path << ',' << src << ',' << dst << ") = " + << min_p_ + path * sd_mult_ + src * size_dst_ + dst << '\n'; +#endif + assert(!dtbasat_); + return min_p_ + path * sd_mult_ + src * size_dst_ + dst; + } + + /// \brief Return the path's litteral corresponding to parameters. + /// Argument ref serves to say whether it is a candidate or a reference + /// litteral. false -> ref | true -> cand + inline int + get_prc(unsigned path, unsigned src, unsigned dst, bool cand) const + { +#if DEBUG_CMN + if (src >= size_src_ || path >= size_path_ || dst >= size_dst_) + { + std::stringstream buffer; + buffer << "bad arguments get_prc(" << path << ',' << src << ',' << dst + << ',' << cand << ")\n"; + throw std::runtime_error(buffer.str()); + } + std::cerr << "get_prc(" << path << ',' << src << ',' << dst << ',' + << cand << ") = " << min_p_ + path * sdr_mult_ + src * dr_mult_ + + dst * 2 + cand << '\n'; +#endif + assert(dtbasat_); + return min_p_ + path * sdr_mult_ + src * dr_mult_ + dst * 2 + cand; + } + + /// \brief Use this function to get a string representation of a transition. + std::string + format_t(bdd_dict_ptr& debug_dict, unsigned src, bdd& cond, + unsigned dst); + + /// \brief Use this function to get a string representation of a transition + /// acc. + std::string + format_ta(bdd_dict_ptr& debug_dict, const acc_cond* debug_cand_acc, + unsigned src, bdd& cond, unsigned dst, const acc_cond::mark_t& acc); + + /// \brief Use this function to get a string representation of a path var. + std::string + format_p(const acc_cond* debug_cand_acc, const acc_cond* debug_ref_acc, + unsigned src_cand, unsigned src_ref, unsigned dst_cand, + unsigned dst_ref, acc_cond::mark_t acc_cand, acc_cond::mark_t acc_ref); + + /// \brief Use this function to get a string representation of a path var. + std::string + format_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand, + unsigned dst_ref); + }; + + /// \brief Good old function that prints log is SPOT_SATLOG. It has been + /// moved from spot/twaalgos/dt*asat.cc files. + void + print_log(timer_map& t, int target_state_number, twa_graph_ptr& res, + satsolver& solver); +} diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index a1e1a890f..1852cdc81 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -17,19 +17,16 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include #include #include -#include -#include #include -#include -#include -#include -#include +#include #include #include -#include +#include +#include +#include +#include // If you set the SPOT_TMPKEEP environment variable the temporary // file used to communicate with the sat solver will be left in @@ -41,6 +38,7 @@ // of all positive variables in the result and their meaning. #define DEBUG 0 + #if DEBUG #define dout out << "c " #define cnf_comment(...) solver.comment(__VA_ARGS__) @@ -57,116 +55,27 @@ namespace spot { static bdd_dict_ptr debug_dict; - struct transition - { - unsigned src; - bdd cond; - unsigned dst; - - transition(unsigned src, bdd cond, unsigned dst) - : src(src), cond(cond), dst(dst) - { - } - - bool operator<(const transition& other) const - { - if (this->src < other.src) - return true; - if (this->src > other.src) - return false; - if (this->dst < other.dst) - return true; - if (this->dst > other.dst) - return false; - return this->cond.id() < other.cond.id(); - } - - bool operator==(const transition& other) const - { - return (this->src == other.src - && this->dst == other.dst - && this->cond.id() == other.cond.id()); - } - }; - - struct src_cond - { - unsigned src; - bdd cond; - - src_cond(unsigned src, bdd cond) - : src(src), cond(cond) - { - } - - bool operator<(const src_cond& other) const - { - if (this->src < other.src) - return true; - if (this->src > other.src) - return false; - return this->cond.id() < other.cond.id(); - } - - bool operator==(const src_cond& other) const - { - return (this->src == other.src - && this->cond.id() == other.cond.id()); - } - }; - - struct state_pair - { - unsigned a; - unsigned b; - - state_pair(unsigned a, unsigned b) - : a(a), b(b) - { - } - - bool operator<(const state_pair& other) const - { - if (this->a < other.a) - return true; - if (this->a > other.a) - return false; - if (this->b < other.b) - return true; - if (this->b > other.b) - return false; - return false; - } - }; - struct path { - int src_cand; int src_ref; - int dst_cand; int dst_ref; - path(int src_cand, int src_ref, - int dst_cand, int dst_ref) - : src_cand(src_cand), src_ref(src_ref), - dst_cand(dst_cand), dst_ref(dst_ref) + path(int src_ref, int dst_ref) + : src_ref(src_ref), dst_ref(dst_ref) + { + } + + path(int src_ref) + : src_ref(src_ref), dst_ref(src_ref) { } bool operator<(const path& other) const { - if (this->src_cand < other.src_cand) - return true; - if (this->src_cand > other.src_cand) - return false; if (this->src_ref < other.src_ref) return true; if (this->src_ref > other.src_ref) return false; - if (this->dst_cand < other.dst_cand) - return true; - if (this->dst_cand > other.dst_cand) - return false; if (this->dst_ref < other.dst_ref) return true; if (this->dst_ref > other.dst_ref) @@ -176,121 +85,211 @@ namespace spot }; - std::ostream& operator<<(std::ostream& os, const state_pair& p) - { - os << '<' << p.a << ',' << p.b << '>'; - return os; - } - - std::ostream& operator<<(std::ostream& os, const transition& t) - { - os << '<' << t.src << ',' - << bdd_format_formula(debug_dict, t.cond) - << ',' << t.dst << '>'; - return os; - } - - std::ostream& operator<<(std::ostream& os, const path& p) - { - os << '<' - << p.src_cand << ',' - << p.src_ref << ',' - << p.dst_cand << ',' - << p.dst_ref << '>'; - return os; - } - struct dict { - typedef std::map trans_map; - trans_map transid; - trans_map transacc; - typedef std::map rev_map; - rev_map revtransid; - rev_map revtransacc; - - std::map prodid; - std::map pathid_ref; - std::map pathid_cand; + std::vector alpha_vect; + std::map path_map; + std::map alpha_map; + vars_helper helper; int nvars = 0; unsigned cand_size; + unsigned ref_size; + + int + transid(unsigned src, unsigned cond, unsigned dst) + { + return helper.get_t(src, cond, dst); + } + + int + transid(unsigned src, bdd& cond, unsigned dst) + { +#if DEBUG + try + { + return helper.get_t(src, alpha_map.at(cond), dst); + } + catch (const std::out_of_range& c) + { + std::cerr << "label of transid " << fmt_t(src, cond, dst) + << " not found.\n"; + throw c; + } +#else + return helper.get_t(src, alpha_map[cond], dst); +#endif + } + + int + transacc(unsigned src, unsigned cond, unsigned dst) + { + return helper.get_ta(src, cond, dst); + } + + int + transacc(unsigned src, bdd& cond, unsigned dst) + { +#if DEBUG + try + { + return helper.get_ta(src, alpha_map.at(cond), dst); + } + catch (const std::out_of_range& c) + { + std::cerr << "label of transacc " << fmt_t(src, cond, dst) + << " not found.\n"; + throw c; + } +#else + return helper.get_ta(src, alpha_map[cond], dst); +#endif + } + + int + pathid_ref(unsigned src_cand, unsigned src_ref, unsigned dst_cand, + unsigned dst_ref) + { +#if DEBUG + try + { + return helper.get_prc( + path_map.at(path(src_ref, dst_ref)), src_cand, dst_cand, false); + } + catch (const std::out_of_range& c) + { + std::cerr << "path(" << src_ref << ',' << dst_ref << ") of pathid_ref" + << ' ' << fmt_p(src_cand, src_ref, dst_cand, dst_ref) + << " not found.\n"; + throw c; + } +#else + return helper.get_prc( + path_map[path(src_ref, dst_ref)], src_cand, dst_cand, false); +#endif + } + +#if DEBUG + int + pathid_ref(unsigned path, unsigned src_cand, unsigned dst_cand) + { + return helper.get_prc(path, src_cand, dst_cand, false); + } + + int + pathid_cand(unsigned path, unsigned src_cand, unsigned dst_cand) + { + return helper.get_prc(path, src_cand, dst_cand, true); + } +#endif + + int + pathid_cand(unsigned src_cand, unsigned src_ref, unsigned dst_cand, + unsigned dst_ref) + { +#if DEBUG + try + { + return helper.get_prc( + path_map.at(path(src_ref, dst_ref)), src_cand, dst_cand, true); + } + catch (const std::out_of_range& c) + { + std::cerr << "path(" << src_ref << ',' << dst_ref + << ") of pathid_cand " + << fmt_p(src_cand, src_ref, dst_cand, dst_ref) << " not found.\n"; + throw c; + } +#else + return helper.get_prc( + path_map[path(src_ref, dst_ref)], src_cand, dst_cand, true); +#endif + } + + std::string + fmt_t(unsigned src, bdd& cond, unsigned dst) + { + return helper.format_t(debug_dict, src, cond, dst); + } + + std::string + fmt_t(unsigned src, unsigned cond, unsigned dst) + { + return helper.format_t(debug_dict, src, alpha_vect[cond], dst); + } + + std::string + fmt_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand, + unsigned dst_ref) + { + return helper.format_p(src_cand, src_ref, dst_cand, dst_ref); + } + }; - unsigned declare_vars(const const_twa_graph_ptr& aut, + void declare_vars(const const_twa_graph_ptr& aut, dict& d, bdd ap, bool state_based, scc_info& sm) { - unsigned ref_size = aut->num_states(); + d.ref_size = aut->num_states(); if (d.cand_size == -1U) - for (unsigned i = 0; i < ref_size; ++i) + for (unsigned i = 0; i < d.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. - for (unsigned i = 0; i < ref_size; ++i) + // In order to optimize memory usage, src_cand & dst_cand have been + // removed from path struct (the reasons are: they were no optimization + // on them and their values are known from the beginning). + // + // However, since some optimizations are based on the following i and k, + // it is necessary to associate to each path constructed, an ID number. + // + // Given this ID, src_cand, dst_cand and a boolean that tells we want + // ref or cand var, the corresponding litteral can be retrieved thanks + // to get_prc(...), a vars_helper's method. + unsigned path_size = 0; + for (unsigned i = 0; i < d.ref_size; ++i) { if (!sm.reachable_state(i)) continue; - unsigned i_scc = sm.scc_of(i); bool is_trivial = sm.is_trivial(i_scc); - for (unsigned j = 0; j < d.cand_size; ++j) + for (unsigned k = 0; k < d.ref_size; ++k) { - d.prodid[state_pair(j, i)] = ++d.nvars; - - // skip trivial SCCs - if (is_trivial) + if (!sm.reachable_state(k)) continue; - - 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; - path p(j, i, l, k); - d.pathid_ref[p] = ++d.nvars; - d.pathid_cand[p] = ++d.nvars; - } - } + if ((sm.scc_of(k) != i_scc || is_trivial) + && !(i == k)) + continue; + d.path_map[path(i, k)] = path_size++; } } - for (unsigned i = 0; i < d.cand_size; ++i) - { - int transacc = -1; - if (state_based) - // All outgoing transitions use the same acceptance variable. - transacc = ++d.nvars; + // Fill dict's bdd vetor (alpha_vect) and save each bdd and it's + // corresponding index in alpha_map. This is necessary beacause some + // loops start from a precise bdd. Therefore, it's useful to know + // it's corresponding index to deal with vars_helper. + bdd all = bddtrue; + for (unsigned j = 0; all != bddfalse; ++j) + { + bdd one = bdd_satoneset(all, ap, bddfalse); + d.alpha_vect.push_back(one); + d.alpha_map[d.alpha_vect[j]] = j; + all -= one; + } - for (unsigned j = 0; j < d.cand_size; ++j) - { - bdd all = bddtrue; - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, ap, bddfalse); - all -= one; + // Initialize vars_helper by giving it all the necessary information. + // 1: nacc_size is 1 (with Büchi) | true: means dtbasat, i-e, not dtwasat. + d.helper.init(d.cand_size, d.alpha_vect.size(), d.cand_size, + 1, path_size, state_based, true); - 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; - d.revtransacc.emplace(ta, t); - } - } - } - - return ref_size; + // Based on all previous informations, helper knows all litterals. + d.helper.declare_all_vars(++d.nvars); } typedef std::pair sat_stats; @@ -300,12 +299,10 @@ namespace spot const const_twa_graph_ptr& ref, dict& d, bool state_based) { - // Compute the AP used in the hard way. - bdd ap = bddtrue; - for (auto& t: ref->edges()) - ap &= bdd_support(t.cond); + // Compute the AP used. + bdd ap = ref->ap_vars(); - // Count the number of atomic propositions + // Count the number of atomic propositions. int nap = 0; { bdd cur = ap; @@ -320,111 +317,96 @@ namespace spot scc_info sm(ref); // Number all the SAT variables we may need. - unsigned ref_size = declare_vars(ref, d, ap, state_based, sm); + declare_vars(ref, d, ap, state_based, sm); - // Tell the satsolver the number of variables + // Store alpha_vect's size once for all. + unsigned alpha_size = d.alpha_vect.size(); + + // Tell the satsolver the number of variables. solver.adjust_nvars(d.nvars); - // empty automaton is impossible + // Empty automaton is impossible. assert(d.cand_size > 0); #if DEBUG debug_dict = ref->get_dict(); - solver.comment("ref_size", ref_size, '\n'); - solver.comment("cand_size", d.cand_size, '\n'); + solver.comment("d.ref_size", d.ref_size, '\n'); + solver.comment("d.cand_size", d.cand_size, '\n'); #endif cnf_comment("symmetry-breaking clauses\n"); unsigned j = 0; - bdd all = bddtrue; - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; - 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]; - cnf_comment("¬", t, '\n'); - solver.add({-ti, 0}); - } - ++j; - } + for (unsigned l = 0; l < alpha_size; ++l, ++j) + for (unsigned i = 0; i < d.cand_size - 1; ++i) + for (unsigned k = i * nap + j + 2; k < d.cand_size; ++k) + { + cnf_comment("¬", d.fmt_t(i, l, k), '\n'); + solver.add({-d.transid(i, l, k), 0}); + } + if (!solver.get_nb_clauses()) cnf_comment("(none)\n"); cnf_comment("(1) the candidate automaton is complete\n"); for (unsigned q1 = 0; q1 < d.cand_size; ++q1) - { - bdd all = bddtrue; - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; - + for (unsigned l = 0; l < alpha_size; ++l) + { #if DEBUG - solver.comment(""); - for (unsigned q2 = 0; q2 < d.cand_size; q2++) - { - transition t(q1, s, q2); - solver.comment_rec(t, "δ"); - if (q2 != d.cand_size) - solver.comment_rec(" ∨ "); - } - solver.comment_rec('\n'); + solver.comment(""); + for (unsigned q2 = 0; q2 < d.cand_size; q2++) + { + solver.comment_rec(d.fmt_t(q1, l, q2), "δ"); + if (q2 != d.cand_size) + solver.comment_rec(" ∨ "); + } + solver.comment_rec('\n'); #endif - - for (unsigned q2 = 0; q2 < d.cand_size; q2++) - { - transition t(q1, s, q2); - int ti = d.transid[t]; - solver.add(ti); - } - solver.add(0); - } - } + for (unsigned q2 = 0; q2 < d.cand_size; q2++) + solver.add(d.transid(q1, l, q2)); + solver.add(0); + } cnf_comment("(2) the initial state is reachable\n"); { unsigned init = ref->get_init_state_number(); - cnf_comment(state_pair(0, init), '\n'); - solver.add({d.prodid[state_pair(0, init)], 0}); + cnf_comment(d.fmt_p(0, init, 0, init), '\n'); + solver.add({d.pathid_ref(0, init, 0, init), 0}); } - for (std::map::const_iterator pit = d.prodid.begin(); - pit != d.prodid.end(); ++pit) + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) { - unsigned q1 = pit->first.a; - unsigned q1p = pit->first.b; + for (unsigned q1p = 0; q1p < d.ref_size; ++q1p) + { + // Added to comply with the variable declaration, i-e to avoid + // using undeclared variables. + if (!sm.reachable_state(q1p)) + continue; - cnf_comment("(3) augmenting paths based on Cand[", q1, "] and Ref[", - q1p, "]\n"); - 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; + cnf_comment("(3) augmenting paths based on Cand[", q1, "] and Ref[", + q1p, "]\n"); + 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; - for (unsigned q2 = 0; q2 < d.cand_size; q2++) - { - transition t(q1, s, q2); - int ti = d.transid[t]; + for (unsigned q2 = 0; q2 < d.cand_size; q2++) + { + int prev = d.pathid_ref(q1, q1p, q1, q1p); + int succ = d.pathid_ref(q2, dp, q2, dp); + if (prev == succ) + continue; - state_pair p2(q2, dp); - int succ = d.prodid[p2]; - - if (pit->second == succ) - continue; - - cnf_comment(pit->first, " ∧ ", t, "δ → ", p2, '\n'); - solver.add({-pit->second, -ti, succ, 0}); - } - } - } + cnf_comment(prev, "∧", d.fmt_t(q1, s, q2), "δ →", + d.fmt_p(q2, dp, q2, dp), '\n'); + solver.add({-prev, -d.transid(q1, s, q2), succ, 0}); + } + } + } + } } const acc_cond& ra = ref->acc(); @@ -432,14 +414,14 @@ 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 (unsigned q1p = 0; q1p < ref_size; ++q1p) + for (unsigned q1p = 0; q1p < d.ref_size; ++q1p) { if (!sm.reachable_state(q1p)) continue; unsigned q1p_scc = sm.scc_of(q1p); if (sm.is_trivial(q1p_scc)) continue; - for (unsigned q2p = 0; q2p < ref_size; ++q2p) + for (unsigned q2p = 0; q2p < d.ref_size; ++q2p) { if (!sm.reachable_state(q2p)) continue; @@ -450,17 +432,11 @@ namespace spot for (unsigned q1 = 0; q1 < d.cand_size; ++q1) for (unsigned q2 = 0; q2 < d.cand_size; ++q2) { - path p1(q1, q1p, q2, q2p); - + std::string f_p = d.fmt_p(q1, q1p, q2, q2p); cnf_comment("(4&5) matching paths from reference based on", - p1, '\n'); - - int pid1; - if (q1 == q2 && q1p == q2p) - pid1 = d.prodid[state_pair(q1, q1p)]; - else - pid1 = d.pathid_ref[p1]; + f_p, '\n'); + int pid1 = d.pathid_ref(q1, q1p, q2, q2p); for (auto& tr: ref->out(q2p)) { unsigned dp = tr.dst; @@ -479,23 +455,20 @@ namespace spot { bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; - - transition t(q2, s, q1); - int ti = d.transid[t]; - int ta = d.transacc[t]; - - cnf_comment(p1, "R ∧", t, "δ → ¬", t, +#if DEBUG + std::string f_t = d.fmt_t(q2, s, q1); + cnf_comment(f_p, "R ∧", f_t, "δ → ¬", f_t, "F\n"); - solver.add({-pid1, -ti, -ta, 0}); +#endif + solver.add({-pid1, + -d.transid(q2, s, q1), + -d.transacc(q2, s, q1), + 0}); } - - } else // (5) not looping { - path p2 = path(q1, q1p, q3, dp); - int pid2 = d.pathid_ref[p2]; - + int pid2 = d.pathid_ref(q1, q1p, q3, dp); if (pid1 == pid2) continue; @@ -505,11 +478,13 @@ namespace spot bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; - transition t(q2, s, q3); - int ti = d.transid[t]; - - cnf_comment(p1, "R ∧", t, "δ →", p2, "R\n"); - solver.add({-pid1, -ti, pid2, 0}); + cnf_comment(f_p, "R ∧", d.fmt_t(q2, s, q3), + "δ →", d.fmt_p(q1, q1p, q3, dp), + "R\n"); + solver.add({-pid1, + -d.transid(q2, s, q3), + pid2, + 0}); } } } @@ -520,14 +495,14 @@ 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 (unsigned q1p = 0; q1p < ref_size; ++q1p) + for (unsigned q1p = 0; q1p < d.ref_size; ++q1p) { if (!sm.reachable_state(q1p)) continue; unsigned q1p_scc = sm.scc_of(q1p); if (sm.is_trivial(q1p_scc)) continue; - for (unsigned q2p = 0; q2p < ref_size; ++q2p) + for (unsigned q2p = 0; q2p < d.ref_size; ++q2p) { if (!sm.reachable_state(q2p)) continue; @@ -538,15 +513,15 @@ namespace spot for (unsigned q1 = 0; q1 < d.cand_size; ++q1) for (unsigned q2 = 0; q2 < d.cand_size; ++q2) { - path p1(q1, q1p, q2, q2p); + std::string f_p = d.fmt_p(q1, q1p, q2, q2p); cnf_comment("(6&7) matching paths from candidate based on", - p1, '\n'); + f_p, '\n'); int pid1; if (q1 == q2 && q1p == q2p) - pid1 = d.prodid[state_pair(q1, q1p)]; + pid1 = d.pathid_ref(q1, q1p, q2, q2p); else - pid1 = d.pathid_cand[p1]; + pid1 = d.pathid_cand(q1, q1p, q2, q2p); for (auto& tr: ref->out(q2p)) { @@ -567,20 +542,20 @@ namespace spot { bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; - - transition t(q2, s, q1); - int ti = d.transid[t]; - int ta = d.transacc[t]; - - cnf_comment(p1, "C ∧", t, "δ →", t, "F\n"); - solver.add({-pid1, -ti, ta, 0}); +#if DEBUG + std::string f_t = d.fmt_t(q2, s, q1); + cnf_comment(f_p, "C ∧", f_t, "δ →", f_t, + "F\n"); +#endif + solver.add({-pid1, + -d.transid(q2, s, q1), + d.transacc(q2, s, q1), + 0}); } } else // (7) no loop { - path p2 = path(q1, q1p, q3, dp); - int pid2 = d.pathid_cand[p2]; - + int pid2 = d.pathid_cand(q1, q1p, q3, dp); if (pid1 == pid2) continue; @@ -589,14 +564,17 @@ namespace spot { bdd s = bdd_satoneset(all, ap, bddfalse); all -= s; - - transition t(q2, s, q3); - int ti = d.transid[t]; - int ta = d.transacc[t]; - - cnf_comment(p1, "C ∧", t, "δ ∧ ¬", t, - "F →", p2, "C\n"); - solver.add({-pid1, -ti, ta, pid2, 0}); +#if DEBUG + std::string f_t = d.fmt_t(q2, s, q3); + cnf_comment(f_p, "C ∧", f_t, "δ ∧ ¬", f_t, + "F →", d.fmt_p(q1, q1p, q3, dp), + "C\n"); +#endif + solver.add({-pid1, + -d.transid(q2, s, q3), + d.transacc(q2, s, q3), + pid2, + 0}); } } } @@ -611,107 +589,120 @@ namespace spot sat_build(const satsolver::solution& solution, dict& satdict, const_twa_graph_ptr aut, bool state_based) { + trace << "sat_build(...)\n"; + auto autdict = aut->get_dict(); auto a = make_twa_graph(autdict); a->copy_ap_of(aut); - acc_cond::mark_t acc = a->set_buchi(); + a->set_buchi(); if (state_based) a->prop_state_acc(true); a->prop_deterministic(true); a->new_states(satdict.cand_size); - unsigned last_aut_trans = -1U; - const transition* last_sat_trans = nullptr; - #if DEBUG std::fstream out("dtba-sat.dbg", std::ios_base::trunc | std::ios_base::out); out.exceptions(std::ifstream::failbit | std::ifstream::badbit); - std::set positive; #endif - - dout << "--- transition variables ---\n"; std::set acc_states; std::set seen_trans; - for (int v: solution) - { - if (v < 0) // FIXME: maybe we can have (v < NNN)? - continue; -#if DEBUG - positive.insert(v); -#endif - - dict::rev_map::const_iterator t = satdict.revtransid.find(v); - - if (t != satdict.revtransid.end()) + unsigned alpha_size = satdict.alpha_vect.size(); + unsigned cand_size = satdict.cand_size; + for (unsigned i = 0; i < cand_size; ++i) + for (unsigned j = 0; j < alpha_size; ++j) + for (unsigned k = 0; k < cand_size; ++k) + { + if (solution[satdict.transid(i, j, k) - 1]) { // Ignore unuseful transitions because of reduced cand_size. - if (t->second.src >= satdict.cand_size) + if (i >= cand_size) continue; // Skip (s,l,d2) if we have already seen some (s,l,d1). - if (seen_trans.insert(src_cond(t->second.src, - t->second.cond)).second) - { - // Mark the transition as accepting if the source is. - bool accept = state_based - && acc_states.find(t->second.src) != acc_states.end(); + if (seen_trans.insert(src_cond(i, satdict.alpha_vect[j])).second) + { + bool accept = false; + if (state_based) + accept = acc_states.find(i) != acc_states.end(); + if (!accept) + accept = solution[satdict.transacc(i, j, k) - 1]; - last_aut_trans = - a->new_acc_edge(t->second.src, t->second.dst, - t->second.cond, accept); - last_sat_trans = &t->second; + a->new_acc_edge(i, k, satdict.alpha_vect[j], accept); - dout << v << '\t' << t->second << "δ\n"; - } + if (state_based && accept) + acc_states.insert(i); + } } - else - { - t = satdict.revtransacc.find(v); - if (t != satdict.revtransacc.end()) - { - dout << v << '\t' << t->second << "F\n"; - if (last_sat_trans && t->second == *last_sat_trans) - { - assert(!state_based); - // This assumes that the SAT solvers output - // variables in increasing order. - a->edge_data(last_aut_trans).acc = acc; - } - else if (state_based) - { - // Accepting translations actually correspond to - // states and are announced before listing - // outgoing transitions. Again, this assumes - // that the SAT solvers output variables in - // increasing order. - acc_states.insert(t->second.src); - } - } - } - } + } #if DEBUG - dout << "--- state_pair variables ---\n"; - for (auto pit: satdict.prodid) - if (positive.find(pit.second) != positive.end()) - dout << pit.second << '\t' << pit.first << "C\n"; - else - dout << -pit.second << "\t¬" << pit.first << "C\n"; + dout << "--- transition variables ---\n"; + for (unsigned i = 0; i < cand_size; ++i) + for (unsigned j = 0; j < alpha_size; ++j) + for (unsigned k = 0; k < cand_size; ++k) + { + int var = satdict.transid(i, j, k); + std::string f_t = satdict.fmt_t(i, j, k); + if (solution[var - 1]) + dout << ' ' << var << "\t " << f_t << '\n'; + else + dout << -var << "\t¬" << f_t << '\n'; + } + dout << "--- transition_acc variables ---\n"; + if (state_based) + { + dout << "In state_based mode with Büchi automaton, there is only 1 " + "litteral for each src, regardless of dst or cond!\n"; + for (unsigned i = 0; i < cand_size; ++i) + { + int var = satdict.transacc(i, 0, 0); + std::string f_t = satdict.fmt_t(i, 0, 0); + if (solution[var - 1]) + dout << ' ' << var << "\t " << f_t << '\n'; + else + dout << -var << "\t¬" << f_t << '\n'; + } + } + else + for (unsigned i = 0; i < cand_size; ++i) + for (unsigned j = 0; j < alpha_size; ++j) + for (unsigned k = 0; k < cand_size; ++k) + { + int var = satdict.transacc(i, j, k); + std::string f_t = satdict.fmt_t(i, j, k); + if (solution[var - 1]) + dout << ' ' << var << "\t " << f_t << '\n'; + else + dout << -var << "\t¬" << f_t << '\n'; + } + dout << "--- ref pathid variables ---\n"; + std::map cand_vars; + for (auto it = satdict.path_map.begin(); it != satdict.path_map.end(); + ++it) + for (unsigned k = 0; k < cand_size; ++k) + for (unsigned l = 0; l < cand_size; ++l) + { + // false:reference | true:cand + int cand_v = satdict.pathid_cand(it->second, k, l); + int ref_v = satdict.pathid_ref(it->second, k, l); + std::string f_p = satdict.fmt_p(k, it->first.src_ref, l, + it->first.dst_ref); - dout << "--- pathid_cand variables ---\n"; - for (auto pit: satdict.pathid_cand) - if (positive.find(pit.second) != positive.end()) - dout << pit.second << '\t' << pit.first << "C\n"; + cand_vars[cand_v] = f_p; + if (solution[ref_v - 1]) + dout << ' ' << ref_v << "\t " << f_p << '\n'; + else + dout << -ref_v << "\t¬" << f_p << '\n'; + } + dout << "--- cand pathid variables ---\n"; + for (auto it = cand_vars.begin(); it != cand_vars.end(); ++it) + { + if (solution[it->first - 1]) + dout << ' ' << it->first << "\t " << it->second << '\n'; else - dout << -pit.second << "\t¬" << pit.first << "C\n"; - - dout << "--- pathid_ref variables ---\n"; - for (auto pit: satdict.pathid_ref) - if (positive.find(pit.second) != positive.end()) - dout << pit.second << '\t' << pit.first << "R\n"; - else - dout << -pit.second << "\t¬" << pit.first << "C\n"; + dout << -it->first << "\t¬" << it->second << '\n'; + } #endif a->merge_edges(); return a; @@ -737,7 +728,7 @@ namespace spot timer_map t; t.start("encode"); - sat_stats s = dtba_to_sat(solver, a, d, state_based); + dtba_to_sat(solver, a, d, state_based); t.stop("encode"); t.start("solve"); solution = solver.get_solution(); @@ -747,41 +738,8 @@ namespace spot if (!solution.second.empty()) res = sat_build(solution.second, d, a, state_based); - // Always copy the environment variable into a static string, - // so that we (1) look it up once, but (2) won't crash if the - // environment is changed. - static std::string log = []() - { - auto s = getenv("SPOT_SATLOG"); - return s ? s : ""; - }(); - if (!log.empty()) - { - std::fstream out(log, - std::ios_base::app | std::ios_base::out); - out.exceptions(std::ifstream::failbit | std::ifstream::badbit); - const timer& te = t.timer("encode"); - const timer& ts = t.timer("solve"); - out << target_state_number << ','; - if (res) - { - twa_sub_statistics st = sub_stats_reachable(res); - out << st.states << ',' << st.edges << ',' << st.transitions; - } - else - { - out << ",,"; - } - out << ',' - << s.first << ',' << s.second << ',' - << te.utime() + te.cutime() << ',' - << te.stime() + te.cstime() << ',' - << ts.utime() + ts.cutime() << ',' - << ts.stime() + ts.cstime() << '\n'; - } - static bool show = getenv("SPOT_SATSHOW"); - if (show && res) - print_dot(std::cout, res); + // Print log if env var SPOT_SATLOG is set. + print_log(t, target_state_number, res, solver); trace << "dtba_sat_synthetize(...) = " << res << '\n'; return res; diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index 90f6b3758..9421806f6 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -17,27 +17,24 @@ // You should have received a copy of the GNU General Public License // along with this program. If not, see . -#include #include #include -#include -#include #include -#include -#include -#include -#include -#include +#include +#include #include #include -#include -#include -#include +#include +#include #include -#include -#include -#include +#include +#include +#include #include +#include +#include +#include +#include // If you set the SPOT_TMPKEEP environment variable the temporary // file used to communicate with the sat solver will be left in @@ -49,6 +46,7 @@ // of all positive variables in the result and their meaning. #define DEBUG 0 + #if DEBUG #define dout out << "c " #define cnf_comment(...) solver.comment(__VA_ARGS__) @@ -67,141 +65,32 @@ namespace spot static const acc_cond* debug_ref_acc = nullptr; static const acc_cond* debug_cand_acc = nullptr; - struct transition - { - unsigned src; - bdd cond; - unsigned dst; - - transition(int src, bdd cond, int dst) - : src(src), cond(cond), dst(dst) - { - } - - bool operator<(const transition& other) const - { - if (this->src < other.src) - return true; - if (this->src > other.src) - return false; - if (this->dst < other.dst) - return true; - if (this->dst > other.dst) - return false; - return this->cond.id() < other.cond.id(); - } - - bool operator==(const transition& other) const - { - return (this->src == other.src - && this->dst == other.dst - && this->cond.id() == other.cond.id()); - } - }; - - struct src_cond - { - unsigned src; - bdd cond; - - src_cond(int src, bdd cond) - : src(src), cond(cond) - { - } - - bool operator<(const src_cond& other) const - { - if (this->src < other.src) - return true; - if (this->src > other.src) - return false; - return this->cond.id() < other.cond.id(); - } - - bool operator==(const src_cond& other) const - { - return (this->src == other.src - && this->cond.id() == other.cond.id()); - } - }; - - struct transition_acc - { - unsigned src; - bdd cond; - acc_cond::mark_t acc; - unsigned dst; - - transition_acc(int src, bdd cond, acc_cond::mark_t acc, int dst) - : src(src), cond(cond), acc(acc), dst(dst) - { - } - - bool operator<(const transition_acc& other) const - { - if (this->src < other.src) - return true; - if (this->src > other.src) - return false; - if (this->dst < other.dst) - return true; - if (this->dst > other.dst) - return false; - if (this->cond.id() < other.cond.id()) - return true; - if (this->cond.id() > other.cond.id()) - return false; - return this->acc < other.acc; - } - - bool operator==(const transition_acc& other) const - { - return (this->src == other.src - && this->dst == other.dst - && this->cond.id() == other.cond.id() - && this->acc == other.acc); - } - }; - struct path { - unsigned src_cand; unsigned src_ref; - unsigned dst_cand; unsigned dst_ref; acc_cond::mark_t acc_cand; acc_cond::mark_t acc_ref; - path(unsigned src_cand, unsigned src_ref) - : src_cand(src_cand), src_ref(src_ref), - dst_cand(src_cand), dst_ref(src_ref), + path(unsigned src_ref) + : src_ref(src_ref), dst_ref(src_ref), acc_cand(0U), acc_ref(0U) { } - path(unsigned src_cand, unsigned src_ref, - unsigned dst_cand, unsigned dst_ref, + path(unsigned src_ref, unsigned dst_ref, acc_cond::mark_t acc_cand, acc_cond::mark_t acc_ref) - : src_cand(src_cand), src_ref(src_ref), - dst_cand(dst_cand), dst_ref(dst_ref), + : src_ref(src_ref), dst_ref(dst_ref), acc_cand(acc_cand), acc_ref(acc_ref) { } bool operator<(const path& other) const { - if (this->src_cand < other.src_cand) - return true; - if (this->src_cand > other.src_cand) - return false; if (this->src_ref < other.src_ref) return true; if (this->src_ref > other.src_ref) return false; - if (this->dst_cand < other.dst_cand) - return true; - if (this->dst_cand > other.dst_cand) - return false; if (this->dst_ref < other.dst_ref) return true; if (this->dst_ref > other.dst_ref) @@ -214,42 +103,11 @@ namespace spot return true; if (this->acc_cand > other.acc_cand) return false; - return false; } }; - std::ostream& operator<<(std::ostream& os, const transition& t) - { - os << '<' << t.src << ',' - << bdd_format_formula(debug_dict, t.cond) - << ',' << t.dst << '>'; - return os; - } - - - std::ostream& operator<<(std::ostream& os, const transition_acc& t) - { - os << '<' << t.src << ',' - << bdd_format_formula(debug_dict, t.cond) << ',' - << debug_cand_acc->format(t.acc) - << ',' << t.dst << '>'; - return os; - } - - std::ostream& operator<<(std::ostream& os, const path& p) - { - os << '<' - << p.src_cand << ',' - << p.src_ref << ',' - << p.dst_cand << ',' - << p.dst_ref << ", " - << debug_cand_acc->format(p.acc_cand) << ", " - << debug_ref_acc->format(p.acc_ref) << '>'; - return os; - } - // If the DNF is // Fin(1)&Fin(2)&Inf(3) | Fin(0)&Inf(3) | Fin(4)&Inf(5)&Inf(6) // this returns the following map: @@ -349,18 +207,15 @@ namespace spot } const_twa_ptr aut; - typedef std::map trans_map; - typedef std::map trans_acc_map; - trans_map transid; - trans_acc_map transaccid; - typedef std::map rev_map; - typedef std::map rev_acc_map; - rev_map revtransid; - rev_acc_map revtransaccid; - std::map pathid; + vars_helper helper; + std::vector alpha_vect; + std::map path_map; + std::map alpha_map; + int nvars = 0; - unsigned cand_size; + unsigned int ref_size; + unsigned int cand_size; unsigned int cand_nacc; acc_cond::acc_code cand_acc; @@ -382,6 +237,126 @@ namespace spot aut->get_dict()->unregister_all_my_variables(this); } + int + transid(unsigned src, unsigned cond, unsigned dst) + { + return helper.get_t(src, cond, dst); + } + + int + transid(unsigned src, bdd& cond, unsigned dst) + { +#if DEBUG + try + { + return helper.get_t(src, alpha_map.at(cond), dst); + } + catch (const std::out_of_range& c) + { + std::cerr << "label of transid " << fmt_t(src, cond, dst) + << " not found.\n"; + throw c; + } +#else + return helper.get_t(src, alpha_map[cond], dst); +#endif + } + + int + transacc(unsigned src, unsigned cond, unsigned dst, unsigned nacc) + { + return helper.get_ta(src, cond, dst, nacc); + } + + int + transacc(unsigned src, bdd& cond, unsigned dst, unsigned nacc) + { +#if DEBUG + try + { + return helper.get_ta(src, alpha_map.at(cond), dst, nacc); + } + catch (const std::out_of_range& c) + { + std::cerr << "label of transacc " << fmt_ta(src, cond, dst, nacc) + << " not found.\n"; + throw c; + } +#else + return helper.get_ta(src, alpha_map[cond], dst, nacc); +#endif + } + + int + pathid(unsigned src_cand, unsigned src_ref, unsigned dst_cand, + unsigned dst_ref, acc_cond::mark_t acc_cand = 0U, + acc_cond::mark_t acc_ref = 0U) + { +#if DEBUG + try + { + return helper.get_p( + path_map.at(path(src_ref, dst_ref, acc_cand, acc_ref)), + src_cand, dst_cand); + } + catch (const std::out_of_range& c) + { + std::cerr << "path(" << src_ref << ',' << dst_ref << ",...) of pathid" + << ' ' + << fmt_p(src_cand, src_ref, dst_cand, dst_ref, acc_cand, acc_ref) + << " not found.\n"; + throw c; + } +#else + return helper.get_p( + path_map[path(src_ref, dst_ref, acc_cand, acc_ref)], + src_cand, dst_cand); +#endif + } + +#if DEBUG + int + pathid(unsigned path, unsigned src_cand, unsigned dst_cand) + { + return helper.get_p(path, src_cand, dst_cand); + } +#endif + + std::string + fmt_t(unsigned src, bdd& cond, unsigned dst) + { + return helper.format_t(debug_dict, src, cond, dst); + } + + std::string + fmt_t(unsigned src, unsigned cond, unsigned dst) + { + return helper.format_t(debug_dict, src, alpha_vect[cond], dst); + } + + std::string + fmt_ta(unsigned src, bdd& cond, unsigned dst, unsigned nacc) + { + return helper.format_ta(debug_dict, debug_cand_acc, src, cond, + dst, cacc.mark(nacc)); + } + + std::string + fmt_ta(unsigned src, unsigned cond, unsigned dst, unsigned nacc) + { + return helper.format_ta(debug_dict, debug_cand_acc, src, + alpha_vect[cond], dst, cacc.mark(nacc)); + } + + std::string + fmt_p(unsigned src_cand, unsigned src_ref, unsigned dst_cand, + unsigned dst_ref, acc_cond::mark_t acc_cand = 0U, + acc_cond::mark_t acc_ref = 0U) + { + return helper.format_p(debug_cand_acc, debug_ref_acc, src_cand, + src_ref, dst_cand, dst_ref, acc_cand, acc_ref); + } + acc_cond::mark_t inf_trim(acc_cond::mark_t m, trimming_map& tm) { @@ -418,7 +393,7 @@ namespace spot }; - unsigned declare_vars(const const_twa_graph_ptr& aut, + void declare_vars(const const_twa_graph_ptr& aut, dict& d, bdd ap, bool state_based, scc_info& sm) { d.is_weak_scc = sm.weak_sccs(); @@ -481,118 +456,77 @@ namespace spot } } - unsigned ref_size = aut->num_states(); + d.ref_size = aut->num_states(); if (d.cand_size == -1U) - for (unsigned i = 0; i < ref_size; ++i) + for (unsigned i = 0; i < d.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. - for (unsigned i = 0; i < ref_size; ++i) + // In order to optimize memory usage, src_cand & dst_cand have been + // removed from path struct (the reasons are: they were no optimization + // on them and their values are known from the beginning). + // + // However, since some optimizations are based on the following i, k, f, + // refhist, it is necessary to associate to each path constructed, + // an ID number. + // + // Given this ID, src_cand, dst_cand, the corresponding litteral can be + // retrived thanks to get_prc(...) a vars_helper's method. + unsigned path_size = 0; + for (unsigned i = 0; i < d.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]; - - for (unsigned j = 0; j < d.cand_size; ++j) + for (unsigned k = 0; k < d.ref_size; ++k) { - for (unsigned k = 0; k < ref_size; ++k) + if (!sm.reachable_state(k)) + continue; + if (sm.scc_of(k) != i_scc) + continue; + size_t sfp = is_weak ? 1 : d.all_ref_acc.size(); + acc_cond::mark_t sccmarks = d.scc_marks[i_scc]; + for (size_t fp = 0; fp < sfp; ++fp) { - if (!sm.reachable_state(k)) + auto refhist = d.all_ref_acc[fp]; + // refhist cannot have more sets than used in the SCC. + if (!is_weak && (sccmarks & refhist) != refhist) continue; - if (sm.scc_of(k) != i_scc) - continue; - for (unsigned l = 0; l < d.cand_size; ++l) + + size_t sf = d.all_cand_acc.size(); + for (size_t f = 0; f < sf; ++f) { - size_t sfp = is_weak ? 1 : d.all_ref_acc.size(); - acc_cond::mark_t sccmarks = d.scc_marks[i_scc]; - for (size_t fp = 0; fp < sfp; ++fp) - { - auto refhist = d.all_ref_acc[fp]; - // refhist cannot have more sets than used in the SCC - if (!is_weak && (sccmarks & refhist) != refhist) - continue; - - 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], refhist); - d.pathid[p] = ++d.nvars; - } - - } + path p(i, k, d.all_cand_acc[f], refhist); + d.path_map[p] = path_size++; } } } } - if (!state_based) + // Fill dict's bdd vetor (alpha_vect) and save each bdd and it's + // corresponding index in alpha_map. This is necessary beacause some + // loops start from a precise bdd. Therefore, it's useful to know + // it's corresponding index to deal with vars_helper. + bdd all = bddtrue; + for (unsigned j = 0; all != bddfalse; ++j) { - 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; - - 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.cacc.mark(n), j); - d.transaccid[ta] = ++d.nvars; - d.revtransaccid.emplace(d.nvars, ta); - } - } - } + bdd one = bdd_satoneset(all, ap, bddfalse); + d.alpha_vect.push_back(one); + d.alpha_map[d.alpha_vect[j]] = j; + all -= one; } - 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 = 0; 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.cacc.mark(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; + // Initialize vars_helper by giving it all the necessary information. + // false: means dtwasat, i-e not dtbasat. + d.helper.init(d.cand_size, d.alpha_vect.size(), d.cand_size, + d.cand_nacc, path_size, state_based, false); - transition t(i, one, j); - d.transid[t] = ++d.nvars; - d.revtransid.emplace(d.nvars, t); - } - } - } - return ref_size; + // Based on all previous informations, helper knows all litterals. + d.helper.declare_all_vars(++d.nvars); } typedef std::pair sat_stats; @@ -604,11 +538,8 @@ namespace spot #if DEBUG debug_dict = ref->get_dict(); #endif - - // Compute the AP used in the hard way. - bdd ap = bddtrue; - for (auto& t: ref->edges()) - ap &= bdd_support(t.cond); + // Compute the AP used. + bdd ap = ref->ap_vars(); // Count the number of atomic propositions int nap = 0; @@ -626,162 +557,122 @@ namespace spot sm.determine_unknown_acceptance(); // Number all the SAT variables we may need. - unsigned ref_size = declare_vars(ref, d, ap, state_based, sm); + declare_vars(ref, d, ap, state_based, sm); - // Tell the satsolver the number of variables + // Store alphabet size once for all. + unsigned alpha_size = d.alpha_vect.size(); + + // Tell the satsolver the number of variables. solver.adjust_nvars(d.nvars); - // empty automaton is impossible + // Empty automaton is impossible. assert(d.cand_size > 0); #if DEBUG debug_ref_acc = &ref->acc(); debug_cand_acc = &d.cacc; - solver.comment("ref_size:", ref_size, '\n'); - solver.comment("cand_size:", d.cand_size, '\n'); + solver.comment("d.ref_size:", d.ref_size, '\n'); + solver.comment("d.cand_size:", d.cand_size, '\n'); #endif auto& racc = ref->acc(); cnf_comment("symmetry-breaking clauses\n"); int j = 0; - bdd all = bddtrue; - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; - 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]; - cnf_comment("¬", t, '\n'); - solver.add({-ti, 0}); - } - ++j; - } + for (unsigned l = 0; l < alpha_size; ++l, ++j) + for (unsigned i = 0; i < d.cand_size - 1; ++i) + for (unsigned k = i * nap + j + 2; k < d.cand_size; ++k) + { + cnf_comment("¬", d.fmt_t(i, l, k), '\n'); + solver.add({-d.transid(i, l, k), 0}); + } + if (!solver.get_nb_clauses()) cnf_comment("(none)\n"); cnf_comment("(8) the candidate automaton is complete\n"); for (unsigned q1 = 0; q1 < d.cand_size; ++q1) - { - bdd all = bddtrue; - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; - + for (unsigned l = 0; l < alpha_size; ++l) + { #if DEBUG - solver.comment(""); - for (unsigned q2 = 0; q2 < d.cand_size; ++q2) - { - transition t(q1, s, q2); - solver.comment_rec(t, "δ"); - if (q2 != d.cand_size) - solver.comment_rec(" ∨ "); - } - solver.comment_rec('\n'); + solver.comment(""); + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) + { + solver.comment_rec(d.fmt_t(q1, l, q2), "δ"); + if (q2 != d.cand_size) + solver.comment_rec(" ∨ "); + } + solver.comment_rec('\n'); #endif - - for (unsigned q2 = 0; q2 < d.cand_size; ++q2) - { - transition t(q1, s, q2); - int ti = d.transid[t]; - - solver.add(ti); - } - solver.add(0); - } - } + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) + solver.add(d.transid(q1, l, q2)); + solver.add(0); + } cnf_comment("(9) the initial state is reachable\n"); { unsigned init = ref->get_init_state_number(); - cnf_comment(path(0, init), '\n'); - solver.add({d.pathid[path(0, init)], 0}); + cnf_comment(d.fmt_p(0, init, 0, init), '\n'); + solver.add({d.pathid(0, init, 0, init), 0}); } if (colored) { unsigned nacc = d.cand_nacc; cnf_comment("transitions belong to exactly one of the", nacc, - "acceptance set\n"); - bdd all = bddtrue; - while (all != bddfalse) - { - bdd l = bdd_satoneset(all, ap, bddfalse); - all -= l; - for (unsigned q1 = 0; q1 < d.cand_size; ++q1) - for (unsigned q2 = 0; q2 < d.cand_size; ++q2) - { - for (unsigned i = 0; i < nacc; ++i) - { - transition_acc ti(q1, l, {i}, q2); - int tai = d.transaccid[ti]; - - for (unsigned j = 0; j < nacc; ++j) - if (i != j) - { - transition_acc tj(q1, l, {j}, q2); - int taj = d.transaccid[tj]; - solver.add({-tai, -taj, 0}); - } - } - for (unsigned i = 0; i < nacc; ++i) - { - transition_acc ti(q1, l, {i}, q2); - int tai = d.transaccid[ti]; - solver.add(tai); - } - solver.add(0); - } - } + "acceptance set\n"); + for (unsigned l = 0; l < alpha_size; ++l) + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) + { + for (unsigned i = 0; i < nacc; ++i) + for (unsigned j = 0; j < nacc; ++j) + if (i != j) + solver.add( + {-d.transacc(q1, l, q2, i), + -d.transacc(q1, l, q2, j), + 0}); + for (unsigned i = 0; i < nacc; ++i) + solver.add(d.transacc(q1, l, q2, i)); + solver.add(0); + } } if (!d.all_silly_cand_acc.empty()) { cnf_comment("no transition with silly acceptance\n"); - bdd all = bddtrue; - while (all != bddfalse) - { - bdd l = bdd_satoneset(all, ap, bddfalse); - all -= l; - for (unsigned q1 = 0; q1 < d.cand_size; ++q1) - for (unsigned q2 = 0; q2 < d.cand_size; ++q2) - for (auto& s: d.all_silly_cand_acc) - { - cnf_comment("no (", q1, ',', - bdd_format_formula(debug_dict, l), ',', s, - ',', q2, ")\n"); - for (unsigned v: s.sets()) - { - transition_acc ta(q1, l, d.cacc.mark(v), q2); - int tai = d.transaccid[ta]; - assert(tai != 0); - solver.add(-tai); - } - for (unsigned v: d.cacc.comp(s).sets()) - { - transition_acc ta(q1, l, d.cacc.mark(v), q2); - int tai = d.transaccid[ta]; - assert(tai != 0); - solver.add(tai); - } - solver.add(0); - } - } + for (unsigned l = 0; l < alpha_size; ++l) + for (unsigned q1 = 0; q1 < d.cand_size; ++q1) + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) + for (auto& s: d.all_silly_cand_acc) + { + cnf_comment("no (", q1, ',', + bdd_format_formula(debug_dict, d.alpha_vect[l]), + ',', s, ',', q2, ")\n"); + for (unsigned v: s.sets()) + { + int tai = d.transacc(q1, l, q2, v); + assert(tai != 0); + solver.add(-tai); + } + for (unsigned v: d.cacc.comp(s).sets()) + { + int tai = d.transacc(q1, l, q2, v); + assert(tai != 0); + solver.add(tai); + } + solver.add(0); + } } for (unsigned q1 = 0; q1 < d.cand_size; ++q1) - for (unsigned q1p = 0; q1p < ref_size; ++q1p) + for (unsigned q1p = 0; q1p < d.ref_size; ++q1p) { if (!sm.reachable_state(q1p)) continue; cnf_comment("(10) augmenting paths based on Cand[", q1, "] and Ref[", q1p, "]\n"); - path p1(q1, q1p); - int p1id = d.pathid[p1]; + int p1id = d.pathid(q1, q1p, q1, q1p); for (auto& tr: ref->out(q1p)) { unsigned dp = tr.dst; @@ -793,29 +684,26 @@ namespace spot for (unsigned q2 = 0; q2 < d.cand_size; ++q2) { - transition t(q1, s, q2); - int ti = d.transid[t]; - - path p2(q2, dp); - int succ = d.pathid[p2]; - + int succ = d.pathid(q2, dp, q2, dp); if (p1id == succ) continue; - cnf_comment(p1, "∧", t, "δ →", p2, '\n'); - solver.add({-p1id, -ti, succ, 0}); + cnf_comment(d.fmt_p(q1, q1p, q1, q1p), " ∧ ", + d.fmt_t(q1, s, q2), "δ → ", + d.fmt_p(q2, dp, q2, dp), '\n'); + solver.add({-p1id, -d.transid(q1, s, q2), succ, 0}); } } } } // construction of constraints (11,12,13) - for (unsigned q1p = 0; q1p < ref_size; ++q1p) + for (unsigned q1p = 0; q1p < d.ref_size; ++q1p) { if (!sm.reachable_state(q1p)) continue; unsigned q1p_scc = sm.scc_of(q1p); - for (unsigned q2p = 0; q2p < ref_size; ++q2p) + for (unsigned q2p = 0; q2p < d.ref_size; ++q2p) { if (!sm.reachable_state(q2p)) continue; @@ -841,14 +729,12 @@ namespace spot if (!is_weak && (sccmarks & refhist) != refhist) continue; - path p(q1, q1p, q2, q2p, - d.all_cand_acc[f], refhist); - - cnf_comment("(11&12&13) paths from ", p, - '\n'); - - int pid = d.pathid[p]; - + acc_cond::mark_t candhist_p = d.all_cand_acc[f]; + std::string f_p = + d.fmt_p(q1, q1p, q2, q2p, candhist_p, refhist); + cnf_comment("(11&12&13) paths from ", f_p, '\n'); + int pid = + d.pathid(q1, q1p, q2, q2p, candhist_p, refhist); for (auto& tr: ref->out(q2p)) { unsigned dp = tr.dst; @@ -865,9 +751,7 @@ namespace spot bdd l = bdd_satoneset(all, ap, bddfalse); all -= l; - transition t(q2, l, q3); - int ti = d.transid[t]; - + int ti = d.transid(q2, l, q3); if (dp == q1p && q3 == q1) // (11,12) loop { bool rejloop = @@ -875,37 +759,26 @@ namespace spot !racc.accepting (curacc | d.all_ref_acc[fp])); - auto missing = - d.cand_acc. - missing(d.all_cand_acc[f], - !rejloop); + auto missing = d.cand_acc + .missing(candhist_p, !rejloop); for (auto& v: missing) { #if DEBUG solver.comment((rejloop ? - "(11) " : "(12) "), p, - " ∧ ", t, "δ → ("); + "(11) " : "(12) "), f_p, + " ∧ ", d.fmt_t(q2, l, q3), + "δ → ("); const char* orsep = ""; for (int s: v) { if (s < 0) - { - transition_acc - ta(q2, l, - d.cacc.mark(-s - 1), - q1); - solver.comment_rec(orsep, - "¬", ta); - } + solver.comment_rec(orsep, + "¬", d.fmt_ta( + q2, l, q1, -s - 1)); else - { - transition_acc - ta(q2, l, - d.cacc.mark(s), q1); - solver.comment_rec(orsep, - ta); - } + solver.comment_rec(orsep, + d.fmt_ta(q2, l, q1, s)); solver.comment_rec("FC"); orsep = " ∨ "; } @@ -915,20 +788,16 @@ namespace spot for (int s: v) if (s < 0) { - transition_acc - ta(q2, l, - d.cacc.mark(-s - 1), - q1); - int tai = d.transaccid[ta]; + int tai = + d.transacc(q2, l, q1, + -s - 1); assert(tai != 0); solver.add(-tai); } else { - transition_acc - ta(q2, l, - d.cacc.mark(s), q1); - int tai = d.transaccid[ta]; + int tai = + d.transacc(q2, l, q1, s); assert(tai != 0); solver.add(tai); } @@ -942,47 +811,42 @@ namespace spot { acc_cond::mark_t f2 = d.cand_inf_trim - (p.acc_cand | + (candhist_p | d.all_cand_acc[f]); acc_cond::mark_t f2p = 0U; if (!is_weak) - f2p = d.ref_inf_trim(p.acc_ref | + f2p = d.ref_inf_trim(refhist | curacc); - - path p2(p.src_cand, p.src_ref, - q3, dp, f2, f2p); - int p2id = d.pathid[p2]; + int p2id = d.pathid( + q1, q1p, q3, dp, f2, f2p); if (pid == p2id) continue; #if DEBUG - solver.comment("(13) ", p, " ∧ ", - t, "δ "); + solver.comment("(13) ", f_p, " ∧ ", + d.fmt_t(q1, l, q3), "δ "); auto biga_ = d.all_cand_acc[f]; for (unsigned m = 0; m < d.cand_nacc; ++m) { - transition_acc - ta(q2, l, - d.cacc.mark(m), q3); const char* not_ = "¬"; if (biga_.has(m)) not_ = ""; solver.comment_rec(" ∧ ", not_, - ta, "FC"); + d.fmt_ta(q2, l, q3, m), + "FC"); } - solver.comment_rec(" → ", p2, - '\n'); + solver.comment_rec(" → ", + d.fmt_p(q1, q1p, q3, dp, f2, + f2p), '\n'); #endif solver.add({-pid, -ti}); auto biga = d.all_cand_acc[f]; for (unsigned m = 0; m < d.cand_nacc; ++m) { - transition_acc - ta(q2, l, - d.cacc.mark(m), q3); - int tai = d.transaccid[ta]; + int tai = + d.transacc(q2, l, q3, m); if (biga.has(m)) tai = -tai; solver.add(tai); @@ -1004,6 +868,8 @@ namespace spot sat_build(const satsolver::solution& solution, dict& satdict, const_twa_graph_ptr aut, bool state_based) { + trace << "sat_build(..., state_based=" << state_based << ")\n"; + auto autdict = aut->get_dict(); auto a = make_twa_graph(autdict); a->copy_ap_of(aut); @@ -1013,90 +879,101 @@ namespace spot a->set_acceptance(satdict.cand_nacc, satdict.cand_acc); a->new_states(satdict.cand_size); - // Last transition set in the automaton. - unsigned last_aut_trans = -1U; - // Last transition read from the SAT result. - const transition* last_sat_trans = nullptr; - #if DEBUG std::fstream out("dtwa-sat.dbg", std::ios_base::trunc | std::ios_base::out); out.exceptions(std::ifstream::failbit | std::ifstream::badbit); - std::set positive; #endif - - dout << "--- transition variables ---\n"; std::map state_acc; std::set seen_trans; - for (int v: solution) - { - if (v < 0) // FIXME: maybe we can have (v < NNN)? - continue; -#if DEBUG - positive.insert(v); -#endif - - dict::rev_map::const_iterator t = satdict.revtransid.find(v); - - if (t != satdict.revtransid.end()) + unsigned alpha_size = satdict.alpha_vect.size(); + for (unsigned i = 0; i < satdict.cand_size; ++i) + for (unsigned j = 0; j < alpha_size; ++j) + for (unsigned k = 0; k < satdict.cand_size; ++k) + { + if (solution[satdict.transid(i, j, k) - 1]) { // Ignore unuseful transitions because of reduced cand_size. - if (t->second.src >= satdict.cand_size) + if (i >= satdict.cand_size) continue; // Skip (s,l,d2) if we have already seen some (s,l,d1). - if (seen_trans.insert(src_cond(t->second.src, - t->second.cond)).second) - { - acc_cond::mark_t acc = 0U; - if (state_based) - { - auto i = state_acc.find(t->second.src); - if (i != state_acc.end()) - acc = i->second; - } + if (seen_trans.insert(src_cond(i, satdict.alpha_vect[j])).second) + { + acc_cond::mark_t acc = 0U; + if (state_based) + { + auto tmp = state_acc.find(i); + if (tmp != state_acc.end()) + acc = tmp->second; + } - last_aut_trans = a->new_edge(t->second.src, - t->second.dst, - t->second.cond, acc); - last_sat_trans = &t->second; + for (unsigned n = 0; n < satdict.cand_nacc; ++n) + if (solution[satdict.transacc(i, j, k, n) - 1]) + acc |= satdict.cacc.mark(n); - dout << v << '\t' << t->second << "δ\n"; - } + a->new_edge(i, k, satdict.alpha_vect[j], acc); + } } - else - { - dict::rev_acc_map::const_iterator ta; - ta = satdict.revtransaccid.find(v); - // This assumes that the sat solvers output variables in - // increasing order. - if (ta != satdict.revtransaccid.end()) - { - dout << v << '\t' << ta->second << "F\n"; + } - if (last_sat_trans && - ta->second.src == last_sat_trans->src && - ta->second.cond == last_sat_trans->cond && - ta->second.dst == last_sat_trans->dst) - { - assert(!state_based); - auto& v = a->edge_data(last_aut_trans).acc; - v |= ta->second.acc; - } - else if (state_based) - { - auto& v = state_acc[ta->second.src]; - v |= ta->second.acc; - } - } - } - } #if DEBUG - dout << "--- pathid variables ---\n"; - for (auto pit: satdict.pathid) - if (positive.find(pit.second) != positive.end()) - dout << pit.second << '\t' << pit.first << "C\n"; + dout << "--- transition variables ---\n"; + for (unsigned i = 0; i < satdict.cand_size; ++i) + for (unsigned j = 0; j < alpha_size; ++j) + for (unsigned k = 0; k < satdict.cand_size; ++k) + { + int var = satdict.transid(i, j, k); + std::string f_t = satdict.fmt_t(i, j, k); + if (solution[var - 1]) + dout << ' ' << var << "\t " << f_t << '\n'; + else + dout << -var << "\t¬" << f_t << '\n'; + } + dout << "--- transition_acc variables ---\n"; + if (state_based) + { + dout << "In state_based mode, there is only 1 litteral for each " + "combination of src and nacc, regardless of dst or cond!\n"; + for (unsigned i = 0; i < satdict.cand_size; ++i) + for (unsigned j = 0; j < satdict.cand_nacc; ++j) + { + int var = satdict.transacc(i, 0, 0, j); + std::string f_ta = satdict.fmt_ta(i, 0, 0, j); + if (solution[var - 1]) + dout << ' ' << var << "\t " << f_ta << '\n'; + else + dout << -var << "\t¬" << f_ta << '\n'; + } + } + else + for (unsigned i = 0; i < satdict.cand_size; ++i) + for (unsigned j = 0; j < alpha_size; ++j) + for (unsigned k = 0; k < satdict.cand_size; ++k) + for (unsigned l = 0; l < satdict.cand_nacc; ++l) + { + int var = satdict.transacc(i, j, k, l); + std::string f_ta = satdict.fmt_ta(i, j, k, l); + if (solution[var - 1]) + dout << ' ' << var << "\t " << f_ta << '\n'; + else + dout << -var << "\t¬" << f_ta << '\n'; + } + dout << "--- path_map variables ---\n"; + for (auto it = satdict.path_map.begin(); it != satdict.path_map.end(); + ++it) + for (unsigned k = 0; k < satdict.cand_size; ++k) + for (unsigned l = 0; l < satdict.cand_size; ++l) + { + int var = satdict.pathid(it->second, k, l); + std::string f_p = satdict.fmt_p(k, it->first.src_ref, l, + it->first.dst_ref, it->first.acc_cand, it->first.acc_ref); + if (solution[var - 1]) + dout << ' ' << var << "\t " << f_p << '\n'; + else + dout << -var << "\t¬" << f_p << '\n'; + } #endif a->merge_edges(); @@ -1128,7 +1005,7 @@ namespace spot timer_map t; t.start("encode"); - sat_stats s = dtwa_to_sat(solver, a, d, state_based, colored); + dtwa_to_sat(solver, a, d, state_based, colored); t.stop("encode"); t.start("solve"); solution = solver.get_solution(); @@ -1138,41 +1015,8 @@ namespace spot if (!solution.second.empty()) res = sat_build(solution.second, d, a, state_based); - // Always copy the environment variable into a static string, - // so that we (1) look it up once, but (2) won't crash if the - // environment is changed. - static std::string log = []() - { - auto s = getenv("SPOT_SATLOG"); - return s ? s : ""; - }(); - if (!log.empty()) - { - std::fstream out(log, - std::ios_base::app | std::ios_base::out); - out.exceptions(std::ifstream::failbit | std::ifstream::badbit); - const timer& te = t.timer("encode"); - const timer& ts = t.timer("solve"); - out << target_state_number << ','; - if (res) - { - twa_sub_statistics st = sub_stats_reachable(res); - out << st.states << ',' << st.edges << ',' << st.transitions; - } - else - { - out << ",,"; - } - out << ',' - << s.first << ',' << s.second << ',' - << te.utime() + te.cutime() << ',' - << te.stime() + te.cstime() << ',' - << ts.utime() + ts.cutime() << ',' - << ts.stime() + ts.cstime() << '\n'; - } - static bool show = getenv("SPOT_SATSHOW"); - if (show && res) - print_dot(std::cout, res); + // Print log if env var SPOT_SATLOG is set. + print_log(t, target_state_number, res, solver); trace << "dtwa_sat_synthetize(...) = " << res << '\n'; return res; diff --git a/tests/core/readsat.cc b/tests/core/readsat.cc index e661ee466..3301f9b21 100644 --- a/tests/core/readsat.cc +++ b/tests/core/readsat.cc @@ -18,12 +18,13 @@ // along with this program. If not, see . #include +#include #include int main() { - spot::satsolver::solution sol = spot::satsolver_get_solution("-"); - for (spot::satsolver::solution::const_iterator i = sol.begin(); + std::vector sol = spot::satsolver_get_solution("-"); + for (std::vector::const_iterator i = sol.begin(); i != sol.end(); ++i) std::cout << ' ' << *i; std::cout << '\n'; diff --git a/tests/core/satmin.test b/tests/core/satmin.test index f8fdc81fb..7145c9e46 100755 --- a/tests/core/satmin.test +++ b/tests/core/satmin.test @@ -37,7 +37,7 @@ ltlcross=ltlcross # (a U X!a) | XG(!b & XFc) # XXG(Fa U Xb) # -# Those one where removed because they were too long in the "expected" file. +# Those ones were removed because they were too long in the "expected" file. # We can not exceed 80 characters! # # p U (q & X(r & F(s & XF(u & XF(v & XFw))))) diff --git a/tests/core/satmin2.test b/tests/core/satmin2.test index 8db6770f3..f19cbf7db 100755 --- a/tests/core/satmin2.test +++ b/tests/core/satmin2.test @@ -149,8 +149,8 @@ properties: trans-labels explicit-labels trans-acc colored complete properties: deterministic --BODY-- State: 0 -[!0] 0 {0} -[0] 0 {1} +[0] 0 {0} +[!0] 0 {1} --END-- EOF