ast_map Class Reference

A map from ASTs to ASTs. More...

#include <z3++.h>

Inheritance diagram for ast_map:

Public Member Functions
	ast_map (context &c)
	ast_map (context &c, Z3_ast_map m)
	ast_map (ast_map const &s)
	~ast_map () override
	operator Z3_ast_map () const
ast_map &	operator= (ast_map const &s)
bool	contains (ast const &k) const
ast	find (ast const &k) const
void	insert (ast const &k, ast const &v)
void	erase (ast const &k)
void	reset ()
unsigned	size () const
ast_vector	keys () const
Public Member Functions inherited from object
	object (context &c)
virtual	~object ()=default
context &	ctx () const
Z3_error_code	check_error () const

Additional Inherited Members
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

A map from ASTs to ASTs.

Definition at line 743 of file z3++.h.

Constructor & Destructor Documentation

ast_map() [1/3]

ast_map ( context &  c )

inline

Definition at line 750 of file z3++.h.

: object(c) { init(Z3_mk_ast_map(c)); }

ast_map() [2/3]

ast_map ( context &  c, Z3_ast_map  m  )

inline

Definition at line 751 of file z3++.h.

: object(c) { init(m); }

ast_map() [3/3]

ast_map ( ast_map const &  s )

inline

Definition at line 752 of file z3++.h.

: object(s) { init(s.m_map); }

~ast_map()

~ast_map ( )

inlineoverride

Definition at line 753 of file z3++.h.

{ Z3_ast_map_dec_ref(ctx(), m_map); }

Member Function Documentation

contains()

bool contains ( ast const &  k ) const

inline

Definition at line 762 of file z3++.h.

                                          {
            check_context(*this, k);
            bool r = Z3_ast_map_contains(ctx(), m_map, k);
            check_error();
            return r;
        }

erase()

void erase ( ast const &  k )

inline

Definition at line 779 of file z3++.h.

                                 {
            check_context(*this, k);
            Z3_ast_map_erase(ctx(), m_map, k);
            check_error();
        }

find()

ast find ( ast const &  k ) const

inline

Definition at line 768 of file z3++.h.

                                     {
            check_context(*this, k);
            Z3_ast r = Z3_ast_map_find(ctx(), m_map, k);
            check_error();
            return ast(ctx(), r);
        }

insert()

void insert ( ast const &  k, ast const &  v  )

inline

Definition at line 774 of file z3++.h.

                                                {
            check_context(*this, k); check_context(*this, v);
            Z3_ast_map_insert(ctx(), m_map, k, v);
            check_error();
        }

keys()

ast_vector keys ( ) const

inline

Definition at line 790 of file z3++.h.

                                {
            Z3_ast_vector r = Z3_ast_map_keys(ctx(), m_map);
            check_error();
            return ast_vector(ctx(), r);
        }

operator Z3_ast_map()

operator Z3_ast_map ( ) const

inline

Definition at line 754 of file z3++.h.

{ return m_map; }

operator=()

ast_map & operator= ( ast_map const &  s )

inline

Definition at line 755 of file z3++.h.

                                             {
            Z3_ast_map_inc_ref(s.ctx(), s.m_map);
            Z3_ast_map_dec_ref(ctx(), m_map);
            object::operator=(s);
            m_map = s.m_map;
            return *this;
        }

reset()

void reset ( )

inline

Definition at line 784 of file z3++.h.

{ Z3_ast_map_reset(ctx(), m_map); check_error(); }

size()

unsigned size ( ) const

inline

Definition at line 785 of file z3++.h.

                              {
            unsigned r = Z3_ast_map_size(ctx(), m_map);
            check_error();
            return r;
        }

Referenced by ParamDescrsRef::__len__(), Goal::__len__(), BitVecNumRef::as_signed_long(), and BitVecSortRef::subsort().