spot  2.12
aiger.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) by the Spot authors, see the AUTHORS file for details.
3 //
4 // This file is part of Spot, a model checking library.
5 //
6 // Spot is free software; you can redistribute it and/or modify it
7 // under the terms of the GNU General Public License as published by
8 // the Free Software Foundation; either version 3 of the License, or
9 // (at your option) any later version.
10 //
11 // Spot is distributed in the hope that it will be useful, but WITHOUT
12 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
13 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
14 // License for more details.
15 //
16 // You should have received a copy of the GNU General Public License
17 // along with this program. If not, see <http://www.gnu.org/licenses/>.
18 
19 #pragma once
20 
21 #include <iosfwd>
22 #include <spot/misc/common.hh>
23 #include <spot/misc/bddlt.hh>
24 #include <spot/twa/fwd.hh>
25 #include <spot/twa/bdddict.hh>
26 #include <spot/tl/formula.hh>
27 #include <spot/tl/apcollect.hh>
28 
29 #include <unordered_map>
30 #include <vector>
31 #include <set>
32 #include <memory>
33 #include <algorithm> // std::none_of
34 #include <sstream>
35 
36 
37 namespace spot
38 {
39  // Forward for synthesis
40  struct mealy_like;
41 
42  class aig;
43 
44  typedef std::shared_ptr<aig> aig_ptr;
45  typedef std::shared_ptr<const aig> const_aig_ptr;
46 
59  class SPOT_API aig
60  {
61  protected:
62  const unsigned num_inputs_;
63  const unsigned num_outputs_;
64  const unsigned num_latches_;
65  const std::vector<std::string> input_names_;
66  const std::vector<std::string> output_names_;
67  unsigned max_var_;
68 
69  std::vector<unsigned> next_latches_;
70  std::vector<unsigned> outputs_;
71  std::vector<std::pair<unsigned, unsigned>> and_gates_;
72  bdd_dict_ptr dict_;
73  // Cache the function computed by each variable as a bdd.
74  // Bidirectional map
75  std::unordered_map<unsigned, bdd> var2bdd_;
76  std::unordered_map<int, unsigned> bdd2var_; //uses id
77  // First anonymous var marking the beginning of variables used
78  // as latches
79  int l0_;
80 
81  bdd all_ins_;
82  bdd all_latches_;
83 
84  // For simulation
85  std::vector<bool> state_;
86 
87  public:
88 
94  using safe_point = std::pair<unsigned, unsigned>;
95  using safe_stash =
96  std::tuple<std::vector<std::pair<unsigned, unsigned>>,
97  std::vector<std::pair<unsigned, bdd>>,
98  std::vector<bdd>>;
99 
104  aig(const std::vector<std::string>& inputs,
105  const std::vector<std::string>& outputs,
106  unsigned num_latches,
107  bdd_dict_ptr dict = make_bdd_dict());
108 
110  aig(unsigned num_inputs, unsigned num_outputs,
111  unsigned num_latches, bdd_dict_ptr dict = make_bdd_dict());
112 
113  ~aig()
114  {
115  dict_->unregister_all_my_variables(this);
116  }
117 
118  protected:
120  void register_new_lit_(unsigned v, const bdd &b);
121  void register_latch_(unsigned i, const bdd& b);
122  void register_input_(unsigned i, const bdd& b);
124  void unregister_lit_(unsigned v);
125 
128  void split_cond_(const bdd& b, char so_mode,
129  std::vector<bdd>& cond_parts);
130 
132  bdd accum_common_(const bdd& b) const;
133 
135  unsigned cube2var_(const bdd& b, const int use_split_off);
136 
137  public:
138 
147 
155  safe_stash roll_back_(safe_point sp,
156  bool do_stash = false);
161  void reapply_(safe_point sp, const safe_stash& ss);
162 
164  unsigned num_outputs() const
165  {
166  return num_outputs_;
167  }
170  const std::vector<unsigned>& outputs() const
171  {
172  SPOT_ASSERT(std::none_of(outputs_.begin(), outputs_.end(),
173  [](unsigned o){return o == -1u; }));
174  return outputs_;
175  }
176 
180  unsigned output(unsigned num) const
181  {
182  return outputs_[num];
183  }
184 
186  const std::vector<std::string>& output_names() const
187  {
188  return output_names_;
189  }
190 
192  unsigned num_inputs() const
193  {
194  return num_inputs_;
195  }
197  const std::vector<std::string>& input_names() const
198  {
199  return input_names_;
200  }
201 
203  unsigned num_latches() const
204  {
205  return num_latches_;
206  }
210  const std::vector<unsigned>& next_latches() const
211  {
212  SPOT_ASSERT(std::none_of(next_latches_.begin(), next_latches_.end(),
213  [](unsigned o){return o == -1u; }));
214  return next_latches_;
215  };
216 
218  unsigned num_gates() const
219  {
220  return and_gates_.size();
221  };
223  const std::vector<std::pair<unsigned, unsigned>>& gates() const
224  {
225  return and_gates_;
226  };
227 
229  unsigned max_var() const
230  {
231  return max_var_;
232  };
233 
235  unsigned input_var(unsigned i, bool neg = false) const
236  {
237  SPOT_ASSERT(i < num_inputs_);
238  return (1 + i) * 2 + neg;
239  }
241  bdd input_bdd(unsigned i, bool neg = false) const
242  {
243  return aigvar2bdd(input_var(i, neg));
244  }
245 
247  unsigned latch_var(unsigned i, bool neg = false) const
248  {
249  SPOT_ASSERT(i < num_latches_);
250  return (1 + num_inputs_ + i) * 2 + neg;
251  }
253  bdd latch_bdd(unsigned i, bool neg = false) const
254  {
255  return aigvar2bdd(latch_var(i, neg));
256  }
257 
259  unsigned gate_var(unsigned i, bool neg = false) const
260  {
261  SPOT_ASSERT(i < num_gates());
262  return (1 + num_inputs_ + num_latches_ + i) * 2 + neg;
263  }
265  bdd gate_bdd(unsigned i, bool neg = false) const
266  {
267  return aigvar2bdd(gate_var(i, neg));
268  }
269 
272  bdd aigvar2bdd(unsigned v, bool neg = false) const
273  {
274  return neg ? bdd_not(var2bdd_.at(v)) : var2bdd_.at(v);
275  }
276 
279  unsigned bdd2aigvar(const bdd& b) const
280  {
281  return bdd2var_.at(b.id());
282  }
283 
285  unsigned bdd2INFvar(const bdd& b);
286 
288  unsigned bdd2ISOPvar(const bdd& b, const int use_split_off = 0);
289 
307  unsigned encode_bdd(const std::vector<bdd>& c_alt,
308  char method = 1, bool use_dual = false,
309  int use_split_off = 0);
310 
312  unsigned encode_bdd(const bdd& b,
313  char method = 1, bool use_dual = false,
314  int use_split_off = 0);
315 
317  void set_output(unsigned i, unsigned v);
318 
320  void set_next_latch(unsigned i, unsigned v);
321 
322  static constexpr unsigned aig_true() noexcept
323  {
324  return 1;
325  };
326 
327  static constexpr unsigned aig_false() noexcept
328  {
329  return 0;
330  };
331 
333  unsigned aig_not(unsigned v);
334 
336  unsigned aig_and(unsigned v1, unsigned v2);
337 
341  unsigned aig_and(std::vector<unsigned>& vs);
342 
344  unsigned aig_or(unsigned v1, unsigned v2);
345 
349  unsigned aig_or(std::vector<unsigned>& vs);
350 
352  unsigned aig_pos(unsigned v);
353 
360  void encode_all_bdds(const std::vector<bdd>& all_bdd);
361 
369  static aig_ptr
370  parse_aag(const std::string& aig_file,
371  bdd_dict_ptr dict = make_bdd_dict());
372 
373  static aig_ptr
374  parse_aag(const char* data,
375  const std::string& filename,
376  bdd_dict_ptr dict = make_bdd_dict());
377 
378  static aig_ptr
379  parse_aag(std::istream& iss,
380  const std::string& filename,
381  bdd_dict_ptr dict = make_bdd_dict());
382 
387  twa_graph_ptr as_automaton(bool keepsplit = false) const;
388 
397  const std::vector<bool>& circ_state() const
398  {
399  SPOT_ASSERT(state_.size() == max_var_ + 2
400  && "State vector does not have the correct size.\n"
401  "Forgot to initialize?");
402  return state_;
403  }
404 
406  bool circ_state_of(unsigned var) const
407  {
408  SPOT_ASSERT(var <= max_var_ + 1
409  && "Variable out of range");
410  return circ_state()[var];
411  }
412 
415  void circ_init();
416 
423  void circ_step(const std::vector<bool>& inputs);
424 
425  };
426 
452  SPOT_API aig_ptr
453  mealy_machine_to_aig(const const_twa_graph_ptr& m, const char* mode);
454  SPOT_API aig_ptr
455  mealy_machine_to_aig(const twa_graph_ptr& m, const char *mode,
456  const std::vector<std::string>& ins,
457  const std::vector<std::string>& outs,
458  const realizability_simplifier* rs = nullptr);
459 
460  SPOT_API aig_ptr
461  mealy_machine_to_aig(const mealy_like& m, const char* mode);
462  SPOT_API aig_ptr
463  mealy_machine_to_aig(mealy_like& m, const char *mode,
464  const std::vector<std::string>& ins,
465  const std::vector<std::string>& outs,
466  const realizability_simplifier* rs = nullptr);
468 
486  SPOT_API aig_ptr
487  mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
488  const char* mode);
489  SPOT_API aig_ptr
490  mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
491  const char* mode);
492  SPOT_API aig_ptr
493  mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
494  const char* mode,
495  const std::vector<std::string>& ins,
496  const std::vector<std::vector<std::string>>& outs,
497  const realizability_simplifier* rs = nullptr);
498  SPOT_API aig_ptr
499  mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
500  const char* mode,
501  const std::vector<std::string>& ins,
502  const std::vector<std::vector<std::string>>& outs,
503  const realizability_simplifier* rs = nullptr);
505 
508  SPOT_API std::ostream&
509  print_aiger(std::ostream& os, const_aig_ptr circuit);
510 
546  SPOT_API std::ostream&
547  print_aiger(std::ostream& os, const const_twa_graph_ptr& aut,
548  const char* mode);
549 }
A class representing AIG circuits.
Definition: aiger.hh:60
bdd gate_bdd(unsigned i, bool neg=false) const
Get the bdd associated to the ith gate.
Definition: aiger.hh:265
unsigned encode_bdd(const std::vector< bdd > &c_alt, char method=1, bool use_dual=false, int use_split_off=0)
Add a bdd to the circuit Assumes that all bdd's given in c_alt fulfill the same purpose,...
bdd aigvar2bdd(unsigned v, bool neg=false) const
Get the bdd associated to a variable.
Definition: aiger.hh:272
static aig_ptr parse_aag(const std::string &aig_file, bdd_dict_ptr dict=make_bdd_dict())
Create a circuit from an aag file with restricted syntax.
twa_graph_ptr as_automaton(bool keepsplit=false) const
Transform the circuit onto an equivalent monitor.
void reapply_(safe_point sp, const safe_stash &ss)
Reapply to stored changes on top of a safe_point.
std::pair< unsigned, unsigned > safe_point
Mark the beginning of a test translation.
Definition: aiger.hh:94
unsigned gate_var(unsigned i, bool neg=false) const
Get the variable associated to the ith gate.
Definition: aiger.hh:259
const std::vector< std::pair< unsigned, unsigned > > & gates() const
Access the underlying container.
Definition: aiger.hh:223
void unregister_lit_(unsigned v)
Remove a literal from both maps.
unsigned aig_and(unsigned v1, unsigned v2)
Compute AND of v1 and v2.
unsigned num_gates() const
Get the total number of and gates.
Definition: aiger.hh:218
unsigned output(unsigned num) const
return the variable associated to output num
Definition: aiger.hh:180
safe_point get_safe_point_() const
Safe the current state of the circuit.
const std::vector< unsigned > & next_latches() const
Get the variables associated to the state of the latches in the next iteration.
Definition: aiger.hh:210
unsigned aig_pos(unsigned v)
Returns the positive form of the given variable.
const std::vector< std::string > & output_names() const
Get the set of output names.
Definition: aiger.hh:186
unsigned bdd2aigvar(const bdd &b) const
Get the variable associated to a bdd.
Definition: aiger.hh:279
unsigned num_inputs() const
Get the number of inputs.
Definition: aiger.hh:192
void circ_init()
(Re)initialize the stepwise evaluation of the circuit. This sets all latches to 0 and clears the outp...
bdd input_bdd(unsigned i, bool neg=false) const
Get the bdd associated to the ith input.
Definition: aiger.hh:241
unsigned input_var(unsigned i, bool neg=false) const
Get the variable associated to the ith input.
Definition: aiger.hh:235
unsigned encode_bdd(const bdd &b, char method=1, bool use_dual=false, int use_split_off=0)
Just like the vector version but with no alternatives given.
aig(unsigned num_inputs, unsigned num_outputs, unsigned num_latches, bdd_dict_ptr dict=make_bdd_dict())
Constructing the circuit with generic names.
unsigned aig_and(std::vector< unsigned > &vs)
Computes the AND of all vars.
unsigned num_outputs() const
Get the number of outputs.
Definition: aiger.hh:164
aig(const std::vector< std::string > &inputs, const std::vector< std::string > &outputs, unsigned num_latches, bdd_dict_ptr dict=make_bdd_dict())
Constructing an "empty" aig, knowing only about the necessary inputs, outputs and latches....
unsigned cube2var_(const bdd &b, const int use_split_off)
Translate a cube into gates, using split-off optionally.
unsigned num_latches() const
Get the number of latches in the circuit.
Definition: aiger.hh:203
bdd accum_common_(const bdd &b) const
Split-off common sub-expressions as cube.
void set_output(unsigned i, unsigned v)
Associate the ith output to the variable v.
unsigned bdd2INFvar(const bdd &b)
Add a bdd to the circuit using if-then-else normal form.
void set_next_latch(unsigned i, unsigned v)
Associate the ith latch state after update to the variable v.
unsigned aig_not(unsigned v)
Negate a variable.
const std::vector< bool > & circ_state() const
Gives access to the current state of the circuit.
Definition: aiger.hh:397
safe_stash roll_back_(safe_point sp, bool do_stash=false)
roll_back to the saved point.
unsigned latch_var(unsigned i, bool neg=false) const
Get the variable associated to the ith latch.
Definition: aiger.hh:247
void circ_step(const std::vector< bool > &inputs)
Performs the next discrete step of the circuit, based on the inputs.
unsigned aig_or(unsigned v1, unsigned v2)
Computes the OR of v1 and v2.
const std::vector< std::string > & input_names() const
Get the set of input names.
Definition: aiger.hh:197
const std::vector< unsigned > & outputs() const
Get the variables associated to the outputs.
Definition: aiger.hh:170
bdd latch_bdd(unsigned i, bool neg=false) const
Get the bdd associated to the ith latch.
Definition: aiger.hh:253
unsigned aig_or(std::vector< unsigned > &vs)
Computes the or of all vars.
void encode_all_bdds(const std::vector< bdd > &all_bdd)
Instead of successively adding bdds to the circuit, one can also pass a vector of all bdds needed to ...
unsigned bdd2ISOPvar(const bdd &b, const int use_split_off=0)
Add a bdd to the circuit using isop normal form.
void register_new_lit_(unsigned v, const bdd &b)
Register a new literal in both maps.
bool circ_state_of(unsigned var) const
Access to the state of a specific variable.
Definition: aiger.hh:406
void split_cond_(const bdd &b, char so_mode, std::vector< bdd > &cond_parts)
Internal function that split a bdd into a conjunction hoping to increase reusage of gates.
unsigned max_var() const
Maximal variable index currently appearing in the circuit.
Definition: aiger.hh:229
Simplify a reactive specification, preserving realizability.
Definition: apcollect.hh:82
LTL/PSL formula interface.
aig_ptr mealy_machine_to_aig(const const_twa_graph_ptr &m, const char *mode)
Convert a mealy (like) machine into an aig relying on the transformation described by mode.
aig_ptr mealy_machines_to_aig(const std::vector< const_twa_graph_ptr > &m_vec, const char *mode)
Convert multiple mealy machines into an aig relying on the transformation described by mode.
std::ostream & print_aiger(std::ostream &os, const_aig_ptr circuit)
Print the aig to stream in AIGER format.
Definition: automata.hh:26
A struct that represents different types of mealy like objects.
Definition: synthesis.hh:196

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1