#include <smt_ast.h>

Inheritance diagram for solver_smt_ast< solver_ast >:

Public Types
typedef solver_ast	solver_ast_type

Public Member Functions
	solver_smt_ast (smt_solver_baset *ctx, solver_ast _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.
virtual void	dump () const

Public Attributes
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.

Member Typedef Documentation

◆ solver_ast_type

template<typename solver_ast>

typedef solver_ast solver_smt_ast< solver_ast >::solver_ast_type

template<typename solver_ast>

solver_smt_ast< solver_ast >::solver_smt_ast	(	smt_solver_baset *	ctx,
		solver_ast	_a,
		smt_sortt	s )

inline

template<typename solver_ast>

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