#include <smtlib_conv.h>

Inheritance diagram for smtlib_smt_ast:

Public Member Functions
	smtlib_smt_ast (smt_solver_baset ctx, const smt_sort s, smt_func_kind k)
	~smtlib_smt_ast () override=default
void	dump () const override
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.

Public Attributes
smt_func_kind	kind
std::string	symname
BigInt	intval
std::string	realval
bool	boolval
int	extract_high
int	extract_low
std::vector< smt_astt >	args
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

◆ smtlib_smt_ast()

smtlib_smt_ast::smtlib_smt_ast	(	smt_solver_baset *	ctx,
		const smt_sort *	s,
		smt_func_kind	k )

inline

◆ ~smtlib_smt_ast()

smtlib_smt_ast::~smtlib_smt_ast ( )

overridedefault

Member Function Documentation

◆ dump()

void smtlib_smt_ast::dump ( ) const

overridevirtual

Reimplemented from smt_ast.

Member Data Documentation

◆ args

std::vector<smt_astt> smtlib_smt_ast::args

◆ boolval

bool smtlib_smt_ast::boolval

◆ extract_high

int smtlib_smt_ast::extract_high

◆ extract_low

int smtlib_smt_ast::extract_low

◆ intval

BigInt smtlib_smt_ast::intval

◆ kind

smt_func_kind smtlib_smt_ast::kind

◆ realval

std::string smtlib_smt_ast::realval

◆ symname

std::string smtlib_smt_ast::symname

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

src/solvers/smtlib/smtlib_conv.h
src/solvers/smtlib/smtlib_conv.cpp

Public Member Functions

Public Attributes