spot 2.11.6.dev
Loading...
Searching...
No Matches
aiger.hh
1// -*- coding: utf-8 -*-
2// Copyright (C) 2020-2021, 2023 Laboratoire de Recherche et
3// Développement de l'Epita (LRDE).
4//
5// This file is part of Spot, a model checking library.
6//
7// Spot is free software; you can redistribute it and/or modify it
8// under the terms of the GNU General Public License as published by
9// the Free Software Foundation; either version 3 of the License, or
10// (at your option) any later version.
11//
12// Spot is distributed in the hope that it will be useful, but WITHOUT
13// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15// License for more details.
16//
17// You should have received a copy of the GNU General Public License
18// along with this program. If not, see <http://www.gnu.org/licenses/>.
19
20#pragma once
21
22#include <iosfwd>
23#include <spot/misc/common.hh>
24#include <spot/misc/bddlt.hh>
25#include <spot/twa/fwd.hh>
26#include <spot/twa/bdddict.hh>
27#include <spot/tl/formula.hh>
28#include <spot/tl/apcollect.hh>
29
30#include <unordered_map>
31#include <vector>
32#include <set>
33#include <memory>
34#include <algorithm> // std::none_of
35#include <sstream>
36
37
38namespace spot
39{
40 // Forward for synthesis
41 struct mealy_like;
42
43 class aig;
44
45 typedef std::shared_ptr<aig> aig_ptr;
46 typedef std::shared_ptr<const aig> const_aig_ptr;
47
60 class SPOT_API aig
61 {
62 protected:
63 const unsigned num_inputs_;
64 const unsigned num_outputs_;
65 const unsigned num_latches_;
66 const std::vector<std::string> input_names_;
67 const std::vector<std::string> output_names_;
68 unsigned max_var_;
69
70 std::vector<unsigned> next_latches_;
71 std::vector<unsigned> outputs_;
72 std::vector<std::pair<unsigned, unsigned>> and_gates_;
73 bdd_dict_ptr dict_;
74 // Cache the function computed by each variable as a bdd.
75 // Bidirectional map
76 std::unordered_map<unsigned, bdd> var2bdd_;
77 std::unordered_map<int, unsigned> bdd2var_; //uses id
78 // First anonymous var marking the beginning of variables used
79 // as latches
80 int l0_;
81
82 bdd all_ins_;
83 bdd all_latches_;
84
85 // For simulation
86 std::vector<bool> state_;
87
88 public:
89
95 using safe_point = std::pair<unsigned, unsigned>;
96 using safe_stash =
97 std::tuple<std::vector<std::pair<unsigned, unsigned>>,
98 std::vector<std::pair<unsigned, bdd>>,
99 std::vector<bdd>>;
100
105 aig(const std::vector<std::string>& inputs,
106 const std::vector<std::string>& outputs,
107 unsigned num_latches,
108 bdd_dict_ptr dict = make_bdd_dict());
109
111 aig(unsigned num_inputs, unsigned num_outputs,
112 unsigned num_latches, bdd_dict_ptr dict = make_bdd_dict());
113
114 ~aig()
115 {
116 dict_->unregister_all_my_variables(this);
117 }
118
119 protected:
121 void register_new_lit_(unsigned v, const bdd &b);
122 void register_latch_(unsigned i, const bdd& b);
123 void register_input_(unsigned i, const bdd& b);
125 void unregister_lit_(unsigned v);
126
129 void split_cond_(const bdd& b, char so_mode,
130 std::vector<bdd>& cond_parts);
131
133 bdd accum_common_(const bdd& b) const;
134
136 unsigned cube2var_(const bdd& b, const int use_split_off);
137
138 public:
139
148
156 safe_stash roll_back_(safe_point sp,
157 bool do_stash = false);
162 void reapply_(safe_point sp, const safe_stash& ss);
163
165 unsigned num_outputs() const
166 {
167 return num_outputs_;
168 }
171 const std::vector<unsigned>& outputs() const
172 {
173 SPOT_ASSERT(std::none_of(outputs_.begin(), outputs_.end(),
174 [](unsigned o){return o == -1u; }));
175 return outputs_;
176 }
177
181 unsigned output(unsigned num) const
182 {
183 return outputs_[num];
184 }
185
187 const std::vector<std::string>& output_names() const
188 {
189 return output_names_;
190 }
191
193 unsigned num_inputs() const
194 {
195 return num_inputs_;
196 }
198 const std::vector<std::string>& input_names() const
199 {
200 return input_names_;
201 }
202
204 unsigned num_latches() const
205 {
206 return num_latches_;
207 }
211 const std::vector<unsigned>& next_latches() const
212 {
213 SPOT_ASSERT(std::none_of(next_latches_.begin(), next_latches_.end(),
214 [](unsigned o){return o == -1u; }));
215 return next_latches_;
216 };
217
219 unsigned num_gates() const
220 {
221 return and_gates_.size();
222 };
224 const std::vector<std::pair<unsigned, unsigned>>& gates() const
225 {
226 return and_gates_;
227 };
228
230 unsigned max_var() const
231 {
232 return max_var_;
233 };
234
236 unsigned input_var(unsigned i, bool neg = false) const
237 {
238 SPOT_ASSERT(i < num_inputs_);
239 return (1 + i) * 2 + neg;
240 }
242 bdd input_bdd(unsigned i, bool neg = false) const
243 {
244 return aigvar2bdd(input_var(i, neg));
245 }
246
248 unsigned latch_var(unsigned i, bool neg = false) const
249 {
250 SPOT_ASSERT(i < num_latches_);
251 return (1 + num_inputs_ + i) * 2 + neg;
252 }
254 bdd latch_bdd(unsigned i, bool neg = false) const
255 {
256 return aigvar2bdd(latch_var(i, neg));
257 }
258
260 unsigned gate_var(unsigned i, bool neg = false) const
261 {
262 SPOT_ASSERT(i < num_gates());
263 return (1 + num_inputs_ + num_latches_ + i) * 2 + neg;
264 }
266 bdd gate_bdd(unsigned i, bool neg = false) const
267 {
268 return aigvar2bdd(gate_var(i, neg));
269 }
270
273 bdd aigvar2bdd(unsigned v, bool neg = false) const
274 {
275 return neg ? bdd_not(var2bdd_.at(v)) : var2bdd_.at(v);
276 }
277
280 unsigned bdd2aigvar(const bdd& b) const
281 {
282 return bdd2var_.at(b.id());
283 }
284
286 unsigned bdd2INFvar(const bdd& b);
287
289 unsigned bdd2ISOPvar(const bdd& b, const int use_split_off = 0);
290
308 unsigned encode_bdd(const std::vector<bdd>& c_alt,
309 char method = 1, bool use_dual = false,
310 int use_split_off = 0);
311
313 unsigned encode_bdd(const bdd& b,
314 char method = 1, bool use_dual = false,
315 int use_split_off = 0);
316
318 void set_output(unsigned i, unsigned v);
319
321 void set_next_latch(unsigned i, unsigned v);
322
323 static constexpr unsigned aig_true() noexcept
324 {
325 return 1;
326 };
327
328 static constexpr unsigned aig_false() noexcept
329 {
330 return 0;
331 };
332
334 unsigned aig_not(unsigned v);
335
337 unsigned aig_and(unsigned v1, unsigned v2);
338
342 unsigned aig_and(std::vector<unsigned>& vs);
343
345 unsigned aig_or(unsigned v1, unsigned v2);
346
350 unsigned aig_or(std::vector<unsigned>& vs);
351
353 unsigned aig_pos(unsigned v);
354
361 void encode_all_bdds(const std::vector<bdd>& all_bdd);
362
370 static aig_ptr
371 parse_aag(const std::string& aig_file,
372 bdd_dict_ptr dict = make_bdd_dict());
373
374 static aig_ptr
375 parse_aag(const char* data,
376 const std::string& filename,
377 bdd_dict_ptr dict = make_bdd_dict());
378
379 static aig_ptr
380 parse_aag(std::istream& iss,
381 const std::string& filename,
382 bdd_dict_ptr dict = make_bdd_dict());
383
388 twa_graph_ptr as_automaton(bool keepsplit = false) const;
389
398 const std::vector<bool>& circ_state() const
399 {
400 SPOT_ASSERT(state_.size() == max_var_ + 2
401 && "State vector does not have the correct size.\n"
402 "Forgot to initialize?");
403 return state_;
404 }
405
407 bool circ_state_of(unsigned var) const
408 {
409 SPOT_ASSERT(var <= max_var_ + 1
410 && "Variable out of range");
411 return circ_state()[var];
412 }
413
416 void circ_init();
417
424 void circ_step(const std::vector<bool>& inputs);
425
426 };
427
453 SPOT_API aig_ptr
454 mealy_machine_to_aig(const const_twa_graph_ptr& m, const char* mode);
455 SPOT_API aig_ptr
456 mealy_machine_to_aig(const twa_graph_ptr& m, const char *mode,
457 const std::vector<std::string>& ins,
458 const std::vector<std::string>& outs,
459 const realizability_simplifier* rs = nullptr);
460
461 SPOT_API aig_ptr
462 mealy_machine_to_aig(const mealy_like& m, const char* mode);
463 SPOT_API aig_ptr
464 mealy_machine_to_aig(mealy_like& m, const char *mode,
465 const std::vector<std::string>& ins,
466 const std::vector<std::string>& outs,
467 const realizability_simplifier* rs = nullptr);
469
487 SPOT_API aig_ptr
488 mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
489 const char* mode);
490 SPOT_API aig_ptr
491 mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
492 const char* mode);
493 SPOT_API aig_ptr
494 mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
495 const char* mode,
496 const std::vector<std::string>& ins,
497 const std::vector<std::vector<std::string>>& outs,
498 const realizability_simplifier* rs = nullptr);
499 SPOT_API aig_ptr
500 mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
501 const char* mode,
502 const std::vector<std::string>& ins,
503 const std::vector<std::vector<std::string>>& outs,
504 const realizability_simplifier* rs = nullptr);
506
509 SPOT_API std::ostream&
510 print_aiger(std::ostream& os, const_aig_ptr circuit);
511
547 SPOT_API std::ostream&
548 print_aiger(std::ostream& os, const const_twa_graph_ptr& aut,
549 const char* mode);
550}
A class representing AIG circuits.
Definition aiger.hh:61
bdd gate_bdd(unsigned i, bool neg=false) const
Get the bdd associated to the ith gate.
Definition aiger.hh:266
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:273
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.
const std::vector< std::pair< unsigned, unsigned > > & gates() const
Access the underlying container.
Definition aiger.hh:224
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 tranlation.
Definition aiger.hh:95
const std::vector< unsigned > & outputs() const
Get the variables associated to the outputs.
Definition aiger.hh:171
unsigned gate_var(unsigned i, bool neg=false) const
Get the variable associated to the ith gate.
Definition aiger.hh:260
const std::vector< unsigned > & next_latches() const
Get the variables associated to the state of the latches in the next iteration.
Definition aiger.hh:211
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:219
unsigned output(unsigned num) const
return the variable associated to output num
Definition aiger.hh:181
safe_point get_safe_point_() const
Safe the current state of the circuit.
const std::vector< std::string > & output_names() const
Get the set of output names.
Definition aiger.hh:187
unsigned aig_pos(unsigned v)
Returns the positive form of the given variable.
unsigned bdd2aigvar(const bdd &b) const
Get the variable associated to a bdd.
Definition aiger.hh:280
unsigned num_inputs() const
Get the number of inputs.
Definition aiger.hh:193
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:242
unsigned input_var(unsigned i, bool neg=false) const
Get the variable associated to the ith input.
Definition aiger.hh:236
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.
const std::vector< std::string > & input_names() const
Get the set of input names.
Definition aiger.hh:198
unsigned num_outputs() const
Get the number of outputs.
Definition aiger.hh:165
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:204
const std::vector< bool > & circ_state() const
Gives access to the current state of the circuit.
Definition aiger.hh:398
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.
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:248
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.
bdd latch_bdd(unsigned i, bool neg=false) const
Get the bdd associated to the ith latch.
Definition aiger.hh:254
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:407
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:230
Simplify a reactive specification, preserving realizability.
Definition apcollect.hh:86
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:27
A struct that represents different types of mealy like objects.
Definition synthesis.hh:197

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.8