context Class Reference

A Context manages all other Z3 objects, global configuration options, etc. More...

#include <z3++.h>

Public Member Functions
	context ()
	context (config &c)
	context (context &&other) noexcept
context &	operator= (context &&other) noexcept
	~context ()
	operator Z3_context () const
Z3_error_code	check_error () const
	Auxiliary method used to check for API usage errors.
void	check_parser_error () const
void	set_enable_exceptions (bool f)
	The C++ API uses by defaults exceptions on errors. For applications that don't work well with exceptions (there should be only few) you have the ability to turn off exceptions. The tradeoffs are that applications have to be very careful about using check_error() after calls that may result in an erroneous state.
bool	enable_exceptions () const
void	set (char const *param, char const *value)
	Update global parameter param with string value.
void	set (char const *param, bool value)
	Update global parameter param with Boolean value.
unsigned	num_simplifiers () const
std::string	simplifier_name (unsigned i) const
std::string	simplifier_description (char const *name) const
void	set (char const *param, int value)
	Update global parameter param with Integer value.
void	interrupt ()
	Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actually stop.
symbol	str_symbol (char const *s)
	Create a Z3 symbol based on the given string.
symbol	int_symbol (int n)
	Create a Z3 symbol based on the given integer.
sort	bool_sort ()
	Return the Boolean sort.
sort	int_sort ()
	Return the integer sort.
sort	real_sort ()
	Return the Real sort.
sort	complex_sort ()
	Return the Complex sort (pairs of Reals).
sort	finite_field_sort (char const *prime)
	Return the prime finite-field sort with the given decimal modulus.
sort	bv_sort (unsigned sz)
	Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.
sort	char_sort ()
	Return the sort for Unicode characters.
sort	string_sort ()
	Return the sort for Unicode strings.
sort	seq_sort (sort &s)
	Return a sequence sort over base sort s.
sort	re_sort (sort &seq_sort)
	Return a regular expression sort over sequences seq_sort.
sort	finite_set_sort (sort &s)
	Return a finite set sort over element sort s.
sort	array_sort (sort d, sort r)
	Return an array sort for arrays from d to r.
sort	array_sort (sort_vector const &d, sort r)
sort	fpa_sort (unsigned ebits, unsigned sbits)
	Return a floating point sort. ebits is a number of exponent bits, sbits is a number of significand bits,.
template<size_t precision>
sort	fpa_sort ()
	Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).
sort	fpa_rounding_mode_sort ()
	Return a RoundingMode sort.
void	set_rounding_mode (rounding_mode rm)
	Sets RoundingMode of FloatingPoints.
sort	enumeration_sort (char const *name, unsigned n, char const *const *enum_names, func_decl_vector &cs, func_decl_vector &ts)
	Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. cs and ts are output parameters. The method stores in cs the constants corresponding to the enumerated elements, and in ts the predicates for testing if terms of the enumeration sort correspond to an enumeration.
func_decl	tuple_sort (char const *name, unsigned n, char const *const *names, sort const *sorts, func_decl_vector &projs)
	Return a tuple constructor. name is the name of the returned constructor, n are the number of arguments, names and sorts are their projected sorts. projs is an output parameter. It contains the set of projection functions.
sort	datatype (symbol const &name, constructors const &cs)
	Create a recursive datatype over a single sort. name is the name of the recursive datatype n - the number of constructors of the datatype cs - the n constructors used to define the datatype.
sort	datatype (symbol const &name, sort_vector const &params, constructors const &cs)
	Create a parametric recursive datatype. name is the name of the recursive datatype params - the sort parameters of the datatype cs - the n constructors used to define the datatype References to the datatype and mutually recursive datatypes can be created using datatype_sort.
sort_vector	datatypes (unsigned n, symbol const *names, constructor_list *const *cons)
	Create a set of mutually recursive datatypes. n - number of recursive datatypes names - array of names of length n cons - array of constructor lists of length n.
sort	datatype_sort (symbol const &name)
	a reference to a recursively defined datatype. Expect that it gets defined as a datatype.
sort	datatype_sort (symbol const &name, sort_vector const &params)
	a reference to a recursively defined parametric datatype. Expect that it gets defined as a datatype.
sort	uninterpreted_sort (char const *name)
	create an uninterpreted sort with the name given by the string or symbol.
sort	uninterpreted_sort (symbol const &name)
func_decl	function (symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl	function (char const *name, unsigned arity, sort const *domain, sort const &range)
func_decl	function (symbol const &name, sort_vector const &domain, sort const &range)
func_decl	function (char const *name, sort_vector const &domain, sort const &range)
func_decl	function (char const *name, sort const &domain, sort const &range)
func_decl	function (char const *name, sort const &d1, sort const &d2, sort const &range)
func_decl	function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &range)
func_decl	function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &range)
func_decl	function (char const *name, sort const &d1, sort const &d2, sort const &d3, sort const &d4, sort const &d5, sort const &range)
func_decl	recfun (symbol const &name, unsigned arity, sort const *domain, sort const &range)
func_decl	recfun (symbol const &name, const sort_vector &domain, sort const &range)
func_decl	recfun (char const *name, sort_vector const &domain, sort const &range)
func_decl	recfun (char const *name, unsigned arity, sort const *domain, sort const &range)
func_decl	recfun (char const *name, sort const &domain, sort const &range)
func_decl	recfun (char const *name, sort const &d1, sort const &d2, sort const &range)
void	recdef (func_decl decl, expr_vector const &args, expr const &body)
	add function definition body to declaration decl. decl needs to be declared using context::recfun.
