parser_context Class Reference

#include <z3++.h>

Inheritance diagram for parser_context:

Public Member Functions
	parser_context (context &c)
	~parser_context () override
	operator bool () const
	operator Z3_parser_context () const
	parser_context (const parser_context &o)
parser_context &	operator= (const parser_context &o)
void	add_sort (const sort &s)
	Add a sort declaration.
void	add_sort (const func_decl &f)
	Add a function declaration.
expr_vector	parse_string (const char *s)
	Parse a string of SMTLIB2 commands. Return assertions.
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

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

Constructor & Destructor Documentation

parser_context() [1/2]

parser_context ( context &  c )

inlineexplicit

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

:object(c), m_pc(Z3_mk_parser_context(c)) { Z3_parser_context_inc_ref(ctx(), m_pc); }

~parser_context()

~parser_context ( )

inlineoverride

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

{ if (m_pc) Z3_parser_context_dec_ref(ctx(), m_pc); }

parser_context() [2/2]

parser_context ( const parser_context &  o )

inline

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

:object(o), m_pc(o.m_pc) { Z3_parser_context_inc_ref(ctx(), m_pc); }

Member Function Documentation

add_sort() [1/2]

void add_sort ( const func_decl &  f )

inline

Add a function declaration.

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

{ Z3_parser_context_add_decl(ctx(), m_pc, f); check_error(); }

add_sort() [2/2]

void add_sort ( const sort &  s )

inline

Add a sort declaration.

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

{ Z3_parser_context_add_sort(ctx(), m_pc, s); check_error(); }

operator bool()

operator bool ( ) const

inlineexplicit

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

{ return m_pc; }

operator Z3_parser_context()

operator Z3_parser_context ( ) const

inline

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

{ return m_pc; }

operator=()

parser_context & operator= ( const parser_context &  o )

inline

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

                                                           {
            if (this != &o) {
                if (m_pc) Z3_parser_context_dec_ref(*m_ctx, m_pc);
                Z3_parser_context_inc_ref(*o.m_ctx, o.m_pc);
                object::operator=(o);
                m_pc = o.m_pc;
            }
            return *this;
        }

parse_string()

expr_vector parse_string ( const char *  s )

inline

Parse a string of SMTLIB2 commands. Return assertions.

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

                                                 {
            auto result = Z3_parser_context_from_string(ctx(), m_pc, s);
            m_ctx->check_error();
            return expr_vector(ctx(), result);
        }