A class representing AIG circuits. More...

#include <spot/twaalgos/aiger.hh>

Collaboration diagram for spot::aig:

Public Types
using	safe_point = std::pair< unsigned, unsigned >
	Mark the beginning of a test tranlation. More...

using	safe_stash = std::tuple< std::vector< std::pair< unsigned, unsigned > >, std::vector< std::pair< unsigned, bdd > >, std::vector< bdd > >

Public Member Functions
	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. A bdd_dict can be handed to the circuit in order to allow for verification against other automata after construction. More...

	aig (unsigned num_inputs, unsigned num_outputs, unsigned num_latches, bdd_dict_ptr dict=make_bdd_dict())
	Constructing the circuit with generic names. More...

safe_point	get_safe_point_ () const
	Safe the current state of the circuit. More...

safe_stash	roll_back_ (safe_point sp, bool do_stash=false)
	roll_back to the saved point. More...

void	reapply_ (safe_point sp, const safe_stash &ss)
	Reapply to stored changes on top of a safe_point. More...

unsigned	num_outputs () const
	Get the number of outputs. More...

const std::vector< unsigned > &	outputs () const
	Get the variables associated to the outputs. More...

const std::vector< std::string > &	output_names () const
	Get the set of output names. More...

unsigned	num_inputs () const
	Get the number of inputs. More...

const std::vector< std::string > &	input_names () const
	Get the set of input names. More...

unsigned	num_latches () const
	Get the number of latches in the circuit. More...

const std::vector< unsigned > &	next_latches () const
	Get the variables associated to the state of the latches in the next iteration. More...

unsigned	num_gates () const
	Get the total number of and gates. More...

const std::vector< std::pair< unsigned, unsigned > > &	gates () const
	Access the underlying container. More...

unsigned	max_var () const
	Maximal variable index currently appearing in the circuit. More...

unsigned	input_var (unsigned i, bool neg=false) const
	Get the variable associated to the ith input. More...

bdd	input_bdd (unsigned i, bool neg=false) const
	Get the bdd associated to the ith input. More...

unsigned	latch_var (unsigned i, bool neg=false) const
	Get the variable associated to the ith latch. More...

bdd	latch_bdd (unsigned i, bool neg=false) const
	Get the bdd associated to the ith latch. More...

unsigned	gate_var (unsigned i, bool neg=false) const
	Get the variable associated to the ith gate. More...

bdd	gate_bdd (unsigned i, bool neg=false) const
	Get the bdd associated to the ith gate. More...

bdd	aigvar2bdd (unsigned v, bool neg=false) const
	Get the bdd associated to a variable. More...

unsigned	bdd2aigvar (const bdd &b) const
	Get the variable associated to a bdd. More...

unsigned	bdd2INFvar (const bdd &b)
	Add a bdd to the circuit using if-then-else normal form. More...

unsigned	bdd2ISOPvar (const bdd &b, const int use_split_off=0)
	Add a bdd to the circuit using isop normal form. More...

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, that is, any of these conditions can be encoded and the corresponding literal returned. Multiple translation options are available whose main goal is to minimize the necessary number of gates. More...

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

void	set_output (unsigned i, unsigned v)
	Associate the ith output to the variable v. More...

void	set_next_latch (unsigned i, unsigned v)
	Associate the ith latch state after update to the variable v. More...

unsigned	aig_not (unsigned v)
	Negate a variable. More...

unsigned	aig_and (unsigned v1, unsigned v2)
	Compute AND of v1 and v2. More...

unsigned	aig_and (std::vector< unsigned > &vs)
	Computes the AND of all vars. More...

unsigned	aig_or (unsigned v1, unsigned v2)
	Computes the OR of v1 and v2. More...

unsigned	aig_or (std::vector< unsigned > &vs)
	Computes the or of all vars. More...

unsigned	aig_pos (unsigned v)
	Returns the positive form of the given variable. More...

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 the circuit. In this case additional optimization steps are taken to minimize the size of the circuit. More...

twa_graph_ptr	as_automaton (bool keepsplit=false) const
	Transform the circuit onto an equivalent monitor. More...

const std::vector< bool > &	circ_state () const
	Gives access to the current state of the circuit. More...

bool	circ_state_of (unsigned var) const
	Access to the state of a specific variable. More...

void	circ_init ()
	(Re)initialize the stepwise evaluation of the circuit. This sets all latches to 0 and clears the output More...