func_decl	user_propagate_function (symbol const &name, sort_vector const &domain, sort const &range)
expr	constant (symbol const &name, sort const &s)
	create an uninterpreted constant.
expr	constant (char const *name, sort const &s)
expr	bool_const (char const *name)
	create uninterpreted constants of a given sort.
expr	int_const (char const *name)
expr	real_const (char const *name)
expr	complex_const (char const *name)
expr	string_const (char const *name)
expr	bv_const (char const *name, unsigned sz)
expr	fpa_const (char const *name, unsigned ebits, unsigned sbits)
template<size_t precision>
expr	fpa_const (char const *name)
expr	variable (unsigned index, sort const &s)
	create a de-Bruijn variable.
expr	fpa_rounding_mode ()
expr	bool_val (bool b)
expr	int_val (int n)
expr	int_val (unsigned n)
expr	int_val (int64_t n)
expr	int_val (uint64_t n)
expr	int_val (char const *n)
expr	real_val (int n)
expr	real_val (unsigned n)
expr	real_val (int64_t n)
expr	real_val (uint64_t n)
expr	real_val (int64_t n, int64_t d)
expr	real_val (char const *n)
expr	complex_val (int re, int im=0)
expr	complex_val (char const *re, char const *im="0")
expr	bv_val (int n, unsigned sz)
expr	bv_val (unsigned n, unsigned sz)
expr	bv_val (int64_t n, unsigned sz)
expr	bv_val (uint64_t n, unsigned sz)
expr	bv_val (char const *n, unsigned sz)
expr	bv_val (unsigned n, bool const *bits)
expr	fpa_val (double n)
expr	fpa_val (float n)
expr	fpa_nan (sort const &s)
expr	fpa_inf (sort const &s, bool sgn)
expr	string_val (char const *s)
expr	string_val (char const *s, unsigned n)
expr	string_val (std::string const &s)
expr	string_val (std::u32string const &s)
expr	num_val (int n, sort const &s)
expr_vector	parse_string (char const *s)
	parsing
expr_vector	parse_file (char const *file)
expr_vector	parse_string (char const *s, sort_vector const &sorts, func_decl_vector const &decls)
expr_vector	parse_file (char const *s, sort_vector const &sorts, func_decl_vector const &decls)
template<>
sort	fpa_sort ()
template<>
sort	fpa_sort ()
template<>
sort	fpa_sort ()
template<>
sort	fpa_sort ()

Friends
class	user_propagator_base

Detailed Description

A Context manages all other Z3 objects, global configuration options, etc.

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

Constructor & Destructor Documentation

context() [1/3]

context ( )

inline

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

{ config c; init(c); }

context() [2/3]

context ( config &  c )

inline

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

{ init(c); }

context() [3/3]

context ( context &&  other )

inlinenoexcept

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

            : m_enable_exceptions(other.m_enable_exceptions),
              m_rounding_mode(other.m_rounding_mode),
              m_ctx(other.m_ctx) {
            other.m_ctx = nullptr;
        }

~context()

~context ( )

inline

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

{ if (m_ctx) Z3_del_context(m_ctx); }

Member Function Documentation

array_sort() [1/2]

sort array_sort ( sort  d, sort  r  )

inline

Return an array sort for arrays from d to r.

Example: Given a context c, c.array_sort(c.int_sort(), c.bool_sort()) is an array sort from integer to Boolean.

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

{ Z3_sort s = Z3_mk_array_sort(m_ctx, d, r); check_error(); return sort(*this, s); }

array_sort() [2/2]

sort array_sort ( sort_vector const &  d, sort  r  )

inline

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

                                                                {
        array<Z3_sort> dom(d);
        Z3_sort s = Z3_mk_array_sort_n(m_ctx, dom.size(), dom.ptr(), r); check_error(); return sort(*this, s);
    }

bool_const()

expr bool_const ( char const *  name )

inline

create uninterpreted constants of a given sort.

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

{ return constant(name, bool_sort()); }

bool_sort()

sort bool_sort ( )

inline

Return the Boolean sort.

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

{ Z3_sort s = Z3_mk_bool_sort(m_ctx); check_error(); return sort(*this, s); }

Referenced by context::bool_const().

bool_val()

expr bool_val ( bool  b )

inline

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

{ return b ? expr(*this, Z3_mk_true(m_ctx)) : expr(*this, Z3_mk_false(m_ctx)); }

Referenced by goal::as_expr(), user_propagator_base::conflict(), user_propagator_base::conflict(), and solver::to_smt2().

bv_const()

expr bv_const ( char const *  name, unsigned  sz  )

