Inheritance diagram for btor_smt_ast:

Public Member Functions
	~btor_smt_ast () override=default
void	dump () const override
Public Member Functions inherited from solver_smt_ast< BoolectorNode * >
	solver_smt_ast (smt_solver_baset ctx, BoolectorNode _a, smt_sortt s)
Public Member Functions inherited from smt_ast
	smt_ast (smt_solver_baset *ctx, smt_sortt s)
virtual	~smt_ast ()=default
virtual smt_astt	with_sort (smt_solver_baset *ctx, smt_sortt s) const
	The same solver term under a different sort.
virtual smt_astt	ite (smt_solver_baset *ctx, smt_astt cond, smt_astt falseop) const
virtual smt_astt	eq (smt_solver_baset *ctx, smt_astt other) const
	Abstractly produce an equality.
virtual void	assign (smt_solver_baset *ctx, smt_astt sym) const
	Abstractly produce an assign.
virtual smt_astt	update (smt_solver_baset *ctx, smt_astt value, unsigned int idx, const expr2tc &idx_expr=expr2tc()) const
	Abstractly produce an "update", i.e., an array 'with' or tuple 'with'.
virtual smt_astt	select (smt_solver_baset *ctx, const expr2tc &idx) const
	Select a value from an array, for both normal arrays and tuple arrays.
virtual smt_astt	project (smt_solver_baset *ctx, unsigned int elem) const
	Project a member from a structure, or an field-array from a struct array.

Additional Inherited Members
Public Types inherited from solver_smt_ast< BoolectorNode * >
typedef BoolectorNode *	solver_ast_type
Public Attributes inherited from solver_smt_ast< BoolectorNode * >
solver_ast_type	a
Public Attributes inherited from smt_ast
smt_sortt	sort
	The sort of this function application.
const smt_solver_baset *	context
	The solver context.

Constructor & Destructor Documentation

◆ ~btor_smt_ast()

btor_smt_ast::~btor_smt_ast ( )

overridedefault

void btor_smt_ast::dump ( ) const

overridevirtual

Reimplemented from smt_ast.

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