void	circ_step (const std::vector< bool > &inputs)
	Performs the next discrete step of the circuit, based on the inputs. More...

Static Public Member Functions
static constexpr unsigned	aig_true () noexcept

static constexpr unsigned	aig_false () noexcept

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

static aig_ptr	parse_aag (const char *data, const std::string &filename, bdd_dict_ptr dict=make_bdd_dict())

static aig_ptr	parse_aag (std::istream &iss, const std::string &filename, bdd_dict_ptr dict=make_bdd_dict())

Protected Member Functions
void	register_new_lit_ (unsigned v, const bdd &b)
	Register a new literal in both maps. More...

void	register_latch_ (unsigned i, const bdd &b)

void	register_input_ (unsigned i, const bdd &b)

void	unregister_lit_ (unsigned v)
	Remove a literal from both maps. More...

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

bdd	accum_common_ (const bdd &b) const
	Split-off common sub-expressions as cube. More...

unsigned	cube2var_ (const bdd &b, const int use_split_off)
	Translate a cube into gates, using split-off optionally. More...

Protected Attributes
const unsigned	num_inputs_

const unsigned	num_outputs_

const unsigned	num_latches_

const std::vector< std::string >	input_names_

const std::vector< std::string >	output_names_

unsigned	max_var_

std::vector< unsigned >	next_latches_

std::vector< unsigned >	outputs_

std::vector< std::pair< unsigned, unsigned > >	and_gates_

bdd_dict_ptr	dict_

std::unordered_map< unsigned, bdd >	var2bdd_

std::unordered_map< int, unsigned >	bdd2var_

int	l0_

bdd	all_ins_

bdd	all_latches_

std::vector< bool >	state_

Detailed Description

A class representing AIG circuits.

AIG circuits consist of (named) inputs, (named) outputs, latches which serve as memory, and gates and negations connecting them. AIG circuits can be used to represent controllers, which is currently their sole purpose within spot. AIGs produce a output sequence based on the following rules: 1) All latches are initialized to 0 2) The next input is read. 3) The output and the state of the latches for the next turn are given by the gates as a function of the current latches and inputs

Member Typedef Documentation

◆ safe_point

using spot::aig::safe_point = std::pair<unsigned, unsigned>

Mark the beginning of a test tranlation.

Sometimes different encodings produces more or less gates. To improve performances, one can "safe" the current status and revert changes afterwards if needed

Constructor & Destructor Documentation

◆ aig() [1/2]

spot::aig::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. A bdd_dict can be handed to the circuit in order to allow for verification against other automata after construction.

◆ aig() [2/2]

spot::aig::aig	(	unsigned	num_inputs,
		unsigned	num_outputs,
		unsigned	num_latches,
		bdd_dict_ptr	dict = `make_bdd_dict()`
	)

Constructing the circuit with generic names.

Member Function Documentation

◆ accum_common_()

bdd spot::aig::accum_common_ ( const bdd & b ) const

protected

Split-off common sub-expressions as cube.

◆ aig_and() [1/2]

unsigned spot::aig::aig_and ( std::vector< unsigned > & vs )

Computes the AND of all vars.

Note: This function modifies the given vector to only contain the result (at position zero) after the call

◆ aig_and() [2/2]

unsigned spot::aig::aig_and	(	unsigned	v1,
		unsigned	v2
	)

Compute AND of v1 and v2.

◆ aig_not()

unsigned spot::aig::aig_not ( unsigned v )

Negate a variable.

◆ aig_or() [1/2]

unsigned spot::aig::aig_or ( std::vector< unsigned > & vs )

Computes the or of all vars.

Note: This function modifies the given vector to only contain the result after call

◆ aig_or() [2/2]

unsigned spot::aig::aig_or	(	unsigned	v1,
		unsigned	v2
	)

Computes the OR of v1 and v2.

◆ aig_pos()

unsigned spot::aig::aig_pos ( unsigned v )

Returns the positive form of the given variable.

◆ aigvar2bdd()

bdd spot::aig::aigvar2bdd	(	unsigned	v,
		bool	neg = `false`
	)		const

inline

Get the bdd associated to a variable.

Note: Throws if non-existent

◆ as_automaton()

twa_graph_ptr spot::aig::as_automaton ( bool keepsplit = false ) const

Transform the circuit onto an equivalent monitor.

Parameters