inline

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

{ return constant(name, bv_sort(sz)); }

bv_sort()

sort bv_sort ( unsigned  sz )

inline

Return the Bit-vector sort of size sz. That is, the sort for bit-vectors of size sz.

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

{ Z3_sort s = Z3_mk_bv_sort(m_ctx, sz); check_error(); return sort(*this, s); }

Referenced by context::bv_const(), context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), and context::bv_val().

bv_val() [1/6]

expr bv_val ( char const *  n, unsigned  sz  )

inline

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

{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_numeral(m_ctx, n, s); check_error(); return expr(*this, r); }

bv_val() [2/6]

expr bv_val ( int  n, unsigned  sz  )

inline

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

{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }

bv_val() [3/6]

expr bv_val ( int64_t  n, unsigned  sz  )

inline

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

{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_int64(m_ctx, n, s); check_error(); return expr(*this, r); }

bv_val() [4/6]

expr bv_val ( uint64_t  n, unsigned  sz  )

inline

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

{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, s); check_error(); return expr(*this, r); }

bv_val() [5/6]

expr bv_val ( unsigned  n, bool const *  bits  )

inline

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

                                                            {
        array<bool> _bits(n);
        for (unsigned i = 0; i < n; ++i) _bits[i] = bits[i] ? 1 : 0;
        Z3_ast r = Z3_mk_bv_numeral(m_ctx, n, _bits.ptr()); check_error(); return expr(*this, r);
    }

bv_val() [6/6]

expr bv_val ( unsigned  n, unsigned  sz  )

inline

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

{ sort s = bv_sort(sz); Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, s); check_error(); return expr(*this, r); }

char_sort()

sort char_sort ( )

inline

Return the sort for Unicode characters.

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

{ Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }

check_error()

Z3_error_code check_error ( ) const

inline

Auxiliary method used to check for API usage errors.

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

                                          {
            Z3_error_code e = Z3_get_error_code(m_ctx);
            if (e != Z3_OK && enable_exceptions())
                Z3_THROW(exception(Z3_get_error_msg(m_ctx, e)));
            return e;
        }

