23#include <spot/misc/common.hh>
24#include <spot/misc/bddlt.hh>
25#include <spot/twa/fwd.hh>
26#include <spot/twa/bdddict.hh>
28#include <spot/tl/relabel.hh>
30#include <unordered_map>
45 typedef std::shared_ptr<aig> aig_ptr;
46 typedef std::shared_ptr<const aig> const_aig_ptr;
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_;
70 std::vector<unsigned> next_latches_;
71 std::vector<unsigned> outputs_;
72 std::vector<std::pair<unsigned, unsigned>> and_gates_;
76 std::unordered_map<unsigned, bdd> var2bdd_;
77 std::unordered_map<int, unsigned> bdd2var_;
86 std::vector<bool> state_;
97 std::tuple<std::vector<std::pair<unsigned, unsigned>>,
98 std::vector<std::pair<unsigned, bdd>>,
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());
111 aig(
unsigned num_inputs,
unsigned num_outputs,
112 unsigned num_latches, bdd_dict_ptr dict = make_bdd_dict());
116 dict_->unregister_all_my_variables(
this);
122 void register_latch_(
unsigned i,
const bdd& b);
123 void register_input_(
unsigned i,
const bdd& b);
130 std::vector<bdd>& cond_parts);
136 unsigned cube2var_(
const bdd& b,
const int use_split_off);
157 bool do_stash =
false);
173 SPOT_ASSERT(std::none_of(outputs_.begin(), outputs_.end(),
174 [](
unsigned o){return o == -1u; }));
180 return output_names_;
204 SPOT_ASSERT(std::none_of(next_latches_.begin(), next_latches_.end(),
205 [](
unsigned o){return o == -1u; }));
206 return next_latches_;
212 return and_gates_.size();
215 const std::vector<std::pair<unsigned, unsigned>>&
gates()
const
229 SPOT_ASSERT(i < num_inputs_);
230 return (1 + i) * 2 + neg;
235 return aigvar2bdd(input_var(i, neg));
241 SPOT_ASSERT(i < num_latches_);
242 return (1 + num_inputs_ + i) * 2 + neg;
247 return aigvar2bdd(latch_var(i, neg));
251 unsigned gate_var(
unsigned i,
bool neg =
false)
const
253 SPOT_ASSERT(i < num_gates());
254 return (1 + num_inputs_ + num_latches_ + i) * 2 + neg;
259 return aigvar2bdd(gate_var(i, neg));
266 return neg ? bdd_not(var2bdd_.at(v)) : var2bdd_.at(v);
273 return bdd2var_.at(b.id());
300 char method = 1,
bool use_dual =
false,
301 int use_split_off = 0);
305 char method = 1,
bool use_dual =
false,
306 int use_split_off = 0);
314 static constexpr unsigned aig_true() noexcept
319 static constexpr unsigned aig_false() noexcept
336 unsigned aig_or(
unsigned v1,
unsigned v2);
341 unsigned aig_or(std::vector<unsigned>& vs);
363 bdd_dict_ptr dict = make_bdd_dict());
366 parse_aag(
const char* data,
367 const std::string& filename,
368 bdd_dict_ptr dict = make_bdd_dict());
371 parse_aag(std::istream& iss,
372 const std::string& filename,
373 bdd_dict_ptr dict = make_bdd_dict());
391 SPOT_ASSERT(state_.size() == max_var_ + 2
392 &&
"State vector does not have the correct size.\n"
393 "Forgot to initialize?");
400 SPOT_ASSERT(var <= max_var_ + 1
401 &&
"Variable out of range");
402 return circ_state()[var];
448 const std::vector<std::string>& ins,
449 const std::vector<std::string>& outs,
450 const relabeling_map* rm =
nullptr);
456 const std::vector<std::string>& ins,
457 const std::vector<std::string>& outs,
458 const relabeling_map* rm =
nullptr);
487 const std::vector<std::string>& ins,
488 const std::vector<std::vector<std::string>>& outs,
489 const relabeling_map* rm =
nullptr);
493 const std::vector<std::string>& ins,
494 const std::vector<std::vector<std::string>>& outs,
495 const relabeling_map* rm =
nullptr);
500 SPOT_API std::ostream&
538 SPOT_API std::ostream&
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:257
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:264
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:215
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:251
const std::vector< unsigned > & next_latches() const
Get the variables associated to the state of the latches in the next iteration.
Definition aiger.hh:202
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:210
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:178
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:271
unsigned num_inputs() const
Get the number of inputs.
Definition aiger.hh:184
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:233
unsigned input_var(unsigned i, bool neg=false) const
Get the variable associated to the ith input.
Definition aiger.hh:227
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:189
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:195
const std::vector< bool > & circ_state() const
Gives access to the current state of the circuit.
Definition aiger.hh:389
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:239
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:245
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:398
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:221
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