cprover
smt_identifier_termt Class Reference

Stores identifiers in unescaped and unquoted form. More...

#include <smt_terms.h>

+ Inheritance diagram for smt_identifier_termt:
+ Collaboration diagram for smt_identifier_termt:

Public Member Functions

 smt_identifier_termt (irep_idt identifier, smt_sortt sort)
 Constructs an identifier term with the given identifier and sort. More...
 
irep_idt identifier () const
 
- Public Member Functions inherited from smt_termt
 smt_termt ()=delete
 
bool operator== (const smt_termt &) const
 
bool operator!= (const smt_termt &) const
 
const smt_sorttget_sort () const
 
void accept (smt_term_const_downcast_visitort &) const
 
void accept (smt_term_const_downcast_visitort &&) const
 
std::string pretty (unsigned indent=0, unsigned max_indent=0) const
 

Additional Inherited Members

- Protected Types inherited from irept
using baset = tree_implementationt
 
- Protected Types inherited from sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >
using dt = tree_nodet< irept, forward_list_as_mapt< irep_namet, irept >, true >
 
using subt = typename dt::subt
 
using named_subt = typename dt::named_subt
 
using tree_implementationt = sharing_treet
 Used to refer to this class from derived classes. More...
 
- Protected Member Functions inherited from smt_termt
 smt_termt (irep_idt id, smt_sortt sort)
 
- Protected Member Functions inherited from irept
bool is_nil () const
 
bool is_not_nil () const
 
 irept (const irep_idt &_id)
 
 irept (const irep_idt &_id, const named_subt &_named_sub, const subt &_sub)
 
 irept ()=default
 
const irep_idtid () const
 
const std::string & id_string () const
 
void id (const irep_idt &_data)
 
const ireptfind (const irep_namet &name) const
 
ireptadd (const irep_namet &name)
 
ireptadd (const irep_namet &name, irept irep)
 
const std::string & get_string (const irep_namet &name) const
 
const irep_idtget (const irep_namet &name) const
 
bool get_bool (const irep_namet &name) const
 
signed int get_int (const irep_namet &name) const
 
std::size_t get_size_t (const irep_namet &name) const
 
long long get_long_long (const irep_namet &name) const
 
void set (const irep_namet &name, const irep_idt &value)
 
void set (const irep_namet &name, irept irep)
 
void set (const irep_namet &name, const long long value)
 
void set_size_t (const irep_namet &name, const std::size_t value)
 
void remove (const irep_namet &name)
 
void move_to_sub (irept &irep)
 
void move_to_named_sub (const irep_namet &name, irept &irep)
 
bool operator== (const irept &other) const
 
bool operator!= (const irept &other) const
 
void swap (irept &irep)
 
bool operator< (const irept &other) const
 defines ordering on the internal representation More...
 
bool ordering (const irept &other) const
 defines ordering on the internal representation More...
 
int compare (const irept &i) const
 defines ordering on the internal representation comments are ignored More...
 
void clear ()
 
void make_nil ()
 
subtget_sub ()
 
const subtget_sub () const
 
named_subtget_named_sub ()
 
const named_subtget_named_sub () const
 
std::size_t hash () const
 
std::size_t full_hash () const
 
bool full_eq (const irept &other) const
 
std::string pretty (unsigned indent=0, unsigned max_indent=0) const
 
- Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >
void detach ()
 
 sharing_treet (irep_idt _id)
 
 sharing_treet (irep_idt _id, named_subt _named_sub, subt _sub)
 
 sharing_treet ()
 
 sharing_treet (const sharing_treet &irep)
 
 sharing_treet (sharing_treet &&irep)
 
sharing_treetoperator= (const sharing_treet &irep)
 
sharing_treetoperator= (sharing_treet &&irep)
 
 ~sharing_treet ()
 
const dtread () const
 
dtwrite ()
 
- Static Protected Member Functions inherited from irept
static bool is_comment (const irep_namet &name)
 
static std::size_t number_of_non_comments (const named_subt &)
 count the number of named_sub elements that are not comments More...
 
- Static Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >
static void remove_ref (dt *old_data)
 
static void nonrecursive_destructor (dt *old_data)
 Does the same as remove_ref, but using an explicit stack instead of recursion. More...
 
- Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >
dtdata
 
- Static Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_namet, irept > >
static dt empty_d
 

Detailed Description

Stores identifiers in unescaped and unquoted form.

Any escaping or quoting required should be performed during printing.

Definition at line 80 of file smt_terms.h.

Constructor & Destructor Documentation

◆ smt_identifier_termt()

smt_identifier_termt::smt_identifier_termt ( irep_idt  identifier,
smt_sortt  sort 
)

Constructs an identifier term with the given identifier and sort.

Parameters
identifierThis should be the unescaped form of the identifier. Escaping of the identifier if required is to be performed as part of the printing operation. The given identifier is checked to ensure that it has not already been escaped, in order to avoid escaping it twice. Performing escaping during the printing will ensure that the identifiers output conform to the specification of the concrete form.
sortThe sort which this term will have. All terms in our abstract form must be sorted, even if those sorts are not printed in all contexts.

Definition at line 57 of file smt_terms.cpp.

Member Function Documentation

◆ identifier()

irep_idt smt_identifier_termt::identifier ( ) const

Definition at line 66 of file smt_terms.cpp.


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