Referenced by context::array_sort(), context::array_sort(), expr::bit2bool(), context::bool_sort(), context::bv_sort(), context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), context::bv_val(), context::char_sort(), object::check_error(), context::check_parser_error(), context::complex_sort(), context::constant(), context::datatype(), context::datatype(), context::datatype_sort(), context::datatype_sort(), context::enumeration_sort(), expr::ext_rotate_left(), expr::ext_rotate_right(), expr::extract(), context::finite_field_sort(), context::finite_set_sort(), z3::foldl(), z3::foldli(), context::fpa_inf(), context::fpa_nan(), context::fpa_rounding_mode_sort(), context::fpa_sort(), context::fpa_val(), context::fpa_val(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::int_sort(), context::int_symbol(), context::int_val(), context::int_val(), context::int_val(), context::int_val(), context::int_val(), z3::map(), z3::mapi(), context::num_simplifiers(), context::num_val(), on_clause::on_clause(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), func_decl::operator()(), context::parse_file(), context::parse_file(), context::parse_string(), context::parse_string(), parser_context::parse_string(), z3::re_diff(), z3::re_intersect(), context::re_sort(), context::real_sort(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), context::recfun(), context::recfun(), expr::repeat(), expr::rotate_left(), expr::rotate_right(), context::seq_sort(), context::simplifier_description(), context::simplifier_name(), context::str_symbol(), context::string_sort(), context::string_val(), context::string_val(), context::string_val(), context::string_val(), z3::to_expr(), z3::to_func_decl(), z3::to_sort(), context::tuple_sort(), context::user_propagate_function(), and context::variable().

check_parser_error()

void check_parser_error ( ) const

inline

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

                                        {
            check_error();
        }

Referenced by solver::from_file(), and solver::from_string().

complex_const()

expr complex_const ( char const *  name )

inline

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

{ return constant(name, complex_sort()); }

complex_sort()

sort complex_sort ( )

inline

Return the Complex sort (pairs of Reals).

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

{ Z3_sort s = Z3_mk_complex_sort(m_ctx); check_error(); return sort(*this, s); }

Referenced by context::complex_const().

complex_val() [1/2]

expr complex_val ( char const *  re, char const *  im = "0"  )

inline

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

                                                                   {
        expr r = real_val(re);
        expr i = real_val(im);
        return complex(r, i);
    }

complex_val() [2/2]

expr complex_val ( int  re, int  im = 0  )

inline

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

                                                   {
        expr r = real_val(re);
        expr i = real_val(im);
        return complex(r, i);
    }

constant() [1/2]

expr constant ( char const *  name, sort const &  s  )

inline

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

{ return constant(str_symbol(name), s); }

constant() [2/2]

expr constant ( symbol const &  name, sort const &  s  )

inline

create an uninterpreted constant.

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

                                                                     {
        Z3_ast r = Z3_mk_const(m_ctx, name, s);
        check_error();
        return expr(*this, r);
    }

Referenced by context::bool_const(), context::bv_const(), context::complex_const(), context::constant(), context::fpa_const(), context::fpa_const(), context::int_const(), context::real_const(), and context::string_const().

datatype() [1/2]

sort datatype ( symbol const &  name, constructors const &  cs  )

inline

Create a recursive datatype over a single sort. name is the name of the recursive datatype n - the number of constructors of the datatype cs - the n constructors used to define the datatype.

References to the datatype can be created using datatype_sort.

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

                                                                            {
        array<Z3_constructor> _cs(cs.size());
        for (unsigned i = 0; i < cs.size(); ++i) _cs[i] = cs[i];
        Z3_sort s = Z3_mk_datatype(*this, name, cs.size(), _cs.ptr());
        check_error();
        return sort(*this, s);
    }

datatype() [2/2]

sort datatype ( symbol const &  name, sort_vector const &  params, constructors const &  cs  )

inline

Create a parametric recursive datatype. name is the name of the recursive datatype params - the sort parameters of the datatype cs - the n constructors used to define the datatype References to the datatype and mutually recursive datatypes can be created using datatype_sort.

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

                                                                                                       {
        array<Z3_sort> _params(params);
        array<Z3_constructor> _cs(cs.size());
        for (unsigned i = 0; i < cs.size(); ++i)
            _cs[i] = cs[i];
        Z3_sort s = Z3_mk_polymorphic_datatype(*this, name, _params.size(), _params.ptr(), cs.size(), _cs.ptr());
        check_error();
        return sort(*this, s);
    }

datatype_sort() [1/2]

sort datatype_sort ( symbol const &  name )

inline

a reference to a recursively defined datatype. Expect that it gets defined as a datatype.

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

                                                         {
        Z3_sort s = Z3_mk_datatype_sort(*this, name, 0, nullptr);
        check_error();
        return sort(*this, s);            
    }

datatype_sort() [2/2]

sort datatype_sort ( symbol const &  name, sort_vector const &  params  )

inline

a reference to a recursively defined parametric datatype. Expect that it gets defined as a datatype.

Parameters

name	name of the datatype
params	sort parameters

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

                                                                                    {
        array<Z3_sort> _params(params);
        Z3_sort s = Z3_mk_datatype_sort(*this, name, _params.size(), _params.ptr());
        check_error();
        return sort(*this, s);            
    }

datatypes()

sort_vector datatypes ( unsigned  n, symbol const *  names, constructor_list *const *  cons  )

inline

Create a set of mutually recursive datatypes. n - number of recursive datatypes names - array of names of length n cons - array of constructor lists of length n.

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

                                       {
        sort_vector result(*this);
        array<Z3_symbol> _names(n);
        array<Z3_sort> _sorts(n);
        array<Z3_constructor_list> _cons(n);
        for (unsigned i = 0; i < n; ++i)
            _names[i] = names[i], _cons[i] = *cons[i];
        Z3_mk_datatypes(*this, n, _names.ptr(), _sorts.ptr(), _cons.ptr());
        for (unsigned i = 0; i < n; ++i)
            result.push_back(sort(*this, _sorts[i]));
        return result;
    }

enable_exceptions()

bool enable_exceptions ( ) const

inline

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

{ return m_enable_exceptions; }

Referenced by context::check_error().

enumeration_sort()

sort enumeration_sort ( char const *  name, unsigned  n, char const *const *  enum_names, func_decl_vector &  cs, func_decl_vector &  ts  )

inline

Return an enumeration sort: enum_names[0], ..., enum_names[n-1]. cs and ts are output parameters. The method stores in cs the constants corresponding to the enumerated elements, and in ts the predicates for testing if terms of the enumeration sort correspond to an enumeration.

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

                                                                                                                                                      {
        array<Z3_symbol> _enum_names(n);
        for (unsigned i = 0; i < n; ++i) { _enum_names[i] = Z3_mk_string_symbol(*this, enum_names[i]); }
        array<Z3_func_decl> _cs(n);
        array<Z3_func_decl> _ts(n);
        Z3_symbol _name = Z3_mk_string_symbol(*this, name);
        sort s = to_sort(*this, Z3_mk_enumeration_sort(*this, _name, n, _enum_names.ptr(), _cs.ptr(), _ts.ptr()));
        check_error();
        for (unsigned i = 0; i < n; ++i) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
        return s;
    }

finite_field_sort()

sort finite_field_sort ( char const *  prime )

inline

Return the prime finite-field sort with the given decimal modulus.

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

{ Z3_sort s = Z3_mk_finite_field_sort(m_ctx, prime); check_error(); return sort(*this, s); }

finite_set_sort()

sort finite_set_sort ( sort &  s )

inline

Return a finite set sort over element sort s.

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

{ Z3_sort r = Z3_mk_finite_set_sort(m_ctx, s); check_error(); return sort(*this, r); }

fpa_const() [1/2]

template<size_t precision>

expr fpa_const ( char const *  name )

inline

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

{ return constant(name, fpa_sort<precision>()); }

fpa_const() [2/2]

expr fpa_const ( char const *  name, unsigned  ebits, unsigned  sbits  )

inline

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

{ return constant(name, fpa_sort(ebits, sbits)); }

fpa_inf()

expr fpa_inf ( sort const &  s, bool  sgn  )

inline

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

{ Z3_ast r = Z3_mk_fpa_inf(m_ctx, s, sgn); check_error(); return expr(*this, r); }

fpa_nan()

expr fpa_nan ( sort const &  s )

inline

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

{ Z3_ast r = Z3_mk_fpa_nan(m_ctx, s); check_error(); return expr(*this, r); }

fpa_rounding_mode()

expr fpa_rounding_mode ( )

inline

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

                                           {
        switch (m_rounding_mode) {
        case RNA: return expr(*this, Z3_mk_fpa_rna(m_ctx));
        case RNE: return expr(*this, Z3_mk_fpa_rne(m_ctx));
        case RTP: return expr(*this, Z3_mk_fpa_rtp(m_ctx));
        case RTN: return expr(*this, Z3_mk_fpa_rtn(m_ctx));
        case RTZ: return expr(*this, Z3_mk_fpa_rtz(m_ctx));
        }
        assert(false);
        return expr(*this, Z3_mk_fpa_rne(m_ctx));
    }

fpa_rounding_mode_sort()

sort fpa_rounding_mode_sort ( )

inline

Return a RoundingMode sort.

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

{ Z3_sort r = Z3_mk_fpa_rounding_mode_sort(m_ctx); check_error(); return sort(*this, r); }

fpa_sort() [1/6]

template<size_t precision>

sort fpa_sort

(

)

Return a FloatingPoint sort with given precision bitwidth (16, 32, 64 or 128).

Referenced by context::fpa_const().

fpa_sort() [2/6]

template<>

sort fpa_sort ( )

inline

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

{ return fpa_sort(5, 11); }

Referenced by context::fpa_sort().

fpa_sort() [3/6]

template<>

sort fpa_sort ( )

inline

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

{ return fpa_sort(8, 24); }

Referenced by context::fpa_sort().

fpa_sort() [4/6]

template<>

sort fpa_sort ( )

inline

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

{ return fpa_sort(11, 53); }

Referenced by context::fpa_sort().

fpa_sort() [5/6]

template<>

sort fpa_sort ( )

inline

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

{ return fpa_sort(15, 113); }

Referenced by context::fpa_sort().

fpa_sort() [6/6]

sort fpa_sort ( unsigned  ebits, unsigned  sbits  )

inline

Return a floating point sort. ebits is a number of exponent bits, sbits is a number of significand bits,.

Precondition

where ebits must be larger than 1 and sbits must be larger than 2.

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

{ Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }

fpa_val() [1/2]

expr fpa_val ( double  n )

inline

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

{ sort s = fpa_sort<64>(); Z3_ast r = Z3_mk_fpa_numeral_double(m_ctx, n, s); check_error(); return expr(*this, r); }

fpa_val() [2/2]

expr fpa_val ( float  n )

inline

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

{ sort s = fpa_sort<32>(); Z3_ast r = Z3_mk_fpa_numeral_float(m_ctx, n, s); check_error(); return expr(*this, r); }

function() [1/9]

func_decl function ( char const *  name, sort const &  d1, sort const &  d2, sort const &  d3, sort const &  d4, sort const &  d5, sort const &  range  )

inline

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

                                                                                                                                                                 {
        check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range); check_context(d5, range);
        Z3_sort args[5] = { d1, d2, d3, d4, d5 };
        Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 5, args, range);
        check_error();
        return func_decl(*this, f);
    }

