#include <util/irep.h>#include <solvers/smt2_incremental/response_or_error.h>#include <solvers/smt2_incremental/smt_index.h>#include <solvers/smt2_incremental/smt_sorts.h>#include <solvers/smt2_incremental/type_traits.h>#include <functional>#include <utility>#include "smt_terms.def"
Include dependency graph for smt_terms.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | smt_termt |
| class | smt_termt::storert< derivedt > |
| Class for adding the ability to up and down cast smt_termt to and from irept. More... | |
| class | smt_bool_literal_termt |
| class | smt_identifier_termt |
| Stores identifiers in unescaped and unquoted form. More... | |
| class | smt_bit_vector_constant_termt |
| class | smt_function_application_termt |
| struct | smt_function_application_termt::has_indicest< functiont, class > |
| struct | smt_function_application_termt::has_indicest< functiont, void_t< decltype(std::declval< functiont >().indices())> > |
| class | smt_function_application_termt::factoryt< functiont > |
| class | smt_forall_termt |
| class | smt_exists_termt |
| class | smt_term_const_downcast_visitort |
Macros | |
| #define | TERM_ID(the_id) virtual void visit(const smt_##the_id##_termt &) = 0; |
Typedefs | |
| using | mp_integer = BigInt |
Macro Definition Documentation
◆ TERM_ID
| #define TERM_ID | ( | the_id | ) | virtual void visit(const smt_##the_id##_termt &) = 0; |
Definition at line 250 of file smt_terms.h.
Typedef Documentation
◆ mp_integer
| using mp_integer = BigInt |
Definition at line 17 of file smt_terms.h.