keepsplit If as_automaton(true) is the same as split_2step(as_automaton(false), outputs)

Note: The complexity is exponential in the number of inputs!

◆ bdd2aigvar()

unsigned spot::aig::bdd2aigvar ( const bdd & b ) const

inline

Get the variable associated to a bdd.

Note: Throws if non-existent

◆ bdd2INFvar()

unsigned spot::aig::bdd2INFvar ( const bdd & b )

Add a bdd to the circuit using if-then-else normal form.

◆ bdd2ISOPvar()

unsigned spot::aig::bdd2ISOPvar	(	const bdd &	b,
		const int	use_split_off = `0`
	)

Add a bdd to the circuit using isop normal form.

◆ circ_init()

void spot::aig::circ_init ( )

(Re)initialize the stepwise evaluation of the circuit. This sets all latches to 0 and clears the output

◆ circ_state()

const std::vector<bool>& spot::aig::circ_state ( ) const

inline

Gives access to the current state of the circuit.

   Corresponds to a vector of booleans holding the truth value
   for each literal. Note that within the vector we have the truth
   value of a literal and its negation, so sim_state()[2*i+1] is
   always the negation of sim_state()[2*i].
   The variable index can be obtained using
   input_var, latch_var or outputs

◆ circ_state_of()

bool spot::aig::circ_state_of ( unsigned var ) const

inline

Access to the state of a specific variable.

◆ circ_step()

void spot::aig::circ_step ( const std::vector< bool > & inputs )

Performs the next discrete step of the circuit, based on the inputs.

Updates the state of the aig such that circ_state holds the values of output and latches AFTER reading the given input

Parameters

inputs : Vector of booleans with size num_inputs()

◆ cube2var_()

unsigned spot::aig::cube2var_	(	const bdd &	b,
		const int	use_split_off
	)

protected

Translate a cube into gates, using split-off optionally.

◆ encode_all_bdds()

void spot::aig::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 the circuit. In this case additional optimization steps are taken to minimize the size of the circuit.

Note: This can be costly and did not bring about any advantages in the SYNTCOMP cases

◆ encode_bdd() [1/2]

unsigned spot::aig::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.

◆ encode_bdd() [2/2]

unsigned spot::aig::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, that is, any of these conditions can be encoded and the corresponding literal returned. Multiple translation options are available whose main goal is to minimize the necessary number of gates.

Parameters

method	How to translate the bdd. 0: If-then-else normal form, 1: isop normal form, 2: try both and retain smaller
use_dual	Encode the negations of the given bdds and retain the smalles implementation
use_split_off	0: Use base algo 1: Separate the different types of input signals (like latches, inputs) to increase gate re-usability and retain smallest circuit 2: Actively search for subexpressions the within expressions

◆ gate_bdd()

bdd spot::aig::gate_bdd	(	unsigned	i,
		bool	neg = `false`
	)		const

inline

Get the bdd associated to the ith gate.

◆ gate_var()

unsigned spot::aig::gate_var	(	unsigned	i,
		bool	neg = `false`
	)		const

inline

Get the variable associated to the ith gate.

◆ gates()

const std::vector<std::pair<unsigned, unsigned> >& spot::aig::gates ( ) const

inline

Access the underlying container.

◆ get_safe_point_()

safe_point spot::aig::get_safe_point_ ( ) const

Safe the current state of the circuit.

Note: This does not make a copy, so rolling back to an older safe point invalidates all newer safepoints. Also only concerns the gates, output and next_latch variables will not change This function is semi-public. Make sure you know what you are doing when using it.

◆ input_bdd()

bdd spot::aig::input_bdd	(	unsigned	i,
		bool	neg = `false`
	)		const

inline

Get the bdd associated to the ith input.

◆ input_names()

const std::vector<std::string>& spot::aig::input_names ( ) const

inline

Get the set of input names.

◆ input_var()

unsigned spot::aig::input_var	(	unsigned	i,
		bool	neg = `false`
	)		const

inline

Get the variable associated to the ith input.

◆ latch_bdd()

bdd spot::aig::latch_bdd	(	unsigned	i,
		bool	neg = `false`
	)		const

inline

Get the bdd associated to the ith latch.

◆ latch_var()

unsigned spot::aig::latch_var	(	unsigned	i,
		bool	neg = `false`
	)		const

inline

Get the variable associated to the ith latch.

◆ max_var()