function() [2/9]

func_decl function ( char const *  name, sort const &  d1, sort const &  d2, sort const &  d3, sort const &  d4, sort const &  range  )

inline

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

                                                                                                                                                {
        check_context(d1, range); check_context(d2, range); check_context(d3, range); check_context(d4, range);
        Z3_sort args[4] = { d1, d2, d3, d4 };
        Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 4, args, range);
        check_error();
        return func_decl(*this, f);
    }

function() [3/9]

func_decl function ( char const *  name, sort const &  d1, sort const &  d2, sort const &  d3, sort const &  range  )

inline

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

                                                                                                                               {
        check_context(d1, range); check_context(d2, range); check_context(d3, range);
        Z3_sort args[3] = { d1, d2, d3 };
        Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 3, args, range);
        check_error();
        return func_decl(*this, f);
    }

function() [4/9]

func_decl function ( char const *  name, sort const &  d1, sort const &  d2, sort const &  range  )

inline

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

                                                                                                              {
        check_context(d1, range); check_context(d2, range);
        Z3_sort args[2] = { d1, d2 };
        Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 2, args, range);
        check_error();
        return func_decl(*this, f);
    }

function() [5/9]

func_decl function ( char const *  name, sort const &  domain, sort const &  range  )

inline

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

                                                                                                 {
        check_context(domain, range);
        Z3_sort args[1] = { domain };
        Z3_func_decl f = Z3_mk_func_decl(m_ctx, str_symbol(name), 1, args, range);
        check_error();
        return func_decl(*this, f);
    }

