satcommon.hh 8.19 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
// -*- 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 <http://www.gnu.org/licenses/>.

#pragma once

#include <tuple>
#include <sstream>
24
#include <vector>
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
#include <spot/misc/bddlt.hh>
#include <spot/misc/satsolver.hh>
#include <spot/misc/timer.hh>
#include <spot/twa/twagraph.hh>

#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);
239
240
241
242

  /// \brief Returns the number of distinct values containted in a vector.
  int
  get_number_of_distinct_vals(std::vector<unsigned> v);
243
}