cprover
|
#include <smt_terms.h>
Classes | |
class | factoryt |
struct | has_indicest |
struct | has_indicest< functiont, std::void_t< decltype(std::declval< functiont >().indices())> > |
Public Member Functions | |
const smt_identifier_termt & | function_identifier () const |
std::vector< std::reference_wrapper< const smt_termt > > | arguments () 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_sortt & | get_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 |
Private Member Functions | |
smt_function_application_termt (smt_identifier_termt function_identifier, std::vector< smt_termt > arguments) | |
Unchecked construction of function application terms. |
Static Private Member Functions | |
template<class functiont> | |
static std::vector< smt_indext > | indices (const functiont &function) |
Returns function.indices() if functiont has an indices member function or returns an empty collection otherwise. |
Additional Inherited Members | |
Protected Types inherited from irept | |
using | baset = tree_implementationt |
Protected Types inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > | |
using | dt |
using | subt |
using | named_subt |
using | tree_implementationt |
Used to refer to this class from derived classes. | |
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_idt & | id () const |
const std::string & | id_string () const |
void | id (const irep_idt &_data) |
const irept & | find (const irep_idt &name) const |
irept & | add (const irep_idt &name) |
irept & | add (const irep_idt &name, irept irep) |
const std::string & | get_string (const irep_idt &name) const |
const irep_idt & | get (const irep_idt &name) const |
bool | get_bool (const irep_idt &name) const |
signed int | get_int (const irep_idt &name) const |
std::size_t | get_size_t (const irep_idt &name) const |
long long | get_long_long (const irep_idt &name) const |
void | set (const irep_idt &name, const irep_idt &value) |
void | set (const irep_idt &name, irept irep) |
void | set (const irep_idt &name, const long long value) |
void | set_size_t (const irep_idt &name, const std::size_t value) |
void | remove (const irep_idt &name) |
void | move_to_sub (irept &irep) |
void | move_to_named_sub (const irep_idt &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 | |
bool | ordering (const irept &other) const |
defines ordering on the internal representation | |
int | compare (const irept &i) const |
defines ordering on the internal representation comments are ignored | |
void | clear () |
void | make_nil () |
subt & | get_sub () |
const subt & | get_sub () const |
named_subt & | get_named_sub () |
const named_subt & | get_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_idt, irept > > | |
void | detach () |
sharing_treet (irep_idt _id) | |
sharing_treet & | operator= (const sharing_treet &irep) |
~sharing_treet () | |
const dt & | read () const |
dt & | write () |
Static Protected Member Functions inherited from irept | |
static bool | is_comment (const irep_idt &name) |
static std::size_t | number_of_non_comments (const named_subt &) |
count the number of named_sub elements that are not comments | |
Static Protected Member Functions inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, 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. | |
Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > | |
dt * | data |
Static Protected Attributes inherited from sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > > | |
static dt | empty_d |
Definition at line 132 of file smt_terms.h.
|
private |
Unchecked construction of function application terms.
The public factoryt sub class should be used to construct instances of this term with the appropriate checks for the function being applied.
Definition at line 128 of file smt_terms.cpp.
std::vector< std::reference_wrapper< const smt_termt > > smt_function_application_termt::arguments | ( | ) | const |
Definition at line 148 of file smt_terms.cpp.
const smt_identifier_termt & smt_function_application_termt::function_identifier | ( | ) | const |
Definition at line 142 of file smt_terms.cpp.
|
inlinestaticprivate |
Returns function.indices() if functiont has an indices member function or returns an empty collection otherwise.
Definition at line 159 of file smt_terms.h.