function() [6/9]

func_decl function ( char const *  name, sort_vector const &  domain, sort const &  range  )

inline

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

                                                                                                      {
        return function(range.ctx().str_symbol(name), domain, range);
    }

function() [7/9]

func_decl function ( char const *  name, unsigned  arity, sort const *  domain, sort const &  range  )

inline

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

                                                                                                                 {
        return function(range.ctx().str_symbol(name), arity, domain, range);
    }

function() [8/9]

func_decl function ( symbol const &  name, sort_vector const &  domain, sort const &  range  )

inline

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

                                                                                                       {
        array<Z3_sort> args(domain.size());
        for (unsigned i = 0; i < domain.size(); ++i) {
            check_context(domain[i], range);
            args[i] = domain[i];
        }
        Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, domain.size(), args.ptr(), range);
        check_error();
        return func_decl(*this, f);
    }

function() [9/9]

func_decl function ( symbol const &  name, unsigned  arity, sort const *  domain, sort const &  range  )

inline

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

                                                                                                                   {
        array<Z3_sort> args(arity);
        for (unsigned i = 0; i < arity; ++i) {
            check_context(domain[i], range);
            args[i] = domain[i];
        }
        Z3_func_decl f = Z3_mk_func_decl(m_ctx, name, arity, args.ptr(), range);
        check_error();
        return func_decl(*this, f);
    }

Referenced by z3::function(), z3::function(), z3::function(), z3::function(), z3::function(), context::function(), z3::function(), context::function(), z3::function(), z3::function(), and z3::function().

int_const()

expr int_const ( char const *  name )

inline

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

{ return constant(name, int_sort()); }

int_sort()

sort int_sort ( )

inline

Return the integer sort.

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

{ Z3_sort s = Z3_mk_int_sort(m_ctx); check_error(); return sort(*this, s); }

Referenced by context::int_const(), context::int_val(), context::int_val(), context::int_val(), context::int_val(), and context::int_val().

int_symbol()

symbol int_symbol ( int  n )

inline

Create a Z3 symbol based on the given integer.

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

{ Z3_symbol r = Z3_mk_int_symbol(m_ctx, n); check_error(); return symbol(*this, r); }

int_val() [1/5]

expr int_val ( char const *  n )

inline

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