unsigned spot::aig::max_var ( ) const

inline

Maximal variable index currently appearing in the circuit.

◆ next_latches()

const std::vector<unsigned>& spot::aig::next_latches ( ) const

inline

Get the variables associated to the state of the latches in the next iteration.

Note: Only available after call to aig::set_next_latch

◆ num_gates()

unsigned spot::aig::num_gates ( ) const

inline

Get the total number of and gates.

◆ num_inputs()

unsigned spot::aig::num_inputs ( ) const

inline

Get the number of inputs.

◆ num_latches()

unsigned spot::aig::num_latches ( ) const

inline

Get the number of latches in the circuit.

◆ num_outputs()

unsigned spot::aig::num_outputs ( ) const

inline

Get the number of outputs.

◆ output_names()

const std::vector<std::string>& spot::aig::output_names ( ) const

inline

Get the set of output names.

◆ outputs()

const std::vector<unsigned>& spot::aig::outputs ( ) const

inline

Get the variables associated to the outputs.

Note: Only available after a call to aig::set_output

◆ parse_aag()

static aig_ptr spot::aig::parse_aag	(	const std::string &	aig_file,
		bdd_dict_ptr	dict = `make_bdd_dict()`
	)

static

Create a circuit from an aag file with restricted syntax.

Note

Additional constraints are:

inputs, latches, and gates have to appear in increasing order.
Inputs are expected to have variable numbers from 2-2*n_i+1 with n_i being the number of inputs
Latches cannot be named

◆ reapply_()

void spot::aig::reapply_	(	safe_point	sp,
		const safe_stash &	ss
	)

Reapply to stored changes on top of a safe_point.

Note: ss has to be obtained from roll_back_(sp, true) This function is semi-public. Make sure you know what you are doing when using it.

◆ register_new_lit_()

void spot::aig::register_new_lit_	(	unsigned	v,
		const bdd &	b
	)

protected

Register a new literal in both maps.

◆ roll_back_()

safe_stash spot::aig::roll_back_	(	safe_point	sp,
		bool	do_stash = `false`
	)

roll_back to the saved point.

Parameters

sp	The safe_point to revert back to
do_stash	Whether or not to save the changes to be possibly reapplied later on

Note: This function is semi-public. Make sure you know what you are doing when using it.

◆ set_next_latch()

void spot::aig::set_next_latch	(	unsigned	i,
		unsigned	v
	)

Associate the ith latch state after update to the variable v.

◆ set_output()

void spot::aig::set_output	(	unsigned	i,
		unsigned	v
	)

Associate the ith output to the variable v.

◆ split_cond_()

void spot::aig::split_cond_	(	const bdd &	b,
		char	so_mode,
		std::vector< bdd > &	cond_parts
	)

protected

Internal function that split a bdd into a conjunction hoping to increase reusage of gates.

◆ unregister_lit_()

void spot::aig::unregister_lit_ ( unsigned v )

protected

Remove a literal from both maps.

The documentation for this class was generated from the following file:

spot/twaalgos/aiger.hh

Public Types

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ safe_point

Constructor & Destructor Documentation

◆ aig() [1/2]

◆ aig() [2/2]

Member Function Documentation

◆ accum_common_()

◆ aig_and() [1/2]

◆ aig_and() [2/2]

◆ aig_not()

◆ aig_or() [1/2]

◆ aig_or() [2/2]

◆ aig_pos()

◆ aigvar2bdd()

◆ as_automaton()

◆ bdd2aigvar()

◆ bdd2INFvar()

◆ bdd2ISOPvar()

◆ circ_init()

◆ circ_state()

◆ circ_state_of()

◆ circ_step()

◆ cube2var_()

◆ encode_all_bdds()

◆ encode_bdd() [1/2]

◆ encode_bdd() [2/2]

◆ gate_bdd()

◆ gate_var()

◆ gates()

◆ get_safe_point_()

◆ input_bdd()

◆ input_names()

◆ input_var()

◆ latch_bdd()

◆ latch_var()

◆ max_var()

◆ next_latches()

◆ num_gates()

◆ num_inputs()

◆ num_latches()

◆ num_outputs()

◆ output_names()

◆ outputs()

◆ parse_aag()

◆ reapply_()

◆ register_new_lit_()

◆ roll_back_()

◆ set_next_latch()

◆ set_output()

◆ split_cond_()

◆ unregister_lit_()