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
29#include <unordered_map>
30#include <vector>
31#include <set>
32#include <memory>
33#include <algorithm> // std::none_of
34#include <sstream>
35
36
37namespace 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 }
177 const std::vector<std::string>& output_names() const
178 {
179 return output_names_;
180 }
181
183 unsigned num_inputs() const
184 {
185 return num_inputs_;
186 }
188 const std::vector<std::string>& input_names() const
189 {
190 return input_names_;
191 }
192
194 unsigned num_latches() const
195 {
196 return num_latches_;
197 }
201 const std::vector<unsigned>& next_latches() const
202 {
203 SPOT_ASSERT(std::none_of(next_latches_.begin(), next_latches_.end(),
204 [](unsigned o){return o == -1u; }));
205 return next_latches_;
206 };
207
209 unsigned num_gates() const
210 {
211 return and_gates_.size();
212 };
214 const std::vector<std::pair<unsigned, unsigned>>& gates() const
215 {
216 return and_gates_;
217 };
218
220 unsigned max_var() const
221 {
222 return max_var_;
223 };
224
226 unsigned input_var(unsigned i, bool neg = false) const
227 {
228 SPOT_ASSERT(i < num_inputs_);
229 return (1 + i) * 2 + neg;
230 }
232 bdd input_bdd(unsigned i, bool neg = false) const
233 {
234 return aigvar2bdd(input_var(i, neg));
235 }
236
238 unsigned latch_var(unsigned i, bool neg = false) const
239 {
240 SPOT_ASSERT(i < num_latches_);
241 return (1 + num_inputs_ + i) * 2 + neg;
242 }
244 bdd latch_bdd(unsigned i, bool neg = false) const
245 {
246 return aigvar2bdd(latch_var(i, neg));
247 }
248
250 unsigned gate_var(unsigned i, bool neg = false) const
251 {
252 SPOT_ASSERT(i < num_gates());
253 return (1 + num_inputs_ + num_latches_ + i) * 2 + neg;
254 }
256 bdd gate_bdd(unsigned i, bool neg = false) const
257 {
258 return aigvar2bdd(gate_var(i, neg));
259 }
260
263 bdd aigvar2bdd(unsigned v, bool neg = false) const
264 {
265 return neg ? bdd_not(var2bdd_.at(v)) : var2bdd_.at(v);
266 }
267
270 unsigned bdd2aigvar(const bdd& b) const
271 {
272 return bdd2var_.at(b.id());
273 }
274
276 unsigned bdd2INFvar(const bdd& b);
277
279 unsigned bdd2ISOPvar(const bdd& b, const int use_split_off = 0);
280
298 unsigned encode_bdd(const std::vector<bdd>& c_alt,
299 char method = 1, bool use_dual = false,
300 int use_split_off = 0);
301
303 unsigned encode_bdd(const bdd& b,
304 char method = 1, bool use_dual = false,
305 int use_split_off = 0);
306
308 void set_output(unsigned i, unsigned v);
309
311 void set_next_latch(unsigned i, unsigned v);
312
313 static constexpr unsigned aig_true() noexcept
314 {
315 return 1;
316 };
317
318 static constexpr unsigned aig_false() noexcept
319 {
320 return 0;
321 };
322
324 unsigned aig_not(unsigned v);
325
327 unsigned aig_and(unsigned v1, unsigned v2);
328
332 unsigned aig_and(std::vector<unsigned>& vs);
333
335 unsigned aig_or(unsigned v1, unsigned v2);
336
340 unsigned aig_or(std::vector<unsigned>& vs);
341
343 unsigned aig_pos(unsigned v);
344
351 void encode_all_bdds(const std::vector<bdd>& all_bdd);
352
360 static aig_ptr
361 parse_aag(const std::string& aig_file,
362 bdd_dict_ptr dict = make_bdd_dict());
363
364 static aig_ptr
365 parse_aag(const char* data,
366 const std::string& filename,
367 bdd_dict_ptr dict = make_bdd_dict());
368
369 static aig_ptr
370 parse_aag(std::istream& iss,
371 const std::string& filename,
372 bdd_dict_ptr dict = make_bdd_dict());
373
378 twa_graph_ptr as_automaton(bool keepsplit = false) const;
379
388 const std::vector<bool>& circ_state() const
389 {
390 SPOT_ASSERT(state_.size() == max_var_ + 2
391 && "State vector does not have the correct size.\n"
392 "Forgot to initialize?");
393 return state_;
394 }
395
397 bool circ_state_of(unsigned var) const
398 {
399 SPOT_ASSERT(var <= max_var_ + 1
400 && "Variable out of range");
401 return circ_state()[var];
402 }
403
406 void circ_init();
407
414 void circ_step(const std::vector<bool>& inputs);
415
416 };
417
440 SPOT_API aig_ptr
441 mealy_machine_to_aig(const const_twa_graph_ptr& m, const char* mode);
442 SPOT_API aig_ptr
443 mealy_machine_to_aig(const twa_graph_ptr& m, const char *mode,
444 const std::vector<std::string>& ins,
445 const std::vector<std::string>& outs);
446
447 SPOT_API aig_ptr
448 mealy_machine_to_aig(const mealy_like& m, const char* mode);
449 SPOT_API aig_ptr
450 mealy_machine_to_aig(mealy_like& m, const char *mode,
451 const std::vector<std::string>& ins,
452 const std::vector<std::string>& outs);
454
469 SPOT_API aig_ptr
470 mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
471 const char* mode);
472 SPOT_API aig_ptr
473 mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
474 const char* mode);
475 SPOT_API aig_ptr
476 mealy_machines_to_aig(const std::vector<const_twa_graph_ptr>& m_vec,
477 const char* mode,
478 const std::vector<std::string>& ins,
479 const std::vector<std::vector<std::string>>& outs);
480 SPOT_API aig_ptr
481 mealy_machines_to_aig(const std::vector<mealy_like>& m_vec,
482 const char* mode,
483 const std::vector<std::string>& ins,
484 const std::vector<std::vector<std::string>>& outs);
486
489 SPOT_API std::ostream&
490 print_aiger(std::ostream& os, const_aig_ptr circuit);
491
527 SPOT_API std::ostream&
528 print_aiger(std::ostream& os, const const_twa_graph_ptr& aut,
529 const char* mode);
530}
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:256
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:263
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:214
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:94
const std::vector< unsigned > & outputs() const
Get the variables associated to the outputs.
Definition aiger.hh:170
unsigned gate_var(unsigned i, bool neg=false) const
Get the variable associated to the ith gate.
Definition aiger.hh:250
const std::vector< unsigned > & next_latches() const
Get the variables associated to the state of the latches in the next iteration.
Definition aiger.hh:201
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:209
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:177
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:270
unsigned num_inputs() const
Get the number of inputs.
Definition aiger.hh:183
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:232
unsigned input_var(unsigned i, bool neg=false) const
Get the variable associated to the ith input.
Definition aiger.hh:226
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:188
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:194
const std::vector< bool > & circ_state() const
Gives access to the current state of the circuit.
Definition aiger.hh:388
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:238
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:244
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:397
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:220
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