bitw_smt_ast Class Reference

#include <bitwuzla_conv.h>

Inheritance diagram for bitw_smt_ast:

Public Member Functions
	~bitw_smt_ast () override=default
smt_astt	with_sort (smt_solver_baset *ctx, smt_sortt s) const override
	The same solver term under a different sort.
void	dump () const override
Public Member Functions inherited from solver_smt_ast< bitwuzla::Term >
	solver_smt_ast (smt_solver_baset *ctx, bitwuzla::Term _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	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< bitwuzla::Term >
typedef bitwuzla::Term	solver_ast_type
Public Attributes inherited from solver_smt_ast< bitwuzla::Term >
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

~bitw_smt_ast()

bitw_smt_ast::~bitw_smt_ast ( )

overridedefault

Member Function Documentation

dump()

void bitw_smt_ast::dump ( ) const

overridevirtual

Reimplemented from smt_ast.

with_sort()

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

overridevirtual

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 from smt_ast.

---

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

• src/solvers/bitwuzla/bitwuzla_conv.h
• src/solvers/bitwuzla/bitwuzla_conv.cpp