simplifier Class Reference

#include <z3++.h>

Inheritance diagram for simplifier:

Public Member Functions
	simplifier (context &c, char const *name)
	simplifier (context &c, Z3_simplifier s)
	simplifier (simplifier const &s)
	~simplifier () override
	operator Z3_simplifier () const
simplifier &	operator= (simplifier const &s)
std::string	help () const
param_descrs	get_param_descrs ()
Public Member Functions inherited from object
	object (context &c)
virtual	~object ()=default
context &	ctx () const
Z3_error_code	check_error () const

Friends
simplifier	operator& (simplifier const &t1, simplifier const &t2)
simplifier	with (simplifier const &t, params const &p)

Additional Inherited Members
Protected Attributes inherited from object
context *	m_ctx

Detailed Description

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

Constructor & Destructor Documentation

simplifier() [1/3]

simplifier ( context &  c, char const *  name  )

inline

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

:object(c) { Z3_simplifier r = Z3_mk_simplifier(c, name); check_error(); init(r); }

simplifier() [2/3]

simplifier ( context &  c, Z3_simplifier  s  )

inline

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

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

simplifier() [3/3]

simplifier ( simplifier const &  s )

inline

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

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

~simplifier()

~simplifier ( )

inlineoverride

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

{ Z3_simplifier_dec_ref(ctx(), m_simplifier); }

Member Function Documentation

get_param_descrs()

param_descrs get_param_descrs ( )

inline

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

{ return param_descrs(ctx(), Z3_simplifier_get_param_descrs(ctx(), m_simplifier)); }

help()

std::string help ( ) const

inline

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

{ char const * r = Z3_simplifier_get_help(ctx(), m_simplifier); check_error();  return r; }

operator Z3_simplifier()

operator Z3_simplifier ( ) const

inline

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

{ return m_simplifier; }

operator=()

simplifier & operator= ( simplifier const &  s )

inline

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

                                                     {
            Z3_simplifier_inc_ref(s.ctx(), s.m_simplifier);
            Z3_simplifier_dec_ref(ctx(), m_simplifier);
            object::operator=(s);
            m_simplifier = s.m_simplifier;
            return *this;
        }

Friends And Related Symbol Documentation

operator&

simplifier operator& ( simplifier const &  t1, simplifier const &  t2  )

friend

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

                                                                              {
        check_context(t1, t2);
        Z3_simplifier r = Z3_simplifier_and_then(t1.ctx(), t1, t2);
        t1.check_error();
        return simplifier(t1.ctx(), r);
    }

with

simplifier with ( simplifier const &  t, params const &  p  )

friend

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

                                                                   {
        Z3_simplifier r = Z3_simplifier_using_params(t.ctx(), t, p);
        t.check_error();
        return simplifier(t.ctx(), r);
    }