smt_terms.h File Reference

#include <util/irep.h>
#include <solvers/smt2_incremental/response_or_error.h>
#include "smt_index.h"
#include "smt_sorts.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, std::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 237 of file smt_terms.h.

Typedef Documentation

mp_integer

using mp_integer = BigInt

Definition at line 17 of file smt_terms.h.