smt_ast Class Reference

#include <smt_ast.h>

Inheritance diagram for smt_ast:

Public Member Functions
	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
smt_sortt	sort
	The sort of this function application.
const smt_solver_baset *	context
	The solver context.

Constructor & Destructor Documentation

smt_ast()

smt_ast::smt_ast ( smt_solver_baset * ctx, smt_sortt s )

inline

~smt_ast()

virtual smt_ast::~smt_ast ( )

virtualdefault

Member Function Documentation

assign()

void smt_ast::assign ( smt_solver_baset * ctx, smt_astt sym ) const

virtual

Abstractly produce an assign.

Defaults to being an equality, however for some special cases up to the backend, there may be optimizations made for array or tuple assigns, and so forth.

Parameters

ctx	SMT context to do the assignment in.
sym	Symbol to assign to

Reimplemented in array_ast, array_sym_smt_ast, tuple_node_smt_ast, and yices_smt_ast.

dump()

virtual void smt_ast::dump ( ) const

inlinevirtual

Reimplemented in array_ast, bitw_smt_ast, btor_smt_ast, cvc5_smt_ast, cvc_smt_ast, mathsat_smt_ast, smtlib_smt_ast, tuple_node_smt_ast, tuple_sym_smt_ast, yices_smt_ast, and z3_smt_ast.

eq()

smt_astt smt_ast::eq ( smt_solver_baset * ctx, smt_astt other ) const

virtual

Abstractly produce an equality.

Does the right thing (TM) whether it's a normal piece of AST or a tuple / array.

Parameters

ctx	SMT context to produce the equality in.
other	Piece of AST to compare 'this' with.

Returns

Boolean typed AST representing an equality

Reimplemented in array_ast, array_sym_smt_ast, tuple_node_smt_ast, and tuple_sym_smt_ast.

ite()

smt_astt smt_ast::ite ( smt_solver_baset * ctx, smt_astt cond, smt_astt falseop ) const

virtual

Reimplemented in array_ast, array_sym_smt_ast, tuple_node_smt_ast, and tuple_sym_smt_ast.

project()

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

virtual

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 in array_sym_smt_ast, tuple_node_smt_ast, tuple_sym_smt_ast, yices_smt_ast, and z3_smt_ast.

select()

smt_astt smt_ast::select ( smt_solver_baset * ctx, const expr2tc & idx ) const

virtual

Select a value from an array, for both normal arrays and tuple arrays.

Parameters

ctx	SMT context to produce this in.
idx	Index to select the value from.

Returns

AST of the array's range sort representing the selected item

Reimplemented in array_ast, array_sym_smt_ast, tuple_node_smt_ast, and tuple_sym_smt_ast.

update()

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

virtual

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 in array_ast, array_sym_smt_ast, tuple_node_smt_ast, tuple_sym_smt_ast, yices_smt_ast, and z3_smt_ast.

with_sort()

smt_astt smt_ast::with_sort ( smt_solver_baset * ctx, smt_sortt s ) const

virtual

The same solver term under a different sort.

The default rewrites this node's sort in place, which is what the bit-vector-only backends have always relied on – there both sorts are the same solver sort. A backend where they are genuinely different solver sorts must return a fresh node, or the rewrite corrupts every other holder of this shared ast.

Reimplemented in bitw_smt_ast.

Member Data Documentation

context

const smt_solver_baset* smt_ast::context

The solver context.

sort

smt_sortt smt_ast::sort

The sort of this function application.

---

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

• src/solvers/smt/smt_ast.h
• src/solvers/smt/smt_solver.cpp
• src/solvers/smt/smt_solver.h