{ Z3_ast r = Z3_mk_numeral(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

int_val() [2/5]

expr int_val ( int  n )

inline

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

{ Z3_ast r = Z3_mk_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

int_val() [3/5]

expr int_val ( int64_t  n )

inline

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

{ Z3_ast r = Z3_mk_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

int_val() [4/5]

expr int_val ( uint64_t  n )

inline

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

{ Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

int_val() [5/5]

expr int_val ( unsigned  n )

inline

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

{ Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, int_sort()); check_error(); return expr(*this, r); }

interrupt()

void interrupt ( )

inline

Interrupt the current procedure being executed by any object managed by this context. This is a soft interruption: there is no guarantee the object will actually stop.

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

{ Z3_interrupt(m_ctx); }

num_simplifiers()

unsigned num_simplifiers ( ) const

inline

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

                                         {
            unsigned r = Z3_get_num_simplifiers(m_ctx);
            check_error();
            return r;
        }

num_val()

expr num_val ( int  n, sort const &  s  )

inline

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

{ Z3_ast r = Z3_mk_int(m_ctx, n, s); check_error(); return expr(*this, r); }

Referenced by func_decl::operator()(), func_decl::operator()(), and func_decl::operator()().

operator Z3_context()

operator Z3_context ( ) const

inline

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

{ return m_ctx; }

operator=()

context & operator= ( context &&  other )

inlinenoexcept

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

                                                       {
            if (this != &other) {
                if (m_ctx) Z3_del_context(m_ctx);
                m_enable_exceptions = other.m_enable_exceptions;
                m_rounding_mode = other.m_rounding_mode;
                m_ctx = other.m_ctx;
                other.m_ctx = nullptr;
            }
            return *this;
        }

parse_file() [1/2]

expr_vector parse_file ( char const *  file )

inline

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

                                                        {
        Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, 0, 0, 0, 0, 0, 0);
        check_error();
        return expr_vector(*this, r);
    }

parse_file() [2/2]

expr_vector parse_file ( char const *  s, sort_vector const &  sorts, func_decl_vector const &  decls  )

inline

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

                                                                                                                 {
        array<Z3_symbol> sort_names(sorts.size());
        array<Z3_symbol> decl_names(decls.size());
        array<Z3_sort>   sorts1(sorts);
        array<Z3_func_decl> decls1(decls);
        for (unsigned i = 0; i < sorts.size(); ++i) {
            sort_names[i] = sorts[i].name();
        }
        for (unsigned i = 0; i < decls.size(); ++i) {
            decl_names[i] = decls[i].name();
        }
        Z3_ast_vector r = Z3_parse_smtlib2_file(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
        check_error();
        return expr_vector(*this, r);
    }

parse_string() [1/2]

expr_vector parse_string ( char const *  s )

inline

parsing

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

                                                          {
        Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, 0, 0, 0, 0, 0, 0);
        check_error();
        return expr_vector(*this, r);
 
    }

parse_string() [2/2]

expr_vector parse_string ( char const *  s, sort_vector const &  sorts, func_decl_vector const &  decls  )

inline

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

                                                                                                                   {
        array<Z3_symbol> sort_names(sorts.size());
        array<Z3_symbol> decl_names(decls.size());
        array<Z3_sort>   sorts1(sorts);
        array<Z3_func_decl> decls1(decls);
        for (unsigned i = 0; i < sorts.size(); ++i) {
            sort_names[i] = sorts[i].name();
        }
        for (unsigned i = 0; i < decls.size(); ++i) {
            decl_names[i] = decls[i].name();
        }
 
        Z3_ast_vector r = Z3_parse_smtlib2_string(*this, s, sorts.size(), sort_names.ptr(), sorts1.ptr(), decls.size(), decl_names.ptr(), decls1.ptr());
        check_error();
        return expr_vector(*this, r);
    }

re_sort()

sort re_sort ( sort &  seq_sort )

inline

Return a regular expression sort over sequences seq_sort.

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

{ Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }

real_const()

expr real_const ( char const *  name )

inline

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

{ return constant(name, real_sort()); }

real_sort()

sort real_sort ( )

inline

Return the Real sort.

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

{ Z3_sort s = Z3_mk_real_sort(m_ctx); check_error(); return sort(*this, s); }

Referenced by context::real_const(), context::real_val(), context::real_val(), context::real_val(), context::real_val(), and context::real_val().

real_val() [1/6]

expr real_val ( char const *  n )

inline

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

{ Z3_ast r = Z3_mk_numeral(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

real_val() [2/6]

expr real_val ( int  n )

inline

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

{ Z3_ast r = Z3_mk_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

Referenced by context::complex_val(), and context::complex_val().

real_val() [3/6]

expr real_val ( int64_t  n )

inline

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

{ Z3_ast r = Z3_mk_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

real_val() [4/6]

expr real_val ( int64_t  n, int64_t  d  )

inline

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

{ Z3_ast r = Z3_mk_real_int64(m_ctx, n, d); check_error(); return expr(*this, r); }

real_val() [5/6]

expr real_val ( uint64_t  n )

inline

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

{ Z3_ast r = Z3_mk_unsigned_int64(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

real_val() [6/6]

expr real_val ( unsigned  n )

inline

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

{ Z3_ast r = Z3_mk_unsigned_int(m_ctx, n, real_sort()); check_error(); return expr(*this, r); }

recdef()

void recdef ( func_decl  decl, expr_vector const &  args, expr const &  body  )

inline

add function definition body to declaration decl. decl needs to be declared using context::recfun.

Parameters

decl
args
body

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

                                                                                      {
        check_context(f, args); check_context(f, body);
        array<Z3_ast> vars(args);
        Z3_add_rec_def(f.ctx(), f, vars.size(), vars.ptr(), body);
    }

recfun() [1/6]

func_decl recfun ( char const *  name, sort const &  d1, sort const &  d2, sort const &  range  )

inline

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

                                                                                                          {
        sort dom[2] = { d1, d2 };
        return recfun(str_symbol(name), 2, dom, range);
    }

recfun() [2/6]

func_decl recfun ( char const *  name, sort const &  domain, sort const &  range  )

inline

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

                                                                                          {
        return recfun(str_symbol(name), 1, &d1, range);
    }

recfun() [3/6]

func_decl recfun ( char const *  name, sort_vector const &  domain, sort const &  range  )

inline

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

                                                                                                     {
        return recfun(str_symbol(name), domain, range);
 
    }

recfun() [4/6]

func_decl recfun ( char const *  name, unsigned  arity, sort const *  domain, sort const &  range  )

inline

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

                                                                                                               {
        return recfun(str_symbol(name), arity, domain, range);
    }

recfun() [5/6]

func_decl recfun ( symbol const &  name, const sort_vector &  domain, sort const &  range  )

inline

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

                                                                                                       {
        check_context(domain, range);
        array<Z3_sort> domain1(domain);
        Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, domain1.size(), domain1.ptr(), range);
        check_error();
        return func_decl(*this, f);
    }

recfun() [6/6]

func_decl recfun ( symbol const &  name, unsigned  arity, sort const *  domain, sort const &  range  )

inline

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

                                                                                                                 {
        array<Z3_sort> args(arity);
        for (unsigned i = 0; i < arity; ++i) {
            check_context(domain[i], range);
            args[i] = domain[i];
        }
        Z3_func_decl f = Z3_mk_rec_func_decl(m_ctx, name, arity, args.ptr(), range);
        check_error();
        return func_decl(*this, f);
 
    }

Referenced by context::recfun(), z3::recfun(), z3::recfun(), context::recfun(), context::recfun(), context::recfun(), z3::recfun(), and z3::recfun().

seq_sort()

sort seq_sort ( sort &  s )

inline

Return a sequence sort over base sort s.

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

{ Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }

set() [1/3]

void set ( char const *  param, bool  value  )

inline

Update global parameter param with Boolean value.

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

{ Z3_update_param_value(m_ctx, param, value ? "true" : "false"); }

set() [2/3]

void set ( char const *  param, char const *  value  )

inline

Update global parameter param with string value.

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

{ Z3_update_param_value(m_ctx, param, value); }

set() [3/3]

void set ( char const *  param, int  value  )

inline

Update global parameter param with Integer value.

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

                                                {
            auto str = std::to_string(value);
            Z3_update_param_value(m_ctx, param, str.c_str());
        }

set_enable_exceptions()

void set_enable_exceptions ( bool  f )

inline

The C++ API uses by defaults exceptions on errors. For applications that don't work well with exceptions (there should be only few) you have the ability to turn off exceptions. The tradeoffs are that applications have to be very careful about using check_error() after calls that may result in an erroneous state.

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

{ m_enable_exceptions = f; }

set_rounding_mode()

void set_rounding_mode ( rounding_mode  rm )

inline

Sets RoundingMode of FloatingPoints.

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

{ m_rounding_mode = rm; }

simplifier_description()

std::string simplifier_description ( char const *  name ) const

inline

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

                                                                 {
            char const* r = Z3_simplifier_get_descr(m_ctx, name);
            check_error();
            return r;
        }

simplifier_name()

std::string simplifier_name ( unsigned  i ) const

inline

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

                                                    {
            char const* r = Z3_get_simplifier_name(m_ctx, i);
            check_error();
            return r;
        }

str_symbol()

symbol str_symbol ( char const *  s )

inline

Create a Z3 symbol based on the given string.

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

{ Z3_symbol r = Z3_mk_string_symbol(m_ctx, s); check_error(); return symbol(*this, r); }

Referenced by context::constant(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::function(), context::recfun(), context::recfun(), context::recfun(), context::recfun(), and solver::solver().

string_const()

expr string_const ( char const *  name )

inline

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

{ return constant(name, string_sort()); }

string_sort()

sort string_sort ( )

inline

Return the sort for Unicode strings.

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

{ Z3_sort s = Z3_mk_string_sort(m_ctx); check_error(); return sort(*this, s); }

Referenced by context::string_const().

string_val() [1/4]

expr string_val ( char const *  s )

inline

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

{ Z3_ast r = Z3_mk_string(m_ctx, s); check_error(); return expr(*this, r); }

string_val() [2/4]

expr string_val ( char const *  s, unsigned  n  )

inline

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

{ Z3_ast r = Z3_mk_lstring(m_ctx, n, s); check_error(); return expr(*this, r); }

string_val() [3/4]

expr string_val ( std::string const &  s )

inline

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

{ Z3_ast r = Z3_mk_string(m_ctx, s.c_str()); check_error(); return expr(*this, r); }

string_val() [4/4]

expr string_val ( std::u32string const &  s )

inline

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

{ Z3_ast r = Z3_mk_u32string(m_ctx, (unsigned)s.size(), (unsigned const*)s.c_str()); check_error(); return expr(*this, r); }

tuple_sort()

func_decl tuple_sort ( char const *  name, unsigned  n, char const *const *  names, sort const *  sorts, func_decl_vector &  projs  )

inline

Return a tuple constructor. name is the name of the returned constructor, n are the number of arguments, names and sorts are their projected sorts. projs is an output parameter. It contains the set of projection functions.

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

                                                                                                                                               {
        array<Z3_symbol> _names(n);
        array<Z3_sort> _sorts(n);
        for (unsigned i = 0; i < n; ++i) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
        array<Z3_func_decl> _projs(n);
        Z3_symbol _name = Z3_mk_string_symbol(*this, name);
        Z3_func_decl tuple;
        sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
        check_error();
        for (unsigned i = 0; i < n; ++i) { projs.push_back(func_decl(*this, _projs[i])); }
        return func_decl(*this, tuple);
    }

uninterpreted_sort() [1/2]

sort uninterpreted_sort ( char const *  name )

inline

create an uninterpreted sort with the name given by the string or symbol.

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

                                                            {
        Z3_symbol _name = Z3_mk_string_symbol(*this, name);
        return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));
    }

uninterpreted_sort() [2/2]

sort uninterpreted_sort ( symbol const &  name )

inline

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

                                                              {
        return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
    }

user_propagate_function()

func_decl user_propagate_function ( symbol const &  name, sort_vector const &  domain, sort const &  range  )

inline

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

                                                                                                                      {
        check_context(domain, range);
        array<Z3_sort> domain1(domain);
        Z3_func_decl f = Z3_solver_propagate_declare(range.ctx(), name, domain1.size(), domain1.ptr(), range);
        check_error();
        return func_decl(*this, f);
    }

variable()

expr variable ( unsigned  index, sort const &  s  )

inline

create a de-Bruijn variable.

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

                                                             { 
        Z3_ast r = Z3_mk_bound(m_ctx, idx, s);
        check_error();
        return expr(*this, r);
    }

Friends And Related Symbol Documentation

user_propagator_base

friend class user_propagator_base

friend

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