Factory for enumerator that can be used to represent a tree grammar. More...

#include <expr_enumerator.h>

Collaboration diagram for enumerator_factoryt:

Public Member Functions
	enumerator_factoryt (const namespacet &ns)

void	add_placeholder (const recursive_enumerator_placeholdert &placeholder)
	Add a new placeholder/nonterminal to the grammar.

void	attach_productions (const std::string &id, const enumeratorst &enumerators)
	Attach `enumerators` to the placeholder with `id`.

Public Attributes
std::map< std::string, const enumeratorst >	productions_map
	Map from names of nonterminals to rhs of productions with lhs being them.

Protected Attributes
const namespacet &	ns

std::set< std::string >	nonterminal_set
	Set of nonterminals in the grammar.

Detailed Description

Factory for enumerator that can be used to represent a tree grammar.

Definition at line 302 of file expr_enumerator.h.

Constructor & Destructor Documentation

◆ enumerator_factoryt()

enumerator_factoryt::enumerator_factoryt ( const namespacet & ns )

inlineexplicit

Definition at line 305 of file expr_enumerator.h.

Member Function Documentation

◆ add_placeholder()

void enumerator_factoryt::add_placeholder ( const recursive_enumerator_placeholdert & placeholder )

Add a new placeholder/nonterminal to the grammar.

Definition at line 427 of file expr_enumerator.cpp.

◆ attach_productions()

void enumerator_factoryt::attach_productions	(	const std::string &	id,
		const enumeratorst &	enumerators
	)

Attach enumerators to the placeholder with id.

Definition at line 435 of file expr_enumerator.cpp.

Member Data Documentation

◆ nonterminal_set

std::set<std::string> enumerator_factoryt::nonterminal_set

protected

Set of nonterminals in the grammar.

Definition at line 326 of file expr_enumerator.h.

◆ ns

const namespacet& enumerator_factoryt::ns

protected

Definition at line 323 of file expr_enumerator.h.

◆ productions_map

std::map<std::string, const enumeratorst> enumerator_factoryt::productions_map

Map from names of nonterminals to rhs of productions with lhs being them.

Example: consider a nonterminal S -> 1 | 1 + S. This map will map the id "S" to a list of enumerators [E_1, E_2] where E_1 enumerates 1 and E_2 enumerates 1 + S.

Definition at line 320 of file expr_enumerator.h.

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

/home/runner/work/cbmc/cbmc/src/goto-synthesizer/expr_enumerator.h
/home/runner/work/cbmc/cbmc/src/goto-synthesizer/expr_enumerator.cpp

Public Member Functions

Public Attributes

Protected Attributes