z3_smt_ast Class Reference

#include <z3_conv.h>

Inheritance diagram for z3_smt_ast:

Public Member Functions
	~z3_smt_ast () override=default
smt_astt	update (smt_solver_baset *ctx, smt_astt value, unsigned int idx, const expr2tc &idx_expr) const override
	Abstractly produce an "update", i.e., an array 'with' or tuple 'with'.
smt_astt	project (smt_solver_baset *ctx, unsigned int elem) const override
	Project a member from a structure, or an field-array from a struct array.
void	dump () const override
Public Member Functions inherited from solver_smt_ast< z3::expr >
	solver_smt_ast (smt_solver_baset *ctx, z3::expr _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	select (smt_solver_baset *ctx, const expr2tc &idx) const
	Select a value from an array, for both normal arrays and tuple arrays.

Additional Inherited Members
Public Types inherited from solver_smt_ast< z3::expr >
typedef z3::expr	solver_ast_type
Public Attributes inherited from solver_smt_ast< z3::expr >
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

~z3_smt_ast()

z3_smt_ast::~z3_smt_ast ( )

overridedefault

Member Function Documentation

dump()

void z3_smt_ast::dump ( ) const

overridevirtual

Reimplemented from smt_ast.

project()

smt_astt z3_smt_ast::project ( smt_solver_baset * ctx, unsigned int elem ) const

overridevirtual

Project a member from a structure, or an field-array from a struct array.

Parameters

ctx	SMT context to produce this in.
elem	Struct index to project.

Returns

AST representing the chosen element / element-array

Reimplemented from smt_ast.

update()

smt_astt z3_smt_ast::update ( smt_solver_baset * ctx, smt_astt value, unsigned int idx, const expr2tc & idx_expr ) const

overridevirtual

Abstractly produce an "update", i.e., an array 'with' or tuple 'with'.

Parameters

ctx	SMT context to make this update in.
value	Value to insert into the updated field
idx	Array index or tuple field
idx_expr	If an array, expression representing the index

Returns

AST of this type, representing the update

Reimplemented from smt_ast.

---

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

• src/solvers/z3/z3_conv.h
• src/solvers/z3/z3_conv.cpp