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. More... | |
| void | attach_productions (const std::string &id, const enumeratorst &enumerators) |
Attach enumerators to the placeholder with id. More... | |
Public Attributes | |
| std::map< std::string, const enumeratorst > | productions_map |
| Map from names of nonterminals to rhs of productions with lhs being them. More... | |
Protected Attributes | |
| const namespacet & | ns |
| std::set< std::string > | nonterminal_set |
| Set of nonterminals in the grammar. More... | |
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()
|
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
|
protected |
Set of nonterminals in the grammar.
Definition at line 326 of file expr_enumerator.h.
◆ 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
